Function Contracts: remove instances of _renamed (model-checking#3274)

The current method for creating the modifies wrapper requires changing
the `ensures` clause to have `_renamed` variables which are unsafe
copies of the original function arguments. This causes issues with
regards to some possible tests as in model-checking#3239.

This change removes the `_renamed` variables and instead simply changes
the modifies clauses within the replace to unsafely dereference the
pointer to modify the contents of it unsafely, condensing all instances
of unsafe Rust into a single location.

Resolves model-checking#3239
Resolves model-checking#3026
May affect model-checking#3027. In my attempt to run this example with slight
modification to fit the current implementation, I got the error `CBMC
appears to have run out of memory. You may want to rerun your proof in
an environment with additional memory or use stubbing to reduce the size
of the code the verifier reasons about.` This suggests that the
compilation is working appropriately but the test case is just too large
for CBMC.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Co-authored-by: Matias Scharager <[email protected]>

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

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;

library/kani_macros/src/sysroot/contracts/replace.rs

@@ -80,23 +80,21 @@ 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
                 )
             }
             ContractConditionsData::Modifies { attr } => {
                 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
                 )

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<Ident, Ident>,
-) -> (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<LocalInit>` 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<Ident, Ident> {
-    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::<HashMap<_, _>>();
-
-    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<Ident>);
-
-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<Ident, Ident>);
-
-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();
-        }
-    }
-}

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");
 }