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;