Addressing code review comments

Moved contracts code gen functions to separate module
Moved `Pointer` trait to `internal` module
Remove channel based modifies contract communication

cprover_bindings/src/irep/to_irep.rs

@@ -504,15 +504,21 @@ impl ToIrep for SwitchCase {
 }
 
 impl ToIrep for Lambda {
+ /// At the moment this function assumes that this lambda is used for a
+ /// `modifies` contract. It should work for any other lambda body, but
+ /// the parameter names use "modifies" in their generated names.
  fn to_irep(&self, mm: &MachineModel) -> Irep {
  let (ops_ireps, types) = self
  .arguments
  .iter()
- .map(|param| {
+ .enumerate()
+ .map(|(index, param)| {
  let ty_rep = param.typ().to_irep(mm);
  (
- Irep::symbol(param.identifier().unwrap_or("_".into()))
- .with_named_sub(IrepId::Type, ty_rep.clone()),
+ Irep::symbol(
+ param.identifier().unwrap_or_else(|| format!("_modifies_{index}").into()),
+ )
+ .with_named_sub(IrepId::Type, ty_rep.clone()),
  ty_rep,
  )
  })

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

@@ -0,0 +1,117 @@
+use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::kani_middle::attributes::KaniAttributes;
+use cbmc::goto_program::FunctionContract;
+use cbmc::goto_program::Lambda;
+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;
+use stable_mir::CrateDef;
+use tracing::debug;
+
+impl<'tcx> GotocCtx<'tcx> {
+ /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
+ /// find or create the `AssignsContract` that needs to be enforced and attach it to the symbol
+ /// for which it needs to be enforced.
+ ///
+ /// 1. Gets the `#[kanitool::inner_check = "..."]` target, then resolves exactly one instance
+ /// of it. Panics if there are more or less than one instance.
+ /// 2. Expects that a `#[kanitool::modifies(...)]` is placed on the `inner_check` function,
+ /// turns it into a CBMC contract and attaches it to the symbol for the previously resolved
+ /// instance.
+ /// 3. Returns the mangled name of the symbol it attached the contract to.
+ /// 4. Resolves the `#[kanitool::checked_with = "..."]` target from `function_under_contract`
+ /// which has `static mut REENTRY : bool` declared inside.
+ /// 5. Returns the full path to this constant that `--nondet-static-exclude` expects which is
+ /// comprised of the file path that `checked_with` is located in, the name of the
+ /// `checked_with` function and the name of the constant (`REENTRY`).
+ pub fn handle_check_contract(
+ &mut self,
+ function_under_contract: InternalDefId,
+ items: &[MonoItem],
+ ) -> AssignsContract {
+ let tcx = self.tcx;
+ let function_under_contract_attrs = KaniAttributes::for_item(tcx, function_under_contract);
+ let wrapped_fn = function_under_contract_attrs.inner_check().unwrap().unwrap();
+
+ let mut instance_under_contract = items.iter().filter_map(|i| match i {
+ MonoItem::Fn(instance @ Instance { def, .. })
+ if wrapped_fn == rustc_internal::internal(def.def_id()) =>
+ {
+ Some(instance.clone())
+ }
+ _ => None,
+ });
+ let instance_of_check = instance_under_contract.next().unwrap();
+ assert!(
+ instance_under_contract.next().is_none(),
+ "Only one instance of a checked function may be in scope"
+ );
+ let attrs_of_wrapped_fn = KaniAttributes::for_item(tcx, wrapped_fn);
+ let assigns_contract = attrs_of_wrapped_fn.modifies_contract().unwrap_or_else(|| {
+ debug!(?instance_of_check, "had no assigns contract specified");
+ vec![]
+ });
+ self.attach_modifies_contract(instance_of_check, assigns_contract);
+
+ let wrapper_name = self.symbol_name_stable(instance_of_check);
+
+ let recursion_wrapper_id =
+ function_under_contract_attrs.checked_with_id().unwrap().unwrap();
+ let span_of_recursion_wrapper = tcx.def_span(recursion_wrapper_id);
+ let location_of_recursion_wrapper = self.codegen_span(&span_of_recursion_wrapper);
+
+ let full_name = format!(
+ "{}:{}::REENTRY",
+ location_of_recursion_wrapper
+ .filename()
+ .expect("recursion location wrapper should have a file name"),
+ tcx.item_name(recursion_wrapper_id),
+ );
+
+ AssignsContract { recursion_tracker: full_name, contracted_function_name: wrapper_name }
+ }
+
+ /// Convert the Kani level contract into a CBMC level contract by creating a
+ /// CBMC lambda.
+ fn codegen_modifies_contract(&mut self, modified_places: Vec<Local>) -> FunctionContract {
+ let goto_annotated_fn_name = self.current_fn().name();
+ let goto_annotated_fn_typ = self
+ .symbol_table
+ .lookup(&goto_annotated_fn_name)
+ .unwrap_or_else(|| panic!("Function '{goto_annotated_fn_name}' is not declared"))
+ .typ
+ .clone();
+
+ let assigns = modified_places
+ .into_iter()
+ .map(|local| {
+ Lambda::as_contract_for(
+ &goto_annotated_fn_typ,
+ None,
+ self.codegen_place_stable(&local.into()).unwrap().goto_expr.dereference(),
+ )
+ })
+ .collect();
+
+ FunctionContract::new(assigns)
+ }
+
+ /// Convert the contract to a CBMC contract, then attach it to `instance`.
+ /// `instance` must have previously been declared.
+ ///
+ /// This merges with any previously attached contracts.
+ pub fn attach_modifies_contract(&mut self, instance: Instance, modified_places: Vec<Local>) {
+ // This should be safe, since the contract is pretty much evaluated as
+ // though it was the first (or last) assertion in the function.
+ assert!(self.current_fn.is_none());
+ let body = instance.body().unwrap();
+ self.set_current_fn(instance, &body);
+ let goto_contract = self.codegen_modifies_contract(modified_places);
+ let name = self.current_fn().name();
+
+ self.symbol_table.attach_contract(name, goto_contract);
+ self.reset_current_fn()
+ }
+}

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

@@ -4,7 +4,7 @@
 //! This file contains functions related to codegenning MIR functions into gotoc
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use cbmc::goto_program::{Expr, FunctionContract, Stmt, Symbol};
+use cbmc::goto_program::{Expr, Stmt, Symbol};
 use cbmc::InternString;
 use rustc_middle::mir::traversal::reverse_postorder;
 use stable_mir::mir::mono::Instance;
@@ -202,50 +202,6 @@ impl<'tcx> GotocCtx<'tcx> {
  );
  }
 
- /// Convert the Kani level contract into a CBMC level contract by creating a
- /// CBMC lambda.
- fn as_goto_contract(&mut self, assigns_contract: Vec<Local>) -> FunctionContract {
- use cbmc::goto_program::Lambda;
-
- let goto_annotated_fn_name = self.current_fn().name();
- let goto_annotated_fn_typ = self
- .symbol_table
- .lookup(&goto_annotated_fn_name)
- .unwrap_or_else(|| panic!("Function '{goto_annotated_fn_name}' is not declared"))
- .typ
- .clone();
-
- let assigns = assigns_contract
- .into_iter()
- .map(|local| {
- Lambda::as_contract_for(
- &goto_annotated_fn_typ,
- None,
- self.codegen_place_stable(&local.into()).unwrap().goto_expr.dereference(),
- )
- })
- .collect();
-
- FunctionContract::new(assigns)
- }
-
- /// Convert the contract to a CBMC contract, then attach it to `instance`.
- /// `instance` must have previously been declared.
- ///
- /// This merges with any previously attached contracts.
- pub fn attach_contract(&mut self, instance: Instance, contract: Vec<Local>) {
- // This should be safe, since the contract is pretty much evaluated as
- // though it was the first (or last) assertion in the function.
- assert!(self.current_fn.is_none());
- let body = instance.body().unwrap();
- self.set_current_fn(instance, &body);
- let goto_contract = self.as_goto_contract(contract);
- let name = self.current_fn().name();
-
- self.symbol_table.attach_contract(name, goto_contract);
- self.reset_current_fn()
- }
-
  pub fn declare_function(&mut self, instance: Instance) {
  debug!("declaring {}; {:?}", instance.name(), instance);
  let body = instance.body().unwrap();

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

@@ -17,6 +17,7 @@ mod statement;
 mod static_var;
 
 // Visible for all codegen module.
+pub mod contract;
 mod ty_stable;
 pub(super) mod typ;
 

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -31,7 +31,7 @@ use rustc_codegen_ssa::{CodegenResults, CrateInfo};
 use rustc_data_structures::fx::{FxHashMap, FxIndexMap};
 use rustc_data_structures::temp_dir::MaybeTempDir;
 use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
-use rustc_hir::def_id::{DefId, LOCAL_CRATE};
+use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE};
 use rustc_metadata::creader::MetadataLoaderDyn;
 use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
@@ -45,7 +45,7 @@ use rustc_smir::rustc_internal;
 use rustc_target::abi::Endian;
 use rustc_target::spec::PanicStrategy;
 use stable_mir::mir::mono::{Instance, MonoItem};
-use stable_mir::CrateDef;
+use stable_mir::{CrateDef, DefId};
 use std::any::Any;
 use std::collections::BTreeMap;
 use std::collections::HashSet;
@@ -63,22 +63,18 @@ use tracing::{debug, error, info};
 
 pub type UnsupportedConstructs = FxHashMap<InternedString, Vec<Location>>;
 
-pub type ContractInfoChannel = std::sync::mpsc::Sender<(InternedString, AssignsContract)>;
-
 #[derive(Clone)]
 pub struct GotocCodegenBackend {
  /// The query is shared with `KaniCompiler` and it is initialized as part of `rustc`
  /// initialization, which may happen after this object is created.
  /// Since we don't have any guarantees on when the compiler creates the Backend object, neither
  /// in which thread it will be used, we prefer to explicitly synchronize any query access.
  queries: Arc<Mutex<QueryDb>>,
-
- contract_channel: ContractInfoChannel,
 }
 
 impl GotocCodegenBackend {
- pub fn new(queries: Arc<Mutex<QueryDb>>, contract_channel: ContractInfoChannel) -> Self {
- GotocCodegenBackend { queries, contract_channel }
+ pub fn new(queries: Arc<Mutex<QueryDb>>) -> Self {
+ GotocCodegenBackend { queries }
  }
 
  /// Generate code that is reachable from the given starting points.
@@ -90,7 +86,7 @@ impl GotocCodegenBackend {
  starting_items: &[MonoItem],
  symtab_goto: &Path,
  machine_model: &MachineModel,
- check_contract: Option<DefId>,
+ check_contract: Option<InternalDefId>,
  ) -> (GotocCtx<'tcx>, Vec<MonoItem>, Option<AssignsContract>) {
  let items = with_timer(
  || collect_reachable_items(tcx, starting_items),
@@ -192,78 +188,6 @@ impl GotocCodegenBackend {
  }
 }
 
-impl<'tcx> GotocCtx<'tcx> {
- /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
- /// find or create the `AssignsContract` that needs to be enforced and attach it to the symbol
- /// for which it needs to be enforced.
- ///
- /// 1. Gets the `#[kanitool::inner_check = "..."]` target, then resolves exactly one instance
- /// of it. Panics if there are more or less than one instance.
- /// 2. Expects that a `#[kanitool::modifies(...)]` is placed on the `inner_check` function,
- /// turns it into a CBMC contract and attaches it to the symbol for the previously resolved
- /// instance.
- /// 3. Returns the mangled name of the symbol it attached the contract to.
- /// 4. Resolves the `#[kanitool::checked_with = "..."]` target from `function_under_contract`
- /// which has `static mut REENTRY : bool` declared inside.
- /// 5. Returns the full path to this constant that `--nondet-static-exclude` expects which is
- /// comprised of the file path that `checked_with` is located in, the name of the
- /// `checked_with` function and the name of the constant (`REENTRY`).
- fn handle_check_contract(
- &mut self,
- function_under_contract: DefId,
- items: &[MonoItem],
- ) -> AssignsContract {
- let tcx = self.tcx;
- let function_under_contract_attrs = KaniAttributes::for_item(tcx, function_under_contract);
- let wrapped_fn = function_under_contract_attrs.inner_check().unwrap().unwrap();
-
- let mut instance_under_contract = items.iter().filter_map(|i| match i {
- MonoItem::Fn(instance @ Instance { def, .. })
- if wrapped_fn == rustc_internal::internal(def.def_id()) =>
- {
- Some(instance.clone())
- }
- _ => None,
- });
- let instance_of_check = instance_under_contract.next().unwrap();
- assert!(
- instance_under_contract.next().is_none(),
- "Only one instance of a checked function may be in scope"
- );
- let attrs_of_wrapped_fn = KaniAttributes::for_item(tcx, wrapped_fn);
- let assigns_contract = attrs_of_wrapped_fn.modifies_contract().unwrap_or_else(|| {
- debug!(?instance_of_check, "had no assigns contract specified");
- vec![]
- });
- self.attach_contract(instance_of_check, assigns_contract);
-
- let wrapper_name = self.symbol_name_stable(instance_of_check);
-
- let recursion_wrapper_id =
- function_under_contract_attrs.checked_with_id().unwrap().unwrap();
- let span_of_recursion_wrapper = tcx.def_span(recursion_wrapper_id);
- let location_of_recursion_wrapper = self.codegen_span(&span_of_recursion_wrapper);
-
- let full_name = format!(
- "{}:{}::REENTRY",
- location_of_recursion_wrapper
- .filename()
- .expect("recursion location wrapper should have a file name"),
- tcx.item_name(recursion_wrapper_id),
- );
-
- AssignsContract { recursion_tracker: full_name, contracted_function_name: wrapper_name }
- }
-}
-
-fn contract_metadata_for_harness(
- tcx: TyCtxt,
- def_id: DefId,
-) -> Result<Option<DefId>, ErrorGuaranteed> {
- let attrs = KaniAttributes::for_item(tcx, def_id);
- Ok(attrs.interpret_the_for_contract_attribute().transpose()?.map(|(_, id, _)| id))
-}
-
 impl CodegenBackend for GotocCodegenBackend {
  fn metadata_loader(&self) -> Box<MetadataLoaderDyn> {
  Box::new(rustc_codegen_ssa::back::metadata::DefaultMetadataLoader)
@@ -317,12 +241,8 @@ impl CodegenBackend for GotocCodegenBackend {
  for harness in harnesses {
  let model_path =
  queries.harness_model_path(&harness.mangled_name()).unwrap();
- let Ok(contract_metadata) = contract_metadata_for_harness(
- tcx,
- rustc_internal::internal(harness.def.def_id()),
- ) else {
- continue;
- };
+ let contract_metadata =
+ contract_metadata_for_harness(tcx, harness.def.def_id()).unwrap();
  let (gcx, items, contract_info) = self.codegen_items(
  tcx,
  &[MonoItem::Fn(harness)],
@@ -332,9 +252,10 @@ impl CodegenBackend for GotocCodegenBackend {
  );
  results.extend(gcx, items, None);
  if let Some(assigns_contract) = contract_info {
- self.contract_channel
- .send((harness.name().intern(), assigns_contract))
- .unwrap();
+ self.queries
+ .lock()
+ .unwrap()
+ .add_modifies_contract(harness.name().intern(), assigns_contract);
  }
  }
  }
@@ -497,6 +418,14 @@ impl CodegenBackend for GotocCodegenBackend {
  }
 }
 
+fn contract_metadata_for_harness(
+ tcx: TyCtxt,
+ def_id: DefId,
+) -> Result<Option<InternalDefId>, ErrorGuaranteed> {
+ let attrs = KaniAttributes::for_def_id(tcx, def_id);
+ Ok(attrs.interpret_the_for_contract_attribute().transpose()?.map(|(_, id, _)| id))
+}
+
 fn check_target(session: &Session) {
  // The requirement below is needed to build a valid CBMC machine model
  // in function `machine_model_from_session` from

kani-compiler/src/codegen_cprover_gotoc/mod.rs

@@ -6,6 +6,6 @@ mod context;
 mod overrides;
 mod utils;
 
-pub use compiler_interface::{ContractInfoChannel, GotocCodegenBackend, UnsupportedConstructs};
+pub use compiler_interface::{GotocCodegenBackend, UnsupportedConstructs};
 pub use context::GotocCtx;
 pub use context::VtableCtx;