Merge branch 'main' into toolchain-upgrade-2024-01-03

model-checking · Mar 4, 2024 · 24419a0 · 24419a0
2 parents da1bdbf + 99ee1a6
commit 24419a0
Show file tree

Hide file tree

Showing 5 changed files with 91 additions and 42 deletions.
diff --git a/Cargo.lock b/Cargo.lock
@@ -14,9 +14,9 @@ dependencies = [
 
 [[package]]
 name = "ahash"
-version = "0.8.9"
+version = "0.8.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d713b3834d76b85304d4d525563c1276e2e30dc97cc67bfb4585a4a29fc2c89f"
+checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011"
 dependencies = [
  "cfg-if",
  "once_cell",
@@ -35,9 +35,9 @@ dependencies = [
 
 [[package]]
 name = "anstream"
-version = "0.6.12"
+version = "0.6.13"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "96b09b5178381e0874812a9b157f7fe84982617e48f71f4e3235482775e5b540"
+checksum = "d96bd03f33fe50a863e394ee9718a706f988b9079b20c3784fb726e7678b62fb"
 dependencies = [
  "anstyle",
  "anstyle-parse",
@@ -198,7 +198,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn 2.0.50",
+ "syn 2.0.52",
 ]
 
 [[package]]
@@ -403,9 +403,9 @@ dependencies = [
 
 [[package]]
 name = "indexmap"
-version = "2.2.3"
+version = "2.2.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "233cf39063f058ea2caae4091bf4a3ef70a653afbc026f5c4a4135d114e3c177"
+checksum = "7b0b929d511467233429c45a44ac1dcaa21ba0f5ba11e4879e6ed28ddb4f9df4"
 dependencies = [
  "equivalent",
  "hashbrown",
@@ -498,7 +498,7 @@ dependencies = [
  "proc-macro-error",
  "proc-macro2",
  "quote",
- "syn 2.0.50",
+ "syn 2.0.52",
 ]
 
 [[package]]
@@ -552,9 +552,9 @@ dependencies = [
 
 [[package]]
 name = "log"
-version = "0.4.20"
+version = "0.4.21"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b5e6163cb8c49088c2c36f57875e58ccd8c87c7427f7fbd50ea6710b2f3f2e8f"
+checksum = "90ed8c1e510134f979dbc4f070f87d4313098b704861a105fe34231c70a3901c"
 
 [[package]]
 name = "matchers"
@@ -816,9 +816,9 @@ dependencies = [
 
 [[package]]
 name = "rayon"
-version = "1.8.1"
+version = "1.9.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fa7237101a77a10773db45d62004a272517633fbcc3df19d96455ede1122e051"
+checksum = "e4963ed1bc86e4f3ee217022bd855b297cef07fb9eac5dfa1f788b220b49b3bd"
 dependencies = [
  "either",
  "rayon-core",
@@ -966,7 +966,7 @@ checksum = "7eb0b34b42edc17f6b7cac84a52a1c5f0e1bb2227e997ca9011ea3dd34e8610b"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.50",
+ "syn 2.0.52",
 ]
 
 [[package]]
@@ -1078,7 +1078,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustversion",
- "syn 2.0.50",
+ "syn 2.0.52",
 ]
 
 [[package]]
@@ -1091,7 +1091,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustversion",
- "syn 2.0.50",
+ "syn 2.0.52",
 ]
 
 [[package]]
@@ -1106,9 +1106,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.50"
+version = "2.0.52"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "74f1bdc9872430ce9b75da68329d1c1746faf50ffac5f19e02b71e37ff881ffb"
+checksum = "b699d15b36d1f02c3e7c69f8ffef53de37aefae075d8488d4ba1a7788d574a07"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1117,9 +1117,9 @@ dependencies = [
 
 [[package]]
 name = "tempfile"
-version = "3.10.0"
+version = "3.10.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a365e8cd18e44762ef95d87f284f4b5cd04107fec2ff3052bd6a3e6069669e67"
+checksum = "85b77fafb263dd9d05cbeac119526425676db3784113aa9295c88498cbf8bff1"
 dependencies = [
  "cfg-if",
  "fastrand",
@@ -1144,7 +1144,7 @@ checksum = "a953cb265bef375dae3de6663da4d3804eee9682ea80d8e2542529b73c531c81"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.50",
+ "syn 2.0.52",
 ]
 
 [[package]]
@@ -1210,7 +1210,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.50",
+ "syn 2.0.52",
 ]
 
 [[package]]
@@ -1322,9 +1322,9 @@ dependencies = [
 
 [[package]]
 name = "walkdir"
-version = "2.4.0"
+version = "2.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d71d857dc86794ca4c280d616f7da00d2dbfd8cd788846559a6813e6aa4b54ee"
+checksum = "29790946404f91d9c5d06f9874efddea1dc06c5efe94541a7d6863108e3a5e4b"
 dependencies = [
  "same-file",
  "winapi-util",
@@ -1505,9 +1505,9 @@ checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8"
 
 [[package]]
 name = "winnow"
-version = "0.6.2"
+version = "0.6.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7a4191c47f15cc3ec71fcb4913cb83d58def65dd3787610213c649283b5ce178"
+checksum = "dffa400e67ed5a4dd237983829e66475f0a4a26938c4b04c21baede6262215b8"
 dependencies = [
  "memchr",
 ]
@@ -1529,5 +1529,5 @@ checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.50",
+ "syn 2.0.52",
 ]
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/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

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/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);

diff --git a/tests/expected/function-contract/generic_infinity_recursion.expected b/tests/expected/function-contract/generic_infinity_recursion.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/function-contract/generic_infinity_recursion.rs b/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);
+}