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..1e8efdf04eb0 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -47,6 +47,20 @@ 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`. 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 { + 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 + } // 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 +139,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 +153,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..c3d459f13cba 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); ) } @@ -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: _| #output { + 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(); diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index e4182041e18b..a9e83c4ad5df 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/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; +//! } //! } //! } //! ``` 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); ) } 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..b92ccdd8b878 --- /dev/null +++ b/tests/expected/function-contract/mutable-references/ensures_with_two_mut_refs_fail.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z function-contracts + +//! 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; + 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/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 new file mode 100644 index 000000000000..624d484c8231 --- /dev/null +++ b/tests/expected/function-contract/mutable-references/return_mut_ref.expected @@ -0,0 +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 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..58dc2e0cbd5c --- /dev/null +++ b/tests/expected/function-contract/mutable-references/return_mut_ref.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z function-contracts + +//! 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(foo)] +fn harness() { + let mut x: u8 = kani::any(); + unsafe { foo(&mut x) }; +}