generate identical contract harnesses to manual ones

Author: Carolyn Zech

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -42,8 +42,8 @@ use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
 use rustc_smir::rustc_internal;
 use rustc_target::spec::PanicStrategy;
+use stable_mir::CrateDef;
 use stable_mir::mir::mono::{Instance, MonoItem};
-use stable_mir::{CrateDef, DefId};
 use std::any::Any;
 use std::collections::BTreeMap;
 use std::fmt::Write;
@@ -212,6 +212,27 @@ impl GotocCodegenBackend {
 
         (gcx, items, contract_info)
     }
+
+    /// Given a contract harness, get the DefId of its target.
+    /// For manual harnesses, extract it from the #[proof_for_contract] attribute.
+    /// For automatic harnesses, extract the target from the harness's GenericArgs.
+    fn target_def_id_for_harness(
+        &self,
+        tcx: TyCtxt,
+        harness: &Instance,
+        is_automatic_harness: bool,
+    ) -> Option<InternalDefId> {
+        if is_automatic_harness {
+            let kind = harness.args().0[0].expect_ty().kind();
+            let (fn_to_verify_def, _) = kind.fn_def().unwrap();
+            let def_id = fn_to_verify_def.def_id();
+            let attrs = KaniAttributes::for_def_id(tcx, def_id);
+            if attrs.has_contract() { Some(rustc_internal::internal(tcx, def_id)) } else { None }
+        } else {
+            let harness_attrs = KaniAttributes::for_def_id(tcx, harness.def.def_id());
+            harness_attrs.interpret_for_contract_attribute().map(|(_, id, _)| id)
+        }
+    }
 }
 
 impl CodegenBackend for GotocCodegenBackend {
@@ -275,8 +296,9 @@ impl CodegenBackend for GotocCodegenBackend {
                         for harness in &unit.harnesses {
                             let transformer = BodyTransformation::new(&queries, tcx, &unit);
                             let model_path = units.harness_model_path(*harness).unwrap();
+                            let is_automatic_harness = units.is_automatic_harness(harness);
                             let contract_metadata =
-                                contract_metadata_for_harness(tcx, harness.def.def_id());
+                                self.target_def_id_for_harness(tcx, harness, is_automatic_harness);
                             let (gcx, items, contract_info) = self.codegen_items(
                                 tcx,
                                 &[MonoItem::Fn(*harness)],
@@ -453,11 +475,6 @@ impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder {
     }
 }
 
-fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option<InternalDefId> {
-    let attrs = KaniAttributes::for_def_id(tcx, def_id);
-    attrs.interpret_for_contract_attribute().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/kani_middle/codegen_units.rs

@@ -133,6 +133,10 @@ impl CodegenUnits {
         self.units.iter()
     }
 
+    pub fn is_automatic_harness(&self, harness: &Harness) -> bool {
+        self.harness_info.get(harness).is_some_and(|md| md.is_automatically_generated)
+    }
+
     /// We store which instance of modifies was generated.
     pub fn store_modifies(&mut self, harness_modifies: &[(Harness, AssignsContract)]) {
         for (harness, modifies) in harness_modifies {

kani-compiler/src/kani_middle/transform/automatic.rs

@@ -7,21 +7,24 @@
 //! then transform its body to be a harness for that function.
 
 use crate::args::ReachabilityType;
+use crate::kani_middle::attributes::KaniAttributes;
 use crate::kani_middle::codegen_units::CodegenUnit;
-use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel};
+use crate::kani_middle::kani_functions::{KaniHook, KaniIntrinsic, KaniModel};
 use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction};
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
+use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
-use stable_mir::mir::{Body, Operand, Place, TerminatorKind};
-use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs};
+use stable_mir::mir::{Body, Mutability, Operand, Place, TerminatorKind};
+use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, RigidTy, Ty};
 use tracing::debug;
 
 #[derive(Debug)]
 pub struct AutomaticHarnessPass {
     /// The FnDef of KaniModel::Any
     kani_any: FnDef,
+    init_contracts_hook: Instance,
     /// All of the automatic harness Instances that we generated in the CodegenUnits constructor
     automatic_harnesses: Vec<Instance>,
 }
@@ -37,6 +40,9 @@ impl AutomaticHarnessPass {
         let kani_fns = query_db.kani_functions();
         let harness_intrinsic = *kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap();
         let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap();
+        let init_contracts_hook = *kani_fns.get(&KaniHook::InitContracts.into()).unwrap();
+        let init_contracts_hook =
+            Instance::resolve(init_contracts_hook, &GenericArgs(vec![])).unwrap();
         let automatic_harnesses = unit
             .harnesses
             .iter()
@@ -46,7 +52,7 @@ impl AutomaticHarnessPass {
                 def == harness_intrinsic
             })
             .collect::<Vec<_>>();
-        Self { kani_any, automatic_harnesses }
+        Self { kani_any, init_contracts_hook, automatic_harnesses }
     }
 }
 
@@ -65,7 +71,7 @@ impl TransformPass for AutomaticHarnessPass {
         matches!(query_db.args().reachability_analysis, ReachabilityType::AllFns)
     }
 
-    fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+    fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
         debug!(function=?instance.name(), "AutomaticHarnessPass::transform");
 
         if !self.automatic_harnesses.contains(&instance) {
@@ -83,6 +89,23 @@ impl TransformPass for AutomaticHarnessPass {
         harness_body.clear_body(TerminatorKind::Return);
         let mut source = SourceInstruction::Terminator { bb: 0 };
 
+        // Contract harnesses need a free(NULL) statement, c.f. kani_core::init_contracts().
+        let attrs = KaniAttributes::for_def_id(tcx, def.def_id());
+        if attrs.has_contract() {
+            let ret_local = harness_body.new_local(
+                Ty::from_rigid_kind(RigidTy::Tuple(vec![])),
+                source.span(harness_body.blocks()),
+                Mutability::Not,
+            );
+            harness_body.insert_call(
+                &self.init_contracts_hook,
+                &mut source,
+                InsertPosition::Before,
+                vec![],
+                Place::from(ret_local),
+            );
+        }
+
         let mut arg_locals = vec![];
 
         // For each argument of `fn_to_verify`, create a nondeterministic value of its type