List Subcommand (Implementation)

kani-compiler/src/args.rs

@@ -47,6 +47,9 @@ pub struct Arguments {
  pub reachability_analysis: ReachabilityType,
  #[clap(long = "enable-stubbing")]
  pub stubbing_enabled: bool,
+ /// Option name used to tell the compiler to execute the list subcommand
+ #[clap(long = "list")]
+ pub list_enabled: bool,
  /// Option name used to define unstable features.
  #[clap(short = 'Z', long = "unstable")]
  pub unstable_features: Vec<String>,

kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs

@@ -2,14 +2,15 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use crate::codegen_cprover_gotoc::{codegen::ty_stable::pointee_type_stable, GotocCtx};
 use crate::kani_middle::attributes::KaniAttributes;
+use crate::kani_middle::find_closure_in_body;
 use cbmc::goto_program::FunctionContract;
 use cbmc::goto_program::{Expr, Lambda, Location, Type};
 use kani_metadata::AssignsContract;
 use rustc_hir::def_id::DefId as InternalDefId;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::{Instance, MonoItem};
-use stable_mir::mir::{Local, VarDebugInfoContents};
-use stable_mir::ty::{FnDef, RigidTy, TyKind};
+use stable_mir::mir::Local;
+use stable_mir::ty::{RigidTy, TyKind};
 use stable_mir::CrateDef;
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -87,33 +88,24 @@ impl<'tcx> GotocCtx<'tcx> {
  recursion_tracker
  }
 
+ fn find_closure(&mut self, inside: Instance, name: &str) -> Option<Instance> {
+ let body = self.transformer.body(self.tcx, inside);
+ find_closure_in_body(&body, name)
+ }
+
  /// Find the modifies recursively since we may have a recursion wrapper.
  /// I.e.: [recursion_wrapper ->]? check -> modifies.
  fn find_modifies(&mut self, instance: Instance) -> Option<Instance> {
  let contract_attrs =
  KaniAttributes::for_instance(self.tcx, instance).contract_attributes()?;
- let mut find_closure = |inside: Instance, name: &str| {
- let body = self.transformer.body(self.tcx, inside);
- body.var_debug_info.iter().find_map(|var_info| {
- if var_info.name.as_str() == name {
- let ty = match &var_info.value {
- VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(),
- VarDebugInfoContents::Const(const_op) => const_op.ty(),
- };
- if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() {
- return Some(Instance::resolve(FnDef(def.def_id()), &args).unwrap());
- }
- }
- None
- })
- };
  let check_instance = if contract_attrs.has_recursion {
- let recursion_check = find_closure(instance, contract_attrs.recursion_check.as_str())?;
- find_closure(recursion_check, contract_attrs.checked_with.as_str())?
+ let recursion_check =
+ self.find_closure(instance, contract_attrs.recursion_check.as_str())?;
+ self.find_closure(recursion_check, contract_attrs.checked_with.as_str())?
  } else {
- find_closure(instance, contract_attrs.checked_with.as_str())?
+ self.find_closure(instance, contract_attrs.checked_with.as_str())?
  };
- find_closure(check_instance, contract_attrs.modifies_wrapper.as_str())
+ self.find_closure(check_instance, contract_attrs.modifies_wrapper.as_str())
  }
 
  /// Convert the Kani level contract into a CBMC level contract by creating a

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -9,6 +9,7 @@ use crate::kani_middle::analysis;
 use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes};
 use crate::kani_middle::check_reachable_items;
 use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits};
+use crate::kani_middle::list::collect_contracted_fns;
 use crate::kani_middle::metadata::gen_test_metadata;
 use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{
@@ -21,8 +22,7 @@ use cbmc::irep::goto_binary_serde::write_goto_binary_file;
 use cbmc::RoundingMode;
 use cbmc::{InternedString, MachineModel};
 use kani_metadata::artifact::convert_type;
-use kani_metadata::UnsupportedFeature;
-use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
+use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata, UnsupportedFeature};
 use kani_metadata::{AssignsContract, CompilerArtifactStub};
 use rustc_codegen_ssa::back::archive::{ArArchiveBuilder, ArchiveBuilder, DEFAULT_OBJECT_READER};
 use rustc_codegen_ssa::back::metadata::create_wrapper_file;
