Retrieve info for recursion tracker reliably

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

@@ -35,8 +35,45 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> 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 recursion_wrapper_id =
+            function_under_contract_attrs.checked_with_id().unwrap().unwrap();
+        let mut recursion_tracker = items.iter().filter_map(|i| match i {
+            MonoItem::Static(recursion_tracker)
+                if (*recursion_tracker).name().contains(
+                    format!("{}::REENTRY", tcx.item_name(recursion_wrapper_id)).as_str(),
+                ) =>
+            {
+                Some(*recursion_tracker)
+            }
+            _ => None,
+        });
+        let recursion_tracker_def = recursion_tracker.next().unwrap();
+        assert!(
+            recursion_tracker.next().is_none(),
+            "Only one recursion tracker (REENTRY) may be in scope"
+        );
+
+        let span_of_recursion_wrapper = tcx.def_span(recursion_wrapper_id);
+        let location_of_recursion_wrapper = self.codegen_span(&span_of_recursion_wrapper);
+        // The name and location for the recursion tracker should match the exact information added
+        // to the symbol table, otherwise our contract instrumentation will silently failed.
+        // This happens because Kani relies on `--nondet-static-exclude` from CBMC to properly
+        // handle this tracker. CBMC silently fails if there is no match in the symbol table
+        // that correspond to the argument of this flag.
+        // More details at https://github.com/model-checking/kani/pull/3045.
+        let full_recursion_tracker_name = format!(
+            "{}:{}",
+            location_of_recursion_wrapper
+                .filename()
+                .expect("recursion location wrapper should have a file name"),
+            // We must use the pretty name of the tracker instead of the mangled name.
+            // This restrictions comes from `--nondet-static-exclude` in CBMC.
+            // Mode details at https://github.com/diffblue/cbmc/issues/8225.
+            recursion_tracker_def.name(),
+        );
+
+        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(tcx, def.def_id()) =>
@@ -56,23 +93,12 @@ impl<'tcx> GotocCtx<'tcx> {
             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 }
+        AssignsContract {
+            recursion_tracker: full_recursion_tracker_name,
+            contracted_function_name: wrapper_name,
+        }
     }
 
     /// Convert the Kani level contract into a CBMC level contract by creating a

tests/expected/function-contract/generic_infinity_recursion.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/generic_infinity_recursion.rs

@@ -0,0 +1,11 @@
+#[kani::requires(x != 0)]
+fn foo<T: std::cmp::PartialEq<i32>>(x: T) {
+    assert_ne!(x, 0);
+    foo(x);
+}
+
+#[kani::proof_for_contract(foo)]
+fn foo_harness() {
+    let input: i32 = kani::any();
+    foo(input);
+}