Reviving havoc protection for reentry tracker

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -37,8 +37,8 @@ use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
 use rustc_middle::mir::mono::MonoItem;
+use rustc_middle::ty::{self, Instance, InstanceDef, ParamEnv, TyCtxt};
 use rustc_middle::util::Providers;
-use rustc_middle::ty::{Instance, InstanceDef, TyCtxt};
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::cstore::MetadataLoaderDyn;
 use rustc_session::output::out_filename;
@@ -82,7 +82,7 @@ impl GotocCodegenBackend {
         starting_items: &[MonoItem<'tcx>],
         symtab_goto: &Path,
         machine_model: &MachineModel,
-        mut check_contract: Option<DefId>,
+        check_contract: Option<DefId>,
     ) -> (GotocCtx<'tcx>, Vec<MonoItem<'tcx>>) {
         let items = with_timer(
             || collect_reachable_items(tcx, starting_items),
@@ -146,25 +146,38 @@ impl GotocCodegenBackend {
                     }
                 }
 
-                if let Some(did) = &mut check_contract {
-                    let attrs = KaniAttributes::for_item(tcx, *did);
-                    *did = attrs.inner_check().unwrap().unwrap()
-                }
+                check_contract.map(|check_contract_def| {
+                    let check_contract_attrs = KaniAttributes::for_item(tcx, check_contract_def);
+                    let wrapper_def = check_contract_attrs.inner_check().unwrap().unwrap();
 
-                let mut instances_of_check = items.iter().copied().filter_map(|i| match i {
-                    MonoItem::Fn(instance @ Instance { def: InstanceDef::Item(did), .. }) => (check_contract == Some(did)).then_some(instance),
-                    _ => None
-                });
-                let instance_of_check = instances_of_check.next().unwrap();
-                assert!(instances_of_check.next().is_none());
-                let attrs = KaniAttributes::for_item(tcx, instance_of_check.def_id());
-                let assigns_contract = attrs.modifies_contract().unwrap_or_else(|| {
-                    debug!(?instance_of_check, "had no assigns contract specified");
-                    vec![]
-                });
-                gcx.attach_contract(instance_of_check, assigns_contract);
+                    let mut instances_of_check = items.iter().copied().filter_map(|i| match i {
+                        MonoItem::Fn(instance @ Instance { def: InstanceDef::Item(did), .. }) => {
+                            (wrapper_def == did).then_some(instance)
+                        }
+                        _ => None,
+                    });
+                    let instance_of_check = instances_of_check.next().unwrap();
+                    assert!(instances_of_check.next().is_none());
+                    let attrs = KaniAttributes::for_item(tcx, instance_of_check.def_id());
+                    let assigns_contract = attrs.modifies_contract().unwrap_or_else(|| {
+                        debug!(?instance_of_check, "had no assigns contract specified");
+                        vec![]
+                    });
+                    gcx.attach_contract(instance_of_check, assigns_contract);
+
+                    let tracker_def = check_contract_attrs.recursion_tracker().unwrap().unwrap();
+                    let tracker_instance = Instance::expect_resolve(
+                        tcx,
+                        ParamEnv::reveal_all(),
+                        tracker_def,
+                        ty::List::empty(),
+                    );
 
-                tcx.symbol_name(instance_of_check).to_string()
+                    (
+                        tcx.symbol_name(instance_of_check).to_string(),
+                        tcx.symbol_name(tracker_instance).to_string(),
+                    )
+                })
             },
             "codegen",
         );

kani-compiler/src/kani_middle/attributes.rs

@@ -60,6 +60,7 @@ enum KaniAttributeKind {
     IsContractGenerated,
     Modifies,
     InnerCheck,
+    RecursionTracker,
 }
 
 impl KaniAttributeKind {
@@ -77,6 +78,7 @@ impl KaniAttributeKind {
             | KaniAttributeKind::ReplacedWith
             | KaniAttributeKind::CheckedWith
             | KaniAttributeKind::Modifies
+            | KaniAttributeKind::RecursionTracker
             | KaniAttributeKind::InnerCheck
             | KaniAttributeKind::IsContractGenerated => false,
         }
@@ -222,6 +224,10 @@ impl<'tcx> KaniAttributes<'tcx> {
             .map(|target| expect_key_string_value(self.tcx.sess, target))
     }
 
+    pub fn recursion_tracker(&self) -> Option<Result<DefId, ErrorGuaranteed>> {
+        self.eval_sibling_attribute(KaniAttributeKind::RecursionTracker)
+    }
+
     fn eval_sibling_attribute(
         &self,
         kind: KaniAttributeKind,
@@ -340,6 +346,9 @@ impl<'tcx> KaniAttributes<'tcx> {
                 KaniAttributeKind::InnerCheck => {
                     self.inner_check();
                 }
+                KaniAttributeKind::RecursionTracker => {
+                    self.recursion_tracker();
+                }
             }
         }
     }
@@ -443,6 +452,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                 | KaniAttributeKind::IsContractGenerated
                 | KaniAttributeKind::Modifies
                 | KaniAttributeKind::InnerCheck
+                | KaniAttributeKind::RecursionTracker
                 | KaniAttributeKind::ReplacedWith => {
                     self.tcx.sess.span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref()));
                 }
@@ -498,7 +508,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                     .span_note(
                         self.tcx.def_span(def_id),
                         format!(
-                            "Try adding a contract to this function or use the unsound `{}` attribute instead.", 
+                            "Try adding a contract to this function or use the unsound `{}` attribute instead.",
                             KaniAttributeKind::Stub.as_ref(),
                         )
                     )

kani-driver/src/call_goto_instrument.rs

@@ -22,7 +22,7 @@ impl KaniSession {
         output: &Path,
         project: &Project,
         harness: &HarnessMetadata,
-        contract_info: Option<String>,
+        contract_info: Option<(String, String)>,
     ) -> Result<()> {
         // We actually start by calling goto-cc to start the specialization:
         self.specialize_to_proof_harness(input, output, &harness.mangled_name)?;
@@ -168,7 +168,7 @@ impl KaniSession {
         &self,
         harness: &HarnessMetadata,
         file: &Path,
-        check: Option<String>,
+        check: Option<(String, String)>,
     ) -> Result<()> {
         if check.is_none() {
             return Ok(());
@@ -177,9 +177,14 @@ impl KaniSession {
         let mut args: Vec<std::ffi::OsString> =
             vec!["--dfcc".into(), (&harness.mangled_name).into()];
 
-        if let Some(function) = check {
+        if let Some((function, recursion_tracker)) = check {
             println!("enforcing function contract for {function}");
-            args.extend(["--enforce-contract".into(), function.into()]);
+            args.extend([
+                "--enforce-contract".into(),
+                function.into(),
+                "--nondet-static-exclude".into(),
+                recursion_tracker.into(),
+            ]);
         }
 
         args.extend([file.into(), file.into()]);

kani-driver/src/harness_runner.rs

@@ -80,7 +80,7 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
         Ok(results)
     }
 
-    fn get_contract_info(&self, harness: &'pr HarnessMetadata) -> Result<Option<String>> {
+    fn get_contract_info(&self, harness: &'pr HarnessMetadata) -> Result<Option<(String, String)>> {
         let contract_info_artifact =
             self.project.get_harness_artifact(&harness, ArtifactType::ContractMetadata).unwrap();