@@ -342,7 +342,14 @@ impl CodegenBackend for GotocCodegenBackend {
  results.harnesses.push(metadata);
  }
  }
- ReachabilityType::None => {}
+ ReachabilityType::None => {
+ // If the list subcommand is enabled, record the necessary KaniMetadata.
+ if queries.args().list_enabled {
+ let mut units: CodegenUnits = CodegenUnits::new(&queries, tcx);
+ collect_contracted_fns(tcx, &mut units);
+ units.write_metadata(&queries, tcx);
+ }
+ }
  ReachabilityType::PubFns => {
  let unit = CodegenUnit::default();
  let transformer = BodyTransformation::new(&queries, tcx, &unit);
@@ -652,6 +659,10 @@ impl GotoCodegenResults {
  proof_harnesses: proofs,
  unsupported_features,
  test_harnesses: tests,
+ // Just leave contracted_functions empty, since we don't use this field unless we're running the
+ // list subcommand and that uses CodegenUnits::generate_metadata instead.
+ // TODO: should we consolidate these generate_metadata functions?
+ contracted_functions: vec![],
  }
  }
 

kani-compiler/src/kani_middle/attributes.rs

@@ -477,7 +477,7 @@ impl<'tcx> KaniAttributes<'tcx> {
  ///
  /// We only extract attributes for harnesses that are local to the current crate.
  /// Note that all attributes should be valid by now.
- pub fn harness_attributes(&self) -> HarnessAttributes {
+ pub fn harness_attributes(&self, is_list_enabled: bool) -> HarnessAttributes {
  // Abort if not local.
  if !self.item.is_local() {
  panic!("Expected a local item, but got: {:?}", self.item);
@@ -505,7 +505,7 @@ impl<'tcx> KaniAttributes<'tcx> {
  harness.unwind_value = parse_unwind(self.tcx, attributes[0])
  }
  KaniAttributeKind::Proof => { /* no-op */ }
- KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness),
+ KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness, is_list_enabled),
  KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness),
  KaniAttributeKind::Unstable => {
  // Internal attribute which shouldn't exist here.
@@ -531,7 +531,7 @@ impl<'tcx> KaniAttributes<'tcx> {
  })
  }
 
- fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes) {
+ fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes, is_list_enabled: bool) {
  let dcx = self.tcx.dcx();
  let (name, id, span) = match self.interpret_for_contract_attribute() {
  None => return, // This error was already emitted
@@ -540,6 +540,13 @@ impl<'tcx> KaniAttributes<'tcx> {
  assert!(matches!(
  &harness.kind, HarnessKind::ProofForContract { target_fn }
  if *target_fn == name.to_string()));
+
+ // Only emit an error if we are trying to actually verify the contract.
+ // (If we are running the list subcommand, we just report later that there are no contracts for this harness).
+ if is_list_enabled {
+ return;
+ }
+
  if KaniAttributes::for_item(self.tcx, id).contract_attributes().is_none() {
  dcx.struct_span_err(
  span,

kani-compiler/src/kani_middle/codegen_units.rs

@@ -14,7 +14,9 @@ use crate::kani_middle::reachability::filter_crate_items;
 use crate::kani_middle::resolve::expect_resolve_fn;
 use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map};
 use crate::kani_queries::QueryDb;
-use kani_metadata::{ArtifactType, AssignsContract, HarnessKind, HarnessMetadata, KaniMetadata};
+use kani_metadata::{
+ ArtifactType, AssignsContract, ContractedFunction, HarnessKind, HarnessMetadata, KaniMetadata,
+};
 use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::OutputType;
@@ -46,6 +48,7 @@ pub struct CodegenUnits {
  units: Vec<CodegenUnit>,
  harness_info: HashMap<Harness, HarnessMetadata>,
  crate_info: CrateInfo,
+ pub contracted_functions: Vec<ContractedFunction>,
 }
 
 #[derive(Clone, Default, Debug)]
@@ -57,26 +60,46 @@ pub struct CodegenUnit {
 impl CodegenUnits {
  pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self {
  let crate_info = CrateInfo { name: stable_mir::local_crate().name.as_str().into() };
- if queries.args().reachability_analysis == ReachabilityType::Harnesses {
- let base_filepath = tcx.output_filenames(()).path(OutputType::Object);
- let base_filename = base_filepath.as_path();
- let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance));
- let all_harnesses = harnesses
- .into_iter()
- .map(|harness| {
- let metadata = gen_proof_metadata(tcx, harness, &base_filename);
- (harness, metadata)
- })
- .collect::<HashMap<_, _>>();
 
+ if queries.args().reachability_analysis != ReachabilityType::Harnesses
+ && !queries.args().list_enabled
+ {
+ // Leave other reachability type handling as is for now.
+ return CodegenUnits {
+ units: vec![],
+ harness_info: HashMap::default(),
+ crate_info,
+ contracted_functions: vec![],
+ };
+ }
+
+ let base_filepath = tcx.output_filenames(()).path(OutputType::Object);
+ let base_filename = base_filepath.as_path();
+ let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance));
+ let all_harnesses = harnesses
+ .into_iter()
+ .map(|harness| {
+ let metadata =
+ gen_proof_metadata(tcx, harness, &base_filename, queries.args().list_enabled);
+ (harness, metadata)
+ })
+ .collect::<HashMap<_, _>>();
+ let mut units = vec![];
+
+ if queries.args().reachability_analysis == ReachabilityType::Harnesses {
  // Even if no_stubs is empty we still need to store rustc metadata.
- let units = group_by_stubs(tcx, &all_harnesses);
+ units = group_by_stubs(tcx, &all_harnesses);
  validate_units(tcx, &units);
  debug!(?units, "CodegenUnits::new");
- CodegenUnits { units, harness_info: all_harnesses, crate_info }
- } else {
- // Leave other reachability type handling as is for now.
- CodegenUnits { units: vec![], harness_info: HashMap::default(), crate_info }
+ }
+
+ tcx.dcx().abort_if_errors();
+
+ CodegenUnits {
+ units,
+ harness_info: all_harnesses,
+ crate_info,
+ contracted_functions: vec![],
  }
  }
 
@@ -111,6 +134,7 @@ impl CodegenUnits {
  proof_harnesses,
  unsupported_features: vec![],
  test_harnesses,
+ contracted_functions: self.contracted_functions.clone(),
  }
  }
 }
@@ -213,7 +237,6 @@ fn validate_units(tcx: TyCtxt, units: &[CodegenUnit]) {
  tcx.dcx().span_err(rustc_internal::internal(tcx, span), msg);
  }
  }
- tcx.dcx().abort_if_errors();
 }
 
 /// Apply stub transitivity operations.

kani-compiler/src/kani_middle/list.rs

