Contracts: History Expressions via "old" monad (model-checking#3232)

Add support for History Expressions. This allows an ensures clause to
evaluate expressions before the function runs, bing them to anonymous
variables and use them after calculating the result to be able to
compare to the state before the function evaluation.

Resolves model-checking#2803

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]>
Co-authored-by: Justus Adam <[email protected]>
Co-authored-by: Felipe R. Monteiro <[email protected]>

library/kani/src/contracts.rs

@@ -225,4 +225,27 @@
 //! Rust pointer type (`&T`, `&mut T`, `*const T` or `*mut T`). In addition `T`
 //! must implement [`Arbitrary`](super::Arbitrary). This is used to assign
 //! `kani::any()` to the location when the function is used in a `stub_verified`.
+//!
+//! ## History Expressions
+//!
+//! Additionally, an ensures clause is allowed to refer to the state of the function arguments before function execution and perform simple computations on them
+//! via an `old` monad. Any instance of `old(computation)` will evaluate the
+//! computation before the function is called. It is required that this computation
+//! is effect free and closed with respect to the function arguments.
+//!
+//! For example, the following code passes kani tests:
+//!
+//! ```
+//! #[kani::modifies(a)]
+//! #[kani::ensures(|result| old(*a).wrapping_add(1) == *a)]
+//! #[kani::ensures(|result : &u32| old(*a).wrapping_add(1) == *result)]
+//! fn add1(a : &mut u32) -> u32 {
+//!     *a=a.wrapping_add(1);
+//!     *a
+//! }
+//! ```
+//!
+//! Here, the value stored in `a` is precomputed and remembered after the function
+//! is called, even though the contents of `a` changed during the function execution.
+//!
 pub use super::{ensures, modifies, proof_for_contract, requires, stub_verified};

library/kani_macros/Cargo.toml

@@ -15,7 +15,7 @@ proc-macro = true
 proc-macro2 = "1.0"
 proc-macro-error = "1.0.4"
 quote = "1.0.20"
-syn = { version = "2.0.18", features = ["full", "visit-mut", "visit"] }
+syn = { version = "2.0.18", features = ["full", "visit-mut", "visit", "extra-traits"] }
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.

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

@@ -9,7 +9,7 @@ use syn::{Expr, FnArg, ItemFn, Token};
 
 use super::{
     helpers::*,
-    shared::{make_unsafe_argument_copies, try_as_result_assign_mut},
+    shared::{build_ensures, try_as_result_assign_mut},
     ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
 };
 
@@ -33,13 +33,14 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#inner)*
                 )
             }
