Retrieve info for recursion tracker reliably (#3045)

Fixes #3035.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Signed-off-by: Felipe R. Monteiro <[email protected]>

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

@@ -35,8 +35,46 @@ 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 expected_name = format!("{}::REENTRY", tcx.item_name(recursion_wrapper_id));
+        let mut recursion_tracker = items.iter().filter_map(|i| match i {
+            MonoItem::Static(recursion_tracker)
+                if (*recursion_tracker).name().contains(expected_name.as_str()) =>
+            {
+                Some(*recursion_tracker)
+            }
+            _ => None,
+        });
+        let recursion_tracker_def = recursion_tracker
+            .next()
+            .expect("There should be at least one recursion tracker (REENTRY) in scope");
+        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 +94,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

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

@@ -33,6 +33,10 @@ impl<'tcx> GotocCtx<'tcx> {
 
         let typ = self.codegen_ty_stable(instance.ty());
         let location = self.codegen_span_stable(def.span());
+        // Contracts instrumentation relies on `--nondet-static-exclude` to properly
+        // havoc static variables. Kani uses the location and pretty name to identify
+        // the correct variables. If the wrong name is used, CBMC may fail silently.
+        // More details at https://github.com/diffblue/cbmc/issues/8225.
         let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location)
             .with_is_hidden(false) // Static items are always user defined.
             .with_pretty_name(pretty_name);

tests/expected/function-contract/generic_infinity_recursion.expected

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

tests/expected/function-contract/generic_infinity_recursion.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! Check Kani handling of generics and recursion with function contracts.
+
+#[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);
+}