diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 2e46d67a5b8e..e76286b398cb 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -34,14 +34,12 @@ impl<'a> ContractConditionsHandler<'a> { ) } ContractConditionsData::Ensures { attr } => { - let (arg_copies, copy_clean, ensures_clause) = - build_ensures(&self.annotated_fn.sig, attr); + let (remembers, ensures_clause) = build_ensures(attr); // The code that enforces the postconditions and cleans up the shallow // argument copies (with `mem::forget`). let exec_postconditions = quote!( kani::assert(#ensures_clause, stringify!(#attr_copy)); - #copy_clean ); assert!(matches!( @@ -52,7 +50,7 @@ impl<'a> ContractConditionsHandler<'a> { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( - #arg_copies + #remembers #(#inner)* #exec_postconditions #result diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index c91c307fba2e..defcd9dae1b4 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -242,8 +242,7 @@ //! state. Each occurrence of `old` is lifted, so is is necessary that //! each lifted occurrence is closed with respect to the function arguments. //! The results of these old computations are placed into -//! `remember_kani_internal_XXX` variables of incrementing index to avoid -//! collisions of variable names. Consider the following example: +//! `remember_kani_internal_XXX` variables which are hashed. Consider the following example: //! //! ``` //! #[kani::ensures(|result| old(*ptr + 1) == *ptr)] @@ -265,50 +264,73 @@ //! This expands to //! //! ``` +//! #[kanitool::checked_with = "modify_recursion_wrapper_633496"] +//! #[kanitool::replaced_with = "modify_replace_633496"] +//! #[kanitool::inner_check = "modify_wrapper_633496"] +//! fn modify(ptr: &mut u32) { { *ptr += 1; } } +//! #[allow(dead_code, unused_variables, unused_mut)] +//! #[kanitool::is_contract_generated(recursion_wrapper)] +//! fn modify_recursion_wrapper_633496(arg0: &mut u32) { +//! static mut REENTRY: bool = false; +//! if unsafe { REENTRY } { +//! modify_replace_633496(arg0) +//! } else { +//! unsafe { REENTRY = true }; +//! let result_kani_internal = modify_check_633496(arg0); +//! unsafe { REENTRY = false }; +//! result_kani_internal +//! } +//! } //! #[allow(dead_code, unused_variables, unused_mut)] //! #[kanitool::is_contract_generated(check)] //! fn modify_check_633496(ptr: &mut u32) { //! let _wrapper_arg_1 = //! unsafe { kani::internal::Pointer::decouple_lifetime(&ptr) }; //! kani::assume(*ptr < 100); -//! let remember_kani_internal_1 = *ptr + 1; -//! let ptr_renamed = kani::internal::untracked_deref(&ptr); -//! let remember_kani_internal_0 = *ptr + 1; -//! let ptr_renamed = kani::internal::untracked_deref(&ptr); +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; //! let result_kani_internal: () = modify_wrapper_633496(ptr, _wrapper_arg_1); //! kani::assert((|result| -//! (remember_kani_internal_0) == -//! *ptr_renamed)(&result_kani_internal), +//! (remember_kani_internal_92cc419d8aca576c) == +//! *ptr)(&result_kani_internal), //! "|result| old(*ptr + 1) == *ptr"); -//! std::mem::forget(ptr_renamed); //! kani::assert((|result| -//! (remember_kani_internal_1) == -//! *ptr_renamed)(&result_kani_internal), +//! (remember_kani_internal_92cc419d8aca576c) == +//! *ptr)(&result_kani_internal), //! "|result| old(*ptr + 1) == *ptr"); -//! std::mem::forget(ptr_renamed); //! result_kani_internal //! } //! #[allow(dead_code, unused_variables, unused_mut)] //! #[kanitool::is_contract_generated(replace)] //! fn modify_replace_633496(ptr: &mut u32) { //! kani::assert(*ptr < 100, "*ptr < 100"); -//! let remember_kani_internal_1 = *ptr + 1; -//! let ptr_renamed = kani::internal::untracked_deref(&ptr); -//! let remember_kani_internal_0 = *ptr + 1; -//! let ptr_renamed = kani::internal::untracked_deref(&ptr); +//! 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(ptr) } = -//! kani::any_modifies(); +//! *unsafe { +//! kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(ptr))) +//! } = kani::any_modifies(); //! kani::assume((|result| -//! (remember_kani_internal_0) == -//! *ptr_renamed)(&result_kani_internal)); -//! std::mem::forget(ptr_renamed); +//! (remember_kani_internal_92cc419d8aca576c) == +//! *ptr)(&result_kani_internal)); //! kani::assume((|result| -//! (remember_kani_internal_1) == -//! *ptr_renamed)(&result_kani_internal)); -//! std::mem::forget(ptr_renamed); +//! (remember_kani_internal_92cc419d8aca576c) == +//! *ptr)(&result_kani_internal)); //! result_kani_internal //! } +//! #[kanitool::modifies(_wrapper_arg_1)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! #[kanitool::is_contract_generated(wrapper)] +//! fn modify_wrapper_633496<'_wrapper_arg_1, +//! WrapperArgType1>(ptr: &mut u32, _wrapper_arg_1: &WrapperArgType1) { +//! *ptr += 1; +//! } +//! #[allow(dead_code)] +//! #[kanitool::proof_for_contract = "modify"] +//! fn main() { +//! kani::internal::init_contracts(); +//! { let mut i = kani::any(); modify(&mut i); } +//! } //! ``` use proc_macro::TokenStream; diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 2290cecb5aec..7a522ea98e08 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -80,15 +80,13 @@ impl<'a> ContractConditionsHandler<'a> { ) } ContractConditionsData::Ensures { attr } => { - let (arg_copies, copy_clean, ensures_clause) = - build_ensures(&self.annotated_fn.sig, attr); + let (remembers, ensures_clause) = build_ensures(attr); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( - #arg_copies + #remembers #(#before)* #(#after)* kani::assume(#ensures_clause); - #copy_clean #result ) } @@ -96,7 +94,7 @@ impl<'a> ContractConditionsHandler<'a> { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #(#before)* - #(*unsafe { kani::internal::Pointer::assignable(#attr) } = kani::any_modifies();)* + #(*unsafe { kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(#attr))) } = kani::any_modifies();)* #(#after)* #result ) diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index 5c85d723f686..2682c0781661 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -7,14 +7,13 @@ //! This is so we can keep [`super`] distraction-free as the definitions of data //! structures and the entry point for contract handling. -use std::collections::{HashMap, HashSet}; +use std::collections::HashMap; use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::{quote, ToTokens}; use std::hash::{DefaultHasher, Hash, Hasher}; use syn::{ - spanned::Spanned, visit::Visit, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, - ExprPath, Path, + spanned::Spanned, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, ExprPath, Path, }; use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT}; @@ -102,26 +101,6 @@ pub fn identifier_for_generated_function( Ident::new(&identifier, proc_macro2::Span::mixed_site()) } -/// We make shallow copies of the argument for the postconditions in both -/// `requires` and `ensures` clauses and later clean them up. -/// -/// This function creates the code necessary to both make the copies (first -/// tuple elem) and to clean them (second tuple elem). -pub fn make_unsafe_argument_copies( - renaming_map: &HashMap, -) -> (TokenStream2, TokenStream2) { - let arg_names = renaming_map.values(); - let also_arg_names = renaming_map.values(); - let arg_values = renaming_map.keys(); - ( - quote!(#(let #arg_names = kani::internal::untracked_deref(&#arg_values);)*), - #[cfg(not(feature = "no_core"))] - quote!(#(std::mem::forget(#also_arg_names);)*), - #[cfg(feature = "no_core")] - quote!(#(core::mem::forget(#also_arg_names);)*), - ) -} - /// Used as the "single source of truth" for [`try_as_result_assign`] and [`try_as_result_assign_mut`] /// since we can't abstract over mutability. Input is the object to match on and the name of the /// function used to convert an `Option` into the result type (e.g. `as_ref` and `as_mut` @@ -184,28 +163,20 @@ pub fn try_as_result_assign_mut(stmt: &mut syn::Stmt) -> Option<&mut syn::LocalI /// When a `#[kani::ensures(|result|expr)]` is expanded, this function is called on with `build_ensures(|result|expr)`. /// This function goes through the expr and extracts out all the `old` expressions and creates a sequence /// of statements that instantiate these expressions as `let remember_kani_internal_x = old_expr;` -/// where x is a unique hash. This is returned as the first return parameter along with changing all the -/// variables to `_renamed`. The second parameter is the closing of all the unsafe argument copies. The third -/// return parameter is the expression formed by passing in the result variable into the input closure and -/// changing all the variables to `_renamed`. -pub fn build_ensures( - fn_sig: &syn::Signature, - data: &ExprClosure, -) -> (TokenStream2, TokenStream2, Expr) { +/// where x is a unique hash. This is returned as the first return parameter. The second +/// return parameter is the expression formed by passing in the result variable into the input closure. +pub fn build_ensures(data: &ExprClosure) -> (TokenStream2, Expr) { let mut remembers_exprs = HashMap::new(); let mut vis = OldVisitor { t: OldLifter::new(), remembers_exprs: &mut remembers_exprs }; let mut expr = &mut data.clone(); vis.visit_expr_closure_mut(&mut expr); - let arg_names = rename_argument_occurrences(fn_sig, &mut expr); - let (start, end) = make_unsafe_argument_copies(&arg_names); - let remembers_stmts: TokenStream2 = remembers_exprs .iter() - .fold(start, |collect, (ident, expr)| quote!(let #ident = #expr; #collect)); + .fold(quote!(), |collect, (ident, expr)| quote!(let #ident = #expr; #collect)); let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - (remembers_stmts, end, Expr::Verbatim(quote!((#expr)(&#result)))) + (remembers_stmts, Expr::Verbatim(quote!((#expr)(&#result)))) } trait OldTrigger { @@ -304,76 +275,3 @@ impl OldTrigger for OldLifter { true } } - -/// A supporting function for creating shallow, unsafe copies of the arguments -/// for the postconditions. -/// -/// This function: -/// - Collects all [`Ident`]s found in the argument patterns; -/// - Creates new names for them; -/// - Replaces all occurrences of those idents in `attrs` with the new names and; -/// - Returns the mapping of old names to new names. -fn rename_argument_occurrences( - sig: &syn::Signature, - attr: &mut ExprClosure, -) -> HashMap { - let mut arg_ident_collector = ArgumentIdentCollector::new(); - arg_ident_collector.visit_signature(&sig); - - let mk_new_ident_for = |id: &Ident| Ident::new(&format!("{}_renamed", id), Span::mixed_site()); - let arg_idents = arg_ident_collector - .0 - .into_iter() - .map(|i| { - let new = mk_new_ident_for(&i); - (i, new) - }) - .collect::>(); - - let mut ident_rewriter = Renamer(&arg_idents); - ident_rewriter.visit_expr_closure_mut(attr); - arg_idents -} - -/// Collect all named identifiers used in the argument patterns of a function. -struct ArgumentIdentCollector(HashSet); - -impl ArgumentIdentCollector { - fn new() -> Self { - Self(HashSet::new()) - } -} - -impl<'ast> Visit<'ast> for ArgumentIdentCollector { - fn visit_pat_ident(&mut self, i: &'ast syn::PatIdent) { - self.0.insert(i.ident.clone()); - syn::visit::visit_pat_ident(self, i) - } - fn visit_receiver(&mut self, _: &'ast syn::Receiver) { - self.0.insert(Ident::new("self", proc_macro2::Span::call_site())); - } -} - -/// Applies the contained renaming (key renamed to value) to every ident pattern -/// and ident expr visited. -struct Renamer<'a>(&'a HashMap); - -impl<'a> VisitMut for Renamer<'a> { - fn visit_expr_path_mut(&mut self, i: &mut syn::ExprPath) { - if i.path.segments.len() == 1 { - i.path - .segments - .first_mut() - .and_then(|p| self.0.get(&p.ident).map(|new| p.ident = new.clone())); - } - } - - /// This restores shadowing. Without this we would rename all ident - /// occurrences, but not rebinding location. This is because our - /// [`Self::visit_expr_path_mut`] is scope-unaware. - fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) { - if let Some(new) = self.0.get(&i.ident) { - i.ident = new.clone(); - } - } -} diff --git a/tests/expected/function-contract/modifies/field_replace_pass.rs b/tests/expected/function-contract/modifies/field_replace_pass.rs index 1bbbaf31121a..b73af85d9597 100644 --- a/tests/expected/function-contract/modifies/field_replace_pass.rs +++ b/tests/expected/function-contract/modifies/field_replace_pass.rs @@ -9,7 +9,7 @@ struct S<'a> { #[kani::requires(*s.target < 100)] #[kani::modifies(s.target)] #[kani::ensures(|result| *s.target == prior + 1)] -fn modify(s: S, prior: u32) { +fn modify(s: &mut S, prior: u32) { *s.target += 1; } @@ -20,8 +20,8 @@ fn main() { let i_copy = i; let mut distraction = kani::any(); let distraction_copy = distraction; - let s = S { distraction: &mut distraction, target: &mut i }; - modify(s, i_copy); + let mut s = S { distraction: &mut distraction, target: &mut i }; + modify(&mut s, i_copy); kani::assert(i == i_copy + 1, "Increment"); kani::assert(distraction == distraction_copy, "Unchanged"); }