diff --git a/Cargo.lock b/Cargo.lock index 434c0e7bb330..ab853a65e544 100644 --- 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 index 2bd3e1ff7c35..a720d1457606 100644 --- 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 index cf4c6173637b..0a0a55ad3dd4 100644 --- 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 new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ 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 new file mode 100644 index 000000000000..d40b7694dbdb --- /dev/null +++ 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>(x: T) { + assert_ne!(x, 0); + foo(x); +} + +#[kani::proof_for_contract(foo)] +fn foo_harness() { + let input: i32 = kani::any(); + foo(input); +}