@@ -0,0 +1,100 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Collects contract and contract harness metadata for the list subcommand.
+
+use std::collections::HashMap;
+
+use crate::kani_middle::attributes::{matches_diagnostic as matches_function, KaniAttributes};
+use crate::kani_middle::codegen_units::CodegenUnits;
+use crate::kani_middle::{find_closure_in_body, InternalDefId, SourceLocation};
+use kani_metadata::ContractedFunction;
+use rustc_middle::ty::TyCtxt;
+use rustc_smir::rustc_internal;
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::{Body, TerminatorKind};
+use stable_mir::ty::{RigidTy, TyKind};
+use stable_mir::{CrateDef, CrateItems};
+
+/// Map each function to its contract harnesses
+/// `fns` includes all functions with contracts and all functions that are targets of a contract harness.
+fn fns_to_harnesses(tcx: TyCtxt) -> HashMap<InternalDefId, Vec<String>> {
+ // We work with stable_mir::CrateItem instead of stable_mir::Instance to include generic items
+ let crate_items: CrateItems = stable_mir::all_local_items();
+
+ let mut fns_to_harnesses: HashMap<InternalDefId, Vec<String>> = HashMap::new();
+
+ for item in crate_items {
+ let def_id = rustc_internal::internal(tcx, item.def_id());
+ let fn_name = tcx.def_path_str(def_id);
+ let attributes = KaniAttributes::for_item(tcx, def_id);
+
+ if attributes.has_contract() {
+ fns_to_harnesses.insert(def_id, vec![]);
+ } else if let Some((_, target_def_id, _)) = attributes.interpret_for_contract_attribute() {
+ if let Some(harnesses) = fns_to_harnesses.get_mut(&target_def_id) {
+ harnesses.push(fn_name);
+ } else {
+ fns_to_harnesses.insert(target_def_id, vec![fn_name]);
+ }
+ }
+ }
+
+ fns_to_harnesses
+}
+
+/// Count the number of contracts in `check_body`, where `check_body` is the body of the
+/// kanitool::checked_with closure (c.f. kani_macros::sysroot::contracts).
+/// In this closure, preconditions are denoted by kani::assume() calls and postconditions by kani::assert() calls.
+/// The number of contracts is the number of times these functions are called inside the closure
+fn count_contracts(tcx: TyCtxt, check_body: &Body) -> usize {
+ let mut count = 0;
+
+ for bb in &check_body.blocks {
+ if let TerminatorKind::Call { ref func, .. } = bb.terminator.kind {
+ let fn_ty = func.ty(check_body.locals()).unwrap();
+ if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = fn_ty.kind() {
+ let instance = Instance::resolve(fn_def, &args).unwrap();
+ // For each precondition or postcondition, increment the count
+ if matches_function(tcx, instance.def, "KaniAssume")
+ || matches_function(tcx, instance.def, "KaniAssert")
+ {
+ count += 1;
+ }
+ }
+ }
+ }
+ count
+}
+
+/// For each function with contracts (or that is a target of a contract harness),
+/// construct a ContractedFunction object for it and store it in `units`.
+pub fn collect_contracted_fns(tcx: TyCtxt, units: &mut CodegenUnits) {
+ for (fn_def_id, harnesses) in fns_to_harnesses(tcx) {
+ let attrs = KaniAttributes::for_item(tcx, fn_def_id);
+
+ // It's possible that a function is a target of a proof for contract but does not actually have contracts.
+ // If the function does have contracts, count them.
+ let total_contracts = if attrs.has_contract() {
+ let contract_attrs =
+ KaniAttributes::for_item(tcx, fn_def_id).contract_attributes().unwrap();
+ let body: Body = rustc_internal::stable(tcx.optimized_mir(fn_def_id));
+ let check_body: Body =
+ find_closure_in_body(&body, contract_attrs.checked_with.as_str())
+ .unwrap()
+ .body()
+ .unwrap();
+
+ count_contracts(tcx, &check_body)
+ } else {
+ 0
+ };
+
+ units.contracted_functions.push(ContractedFunction {
+ function: tcx.def_path_str(fn_def_id),
+ file: SourceLocation::new(rustc_internal::stable(tcx.def_span(fn_def_id))).filename,
+ harnesses,
+ total_contracts,
+ });
+ }
+}

kani-compiler/src/kani_middle/metadata.rs

@@ -14,7 +14,12 @@ use stable_mir::CrateDef;
 use super::{attributes::KaniAttributes, SourceLocation};
 
 /// Create the harness metadata for a proof harness for a given function.
-pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata {
+pub fn gen_proof_metadata(
+ tcx: TyCtxt,
+ instance: Instance,
+ base_name: &Path,
+ is_list_enabled: bool,
+) -> HarnessMetadata {
  let def = instance.def;
  let kani_attributes = KaniAttributes::for_instance(tcx, instance);
  let pretty_name = instance.name();
@@ -33,7 +38,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
  original_file: loc.filename,
  original_start_line: loc.start_line,
  original_end_line: loc.end_line,
- attributes: kani_attributes.harness_attributes(),
+ attributes: kani_attributes.harness_attributes(is_list_enabled),
  // TODO: This no longer needs to be an Option.
  goto_file: Some(model_file),
  contract: Default::default(),