Update the search for REENTRY and add documentation

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

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

@@ -35,22 +35,42 @@ 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_tracker = items.iter().find_map(|i| match i {
+        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("REENTRY") =>
+                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.is_some(),
-            "There should exist a recursion tracker called REENTRY"
+            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"),
+            recursion_tracker_def.name(),
         );
-        let recursion_tracker = recursion_tracker.unwrap();
 
+        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()) =>
@@ -70,23 +90,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!(
-            "{}:{}",
-            location_of_recursion_wrapper
-                .filename()
-                .expect("recursion location wrapper should have a file name"),
-            recursion_tracker.name(),
-        );
-
-        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