From 3878527834bd849221248bbfbddb387f946d817a Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Tue, 10 Jun 2025 17:56:35 -0700 Subject: [PATCH 01/12] Ensure that contract closures are FnOnce --- .../src/sysroot/contracts/assert.rs | 6 ++--- .../src/sysroot/contracts/bootstrap.rs | 8 +++++-- .../src/sysroot/contracts/check.rs | 6 ++--- .../src/sysroot/contracts/helpers.rs | 22 ++++++++++++++++--- .../src/sysroot/contracts/replace.rs | 2 +- 5 files changed, 32 insertions(+), 12 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/assert.rs b/library/kani_macros/src/sysroot/contracts/assert.rs index d954c10b6425..fb1d0e11a31b 100644 --- a/library/kani_macros/src/sysroot/contracts/assert.rs +++ b/library/kani_macros/src/sysroot/contracts/assert.rs @@ -29,7 +29,7 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(assert)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #assert_ident = || #output #body; + let mut #assert_ident = kani_force_fn_once(|| #output #body); ) } @@ -49,9 +49,9 @@ impl<'a> ContractConditionsHandler<'a> { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); parse_quote!( - let mut body_wrapper = || #output { + let mut body_wrapper = kani_force_fn_once(|| #output { #(#stmts)* - }; + }); let #result : #return_type = #body_wrapper_ident(); #result ) diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 2341655ec9ff..121c7f6bf24c 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -47,6 +47,10 @@ impl<'a> ContractConditionsHandler<'a> { #[kanitool::asserted_with = #assert_name] #[kanitool::modifies_wrapper = #modifies_name] #vis #sig { + #[inline(never)] + const fn kani_force_fn_once T>(f: F) -> F { + f + } // Dummy function used to force the compiler to capture the environment. // We cannot call closures inside constant functions. // This function gets replaced by `kani::internal::call_closure`. @@ -125,7 +129,7 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(recursion_check)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #recursion_ident = || #output + let mut #recursion_ident = kani_force_fn_once(|| #output { #[kanitool::recursion_tracker] static mut REENTRY: bool = false; @@ -139,7 +143,7 @@ impl<'a> ContractConditionsHandler<'a> { unsafe { REENTRY = false }; #result } - }; + }); ) } diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index a1a174360895..81a70f38a8cb 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -114,7 +114,7 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(check)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #check_ident = || #output #body; + let mut #check_ident = kani_force_fn_once(|| #output #body); ) } @@ -133,7 +133,7 @@ impl<'a> ContractConditionsHandler<'a> { /// Emit a modifies wrapper. It's only argument is the list of addresses that may be modified. pub fn modifies_closure( &self, - output: &ReturnType, + _output: &ReturnType, body: &Block, redefs: TokenStream2, ) -> TokenStream2 { @@ -144,7 +144,7 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(wrapper)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #modifies_ident = |#wrapper_ident: _| #output { + let mut #modifies_ident = |#wrapper_ident: _| { #redefs #(#stmts)* }; diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index c79a5520ceb3..c2474b9d22f8 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -123,9 +123,25 @@ pub fn closure_body(closure: &mut Stmt) -> &mut ExprBlock { let Stmt::Local(Local { init: Some(LocalInit { expr, .. }), .. }) = closure else { unreachable!() }; - let Expr::Closure(closure) = expr.as_mut() else { unreachable!() }; - let Expr::Block(body) = closure.body.as_mut() else { unreachable!() }; - body + match expr.as_mut() { + // The case of closures wrapped in `kani_force_fn_once` + Expr::Call(call) if call.args.len() == 1 => { + let arg = call.args.first_mut().unwrap(); + match arg { + Expr::Closure(closure) => { + let Expr::Block(body) = closure.body.as_mut() else { unreachable!() }; + body + } + _ => unreachable!(), + } + } + + Expr::Closure(closure) => { + let Expr::Block(body) = closure.body.as_mut() else { unreachable!() }; + body + } + _ => unreachable!(), + } } /// Does the provided path have the same chain of identifiers as `mtch` (match) diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 5a450b3ca9d4..719a96dcc429 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -133,7 +133,7 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(replace)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #replace_ident = || #output #body; + let mut #replace_ident = kani_force_fn_once(|| #output #body); ) } From 77cb0158816e856d690d85799e8d7add29ce4158 Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Wed, 11 Jun 2025 08:58:31 -0700 Subject: [PATCH 02/12] Wrap modifies closure --- .../kani_macros/src/sysroot/contracts/bootstrap.rs | 6 ++++++ library/kani_macros/src/sysroot/contracts/check.rs | 14 ++++++++++---- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 121c7f6bf24c..8aa1c3b353a3 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -47,10 +47,16 @@ impl<'a> ContractConditionsHandler<'a> { #[kanitool::asserted_with = #assert_name] #[kanitool::modifies_wrapper = #modifies_name] #vis #sig { + // Dummy functions used to force the compiler to annotate Kani's + // closures as FnOnce. #[inline(never)] const fn kani_force_fn_once T>(f: F) -> F { f } + #[inline(never)] + const fn kani_force_fn_once_with_args T>(f: F) -> F { + f + } // Dummy function used to force the compiler to capture the environment. // We cannot call closures inside constant functions. // This function gets replaced by `kani::internal::call_closure`. diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 81a70f38a8cb..c3d459f13cba 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -133,7 +133,7 @@ impl<'a> ContractConditionsHandler<'a> { /// Emit a modifies wrapper. It's only argument is the list of addresses that may be modified. pub fn modifies_closure( &self, - _output: &ReturnType, + output: &ReturnType, body: &Block, redefs: TokenStream2, ) -> TokenStream2 { @@ -144,10 +144,10 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(wrapper)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #modifies_ident = |#wrapper_ident: _| { + let mut #modifies_ident = kani_force_fn_once_with_args(|#wrapper_ident: _| #output { #redefs #(#stmts)* - }; + }); ) } @@ -157,7 +157,13 @@ impl<'a> ContractConditionsHandler<'a> { let Stmt::Local(Local { init: Some(LocalInit { expr, .. }), .. }) = closure_stmt else { unreachable!() }; - let Expr::Closure(closure) = expr.as_ref() else { unreachable!() }; + // The closure is wrapped into `kani_force_fn_once_with_args` + let Expr::Call(call) = expr.as_ref() else { unreachable!() }; + if call.args.len() != 1 { + unreachable!() + } + let expr = call.args.first().unwrap(); + let Expr::Closure(closure) = expr else { unreachable!() }; let Expr::Block(body) = closure.body.as_ref() else { unreachable!() }; let stream = self.modifies_closure(&closure.output, &body.block, TokenStream2::new()); *closure_stmt = syn::parse2(stream).unwrap(); From e7c39839870b1e37f7cbc37fff1129f832f6b42f Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Thu, 12 Jun 2025 00:20:44 -0700 Subject: [PATCH 03/12] Handle force_fn during the contract pass --- .../src/kani_middle/kani_functions.rs | 4 +++ .../src/kani_middle/transform/contracts.rs | 31 +++++++++++++++++++ library/kani_core/src/lib.rs | 24 ++++++++++++++ .../src/sysroot/contracts/bootstrap.rs | 2 ++ 4 files changed, 61 insertions(+) diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index c489654c0249..3695ac17e486 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -91,6 +91,10 @@ pub enum KaniModel { PtrOffsetFromUnsigned, #[strum(serialize = "RunContractModel")] RunContract, + #[strum(serialize = "ForceContractTypeModel")] + ForceContractType, + #[strum(serialize = "ForceContractTypeWithArgumentsModel")] + ForceContractTypeWithArguments, #[strum(serialize = "RunLoopContractModel")] RunLoopContract, #[strum(serialize = "SetPtrInitializedModel")] diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index e3ca9a53c66b..51c29fded4cc 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -282,6 +282,10 @@ pub struct FunctionWithContractPass { unused_closures: HashSet, /// Cache KaniRunContract function used to implement contracts. run_contract_fn: Option, + /// Kani ForceFnOnce function used to enforce correct closure annotation. + force_fn_once: Option, + /// Kani ForceFnOnceWithArgs function used to enforce correct closure annotation. + force_fn_once_with_args: Option, } impl TransformPass for FunctionWithContractPass { @@ -313,6 +317,17 @@ impl TransformPass for FunctionWithContractPass { { let run = Instance::resolve(self.run_contract_fn.unwrap(), args).unwrap(); (true, run.body().unwrap()) + } else if KaniAttributes::for_instance(tcx, instance).fn_marker() + == Some(Symbol::intern("kani_force_fn_once")) + { + let run = Instance::resolve(self.force_fn_once.unwrap(), args).unwrap(); + (true, run.body().unwrap()) + } else if KaniAttributes::for_instance(tcx, instance).fn_marker() + == Some(Symbol::intern("kani_force_fn_once_with_args")) + { + let run = + Instance::resolve(self.force_fn_once_with_args.unwrap(), args).unwrap(); + (true, run.body().unwrap()) } else { // Not a contract annotated function (false, body) @@ -372,12 +387,28 @@ impl FunctionWithContractPass { let run_contract_fn = queries.kani_functions().get(&KaniModel::RunContract.into()).copied(); assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function"); + + let force_fn_once = + queries.kani_functions().get(&KaniModel::ForceContractType.into()).copied(); + assert!(force_fn_once.is_some(), "Failed to find Kani force_fn_once function"); + + let force_fn_once_with_args = queries + .kani_functions() + .get(&KaniModel::ForceContractTypeWithArguments.into()) + .copied(); + assert!( + force_fn_once_with_args.is_some(), + "Failed to find Kani force_fn_once_with_args function" + ); + FunctionWithContractPass { check_fn, replace_fns, assert_contracts: !queries.args().no_assert_contracts, unused_closures: Default::default(), run_contract_fn, + force_fn_once, + force_fn_once_with_args, } } else { // If reachability mode is PubFns or Tests, we just remove any contract logic. diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 8d2f0c6605d6..c84e5c8c22b8 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -567,6 +567,30 @@ macro_rules! kani_intrinsics { func() } + /// Function that wraps a closure without arguments used to implement contracts. + /// + /// To ensure Rust correctly infers type of a contract closure as FnOnce, we wrap it in a dummy + /// function that explicitly requires an FnOnce. This wrapping is done at the point of closure + /// definition. + #[doc(hidden)] + #[allow(dead_code)] + #[kanitool::fn_marker = "ForceContractTypeModel"] + fn force_fn_once T>(func: F) -> F { + func + } + + /// Function that wraps a closure with one argument used to implement contracts. + /// + /// To ensure Rust correctly infers type of a contract closure as FnOnce, we wrap it in a dummy + /// function that explicitly requires an FnOnce. This wrapping is done at the point of closure + /// definition. + #[doc(hidden)] + #[allow(dead_code)] + #[kanitool::fn_marker = "ForceContractTypeWithArgumentsModel"] + fn force_fn_once_with_args T>(func: F) -> F { + func + } + /// Function that calls a closure used to implement loop contracts. /// /// In contracts, we cannot invoke the generated closures directly, instead, we call register diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 8aa1c3b353a3..b7548b2bcfd6 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -50,10 +50,12 @@ impl<'a> ContractConditionsHandler<'a> { // Dummy functions used to force the compiler to annotate Kani's // closures as FnOnce. #[inline(never)] + #[kanitool::fn_marker = "kani_force_fn_once"] const fn kani_force_fn_once T>(f: F) -> F { f } #[inline(never)] + #[kanitool::fn_marker = "kani_force_fn_once_with_args"] const fn kani_force_fn_once_with_args T>(f: F) -> F { f } From 187b6162be7264155ff90a5bdc9392e91a393c08 Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Tue, 17 Jun 2025 15:14:14 -0700 Subject: [PATCH 04/12] Add tests for contracts for functions returning mut ref --- .../ensures_with_two_mut_refs_fail.expected | 1 + .../ensures_with_two_mut_refs_fail.rs | 15 +++++++++++++++ .../mutable-references/return_mut_ref.expected | 11 +++++++++++ .../mutable-references/return_mut_ref.rs | 16 ++++++++++++++++ 4 files changed, 43 insertions(+) create mode 100644 tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.expected create mode 100644 tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.rs create mode 100644 tests/expected/function-contract/mutable-references/return_mut_ref.expected create mode 100644 tests/expected/function-contract/mutable-references/return_mut_ref.rs diff --git a/tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.expected b/tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.expected new file mode 100644 index 000000000000..16f05649a813 --- /dev/null +++ b/tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.expected @@ -0,0 +1 @@ +error[E0501]: cannot borrow value as immutable because previous closure requires unique access diff --git a/tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.rs b/tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.rs new file mode 100644 index 000000000000..257efc1b64b7 --- /dev/null +++ b/tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z function-contracts + +#[kani::ensures(|result| **result == 42 && *result == n)] +#[kani::modifies(n)] +fn forty_two(n: &mut u8) -> &mut u8 { + *n = 42; + n +} + +#[kani::proof_for_contract(forty_two)] +fn forty_two_harness() { + forty_two(&mut kani::any()); +} diff --git a/tests/expected/function-contract/mutable-references/return_mut_ref.expected b/tests/expected/function-contract/mutable-references/return_mut_ref.expected new file mode 100644 index 000000000000..54fa880047e5 --- /dev/null +++ b/tests/expected/function-contract/mutable-references/return_mut_ref.expected @@ -0,0 +1,11 @@ +assertion\ + - Status: UNREACHABLE\ + - Description: "attempt to divide by zero"\ +in function divide_by + +assertion\ + - Status: SUCCESS\ + - Description: "|result| **result <= a"\ +in function divide_by + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/mutable-references/return_mut_ref.rs b/tests/expected/function-contract/mutable-references/return_mut_ref.rs new file mode 100644 index 000000000000..443c2f68c1fa --- /dev/null +++ b/tests/expected/function-contract/mutable-references/return_mut_ref.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z function-contracts + +#[kani::requires(*b > 0 && *b < a)] +#[kani::ensures(|result| **result <= a)] +#[kani::modifies(b)] +fn divide_by(a: u8, b: &mut u8) -> &mut u8 { + *b = a / *b; + b +} + +#[kani::proof_for_contract(divide_by)] +fn divide_by_harness() { + divide_by(kani::any(), &mut kani::any()); +} From 8ddd6835e063df8522b402d34766da3e6fb19dcb Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Mon, 23 Jun 2025 17:20:22 -0700 Subject: [PATCH 05/12] Update tests --- .../ensures_with_two_mut_refs_fail.rs | 6 +++++- .../mut_ref_ensures_and_modifies.expected | 11 ++++++++++ .../mut_ref_ensures_and_modifies.rs | 18 +++++++++++++++++ .../return_mut_ref.expected | 10 ---------- .../mutable-references/return_mut_ref.rs | 20 ++++++++++--------- tests/perf/s2n-quic | 2 +- 6 files changed, 46 insertions(+), 21 deletions(-) create mode 100644 tests/expected/function-contract/mutable-references/mut_ref_ensures_and_modifies.expected create mode 100644 tests/expected/function-contract/mutable-references/mut_ref_ensures_and_modifies.rs diff --git a/tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.rs b/tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.rs index 257efc1b64b7..b92ccdd8b878 100644 --- a/tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.rs +++ b/tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.rs @@ -2,7 +2,11 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Z function-contracts -#[kani::ensures(|result| **result == 42 && *result == n)] +//! When a contract returns a mutable reference to one of its arguments, we cannot +//! use the `ensures` parameter alongside the function's argument, as they are two +//! mutable references to the same data. + +#[kani::ensures(|result| **result == 42 && **result == *n)] #[kani::modifies(n)] fn forty_two(n: &mut u8) -> &mut u8 { *n = 42; diff --git a/tests/expected/function-contract/mutable-references/mut_ref_ensures_and_modifies.expected b/tests/expected/function-contract/mutable-references/mut_ref_ensures_and_modifies.expected new file mode 100644 index 000000000000..54fa880047e5 --- /dev/null +++ b/tests/expected/function-contract/mutable-references/mut_ref_ensures_and_modifies.expected @@ -0,0 +1,11 @@ +assertion\ + - Status: UNREACHABLE\ + - Description: "attempt to divide by zero"\ +in function divide_by + +assertion\ + - Status: SUCCESS\ + - Description: "|result| **result <= a"\ +in function divide_by + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/mutable-references/mut_ref_ensures_and_modifies.rs b/tests/expected/function-contract/mutable-references/mut_ref_ensures_and_modifies.rs new file mode 100644 index 000000000000..64f34c475824 --- /dev/null +++ b/tests/expected/function-contract/mutable-references/mut_ref_ensures_and_modifies.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z function-contracts + +//! Verify `ensures` and `modifies` for functions returning mutable references. + +#[kani::requires(*b > 0 && *b < a)] +#[kani::ensures(|result| **result <= a)] +#[kani::modifies(b)] +fn divide_by(a: u8, b: &mut u8) -> &mut u8 { + *b = a / *b; + b +} + +#[kani::proof_for_contract(divide_by)] +fn divide_by_harness() { + divide_by(kani::any(), &mut kani::any()); +} diff --git a/tests/expected/function-contract/mutable-references/return_mut_ref.expected b/tests/expected/function-contract/mutable-references/return_mut_ref.expected index 54fa880047e5..34c886c358cb 100644 --- a/tests/expected/function-contract/mutable-references/return_mut_ref.expected +++ b/tests/expected/function-contract/mutable-references/return_mut_ref.expected @@ -1,11 +1 @@ -assertion\ - - Status: UNREACHABLE\ - - Description: "attempt to divide by zero"\ -in function divide_by - -assertion\ - - Status: SUCCESS\ - - Description: "|result| **result <= a"\ -in function divide_by - VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/mutable-references/return_mut_ref.rs b/tests/expected/function-contract/mutable-references/return_mut_ref.rs index 443c2f68c1fa..58dc2e0cbd5c 100644 --- a/tests/expected/function-contract/mutable-references/return_mut_ref.rs +++ b/tests/expected/function-contract/mutable-references/return_mut_ref.rs @@ -2,15 +2,17 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Z function-contracts -#[kani::requires(*b > 0 && *b < a)] -#[kani::ensures(|result| **result <= a)] -#[kani::modifies(b)] -fn divide_by(a: u8, b: &mut u8) -> &mut u8 { - *b = a / *b; - b +//! Checking that we can write contracts for functions returning mutable references. +//! This verifies that Rust correctly identifies contract closures as `FnOnce`. +//! See https://github.com/model-checking/kani/issues/3764 + +#[kani::requires(*val != 0)] +unsafe fn foo(val: &mut u8) -> &mut u8 { + val } -#[kani::proof_for_contract(divide_by)] -fn divide_by_harness() { - divide_by(kani::any(), &mut kani::any()); +#[kani::proof_for_contract(foo)] +fn harness() { + let mut x: u8 = kani::any(); + unsafe { foo(&mut x) }; } diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index b1b5bf8bee2e..3129ad5ac618 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit b1b5bf8bee2e3998cf5a7bf9a90bb3b96b57cd37 +Subproject commit 3129ad5ac618bb7b9b4fcddb67129af0f274c99e From 5508ba7acfd08669f70b8de286fb0970d8bac9df Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Mon, 23 Jun 2025 17:28:22 -0700 Subject: [PATCH 06/12] Add a bit of explanations --- library/kani_macros/src/sysroot/contracts/bootstrap.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index b7548b2bcfd6..1e8efdf04eb0 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -48,7 +48,9 @@ impl<'a> ContractConditionsHandler<'a> { #[kanitool::modifies_wrapper = #modifies_name] #vis #sig { // Dummy functions used to force the compiler to annotate Kani's - // closures as FnOnce. + // closures as `FnOnce`. Without this, Rust infers the generated closures as `FnMut`, + // preventing us from writing contracts for functions returning mutable references. + // See https://github.com/model-checking/kani/issues/3764 #[inline(never)] #[kanitool::fn_marker = "kani_force_fn_once"] const fn kani_force_fn_once T>(f: F) -> F { From b2c19f754ec89c2ccfe7e12fdb68dbe9275a25db Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Mon, 23 Jun 2025 17:41:53 -0700 Subject: [PATCH 07/12] Undo updates of submodules. --- tests/perf/s2n-quic | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 3129ad5ac618..b1b5bf8bee2e 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 3129ad5ac618bb7b9b4fcddb67129af0f274c99e +Subproject commit b1b5bf8bee2e3998cf5a7bf9a90bb3b96b57cd37 From e19f510e2c310ede1a8c2479c3275bb92dced8aa Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Wed, 25 Jun 2025 08:36:04 -0700 Subject: [PATCH 08/12] Update tests --- .../return_mut_ref.expected | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/tests/expected/function-contract/mutable-references/return_mut_ref.expected b/tests/expected/function-contract/mutable-references/return_mut_ref.expected index 34c886c358cb..624d484c8231 100644 --- a/tests/expected/function-contract/mutable-references/return_mut_ref.expected +++ b/tests/expected/function-contract/mutable-references/return_mut_ref.expected @@ -1 +1,31 @@ +pointer_dereference\ + - Status: SUCCESS\ + - Description: "dereference failure: pointer NULL"\ +in function foo + +pointer_dereference\ + - Status: SUCCESS\ + - Description: "dereference failure: pointer invalid"\ +in function foo + +pointer_dereference\ + - Status: SUCCESS\ + - Description: "dereference failure: deallocated dynamic object"\ +in function foo + +pointer_dereference\ + - Status: SUCCESS\ + - Description: "dereference failure: dead object"\ +in function foo + +pointer_dereference\ + - Status: SUCCESS\ + - Description: "dereference failure: pointer outside object bounds"\ +in function foo + +pointer_dereference\ + - Status: SUCCESS\ + - Description: "dereference failure: invalid integer address"\ +in function foo + VERIFICATION:- SUCCESSFUL From cf8846a8ed3bd62338cd44e353cd0b13f41b719e Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Wed, 25 Jun 2025 09:13:48 -0700 Subject: [PATCH 09/12] Make force_fn_onces unreachable --- library/kani_macros/src/sysroot/contracts/bootstrap.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 1e8efdf04eb0..1d218e5a31ea 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -51,15 +51,17 @@ impl<'a> ContractConditionsHandler<'a> { // closures as `FnOnce`. Without this, Rust infers the generated closures as `FnMut`, // preventing us from writing contracts for functions returning mutable references. // See https://github.com/model-checking/kani/issues/3764 + // These functions get replaced by `kani::internal::force_fn_once` and + // `kani::internal::force_fn_once_with_args`, respectively. #[inline(never)] #[kanitool::fn_marker = "kani_force_fn_once"] const fn kani_force_fn_once T>(f: F) -> F { - f + unreachable!() } #[inline(never)] #[kanitool::fn_marker = "kani_force_fn_once_with_args"] const fn kani_force_fn_once_with_args T>(f: F) -> F { - f + unreachable!() } // Dummy function used to force the compiler to capture the environment. // We cannot call closures inside constant functions. From be40caa96f9cb32beb3bf126a4bf1f8bb35c3d1e Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Wed, 25 Jun 2025 15:21:47 -0700 Subject: [PATCH 10/12] Undo updates of compiler and core --- .../src/kani_middle/kani_functions.rs | 4 --- .../src/kani_middle/transform/contracts.rs | 31 ------------------- library/kani_core/src/lib.rs | 24 -------------- .../src/sysroot/contracts/bootstrap.rs | 4 +-- 4 files changed, 2 insertions(+), 61 deletions(-) diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index d2f1900eba81..fd5e8a6b1246 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -91,10 +91,6 @@ pub enum KaniModel { PtrOffsetFromUnsigned, #[strum(serialize = "RunContractModel")] RunContract, - #[strum(serialize = "ForceContractTypeModel")] - ForceContractType, - #[strum(serialize = "ForceContractTypeWithArgumentsModel")] - ForceContractTypeWithArguments, #[strum(serialize = "RunLoopContractModel")] RunLoopContract, #[strum(serialize = "SetPtrInitializedModel")] diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 51c29fded4cc..e3ca9a53c66b 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -282,10 +282,6 @@ pub struct FunctionWithContractPass { unused_closures: HashSet, /// Cache KaniRunContract function used to implement contracts. run_contract_fn: Option, - /// Kani ForceFnOnce function used to enforce correct closure annotation. - force_fn_once: Option, - /// Kani ForceFnOnceWithArgs function used to enforce correct closure annotation. - force_fn_once_with_args: Option, } impl TransformPass for FunctionWithContractPass { @@ -317,17 +313,6 @@ impl TransformPass for FunctionWithContractPass { { let run = Instance::resolve(self.run_contract_fn.unwrap(), args).unwrap(); (true, run.body().unwrap()) - } else if KaniAttributes::for_instance(tcx, instance).fn_marker() - == Some(Symbol::intern("kani_force_fn_once")) - { - let run = Instance::resolve(self.force_fn_once.unwrap(), args).unwrap(); - (true, run.body().unwrap()) - } else if KaniAttributes::for_instance(tcx, instance).fn_marker() - == Some(Symbol::intern("kani_force_fn_once_with_args")) - { - let run = - Instance::resolve(self.force_fn_once_with_args.unwrap(), args).unwrap(); - (true, run.body().unwrap()) } else { // Not a contract annotated function (false, body) @@ -387,28 +372,12 @@ impl FunctionWithContractPass { let run_contract_fn = queries.kani_functions().get(&KaniModel::RunContract.into()).copied(); assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function"); - - let force_fn_once = - queries.kani_functions().get(&KaniModel::ForceContractType.into()).copied(); - assert!(force_fn_once.is_some(), "Failed to find Kani force_fn_once function"); - - let force_fn_once_with_args = queries - .kani_functions() - .get(&KaniModel::ForceContractTypeWithArguments.into()) - .copied(); - assert!( - force_fn_once_with_args.is_some(), - "Failed to find Kani force_fn_once_with_args function" - ); - FunctionWithContractPass { check_fn, replace_fns, assert_contracts: !queries.args().no_assert_contracts, unused_closures: Default::default(), run_contract_fn, - force_fn_once, - force_fn_once_with_args, } } else { // If reachability mode is PubFns or Tests, we just remove any contract logic. diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index c84e5c8c22b8..8d2f0c6605d6 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -567,30 +567,6 @@ macro_rules! kani_intrinsics { func() } - /// Function that wraps a closure without arguments used to implement contracts. - /// - /// To ensure Rust correctly infers type of a contract closure as FnOnce, we wrap it in a dummy - /// function that explicitly requires an FnOnce. This wrapping is done at the point of closure - /// definition. - #[doc(hidden)] - #[allow(dead_code)] - #[kanitool::fn_marker = "ForceContractTypeModel"] - fn force_fn_once T>(func: F) -> F { - func - } - - /// Function that wraps a closure with one argument used to implement contracts. - /// - /// To ensure Rust correctly infers type of a contract closure as FnOnce, we wrap it in a dummy - /// function that explicitly requires an FnOnce. This wrapping is done at the point of closure - /// definition. - #[doc(hidden)] - #[allow(dead_code)] - #[kanitool::fn_marker = "ForceContractTypeWithArgumentsModel"] - fn force_fn_once_with_args T>(func: F) -> F { - func - } - /// Function that calls a closure used to implement loop contracts. /// /// In contracts, we cannot invoke the generated closures directly, instead, we call register diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 1d218e5a31ea..6d310286a2df 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -56,12 +56,12 @@ impl<'a> ContractConditionsHandler<'a> { #[inline(never)] #[kanitool::fn_marker = "kani_force_fn_once"] const fn kani_force_fn_once T>(f: F) -> F { - unreachable!() + f } #[inline(never)] #[kanitool::fn_marker = "kani_force_fn_once_with_args"] const fn kani_force_fn_once_with_args T>(f: F) -> F { - unreachable!() + f } // Dummy function used to force the compiler to capture the environment. // We cannot call closures inside constant functions. From 8dad0cde7e782d5729593c7fd7fd26359a6caf70 Mon Sep 17 00:00:00 2001 From: Fedor Ryabinin Date: Wed, 25 Jun 2025 15:23:50 -0700 Subject: [PATCH 11/12] Update comments --- library/kani_macros/src/sysroot/contracts/bootstrap.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 6d310286a2df..1e8efdf04eb0 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -51,8 +51,6 @@ impl<'a> ContractConditionsHandler<'a> { // closures as `FnOnce`. Without this, Rust infers the generated closures as `FnMut`, // preventing us from writing contracts for functions returning mutable references. // See https://github.com/model-checking/kani/issues/3764 - // These functions get replaced by `kani::internal::force_fn_once` and - // `kani::internal::force_fn_once_with_args`, respectively. #[inline(never)] #[kanitool::fn_marker = "kani_force_fn_once"] const fn kani_force_fn_once T>(f: F) -> F { From 006afe5a90d2936e78df7b64583bede00e29edbf Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 3 Jul 2025 14:46:23 -0400 Subject: [PATCH 12/12] update module documentation --- .../kani_macros/src/sysroot/contracts/mod.rs | 475 ++++++++++-------- 1 file changed, 266 insertions(+), 209 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index cc792614e2d5..e11b4bf2608e 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -153,120 +153,139 @@ //! #[kanitool::recursion_check = "__kani_recursion_check_div"] //! #[kanitool::checked_with = "__kani_check_div"] //! #[kanitool::replaced_with = "__kani_replace_div"] -//! #[kanitool::modifies_wrapper = "__kani_modifies_div"] //! #[kanitool::asserted_with = "__kani_assert_div"] +//! #[kanitool::modifies_wrapper = "__kani_modifies_div"] //! fn div(dividend: u32, divisor: u32) -> u32 { //! #[inline(never)] +//! #[kanitool::fn_marker = "kani_force_fn_once"] +//! const fn kani_force_fn_once T>(f: F) -> F { +//! f +//! } +//! #[inline(never)] +//! #[kanitool::fn_marker = "kani_force_fn_once_with_args"] +//! const fn kani_force_fn_once_with_args T>(f: F) -> F { +//! f +//! } +//! #[inline(never)] //! #[kanitool::fn_marker = "kani_register_contract"] -//! pub const fn kani_register_contract T>(f: F) -> T { -//! kani::panic("internal error: entered unreachable code: ") +//! const fn kani_register_contract T>(f: F) -> T { +//! unreachable!() //! } -//! let kani_contract_mode = kani::internal::mode(); +//! #[inline(never)] +//! #[kanitool::fn_marker = "kani_contract_mode"] +//! const fn kani_contract_mode() -> kani::internal::Mode { +//! kani::internal::ORIGINAL +//! } +//! let kani_contract_mode = kani_contract_mode(); //! match kani_contract_mode { //! kani::internal::RECURSION_CHECK => { //! #[kanitool::is_contract_generated(recursion_check)] //! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_recursion_check_div = -//! || -> u32 -//! { -//! #[kanitool::recursion_tracker] -//! static mut REENTRY: bool = false; -//! if unsafe { REENTRY } { -//! #[kanitool::is_contract_generated(replace)] -//! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_replace_div = -//! || -> u32 -//! { -//! kani::assert(divisor != 0, "divisor != 0"); -//! let result_kani_internal: u32 = kani::any_modifies(); -//! kani::assume(kani::internal::apply_closure(|result: &u32| -//! *result <= dividend, &result_kani_internal)); -//! result_kani_internal -//! }; -//! __kani_replace_div() -//! } else { -//! unsafe { REENTRY = true }; -//! #[kanitool::is_contract_generated(check)] -//! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_check_div = -//! || -> u32 -//! { -//! kani::assume(divisor != 0); -//! let _wrapper_arg = (); -//! #[kanitool::is_contract_generated(wrapper)] -//! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_modifies_div = -//! |_wrapper_arg| -> u32 { dividend / divisor }; -//! let result_kani_internal: u32 = -//! __kani_modifies_div(_wrapper_arg); -//! kani::assert(kani::internal::apply_closure(|result: &u32| -//! *result <= dividend, &result_kani_internal), -//! "|result : &u32| *result <= dividend"); -//! result_kani_internal -//! }; -//! let result_kani_internal = __kani_check_div(); -//! unsafe { REENTRY = false }; -//! result_kani_internal -//! } -//! }; -//! ; +//! let mut __kani_recursion_check_div = kani_force_fn_once(|| -> u32 { +//! #[kanitool::recursion_tracker] +//! static mut REENTRY: bool = false; +//! if unsafe { REENTRY } { +//! #[kanitool::is_contract_generated(replace)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_replace_div = kani_force_fn_once(|| -> u32 { +//! kani::assert(divisor != 0, stringify!(divisor != 0)); +//! let result_kani_internal: u32 = kani::any_modifies(); +//! let dividend = dividend; +//! let divisor = divisor; +//! kani::assume(kani::internal::apply_closure( +//! |result: &u32| *result <= dividend, +//! &result_kani_internal, +//! )); +//! result_kani_internal +//! }); +//! __kani_replace_div() +//! } else { +//! unsafe { REENTRY = true }; +//! #[kanitool::is_contract_generated(check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_check_div = kani_force_fn_once(|| -> u32 { +//! kani::assume(divisor != 0); +//! let _wrapper_arg = (); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_div = +//! kani_force_fn_once_with_args(|_wrapper_arg: _| -> u32 { +//! dividend / divisor +//! }); +//! let result_kani_internal: u32 = __kani_modifies_div(_wrapper_arg); +//! kani::assert( +//! kani::internal::apply_closure( +//! |result: &u32| *result <= dividend, +//! &result_kani_internal, +//! ), +//! stringify!(|result: &u32| *result <= dividend), +//! ); +//! result_kani_internal +//! }); +//! let result_kani_internal = __kani_check_div(); +//! unsafe { REENTRY = false }; +//! result_kani_internal +//! } +//! }); //! kani_register_contract(__kani_recursion_check_div) //! } //! kani::internal::REPLACE => { //! #[kanitool::is_contract_generated(replace)] //! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_replace_div = -//! || -> u32 -//! { -//! kani::assert(divisor != 0, "divisor != 0"); -//! let result_kani_internal: u32 = kani::any_modifies(); -//! kani::assume(kani::internal::apply_closure(|result: &u32| -//! *result <= dividend, &result_kani_internal)); -//! result_kani_internal -//! }; -//! ; +//! let mut __kani_replace_div = kani_force_fn_once(|| -> u32 { +//! kani::assert(divisor != 0, stringify!(divisor != 0)); +//! let result_kani_internal: u32 = kani::any_modifies(); +//! let dividend = dividend; +//! let divisor = divisor; +//! kani::assume(kani::internal::apply_closure( +//! |result: &u32| *result <= dividend, +//! &result_kani_internal, +//! )); +//! result_kani_internal +//! }); //! kani_register_contract(__kani_replace_div) //! } //! kani::internal::SIMPLE_CHECK => { //! #[kanitool::is_contract_generated(check)] //! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_check_div = -//! || -> u32 -//! { -//! kani::assume(divisor != 0); -//! let _wrapper_arg = (); -//! #[kanitool::is_contract_generated(wrapper)] -//! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_modifies_div = -//! |_wrapper_arg| -> u32 { dividend / divisor }; -//! let result_kani_internal: u32 = -//! __kani_modifies_div(_wrapper_arg); -//! kani::assert(kani::internal::apply_closure(|result: &u32| -//! *result <= dividend, &result_kani_internal), -//! "|result : &u32| *result <= dividend"); -//! result_kani_internal -//! }; -//! ; +//! let mut __kani_check_div = kani_force_fn_once(|| -> u32 { +//! kani::assume(divisor != 0); +//! let _wrapper_arg = (); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_div = +//! kani_force_fn_once_with_args(|_wrapper_arg: _| -> u32 { dividend / divisor }); +//! let result_kani_internal: u32 = __kani_modifies_div(_wrapper_arg); +//! kani::assert( +//! kani::internal::apply_closure( +//! |result: &u32| *result <= dividend, +//! &result_kani_internal, +//! ), +//! stringify!(|result: &u32| *result <= dividend), +//! ); +//! result_kani_internal +//! }); //! kani_register_contract(__kani_check_div) //! } //! kani::internal::ASSERT => { //! #[kanitool::is_contract_generated(assert)] //! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_assert_div = -//! || -> u32 -//! { -//! kani::assert(divisor != 0, "divisor != 0"); -//! let mut body_wrapper = || -> u32 { dividend / divisor }; -//! let result_kani_internal: u32 = body_wrapper(); -//! kani::assert(kani::internal::apply_closure(|result: &u32| -//! *result <= dividend, &result_kani_internal), -//! "|result : &u32| *result <= dividend"); -//! result_kani_internal -//! }; -//! ; +//! let mut __kani_assert_div = kani_force_fn_once(|| -> u32 { +//! kani::assert(divisor != 0, stringify!(divisor != 0)); +//! let mut body_wrapper = kani_force_fn_once(|| -> u32 { dividend / divisor }); +//! let result_kani_internal: u32 = body_wrapper(); +//! kani::assert( +//! kani::internal::apply_closure( +//! |result: &u32| *result <= dividend, +//! &result_kani_internal, +//! ), +//! stringify!(|result: &u32| *result <= dividend), +//! ); +//! result_kani_internal +//! }); //! kani_register_contract(__kani_assert_div) //! } -//! _ => { dividend / divisor } +//! _ => dividend / divisor, //! } //! } //! ``` @@ -304,153 +323,191 @@ //! #[kanitool::recursion_check = "__kani_recursion_check_modify"] //! #[kanitool::checked_with = "__kani_check_modify"] //! #[kanitool::replaced_with = "__kani_replace_modify"] -//! #[kanitool::modifies_wrapper = "__kani_modifies_modify"] //! #[kanitool::asserted_with = "__kani_assert_modify"] +//! #[kanitool::modifies_wrapper = "__kani_modifies_modify"] //! fn modify(ptr: &mut u32) { +//! #[inline(never)] +//! #[kanitool::fn_marker = "kani_force_fn_once"] +//! const fn kani_force_fn_once T>(f: F) -> F { +//! f +//! } +//! #[inline(never)] +//! #[kanitool::fn_marker = "kani_force_fn_once_with_args"] +//! const fn kani_force_fn_once_with_args T>(f: F) -> F { +//! f +//! } //! #[inline(never)] //! #[kanitool::fn_marker = "kani_register_contract"] -//! pub const fn kani_register_contract T>(f: F) -> T { -//! kani::panic("internal error: entered unreachable code: ") +//! const fn kani_register_contract T>(f: F) -> T { +//! unreachable!() +//! } +//! #[inline(never)] +//! #[kanitool::fn_marker = "kani_contract_mode"] +//! const fn kani_contract_mode() -> kani::internal::Mode { +//! kani::internal::ORIGINAL //! } -//! let kani_contract_mode = kani::internal::mode(); +//! let kani_contract_mode = kani_contract_mode(); //! match kani_contract_mode { //! kani::internal::RECURSION_CHECK => { //! #[kanitool::is_contract_generated(recursion_check)] //! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_recursion_check_modify = -//! || -//! { -//! #[kanitool::recursion_tracker] -//! static mut REENTRY: bool = false; -//! if unsafe { REENTRY } { -//! #[kanitool::is_contract_generated(replace)] -//! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_replace_modify = -//! || -//! { -//! kani::assert(*ptr < 100, "*ptr < 100"); -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let result_kani_internal: () = kani::any_modifies(); -//! *unsafe { -//! kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(ptr))) -//! } = kani::any_modifies(); -//! kani::assume(kani::internal::apply_closure(|result| -//! (remember_kani_internal_92cc419d8aca576c) == *ptr, -//! &result_kani_internal)); -//! kani::assume(kani::internal::apply_closure(|result| -//! (remember_kani_internal_92cc419d8aca576c) == *ptr, -//! &result_kani_internal)); -//! result_kani_internal -//! }; -//! __kani_replace_modify() -//! } else { -//! unsafe { REENTRY = true }; -//! #[kanitool::is_contract_generated(check)] -//! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_check_modify = -//! || -//! { -//! kani::assume(*ptr < 100); -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let _wrapper_arg = (ptr as *const _,); -//! #[kanitool::is_contract_generated(wrapper)] -//! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_modifies_modify = -//! |_wrapper_arg| { *ptr += 1; }; -//! let result_kani_internal: () = -//! __kani_modifies_modify(_wrapper_arg); -//! kani::assert(kani::internal::apply_closure(|result| -//! (remember_kani_internal_92cc419d8aca576c) == *ptr, -//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); -//! kani::assert(kani::internal::apply_closure(|result| -//! (remember_kani_internal_92cc419d8aca576c) == *ptr, -//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); -//! result_kani_internal -//! }; -//! let result_kani_internal = __kani_check_modify(); -//! unsafe { REENTRY = false }; -//! result_kani_internal -//! } -//! }; -//! ; +//! let mut __kani_recursion_check_modify = kani_force_fn_once(|| { +//! #[kanitool::recursion_tracker] +//! static mut REENTRY: bool = false; +//! if unsafe { REENTRY } { +//! #[kanitool::is_contract_generated(replace)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_replace_modify = kani_force_fn_once(|| { +//! kani::assert(*ptr < 100, stringify!(*ptr < 100)); +//! let remember_kani_internal_2e780b148d45b5c8 = *ptr + 1; +//! let remember_kani_internal_2e780b148d45b5c8 = *ptr + 1; +//! let result_kani_internal: () = kani::any_modifies(); +//! unsafe { +//! kani::internal::write_any(kani::internal::Pointer::assignable( +//! kani::internal::untracked_deref(&ptr), +//! )) +//! }; +//! let ptr = ptr; +//! kani::assume(kani::internal::apply_closure( +//! |result| (remember_kani_internal_2e780b148d45b5c8) == *ptr, +//! &result_kani_internal, +//! )); +//! kani::assume(kani::internal::apply_closure( +//! |result| (remember_kani_internal_2e780b148d45b5c8) == *ptr, +//! &result_kani_internal, +//! )); +//! result_kani_internal +//! }); +//! __kani_replace_modify() +//! } else { +//! unsafe { REENTRY = true }; +//! #[kanitool::is_contract_generated(check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_check_modify = kani_force_fn_once(|| { +//! kani::assume(*ptr < 100); +//! let remember_kani_internal_2e780b148d45b5c8 = *ptr + 1; +//! let remember_kani_internal_2e780b148d45b5c8 = *ptr + 1; +//! let _wrapper_arg = (ptr as *const _,); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_modify = +//! kani_force_fn_once_with_args(|_wrapper_arg: _| { +//! *ptr += 1; +//! }); +//! let result_kani_internal: () = __kani_modifies_modify(_wrapper_arg); +//! kani::assert( +//! kani::internal::apply_closure( +//! |result| (remember_kani_internal_2e780b148d45b5c8) == *ptr, +//! &result_kani_internal, +//! ), +//! stringify!(|result| old(*ptr + 1) == *ptr), +//! ); +//! kani::assert( +//! kani::internal::apply_closure( +//! |result| (remember_kani_internal_2e780b148d45b5c8) == *ptr, +//! &result_kani_internal, +//! ), +//! stringify!(|result| old(*ptr + 1) == *ptr), +//! ); +//! result_kani_internal +//! }); +//! let result_kani_internal = __kani_check_modify(); +//! unsafe { REENTRY = false }; +//! result_kani_internal +//! } +//! }); //! kani_register_contract(__kani_recursion_check_modify) //! } //! kani::internal::REPLACE => { //! #[kanitool::is_contract_generated(replace)] //! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_replace_modify = -//! || -//! { -//! kani::assert(*ptr < 100, "*ptr < 100"); -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let result_kani_internal: () = kani::any_modifies(); -//! *unsafe { -//! kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(ptr))) -//! } = kani::any_modifies(); -//! kani::assume(kani::internal::apply_closure(|result| -//! (remember_kani_internal_92cc419d8aca576c) == *ptr, -//! &result_kani_internal)); -//! kani::assume(kani::internal::apply_closure(|result| -//! (remember_kani_internal_92cc419d8aca576c) == *ptr, -//! &result_kani_internal)); -//! result_kani_internal -//! }; -//! ; +//! let mut __kani_replace_modify = kani_force_fn_once(|| { +//! kani::assert(*ptr < 100, stringify!(*ptr < 100)); +//! let remember_kani_internal_2e780b148d45b5c8 = *ptr + 1; +//! let remember_kani_internal_2e780b148d45b5c8 = *ptr + 1; +//! let result_kani_internal: () = kani::any_modifies(); +//! unsafe { +//! kani::internal::write_any(kani::internal::Pointer::assignable( +//! kani::internal::untracked_deref(&ptr), +//! )) +//! }; +//! let ptr = ptr; +//! kani::assume(kani::internal::apply_closure( +//! |result| (remember_kani_internal_2e780b148d45b5c8) == *ptr, +//! &result_kani_internal, +//! )); +//! kani::assume(kani::internal::apply_closure( +//! |result| (remember_kani_internal_2e780b148d45b5c8) == *ptr, +//! &result_kani_internal, +//! )); +//! result_kani_internal +//! }); //! kani_register_contract(__kani_replace_modify) //! } //! kani::internal::SIMPLE_CHECK => { //! #[kanitool::is_contract_generated(check)] //! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_check_modify = -//! || -//! { -//! kani::assume(*ptr < 100); -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let _wrapper_arg = (ptr as *const _,); -//! #[kanitool::is_contract_generated(wrapper)] -//! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_modifies_modify = -//! |_wrapper_arg| { *ptr += 1; }; -//! let result_kani_internal: () = -//! __kani_modifies_modify(_wrapper_arg); -//! kani::assert(kani::internal::apply_closure(|result| -//! (remember_kani_internal_92cc419d8aca576c) == *ptr, -//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); -//! kani::assert(kani::internal::apply_closure(|result| -//! (remember_kani_internal_92cc419d8aca576c) == *ptr, -//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); -//! result_kani_internal -//! }; -//! ; +//! let mut __kani_check_modify = kani_force_fn_once(|| { +//! kani::assume(*ptr < 100); +//! let remember_kani_internal_2e780b148d45b5c8 = *ptr + 1; +//! let remember_kani_internal_2e780b148d45b5c8 = *ptr + 1; +//! let _wrapper_arg = (ptr as *const _,); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_modify = kani_force_fn_once_with_args(|_wrapper_arg: _| { +//! *ptr += 1; +//! }); +//! let result_kani_internal: () = __kani_modifies_modify(_wrapper_arg); +//! kani::assert( +//! kani::internal::apply_closure( +//! |result| (remember_kani_internal_2e780b148d45b5c8) == *ptr, +//! &result_kani_internal, +//! ), +//! stringify!(|result| old(*ptr + 1) == *ptr), +//! ); +//! kani::assert( +//! kani::internal::apply_closure( +//! |result| (remember_kani_internal_2e780b148d45b5c8) == *ptr, +//! &result_kani_internal, +//! ), +//! stringify!(|result| old(*ptr + 1) == *ptr), +//! ); +//! result_kani_internal +//! }); //! kani_register_contract(__kani_check_modify) //! } //! kani::internal::ASSERT => { //! #[kanitool::is_contract_generated(assert)] //! #[allow(dead_code, unused_variables, unused_mut)] -//! let mut __kani_assert_modify = -//! || -//! { -//! kani::assert(*ptr < 100, "*ptr < 100"); -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let mut body_wrapper = || { *ptr += 1; }; -//! let result_kani_internal: () = body_wrapper(); -//! kani::assert(kani::internal::apply_closure(|result| -//! (remember_kani_internal_92cc419d8aca576c) == *ptr, -//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); -//! kani::assert(kani::internal::apply_closure(|result| -//! (remember_kani_internal_92cc419d8aca576c) == *ptr, -//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); -//! result_kani_internal -//! }; -//! ; +//! let mut __kani_assert_modify = kani_force_fn_once(|| { +//! kani::assert(*ptr < 100, stringify!(*ptr < 100)); +//! let remember_kani_internal_2e780b148d45b5c8 = *ptr + 1; +//! let remember_kani_internal_2e780b148d45b5c8 = *ptr + 1; +//! let mut body_wrapper = kani_force_fn_once(|| { +//! *ptr += 1; +//! }); +//! let result_kani_internal: () = body_wrapper(); +//! kani::assert( +//! kani::internal::apply_closure( +//! |result| (remember_kani_internal_2e780b148d45b5c8) == *ptr, +//! &result_kani_internal, +//! ), +//! stringify!(|result| old(*ptr + 1) == *ptr), +//! ); +//! kani::assert( +//! kani::internal::apply_closure( +//! |result| (remember_kani_internal_2e780b148d45b5c8) == *ptr, +//! &result_kani_internal, +//! ), +//! stringify!(|result| old(*ptr + 1) == *ptr), +//! ); +//! result_kani_internal +//! }); //! kani_register_contract(__kani_assert_modify) //! } -//! _ => { *ptr += 1; } +//! _ => { +//! *ptr += 1; +//! } //! } //! } //! ```