From d5479c0c0e1f085086c6fda897267afd6fb5bbf8 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Mon, 26 Feb 2024 18:08:44 +0000 Subject: [PATCH 1/9] Retrieve info for recursion tracker reliably Fixes https://github.com/model-checking/kani/issues/3035 Signed-off-by: Felipe R. Monteiro --- .../codegen_cprover_gotoc/codegen/contract.rs | 21 +++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 2bd3e1ff7c35..2a3c842b3286 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -37,6 +37,23 @@ impl<'tcx> GotocCtx<'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() + .filter_map(|i| match i { + MonoItem::Static(recursion_tracker) + if (*recursion_tracker).name().contains("REENTRY") => + { + Some(*recursion_tracker) + } + _ => None, + }) + .next(); + assert!( + recursion_tracker.is_some(), + "There should exist a recursion tracker called REENTRY" + ); + let instance_recursion_tracker = recursion_tracker.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()) => @@ -65,11 +82,11 @@ impl<'tcx> GotocCtx<'tcx> { 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), + instance_recursion_tracker.name(), ); AssignsContract { recursion_tracker: full_name, contracted_function_name: wrapper_name } From 5dd12533b5f345f78ff1f3343855babd20422839 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Wed, 28 Feb 2024 04:50:54 +0000 Subject: [PATCH 2/9] Use find instead of filter_map Signed-off-by: Felipe R. Monteiro --- .../codegen_cprover_gotoc/codegen/contract.rs | 23 ++++++++----------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 2a3c842b3286..44a26adee98d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -37,22 +37,19 @@ impl<'tcx> GotocCtx<'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() - .filter_map(|i| match i { - MonoItem::Static(recursion_tracker) - if (*recursion_tracker).name().contains("REENTRY") => - { - Some(*recursion_tracker) - } - _ => None, - }) - .next(); + let recursion_tracker = items.iter().find_map(|i| match i { + MonoItem::Static(recursion_tracker) + if (*recursion_tracker).name().contains("REENTRY") => + { + Some(*recursion_tracker) + } + _ => None, + }); assert!( recursion_tracker.is_some(), "There should exist a recursion tracker called REENTRY" ); - let instance_recursion_tracker = recursion_tracker.unwrap(); + let recursion_tracker = recursion_tracker.unwrap(); let mut instance_under_contract = items.iter().filter_map(|i| match i { MonoItem::Fn(instance @ Instance { def, .. }) @@ -86,7 +83,7 @@ impl<'tcx> GotocCtx<'tcx> { location_of_recursion_wrapper .filename() .expect("recursion location wrapper should have a file name"), - instance_recursion_tracker.name(), + recursion_tracker.name(), ); AssignsContract { recursion_tracker: full_name, contracted_function_name: wrapper_name } From 569208a185d14cedee402fcb6b1ee84cad5171b0 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 29 Feb 2024 23:37:25 +0000 Subject: [PATCH 3/9] Update the search for REENTRY and add documentation Signed-off-by: Felipe R. Monteiro --- .../codegen_cprover_gotoc/codegen/contract.rs | 51 +++++++++++-------- 1 file changed, 30 insertions(+), 21 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 44a26adee98d..3a35a4b84422 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/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 From e2f75fcad1a0c35d12e85b653c6bbe7f1ad48816 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 1 Mar 2024 02:45:18 +0000 Subject: [PATCH 4/9] Add a comment to clarify not using mangled_name Signed-off-by: Felipe R. Monteiro --- kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 3a35a4b84422..a3095195d0ff 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -67,6 +67,9 @@ impl<'tcx> GotocCtx<'tcx> { 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(), ); From 96ddb5ab45929e5f55db479c7464d740e1be8003 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 1 Mar 2024 02:46:17 +0000 Subject: [PATCH 5/9] Add a test with generics and infinity recursion Signed-off-by: Felipe R. Monteiro --- .../generic_infinity_recursion.expected | 1 + .../function-contract/generic_infinity_recursion.rs | 11 +++++++++++ 2 files changed, 12 insertions(+) create mode 100644 tests/expected/function-contract/generic_infinity_recursion.expected create mode 100644 tests/expected/function-contract/generic_infinity_recursion.rs 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..880f00714b32 --- /dev/null +++ b/tests/expected/function-contract/generic_infinity_recursion.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL \ No newline at end of file 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..dfc52a7e705b --- /dev/null +++ b/tests/expected/function-contract/generic_infinity_recursion.rs @@ -0,0 +1,11 @@ +#[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); +} From 4cabf2150ea6ecf7af9058ae56162b7f4754f65f Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 1 Mar 2024 02:47:49 +0000 Subject: [PATCH 6/9] New line Signed-off-by: Felipe R. Monteiro --- .../function-contract/generic_infinity_recursion.expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/function-contract/generic_infinity_recursion.expected b/tests/expected/function-contract/generic_infinity_recursion.expected index 880f00714b32..34c886c358cb 100644 --- a/tests/expected/function-contract/generic_infinity_recursion.expected +++ b/tests/expected/function-contract/generic_infinity_recursion.expected @@ -1 +1 @@ -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL From e3b2c353d4cc8096069320945d68ea9ab020a351 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 1 Mar 2024 18:48:53 +0000 Subject: [PATCH 7/9] Move format outside of the loop Signed-off-by: Felipe R. Monteiro --- .../src/codegen_cprover_gotoc/codegen/contract.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index a3095195d0ff..a720d1457606 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -38,17 +38,18 @@ impl<'tcx> GotocCtx<'tcx> { 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( - format!("{}::REENTRY", tcx.item_name(recursion_wrapper_id)).as_str(), - ) => + if (*recursion_tracker).name().contains(expected_name.as_str()) => { Some(*recursion_tracker) } _ => None, }); - let recursion_tracker_def = recursion_tracker.next().unwrap(); + 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" From 84674d3bf4c0d345ac37829220b401e2130e8a82 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 1 Mar 2024 18:49:13 +0000 Subject: [PATCH 8/9] Add header to test case Signed-off-by: Felipe R. Monteiro --- .../function-contract/generic_infinity_recursion.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tests/expected/function-contract/generic_infinity_recursion.rs b/tests/expected/function-contract/generic_infinity_recursion.rs index dfc52a7e705b..d40b7694dbdb 100644 --- a/tests/expected/function-contract/generic_infinity_recursion.rs +++ b/tests/expected/function-contract/generic_infinity_recursion.rs @@ -1,3 +1,9 @@ +// 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); From ba5d4c1ccdced754cef50d9a0c29a0f4c80c7fbd Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 1 Mar 2024 23:38:34 +0000 Subject: [PATCH 9/9] Add extra comment about --nondet-static-exclude isssue Signed-off-by: Felipe R. Monteiro --- kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs | 4 ++++ 1 file changed, 4 insertions(+) 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);