From 2971595da365d0d7ef7015565223ed15e9f74390 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Tue, 18 Jun 2024 15:09:59 -0400 Subject: [PATCH 1/2] Contracts: History Expressions via "old" monad (#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 #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 Co-authored-by: Justus Adam Co-authored-by: Felipe R. Monteiro --- library/kani/src/contracts.rs | 23 ++ library/kani_macros/Cargo.toml | 2 +- .../src/sysroot/contracts/check.rs | 9 +- .../src/sysroot/contracts/helpers.rs | 18 ++ .../src/sysroot/contracts/initialize.rs | 88 +------- .../kani_macros/src/sysroot/contracts/mod.rs | 86 +++++++- .../src/sysroot/contracts/replace.rs | 9 +- .../src/sysroot/contracts/shared.rs | 205 +++++++++++++++++- rfc/src/rfcs/0009-function-contracts.md | 43 ++++ .../function-contract/history/block.expected | 5 + .../function-contract/history/block.rs | 17 ++ .../history/clone_pass.expected | 5 + .../function-contract/history/clone_pass.rs | 28 +++ .../history/copy_pass.expected | 5 + .../function-contract/history/copy_pass.rs | 28 +++ .../history/function_call.expected | 5 + .../history/function_call.rs | 24 ++ .../history/no_modifies.expected | 5 + .../function-contract/history/no_modifies.rs | 17 ++ .../history/old_old.expected | 2 + .../function-contract/history/old_old.rs | 18 ++ .../history/side_effect.expected | 2 + .../function-contract/history/side_effect.rs | 23 ++ .../history/simple_fail.expected | 7 + .../function-contract/history/simple_fail.rs | 16 ++ .../history/simple_pass.expected | 5 + .../function-contract/history/simple_pass.rs | 16 ++ .../history/simple_pass_twice.expected | 9 + .../history/simple_pass_twice.rs | 17 ++ .../function-contract/history/stub.expected | 9 + .../function-contract/history/stub.rs | 31 +++ .../history/ui/no_args.expected | 1 + .../function-contract/history/ui/no_args.rs | 18 ++ .../history/ui/noncopy_ignore.expected | 1 + .../history/ui/noncopy_ignore.rs | 16 ++ .../history/ui/old_result.expected | 1 + .../history/ui/old_result.rs | 16 ++ .../history/ui/statement.expected | 1 + .../function-contract/history/ui/statement.rs | 16 ++ 39 files changed, 746 insertions(+), 101 deletions(-) create mode 100644 tests/expected/function-contract/history/block.expected create mode 100644 tests/expected/function-contract/history/block.rs create mode 100644 tests/expected/function-contract/history/clone_pass.expected create mode 100644 tests/expected/function-contract/history/clone_pass.rs create mode 100644 tests/expected/function-contract/history/copy_pass.expected create mode 100644 tests/expected/function-contract/history/copy_pass.rs create mode 100644 tests/expected/function-contract/history/function_call.expected create mode 100644 tests/expected/function-contract/history/function_call.rs create mode 100644 tests/expected/function-contract/history/no_modifies.expected create mode 100644 tests/expected/function-contract/history/no_modifies.rs create mode 100644 tests/expected/function-contract/history/old_old.expected create mode 100644 tests/expected/function-contract/history/old_old.rs create mode 100644 tests/expected/function-contract/history/side_effect.expected create mode 100644 tests/expected/function-contract/history/side_effect.rs create mode 100644 tests/expected/function-contract/history/simple_fail.expected create mode 100644 tests/expected/function-contract/history/simple_fail.rs create mode 100644 tests/expected/function-contract/history/simple_pass.expected create mode 100644 tests/expected/function-contract/history/simple_pass.rs create mode 100644 tests/expected/function-contract/history/simple_pass_twice.expected create mode 100644 tests/expected/function-contract/history/simple_pass_twice.rs create mode 100644 tests/expected/function-contract/history/stub.expected create mode 100644 tests/expected/function-contract/history/stub.rs create mode 100644 tests/expected/function-contract/history/ui/no_args.expected create mode 100644 tests/expected/function-contract/history/ui/no_args.rs create mode 100644 tests/expected/function-contract/history/ui/noncopy_ignore.expected create mode 100644 tests/expected/function-contract/history/ui/noncopy_ignore.rs create mode 100644 tests/expected/function-contract/history/ui/old_result.expected create mode 100644 tests/expected/function-contract/history/ui/old_result.rs create mode 100644 tests/expected/function-contract/history/ui/statement.expected create mode 100644 tests/expected/function-contract/history/ui/statement.rs diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index 65b9ec7c01cc..beddd7cc580e 100644 --- a/library/kani/src/contracts.rs +++ b/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}; diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index dbe2126d0458..e0c79a39c105 100644 --- a/library/kani_macros/Cargo.toml +++ b/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. diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index bd4c09b07796..2e46d67a5b8e 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/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 ); diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index baa25b8104e8..174f0f9483d7 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/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))) + }; +} diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index aee0c21bc82d..73621b2aeec5 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/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 { - 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/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 7a25cc390100..c91c307fba2e 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/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, /// The contents of the attribute. - attr: Expr, + attr: ExprClosure, }, Modifies { attr: Vec, diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 1a84e40523c2..2290cecb5aec 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/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 ) diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index bf204e6bca32..5c85d723f686 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -7,11 +7,15 @@ //! 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; +use std::collections::{HashMap, HashSet}; use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::{quote, ToTokens}; -use syn::Attribute; +use std::hash::{DefaultHasher, Hash, Hasher}; +use syn::{ + spanned::Spanned, visit::Visit, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, + ExprPath, Path, +}; use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT}; @@ -176,3 +180,200 @@ pub fn try_as_result_assign(stmt: &syn::Stmt) -> Option<&syn::LocalInit> { pub fn try_as_result_assign_mut(stmt: &mut syn::Stmt) -> Option<&mut syn::LocalInit> { try_as_result_assign_pat!(stmt, as_mut) } + +/// 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) { + 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)); + + let result: Ident = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + (remembers_stmts, end, Expr::Verbatim(quote!((#expr)(&#result)))) +} + +trait OldTrigger { + /// You are provided with the expression that is the first argument of the + /// `old()` call. You may modify it as you see fit. The return value + /// indicates whether the entire `old()` call should be replaced by the + /// (potentially altered) first argument. + /// + /// The second argument is the span of the original `old` expression. + /// + /// The third argument is a collection of all the expressions that need to be lifted + /// into the past environment as new remember variables. + fn trigger(&mut self, e: &mut Expr, s: Span, output: &mut HashMap) -> bool; +} + +struct OldLifter; + +impl OldLifter { + fn new() -> Self { + Self + } +} + +struct OldDenier; + +impl OldTrigger for OldDenier { + fn trigger(&mut self, _: &mut Expr, s: Span, _: &mut HashMap) -> bool { + s.unwrap().error("Nested calls to `old` are prohibited").emit(); + false + } +} + +struct OldVisitor<'a, T> { + t: T, + remembers_exprs: &'a mut HashMap, +} + +impl syn::visit_mut::VisitMut for OldVisitor<'_, T> { + fn visit_expr_mut(&mut self, ex: &mut Expr) { + let trigger = match &*ex { + Expr::Call(call @ ExprCall { func, attrs, args, .. }) => match func.as_ref() { + Expr::Path(ExprPath { + attrs: func_attrs, + qself: None, + path: Path { leading_colon: None, segments }, + }) if segments.len() == 1 + && segments.first().map_or(false, |sgm| sgm.ident == "old") => + { + let first_segment = segments.first().unwrap(); + assert_spanned_err!(first_segment.arguments.is_empty(), first_segment); + assert_spanned_err!(attrs.is_empty(), call); + assert_spanned_err!(func_attrs.is_empty(), func); + assert_spanned_err!(args.len() == 1, call); + true + } + _ => false, + }, + _ => false, + }; + if trigger { + let span = ex.span(); + let new_expr = if let Expr::Call(ExprCall { ref mut args, .. }) = ex { + self.t + .trigger(args.iter_mut().next().unwrap(), span, self.remembers_exprs) + .then(|| args.pop().unwrap().into_value()) + } else { + unreachable!() + }; + if let Some(new) = new_expr { + let _ = std::mem::replace(ex, new); + } + } else { + syn::visit_mut::visit_expr_mut(self, ex) + } + } +} + +impl OldTrigger for OldLifter { + fn trigger( + &mut self, + e: &mut Expr, + _: Span, + remembers_exprs: &mut HashMap, + ) -> bool { + let mut denier = OldVisitor { t: OldDenier, remembers_exprs }; + // This ensures there are no nested calls to `old` + denier.visit_expr_mut(e); + let mut hasher = DefaultHasher::new(); + e.hash(&mut hasher); + let ident = + Ident::new(&format!("remember_kani_internal_{:x}", hasher.finish()), Span::call_site()); + // save the original expression to be lifted into the past remember environment + remembers_exprs.insert(ident.clone(), (*e).clone()); + // change the expression to refer to the new remember variable + let _ = std::mem::replace(e, Expr::Verbatim(quote!((#ident)))); + 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/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md index deeeca66ab7a..a8bd7bf66041 100644 --- a/rfc/src/rfcs/0009-function-contracts.md +++ b/rfc/src/rfcs/0009-function-contracts.md @@ -549,6 +549,49 @@ This is the technical portion of the RFC. Please provide high level details of t +We developed the `old` contract for history expressions via understanding it as a [modality](https://en.wikipedia.org/wiki/Monad_(functional_programming)) originating from [Moggi 1991](https://www.sciencedirect.com/science/article/pii/0890540191900524). +The `old` monad links the "language of the past" to the "language of the present". +Implementing the full generality of the monad is rather difficult, so we focus on a particular usage of the monad. + +We have an external syntax representation which is what the user inputs. We then parse this and logically manipulate it as a monad, prefixing all the `bind` operations. We then output the final compiled macro output as Rust code. + +In particular, if we have an ensures statement like +```rust +#[kani::ensures(old(*ptr)+1==*ptr)] +``` +Then we comprehend this as syntax for the statement (not within Rust) +``` +bind (*ptr : O(u32)) (|remember : u32| remember + 1 == *ptr) +``` +Here, the `O(u32)` is taking the type of the past `u32` and converting it into a type in the present `O(u32)` while the bind operation lets you use the value of the past `u32` to express a type in the present `bool`. + +This then gets compiled to (within Rust) +```rust +let remember = *ptr; +let result = ...; +kani::assert(remember + 1 == *ptr) +``` +This means that the underlying principle of the monad is there, but external syntax appears to be less like a monad because otherwise it would be too difficult to implement, and the user most likely only cares about this particular construction of prefixing all the `bind` operations. + +This construction requires that `old` expressions are closed with resprect to the input parameters. This is due to the lifting into the prefixed `bind` operations. + +A major drawback is that eta expansion fails. If we eta expand a function f, it becomes |x|f(x). Note that eta expansions guarantee that the original f and the |x|f(x) are equivalent which makes a lot of sense since you’re just calling the same function. However, we have that `old(y)` is not equivalent to `(|x|old(x))(y)`. `y` is a closed expression, so the first statement works. `x` is a bound variable, so it is an open expression, so compilation will fail. + +The reason for this restriction is that the user will most likely only want to use this particular prefixed `bind` structure for their code, so exposing the concept of monads to the user level would only confuse the user. It is also simpler from an implementation perspective to limit the monad to this particular usage. + +As for nested old, such as `old(old(*ptr)+*ptr)`, it is reasonable to interpret this as syntax representing +``` +bind (bind(*ptr)(|remember_1| remember_1 + *ptr)) (|remember_0| ...) +``` +which compiles to +```rust +let remember_1 = *ptr; +let remember_0 = remember_1 + *ptr; +let result = ...; +... +``` +so the restriction is just a matter of there not being implementation support for this kind of statement rather than the theory itself. It is not particularly useful to implement this because we claim that there should be no effectful computation within the contracts, so you can substitute the `remember_1` into the second line without worrying about the effects. Hence, we opt for simply restricting this behavior instead of implementing it. (Note: it can be implemented by changing `denier.visit_expr_mut(e);` into `self.visit_expr_mut(e);`) +