Merge remote-tracking branch 'origin/main' into cbmc-6

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,14 +33,13 @@ 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 (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(#attr, stringify!(#attr_copy));
-                    #copy_clean
+                    kani::assert(#ensures_clause, stringify!(#attr_copy));
                 );
 
                 assert!(matches!(
@@ -51,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/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,114 @@
 //!     }
 //! }
 //! ```
+//!
+//! 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 which are hashed. 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
+//!
+//! ```
+//! #[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_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_92cc419d8aca576c) ==
+//!                         *ptr)(&result_kani_internal),
+//!         "|result| old(*ptr + 1) == *ptr");
+//!     kani::assert((|result|
+//!                     (remember_kani_internal_92cc419d8aca576c) ==
+//!                         *ptr)(&result_kani_internal),
+//!         "|result| old(*ptr + 1) == *ptr");
+//!     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_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((|result|
+//!                     (remember_kani_internal_92cc419d8aca576c) ==
+//!                         *ptr)(&result_kani_internal));
+//!     kani::assume((|result|
+//!                     (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;
 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 +451,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,23 +79,22 @@ 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 (remembers, ensures_clause) = build_ensures(attr);
                 let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
                 quote!(
-                    #arg_copies
+                    #remembers
                     #(#before)*
                     #(#after)*
-                    kani::assume(#attr);
-                    #copy_clean
+                    kani::assume(#ensures_clause);
                     #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
                 )