-            ContractConditionsData::Ensures { argument_names, attr } => {
-                let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names);
+            ContractConditionsData::Ensures { attr } => {
+                let (arg_copies, copy_clean, ensures_clause) =
+                    build_ensures(&self.annotated_fn.sig, attr);
 
                 // The code that enforces the postconditions and cleans up the shallow
                 // argument copies (with `mem::forget`).
                 let exec_postconditions = quote!(
-                    kani::assert(#attr, stringify!(#attr_copy));
+                    kani::assert(#ensures_clause, stringify!(#attr_copy));
                     #copy_clean
                 );
 

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

@@ -268,3 +268,21 @@ pub fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 {
     let long_hash = hasher.finish();
     long_hash % SIX_HEX_DIGITS_MASK
 }
+
+macro_rules! assert_spanned_err {
+    ($condition:expr, $span_source:expr, $msg:expr, $($args:expr),+) => {
+        if !$condition {
+            $span_source.span().unwrap().error(format!($msg, $($args),*)).emit();
+            assert!(false);
+        }
+    };
+    ($condition:expr, $span_source:expr, $msg:expr $(,)?) => {
+        if !$condition {
+            $span_source.span().unwrap().error($msg).emit();
+            assert!(false);
+        }
+    };
+    ($condition:expr, $span_source:expr) => {
+        assert_spanned_err!($condition, $span_source, concat!("Failed assertion ", stringify!($condition)))
+    };
+}

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

@@ -3,17 +3,14 @@
 
 //! Initialization routine for the contract handler
 
-use std::collections::{HashMap, HashSet};
-
 use proc_macro::{Diagnostic, TokenStream};
-use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
-use quote::quote;
-use syn::{spanned::Spanned, visit::Visit, visit_mut::VisitMut, Expr, ExprClosure, ItemFn};
+use proc_macro2::{Ident, TokenStream as TokenStream2};
+use syn::{spanned::Spanned, ItemFn};
 
 use super::{
     helpers::{chunks_by, is_token_stream_2_comma, matches_path},
     ContractConditionsData, ContractConditionsHandler, ContractConditionsType,
-    ContractFunctionState, INTERNAL_RESULT_IDENT,
+    ContractFunctionState,
 };
 
 impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState {
@@ -82,11 +79,7 @@ impl<'a> ContractConditionsHandler<'a> {
                 ContractConditionsData::Requires { attr: syn::parse(attr)? }
             }
             ContractConditionsType::Ensures => {
-                let mut data: ExprClosure = syn::parse(attr)?;
-                let argument_names = rename_argument_occurrences(&annotated_fn.sig, &mut data);
-                let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-                let app: Expr = Expr::Verbatim(quote!((#data)(&#result)));
-                ContractConditionsData::Ensures { argument_names, attr: app }
+                ContractConditionsData::Ensures { attr: syn::parse(attr)? }
             }
             ContractConditionsType::Modifies => {
                 ContractConditionsData::new_modifies(attr, &mut output)
@@ -115,76 +108,3 @@ impl ContractConditionsData {
         ContractConditionsData::Modifies { attr }
     }
 }
-
-/// 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();
-        }
-    }
-}

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

@@ -233,15 +233,92 @@
 //!     }
 //! }
 //! ```
+//!
+//! Additionally, there is functionality that allows the referencing of
+//! history values within the ensures statement. This means we can
+//! precompute a value before the function is called and have access to
+//! this value in the later ensures statement. This is done via the
+//! `old` monad which lets you access the old state within the present
+//! 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:
+//!
+//! ```
+//! #[kani::ensures(|result| old(*ptr + 1) == *ptr)]
+//! #[kani::ensures(|result| old(*ptr + 1) == *ptr)]
+//! #[kani::requires(*ptr < 100)]
+//! #[kani::modifies(ptr)]
+//! fn modify(ptr: &mut u32) {
+//!     *ptr += 1;
+//! }
+//!
+//! #[kani::proof_for_contract(modify)]
+//! fn main() {
+//!     let mut i = kani::any();
+//!     modify(&mut i);
+//! }
+//!
+//! ```
+//!
+//! This expands to
+//!
+//! ```
+//! #[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 result_kani_internal: () = modify_wrapper_633496(ptr, _wrapper_arg_1);
+//!     kani::assert((|result|
+//!                     (remember_kani_internal_0) ==
+//!                         *ptr_renamed)(&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),
+//!         "|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 result_kani_internal: () = kani::any_modifies();
+//!     *unsafe { kani::internal::Pointer::assignable(ptr) } =
+//!         kani::any_modifies();
+//!     kani::assume((|result|
+//!                     (remember_kani_internal_0) ==
+//!                         *ptr_renamed)(&result_kani_internal));
+//!     std::mem::forget(ptr_renamed);
+//!     kani::assume((|result|
+//!                     (remember_kani_internal_1) ==
+//!                         *ptr_renamed)(&result_kani_internal));
+//!     std::mem::forget(ptr_renamed);
+//!     result_kani_internal
+//! }
+//! ```
 
 use proc_macro::TokenStream;
 use proc_macro2::{Ident, TokenStream as TokenStream2};
 use quote::{quote, ToTokens};
-use std::collections::HashMap;
-use syn::{parse_macro_input, Expr, ItemFn};
+use syn::{parse_macro_input, Expr, ExprClosure, ItemFn};
 
 mod bootstrap;
 mod check;
+#[macro_use]
 mod helpers;
 mod initialize;
 mod replace;
@@ -352,11 +429,8 @@ enum ContractConditionsData {
         attr: Expr,
     },
     Ensures {
-        /// Translation map from original argument names to names of the copies
-        /// we will be emitting.
-        argument_names: HashMap<Ident, Ident>,
         /// The contents of the attribute.
-        attr: Expr,
+        attr: ExprClosure,
     },
     Modifies {
         attr: Vec<Expr>,

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

@@ -8,7 +8,7 @@ use quote::quote;
 
 use super::{
     helpers::*,
-    shared::{make_unsafe_argument_copies, try_as_result_assign},
+    shared::{build_ensures, try_as_result_assign},
     ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
 };
 
@@ -79,14 +79,15 @@ impl<'a> ContractConditionsHandler<'a> {
                     #result
                 )
             }
-            ContractConditionsData::Ensures { attr, argument_names } => {
-                let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names);
+            ContractConditionsData::Ensures { attr } => {
+                let (arg_copies, copy_clean, ensures_clause) =
+                    build_ensures(&self.annotated_fn.sig, attr);
                 let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
                 quote!(
                     #arg_copies
                     #(#before)*
                     #(#after)*
-                    kani::assume(#attr);
+                    kani::assume(#ensures_clause);
                     #copy_clean
                     #result
                 )