Contracts: History Expressions via "old" monad

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/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, count_remembers, try_as_result_assign_mut},
     ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
 };
 
@@ -25,6 +25,7 @@ impl<'a> ContractConditionsHandler<'a> {
     pub fn make_check_body(&mut self) -> TokenStream2 {
         let mut inner = self.ensure_bootstrapped_check_body();
         let Self { attr_copy, .. } = self;
+        let remember_count: usize = count_remembers(&inner);
 
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
@@ -33,13 +34,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, remember_count);
 
                 // 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, count_remembers, try_as_result_assign},
     ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
 };
 
@@ -67,6 +67,7 @@ impl<'a> ContractConditionsHandler<'a> {
     /// generating a replace function.
     fn make_replace_body(&self) -> TokenStream2 {
         let (before, after) = self.ensure_bootstrapped_replace_body();
+        let remember_count = count_remembers(&before);
 
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
@@ -79,14 +80,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, remember_count);
                 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
                 )