From bac0d0edc84d7a3e0a3a11a8df59e5e17d1e7313 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 8 Jul 2024 13:18:16 -0700 Subject: [PATCH 01/18] Initial refactoring of contracts Initial setup works with only one annotation. Next steps: 1. Adjust compiler to search for the closures. 2. Handle multiple annotations. --- .../src/sysroot/contracts/bootstrap.rs | 113 ++++----- .../src/sysroot/contracts/check.rs | 223 +++++------------- .../src/sysroot/contracts/helpers.rs | 37 ++- .../src/sysroot/contracts/initialize.rs | 37 +-- .../kani_macros/src/sysroot/contracts/mod.rs | 152 ++++-------- .../src/sysroot/contracts/replace.rs | 34 +-- .../src/sysroot/contracts/shared.rs | 71 +----- .../function-contract/trait_impls/methods.rs | 35 +++ 8 files changed, 238 insertions(+), 464 deletions(-) create mode 100644 tests/expected/function-contract/trait_impls/methods.rs diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index dee0bca42c54..a1282d61b3ef 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -4,106 +4,79 @@ //! Special way we handle the first time we encounter a contract attribute on a //! function. -use proc_macro2::{Ident, Span}; +use proc_macro2::{Ident, Span, TokenStream}; use quote::quote; -use syn::ItemFn; +use syn::{ExprClosure, FnArg, ItemFn, Signature}; -use super::{ - helpers::*, shared::identifier_for_generated_function, ContractConditionsHandler, - INTERNAL_RESULT_IDENT, -}; +use super::{helpers::*, ContractConditionsHandler, INTERNAL_RESULT_IDENT}; impl<'a> ContractConditionsHandler<'a> { - /// The complex case. We are the first time a contract is handled on this function, so - /// we're responsible for + /// Generate initial contract. /// - /// 1. Generating a name for the check function - /// 2. Emitting the original, unchanged item and register the check - /// function on it via attribute - /// 3. Renaming our item to the new name - /// 4. And (minor point) adding #[allow(dead_code)] and - /// #[allow(unused_variables)] to the check function attributes + /// 1. Generating the body for all the closures used by contracts. + /// - The recursion closure body is always the same, and it is generated in this stage. + /// - The other closures body will depend on which annotation is being processed. + /// 2. Emitting the extended function with the new closures and the new contract attributes pub fn handle_untouched(&mut self) { - // We'll be using this to postfix the generated names for the "check" - // and "replace" functions. - let item_hash = self.hash.unwrap(); + let replace_name = &self.replace_name; + let modifies_name = &self.modify_name; + let recursion_name = &self.recursion_name; - let original_function_name = self.annotated_fn.sig.ident.clone(); - - let check_fn_name = - identifier_for_generated_function(&original_function_name, "check", item_hash); - let replace_fn_name = - identifier_for_generated_function(&original_function_name, "replace", item_hash); - let recursion_wrapper_name = identifier_for_generated_function( - &original_function_name, - "recursion_wrapper", - item_hash, - ); - - // Constructing string literals explicitly here, because `stringify!` - // doesn't work. Let's say we have an identifier `check_fn` and we were - // to do `quote!(stringify!(check_fn))` to try to have it expand to - // `"check_fn"` in the generated code. Then when the next macro parses - // this it will *not* see the literal `"check_fn"` as you may expect but - // instead the *expression* `stringify!(check_fn)`. - let replace_fn_name_str = syn::LitStr::new(&replace_fn_name.to_string(), Span::call_site()); - let wrapper_fn_name_str = - syn::LitStr::new(&self.make_wrapper_name().to_string(), Span::call_site()); - let recursion_wrapper_name_str = - syn::LitStr::new(&recursion_wrapper_name.to_string(), Span::call_site()); + let recursion_closure = self.recursion_closure(); + let replace_closure = self.replace_closure(); + println!("{recursion_closure}"); // The order of `attrs` and `kanitool::{checked_with, // is_contract_generated}` is important here, because macros are // expanded outside in. This way other contract annotations in `attrs` // sees those attributes and can use them to determine // `function_state`. - // - // The same care is taken when we emit check and replace functions. - // emit the check function. - let is_impl_fn = is_probably_impl_fn(&self.annotated_fn); let ItemFn { attrs, vis, sig, block } = &self.annotated_fn; self.output.extend(quote!( #(#attrs)* - #[kanitool::checked_with = #recursion_wrapper_name_str] - #[kanitool::replaced_with = #replace_fn_name_str] - #[kanitool::inner_check = #wrapper_fn_name_str] + #[kanitool::checked_with = #recursion_name] + #[kanitool::replaced_with = #replace_name] + #[kanitool::inner_check = #modifies_name] #vis #sig { + #replace_closure + #recursion_closure + // -- Now emit the original code. #block } )); + } - let mut wrapper_sig = sig.clone(); - wrapper_sig.ident = recursion_wrapper_name; - // We use non-constant functions, thus, the wrapper cannot be constant. - wrapper_sig.constness = None; + /// Generate the tokens for the recursion closure. + fn recursion_closure(&self) -> TokenStream { + let ItemFn { ref sig, .. } = self.annotated_fn; + let (inputs, args) = closure_args(&sig.inputs); + let output = &sig.output; + let span = Span::call_site(); + let result = Ident::new(INTERNAL_RESULT_IDENT, span); + let replace_ident = Ident::new(&self.replace_name, span); + let check_ident = Ident::new(&self.check_name, span); + let recursion_ident = Ident::new(&self.recursion_name, span); - let args = pats_to_idents(&mut wrapper_sig.inputs).collect::>(); - let also_args = args.iter(); - let (call_check, call_replace) = if is_impl_fn { - (quote!(Self::#check_fn_name), quote!(Self::#replace_fn_name)) - } else { - (quote!(#check_fn_name), quote!(#replace_fn_name)) - }; + let replace_closure = self.replace_closure(); + let check_closure = self.check_closure(); - let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - self.output.extend(quote!( + quote!( + #[kanitool::is_contract_generated(recursion_check)] #[allow(dead_code, unused_variables, unused_mut)] - #[kanitool::is_contract_generated(recursion_wrapper)] - #wrapper_sig { + let mut #recursion_ident = |#inputs| #output + { static mut REENTRY: bool = false; if unsafe { REENTRY } { - #call_replace(#(#args),*) + #replace_closure + #replace_ident(#(#args),*) } else { + #check_closure unsafe { REENTRY = true }; - let #result = #call_check(#(#also_args),*); + let #result = #check_ident(#(#args),*); unsafe { REENTRY = false }; #result } - } - )); - - self.emit_check_function(Some(check_fn_name)); - self.emit_replace_function(Some(replace_fn_name)); - self.emit_augmented_modifies_wrapper(); + }; + ) } } diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index e76286b398cb..3609ccb96f90 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -5,7 +5,7 @@ use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::quote; -use syn::{Expr, FnArg, ItemFn, Token}; +use syn::{parse_quote, Expr, FnArg, ItemFn, Token}; use super::{ helpers::*, @@ -22,15 +22,15 @@ impl<'a> ContractConditionsHandler<'a> { /// /// Mutable because a `modifies` clause may need to extend the inner call to /// the wrapper with new arguments. - pub fn make_check_body(&mut self) -> TokenStream2 { - let mut inner = self.ensure_bootstrapped_check_body(); + pub fn make_check_body(&self) -> TokenStream2 { + let mut body_stmts = self.get_check_body(); let Self { attr_copy, .. } = self; match &self.condition_type { ContractConditionsData::Requires { attr } => { quote!( kani::assume(#attr); - #(#inner)* + #(#body_stmts)* ) } ContractConditionsData::Ensures { attr } => { @@ -42,25 +42,20 @@ impl<'a> ContractConditionsHandler<'a> { kani::assert(#ensures_clause, stringify!(#attr_copy)); ); - assert!(matches!( - inner.pop(), - Some(syn::Stmt::Expr(syn::Expr::Path(pexpr), None)) - if pexpr.path.get_ident().map_or(false, |id| id == INTERNAL_RESULT_IDENT) - )); - - let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + let return_expr = body_stmts.pop(); quote!( #remembers - #(#inner)* + #(#body_stmts)* #exec_postconditions - #result + #return_expr ) } ContractConditionsData::Modifies { attr } => { - let wrapper_name = self.make_wrapper_name().to_string(); + let wrapper_name = &self.modify_name; - let wrapper_args = if let Some(wrapper_call_args) = - inner.iter_mut().find_map(|stmt| try_as_wrapper_call_args(stmt, &wrapper_name)) + let wrapper_args = if let Some(wrapper_call_args) = body_stmts + .iter_mut() + .find_map(|stmt| try_as_wrapper_call_args(stmt, &wrapper_name)) { let wrapper_args = make_wrapper_idents( wrapper_call_args.len(), @@ -71,64 +66,55 @@ impl<'a> ContractConditionsHandler<'a> { .extend(wrapper_args.clone().map(|a| Expr::Verbatim(quote!(#a)))); wrapper_args } else { - unreachable!( - "Invariant broken, check function did not contain a call to the wrapper function" - ) + unreachable!("Expected check function to call to the modifies wrapper function") }; quote!( - #(let #wrapper_args = unsafe { kani::internal::Pointer::decouple_lifetime(&#attr) };)* - #(#inner)* + // Cast to *const () since we only care about the address. + #(let #wrapper_args = #attr as *const _ as *const ();)* + #(#body_stmts)* ) } } } - /// Get the sequence of statements of the previous check body or create the default one. - fn ensure_bootstrapped_check_body(&self) -> Vec { - let wrapper_name = self.make_wrapper_name(); + /// Get the body of the previous check closure. + fn get_check_body(&self) -> Vec { + let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); let return_type = return_type_to_type(&self.annotated_fn.sig.output); + let modifies_closure = self.modifies_closure(); if self.is_first_emit() { - let args = exprs_for_args(&self.annotated_fn.sig.inputs); - let wrapper_call = if is_probably_impl_fn(self.annotated_fn) { - quote!(Self::#wrapper_name) - } else { - quote!(#wrapper_name) - }; + let (_, args) = closure_args(&self.annotated_fn.sig.inputs); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - syn::parse_quote!( - let #result : #return_type = #wrapper_call(#(#args),*); + parse_quote!( + #modifies_closure + let #result : #return_type = #modifies_ident(#(#args),*); #result ) } else { - self.annotated_fn.block.stmts.clone() + todo!("Find old body"); + // self.annotated_fn.block.stmts.clone() } } - /// Emit the check function into the output stream. + /// Generate a token stream that represents the check closure. /// /// See [`Self::make_check_body`] for the most interesting parts of this /// function. - pub fn emit_check_function(&mut self, override_function_dent: Option) { - self.emit_common_header(); - - if self.function_state.emit_tag_attr() { - // If it's the first time we also emit this marker. Again, order is - // important so this happens as the last emitted attribute. - self.output.extend(quote!(#[kanitool::is_contract_generated(check)])); - } + pub fn check_closure(&self) -> TokenStream2 { + let check_ident = Ident::new(&self.check_name, Span::call_site()); + let sig = &self.annotated_fn.sig; + let (inputs, _args) = closure_args(&sig.inputs); + let output = &sig.output; let body = self.make_check_body(); - let mut sig = self.annotated_fn.sig.clone(); - // We use non-constant functions, thus, the wrapper cannot be constant. - sig.constness = None; - if let Some(ident) = override_function_dent { - sig.ident = ident; - } - self.output.extend(quote!( - #sig { + + quote!( + #[kanitool::is_contract_generated(replace)] + #[allow(dead_code, unused_variables, unused_mut)] + let mut #check_ident = |#inputs| #output { #body - } - )) + }; + ) } /// Emit a modifies wrapper, possibly augmenting a prior, existing one. @@ -140,63 +126,27 @@ impl<'a> ContractConditionsHandler<'a> { /// implement `kani::Arbitrary` for checking. Now, we annotate each /// argument with a generic type parameter, so the compiler can /// continue inferring the correct types. - pub fn emit_augmented_modifies_wrapper(&mut self) { - if let ContractConditionsData::Modifies { attr } = &self.condition_type { - let wrapper_args = make_wrapper_idents( - self.annotated_fn.sig.inputs.len(), - attr.len(), - WRAPPER_ARG_PREFIX, - ); - // Generate a unique type parameter identifier - let type_params = make_wrapper_idents( - self.annotated_fn.sig.inputs.len(), - attr.len(), - "WrapperArgType", - ); - let sig = &mut self.annotated_fn.sig; - for (arg, arg_type) in wrapper_args.clone().zip(type_params) { - // Add the type parameter to the function signature's generic parameters list - sig.generics.params.push(syn::GenericParam::Type(syn::TypeParam { - attrs: vec![], - ident: arg_type.clone(), - colon_token: None, - bounds: Default::default(), - eq_token: None, - default: None, - })); - let lifetime = syn::Lifetime { apostrophe: Span::call_site(), ident: arg.clone() }; - sig.inputs.push(FnArg::Typed(syn::PatType { - attrs: vec![], - colon_token: Token![:](Span::call_site()), - pat: Box::new(syn::Pat::Verbatim(quote!(#arg))), - ty: Box::new(syn::parse_quote! { &#arg_type }), - })); - sig.generics.params.push(syn::GenericParam::Lifetime(syn::LifetimeParam { - lifetime, - colon_token: None, - bounds: Default::default(), - attrs: vec![], - })); - } - - self.output.extend(quote!(#[kanitool::modifies(#(#wrapper_args),*)])) - } - self.emit_common_header(); - - if self.function_state.emit_tag_attr() { - // If it's the first time we also emit this marker. Again, order is - // important so this happens as the last emitted attribute. - self.output.extend(quote!(#[kanitool::is_contract_generated(wrapper)])); - } - - let name = self.make_wrapper_name(); - let ItemFn { vis, sig, block, .. } = self.annotated_fn; - - let mut sig = sig.clone(); - sig.ident = name; - self.output.extend(quote!( - #vis #sig #block - )); + pub fn modifies_closure(&self) -> TokenStream2 { + // TODO: Get existing signature. + let sig = &self.annotated_fn.sig; + let wrapper_args: Vec<_> = + if let ContractConditionsData::Modifies { attr } = &self.condition_type { + make_wrapper_idents(sig.inputs.len(), attr.len(), WRAPPER_ARG_PREFIX).collect() + } else { + make_wrapper_idents(sig.inputs.len(), 0, WRAPPER_ARG_PREFIX).collect() + }; + let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); + let (inputs, _args) = closure_args(&sig.inputs); + let output = &sig.output; + let body = &self.annotated_fn.block; + quote!( + #[kanitool::is_contract_generated(wrapper)] + #(#[kanitool::modifies(#wrapper_args)])* + #[allow(dead_code, unused_variables, unused_mut)] + let mut #modifies_ident = |#inputs #(, #wrapper_args: *const ())*| #output { + #body + }; + ) } } @@ -233,58 +183,3 @@ fn make_wrapper_idents( ) -> impl Iterator + Clone + 'static { (low..).map(move |i| Ident::new(&format!("{prefix}{i}"), Span::mixed_site())).take(num) } - -#[cfg(test)] -mod test { - macro_rules! detect_impl_fn { - ($expect_pass:expr, $($tt:tt)*) => {{ - let syntax = stringify!($($tt)*); - let ast = syn::parse_str(syntax).unwrap(); - assert!($expect_pass == super::is_probably_impl_fn(&ast), - "Incorrect detection.\nExpected is_impl_fun: {}\nInput Expr; {}\nParsed: {:?}", - $expect_pass, - syntax, - ast - ); - }} - } - - #[test] - fn detect_impl_fn_by_receiver() { - detect_impl_fn!(true, fn self_by_ref(&self, u: usize) -> bool {}); - - detect_impl_fn!(true, fn self_by_self(self, u: usize) -> bool {}); - } - - #[test] - fn detect_impl_fn_by_self_ty() { - detect_impl_fn!(true, fn self_by_construct(u: usize) -> Self {}); - detect_impl_fn!(true, fn self_by_wrapped_construct(u: usize) -> Arc {}); - - detect_impl_fn!(true, fn self_by_other_arg(u: usize, slf: Self) {}); - - detect_impl_fn!(true, fn self_by_other_wrapped_arg(u: usize, slf: Vec) {}) - } - - #[test] - fn detect_impl_fn_by_qself() { - detect_impl_fn!( - true, - fn self_by_mention(u: usize) { - Self::other(u) - } - ); - } - - #[test] - fn detect_no_impl_fn() { - detect_impl_fn!( - false, - fn self_by_mention(u: usize) { - let self_name = 18; - let self_lit = "self"; - let self_lit = "Self"; - } - ); - } -} diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index 174f0f9483d7..2b8c9dc7ad53 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -7,7 +7,9 @@ use proc_macro2::{Ident, Span}; use quote::{quote, ToTokens}; use std::borrow::Cow; -use syn::{spanned::Spanned, visit::Visit, Expr, FnArg, ItemFn}; +use syn::punctuated::Punctuated; +use syn::token::Comma; +use syn::{spanned::Spanned, visit::Visit, Expr, FnArg, ItemFn, Pat}; /// If an explicit return type was provided it is returned, otherwise `()`. pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { @@ -175,25 +177,20 @@ pub fn is_probably_impl_fn(fun: &ItemFn) -> bool { self_detector.0 } -/// Convert every use of a pattern in this signature to a simple, fresh, binding-only -/// argument ([`syn::PatIdent`]) and return the [`Ident`] that was generated. -pub fn pats_to_idents

( - sig: &mut syn::punctuated::Punctuated, -) -> impl Iterator + '_ { - sig.iter_mut().enumerate().map(|(i, arg)| match arg { - syn::FnArg::Receiver(_) => Ident::from(syn::Token![self](Span::call_site())), - syn::FnArg::Typed(syn::PatType { pat, .. }) => { - let ident = Ident::new(&format!("arg{i}"), Span::mixed_site()); - *pat.as_mut() = syn::Pat::Ident(syn::PatIdent { - attrs: vec![], - by_ref: None, - mutability: None, - ident: ident.clone(), - subpat: None, - }); - ident - } - }) +/// Extract the closure arguments which should skip `self`. +/// +/// Return the declaration form as well as just a plain list of idents for each. +pub fn closure_args( + inputs: &Punctuated, +) -> (Punctuated<&syn::FnArg, Comma>, Vec<&Ident>) { + inputs + .iter() + .filter_map(|arg| { + let FnArg::Typed(syn::PatType { pat, .. }) = arg else { return None }; + let Pat::Ident(pat_ident) = pat.as_ref() else { return None }; + Some((arg, &pat_ident.ident)) + }) + .collect() } /// Does the provided path have the same chain of identifiers as `mtch` (match) diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index 73621b2aeec5..fc802ceb1369 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/library/kani_macros/src/sysroot/contracts/initialize.rs @@ -19,24 +19,9 @@ impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState { /// Find out if this attribute could be describing a "contract handling" /// state and if so return it. fn try_from(attribute: &'a syn::Attribute) -> Result { - if let syn::Meta::List(lst) = &attribute.meta { - if matches_path(&lst.path, &["kanitool", "is_contract_generated"]) { - let ident = syn::parse2::(lst.tokens.clone()) - .map_err(|e| Some(lst.span().unwrap().error(format!("{e}"))))?; - let ident_str = ident.to_string(); - return match ident_str.as_str() { - "check" => Ok(Self::Check), - "replace" => Ok(Self::Replace), - "wrapper" => Ok(Self::ModifiesWrapper), - _ => { - Err(Some(lst.span().unwrap().error("Expected `check` or `replace` ident"))) - } - }; - } - } if let syn::Meta::NameValue(nv) = &attribute.meta { if matches_path(&nv.path, &["kanitool", "checked_with"]) { - return Ok(ContractFunctionState::Original); + return Ok(ContractFunctionState::Expanded); } } Err(None) @@ -71,7 +56,6 @@ impl<'a> ContractConditionsHandler<'a> { attr: TokenStream, annotated_fn: &'a mut ItemFn, attr_copy: TokenStream2, - hash: Option, ) -> Result { let mut output = TokenStream2::new(); let condition_type = match is_requires { @@ -86,7 +70,24 @@ impl<'a> ContractConditionsHandler<'a> { } }; - Ok(Self { function_state, condition_type, annotated_fn, attr_copy, output, hash }) + let fn_name = &annotated_fn.sig.ident; + let generate_name = |purpose| format!("__kani_{purpose}_{fn_name}"); + let check_name = generate_name("check"); + let replace_name = generate_name("replace"); + let recursion_name = generate_name("recursion_check"); + let modifies_name = generate_name("modifies"); + + Ok(Self { + function_state, + condition_type, + annotated_fn, + attr_copy, + output, + check_name, + replace_name, + recursion_name, + modify_name: modifies_name, + }) } } impl ContractConditionsData { diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index defcd9dae1b4..5ec76370b1cf 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -26,26 +26,23 @@ //! instead of throwing a hard error but this means we cannot detect if a given //! function has further contract attributes placed on it during any given //! expansion. As a result every expansion needs to leave the code in a valid -//! state that could be used for all contract functionality but it must alow +//! state that could be used for all contract functionality, but it must allow //! further contract attributes to compose with what was already generated. In -//! addition we also want to make sure to support non-contract attributes on +//! addition, we also want to make sure to support non-contract attributes on //! functions with contracts. //! //! To this end we use a state machine. The initial state is an "untouched" //! function with possibly multiple contract attributes, none of which have been //! expanded. When we expand the first (outermost) `requires` or `ensures` -//! attribute on such a function we re-emit the function unchanged but we also -//! generate fresh "check" and "replace" functions that enforce the condition +//! attribute on such a function we re-emit the function with a few closures defined +//! in their body, which correspond to the "check" and "replace" that enforce the condition //! carried by the attribute currently being expanded. //! -//! We don't copy all attributes from the original function since they may have -//! unintended consequences for the stubs, such as `inline` or `rustc_diagnostic_item`. -//! -//! We also add new marker attributes to -//! advance the state machine. The "check" function gets a +//! We also add new marker attributes to the original function to +//! advance the state machine. The "check" closure gets a //! `kanitool::is_contract_generated(check)` attributes and analogous for //! replace. The re-emitted original meanwhile is decorated with -//! `kanitool::checked_with(name_of_generated_check_function)` and an analogous +//! `kanitool::checked_with(name_of_generated_check_variable)` and an analogous //! `kanittool::replaced_with` attribute also. The next contract attribute that //! is expanded will detect the presence of these markers in the attributes of //! the item and be able to determine their position in the state machine this @@ -67,42 +64,24 @@ //! │ Function │ //! └─────┬─────┘ //! │ -//! Emit │ Generate + Copy Attributes -//! ┌─────────────────┴─────┬──────────┬─────────────────┐ -//! │ │ │ │ -//! │ │ │ │ -//! ▼ ▼ ▼ ▼ -//! ┌──────────┐ ┌───────────┐ ┌───────┐ ┌─────────┐ -//! │ Original │◄─┐ │ Recursion │ │ Check │◄─┐ │ Replace │◄─┐ -//! └──┬───────┘ │ │ Wrapper │ └───┬───┘ │ └────┬────┘ │ -//! │ │ Ignore └───────────┘ │ │ Augment │ │ Augment -//! └──────────┘ └──────┘ └───────┘ -//! -//! │ │ │ │ -//! └───────────────┘ └─────────────────────────────────────────────┘ -//! -//! Presence of Presence of -//! "checked_with" "is_contract_generated" -//! -//! State is detected via +//! │ Annotate original + generate closures +//! │ +//! ▼ +//! ┌──────────┐ +//! │ Original │◄─┐ +//! └──┬───────┘ │ +//! │ │ Expand +//! └──────────┘ closures //! ``` //! -//! All named arguments of the annotated function are unsafely shallow-copied -//! with the `kani::internal::untracked_deref` function to circumvent the borrow checker -//! for postconditions. The case where this is relevant is if you want to return -//! a mutable borrow from the function which means any immutable borrow in the -//! postcondition would be illegal. We must ensure that those copies are not -//! dropped (causing a double-free) so after the postconditions we call -//! `mem::forget` on each copy. +//! ## Check closure //! -//! ## Check function -//! -//! Generates a `_check_` function that assumes preconditions -//! and asserts postconditions. The check function is also marked as generated +//! Generates a `__kani__check` closure that assumes preconditions +//! and asserts postconditions. The check closure is also marked as generated //! with the `#[kanitool::is_contract_generated(check)]` attribute. //! //! Decorates the original function with `#[kanitool::checked_by = -//! "_check_"]`. +//! "__kani_check_"]`. //! //! The check function is a copy of the original function with preconditions //! added before the body and postconditions after as well as injected before @@ -111,16 +90,16 @@ //! //! ## Replace Function //! -//! As the mirror to that also generates a `_replace_` -//! function that asserts preconditions and assumes postconditions. The replace +//! As the mirror to that also generates a `__kani_replace_` +//! closure that asserts preconditions and assumes postconditions. The replace //! function is also marked as generated with the //! `#[kanitool::is_contract_generated(replace)]` attribute. //! //! Decorates the original function with `#[kanitool::replaced_by = -//! "_replace_"]`. +//! "__kani_replace_"]`. //! -//! The replace function has the same signature as the original function but its -//! body is replaced by `kani::any()`, which generates a non-deterministic +//! The replace closure has the same signature as the original function but its +//! body is replaced by `kani::any_modifies()`, which generates a non-deterministic //! value. //! //! ## Inductive Verification @@ -148,11 +127,11 @@ //! flip the tracker variable back to `false` in case the function is called //! more than once in its harness. //! -//! To facilitate all this we generate a `_recursion_wrapper_` +//! To facilitate all this we generate a `__kani_recursion_check_` //! function with the following shape: //! //! ```ignored -//! fn recursion_wrapper_...(fn args ...) { +//! let __kani_recursion_check_func = |(args ...)| { //! static mut REENTRY: bool = false; //! //! if unsafe { REENTRY } { @@ -163,11 +142,11 @@ //! unsafe { reentry = false }; //! result_kani_internal //! } -//! } +//! }; //! ``` //! -//! We register this function as `#[kanitool::checked_with = -//! "recursion_wrapper_..."]` instead of the check function. +//! We register this closure as `#[kanitool::checked_with = "__kani_recursion_..."]` instead of the +//! check function. //! //! # Complete example //! @@ -180,9 +159,9 @@ //! ``` //! //! Turns into -//! +//! TODO: Update this //! ``` -//! #[kanitool::checked_with = "div_recursion_wrapper_965916"] +//! #[kanitool::checked_with = "div_recursion_check_965916"] //! #[kanitool::replaced_with = "div_replace_965916"] //! fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } //! @@ -219,8 +198,8 @@ //! //! #[allow(dead_code)] //! #[allow(unused_variables)] -//! #[kanitool::is_contract_generated(recursion_wrapper)] -//! fn div_recursion_wrapper_965916(dividend: u32, divisor: u32) -> u32 { +//! #[kanitool::is_contract_generated(recursion_check)] +//! fn div_recursion_check_965916(dividend: u32, divisor: u32) -> u32 { //! static mut REENTRY: bool = false; //! //! if unsafe { REENTRY } { @@ -262,15 +241,16 @@ //! ``` //! //! This expands to +//! TODO: Update this //! //! ``` -//! #[kanitool::checked_with = "modify_recursion_wrapper_633496"] +//! #[kanitool::checked_with = "modify_recursion_check_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) { +//! #[kanitool::is_contract_generated(recursion_check)] +//! fn modify_recursion_check_633496(arg0: &mut u32) { //! static mut REENTRY: bool = false; //! if unsafe { REENTRY } { //! modify_replace_633496(arg0) @@ -403,18 +383,11 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { /// Classifies the state a function is in in the contract handling pipeline. #[derive(Clone, Copy, PartialEq, Eq)] enum ContractFunctionState { - /// This is the original code, re-emitted from a contract attribute. - Original, + /// This is the function already expanded with the closures. + Expanded, /// This is the first time a contract attribute is evaluated on this /// function. Untouched, - /// This is a check function that was generated from a previous evaluation - /// of a contract attribute. - Check, - /// This is a replace function that was generated from a previous evaluation - /// of a contract attribute. - Replace, - ModifiesWrapper, } /// The information needed to generate the bodies of check and replacement @@ -424,12 +397,19 @@ struct ContractConditionsHandler<'a> { /// Information specific to the type of contract attribute we're expanding. condition_type: ContractConditionsData, /// Body of the function this attribute was found on. - annotated_fn: &'a mut ItemFn, + annotated_fn: &'a ItemFn, /// An unparsed, unmodified copy of `attr`, used in the error messages. attr_copy: TokenStream2, /// The stream to which we should write the generated code. output: TokenStream2, - hash: Option, + /// The name of the check closure. + check_name: String, + /// The name of the replace closure. + replace_name: String, + /// The name of the recursion closure. + recursion_name: String, + /// The name of the modifies closure. + modify_name: String, } /// Which kind of contract attribute are we dealing with? @@ -463,22 +443,9 @@ impl<'a> ContractConditionsHandler<'a> { /// Handle the contract state and return the generated code fn dispatch_on(mut self, state: ContractFunctionState) -> TokenStream2 { match state { - ContractFunctionState::ModifiesWrapper => self.emit_augmented_modifies_wrapper(), - ContractFunctionState::Check => { - // The easy cases first: If we are on a check or replace function - // emit them again but with additional conditions layered on. - // - // Since we are already on the check function, it will have an - // appropriate, unique generated name which we are just going to - // pass on. - self.emit_check_function(None); - } - ContractFunctionState::Replace => { - // Analogous to above - self.emit_replace_function(None); - } - ContractFunctionState::Original => { - unreachable!("Impossible: This is handled via short circuiting earlier.") + ContractFunctionState::Expanded => { + // We are on the already expanded function. + todo!("Expand closures") } ContractFunctionState::Untouched => self.handle_untouched(), } @@ -501,29 +468,12 @@ fn contract_main( let mut item_fn = parse_macro_input!(item as ItemFn); let function_state = ContractFunctionState::from_attributes(&item_fn.attrs); - - if matches!(function_state, ContractFunctionState::Original) { - // If we're the original function that means we're *not* the first time - // that a contract attribute is handled on this function. This means - // there must exist a generated check function somewhere onto which the - // attributes have been copied and where they will be expanded into more - // checks. So we just return ourselves unchanged. - // - // Since this is the only function state case that doesn't need a - // handler to be constructed, we do this match early, separately. - return item_fn.into_token_stream().into(); - } - - let hash = matches!(function_state, ContractFunctionState::Untouched) - .then(|| helpers::short_hash_of_token_stream(&item_stream_clone)); - let handler = match ContractConditionsHandler::new( function_state, is_requires, attr, &mut item_fn, attr_copy, - hash, ) { Ok(handler) => handler, Err(e) => return e.into_compile_error().into(), diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 7a522ea98e08..d5dcd1e3a6db 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -3,7 +3,7 @@ //! Logic used for generating the code that replaces a function with its contract. -use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; +use proc_macro2::{Ident, Span, TokenStream}; use quote::quote; use super::{ @@ -65,7 +65,7 @@ impl<'a> ContractConditionsHandler<'a> { /// /// `use_nondet_result` will only be true if this is the first time we are /// generating a replace function. - fn make_replace_body(&self) -> TokenStream2 { + fn make_replace_body(&self) -> TokenStream { let (before, after) = self.ensure_bootstrapped_replace_body(); match &self.condition_type { @@ -106,28 +106,20 @@ impl<'a> ContractConditionsHandler<'a> { /// /// See [`Self::make_replace_body`] for the most interesting parts of this /// function. - pub fn emit_replace_function(&mut self, override_function_ident: Option) { - self.emit_common_header(); - - if self.function_state.emit_tag_attr() { - // If it's the first time we also emit this marker. Again, order is - // important so this happens as the last emitted attribute. - self.output.extend(quote!(#[kanitool::is_contract_generated(replace)])); - } - let mut sig = self.annotated_fn.sig.clone(); - // We use non-constant functions, thus, the wrapper cannot be constant. - sig.constness = None; + pub fn replace_closure(&self) -> TokenStream { + let replace_ident = Ident::new(&self.replace_name, Span::call_site()); + let sig = &self.annotated_fn.sig; + let (inputs, _args) = closure_args(&sig.inputs); + let output = &sig.output; let body = self.make_replace_body(); - if let Some(ident) = override_function_ident { - sig.ident = ident; - } - // Finally emit the check function itself. - self.output.extend(quote!( - #sig { + quote!( + #[kanitool::is_contract_generated(replace)] + #[allow(dead_code, unused_variables, unused_mut)] + let mut #replace_ident = |#inputs| #output { #body - } - )); + }; + ) } } diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index 1ab791d9a117..4963bbbf4387 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -9,7 +9,7 @@ use std::collections::HashMap; -use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; +use proc_macro2::{Ident, Span, TokenStream as TokenStream2, TokenStream}; use quote::{quote, ToTokens}; use std::hash::{DefaultHasher, Hash, Hasher}; use syn::{ @@ -30,75 +30,6 @@ impl<'a> ContractConditionsHandler<'a> { pub fn is_first_emit(&self) -> bool { matches!(self.function_state, ContractFunctionState::Untouched) } - - /// Create a new name for the assigns wrapper function *or* get the name of - /// the wrapper we must have already generated. This is so that we can - /// recognize a call to that wrapper inside the check function. - pub fn make_wrapper_name(&self) -> Ident { - if let Some(hash) = self.hash { - identifier_for_generated_function(&self.annotated_fn.sig.ident, "wrapper", hash) - } else { - let str_name = self.annotated_fn.sig.ident.to_string(); - let splits = str_name.rsplitn(3, '_').collect::>(); - let [hash, _, base] = splits.as_slice() else { - unreachable!("Odd name for function {str_name}, splits were {}", splits.len()); - }; - - Ident::new(&format!("{base}_wrapper_{hash}"), Span::call_site()) - } - } - - /// Emit attributes common to check or replace function into the output - /// stream. - pub fn emit_common_header(&mut self) { - if self.function_state.emit_tag_attr() { - self.output.extend(quote!( - #[allow(dead_code, unused_variables, unused_mut)] - )); - } - - #[cfg(not(feature = "no_core"))] - self.output.extend(self.annotated_fn.attrs.iter().flat_map(Attribute::to_token_stream)); - - // When verifying core and standard library, we need to add an unstable attribute to - // the functions generated by Kani. - // We also need to filter `rustc_diagnostic_item` attribute. - // We should consider a better strategy than just duplicating all attributes. - #[cfg(feature = "no_core")] - { - self.output.extend(quote!( - #[unstable(feature="kani", issue="none")] - )); - self.output.extend( - self.annotated_fn - .attrs - .iter() - .filter(|attr| { - if let Some(ident) = attr.path().get_ident() { - let name = ident.to_string(); - !name.starts_with("rustc") - && !(name == "stable") - && !(name == "unstable") - } else { - true - } - }) - .flat_map(Attribute::to_token_stream), - ); - } - } -} - -/// Makes consistent names for a generated function which was created for -/// `purpose`, from an attribute that decorates `related_function` with the -/// hash `hash`. -pub fn identifier_for_generated_function( - related_function_name: &Ident, - purpose: &str, - hash: u64, -) -> Ident { - let identifier = format!("{}_{purpose}_{hash:x}", related_function_name); - Ident::new(&identifier, proc_macro2::Span::mixed_site()) } /// Used as the "single source of truth" for [`try_as_result_assign`] and [`try_as_result_assign_mut`] diff --git a/tests/expected/function-contract/trait_impls/methods.rs b/tests/expected/function-contract/trait_impls/methods.rs new file mode 100644 index 000000000000..31cc022a442c --- /dev/null +++ b/tests/expected/function-contract/trait_impls/methods.rs @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. +// kani-flags: -Zfunction-contracts + +//! Check that we can add contract to a trait implementation. +//! Original code taken from: +//! + +use std::ops::Add; + +#[derive(Debug, Copy, Clone, PartialEq, kani::Arbitrary)] +struct Point { + x: i32, + y: i32, +} + +impl Add for Point { + type Output = Self; + + #[kani::requires(!self.x.overflowing_add(other.x).1)] + #[kani::requires(!self.y.overflowing_add(other.y).1)] + #[kani::ensures(|result| result.x == self.x + other.x)] + #[kani::ensures(|result| result.y == self.y + other.y)] + fn add(self, other: Self) -> Self { + Self { x: self.x + other.x, y: self.y + other.y } + } +} + +#[kani::proof_for_contract(add)] +fn check_add() { + let (p1, p2): (Point, Point) = kani::any(); + p1.add(p2); +} From 18e8b0db27bdb48965769348a572c195026a6bd6 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 8 Jul 2024 22:02:17 -0700 Subject: [PATCH 02/18] Implement multiple attributes --- library/kani/src/internal.rs | 2 + .../src/sysroot/contracts/bootstrap.rs | 51 ++++- .../src/sysroot/contracts/check.rs | 109 ++++++--- .../src/sysroot/contracts/helpers.rs | 211 +++--------------- .../src/sysroot/contracts/initialize.rs | 6 +- .../kani_macros/src/sysroot/contracts/mod.rs | 24 +- .../src/sysroot/contracts/replace.rs | 79 ++++--- .../src/sysroot/contracts/shared.rs | 24 +- .../function-contract/trait_impls/methods.rs | 17 +- 9 files changed, 211 insertions(+), 312 deletions(-) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 509f2cf51962..b589e03f809f 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -70,6 +70,8 @@ impl<'a, T> Pointer<'a> for *mut T { /// A way to break the ownerhip rules. Only used by contracts where we can /// guarantee it is done safely. +/// TODO: Remove this! This is not safe. Users should be able to use `ptr::read` and `old` if +/// they really need to. #[inline(never)] #[doc(hidden)] #[rustc_diagnostic_item = "KaniUntrackedDeref"] diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index a1282d61b3ef..4d0e57622ef8 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -6,25 +6,21 @@ use proc_macro2::{Ident, Span, TokenStream}; use quote::quote; -use syn::{ExprClosure, FnArg, ItemFn, Signature}; +use syn::{Expr, ItemFn, Stmt}; use super::{helpers::*, ContractConditionsHandler, INTERNAL_RESULT_IDENT}; impl<'a> ContractConditionsHandler<'a> { /// Generate initial contract. /// - /// 1. Generating the body for all the closures used by contracts. - /// - The recursion closure body is always the same, and it is generated in this stage. - /// - The other closures body will depend on which annotation is being processed. - /// 2. Emitting the extended function with the new closures and the new contract attributes + /// 1. Generating the body for the recursion closure used by contracts. + /// - The recursion closure body will contain the check and replace closure. pub fn handle_untouched(&mut self) { let replace_name = &self.replace_name; let modifies_name = &self.modify_name; let recursion_name = &self.recursion_name; - let recursion_closure = self.recursion_closure(); - let replace_closure = self.replace_closure(); - println!("{recursion_closure}"); + let recursion_closure = self.new_recursion_closure(); // The order of `attrs` and `kanitool::{checked_with, // is_contract_generated}` is important here, because macros are @@ -38,7 +34,6 @@ impl<'a> ContractConditionsHandler<'a> { #[kanitool::replaced_with = #replace_name] #[kanitool::inner_check = #modifies_name] #vis #sig { - #replace_closure #recursion_closure // -- Now emit the original code. #block @@ -46,8 +41,21 @@ impl<'a> ContractConditionsHandler<'a> { )); } + /// Handle subsequent contract attributes. + /// + /// Find the closures added by the initial setup, parse them and expand their body according + /// to the attribute being handled. + pub fn handle_expanded(&mut self) { + let mut annotated_fn = self.annotated_fn.clone(); + let ItemFn { block, .. } = &mut annotated_fn; + let recursion_closure = find_contract_closure(&mut block.stmts, "recursion_check"); + + self.expand_recursion(recursion_closure); + self.output.extend(quote!(#annotated_fn)); + } + /// Generate the tokens for the recursion closure. - fn recursion_closure(&self) -> TokenStream { + fn new_recursion_closure(&self) -> TokenStream { let ItemFn { ref sig, .. } = self.annotated_fn; let (inputs, args) = closure_args(&sig.inputs); let output = &sig.output; @@ -70,8 +78,8 @@ impl<'a> ContractConditionsHandler<'a> { #replace_closure #replace_ident(#(#args),*) } else { - #check_closure unsafe { REENTRY = true }; + #check_closure let #result = #check_ident(#(#args),*); unsafe { REENTRY = false }; #result @@ -79,4 +87,25 @@ impl<'a> ContractConditionsHandler<'a> { }; ) } + + /// Expand an existing recursion closure with the new condition. + fn expand_recursion(&self, closure: &mut Stmt) { + // TODO: Need to enter if / else. Make this traverse body and return list statements :( + let body = closure_body(closure); + let stmts = &mut body.block.stmts; + let if_reentry = stmts + .iter_mut() + .find_map(|stmt| { + if let Stmt::Expr(Expr::If(if_expr), ..) = stmt { Some(if_expr) } else { None } + }) + .unwrap(); + + let replace_closure = find_contract_closure(&mut if_reentry.then_branch.stmts, "replace"); + self.expand_replace(replace_closure); + + let else_branch = if_reentry.else_branch.as_mut().unwrap(); + let Expr::Block(else_block) = else_branch.1.as_mut() else { unreachable!() }; + let check_closure = find_contract_closure(&mut else_block.block.stmts, "check"); + self.expand_check(check_closure); + } } diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 3609ccb96f90..10999912a294 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -5,7 +5,10 @@ use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::quote; -use syn::{parse_quote, Expr, FnArg, ItemFn, Token}; +use std::mem; +use syn::punctuated::Punctuated; +use syn::token::Comma; +use syn::{parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, ReturnType, Stmt}; use super::{ helpers::*, @@ -22,16 +25,15 @@ impl<'a> ContractConditionsHandler<'a> { /// /// Mutable because a `modifies` clause may need to extend the inner call to /// the wrapper with new arguments. - pub fn make_check_body(&self) -> TokenStream2 { - let mut body_stmts = self.get_check_body(); + pub fn make_check_body(&self, mut body_stmts: Vec) -> TokenStream2 { let Self { attr_copy, .. } = self; match &self.condition_type { ContractConditionsData::Requires { attr } => { - quote!( + quote!({ kani::assume(#attr); #(#body_stmts)* - ) + }) } ContractConditionsData::Ensures { attr } => { let (remembers, ensures_clause) = build_ensures(attr); @@ -43,12 +45,12 @@ impl<'a> ContractConditionsHandler<'a> { ); let return_expr = body_stmts.pop(); - quote!( + quote!({ #remembers #(#body_stmts)* #exec_postconditions #return_expr - ) + }) } ContractConditionsData::Modifies { attr } => { let wrapper_name = &self.modify_name; @@ -69,32 +71,31 @@ impl<'a> ContractConditionsHandler<'a> { unreachable!("Expected check function to call to the modifies wrapper function") }; - quote!( + quote!({ // Cast to *const () since we only care about the address. #(let #wrapper_args = #attr as *const _ as *const ();)* #(#body_stmts)* - ) + }) } } } - /// Get the body of the previous check closure. - fn get_check_body(&self) -> Vec { + /// Initialize the list of statements for the check closure body. + fn initial_check_stmts(&self) -> Vec { let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); let return_type = return_type_to_type(&self.annotated_fn.sig.output); - let modifies_closure = self.modifies_closure(); - if self.is_first_emit() { - let (_, args) = closure_args(&self.annotated_fn.sig.inputs); - let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - parse_quote!( - #modifies_closure - let #result : #return_type = #modifies_ident(#(#args),*); - #result - ) - } else { - todo!("Find old body"); - // self.annotated_fn.block.stmts.clone() - } + let modifies_closure = self.modifies_closure( + &self.annotated_fn.sig.inputs, + &self.annotated_fn.sig.output, + &self.annotated_fn.block, + ); + let (_, args) = closure_args(&self.annotated_fn.sig.inputs); + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + parse_quote!( + #modifies_closure + let #result : #return_type = #modifies_ident(#(#args),*); + #result + ) } /// Generate a token stream that represents the check closure. @@ -106,17 +107,25 @@ impl<'a> ContractConditionsHandler<'a> { let sig = &self.annotated_fn.sig; let (inputs, _args) = closure_args(&sig.inputs); let output = &sig.output; - let body = self.make_check_body(); + let body_stmts = self.initial_check_stmts(); + let body = self.make_check_body(body_stmts); quote!( - #[kanitool::is_contract_generated(replace)] + #[kanitool::is_contract_generated(check)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #check_ident = |#inputs| #output { - #body - }; + let mut #check_ident = |#inputs| #output #body; ) } + /// Expand the check body. + /// + /// First find the modifies body and expand that. Then expand the rest of the body. + pub fn expand_check(&self, closure: &mut Stmt) { + let body = closure_body(closure); + self.expand_modifies(find_contract_closure(&mut body.block.stmts, "wrapper")); + *body = syn::parse2(self.make_check_body(mem::take(&mut body.block.stmts))).unwrap(); + } + /// Emit a modifies wrapper, possibly augmenting a prior, existing one. /// /// We only augment if this clause is a `modifies` clause. Before, @@ -126,19 +135,21 @@ impl<'a> ContractConditionsHandler<'a> { /// implement `kani::Arbitrary` for checking. Now, we annotate each /// argument with a generic type parameter, so the compiler can /// continue inferring the correct types. - pub fn modifies_closure(&self) -> TokenStream2 { - // TODO: Get existing signature. - let sig = &self.annotated_fn.sig; + pub fn modifies_closure( + &self, + inputs: &Punctuated, + output: &ReturnType, + body: &Block, + ) -> TokenStream2 { + // Filter receiver + let (inputs, _args) = closure_args(inputs); let wrapper_args: Vec<_> = if let ContractConditionsData::Modifies { attr } = &self.condition_type { - make_wrapper_idents(sig.inputs.len(), attr.len(), WRAPPER_ARG_PREFIX).collect() + make_wrapper_idents(inputs.len(), attr.len(), WRAPPER_ARG_PREFIX).collect() } else { - make_wrapper_idents(sig.inputs.len(), 0, WRAPPER_ARG_PREFIX).collect() + make_wrapper_idents(inputs.len(), 0, WRAPPER_ARG_PREFIX).collect() }; let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); - let (inputs, _args) = closure_args(&sig.inputs); - let output = &sig.output; - let body = &self.annotated_fn.block; quote!( #[kanitool::is_contract_generated(wrapper)] #(#[kanitool::modifies(#wrapper_args)])* @@ -148,6 +159,30 @@ impl<'a> ContractConditionsHandler<'a> { }; ) } + + /// Expand the modifies closure if we are handling a modifies attribute. Otherwise, no-op. + pub fn expand_modifies(&self, closure_stmt: &mut Stmt) { + if matches!(&self.condition_type, ContractConditionsData::Modifies { .. }) { + let Stmt::Local(Local { init: Some(LocalInit { expr, .. }), .. }) = closure_stmt else { + unreachable!() + }; + let Expr::Closure(closure) = expr.as_ref() else { unreachable!() }; + let Expr::Block(body) = closure.body.as_ref() else { unreachable!() }; + let inputs = closure + .inputs + .iter() + .map(|pat| { + if let Pat::Type(pat_type) = pat { + FnArg::Typed(pat_type.clone()) + } else { + panic!("Expected closure argument, but found: {pat:?}") + } + }) + .collect(); + let stream = self.modifies_closure(&inputs, &closure.output, &body.block); + *closure_stmt = syn::parse2(stream).unwrap(); + } + } } /// Try to interpret this statement as `let result : <...> = (args ...);` and diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index 2b8c9dc7ad53..e79e440594e4 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -5,11 +5,10 @@ //! specific to Kani and contracts. use proc_macro2::{Ident, Span}; -use quote::{quote, ToTokens}; use std::borrow::Cow; use syn::punctuated::Punctuated; use syn::token::Comma; -use syn::{spanned::Spanned, visit::Visit, Expr, FnArg, ItemFn, Pat}; +use syn::{parse_quote, Attribute, Expr, ExprBlock, FnArg, Local, LocalInit, Pat, Stmt}; /// If an explicit return type was provided it is returned, otherwise `()`. pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { @@ -22,161 +21,6 @@ pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { } } -/// Create an expression that reconstructs a struct that was matched in a pattern. -/// -/// Does not support enums, wildcards, pattern alternatives (`|`), range patterns, or verbatim. -pub fn pat_to_expr(pat: &syn::Pat) -> Expr { - use syn::Pat; - let mk_err = |typ| { - pat.span() - .unwrap() - .error(format!("`{typ}` patterns are not supported for functions with contracts")) - .emit(); - unreachable!() - }; - match pat { - Pat::Const(c) => Expr::Const(c.clone()), - Pat::Ident(id) => Expr::Verbatim(id.ident.to_token_stream()), - Pat::Lit(lit) => Expr::Lit(lit.clone()), - Pat::Reference(rf) => Expr::Reference(syn::ExprReference { - attrs: vec![], - and_token: rf.and_token, - mutability: rf.mutability, - expr: Box::new(pat_to_expr(&rf.pat)), - }), - Pat::Tuple(tup) => Expr::Tuple(syn::ExprTuple { - attrs: vec![], - paren_token: tup.paren_token, - elems: tup.elems.iter().map(pat_to_expr).collect(), - }), - Pat::Slice(slice) => Expr::Reference(syn::ExprReference { - attrs: vec![], - and_token: syn::Token!(&)(Span::call_site()), - mutability: None, - expr: Box::new(Expr::Array(syn::ExprArray { - attrs: vec![], - bracket_token: slice.bracket_token, - elems: slice.elems.iter().map(pat_to_expr).collect(), - })), - }), - Pat::Path(pth) => Expr::Path(pth.clone()), - Pat::Or(_) => mk_err("or"), - Pat::Rest(_) => mk_err("rest"), - Pat::Wild(_) => mk_err("wildcard"), - Pat::Paren(inner) => pat_to_expr(&inner.pat), - Pat::Range(_) => mk_err("range"), - Pat::Struct(strct) => { - if strct.rest.is_some() { - mk_err(".."); - } - Expr::Struct(syn::ExprStruct { - attrs: vec![], - path: strct.path.clone(), - brace_token: strct.brace_token, - dot2_token: None, - rest: None, - qself: strct.qself.clone(), - fields: strct - .fields - .iter() - .map(|field_pat| syn::FieldValue { - attrs: vec![], - member: field_pat.member.clone(), - colon_token: field_pat.colon_token, - expr: pat_to_expr(&field_pat.pat), - }) - .collect(), - }) - } - Pat::Verbatim(_) => mk_err("verbatim"), - Pat::Type(pt) => pat_to_expr(pt.pat.as_ref()), - Pat::TupleStruct(_) => mk_err("tuple struct"), - _ => mk_err("unknown"), - } -} - -/// For each argument create an expression that passes this argument along unmodified. -/// -/// Reconstructs structs that may have been deconstructed with patterns. -pub fn exprs_for_args( - args: &syn::punctuated::Punctuated, -) -> impl Iterator + Clone + '_ { - args.iter().map(|arg| match arg { - FnArg::Receiver(_) => Expr::Verbatim(quote!(self)), - FnArg::Typed(typed) => pat_to_expr(&typed.pat), - }) -} - -/// The visitor used by [`is_probably_impl_fn`]. See function documentation for -/// more information. -struct SelfDetector(bool); - -impl<'ast> Visit<'ast> for SelfDetector { - fn visit_ident(&mut self, i: &'ast syn::Ident) { - self.0 |= i == &Ident::from(syn::Token![Self](Span::mixed_site())) - } - - fn visit_receiver(&mut self, _node: &'ast syn::Receiver) { - self.0 = true; - } -} - -/// Try to determine if this function is part of an `impl`. -/// -/// Detects *methods* by the presence of a receiver argument. Heuristically -/// detects *associated functions* by the use of `Self` anywhere. -/// -/// Why do we need this? It's because if we want to call this `fn`, or any other -/// `fn` we generate into the same context we need to use `foo()` or -/// `Self::foo()` respectively depending on whether this is a plain or -/// associated function or Rust will complain. For the contract machinery we -/// need to generate and then call various functions we generate as well as the -/// original contracted function and so we need to determine how to call them -/// correctly. -/// -/// We can only solve this heuristically. The fundamental problem with Rust -/// macros is that they only see the syntax that's given to them and no other -/// context. It is however that context (of an `impl` block) that definitively -/// determines whether the `fn` is a plain function or an associated function. -/// -/// The heuristic itself is flawed, but it's the best we can do. For instance -/// this is perfectly legal -/// -/// ``` -/// struct S; -/// impl S { -/// #[i_want_to_call_you] -/// fn helper(u: usize) -> bool { -/// u < 8 -/// } -/// } -/// ``` -/// -/// This function would have to be called `S::helper()` but to the -/// `#[i_want_to_call_you]` attribute this function looks just like a bare -/// function because it never mentions `self` or `Self`. While this is a rare -/// case, the following is much more likely and suffers from the same problem, -/// because we can't know that `Vec == Self`. -/// -/// ``` -/// impl Vec { -/// fn new() -> Vec { -/// Vec { cap: 0, buf: NonNull::dangling() } -/// } -/// } -/// ``` -/// -/// **Side note:** You may be tempted to suggest that we could try and parse -/// `syn::ImplItemFn` and distinguish that from `syn::ItemFn` to distinguish -/// associated function from plain functions. However parsing in an attribute -/// placed on *any* `fn` will always succeed for *both* `syn::ImplItemFn` and -/// `syn::ItemFn`, thus not letting us distinguish between the two. -pub fn is_probably_impl_fn(fun: &ItemFn) -> bool { - let mut self_detector = SelfDetector(false); - self_detector.visit_item_fn(fun); - self_detector.0 -} - /// Extract the closure arguments which should skip `self`. /// /// Return the declaration form as well as just a plain list of idents for each. @@ -193,6 +37,30 @@ pub fn closure_args( .collect() } +/// Find a closure statement attached with `kanitool::is_contract_generated` attribute. +pub fn find_contract_closure<'a>(stmts: &'a mut [Stmt], name: &'static str) -> &'a mut Stmt { + let contract = stmts.iter_mut().find(|stmt| { + if let Stmt::Local(local) = stmt { + let ident = Ident::new(name, Span::call_site()); + let attr: Attribute = parse_quote!(#[kanitool::is_contract_generated(#ident)]); + local.attrs.contains(&attr) + } else { + false + } + }); + contract.expect(&format!("Internal Failure: Expected to find closure `{name}`, but found none")) +} + +/// Extract the body of a closure declaration. +pub fn closure_body(closure: &mut Stmt) -> &mut ExprBlock { + let Stmt::Local(Local { init: Some(LocalInit { expr, .. }), .. }) = closure else { + unreachable!() + }; + let Expr::Closure(closure) = expr.as_mut() else { unreachable!() }; + let Expr::Block(body) = closure.body.as_mut() else { unreachable!() }; + body +} + /// Does the provided path have the same chain of identifiers as `mtch` (match) /// and no arguments anywhere? /// @@ -237,35 +105,6 @@ pub fn chunks_by<'a, T, C: Default + Extend>( }) } -/// Create a unique hash for a token stream (basically a [`std::hash::Hash`] -/// impl for `proc_macro2::TokenStream`). -fn hash_of_token_stream(hasher: &mut H, stream: proc_macro2::TokenStream) { - use proc_macro2::TokenTree; - use std::hash::Hash; - for token in stream { - match token { - TokenTree::Ident(i) => i.hash(hasher), - TokenTree::Punct(p) => p.as_char().hash(hasher), - TokenTree::Group(g) => { - std::mem::discriminant(&g.delimiter()).hash(hasher); - hash_of_token_stream(hasher, g.stream()); - } - TokenTree::Literal(lit) => lit.to_string().hash(hasher), - } - } -} - -/// Hash this `TokenStream` and return an integer that is at most digits -/// long when hex formatted. -pub fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 { - const SIX_HEX_DIGITS_MASK: u64 = 0x1_000_000; - use std::hash::Hasher; - let mut hasher = std::collections::hash_map::DefaultHasher::default(); - hash_of_token_stream(&mut hasher, proc_macro2::TokenStream::from(stream.clone())); - 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 { diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index fc802ceb1369..50c63173b601 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/library/kani_macros/src/sysroot/contracts/initialize.rs @@ -4,8 +4,8 @@ //! Initialization routine for the contract handler use proc_macro::{Diagnostic, TokenStream}; -use proc_macro2::{Ident, TokenStream as TokenStream2}; -use syn::{spanned::Spanned, ItemFn}; +use proc_macro2::TokenStream as TokenStream2; +use syn::ItemFn; use super::{ helpers::{chunks_by, is_token_stream_2_comma, matches_path}, @@ -51,7 +51,6 @@ impl<'a> ContractConditionsHandler<'a> { /// Initialize the handler. Constructs the required /// [`ContractConditionsType`] depending on `is_requires`. pub fn new( - function_state: ContractFunctionState, is_requires: ContractConditionsType, attr: TokenStream, annotated_fn: &'a mut ItemFn, @@ -78,7 +77,6 @@ impl<'a> ContractConditionsHandler<'a> { let modifies_name = generate_name("modifies"); Ok(Self { - function_state, condition_type, annotated_fn, attr_copy, diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 5ec76370b1cf..ad2246375e13 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -33,7 +33,7 @@ //! //! To this end we use a state machine. The initial state is an "untouched" //! function with possibly multiple contract attributes, none of which have been -//! expanded. When we expand the first (outermost) `requires` or `ensures` +//! expanded. When we expand the first (outermost) contract //! attribute on such a function we re-emit the function with a few closures defined //! in their body, which correspond to the "check" and "replace" that enforce the condition //! carried by the attribute currently being expanded. @@ -315,7 +315,7 @@ use proc_macro::TokenStream; use proc_macro2::{Ident, TokenStream as TokenStream2}; -use quote::{quote, ToTokens}; +use quote::quote; use syn::{parse_macro_input, Expr, ExprClosure, ItemFn}; mod bootstrap; @@ -380,7 +380,7 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { .into() } -/// Classifies the state a function is in in the contract handling pipeline. +/// Classifies the state a function is in the contract handling pipeline. #[derive(Clone, Copy, PartialEq, Eq)] enum ContractFunctionState { /// This is the function already expanded with the closures. @@ -393,7 +393,6 @@ enum ContractFunctionState { /// The information needed to generate the bodies of check and replacement /// functions that integrate the conditions from this contract attribute. struct ContractConditionsHandler<'a> { - function_state: ContractFunctionState, /// Information specific to the type of contract attribute we're expanding. condition_type: ContractConditionsData, /// Body of the function this attribute was found on. @@ -443,10 +442,8 @@ impl<'a> ContractConditionsHandler<'a> { /// Handle the contract state and return the generated code fn dispatch_on(mut self, state: ContractFunctionState) -> TokenStream2 { match state { - ContractFunctionState::Expanded => { - // We are on the already expanded function. - todo!("Expand closures") - } + // We are on the already expanded function. + ContractFunctionState::Expanded => self.handle_expanded(), ContractFunctionState::Untouched => self.handle_untouched(), } self.output @@ -463,18 +460,9 @@ fn contract_main( is_requires: ContractConditionsType, ) -> TokenStream { let attr_copy = TokenStream2::from(attr.clone()); - - let item_stream_clone = item.clone(); let mut item_fn = parse_macro_input!(item as ItemFn); - let function_state = ContractFunctionState::from_attributes(&item_fn.attrs); - let handler = match ContractConditionsHandler::new( - function_state, - is_requires, - attr, - &mut item_fn, - attr_copy, - ) { + let handler = match ContractConditionsHandler::new(is_requires, attr, &mut item_fn, attr_copy) { Ok(handler) => handler, Err(e) => return e.into_compile_error().into(), }; diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index d5dcd1e3a6db..b05085212a5f 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -5,6 +5,8 @@ use proc_macro2::{Ident, Span, TokenStream}; use quote::quote; +use std::mem; +use syn::Stmt; use super::{ helpers::*, @@ -13,6 +15,13 @@ use super::{ }; impl<'a> ContractConditionsHandler<'a> { + /// Create initial set of replace statements which is the return havoc. + fn initial_replace_stmts(&self) -> Vec { + let return_type = return_type_to_type(&self.annotated_fn.sig.output); + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)] + } + /// Split an existing replace body of the form /// /// ```ignore @@ -35,26 +44,21 @@ impl<'a> ContractConditionsHandler<'a> { /// Such that the first vector contains everything up to and including the single result havoc /// and the second one the rest, excluding the return. /// - /// If this is the first time we're emitting replace we create the return havoc and nothing else. - fn ensure_bootstrapped_replace_body(&self) -> (Vec, Vec) { - if self.is_first_emit() { - let return_type = return_type_to_type(&self.annotated_fn.sig.output); - let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - (vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)], vec![]) - } else { - let stmts = &self.annotated_fn.block.stmts; - let idx = stmts - .iter() - .enumerate() - .find_map(|(i, elem)| is_replace_return_havoc(elem).then_some(i)) - .unwrap_or_else(|| { - panic!("ICE: Could not find result let binding in statement sequence") - }); - // We want the result assign statement to end up as the last statement in the first - // vector, hence the `+1`. - let (before, after) = stmts.split_at(idx + 1); - (before.to_vec(), after.split_last().unwrap().1.to_vec()) - } + fn split_replace(&self, mut stmts: Vec) -> (Vec, Vec) { + // Pop the return result since we always re-add it. + stmts.pop(); + + let idx = stmts + .iter() + .enumerate() + .find_map(|(i, elem)| is_replace_return_havoc(elem).then_some(i)) + .unwrap_or_else(|| { + panic!("ICE: Could not find result let binding in statement sequence") + }); + // We want the result assign statement to end up as the last statement in the first + // vector, hence the `+1`. + let (before, after) = stmts.split_at_mut(idx + 1); + (before.to_vec(), after.to_vec()) } /// Create the body of a stub for this contract. @@ -65,62 +69,67 @@ impl<'a> ContractConditionsHandler<'a> { /// /// `use_nondet_result` will only be true if this is the first time we are /// generating a replace function. - fn make_replace_body(&self) -> TokenStream { - let (before, after) = self.ensure_bootstrapped_replace_body(); - + fn expand_replace_body(&self, before: &[Stmt], after: &[Stmt]) -> TokenStream { match &self.condition_type { ContractConditionsData::Requires { attr } => { let Self { attr_copy, .. } = self; let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - quote!( + quote!({ kani::assert(#attr, stringify!(#attr_copy)); #(#before)* #(#after)* #result - ) + }) } ContractConditionsData::Ensures { attr } => { let (remembers, ensures_clause) = build_ensures(attr); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - quote!( + quote!({ #remembers #(#before)* #(#after)* kani::assume(#ensures_clause); #result - ) + }) } ContractConditionsData::Modifies { attr } => { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - quote!( + quote!({ #(#before)* #(*unsafe { kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(#attr))) } = kani::any_modifies();)* #(#after)* #result - ) + }) } } } - /// Emit the replace funtion into the output stream. + /// Emit the replace function into the output stream. /// - /// See [`Self::make_replace_body`] for the most interesting parts of this + /// See [`Self::expand_replace_body`] for the most interesting parts of this /// function. pub fn replace_closure(&self) -> TokenStream { let replace_ident = Ident::new(&self.replace_name, Span::call_site()); let sig = &self.annotated_fn.sig; let (inputs, _args) = closure_args(&sig.inputs); let output = &sig.output; - let body = self.make_replace_body(); + let before = self.initial_replace_stmts(); + let body = self.expand_replace_body(&before, &vec![]); quote!( #[kanitool::is_contract_generated(replace)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #replace_ident = |#inputs| #output { - #body - }; + let mut #replace_ident = |#inputs| #output #body; ) } + + /// Expand the `replace` body with the new attribute. + pub fn expand_replace(&self, closure: &mut Stmt) { + let body = closure_body(closure); + let (before, after) = self.split_replace(mem::take(&mut body.block.stmts)); + let stream = self.expand_replace_body(&before, &after); + *body = syn::parse2(stream).unwrap(); + } } /// Is this statement `let result_kani_internal : <...> = kani::any_modifies();`. diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index 4963bbbf4387..dce13090cfcc 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -9,28 +9,12 @@ use std::collections::HashMap; -use proc_macro2::{Ident, Span, TokenStream as TokenStream2, TokenStream}; -use quote::{quote, ToTokens}; +use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; +use quote::quote; use std::hash::{DefaultHasher, Hash, Hasher}; -use syn::{ - spanned::Spanned, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, ExprPath, Path, -}; +use syn::{spanned::Spanned, visit_mut::VisitMut, Expr, ExprCall, ExprClosure, ExprPath, Path}; -use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT}; - -impl ContractFunctionState { - /// Do we need to emit the `is_contract_generated` tag attribute on the - /// generated function(s)? - pub fn emit_tag_attr(self) -> bool { - matches!(self, ContractFunctionState::Untouched) - } -} - -impl<'a> ContractConditionsHandler<'a> { - pub fn is_first_emit(&self) -> bool { - matches!(self.function_state, ContractFunctionState::Untouched) - } -} +use super::INTERNAL_RESULT_IDENT; /// 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 diff --git a/tests/expected/function-contract/trait_impls/methods.rs b/tests/expected/function-contract/trait_impls/methods.rs index 31cc022a442c..46204249946c 100644 --- a/tests/expected/function-contract/trait_impls/methods.rs +++ b/tests/expected/function-contract/trait_impls/methods.rs @@ -7,6 +7,11 @@ //! Check that we can add contract to a trait implementation. //! Original code taken from: //! +//! +//! TODO: Add the following tests +//! Multiple annotations and: +//! - mut args +//! - inner functions use std::ops::Add; @@ -28,8 +33,18 @@ impl Add for Point { } } +impl Point { + #[kani::modifies(&mut self.x)] + #[kani::requires(!self.x.overflowing_add(val).1)] + #[kani::ensures(|_| val > 0 || self.x < old(self.x))] + #[kani::ensures(|_| val < 0 || self.x > old(self.x))] + pub fn add_x(&mut self, val: i32) { + self.x += val; + } +} + #[kani::proof_for_contract(add)] fn check_add() { let (p1, p2): (Point, Point) = kani::any(); - p1.add(p2); + let _ = p1.add(p2); } From 63959bfaa8212a0214133b424923d474e6cfcd67 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 10 Jul 2024 14:43:52 -0700 Subject: [PATCH 03/18] Add replace / check closures to the main body This will simplify transformation quite a bit. We should consider only adding the recursion closure if `#[recursion]` tag is added to the function. --- .../src/sysroot/contracts/bootstrap.rs | 28 ++++++++++++++----- 1 file changed, 21 insertions(+), 7 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 4d0e57622ef8..83a2e5d92235 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -19,8 +19,11 @@ impl<'a> ContractConditionsHandler<'a> { let replace_name = &self.replace_name; let modifies_name = &self.modify_name; let recursion_name = &self.recursion_name; + let check_name = &self.check_name; - let recursion_closure = self.new_recursion_closure(); + let replace_closure = self.replace_closure(); + let check_closure = self.check_closure(); + let recursion_closure = self.new_recursion_closure(&replace_closure, &check_closure); // The order of `attrs` and `kanitool::{checked_with, // is_contract_generated}` is important here, because macros are @@ -30,11 +33,15 @@ impl<'a> ContractConditionsHandler<'a> { let ItemFn { attrs, vis, sig, block } = &self.annotated_fn; self.output.extend(quote!( #(#attrs)* - #[kanitool::checked_with = #recursion_name] + #[kanitool::recursion_check = #recursion_name] + #[kanitool::checked_with = #check_name] #[kanitool::replaced_with = #replace_name] #[kanitool::inner_check = #modifies_name] #vis #sig { + // The order doesn't matter since we replicate the logic inside recursion closure. #recursion_closure + #replace_closure + #check_closure // -- Now emit the original code. #block } @@ -49,13 +56,23 @@ impl<'a> ContractConditionsHandler<'a> { let mut annotated_fn = self.annotated_fn.clone(); let ItemFn { block, .. } = &mut annotated_fn; let recursion_closure = find_contract_closure(&mut block.stmts, "recursion_check"); - self.expand_recursion(recursion_closure); + + let replace_closure = find_contract_closure(&mut block.stmts, "replace"); + self.expand_replace(replace_closure); + + let check_closure = find_contract_closure(&mut block.stmts, "check"); + self.expand_check(check_closure); + self.output.extend(quote!(#annotated_fn)); } /// Generate the tokens for the recursion closure. - fn new_recursion_closure(&self) -> TokenStream { + fn new_recursion_closure( + &self, + replace_closure: &TokenStream, + check_closure: &TokenStream, + ) -> TokenStream { let ItemFn { ref sig, .. } = self.annotated_fn; let (inputs, args) = closure_args(&sig.inputs); let output = &sig.output; @@ -65,9 +82,6 @@ impl<'a> ContractConditionsHandler<'a> { let check_ident = Ident::new(&self.check_name, span); let recursion_ident = Ident::new(&self.recursion_name, span); - let replace_closure = self.replace_closure(); - let check_closure = self.check_closure(); - quote!( #[kanitool::is_contract_generated(recursion_check)] #[allow(dead_code, unused_variables, unused_mut)] From 9c98eae2021ffb74959445e5c2741244525c5f3b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 11 Jul 2024 16:08:41 -0700 Subject: [PATCH 04/18] Handle static reentry and end-2-end flow Just over 50% of tests is passing. Better than before. :) - Need to handle `self` --- .../codegen_cprover_gotoc/codegen/contract.rs | 141 ++++++---- .../compiler_interface.rs | 9 +- kani-compiler/src/kani_middle/attributes.rs | 256 +++++++++--------- .../src/kani_middle/transform/body.rs | 21 +- .../src/kani_middle/transform/contracts.rs | 244 ++++++++++++++++- .../kani_middle/transform/kani_intrinsics.rs | 7 +- .../src/kani_middle/transform/mod.rs | 5 +- kani-driver/src/call_goto_instrument.rs | 10 +- kani_metadata/src/harness.rs | 8 +- .../src/sysroot/contracts/bootstrap.rs | 1 + 10 files changed, 486 insertions(+), 216 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index d35015aa040d..8d212de11aa5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -2,13 +2,16 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::attributes::KaniAttributes; +use crate::kani_middle::transform::BodyTransformation; use cbmc::goto_program::FunctionContract; use cbmc::goto_program::{Lambda, Location}; +use cbmc::irep::Symbol; use kani_metadata::AssignsContract; use rustc_hir::def_id::DefId as InternalDefId; use rustc_smir::rustc_internal; use stable_mir::mir::mono::{Instance, MonoItem}; -use stable_mir::mir::Local; +use stable_mir::mir::{Body, Local, VarDebugInfoContents}; +use stable_mir::ty::{ClosureKind, FnDef, RigidTy, TyKind}; use stable_mir::CrateDef; use tracing::debug; @@ -34,73 +37,91 @@ impl<'tcx> GotocCtx<'tcx> { items: &[MonoItem], ) -> AssignsContract { let tcx = self.tcx; - let function_under_contract_attrs = KaniAttributes::for_item(tcx, function_under_contract); - - let recursion_wrapper_id = - function_under_contract_attrs.checked_with_id().unwrap().unwrap(); - let expected_name = format!("{}::REENTRY", tcx.item_name(recursion_wrapper_id)); - let mut recursion_tracker = items.iter().filter_map(|i| match i { - MonoItem::Static(recursion_tracker) - if (*recursion_tracker).name().contains(expected_name.as_str()) => - { - Some(*recursion_tracker) - } - _ => None, - }); - - let recursion_tracker_def = recursion_tracker - .next() - .expect("There should be at least one recursion tracker (REENTRY) in scope"); - assert!( - recursion_tracker.next().is_none(), - "Only one recursion tracker (REENTRY) may be in scope" - ); + let modify_instance = items + .iter() + .find_map(|item| { + // Find the instance under contract + let MonoItem::Fn(instance) = *item else { return None }; + if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract { + tracing::error!(name=?instance.name(), "------ here"); + self.find_modifies_closure(instance) + } else { + None + } + }) + .unwrap(); - let span_of_recursion_wrapper = tcx.def_span(recursion_wrapper_id); - let location_of_recursion_wrapper = self.codegen_span(&span_of_recursion_wrapper); - // The name and location for the recursion tracker should match the exact information added - // to the symbol table, otherwise our contract instrumentation will silently failed. - // This happens because Kani relies on `--nondet-static-exclude` from CBMC to properly - // handle this tracker. CBMC silently fails if there is no match in the symbol table - // that correspond to the argument of this flag. - // More details at https://github.com/model-checking/kani/pull/3045. - let full_recursion_tracker_name = format!( - "{}:{}", - location_of_recursion_wrapper - .filename() - .expect("recursion location wrapper should have a file name"), - // We must use the pretty name of the tracker instead of the mangled name. - // This restrictions comes from `--nondet-static-exclude` in CBMC. - // Mode details at https://github.com/diffblue/cbmc/issues/8225. - recursion_tracker_def.name(), - ); + let recursion_tracker = self.find_recursion_tracker(items); + AssignsContract { + recursion_tracker, + contracted_function_name: modify_instance.mangled_name(), + } + } - let wrapped_fn = function_under_contract_attrs.inner_check().unwrap().unwrap(); - let mut instance_under_contract = items.iter().filter_map(|i| match i { - MonoItem::Fn(instance @ Instance { def, .. }) - if wrapped_fn == rustc_internal::internal(tcx, def.def_id()) => + /// The name and location for the recursion tracker should match the exact information added + /// to the symbol table, otherwise our contract instrumentation will silently failed. + /// This happens because Kani relies on `--nondet-static-exclude` from CBMC to properly + /// handle this tracker. CBMC silently fails if there is no match in the symbol table + /// that correspond to the argument of this flag. + /// More details at https://github.com/model-checking/kani/pull/3045. + /// + /// We must use the pretty name of the tracker instead of the mangled name. + /// This restriction comes from `--nondet-static-exclude` in CBMC. + /// Mode details at https://github.com/diffblue/cbmc/issues/8225. + fn find_recursion_tracker(&mut self, items: &[MonoItem]) -> Option { + // Return item tagged with `#[kanitool::recursion_tracker]` + let mut recursion_trackers = items.iter().filter_map(|item| { + let MonoItem::Static(static_item) = item else { return None }; + if !static_item + .attrs_by_path(&["kanitool".into(), "recursion_tracker".into()]) + .is_empty() { - Some(*instance) + let span = static_item.span(); + let loc = self.codegen_span_stable(span); + Some(format!( + "{}:{}", + loc.filename().expect("recursion location wrapper should have a file name"), + static_item.name(), + )) + } else { + None } - _ => None, }); - let instance_of_check = instance_under_contract.next().unwrap(); + + let recursion_tracker = recursion_trackers.next(); assert!( - instance_under_contract.next().is_none(), - "Only one instance of a checked function may be in scope" + recursion_trackers.next().is_none(), + "Expected up to one recursion tracker (`REENTRY`) in scope" ); - let attrs_of_wrapped_fn = KaniAttributes::for_item(tcx, wrapped_fn); - let assigns_contract = attrs_of_wrapped_fn.modifies_contract().unwrap_or_else(|| { - debug!(?instance_of_check, "had no assigns contract specified"); - vec![] - }); - self.attach_modifies_contract(instance_of_check, assigns_contract); - let wrapper_name = instance_of_check.mangled_name(); + recursion_tracker + } - AssignsContract { - recursion_tracker: full_recursion_tracker_name, - contracted_function_name: wrapper_name, - } + /// Find the modifies closure recursively since it can be inside check or recursion closure. + fn find_modifies_closure(&mut self, instance: Instance) -> Option { + let contract_attrs = + KaniAttributes::for_instance(self.tcx, instance).contract_attributes()?; + let mut find_closure = |inside: Instance, name: &str| { + let body = self.transformer.body(self.tcx, inside); + body.var_debug_info.iter().find_map(|var_info| { + if var_info.name.as_str() == name { + let ty = match &var_info.value { + VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(), + VarDebugInfoContents::Const(const_op) => const_op.ty(), + }; + if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() { + return Some(Instance::resolve(FnDef(def.def_id()), &args).unwrap()); + } + } + None + }) + }; + let outside_check = if contract_attrs.has_recursion { + find_closure(instance, contract_attrs.recursion_check.as_str())? + } else { + instance + }; + let check = find_closure(outside_check, contract_attrs.checked_with.as_str())?; + find_closure(check, contract_attrs.inner_check.as_str()) } /// Convert the Kani level contract into a CBMC level contract by creating a diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index abb69a655472..43f7818fbcc6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -244,7 +244,7 @@ impl CodegenBackend for GotocCodegenBackend { for harness in &unit.harnesses { let model_path = units.harness_model_path(*harness).unwrap(); let contract_metadata = - contract_metadata_for_harness(tcx, harness.def.def_id()).unwrap(); + contract_metadata_for_harness(tcx, harness.def.def_id()); let (gcx, items, contract_info) = self.codegen_items( tcx, &[MonoItem::Fn(*harness)], @@ -428,12 +428,9 @@ impl CodegenBackend for GotocCodegenBackend { } } -fn contract_metadata_for_harness( - tcx: TyCtxt, - def_id: DefId, -) -> Result, ErrorGuaranteed> { +fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option { let attrs = KaniAttributes::for_def_id(tcx, def_id); - Ok(attrs.interpret_the_for_contract_attribute().transpose()?.map(|(_, id, _)| id)) + attrs.interpret_for_contract_attribute().map(|(_, id, _)| id) } fn check_target(session: &Session) { diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 84ec8d627c59..8b087492d511 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -56,6 +56,9 @@ enum KaniAttributeKind { /// name of the function which was generated as the sound stub from the /// contract of this function. ReplacedWith, + /// Attribute on a function with a contract that identifies the code + /// implementing the recursive check for the harness. + RecursionCheck, /// Attribute on a function that was auto-generated from expanding a /// function contract. IsContractGenerated, @@ -74,6 +77,8 @@ enum KaniAttributeKind { /// We use this attribute to properly instantiate `kani::any_modifies` in /// cases when recursion is present given our contracts instrumentation. Recursion, + /// Attribute used to mark the static variable used for tracking recursion check. + RecursionTracker, } impl KaniAttributeKind { @@ -89,7 +94,9 @@ impl KaniAttributeKind { | KaniAttributeKind::Unwind => true, KaniAttributeKind::Unstable | KaniAttributeKind::Recursion + | KaniAttributeKind::RecursionTracker | KaniAttributeKind::ReplacedWith + | KaniAttributeKind::RecursionCheck | KaniAttributeKind::CheckedWith | KaniAttributeKind::Modifies | KaniAttributeKind::InnerCheck @@ -121,6 +128,21 @@ pub struct KaniAttributes<'tcx> { map: BTreeMap>, } +#[derive(Clone, Debug)] +/// Bundle contract attributes for a function annotated with contracts. +pub struct ContractAttributes { + /// Whether the contract was marked with #[recursion] attribute. + pub has_recursion: bool, + /// The name of the contract recursion check. + pub recursion_check: Symbol, + /// The name of the contract check. + pub checked_with: Symbol, + /// The name of the contract replacement. + pub replaced_with: Symbol, + /// The name of the inner check used to modify clauses. + pub inner_check: Symbol, +} + impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { f.debug_struct("KaniAttributes") @@ -178,22 +200,28 @@ impl<'tcx> KaniAttributes<'tcx> { /// returned `Symbol` and `DefId` are respectively the name and id of /// `TARGET`. The `Span` is that of the contents of the attribute and used /// for error reporting. - fn interpret_stub_verified_attribute( - &self, - ) -> Vec> { + /// + /// Any error is emitted and the attribute is filtered out. + pub fn interpret_stub_verified_attribute(&self) -> Vec<(Symbol, DefId, Span)> { self.map .get(&KaniAttributeKind::StubVerified) .map_or([].as_slice(), Vec::as_slice) .iter() - .map(|attr| { - let name = expect_key_string_value(self.tcx.sess, attr)?; - let ok = self.resolve_sibling(name.as_str()).map_err(|e| { - self.tcx.dcx().span_err( - attr.span, - format!("Failed to resolve replacement function {}: {e}", name.as_str()), - ) - })?; - Ok((name, ok, attr.span)) + .filter_map(|attr| { + let name = expect_key_string_value(self.tcx.sess, attr).ok()?; + let def = self + .resolve_from_mod(name.as_str()) + .map_err(|e| { + self.tcx.dcx().span_err( + attr.span, + format!( + "Failed to resolve replacement function {}: {e}", + name.as_str() + ), + ) + }) + .ok()?; + Some((name, def, attr.span)) }) .collect() } @@ -205,33 +233,26 @@ impl<'tcx> KaniAttributes<'tcx> { /// Parse and extract the `proof_for_contract(TARGET)` attribute. The /// returned symbol and DefId are respectively the name and id of `TARGET`, /// the span in the span for the attribute (contents). - pub(crate) fn interpret_the_for_contract_attribute( - &self, - ) -> Option> { - self.expect_maybe_one(KaniAttributeKind::ProofForContract).map(|target| { - let name = expect_key_string_value(self.tcx.sess, target)?; - self.resolve_sibling(name.as_str()).map(|ok| (name, ok, target.span)).map_err( - |resolve_err| { - self.tcx.dcx().span_err( - target.span, - format!( - "Failed to resolve checking function {} because {resolve_err}", - name.as_str() - ), - ) - }, - ) - }) - } - - /// Extract the name of the sibling function this function's contract is - /// checked with (if any). /// - /// `None` indicates this function does not use a contract, `Some(Err(_))` - /// indicates a contract does exist but an error occurred during resolution. - pub fn checked_with(&self) -> Option> { - self.expect_maybe_one(KaniAttributeKind::CheckedWith) - .map(|target| expect_key_string_value(self.tcx.sess, target)) + /// In the case of an error, this function will emit the error and return `None`. + pub(crate) fn interpret_for_contract_attribute(&self) -> Option<(Symbol, DefId, Span)> { + self.expect_maybe_one(KaniAttributeKind::ProofForContract) + .map(|target| { + let name = expect_key_string_value(self.tcx.sess, target).ok()?; + self.resolve_from_mod(name.as_str()) + .map(|ok| (name, ok, target.span)) + .map_err(|resolve_err| { + self.tcx.dcx().span_err( + target.span, + format!( + "Failed to resolve checking function {} because {resolve_err}", + name.as_str() + ), + ) + }) + .ok() + }) + .flatten() } pub fn proof_for_contract(&self) -> Option> { @@ -239,61 +260,47 @@ impl<'tcx> KaniAttributes<'tcx> { .map(|target| expect_key_string_value(self.tcx.sess, target)) } - pub fn inner_check(&self) -> Option> { - self.eval_sibling_attribute(KaniAttributeKind::InnerCheck) - } + /// Extract the name of the local that represents this function's contract is + /// checked with (if any). + /// + /// `None` indicates this function does not use a contract, or an error was found. + /// Note that the error will already be emitted, so we don't return an error. + pub fn contract_attributes(&self) -> Option { + let has_recursion = self.has_recursion(); + let recursion_check = self.attribute_value(KaniAttributeKind::RecursionCheck); + let checked_with = self.attribute_value(KaniAttributeKind::CheckedWith); + let replace_with = self.attribute_value(KaniAttributeKind::ReplacedWith); + let inner_check = self.attribute_value(KaniAttributeKind::InnerCheck); - pub fn replaced_with(&self) -> Option> { - self.expect_maybe_one(KaniAttributeKind::ReplacedWith) - .map(|target| expect_key_string_value(self.tcx.sess, target)) + let total = recursion_check + .iter() + .chain(&checked_with) + .chain(&replace_with) + .chain(&inner_check) + .count(); + if total != 0 && total != 4 { + self.tcx.sess.dcx().err(format!( + "Failed to parse contract instrumentation tags in function `{}`.\ + Expected `4` attributes, but was only able to process `{total}`", + self.tcx.def_path_str(self.item) + )); + } + Some(ContractAttributes { + has_recursion, + recursion_check: recursion_check?, + checked_with: checked_with?, + replaced_with: replace_with?, + inner_check: inner_check?, + }) } /// Retrieves the global, static recursion tracker variable. pub fn checked_with_id(&self) -> Option> { - self.eval_sibling_attribute(KaniAttributeKind::CheckedWith) - } - - /// Find the `mod` that `self.item` is defined in, then search in the items defined in this - /// `mod` for an item that is named after the `name` in the `#[kanitool:: = ""]` - /// annotation on `self.item`. - /// - /// This is similar to [`resolve_fn`] but more efficient since it only looks inside one `mod`. - fn eval_sibling_attribute( - &self, - kind: KaniAttributeKind, - ) -> Option> { - use rustc_hir::{Item, ItemKind, Mod, Node}; - self.expect_maybe_one(kind).map(|target| { - let name = expect_key_string_value(self.tcx.sess, target)?; - let hir_map = self.tcx.hir(); - let hir_id = self.tcx.local_def_id_to_hir_id(self.item.expect_local()); - let find_in_mod = |md: &Mod<'_>| { - md.item_ids - .iter() - .find(|it| hir_map.item(**it).ident.name == name) - .unwrap() - .hir_id() - }; - - let result = match self.tcx.parent_hir_node(hir_id) { - Node::Item(Item { kind, .. }) => match kind { - ItemKind::Mod(m) => find_in_mod(m), - ItemKind::Impl(imp) => { - imp.items.iter().find(|it| it.ident.name == name).unwrap().id.hir_id() - } - other => panic!("Odd parent item kind {other:?}"), - }, - Node::Crate(m) => find_in_mod(m), - other => panic!("Odd parent node type {other:?}"), - } - .expect_owner() - .def_id - .to_def_id(); - Ok(result) - }) + todo!("Delete-me") } - fn resolve_sibling(&self, path_str: &str) -> Result> { + /// Resolve a path starting from this item's module context. + fn resolve_from_mod(&self, path_str: &str) -> Result> { resolve_fn( self.tcx, self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(), @@ -367,9 +374,11 @@ impl<'tcx> KaniAttributes<'tcx> { KaniAttributeKind::StubVerified => { expect_single(self.tcx, kind, &attrs); } - KaniAttributeKind::CheckedWith | KaniAttributeKind::ReplacedWith => { - self.expect_maybe_one(kind) - .map(|attr| expect_key_string_value(&self.tcx.sess, attr)); + KaniAttributeKind::CheckedWith + | KaniAttributeKind::InnerCheck + | KaniAttributeKind::RecursionCheck + | KaniAttributeKind::ReplacedWith => { + self.attribute_value(kind); } KaniAttributeKind::IsContractGenerated => { // Ignored here because this is only used by the proc macros @@ -379,13 +388,25 @@ impl<'tcx> KaniAttributes<'tcx> { KaniAttributeKind::Modifies => { self.modifies_contract(); } - KaniAttributeKind::InnerCheck => { - self.inner_check(); + KaniAttributeKind::RecursionTracker => { + // Nothing to do here. This is used by contract instrumentation. } } } } + /// Get the value of an attribute if one exists. + /// + /// This expects up to one attribute with format `#[kanitool::("")]`. + /// + /// Any format or expectation error is emitted already, and does not need to be handled + /// upstream. + fn attribute_value(&self, kind: KaniAttributeKind) -> Option { + self.expect_maybe_one(kind) + .map(|target| expect_key_string_value(self.tcx.sess, target).ok()) + .flatten() + } + /// Check that any unstable API has been enabled. Otherwise, emit an error. /// /// TODO: Improve error message by printing the span of the harness instead of the definition. @@ -488,6 +509,8 @@ impl<'tcx> KaniAttributes<'tcx> { | KaniAttributeKind::IsContractGenerated | KaniAttributeKind::Modifies | KaniAttributeKind::InnerCheck + | KaniAttributeKind::RecursionCheck + | KaniAttributeKind::RecursionTracker | KaniAttributeKind::ReplacedWith => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref())); } @@ -498,15 +521,11 @@ impl<'tcx> KaniAttributes<'tcx> { fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes) { let dcx = self.tcx.dcx(); - let (name, id, span) = match self.interpret_the_for_contract_attribute() { - None => unreachable!( - "impossible, was asked to handle `proof_for_contract` but didn't find such an attribute." - ), - Some(Err(_)) => return, // This error was already emitted - Some(Ok(values)) => values, + let (name, id, span) = match self.interpret_for_contract_attribute() { + None => return, // This error was already emitted + Some(values) => values, }; - let Some(Ok(replacement_name)) = KaniAttributes::for_item(self.tcx, id).checked_with() - else { + if KaniAttributes::for_item(self.tcx, id).contract_attributes().is_none() { dcx.struct_span_err( span, format!( @@ -517,23 +536,15 @@ impl<'tcx> KaniAttributes<'tcx> { .with_span_note(self.tcx.def_span(id), "Try adding a contract to this function.") .emit(); return; - }; - harness.stubs.push(self.stub_for_relative_item(name, replacement_name)); + } + harness.for_contract = Some(name.to_string()); } fn handle_stub_verified(&self, harness: &mut HarnessAttributes) { let dcx = self.tcx.dcx(); - for contract in self.interpret_stub_verified_attribute() { - let Ok((name, def_id, span)) = contract else { - // This error has already been emitted so we can ignore it now. - // Later the session will fail anyway so we can just - // optimistically forge on and try to find more errors. - continue; - }; - let replacement_name = match KaniAttributes::for_item(self.tcx, def_id).replaced_with() - { - None => { - dcx.struct_span_err( + for (name, def_id, span) in self.interpret_stub_verified_attribute() { + if KaniAttributes::for_item(self.tcx, def_id).contract_attributes().is_none() { + dcx.struct_span_err( span, format!( "Failed to generate verified stub: Function `{}` has no contract.", @@ -548,12 +559,9 @@ impl<'tcx> KaniAttributes<'tcx> { ) ) .emit(); - continue; - } - Some(Ok(replacement_name)) => replacement_name, - Some(Err(_)) => continue, - }; - harness.stubs.push(self.stub_for_relative_item(name, replacement_name)) + return; + } + harness.verified_stubs.push(name.to_string()) } } @@ -579,18 +587,6 @@ impl<'tcx> KaniAttributes<'tcx> { } } - fn stub_for_relative_item(&self, anchor: Symbol, replacement: Symbol) -> Stub { - let local_id = self.item.expect_local(); - let current_module = self.tcx.parent_module_from_def_id(local_id); - let replace_str = replacement.as_str(); - let original_str = anchor.as_str(); - let replacement = original_str - .rsplit_once("::") - .map_or_else(|| replace_str.to_string(), |t| t.0.to_string() + "::" + replace_str); - resolve::resolve_fn(self.tcx, current_module.to_local_def_id(), &replacement).unwrap(); - Stub { original: original_str.to_string(), replacement } - } - /// Parse and interpret the `kanitool::modifies(var1, var2, ...)` annotation into the vector /// `[var1, var2, ...]`. pub fn modifies_contract(&self) -> Option> { diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 22895bd8d20d..181568d3e3f7 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -7,10 +7,14 @@ use crate::kani_middle::find_fn_def; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::mir::*; -use stable_mir::ty::{GenericArgs, MirConst, Span, Ty, UintTy}; +use stable_mir::ty::{GenericArgs, MirConst, Region, RegionKind, Span, Ty, UintTy}; use std::fmt::Debug; use std::mem; +pub const fn re_erased() -> Region { + Region { kind: RegionKind::ReErased } +} + /// This structure mimics a Body that can actually be modified. pub struct MutableBody { blocks: Vec, @@ -54,6 +58,10 @@ impl MutableBody { &self.locals } + pub fn arg_count(&self) -> usize { + self.arg_count + } + /// Create a mutable body from the original MIR body. pub fn from(body: Body) -> Self { MutableBody { @@ -367,10 +375,10 @@ impl MutableBody { /// by the compiler. This function allow us to delete the dummy body before /// creating a new one. /// - /// Note: We do not prune the local variables today for simplicity. - pub fn clear_body(&mut self) { + /// Keep all the locals untouched, so they can be reused by the passes if needed. + pub fn clear_body(&mut self, kind: TerminatorKind) { self.blocks.clear(); - let terminator = Terminator { kind: TerminatorKind::Return, span: self.span }; + let terminator = Terminator { kind, span: self.span }; self.blocks.push(BasicBlock { statements: Vec::default(), terminator }) } } @@ -419,6 +427,11 @@ impl SourceInstruction { } } +/// Create a new operand that moves local. +pub fn new_move_operand(local: Local) -> Operand { + Operand::Move(Place::from(Local::from(local))) +} + fn find_instance(tcx: TyCtxt, diagnostic: &str) -> Option { Instance::resolve(find_fn_def(tcx, diagnostic)?, &GenericArgs(vec![])).ok() } diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index eb5266e0a0eb..525019a4137b 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -3,15 +3,23 @@ //! This module contains code related to the MIR-to-MIR pass to enable contracts. use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; -use crate::kani_middle::transform::body::MutableBody; +use crate::kani_middle::transform::body::{ + new_move_operand, re_erased, CheckType, InsertPosition, MutableBody, SourceInstruction, +}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use cbmc::{InternString, InternedString}; +use rustc_hir::def_id::DefId as InternalDefId; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; -use stable_mir::mir::{Body, ConstOperand, Operand, TerminatorKind}; -use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind}; +use stable_mir::mir::{ + AggregateKind, Body, BorrowKind, ConstOperand, Local, Mutability, Operand, Place, Rvalue, + TerminatorKind, VarDebugInfo, VarDebugInfoContents, +}; +use stable_mir::ty::{ + ClosureDef, ClosureKind, FnDef, GenericArgs, MirConst, Region, RigidTy, Ty, TyKind, +}; use stable_mir::{CrateDef, DefId}; use std::collections::HashSet; use std::fmt::Debug; @@ -41,7 +49,7 @@ impl TransformPass for AnyModifiesPass { where Self: Sized, { - // TODO: Check if this is the harness has proof_for_contract + // TODO: Check if the harness has proof_for_contract query_db.args().unstable_features.contains(&"function-contracts".to_string()) && self.kani_any.is_some() } @@ -161,8 +169,232 @@ impl AnyModifiesPass { (true, body) } else { let mut new_body = MutableBody::from(body); - new_body.clear_body(); - (false, new_body.into()) + new_body.clear_body(TerminatorKind::Unreachable); + (true, new_body.into()) } } } + +/// This pass will transform functions annotated with contracts based on the harness configuration. +/// +/// For functions that are being checked, change the body to invoke the "check" closure. +/// For functions that are being stubbed, change the body to invoke the "replace" closure. +/// +/// Functions with contract contains +#[derive(Debug)] +pub struct FunctionWithContractPass { + /// Function that is being checked, if any. + check_fn: Option, + /// Functions that should be stubbed by their contract. + replace_fns: HashSet, + /// Functions annotated with contract attributes will contain contract closures even if they + /// are not to be used in this harness. + /// In order to avoid bringing unnecessary logic, we clear their body. + unused_closures: HashSet, +} + +impl TransformPass for FunctionWithContractPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Stubbing + } + + fn is_enabled(&self, _query_db: &QueryDb) -> bool + where + Self: Sized, + { + true + } + + /// Transform the function body by replacing it with the stub body. + fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + trace!(function=?instance.name(), "FunctionWithContractPass::transform"); + let _ = + tracing::error_span!("FunctionWithContractPass::transform {}", name = instance.name()) + .entered(); + match instance.ty().kind().rigid().unwrap() { + RigidTy::FnDef(def, _args) => { + if let Some(target_closure) = self.select_closure(tcx, *def, &body) { + tracing::error!(?target_closure, "FunctionWithContractPass::transform"); + (true, self.replace_by_closure(body, target_closure)) + } else { + // Not a contract annotated function + (false, body) + } + } + RigidTy::Closure(def, _args) => { + if self.unused_closures.contains(def) { + tracing::error!("FunctionWithContractPass::transform delete"); + // Delete body and mark it as unreachable. + let mut new_body = MutableBody::from(body); + new_body.clear_body(TerminatorKind::Unreachable); + (true, new_body.into()) + } else { + // Not a contract annotated function + (false, body) + } + } + other => unreachable!("Unexpected instance type: `{other:?}`"), + } + } +} + +impl FunctionWithContractPass { + /// Build the pass by collecting which functions we are stubbing and which ones we are + /// verifying. + pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> FunctionWithContractPass { + let harness = unit.harnesses.first().unwrap(); + let attrs = KaniAttributes::for_instance(tcx, *harness); + let check_fn = attrs.interpret_for_contract_attribute().map(|(_, def_id, span)| def_id); + let replace_fns: HashSet<_> = attrs + .interpret_stub_verified_attribute() + .iter() + .map(|(_, def_id, span)| *def_id) + .collect(); + FunctionWithContractPass { check_fn, replace_fns, unused_closures: Default::default() } + } + + /// Create the following body: + /// + /// fn original([self], args*) { + /// bb0: { + // _3 = {closure@span} { self: _1 }; # If receiver. Otherwise, skip. + // _4 = &_3; # Closure reference is the first argument of the closure. + // _5 = (args*); # Closure arguments tupled is the second argument. + // _0 = <{closure@span} as Fn<(u32,)>>::call(move _4, move _5) -> [return: bb1]; + // } + // + // bb1: { + // return; + // } + /// } + fn replace_by_closure(&self, body: Body, closure: ClosureInfo) -> Body { + tracing::error!(?closure, "replace_by_closure"); + let mut new_body = MutableBody::from(body); + new_body.clear_body(TerminatorKind::Return); + let mut source = SourceInstruction::Terminator { bb: 0 }; + + // 1- Create the closure structure if needed, i.e., if it captures the receiver. + let closure_ty = closure.ty; + let captures = !closure_ty.layout().unwrap().shape().is_1zst(); + let closure_local = if captures { + // This closure captures the receiver. + let capture = Rvalue::Aggregate( + AggregateKind::Closure(closure.def, closure.args.clone()), + vec![new_move_operand(Local::from(1usize))], + ); + assert_eq!(capture.ty(new_body.locals()), Ok(closure_ty), "Expected to capture `self`"); + + new_body.new_assignment(capture, &mut source, InsertPosition::Before) + } else { + new_body.new_local(closure_ty, source.span(new_body.blocks()), Mutability::Not) + }; + + // 2- Take the structure address. + let capture_addr = new_body.new_assignment( + Rvalue::Ref(re_erased(), BorrowKind::Shared, Place::from(closure_local)), + &mut source, + InsertPosition::Before, + ); + + // 3- Create tuple with arguments. + let arg_start = if captures { 2 } else { 1 }; + let arg_locals: Vec<_> = + (arg_start..=new_body.arg_count()).map(|l| new_move_operand(l)).collect(); + let tupled_args = new_body.new_assignment( + Rvalue::Aggregate(AggregateKind::Tuple, arg_locals), + &mut source, + InsertPosition::Before, + ); + + // 4- Call closure and store result into `_0` + let closure_args = vec![new_move_operand(capture_addr), new_move_operand(tupled_args)]; + let closure_instance = + Instance::resolve_closure(closure.def, &closure.args, ClosureKind::FnOnce).unwrap(); + tracing::error!(mangled=?closure_instance.mangled_name(), "replace_by_closure"); + new_body.add_call( + &closure_instance, + &mut source, + InsertPosition::Before, + closure_args, + Place::from(Local::from(0usize)), + ); + + new_body.into() + } + + /// Select which contract closure to keep, if any, and mark the rest as unused. + fn select_closure(&mut self, tcx: TyCtxt, fn_def: FnDef, body: &Body) -> Option { + let kani_attributes = KaniAttributes::for_def_id(tcx, fn_def.def_id()); + if let Some(contract) = kani_attributes.contract_attributes() { + let recursion_closure = + find_closure(tcx, fn_def, &body, contract.recursion_check.as_str()); + let check_closure = find_closure(tcx, fn_def, &body, contract.checked_with.as_str()); + let replace_closure = find_closure(tcx, fn_def, &body, contract.replaced_with.as_str()); + let fn_def_id = rustc_internal::internal(tcx, fn_def.def_id()); + if self.check_fn == Some(fn_def_id) { + // Delete replace closure and one check closure depending on the type. + self.unused_closures.insert(replace_closure.def); + if contract.has_recursion { + self.unused_closures.insert(check_closure.def); + Some(recursion_closure) + } else { + self.unused_closures.insert(recursion_closure.def); + Some(check_closure) + } + } else if self.replace_fns.contains(&fn_def_id) { + // Delete the check closures. + self.unused_closures.insert(recursion_closure.def); + self.unused_closures.insert(check_closure.def); + Some(replace_closure) + } else { + // No contract instrumentation needed. Add all closures to the list of unused. + self.unused_closures.insert(recursion_closure.def); + self.unused_closures.insert(check_closure.def); + self.unused_closures.insert(replace_closure.def); + None + } + } else { + // Nothing to do + None + } + } +} + +#[derive(Clone, Debug)] +struct ClosureInfo { + ty: Ty, + def: ClosureDef, + args: GenericArgs, +} + +fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureInfo { + body.var_debug_info + .iter() + .find_map(|var_info| { + tracing::error!(name=?var_info.name, target=?var_info, + "find_closure"); + if var_info.name.as_str() == name { + let ty = match &var_info.value { + VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(), + VarDebugInfoContents::Const(const_op) => const_op.ty(), + }; + tracing::error!(name=?var_info.name, ty=?ty, + "find_closure"); + if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() { + return Some(ClosureInfo { ty, def, args }); + } + } + None + }) + .unwrap_or_else(|| { + tcx.sess.dcx().err(format!( + "Failed to find contract closure `{name}` in function `{}`", + fn_def.name() + )); + tcx.sess.dcx().abort_if_errors(); + unreachable!() + }) +} diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index ea7bf8625228..ba77b3a43ec3 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -19,7 +19,8 @@ use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ - BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL, + BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, TerminatorKind, + RETURN_LOCAL, }; use stable_mir::target::MachineInfo; use stable_mir::ty::{FnDef, MirConst, RigidTy, Ty, TyKind, UintTy}; @@ -86,7 +87,7 @@ impl IntrinsicGeneratorPass { /// ``` fn valid_value_body(&self, tcx: TyCtxt, body: Body) -> Body { let mut new_body = MutableBody::from(body); - new_body.clear_body(); + new_body.clear_body(TerminatorKind::Return); // Initialize return variable with True. let ret_var = RETURN_LOCAL; @@ -163,7 +164,7 @@ impl IntrinsicGeneratorPass { /// ``` fn is_initialized_body(&mut self, tcx: TyCtxt, body: Body) -> Body { let mut new_body = MutableBody::from(body); - new_body.clear_body(); + new_body.clear_body(TerminatorKind::Return); // Initialize return variable with True. let ret_var = RETURN_LOCAL; diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 56ab0be493c4..7cc8e9f2ee06 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -20,7 +20,7 @@ use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::transform::body::CheckType; use crate::kani_middle::transform::check_uninit::UninitPass; use crate::kani_middle::transform::check_values::ValidValuePass; -use crate::kani_middle::transform::contracts::AnyModifiesPass; +use crate::kani_middle::transform::contracts::{AnyModifiesPass, FunctionWithContractPass}; use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; @@ -63,7 +63,8 @@ impl BodyTransformation { let check_type = CheckType::new(tcx); transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); - // This has to come after stubs since we want this to replace the stubbed body. + // This has to come after the contract pass since we want this to replace the closure body. + transformer.add_pass(queries, FunctionWithContractPass::new(tcx, &unit)); transformer.add_pass(queries, AnyModifiesPass::new(tcx, &unit)); transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() }); // Putting `UninitPass` after `ValidValuePass` makes sure that the code generated by diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 83744eddabfd..3ee569875211 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -166,17 +166,19 @@ impl KaniSession { pub fn instrument_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> { let Some(assigns) = harness.contract.as_ref() else { return Ok(()) }; - let args: &[std::ffi::OsString] = &[ + let mut args: Vec = vec![ "--dfcc".into(), (&harness.mangled_name).into(), "--enforce-contract".into(), assigns.contracted_function_name.as_str().into(), - "--nondet-static-exclude".into(), - assigns.recursion_tracker.as_str().into(), file.into(), file.into(), ]; - self.call_goto_instrument(args) + if let Some(tracker) = &assigns.recursion_tracker { + args.push("--nondet-static-exclude".into()); + args.push(tracker.as_str().into()); + } + self.call_goto_instrument(&args) } /// Generate a .demangled.c file from the .c file using the `prettyName`s from the symbol table diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 3dd6c82ebd39..ecd1aa20e6c5 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -11,7 +11,8 @@ pub struct AssignsContract { /// The target of the contract pub contracted_function_name: String, /// A static global variable used to track recursion that must not be havocked. - pub recursion_tracker: String, + /// This is only needed if the function is tagged with `#[kani::recursive]` + pub recursion_tracker: Option, } /// We emit this structure for each annotated proof harness (`#[kani::proof]`) we find. @@ -50,6 +51,11 @@ pub struct HarnessAttributes { pub unwind_value: Option, /// The stubs used in this harness. pub stubs: Vec, + /// The name of the function with contract that is being verified if this is a proof for + /// contract. + pub for_contract: Option, + /// The name of the functions being stubbed by their contract. + pub verified_stubs: Vec, } /// The stubbing type. diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 83a2e5d92235..904f413ed078 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -87,6 +87,7 @@ impl<'a> ContractConditionsHandler<'a> { #[allow(dead_code, unused_variables, unused_mut)] let mut #recursion_ident = |#inputs| #output { + #[kanitool::recursion_tracker] static mut REENTRY: bool = false; if unsafe { REENTRY } { #replace_closure From c694db4aeb894aaed1241f572fb7afe6fdaf2c21 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 12 Jul 2024 00:13:49 -0700 Subject: [PATCH 05/18] Get modifies working Still need to fix Receiver handling and closure transformation. 62 passing, 16 failing --- .../codegen_cprover_gotoc/codegen/contract.rs | 85 +++++++------ kani-compiler/src/kani_middle/attributes.rs | 26 ---- .../src/kani_middle/codegen_units.rs | 49 +++++-- kani-compiler/src/kani_middle/resolve.rs | 31 +++++ .../src/kani_middle/transform/contracts.rs | 26 ++-- .../src/kani_middle/transform/mod.rs | 3 +- .../src/sysroot/contracts/check.rs | 120 +++++++----------- 7 files changed, 176 insertions(+), 164 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 8d212de11aa5..c4b6c36a6d9c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -1,9 +1,10 @@ +use std::io::stdout; // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::transform::BodyTransformation; -use cbmc::goto_program::FunctionContract; +use cbmc::goto_program::{DatatypeComponent, FunctionContract, Type}; use cbmc::goto_program::{Lambda, Location}; use cbmc::irep::Symbol; use kani_metadata::AssignsContract; @@ -22,14 +23,12 @@ impl<'tcx> GotocCtx<'tcx> { /// /// 1. Gets the `#[kanitool::inner_check = "..."]` target, then resolves exactly one instance /// of it. Panics if there are more or less than one instance. - /// 2. Expects that a `#[kanitool::modifies(...)]` is placed on the `inner_check` function, - /// turns it into a CBMC contract and attaches it to the symbol for the previously resolved - /// instance. + /// 2. The additional arguments for the inner checks are locations that may be modified. + /// Add them to the list of CBMC's assigns. /// 3. Returns the mangled name of the symbol it attached the contract to. - /// 4. Resolves the `#[kanitool::checked_with = "..."]` target from `function_under_contract` - /// which has `static mut REENTRY : bool` declared inside. - /// 5. Returns the full path to this constant that `--nondet-static-exclude` expects which is - /// comprised of the file path that `checked_with` is located in, the name of the + /// 4. Returns the full path to the static marked with `#[kanitool::recursion_tracker]` which + /// is passed to the `--nondet-static-exclude` argument. + /// This flag expects the file path that `checked_with` is located in, the name of the /// `checked_with` function and the name of the constant (`REENTRY`). pub fn handle_check_contract( &mut self, @@ -37,25 +36,22 @@ impl<'tcx> GotocCtx<'tcx> { items: &[MonoItem], ) -> AssignsContract { let tcx = self.tcx; - let modify_instance = items + let (check, modify) = items .iter() .find_map(|item| { // Find the instance under contract let MonoItem::Fn(instance) = *item else { return None }; if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract { tracing::error!(name=?instance.name(), "------ here"); - self.find_modifies_closure(instance) + self.find_check_and_modifies(instance) } else { None } }) .unwrap(); - + self.attach_modifies_contract(modify); let recursion_tracker = self.find_recursion_tracker(items); - AssignsContract { - recursion_tracker, - contracted_function_name: modify_instance.mangled_name(), - } + AssignsContract { recursion_tracker, contracted_function_name: modify.mangled_name() } } /// The name and location for the recursion tracker should match the exact information added @@ -96,8 +92,8 @@ impl<'tcx> GotocCtx<'tcx> { recursion_tracker } - /// Find the modifies closure recursively since it can be inside check or recursion closure. - fn find_modifies_closure(&mut self, instance: Instance) -> Option { + /// Find the modifies and the check closure recursively since we may have a recursion wrapper. + fn find_check_and_modifies(&mut self, instance: Instance) -> Option<(Instance, Instance)> { let contract_attrs = KaniAttributes::for_instance(self.tcx, instance).contract_attributes()?; let mut find_closure = |inside: Instance, name: &str| { @@ -121,20 +117,20 @@ impl<'tcx> GotocCtx<'tcx> { instance }; let check = find_closure(outside_check, contract_attrs.checked_with.as_str())?; - find_closure(check, contract_attrs.inner_check.as_str()) + Some((check, find_closure(check, contract_attrs.inner_check.as_str())?)) } /// Convert the Kani level contract into a CBMC level contract by creating a /// CBMC lambda. fn codegen_modifies_contract( &mut self, - modified_places: Vec, + goto_annotated_fn_name: &str, + modifies: Instance, loc: Location, ) -> FunctionContract { - let goto_annotated_fn_name = self.current_fn().name(); let goto_annotated_fn_typ = self .symbol_table - .lookup(&goto_annotated_fn_name) + .lookup(goto_annotated_fn_name) .unwrap_or_else(|| panic!("Function '{goto_annotated_fn_name}' is not declared")) .typ .clone(); @@ -160,14 +156,29 @@ impl<'tcx> GotocCtx<'tcx> { }) .unwrap_or_default(); - let assigns = modified_places + // The last argument is a tuple with addresses that can be modified. + let capture_local = Local::from(modifies.fn_abi().unwrap().args.len()); + let capture_ty = self.local_ty_stable(capture_local); + let captured_args = + self.codegen_place_stable(&capture_local.into(), loc).unwrap().goto_expr; + let TyKind::RigidTy(RigidTy::Tuple(capture_tys)) = capture_ty.kind() else { + unreachable!("found {:?}", capture_ty.kind()) + }; + let assigns = capture_tys .into_iter() - .map(|local| { - Lambda::as_contract_for( - &goto_annotated_fn_typ, - None, - self.codegen_place_stable(&local.into(), loc).unwrap().goto_expr.dereference(), - ) + .enumerate() + .filter_map(|(idx, ty)| { + let kind = ty.kind(); + kind.is_raw_ptr().then(|| { + Lambda::as_contract_for( + &goto_annotated_fn_typ, + None, + captured_args + .clone() + .member(idx.to_string(), &self.symbol_table) + .dereference(), + ) + }) }) .chain(shadow_memory_assign) .collect(); @@ -179,17 +190,19 @@ impl<'tcx> GotocCtx<'tcx> { /// `instance` must have previously been declared. /// /// This merges with any previously attached contracts. - pub fn attach_modifies_contract(&mut self, instance: Instance, modified_places: Vec) { + pub fn attach_modifies_contract(&mut self, instance: Instance) { // This should be safe, since the contract is pretty much evaluated as // though it was the first (or last) assertion in the function. assert!(self.current_fn.is_none()); - let body = instance.body().unwrap(); + let body = self.transformer.body(self.tcx, instance); self.set_current_fn(instance, &body); - let goto_contract = - self.codegen_modifies_contract(modified_places, self.codegen_span_stable(body.span)); - let name = self.current_fn().name(); - - self.symbol_table.attach_contract(name, goto_contract); - self.reset_current_fn() + let mangled_name = instance.mangled_name(); + let goto_contract = self.codegen_modifies_contract( + &mangled_name, + instance, + self.codegen_span_stable(instance.def.span()), + ); + self.symbol_table.attach_contract(&mangled_name, goto_contract); + self.reset_current_fn(); } } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 8b087492d511..dd6563af042c 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -62,11 +62,6 @@ enum KaniAttributeKind { /// Attribute on a function that was auto-generated from expanding a /// function contract. IsContractGenerated, - /// Identifies a set of pointer arguments that should be added to the write - /// set when checking a function contract. Placed on the inner check function. - /// - /// Emitted by the expansion of a `modifies` function contract clause. - Modifies, /// A function used as the inner code of a contract check. /// /// Contains the original body of the contracted function. The signature is @@ -98,7 +93,6 @@ impl KaniAttributeKind { | KaniAttributeKind::ReplacedWith | KaniAttributeKind::RecursionCheck | KaniAttributeKind::CheckedWith - | KaniAttributeKind::Modifies | KaniAttributeKind::InnerCheck | KaniAttributeKind::IsContractGenerated => false, } @@ -385,9 +379,6 @@ impl<'tcx> KaniAttributes<'tcx> { // to communicate with one another. So by the time it gets // here we don't care if it's valid or not. } - KaniAttributeKind::Modifies => { - self.modifies_contract(); - } KaniAttributeKind::RecursionTracker => { // Nothing to do here. This is used by contract instrumentation. } @@ -507,7 +498,6 @@ impl<'tcx> KaniAttributes<'tcx> { } KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated - | KaniAttributeKind::Modifies | KaniAttributeKind::InnerCheck | KaniAttributeKind::RecursionCheck | KaniAttributeKind::RecursionTracker @@ -586,22 +576,6 @@ impl<'tcx> KaniAttributes<'tcx> { } } } - - /// Parse and interpret the `kanitool::modifies(var1, var2, ...)` annotation into the vector - /// `[var1, var2, ...]`. - pub fn modifies_contract(&self) -> Option> { - let local_def_id = self.item.expect_local(); - self.map.get(&KaniAttributeKind::Modifies).map(|attr| { - attr.iter() - .flat_map(|clause| match &clause.get_normal_item().args { - AttrArgs::Delimited(lvals) => { - parse_modify_values(self.tcx, local_def_id, &lvals.tokens) - } - _ => unreachable!(), - }) - .collect() - }) - } } /// Pattern macro for the comma token used in attributes. diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 260b363a868a..6c6bea6ea223 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -11,6 +11,7 @@ use crate::args::ReachabilityType; use crate::kani_middle::attributes::is_proof_harness; use crate::kani_middle::metadata::gen_proof_metadata; use crate::kani_middle::reachability::filter_crate_items; +use crate::kani_middle::resolve::{expect_resolve_fn, resolve_fn}; use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; use crate::kani_queries::QueryDb; use kani_metadata::{ArtifactType, AssignsContract, HarnessMetadata, KaniMetadata}; @@ -19,15 +20,15 @@ use rustc_middle::ty::TyCtxt; use rustc_session::config::OutputType; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; -use stable_mir::ty::{FnDef, RigidTy, TyKind}; +use stable_mir::ty::{FnDef, IndexedVal, RigidTy, TyKind}; use stable_mir::CrateDef; -use std::collections::{BTreeMap, HashMap, HashSet}; +use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; use std::fs::File; use std::io::BufWriter; use std::path::{Path, PathBuf}; use tracing::debug; -/// A stable (across compilation sessions) identifier for the harness function. +/// An identifier for the harness function. type Harness = Instance; /// A set of stubs. @@ -124,20 +125,21 @@ fn stub_def(tcx: TyCtxt, def_id: DefId) -> FnDef { } } -/// Group the harnesses by their stubs. +/// Group the harnesses by their stubs and contract usage. fn group_by_stubs( tcx: TyCtxt, all_harnesses: &HashMap, ) -> Vec { - let mut per_stubs: HashMap, CodegenUnit> = - HashMap::default(); + let mut per_stubs: HashMap<_, CodegenUnit> = HashMap::default(); for (harness, metadata) in all_harnesses { let stub_ids = harness_stub_map(tcx, *harness, metadata); + let contracts = extract_contracts(tcx, *harness, metadata); let stub_map = stub_ids .iter() .map(|(k, v)| (tcx.def_path_hash(*k), tcx.def_path_hash(*v))) .collect::>(); - if let Some(unit) = per_stubs.get_mut(&stub_map) { + let key = (contracts, stub_map); + if let Some(unit) = per_stubs.get_mut(&key) { unit.harnesses.push(*harness); } else { let stubs = stub_ids @@ -145,12 +147,43 @@ fn group_by_stubs( .map(|(from, to)| (stub_def(tcx, *from), stub_def(tcx, *to))) .collect::>(); let stubs = apply_transitivity(tcx, *harness, stubs); - per_stubs.insert(stub_map, CodegenUnit { stubs, harnesses: vec![*harness] }); + per_stubs.insert(key, CodegenUnit { stubs, harnesses: vec![*harness] }); } } per_stubs.into_values().collect() } +#[derive(Copy, Clone, Debug, Ord, PartialOrd, PartialEq, Eq, Hash)] +enum ContractUsage { + Stub(usize), + Check(usize), +} + +/// Extract the contract related usages. +/// +/// Note that any error interpreting the result is emitted, but we delay aborting, so we emit as +/// many errors as possible. +fn extract_contracts( + tcx: TyCtxt, + harness: Harness, + metadata: &HarnessMetadata, +) -> BTreeSet { + let def = harness.def; + let mut result = BTreeSet::new(); + if let Some(check) = &metadata.attributes.for_contract { + if let Ok(check_def) = expect_resolve_fn(tcx, def, check, "proof_for_contract") { + result.insert(ContractUsage::Check(check_def.def_id().to_index())); + } + } + + for stub in &metadata.attributes.verified_stubs { + let Ok(stub_def) = expect_resolve_fn(tcx, def, stub, "stub_verified") else { continue }; + result.insert(ContractUsage::Stub(stub_def.def_id().to_index())); + } + + result +} + /// Extract the filename for the metadata file. fn metadata_output_path(tcx: TyCtxt) -> PathBuf { let filepath = tcx.output_filenames(()).path(OutputType::Object); diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 816f25343fe3..6e4d071ea501 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -9,14 +9,18 @@ //! //! Note that glob use statements can form loops. The paths can also walk through the loop. +use rustc_smir::rustc_internal; use std::collections::HashSet; use std::fmt; use std::iter::Peekable; +use rustc_errors::ErrorGuaranteed; use rustc_hir::def::{DefKind, Res}; use rustc_hir::def_id::{DefId, LocalDefId, LocalModDefId, CRATE_DEF_INDEX, LOCAL_CRATE}; use rustc_hir::{ItemKind, UseKind}; use rustc_middle::ty::TyCtxt; +use stable_mir::ty::{FnDef, RigidTy, TyKind}; +use stable_mir::{CrateDef, DefId as StableDefId}; use tracing::debug; /// Attempts to resolve a simple path (in the form of a string) to a function / method `DefId`. @@ -47,6 +51,33 @@ pub fn resolve_fn<'tcx>( } } +/// Resolve the name of a function from the context of the definition provided. +/// +/// Ideally this should pass a more precise span, but we don't keep them around. +pub fn expect_resolve_fn( + tcx: TyCtxt, + res_cx: T, + name: &str, + reason: &str, +) -> Result { + let internal_def_id = rustc_internal::internal(tcx, res_cx.def_id()); + let current_module = tcx.parent_module_from_def_id(internal_def_id.as_local().unwrap()); + let maybe_resolved = resolve_fn(tcx, current_module.to_local_def_id(), name); + let resolved = maybe_resolved.map_err(|err| { + tcx.dcx().span_err( + rustc_internal::internal(tcx, res_cx.span()), + format!("Failed to resolve `{name}` for `{reason}`: {err}"), + ) + })?; + let ty_internal = tcx.type_of(resolved).instantiate_identity(); + let ty = rustc_internal::stable(ty_internal); + if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = ty.kind() { + Ok(def) + } else { + unreachable!("Expected function for `{name}`, but found: {ty}") + } +} + /// Attempts to resolve a simple path (in the form of a string) to a `DefId`. /// The current module is provided as an argument in order to resolve relative /// paths. diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 525019a4137b..d79e68f7ab26 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -23,6 +23,7 @@ use stable_mir::ty::{ use stable_mir::{CrateDef, DefId}; use std::collections::HashSet; use std::fmt::Debug; +use std::io::{stdout, Stdout}; use tracing::{debug, trace}; /// Check if we can replace calls to any_modifies. @@ -61,8 +62,8 @@ impl TransformPass for AnyModifiesPass { if instance.def.def_id() == self.kani_any.unwrap().def_id() { // Ensure kani::any is valid. self.any_body(tcx, body) - } else if self.should_apply(tcx, instance) { - // Replace any modifies occurrences. + } else if instance.ty().kind().is_closure() { + // Replace any modifies occurrences. They should only happen in the contract closures. self.replace_any_modifies(body) } else { (false, body) @@ -97,17 +98,6 @@ impl AnyModifiesPass { AnyModifiesPass { kani_any, kani_any_modifies, target_fn, stubbed } } - /// If we apply `transform_any_modifies` in all contract-generated items, - /// we will end up instantiating `kani::any_modifies` for the replace function - /// every time, even if we are only checking the contract, because the function - /// is always included during contract instrumentation. Thus, we must only apply - /// the transformation if we are using a verified stub or in the presence of recursion. - fn should_apply(&self, tcx: TyCtxt, instance: Instance) -> bool { - let item_attributes = - KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, instance.def.def_id())); - self.stubbed.contains(&instance.def.def_id()) || item_attributes.has_recursion() - } - /// Replace calls to `any_modifies` by calls to `any`. fn replace_any_modifies(&self, mut body: Body) -> (bool, Body) { let mut changed = false; @@ -211,6 +201,7 @@ impl TransformPass for FunctionWithContractPass { /// Transform the function body by replacing it with the stub body. fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { trace!(function=?instance.name(), "FunctionWithContractPass::transform"); + tracing::error!(function=?instance.name(), "FunctionWithContractPass::transform"); let _ = tracing::error_span!("FunctionWithContractPass::transform {}", name = instance.name()) .entered(); @@ -218,7 +209,10 @@ impl TransformPass for FunctionWithContractPass { RigidTy::FnDef(def, _args) => { if let Some(target_closure) = self.select_closure(tcx, *def, &body) { tracing::error!(?target_closure, "FunctionWithContractPass::transform"); - (true, self.replace_by_closure(body, target_closure)) + let _ = body.dump(&mut stdout(), &instance.name()); + let new_body = self.replace_by_closure(body, target_closure); + let _ = new_body.dump(&mut stdout(), &instance.name()); + (true, new_body) } else { // Not a contract annotated function (false, body) @@ -374,15 +368,11 @@ fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureI body.var_debug_info .iter() .find_map(|var_info| { - tracing::error!(name=?var_info.name, target=?var_info, - "find_closure"); if var_info.name.as_str() == name { let ty = match &var_info.value { VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(), VarDebugInfoContents::Const(const_op) => const_op.ty(), }; - tracing::error!(name=?var_info.name, ty=?ty, - "find_closure"); if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() { return Some(ClosureInfo { ty, def, args }); } diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 7cc8e9f2ee06..b12f16b3e35a 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -63,8 +63,9 @@ impl BodyTransformation { let check_type = CheckType::new(tcx); transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); - // This has to come after the contract pass since we want this to replace the closure body. transformer.add_pass(queries, FunctionWithContractPass::new(tcx, &unit)); + // This has to come after the contract pass since we want this to only replace the closure + // body that is relevant for this harness. transformer.add_pass(queries, AnyModifiesPass::new(tcx, &unit)); transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() }); // Putting `UninitPass` after `ValidValuePass` makes sure that the code generated by diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 10999912a294..2d4dc0046f6b 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -4,11 +4,11 @@ //! Logic used for generating the code that checks a contract. use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; -use quote::quote; +use quote::{quote, ToTokens}; use std::mem; use syn::punctuated::Punctuated; use syn::token::Comma; -use syn::{parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, ReturnType, Stmt}; +use syn::{parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt}; use super::{ helpers::*, @@ -16,18 +16,14 @@ use super::{ ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, }; -const WRAPPER_ARG_PREFIX: &str = "_wrapper_arg_"; +const WRAPPER_ARG: &str = "_wrapper_arg"; impl<'a> ContractConditionsHandler<'a> { /// Create the body of a check function. /// /// Wraps the conditions from this attribute around `self.body`. - /// - /// Mutable because a `modifies` clause may need to extend the inner call to - /// the wrapper with new arguments. pub fn make_check_body(&self, mut body_stmts: Vec) -> TokenStream2 { let Self { attr_copy, .. } = self; - match &self.condition_type { ContractConditionsData::Requires { attr } => { quote!({ @@ -53,29 +49,29 @@ impl<'a> ContractConditionsHandler<'a> { }) } ContractConditionsData::Modifies { attr } => { - let wrapper_name = &self.modify_name; - - let wrapper_args = if let Some(wrapper_call_args) = body_stmts - .iter_mut() - .find_map(|stmt| try_as_wrapper_call_args(stmt, &wrapper_name)) - { - let wrapper_args = make_wrapper_idents( - wrapper_call_args.len(), - attr.len(), - WRAPPER_ARG_PREFIX, - ); - wrapper_call_args - .extend(wrapper_args.clone().map(|a| Expr::Verbatim(quote!(#a)))); - wrapper_args + let wrapper_arg_ident = Ident::new(WRAPPER_ARG, Span::call_site()); + let wrapper_tuple = body_stmts.iter_mut().find_map(|stmt| { + if let Stmt::Local(Local { + pat: Pat::Ident(PatIdent { ident, .. }), + init: Some(LocalInit { expr, .. }), + .. + }) = stmt + { + (ident == &wrapper_arg_ident).then_some(expr.as_mut()) + } else { + None + } + }); + if let Some(Expr::Tuple(values)) = wrapper_tuple { + values.elems.extend(attr.iter().map(|attr| { + let expr: Expr = parse_quote!(#attr + as *const _); + expr + })); } else { - unreachable!("Expected check function to call to the modifies wrapper function") - }; - - quote!({ - // Cast to *const () since we only care about the address. - #(let #wrapper_args = #attr as *const _ as *const ();)* - #(#body_stmts)* - }) + unreachable!("Expected tuple but found `{wrapper_tuple:?}`") + } + quote!({#(#body_stmts)*}) } } } @@ -83,17 +79,21 @@ impl<'a> ContractConditionsHandler<'a> { /// Initialize the list of statements for the check closure body. fn initial_check_stmts(&self) -> Vec { let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); + let wrapper_arg_ident = Ident::new(WRAPPER_ARG, Span::call_site()); let return_type = return_type_to_type(&self.annotated_fn.sig.output); + let (inputs, _) = closure_args(&self.annotated_fn.sig.inputs); let modifies_closure = self.modifies_closure( - &self.annotated_fn.sig.inputs, + &inputs, &self.annotated_fn.sig.output, &self.annotated_fn.block, + true, ); let (_, args) = closure_args(&self.annotated_fn.sig.inputs); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); parse_quote!( + let #wrapper_arg_ident = (); #modifies_closure - let #result : #return_type = #modifies_ident(#(#args),*); + let #result : #return_type = #modifies_ident(#(#args,)* #wrapper_arg_ident); #result ) } @@ -126,37 +126,25 @@ impl<'a> ContractConditionsHandler<'a> { *body = syn::parse2(self.make_check_body(mem::take(&mut body.block.stmts))).unwrap(); } - /// Emit a modifies wrapper, possibly augmenting a prior, existing one. - /// - /// We only augment if this clause is a `modifies` clause. Before, - /// we annotated the wrapper arguments with `impl kani::Arbitrary`, - /// so Rust would infer the proper types for each argument. - /// We want to remove the restriction that these arguments must - /// implement `kani::Arbitrary` for checking. Now, we annotate each - /// argument with a generic type parameter, so the compiler can - /// continue inferring the correct types. - pub fn modifies_closure( + /// Emit a modifies wrapper. The first time, we augment the list of inputs to track modifies. + pub fn modifies_closure( &self, - inputs: &Punctuated, + inputs: &Punctuated, output: &ReturnType, body: &Block, + include_modifies: bool, ) -> TokenStream2 { // Filter receiver - let (inputs, _args) = closure_args(inputs); - let wrapper_args: Vec<_> = - if let ContractConditionsData::Modifies { attr } = &self.condition_type { - make_wrapper_idents(inputs.len(), attr.len(), WRAPPER_ARG_PREFIX).collect() - } else { - make_wrapper_idents(inputs.len(), 0, WRAPPER_ARG_PREFIX).collect() - }; + let wrapper_ident = if include_modifies { + vec![Ident::new(WRAPPER_ARG, Span::call_site())] + } else { + vec![] + }; let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); quote!( #[kanitool::is_contract_generated(wrapper)] - #(#[kanitool::modifies(#wrapper_args)])* #[allow(dead_code, unused_variables, unused_mut)] - let mut #modifies_ident = |#inputs #(, #wrapper_args: *const ())*| #output { - #body - }; + let mut #modifies_ident = |#inputs #(, #wrapper_ident: _)*| #output #body; ) } @@ -168,19 +156,11 @@ impl<'a> ContractConditionsHandler<'a> { }; let Expr::Closure(closure) = expr.as_ref() else { unreachable!() }; let Expr::Block(body) = closure.body.as_ref() else { unreachable!() }; - let inputs = closure - .inputs - .iter() - .map(|pat| { - if let Pat::Type(pat_type) = pat { - FnArg::Typed(pat_type.clone()) - } else { - panic!("Expected closure argument, but found: {pat:?}") - } - }) - .collect(); - let stream = self.modifies_closure(&inputs, &closure.output, &body.block); + let stream = + self.modifies_closure(&closure.inputs, &closure.output, &body.block, false); + println!("---- here:\n{stream}\n"); *closure_stmt = syn::parse2(stream).unwrap(); + println!("---- there"); } } } @@ -208,13 +188,3 @@ fn try_as_wrapper_call_args<'a>( _ => None, } } - -/// Make `num` [`Ident`]s with the names `prefix{i}` with `i` starting at `low` and -/// increasing by one each time. -fn make_wrapper_idents( - low: usize, - num: usize, - prefix: &'static str, -) -> impl Iterator + Clone + 'static { - (low..).map(move |i| Ident::new(&format!("{prefix}{i}"), Span::mixed_site())).take(num) -} From 331cd30dbdfa9e25faa20db98e5226433bc1fa55 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 12 Jul 2024 11:37:50 -0700 Subject: [PATCH 06/18] Most tests passing. Only receiver needs handling - TODO: Remove all the debug stuff --- .../src/kani_middle/transform/contracts.rs | 5 +- .../src/sysroot/contracts/bootstrap.rs | 5 +- .../src/sysroot/contracts/check.rs | 59 +++------- .../src/sysroot/contracts/helpers.rs | 101 ++++++++++++++++-- .../src/sysroot/contracts/replace.rs | 4 +- .../src/sysroot/contracts/shared.rs | 13 --- .../gcd_rec_replacement_pass.expected | 2 +- .../gcd_replacement_pass.expected | 2 +- .../modifies/global_fail.expected | 8 +- .../modifies/havoc_pass.expected | 25 ----- .../modifies/havoc_pass_reordered.expected | 25 ----- .../modifies/vec_pass.expected | 10 +- .../expected/function-contract/pattern_use.rs | 3 +- .../simple_replace_pass.expected | 2 +- 14 files changed, 128 insertions(+), 136 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index d79e68f7ab26..d9f931007469 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -230,7 +230,10 @@ impl TransformPass for FunctionWithContractPass { (false, body) } } - other => unreachable!("Unexpected instance type: `{other:?}`"), + other => { + /* static variables case */ + (false, body) + } } } } diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 904f413ed078..c375dd26fd84 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -74,7 +74,8 @@ impl<'a> ContractConditionsHandler<'a> { check_closure: &TokenStream, ) -> TokenStream { let ItemFn { ref sig, .. } = self.annotated_fn; - let (inputs, args) = closure_args(&sig.inputs); + let inputs = closure_params(&sig.inputs); + let args = closure_args(&sig.inputs); let output = &sig.output; let span = Span::call_site(); let result = Ident::new(INTERNAL_RESULT_IDENT, span); @@ -85,7 +86,7 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(recursion_check)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #recursion_ident = |#inputs| #output + let mut #recursion_ident = |#(#inputs),*| #output { #[kanitool::recursion_tracker] static mut REENTRY: bool = false; diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 2d4dc0046f6b..1d46a3504a4f 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -6,14 +6,11 @@ use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::{quote, ToTokens}; use std::mem; -use syn::punctuated::Punctuated; -use syn::token::Comma; -use syn::{parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt}; +use syn::{parse_quote, Block, Expr, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt}; use super::{ - helpers::*, - shared::{build_ensures, try_as_result_assign_mut}, - ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, + helpers::*, shared::build_ensures, ContractConditionsData, ContractConditionsHandler, + INTERNAL_RESULT_IDENT, }; const WRAPPER_ARG: &str = "_wrapper_arg"; @@ -81,14 +78,14 @@ impl<'a> ContractConditionsHandler<'a> { let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); let wrapper_arg_ident = Ident::new(WRAPPER_ARG, Span::call_site()); let return_type = return_type_to_type(&self.annotated_fn.sig.output); - let (inputs, _) = closure_args(&self.annotated_fn.sig.inputs); + let inputs = closure_params(&self.annotated_fn.sig.inputs); let modifies_closure = self.modifies_closure( - &inputs, + inputs, &self.annotated_fn.sig.output, &self.annotated_fn.block, true, ); - let (_, args) = closure_args(&self.annotated_fn.sig.inputs); + let args = closure_args(&self.annotated_fn.sig.inputs); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); parse_quote!( let #wrapper_arg_ident = (); @@ -105,7 +102,7 @@ impl<'a> ContractConditionsHandler<'a> { pub fn check_closure(&self) -> TokenStream2 { let check_ident = Ident::new(&self.check_name, Span::call_site()); let sig = &self.annotated_fn.sig; - let (inputs, _args) = closure_args(&sig.inputs); + let inputs = closure_params(&sig.inputs); let output = &sig.output; let body_stmts = self.initial_check_stmts(); let body = self.make_check_body(body_stmts); @@ -113,7 +110,7 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(check)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #check_ident = |#inputs| #output #body; + let mut #check_ident = |#(#inputs),*| #output #body; ) } @@ -127,24 +124,22 @@ impl<'a> ContractConditionsHandler<'a> { } /// Emit a modifies wrapper. The first time, we augment the list of inputs to track modifies. - pub fn modifies_closure( + pub fn modifies_closure>( &self, - inputs: &Punctuated, + inputs: I, output: &ReturnType, body: &Block, include_modifies: bool, ) -> TokenStream2 { // Filter receiver - let wrapper_ident = if include_modifies { - vec![Ident::new(WRAPPER_ARG, Span::call_site())] - } else { - vec![] - }; + let wrapper_ident = include_modifies.then_some(Ident::new(WRAPPER_ARG, Span::call_site())); + let wrapper_it = wrapper_ident.iter(); let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); + let inputs = inputs.into_iter(); quote!( #[kanitool::is_contract_generated(wrapper)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #modifies_ident = |#inputs #(, #wrapper_ident: _)*| #output #body; + let mut #modifies_ident = |#(#inputs,)* #(#wrapper_it: _,)*| #output #body; ) } @@ -158,33 +153,7 @@ impl<'a> ContractConditionsHandler<'a> { let Expr::Block(body) = closure.body.as_ref() else { unreachable!() }; let stream = self.modifies_closure(&closure.inputs, &closure.output, &body.block, false); - println!("---- here:\n{stream}\n"); *closure_stmt = syn::parse2(stream).unwrap(); - println!("---- there"); } } } - -/// Try to interpret this statement as `let result : <...> = (args ...);` and -/// return a mutable reference to the parameter list. -fn try_as_wrapper_call_args<'a>( - stmt: &'a mut syn::Stmt, - wrapper_fn_name: &str, -) -> Option<&'a mut syn::punctuated::Punctuated> { - let syn::LocalInit { diverge: None, expr: init_expr, .. } = try_as_result_assign_mut(stmt)? - else { - return None; - }; - - match init_expr.as_mut() { - Expr::Call(syn::ExprCall { func: box_func, args, .. }) => match box_func.as_ref() { - syn::Expr::Path(syn::ExprPath { qself: None, path, .. }) - if path.get_ident().map_or(false, |id| id == wrapper_fn_name) => - { - Some(args) - } - _ => None, - }, - _ => None, - } -} diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index e79e440594e4..071958a9e41e 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -5,10 +5,12 @@ //! specific to Kani and contracts. use proc_macro2::{Ident, Span}; +use quote::ToTokens; use std::borrow::Cow; use syn::punctuated::Punctuated; +use syn::spanned::Spanned; use syn::token::Comma; -use syn::{parse_quote, Attribute, Expr, ExprBlock, FnArg, Local, LocalInit, Pat, Stmt}; +use syn::{parse_quote, Attribute, Expr, ExprBlock, FnArg, Local, LocalInit, Stmt}; /// If an explicit return type was provided it is returned, otherwise `()`. pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { @@ -20,23 +22,102 @@ pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { syn::ReturnType::Type(_, typ) => Cow::Borrowed(typ.as_ref()), } } +/// Create an expression that reconstructs a struct that was matched in a pattern. +/// +/// Does not support enums, wildcards, pattern alternatives (`|`), range patterns, or verbatim. +pub fn pat_to_expr(pat: &syn::Pat) -> Expr { + use syn::Pat; + let mk_err = |typ| { + pat.span() + .unwrap() + .error(format!("`{typ}` patterns are not supported for functions with contracts")) + .emit(); + unreachable!() + }; + match pat { + Pat::Const(c) => Expr::Const(c.clone()), + Pat::Ident(id) => Expr::Verbatim(id.ident.to_token_stream()), + Pat::Lit(lit) => Expr::Lit(lit.clone()), + Pat::Reference(rf) => Expr::Reference(syn::ExprReference { + attrs: vec![], + and_token: rf.and_token, + mutability: rf.mutability, + expr: Box::new(pat_to_expr(&rf.pat)), + }), + Pat::Tuple(tup) => Expr::Tuple(syn::ExprTuple { + attrs: vec![], + paren_token: tup.paren_token, + elems: tup.elems.iter().map(pat_to_expr).collect(), + }), + Pat::Slice(slice) => Expr::Reference(syn::ExprReference { + attrs: vec![], + and_token: syn::Token!(&)(Span::call_site()), + mutability: None, + expr: Box::new(Expr::Array(syn::ExprArray { + attrs: vec![], + bracket_token: slice.bracket_token, + elems: slice.elems.iter().map(pat_to_expr).collect(), + })), + }), + Pat::Path(pth) => Expr::Path(pth.clone()), + Pat::Or(_) => mk_err("or"), + Pat::Rest(_) => mk_err("rest"), + Pat::Wild(_) => mk_err("wildcard"), + Pat::Paren(inner) => pat_to_expr(&inner.pat), + Pat::Range(_) => mk_err("range"), + Pat::Struct(strct) => { + if strct.rest.is_some() { + mk_err(".."); + } + Expr::Struct(syn::ExprStruct { + attrs: vec![], + path: strct.path.clone(), + brace_token: strct.brace_token, + dot2_token: None, + rest: None, + qself: strct.qself.clone(), + fields: strct + .fields + .iter() + .map(|field_pat| syn::FieldValue { + attrs: vec![], + member: field_pat.member.clone(), + colon_token: field_pat.colon_token, + expr: pat_to_expr(&field_pat.pat), + }) + .collect(), + }) + } + Pat::Verbatim(_) => mk_err("verbatim"), + Pat::Type(pt) => pat_to_expr(pt.pat.as_ref()), + Pat::TupleStruct(_) => mk_err("tuple struct"), + _ => mk_err("unknown"), + } +} /// Extract the closure arguments which should skip `self`. /// /// Return the declaration form as well as just a plain list of idents for each. -pub fn closure_args( - inputs: &Punctuated, -) -> (Punctuated<&syn::FnArg, Comma>, Vec<&Ident>) { - inputs - .iter() - .filter_map(|arg| { - let FnArg::Typed(syn::PatType { pat, .. }) = arg else { return None }; - let Pat::Ident(pat_ident) = pat.as_ref() else { return None }; - Some((arg, &pat_ident.ident)) +/// TODO: Handle `mut` arguments. +pub fn closure_args(inputs: &Punctuated) -> Vec { + closure_params(inputs) + .map(|arg| { + if let FnArg::Typed(typed) = arg { + pat_to_expr(&typed.pat) + } else { + unreachable!("Receiver should've been filtered") + } }) .collect() } +/// Extract the closure parameters by excluding any receiver. +pub fn closure_params( + inputs: &Punctuated, +) -> impl Iterator + '_ { + inputs.iter().filter(|arg| matches!(arg, FnArg::Typed(_))) +} + /// Find a closure statement attached with `kanitool::is_contract_generated` attribute. pub fn find_contract_closure<'a>(stmts: &'a mut [Stmt], name: &'static str) -> &'a mut Stmt { let contract = stmts.iter_mut().find(|stmt| { diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index b05085212a5f..82efc4f7827f 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -111,7 +111,7 @@ impl<'a> ContractConditionsHandler<'a> { pub fn replace_closure(&self) -> TokenStream { let replace_ident = Ident::new(&self.replace_name, Span::call_site()); let sig = &self.annotated_fn.sig; - let (inputs, _args) = closure_args(&sig.inputs); + let inputs = closure_params(&sig.inputs); let output = &sig.output; let before = self.initial_replace_stmts(); let body = self.expand_replace_body(&before, &vec![]); @@ -119,7 +119,7 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(replace)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #replace_ident = |#inputs| #output #body; + let mut #replace_ident = |#(#inputs),*| #output #body; ) } diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index dce13090cfcc..f189a9f98b0c 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -62,19 +62,6 @@ pub fn try_as_result_assign(stmt: &syn::Stmt) -> Option<&syn::LocalInit> { try_as_result_assign_pat!(stmt, as_ref) } -/// Try to parse this statement as `let result : <...> = ;` and return a mutable reference to -/// `init`. -/// -/// This is the shape of statement we create in check functions (with `init` being a call to check -/// function with additional pointer arguments for the `modifies` clause) and we need to recognize -/// it to then edit this call if we find another `modifies` clause and add its additional arguments. -/// additional conditions. -/// -/// It's a thin wrapper around [`try_as_result_assign_pat!`] to create a mutable match. -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;` diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.expected b/tests/expected/function-contract/gcd_rec_replacement_pass.expected index 29c61cf9437c..b522716cc001 100644 --- a/tests/expected/function-contract/gcd_rec_replacement_pass.expected +++ b/tests/expected/function-contract/gcd_rec_replacement_pass.expected @@ -10,7 +10,7 @@ Frac::check_equals.assertion\ - Status: SUCCESS\ - Description: "assertion failed: gcd1 == gcd2" -gcd.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "x != 0 && y != 0" diff --git a/tests/expected/function-contract/gcd_replacement_pass.expected b/tests/expected/function-contract/gcd_replacement_pass.expected index 48d3565ef9f1..1c6df8455267 100644 --- a/tests/expected/function-contract/gcd_replacement_pass.expected +++ b/tests/expected/function-contract/gcd_replacement_pass.expected @@ -1,4 +1,4 @@ -gcd.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "x != 0 && y != 0" diff --git a/tests/expected/function-contract/modifies/global_fail.expected b/tests/expected/function-contract/modifies/global_fail.expected index 04e0359ad8a4..a9ecaf689376 100644 --- a/tests/expected/function-contract/modifies/global_fail.expected +++ b/tests/expected/function-contract/modifies/global_fail.expected @@ -1,9 +1,9 @@ assigns\ - Status: FAILURE\ -- Description: "Check that *var_1 is assignable"\ -in function modify_wrapper +- Description: "Check that *var_3 is assignable"\ +in function modify -Failed Checks: Check that *var_1 is assignable\ -in modify_wrapper +Failed Checks: Check that *var_3 is assignable\ +in modify VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/havoc_pass.expected b/tests/expected/function-contract/modifies/havoc_pass.expected index 02ce972ef370..5fb91406ae18 100644 --- a/tests/expected/function-contract/modifies/havoc_pass.expected +++ b/tests/expected/function-contract/modifies/havoc_pass.expected @@ -10,29 +10,4 @@ copy.assigns\ - Description: "Check that var_4 is assignable"\ in function copy -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_3 is assignable"\ -in function copy\ - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_5 is assignable"\ -in function copy - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that *var_5 is assignable"\ -in function copy\ - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_7 is assignable"\ -in function copy - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that *var_7 is assignable"\ -in function copy - VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected index 02ce972ef370..2ea601aa26a0 100644 --- a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected +++ b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected @@ -5,34 +5,9 @@ in function copy_replace VERIFICATION:- SUCCESSFUL -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_4 is assignable"\ -in function copy - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_3 is assignable"\ -in function copy\ - copy.assigns\ - Status: SUCCESS\ - Description: "Check that var_5 is assignable"\ in function copy -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that *var_5 is assignable"\ -in function copy\ - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_7 is assignable"\ -in function copy - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that *var_7 is assignable"\ -in function copy - VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/vec_pass.expected b/tests/expected/function-contract/modifies/vec_pass.expected index 4d5407fdd850..4ac03d025558 100644 --- a/tests/expected/function-contract/modifies/vec_pass.expected +++ b/tests/expected/function-contract/modifies/vec_pass.expected @@ -1,17 +1,17 @@ -modify.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "v.len() > 0"\ in function modify -modify_replace.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "element set"\ -in function modify_replace +in function modify -modify_replace.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "vector tail equality"\ -in function modify_replace +in function modify assertion\ - Status: SUCCESS\ diff --git a/tests/expected/function-contract/pattern_use.rs b/tests/expected/function-contract/pattern_use.rs index ead1c1538b4d..b02cc776d299 100644 --- a/tests/expected/function-contract/pattern_use.rs +++ b/tests/expected/function-contract/pattern_use.rs @@ -1,9 +1,10 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts +//! Test that contracts supports function args with pattern use and mut declaration. #[kani::ensures(|result : &u32| *result <= dividend)] -fn div((dividend, divisor): (u32, u32)) -> u32 { +fn div((mut dividend, divisor): (u32, u32)) -> u32 { dividend / divisor } diff --git a/tests/expected/function-contract/simple_replace_pass.expected b/tests/expected/function-contract/simple_replace_pass.expected index e1fc78ca462f..7dbc9bae68bd 100644 --- a/tests/expected/function-contract/simple_replace_pass.expected +++ b/tests/expected/function-contract/simple_replace_pass.expected @@ -1,4 +1,4 @@ -div.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "divisor != 0" From 8c240f97260c5d833a59ff90f8942e0cf50a1de3 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 18 Jul 2024 21:28:03 -0700 Subject: [PATCH 07/18] Working version! Need to cleanup --- .../codegen_cprover_gotoc/codegen/contract.rs | 17 +- kani-compiler/src/kani_middle/attributes.rs | 21 +- .../src/kani_middle/transform/body.rs | 28 +++ .../src/kani_middle/transform/contracts.rs | 216 ++++++++++-------- library/kani/src/internal.rs | 46 ++++ .../src/sysroot/contracts/bootstrap.rs | 53 +++-- .../src/sysroot/contracts/check.rs | 88 +++++-- .../src/sysroot/contracts/helpers.rs | 166 +++++++------- .../src/sysroot/contracts/replace.rs | 3 +- .../modifies/havoc_pass.expected | 4 +- .../modifies/simple_fail.expected | 4 +- .../trait_impls/associated_fn.expected | 7 + .../trait_impls/associated_fn.rs | 36 +++ .../function-contract/trait_impls/methods.rs | 35 ++- 14 files changed, 479 insertions(+), 245 deletions(-) create mode 100644 tests/expected/function-contract/trait_impls/associated_fn.expected create mode 100644 tests/expected/function-contract/trait_impls/associated_fn.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index c4b6c36a6d9c..0ceedba4800f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -42,7 +42,6 @@ impl<'tcx> GotocCtx<'tcx> { // Find the instance under contract let MonoItem::Fn(instance) = *item else { return None }; if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract { - tracing::error!(name=?instance.name(), "------ here"); self.find_check_and_modifies(instance) } else { None @@ -157,14 +156,14 @@ impl<'tcx> GotocCtx<'tcx> { .unwrap_or_default(); // The last argument is a tuple with addresses that can be modified. - let capture_local = Local::from(modifies.fn_abi().unwrap().args.len()); - let capture_ty = self.local_ty_stable(capture_local); - let captured_args = - self.codegen_place_stable(&capture_local.into(), loc).unwrap().goto_expr; - let TyKind::RigidTy(RigidTy::Tuple(capture_tys)) = capture_ty.kind() else { - unreachable!("found {:?}", capture_ty.kind()) + let modifies_local = Local::from(modifies.fn_abi().unwrap().args.len()); + let modifies_ty = self.local_ty_stable(modifies_local); + let modifies_args = + self.codegen_place_stable(&modifies_local.into(), loc).unwrap().goto_expr; + let TyKind::RigidTy(RigidTy::Tuple(modifies_tys)) = modifies_ty.kind() else { + unreachable!("found {:?}", modifies_ty.kind()) }; - let assigns = capture_tys + let assigns: Vec<_> = modifies_tys .into_iter() .enumerate() .filter_map(|(idx, ty)| { @@ -173,7 +172,7 @@ impl<'tcx> GotocCtx<'tcx> { Lambda::as_contract_for( &goto_annotated_fn_typ, None, - captured_args + modifies_args .clone() .member(idx.to_string(), &self.symbol_table) .dereference(), diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index dd6563af042c..0a6be37c06af 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -74,6 +74,9 @@ enum KaniAttributeKind { Recursion, /// Attribute used to mark the static variable used for tracking recursion check. RecursionTracker, + /// Generic marker that can be used to mark functions so this list doesn't have to keep growing. + /// This takes a key which is the marker. + FnMarker, } impl KaniAttributeKind { @@ -88,6 +91,7 @@ impl KaniAttributeKind { | KaniAttributeKind::StubVerified | KaniAttributeKind::Unwind => true, KaniAttributeKind::Unstable + | KaniAttributeKind::FnMarker | KaniAttributeKind::Recursion | KaniAttributeKind::RecursionTracker | KaniAttributeKind::ReplacedWith @@ -288,9 +292,14 @@ impl<'tcx> KaniAttributes<'tcx> { }) } - /// Retrieves the global, static recursion tracker variable. - pub fn checked_with_id(&self) -> Option> { - todo!("Delete-me") + /// Return a function marker if any. + pub fn fn_marker(&self) -> Option { + self.attribute_value(KaniAttributeKind::FnMarker) + } + + /// Check if function is annotated with any contract attribute. + pub fn has_contract(&self) -> bool { + self.map.contains_key(&KaniAttributeKind::CheckedWith) } /// Resolve a path starting from this item's module context. @@ -368,7 +377,8 @@ impl<'tcx> KaniAttributes<'tcx> { KaniAttributeKind::StubVerified => { expect_single(self.tcx, kind, &attrs); } - KaniAttributeKind::CheckedWith + KaniAttributeKind::FnMarker + | KaniAttributeKind::CheckedWith | KaniAttributeKind::InnerCheck | KaniAttributeKind::RecursionCheck | KaniAttributeKind::ReplacedWith => { @@ -504,6 +514,9 @@ impl<'tcx> KaniAttributes<'tcx> { | KaniAttributeKind::ReplacedWith => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref())); } + KaniAttributeKind::FnMarker => { + /* no-op */ + } }; harness }) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 181568d3e3f7..e99436bd745d 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -151,6 +151,19 @@ impl MutableBody { result } + /// Add a new assignment to an existing place. + pub fn assign_to( + &mut self, + place: Place, + rvalue: Rvalue, + source: &mut SourceInstruction, + position: InsertPosition, + ) { + let span = source.span(&self.blocks); + let stmt = Statement { kind: StatementKind::Assign(place, rvalue), span }; + self.insert_stmt(stmt, source, position); + } + /// Add a new assert to the basic block indicated by the given index. /// /// The new assertion will have the same span as the source instruction, and the basic block @@ -381,6 +394,15 @@ impl MutableBody { let terminator = Terminator { kind, span: self.span }; self.blocks.push(BasicBlock { statements: Vec::default(), terminator }) } + + /// Replace a terminator from the given basic block + pub fn replace_terminator( + &mut self, + source_instruction: &SourceInstruction, + new_term: Terminator, + ) { + self.blocks.get_mut(source_instruction.bb()).unwrap().terminator = new_term; + } } #[derive(Clone, Debug)] @@ -425,6 +447,12 @@ impl SourceInstruction { SourceInstruction::Terminator { bb } => blocks[bb].terminator.span, } } + + pub fn bb(&self) -> BasicBlockIdx { + match *self { + SourceInstruction::Statement { bb, .. } | SourceInstruction::Terminator { bb } => bb, + } + } } /// Create a new operand that moves local. diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index d9f931007469..73d8893c7464 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -3,6 +3,7 @@ //! This module contains code related to the MIR-to-MIR pass to enable contracts. use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; +use crate::kani_middle::find_fn_def; use crate::kani_middle::transform::body::{ new_move_operand, re_erased, CheckType, InsertPosition, MutableBody, SourceInstruction, }; @@ -12,13 +13,14 @@ use cbmc::{InternString, InternedString}; use rustc_hir::def_id::DefId as InternalDefId; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; +use rustc_span::Symbol; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ AggregateKind, Body, BorrowKind, ConstOperand, Local, Mutability, Operand, Place, Rvalue, - TerminatorKind, VarDebugInfo, VarDebugInfoContents, + Terminator, TerminatorKind, UnwindAction, VarDebugInfo, VarDebugInfoContents, }; use stable_mir::ty::{ - ClosureDef, ClosureKind, FnDef, GenericArgs, MirConst, Region, RigidTy, Ty, TyKind, + ClosureDef, ClosureKind, FnDef, GenericArgs, MirConst, Region, RigidTy, Ty, TyKind, UintTy, }; use stable_mir::{CrateDef, DefId}; use std::collections::HashSet; @@ -201,18 +203,18 @@ impl TransformPass for FunctionWithContractPass { /// Transform the function body by replacing it with the stub body. fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { trace!(function=?instance.name(), "FunctionWithContractPass::transform"); - tracing::error!(function=?instance.name(), "FunctionWithContractPass::transform"); - let _ = - tracing::error_span!("FunctionWithContractPass::transform {}", name = instance.name()) - .entered(); match instance.ty().kind().rigid().unwrap() { - RigidTy::FnDef(def, _args) => { - if let Some(target_closure) = self.select_closure(tcx, *def, &body) { - tracing::error!(?target_closure, "FunctionWithContractPass::transform"); - let _ = body.dump(&mut stdout(), &instance.name()); - let new_body = self.replace_by_closure(body, target_closure); - let _ = new_body.dump(&mut stdout(), &instance.name()); + RigidTy::FnDef(def, args) => { + if let Some(mode) = self.contract_mode(tcx, *def) { + self.mark_unused(tcx, *def, &body, mode); + let new_body = self.set_mode(tcx, body, mode); (true, new_body) + } else if KaniAttributes::for_instance(tcx, instance).fn_marker() + == Some(Symbol::intern("kani_register_contract")) + { + let run = Instance::resolve(find_fn_def(tcx, "KaniRunContract").unwrap(), args) + .unwrap(); + (true, run.body().unwrap()) } else { // Not a contract annotated function (false, body) @@ -220,7 +222,6 @@ impl TransformPass for FunctionWithContractPass { } RigidTy::Closure(def, _args) => { if self.unused_closures.contains(def) { - tracing::error!("FunctionWithContractPass::transform delete"); // Delete body and mark it as unreachable. let mut new_body = MutableBody::from(body); new_body.clear_body(TerminatorKind::Unreachable); @@ -253,113 +254,142 @@ impl FunctionWithContractPass { FunctionWithContractPass { check_fn, replace_fns, unused_closures: Default::default() } } - /// Create the following body: - /// + /// Functions with contract have the following structure: + /// ```ignore /// fn original([self], args*) { - /// bb0: { - // _3 = {closure@span} { self: _1 }; # If receiver. Otherwise, skip. - // _4 = &_3; # Closure reference is the first argument of the closure. - // _5 = (args*); # Closure arguments tupled is the second argument. - // _0 = <{closure@span} as Fn<(u32,)>>::call(move _4, move _5) -> [return: bb1]; - // } - // - // bb1: { - // return; - // } + /// let kani_contract_mode = kani::internal::mode(); // ** Replace this call + /// match kani_contract_mode { + /// kani::internal::RECURSION_CHECK => { + /// let closure = |/*args*/|{ /*body*/}; + /// kani_register_contract(closure) // ** Replace this call + /// } + /// kani::internal::REPLACE => { + /// // same as above + /// } + /// kani::internal::SIMPLE_CHECK => { + /// // same as above + /// } + /// _ => { /* original code */} + /// } /// } - fn replace_by_closure(&self, body: Body, closure: ClosureInfo) -> Body { - tracing::error!(?closure, "replace_by_closure"); + /// ``` + /// See function `handle_untouched` inside `kani_macros`. + /// + /// Thus, we need to: + /// 1. Initialize `kani_contract_mode` variable to the value corresponding to the mode. + /// + /// Thus replace this call: + /// ```ignore + /// let kani_contract_mode = kani::internal::mode(); // ** Replace this call + /// ``` + /// by: + /// ```ignore + /// let kani_contract_mode = mode_const; + /// goto bbX; + /// ``` + /// 2. Replace `kani_register_contract` by the call to the closure. + fn set_mode(&self, tcx: TyCtxt, body: Body, mode: ContractMode) -> Body { + debug!(?mode, "set_mode"); + let mode_fn = find_fn_def(tcx, "KaniContractMode").unwrap(); let mut new_body = MutableBody::from(body); - new_body.clear_body(TerminatorKind::Return); - let mut source = SourceInstruction::Terminator { bb: 0 }; - - // 1- Create the closure structure if needed, i.e., if it captures the receiver. - let closure_ty = closure.ty; - let captures = !closure_ty.layout().unwrap().shape().is_1zst(); - let closure_local = if captures { - // This closure captures the receiver. - let capture = Rvalue::Aggregate( - AggregateKind::Closure(closure.def, closure.args.clone()), - vec![new_move_operand(Local::from(1usize))], - ); - assert_eq!(capture.ty(new_body.locals()), Ok(closure_ty), "Expected to capture `self`"); - - new_body.new_assignment(capture, &mut source, InsertPosition::Before) - } else { - new_body.new_local(closure_ty, source.span(new_body.blocks()), Mutability::Not) - }; - - // 2- Take the structure address. - let capture_addr = new_body.new_assignment( - Rvalue::Ref(re_erased(), BorrowKind::Shared, Place::from(closure_local)), - &mut source, - InsertPosition::Before, - ); + let (mut mode_call, ret, target) = new_body + .blocks() + .iter() + .enumerate() + .find_map(|(bb_idx, bb)| { + if let TerminatorKind::Call { func, target, destination, .. } = &bb.terminator.kind + { + let (callee, _) = func.ty(new_body.locals()).unwrap().kind().fn_def()?; + (callee == mode_fn).then(|| { + ( + SourceInstruction::Terminator { bb: bb_idx }, + destination.clone(), + target.unwrap(), + ) + }) + } else { + None + } + }) + .unwrap(); - // 3- Create tuple with arguments. - let arg_start = if captures { 2 } else { 1 }; - let arg_locals: Vec<_> = - (arg_start..=new_body.arg_count()).map(|l| new_move_operand(l)).collect(); - let tupled_args = new_body.new_assignment( - Rvalue::Aggregate(AggregateKind::Tuple, arg_locals), - &mut source, + let span = mode_call.span(new_body.blocks()); + let mode_const = new_body.new_const_operand(mode as _, UintTy::U8, span); + new_body.assign_to( + ret.clone(), + Rvalue::Use(mode_const), + &mut mode_call, InsertPosition::Before, ); - - // 4- Call closure and store result into `_0` - let closure_args = vec![new_move_operand(capture_addr), new_move_operand(tupled_args)]; - let closure_instance = - Instance::resolve_closure(closure.def, &closure.args, ClosureKind::FnOnce).unwrap(); - tracing::error!(mangled=?closure_instance.mangled_name(), "replace_by_closure"); - new_body.add_call( - &closure_instance, - &mut source, - InsertPosition::Before, - closure_args, - Place::from(Local::from(0usize)), + new_body.replace_terminator( + &mode_call, + Terminator { kind: TerminatorKind::Goto { target }, span }, ); new_body.into() } - /// Select which contract closure to keep, if any, and mark the rest as unused. - fn select_closure(&mut self, tcx: TyCtxt, fn_def: FnDef, body: &Body) -> Option { + /// Return which contract mode to use for this function if any. + fn contract_mode(&self, tcx: TyCtxt, fn_def: FnDef) -> Option { let kani_attributes = KaniAttributes::for_def_id(tcx, fn_def.def_id()); - if let Some(contract) = kani_attributes.contract_attributes() { - let recursion_closure = - find_closure(tcx, fn_def, &body, contract.recursion_check.as_str()); - let check_closure = find_closure(tcx, fn_def, &body, contract.checked_with.as_str()); - let replace_closure = find_closure(tcx, fn_def, &body, contract.replaced_with.as_str()); + kani_attributes.has_contract().then(|| { let fn_def_id = rustc_internal::internal(tcx, fn_def.def_id()); if self.check_fn == Some(fn_def_id) { - // Delete replace closure and one check closure depending on the type. - self.unused_closures.insert(replace_closure.def); - if contract.has_recursion { - self.unused_closures.insert(check_closure.def); - Some(recursion_closure) + if kani_attributes.has_recursion() { + ContractMode::RecursiveCheck } else { - self.unused_closures.insert(recursion_closure.def); - Some(check_closure) + ContractMode::SimpleCheck } } else if self.replace_fns.contains(&fn_def_id) { - // Delete the check closures. - self.unused_closures.insert(recursion_closure.def); - self.unused_closures.insert(check_closure.def); - Some(replace_closure) + ContractMode::Replace } else { + ContractMode::Original + } + }) + } + + /// Select any unused closure for body deletion. + fn mark_unused(&mut self, tcx: TyCtxt, fn_def: FnDef, body: &Body, mode: ContractMode) { + let contract = + KaniAttributes::for_def_id(tcx, fn_def.def_id()).contract_attributes().unwrap(); + let recursion_closure = find_closure(tcx, fn_def, &body, contract.recursion_check.as_str()); + let check_closure = find_closure(tcx, fn_def, &body, contract.checked_with.as_str()); + let replace_closure = find_closure(tcx, fn_def, &body, contract.replaced_with.as_str()); + match mode { + ContractMode::Original => { // No contract instrumentation needed. Add all closures to the list of unused. self.unused_closures.insert(recursion_closure.def); self.unused_closures.insert(check_closure.def); self.unused_closures.insert(replace_closure.def); - None } - } else { - // Nothing to do - None + ContractMode::RecursiveCheck => { + self.unused_closures.insert(replace_closure.def); + self.unused_closures.insert(check_closure.def); + } + ContractMode::SimpleCheck => { + self.unused_closures.insert(replace_closure.def); + self.unused_closures.insert(recursion_closure.def); + } + ContractMode::Replace => { + self.unused_closures.insert(recursion_closure.def); + self.unused_closures.insert(check_closure.def); + } } } } +/// Enumeration that store the value of which implementation should be selected. +/// +/// Keep the discriminant values in sync with [kani::internal::mode]. +#[derive(Copy, Clone, Debug, PartialEq, Eq)] +enum ContractMode { + Original = 0, + RecursiveCheck = 1, + SimpleCheck = 2, + Replace = 3, +} + +/// Information about a closure. #[derive(Clone, Debug)] struct ClosureInfo { ty: Ty, diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index b589e03f809f..02048449f2b2 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -95,7 +95,53 @@ pub fn init_contracts() {} /// This should only be used within contracts. The intent is to /// perform type inference on a closure's argument +/// TODO: This should be generated inside the function that has contract. This is used for +/// remembers. #[doc(hidden)] pub fn apply_closure bool>(f: U, x: &T) -> bool { f(x) } + +/// Function that calls a closure used to implement contracts. +/// +/// In contracts, we cannot invoke the generated closures directly, instead, we call register +/// contract. This function is a no-op. However, in the reality, we do want to call the closure, +/// so we swap the register body by this function body. +#[doc(hidden)] +#[allow(dead_code)] +#[rustc_diagnostic_item = "KaniRunContract"] +fn run_contract_fn T>(func: F) -> T { + func() +} + +/// This is used for documentation's sake of which implementation to keep during contract verification. +#[doc(hidden)] +type Mode = u8; + +/// Keep the original body. +pub const ORIGINAL: Mode = 0; + +/// Run the check with recursion support. +pub const RECURSION_CHECK: Mode = 1; + +/// Run the simple check with no recursion support. +pub const SIMPLE_CHECK: Mode = 2; + +/// Stub the body with its contract. +pub const REPLACE: Mode = 3; + +/// This function is only used to help with contract instrumentation. +/// +/// It should be removed from the end user code during contract transformation. +/// By default, return the original code (used in concrete playback). +#[doc(hidden)] +#[inline(never)] +#[crate::unstable( + feature = "function-contracts", + issue = 2652, + reason = "experimental support for function contracts" +)] +#[rustc_diagnostic_item = "KaniContractMode"] +pub const fn mode() -> Mode { + ORIGINAL +} diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index c375dd26fd84..a5b009563954 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -25,6 +25,11 @@ impl<'a> ContractConditionsHandler<'a> { let check_closure = self.check_closure(); let recursion_closure = self.new_recursion_closure(&replace_closure, &check_closure); + let span = Span::call_site(); + let replace_ident = Ident::new(&self.replace_name, span); + let check_ident = Ident::new(&self.check_name, span); + let recursion_ident = Ident::new(&self.recursion_name, span); + // The order of `attrs` and `kanitool::{checked_with, // is_contract_generated}` is important here, because macros are // expanded outside in. This way other contract annotations in `attrs` @@ -38,12 +43,30 @@ impl<'a> ContractConditionsHandler<'a> { #[kanitool::replaced_with = #replace_name] #[kanitool::inner_check = #modifies_name] #vis #sig { - // The order doesn't matter since we replicate the logic inside recursion closure. - #recursion_closure - #replace_closure - #check_closure - // -- Now emit the original code. - #block + // Dummy function used to force the compiler to capture the environment. + // We cannot call closures inside constant functions. + // This function gets replaced by `kani::internal::call_closure`. + #[inline(never)] + #[kanitool::fn_marker = "kani_register_contract"] + pub const fn kani_register_contract T>(f: F) -> T { + unreachable!() + } + let kani_contract_mode = kani::internal::mode(); + match kani_contract_mode { + kani::internal::RECURSION_CHECK => { + #recursion_closure; + kani_register_contract(#recursion_ident) + } + kani::internal::REPLACE => { + #replace_closure; + kani_register_contract(#replace_ident) + } + kani::internal::SIMPLE_CHECK => { + #check_closure; + kani_register_contract(#check_ident) + } + _ => #block + } } )); } @@ -55,13 +78,13 @@ impl<'a> ContractConditionsHandler<'a> { pub fn handle_expanded(&mut self) { let mut annotated_fn = self.annotated_fn.clone(); let ItemFn { block, .. } = &mut annotated_fn; - let recursion_closure = find_contract_closure(&mut block.stmts, "recursion_check"); + let recursion_closure = expect_closure_in_match(&mut block.stmts, "recursion_check"); self.expand_recursion(recursion_closure); - let replace_closure = find_contract_closure(&mut block.stmts, "replace"); + let replace_closure = expect_closure_in_match(&mut block.stmts, "replace"); self.expand_replace(replace_closure); - let check_closure = find_contract_closure(&mut block.stmts, "check"); + let check_closure = expect_closure_in_match(&mut block.stmts, "check"); self.expand_check(check_closure); self.output.extend(quote!(#annotated_fn)); @@ -74,8 +97,6 @@ impl<'a> ContractConditionsHandler<'a> { check_closure: &TokenStream, ) -> TokenStream { let ItemFn { ref sig, .. } = self.annotated_fn; - let inputs = closure_params(&sig.inputs); - let args = closure_args(&sig.inputs); let output = &sig.output; let span = Span::call_site(); let result = Ident::new(INTERNAL_RESULT_IDENT, span); @@ -86,17 +107,17 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(recursion_check)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #recursion_ident = |#(#inputs),*| #output + let mut #recursion_ident = || #output { #[kanitool::recursion_tracker] static mut REENTRY: bool = false; if unsafe { REENTRY } { #replace_closure - #replace_ident(#(#args),*) + #replace_ident() } else { unsafe { REENTRY = true }; #check_closure - let #result = #check_ident(#(#args),*); + let #result = #check_ident(); unsafe { REENTRY = false }; #result } @@ -116,12 +137,12 @@ impl<'a> ContractConditionsHandler<'a> { }) .unwrap(); - let replace_closure = find_contract_closure(&mut if_reentry.then_branch.stmts, "replace"); + let replace_closure = expect_closure(&mut if_reentry.then_branch.stmts, "replace"); self.expand_replace(replace_closure); let else_branch = if_reentry.else_branch.as_mut().unwrap(); let Expr::Block(else_block) = else_branch.1.as_mut() else { unreachable!() }; - let check_closure = find_contract_closure(&mut else_block.block.stmts, "check"); + let check_closure = expect_closure(&mut else_block.block.stmts, "check"); self.expand_check(check_closure); } } diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 1d46a3504a4f..49abcaba2c0a 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -4,9 +4,13 @@ //! Logic used for generating the code that checks a contract. use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; -use quote::{quote, ToTokens}; +use quote::quote; use std::mem; -use syn::{parse_quote, Block, Expr, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt}; +use syn::punctuated::Punctuated; +use syn::token::{Comma, SelfValue}; +use syn::{ + parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, PatType, ReturnType, Stmt, +}; use super::{ helpers::*, shared::build_ensures, ContractConditionsData, ContractConditionsHandler, @@ -78,19 +82,15 @@ impl<'a> ContractConditionsHandler<'a> { let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); let wrapper_arg_ident = Ident::new(WRAPPER_ARG, Span::call_site()); let return_type = return_type_to_type(&self.annotated_fn.sig.output); - let inputs = closure_params(&self.annotated_fn.sig.inputs); - let modifies_closure = self.modifies_closure( - inputs, - &self.annotated_fn.sig.output, - &self.annotated_fn.block, - true, - ); - let args = closure_args(&self.annotated_fn.sig.inputs); + let mut_recv = self.has_mutable_receiver().then(|| quote!(core::ptr::addr_of!(self),)); + let redefs = self.arg_redefinitions(); + let modifies_closure = + self.modifies_closure(&self.annotated_fn.sig.output, &self.annotated_fn.block, redefs); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); parse_quote!( - let #wrapper_arg_ident = (); + let #wrapper_arg_ident = (#mut_recv); #modifies_closure - let #result : #return_type = #modifies_ident(#(#args,)* #wrapper_arg_ident); + let #result : #return_type = #modifies_ident(#wrapper_arg_ident); #result ) } @@ -102,7 +102,6 @@ impl<'a> ContractConditionsHandler<'a> { pub fn check_closure(&self) -> TokenStream2 { let check_ident = Ident::new(&self.check_name, Span::call_site()); let sig = &self.annotated_fn.sig; - let inputs = closure_params(&sig.inputs); let output = &sig.output; let body_stmts = self.initial_check_stmts(); let body = self.make_check_body(body_stmts); @@ -110,7 +109,7 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(check)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #check_ident = |#(#inputs),*| #output #body; + let mut #check_ident = || #output #body; ) } @@ -119,27 +118,30 @@ impl<'a> ContractConditionsHandler<'a> { /// First find the modifies body and expand that. Then expand the rest of the body. pub fn expand_check(&self, closure: &mut Stmt) { let body = closure_body(closure); - self.expand_modifies(find_contract_closure(&mut body.block.stmts, "wrapper")); + self.expand_modifies(find_contract_closure(&mut body.block.stmts, "wrapper").expect( + &format!("Internal Failure: Expected to find `wrapper` closure, but found none"), + )); *body = syn::parse2(self.make_check_body(mem::take(&mut body.block.stmts))).unwrap(); } - /// Emit a modifies wrapper. The first time, we augment the list of inputs to track modifies. - pub fn modifies_closure>( + /// Emit a modifies wrapper. It's only argument is the list of addresses that may be modified. + pub fn modifies_closure( &self, - inputs: I, output: &ReturnType, body: &Block, - include_modifies: bool, + redefs: TokenStream2, ) -> TokenStream2 { // Filter receiver - let wrapper_ident = include_modifies.then_some(Ident::new(WRAPPER_ARG, Span::call_site())); - let wrapper_it = wrapper_ident.iter(); + let wrapper_ident = Ident::new(WRAPPER_ARG, Span::call_site()); let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); - let inputs = inputs.into_iter(); + let stmts = &body.stmts; quote!( #[kanitool::is_contract_generated(wrapper)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #modifies_ident = |#(#inputs,)* #(#wrapper_it: _,)*| #output #body; + let mut #modifies_ident = |#wrapper_ident: _| #output { + #redefs + #(#stmts)* + }; ) } @@ -151,9 +153,45 @@ impl<'a> ContractConditionsHandler<'a> { }; let Expr::Closure(closure) = expr.as_ref() else { unreachable!() }; let Expr::Block(body) = closure.body.as_ref() else { unreachable!() }; - let stream = - self.modifies_closure(&closure.inputs, &closure.output, &body.block, false); + let stream = self.modifies_closure(&closure.output, &body.block, TokenStream2::new()); *closure_stmt = syn::parse2(stream).unwrap(); } } + + /// Return whether the original function has a mutable receiver. + fn has_mutable_receiver(&self) -> bool { + let first_arg = self.annotated_fn.sig.inputs.first(); + first_arg + .map(|arg| { + matches!( + arg, + FnArg::Receiver(syn::Receiver { mutability: Some(_), reference: None, .. },) + ) + }) + .unwrap_or(false) + } + + /// Generate argument re-definitions for mutable arguments. + /// + /// This is used so Kani doesn't think that modifying a local argument value is a side effect. + fn arg_redefinitions(&self) -> TokenStream2 { + let mut result = TokenStream2::new(); + for (mutability, ident) in self.arg_bindings() { + if mutability == MutBinding::Mut { + result.extend(quote!(let mut #ident = #ident;)) + } else { + // This would make some replace some temporary variables from error messages. + //result.extend(quote!(let #ident = #ident; )) + } + } + result + } + + /// Extract all arguments bindings and their mutability. + fn arg_bindings(&self) -> impl Iterator { + self.annotated_fn.sig.inputs.iter().flat_map(|arg| match arg { + FnArg::Receiver(_) => vec![], + FnArg::Typed(typed) => pat_to_bindings(typed.pat.as_ref()), + }) + } } diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index 071958a9e41e..32f083216192 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -10,7 +10,7 @@ use std::borrow::Cow; use syn::punctuated::Punctuated; use syn::spanned::Spanned; use syn::token::Comma; -use syn::{parse_quote, Attribute, Expr, ExprBlock, FnArg, Local, LocalInit, Stmt}; +use syn::{parse_quote, Attribute, Expr, ExprBlock, FnArg, Local, LocalInit, PatIdent, Stmt}; /// If an explicit return type was provided it is returned, otherwise `()`. pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { @@ -22,10 +22,31 @@ pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { syn::ReturnType::Type(_, typ) => Cow::Borrowed(typ.as_ref()), } } -/// Create an expression that reconstructs a struct that was matched in a pattern. + +/// Extract the closure parameters by excluding the receiver if one exists. +pub fn closure_inputs(inputs: &Punctuated) -> Punctuated { + inputs + .iter() + .filter_map(|arg| { + if let FnArg::Typed(typed_pat) = arg { + Some(syn::Pat::Type(typed_pat.clone())) + } else { + None + } + }) + .collect() +} + +#[derive(Copy, Clone, Eq, PartialEq)] +pub enum MutBinding { + Mut, + NotMut, +} + +/// Extract all local bindings from a given pattern. /// -/// Does not support enums, wildcards, pattern alternatives (`|`), range patterns, or verbatim. -pub fn pat_to_expr(pat: &syn::Pat) -> Expr { +/// Does not support range patterns, or verbatim. +pub fn pat_to_bindings(pat: &syn::Pat) -> Vec<(MutBinding, &Ident)> { use syn::Pat; let mk_err = |typ| { pat.span() @@ -35,92 +56,47 @@ pub fn pat_to_expr(pat: &syn::Pat) -> Expr { unreachable!() }; match pat { - Pat::Const(c) => Expr::Const(c.clone()), - Pat::Ident(id) => Expr::Verbatim(id.ident.to_token_stream()), - Pat::Lit(lit) => Expr::Lit(lit.clone()), - Pat::Reference(rf) => Expr::Reference(syn::ExprReference { - attrs: vec![], - and_token: rf.and_token, - mutability: rf.mutability, - expr: Box::new(pat_to_expr(&rf.pat)), - }), - Pat::Tuple(tup) => Expr::Tuple(syn::ExprTuple { - attrs: vec![], - paren_token: tup.paren_token, - elems: tup.elems.iter().map(pat_to_expr).collect(), - }), - Pat::Slice(slice) => Expr::Reference(syn::ExprReference { - attrs: vec![], - and_token: syn::Token!(&)(Span::call_site()), - mutability: None, - expr: Box::new(Expr::Array(syn::ExprArray { - attrs: vec![], - bracket_token: slice.bracket_token, - elems: slice.elems.iter().map(pat_to_expr).collect(), - })), - }), - Pat::Path(pth) => Expr::Path(pth.clone()), - Pat::Or(_) => mk_err("or"), - Pat::Rest(_) => mk_err("rest"), - Pat::Wild(_) => mk_err("wildcard"), - Pat::Paren(inner) => pat_to_expr(&inner.pat), - Pat::Range(_) => mk_err("range"), + Pat::Const(c) => vec![], + Pat::Ident(PatIdent { ident, subpat: Some(subpat), mutability, .. }) => { + let mut idents = pat_to_bindings(subpat.1.as_ref()); + idents.push((mutability.map_or(MutBinding::NotMut, |_| MutBinding::Mut), ident)); + idents + } + Pat::Ident(PatIdent { ident, mutability, .. }) => { + vec![(mutability.map_or(MutBinding::NotMut, |_| MutBinding::Mut), ident)] + } + Pat::Lit(lit) => vec![], + Pat::Reference(rf) => vec![], + Pat::Tuple(tup) => tup.elems.iter().flat_map(pat_to_bindings).collect(), + Pat::Slice(slice) => slice.elems.iter().flat_map(pat_to_bindings).collect(), + Pat::Path(pth) => { + vec![] + } + Pat::Or(pat_or) => { + // Note: Patterns are not accepted in function arguments. + // No matter what, the same bindings must exist in all the patterns. + pat_or.cases.first().map(pat_to_bindings).unwrap_or_default() + } + Pat::Rest(_) => vec![], + Pat::Wild(_) => vec![], + Pat::Paren(inner) => pat_to_bindings(&inner.pat), + Pat::Range(_) => vec![], Pat::Struct(strct) => { - if strct.rest.is_some() { - mk_err(".."); - } - Expr::Struct(syn::ExprStruct { - attrs: vec![], - path: strct.path.clone(), - brace_token: strct.brace_token, - dot2_token: None, - rest: None, - qself: strct.qself.clone(), - fields: strct - .fields - .iter() - .map(|field_pat| syn::FieldValue { - attrs: vec![], - member: field_pat.member.clone(), - colon_token: field_pat.colon_token, - expr: pat_to_expr(&field_pat.pat), - }) - .collect(), - }) + strct.fields.iter().flat_map(|field_pat| pat_to_bindings(&field_pat.pat)).collect() } Pat::Verbatim(_) => mk_err("verbatim"), - Pat::Type(pt) => pat_to_expr(pt.pat.as_ref()), - Pat::TupleStruct(_) => mk_err("tuple struct"), + Pat::Type(pt) => pat_to_bindings(pt.pat.as_ref()), + Pat::TupleStruct(tup) => tup.elems.iter().flat_map(pat_to_bindings).collect(), _ => mk_err("unknown"), } } -/// Extract the closure arguments which should skip `self`. -/// -/// Return the declaration form as well as just a plain list of idents for each. -/// TODO: Handle `mut` arguments. -pub fn closure_args(inputs: &Punctuated) -> Vec { - closure_params(inputs) - .map(|arg| { - if let FnArg::Typed(typed) = arg { - pat_to_expr(&typed.pat) - } else { - unreachable!("Receiver should've been filtered") - } - }) - .collect() -} - -/// Extract the closure parameters by excluding any receiver. -pub fn closure_params( - inputs: &Punctuated, -) -> impl Iterator + '_ { - inputs.iter().filter(|arg| matches!(arg, FnArg::Typed(_))) -} - /// Find a closure statement attached with `kanitool::is_contract_generated` attribute. -pub fn find_contract_closure<'a>(stmts: &'a mut [Stmt], name: &'static str) -> &'a mut Stmt { - let contract = stmts.iter_mut().find(|stmt| { +pub fn find_contract_closure<'a>( + stmts: &'a mut [Stmt], + name: &'static str, +) -> Option<&'a mut Stmt> { + stmts.iter_mut().find(|stmt| { if let Stmt::Local(local) = stmt { let ident = Ident::new(name, Span::call_site()); let attr: Attribute = parse_quote!(#[kanitool::is_contract_generated(#ident)]); @@ -128,8 +104,32 @@ pub fn find_contract_closure<'a>(stmts: &'a mut [Stmt], name: &'static str) -> & } else { false } + }) +} + +/// Find a closure defined in one of the provided statements. +/// +/// Panic if no closure was found. +pub fn expect_closure<'a>(stmts: &'a mut [Stmt], name: &'static str) -> &'a mut Stmt { + find_contract_closure(stmts, name) + .expect(&format!("Internal Failure: Expected to find `{name}` closure, but found none")) +} + +/// Find a closure inside a match block. +/// +/// Panic if no closure was found. +pub fn expect_closure_in_match<'a>(stmts: &'a mut [Stmt], name: &'static str) -> &'a mut Stmt { + let closure = stmts.iter_mut().find_map(|stmt| { + if let Stmt::Expr(Expr::Match(match_expr), ..) = stmt { + match_expr.arms.iter_mut().find_map(|arm| { + let Expr::Block(block) = arm.body.as_mut() else { return None }; + find_contract_closure(&mut block.block.stmts, name) + }) + } else { + None + } }); - contract.expect(&format!("Internal Failure: Expected to find closure `{name}`, but found none")) + closure.expect(&format!("Internal Failure: Expected to find `{name}` closure, but found none")) } /// Extract the body of a closure declaration. diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 82efc4f7827f..a705737a3e31 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -111,7 +111,6 @@ impl<'a> ContractConditionsHandler<'a> { pub fn replace_closure(&self) -> TokenStream { let replace_ident = Ident::new(&self.replace_name, Span::call_site()); let sig = &self.annotated_fn.sig; - let inputs = closure_params(&sig.inputs); let output = &sig.output; let before = self.initial_replace_stmts(); let body = self.expand_replace_body(&before, &vec![]); @@ -119,7 +118,7 @@ impl<'a> ContractConditionsHandler<'a> { quote!( #[kanitool::is_contract_generated(replace)] #[allow(dead_code, unused_variables, unused_mut)] - let mut #replace_ident = |#(#inputs),*| #output #body; + let mut #replace_ident = || #output #body; ) } diff --git a/tests/expected/function-contract/modifies/havoc_pass.expected b/tests/expected/function-contract/modifies/havoc_pass.expected index 5fb91406ae18..d5679f71b74c 100644 --- a/tests/expected/function-contract/modifies/havoc_pass.expected +++ b/tests/expected/function-contract/modifies/havoc_pass.expected @@ -1,11 +1,11 @@ -copy_replace.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "equality"\ in function copy_replace VERIFICATION:- SUCCESSFUL -copy.assigns\ +.assigns\ - Status: SUCCESS\ - Description: "Check that var_4 is assignable"\ in function copy diff --git a/tests/expected/function-contract/modifies/simple_fail.expected b/tests/expected/function-contract/modifies/simple_fail.expected index ffaee2293931..269ffa6cc2e2 100644 --- a/tests/expected/function-contract/modifies/simple_fail.expected +++ b/tests/expected/function-contract/modifies/simple_fail.expected @@ -1,7 +1,7 @@ assigns\ - Status: FAILURE\ -- Description: "Check that *ptr is assignable" +- Description: "Check that *var_6 is assignable" -Failed Checks: Check that *ptr is assignable +Failed Checks: Check that *var_6 is assignable VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/trait_impls/associated_fn.expected b/tests/expected/function-contract/trait_impls/associated_fn.expected new file mode 100644 index 000000000000..c6f4c6382f17 --- /dev/null +++ b/tests/expected/function-contract/trait_impls/associated_fn.expected @@ -0,0 +1,7 @@ +Checking harness check_foo_b... +VERIFICATION:- SUCCESSFUL + +Checking harness check_foo_a... +VERIFICATION:- SUCCESSFUL + +Complete - 2 successfully verified harnesses, 0 failures, 2 total diff --git a/tests/expected/function-contract/trait_impls/associated_fn.rs b/tests/expected/function-contract/trait_impls/associated_fn.rs new file mode 100644 index 000000000000..807469bcc7e3 --- /dev/null +++ b/tests/expected/function-contract/trait_impls/associated_fn.rs @@ -0,0 +1,36 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +//! Check that we can add contracts to associated functions. + +extern crate kani; + +#[derive(PartialEq, Eq)] +enum Foo { + A(u8), + B(char), +} + +impl Foo { + #[kani::ensures(|result| *result == Foo::A(inner))] + pub fn new_a(inner: u8) -> Foo { + Foo::A(inner) + } + + #[kani::requires(char::from_u32(inner).is_some())] + #[kani::ensures(|result| matches!(*result, Foo::B(c) if u32::from(c) == inner))] + pub unsafe fn new_b(inner: u32) -> Foo { + Foo::B(char::from_u32_unchecked(inner)) + } +} + +#[kani::proof_for_contract(Foo::new_a)] +fn check_foo_a() { + let _ = Foo::new_a(kani::any()); +} + +#[kani::proof_for_contract(Foo::new_b)] +fn check_foo_b() { + let _ = unsafe { Foo::new_b(kani::any()) }; +} diff --git a/tests/expected/function-contract/trait_impls/methods.rs b/tests/expected/function-contract/trait_impls/methods.rs index 46204249946c..128710f1436d 100644 --- a/tests/expected/function-contract/trait_impls/methods.rs +++ b/tests/expected/function-contract/trait_impls/methods.rs @@ -4,14 +4,9 @@ // See GitHub history for details. // kani-flags: -Zfunction-contracts -//! Check that we can add contract to a trait implementation. +//! Check that we can add contract to methods and trait implementations. //! Original code taken from: //! -//! -//! TODO: Add the following tests -//! Multiple annotations and: -//! - mut args -//! - inner functions use std::ops::Add; @@ -36,14 +31,36 @@ impl Add for Point { impl Point { #[kani::modifies(&mut self.x)] #[kani::requires(!self.x.overflowing_add(val).1)] - #[kani::ensures(|_| val > 0 || self.x < old(self.x))] - #[kani::ensures(|_| val < 0 || self.x > old(self.x))] + #[kani::ensures(|_| val < 0 || self.x >= old(self.x))] + #[kani::ensures(|_| val > 0 || self.x <= old(self.x))] pub fn add_x(&mut self, val: i32) { self.x += val; } + + #[kani::requires(self.y < i32::MAX)] + #[kani::ensures(|result| result.y == old(self.y) + 1)] + pub fn next_y(mut self) -> Self { + self.y += 1; + self + } +} + +#[kani::proof_for_contract(Point::add_x)] +fn check_add_x() { + let mut p1: Point = kani::any(); + let _ = p1.add_x(kani::any()); +} + +#[kani::proof_for_contract(Point::next_y)] +fn check_next_y() { + let p1: Point = kani::any(); + let _ = p1.next_y(); } -#[kani::proof_for_contract(add)] +/// We should enable this once we add support to specifying trait methods: +/// +#[cfg(ignore)] +#[kani::proof_for_contract(Point::add)] fn check_add() { let (p1, p2): (Point, Point) = kani::any(); let _ = p1.add(p2); From 543252280dbf59dfc21f5aaa62bd32f5c9d605a2 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 18 Jul 2024 23:12:27 -0700 Subject: [PATCH 08/18] Clean up dead functions, unused imports and clippy --- .../codegen_cprover_gotoc/codegen/contract.rs | 21 ++-- kani-compiler/src/kani_middle/attributes.rs | 105 +++--------------- .../src/kani_middle/codegen_units.rs | 4 +- kani-compiler/src/kani_middle/resolve.rs | 2 +- .../src/kani_middle/transform/body.rs | 11 +- .../src/kani_middle/transform/contracts.rs | 61 ++++------ .../src/sysroot/contracts/check.rs | 6 +- .../src/sysroot/contracts/helpers.rs | 27 +---- .../trait_impls/methods.expected | 17 +++ 9 files changed, 77 insertions(+), 177 deletions(-) create mode 100644 tests/expected/function-contract/trait_impls/methods.expected diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 0ceedba4800f..791857c6f607 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -1,20 +1,16 @@ -use std::io::stdout; // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::attributes::KaniAttributes; -use crate::kani_middle::transform::BodyTransformation; -use cbmc::goto_program::{DatatypeComponent, FunctionContract, Type}; +use cbmc::goto_program::FunctionContract; use cbmc::goto_program::{Lambda, Location}; -use cbmc::irep::Symbol; use kani_metadata::AssignsContract; use rustc_hir::def_id::DefId as InternalDefId; use rustc_smir::rustc_internal; use stable_mir::mir::mono::{Instance, MonoItem}; -use stable_mir::mir::{Body, Local, VarDebugInfoContents}; -use stable_mir::ty::{ClosureKind, FnDef, RigidTy, TyKind}; +use stable_mir::mir::{Local, VarDebugInfoContents}; +use stable_mir::ty::{FnDef, RigidTy, TyKind}; use stable_mir::CrateDef; -use tracing::debug; impl<'tcx> GotocCtx<'tcx> { /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`, @@ -36,13 +32,13 @@ impl<'tcx> GotocCtx<'tcx> { items: &[MonoItem], ) -> AssignsContract { let tcx = self.tcx; - let (check, modify) = items + let modify = items .iter() .find_map(|item| { // Find the instance under contract let MonoItem::Fn(instance) = *item else { return None }; if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract { - self.find_check_and_modifies(instance) + self.find_modifies(instance) } else { None } @@ -91,8 +87,9 @@ impl<'tcx> GotocCtx<'tcx> { recursion_tracker } - /// Find the modifies and the check closure recursively since we may have a recursion wrapper. - fn find_check_and_modifies(&mut self, instance: Instance) -> Option<(Instance, Instance)> { + /// Find the modifies recursively since we may have a recursion wrapper. + /// I.e.: [recursion_wrapper ->]? check -> modifies. + fn find_modifies(&mut self, instance: Instance) -> Option { let contract_attrs = KaniAttributes::for_instance(self.tcx, instance).contract_attributes()?; let mut find_closure = |inside: Instance, name: &str| { @@ -116,7 +113,7 @@ impl<'tcx> GotocCtx<'tcx> { instance }; let check = find_closure(outside_check, contract_attrs.checked_with.as_str())?; - Some((check, find_closure(check, contract_attrs.inner_check.as_str())?)) + find_closure(check, contract_attrs.inner_check.as_str()) } /// Convert the Kani level contract into a CBMC level contract by creating a diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 0a6be37c06af..14d386bfc54c 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -6,24 +6,16 @@ use std::collections::BTreeMap; use kani_metadata::{CbmcSolver, HarnessAttributes, Stub}; use rustc_ast::{ - attr, - token::Token, - token::TokenKind, - tokenstream::{TokenStream, TokenTree}, - AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, + attr, AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, NestedMetaItem, }; use rustc_errors::ErrorGuaranteed; -use rustc_hir::{ - def::DefKind, - def_id::{DefId, LocalDefId}, -}; +use rustc_hir::{def::DefKind, def_id::DefId}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_session::Session; use rustc_smir::rustc_internal; use rustc_span::{Span, Symbol}; use stable_mir::mir::mono::Instance as InstanceStable; -use stable_mir::mir::Local; use stable_mir::{CrateDef, DefId as StableDefId}; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; @@ -234,23 +226,21 @@ impl<'tcx> KaniAttributes<'tcx> { /// /// In the case of an error, this function will emit the error and return `None`. pub(crate) fn interpret_for_contract_attribute(&self) -> Option<(Symbol, DefId, Span)> { - self.expect_maybe_one(KaniAttributeKind::ProofForContract) - .map(|target| { - let name = expect_key_string_value(self.tcx.sess, target).ok()?; - self.resolve_from_mod(name.as_str()) - .map(|ok| (name, ok, target.span)) - .map_err(|resolve_err| { - self.tcx.dcx().span_err( - target.span, - format!( - "Failed to resolve checking function {} because {resolve_err}", - name.as_str() - ), - ) - }) - .ok() - }) - .flatten() + self.expect_maybe_one(KaniAttributeKind::ProofForContract).and_then(|target| { + let name = expect_key_string_value(self.tcx.sess, target).ok()?; + self.resolve_from_mod(name.as_str()) + .map(|ok| (name, ok, target.span)) + .map_err(|resolve_err| { + self.tcx.dcx().span_err( + target.span, + format!( + "Failed to resolve checking function {} because {resolve_err}", + name.as_str() + ), + ) + }) + .ok() + }) } pub fn proof_for_contract(&self) -> Option> { @@ -404,8 +394,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// upstream. fn attribute_value(&self, kind: KaniAttributeKind) -> Option { self.expect_maybe_one(kind) - .map(|target| expect_key_string_value(self.tcx.sess, target).ok()) - .flatten() + .and_then(|target| expect_key_string_value(self.tcx.sess, target).ok()) } /// Check that any unstable API has been enabled. Otherwise, emit an error. @@ -591,64 +580,6 @@ impl<'tcx> KaniAttributes<'tcx> { } } -/// Pattern macro for the comma token used in attributes. -macro_rules! comma_tok { - () => { - TokenTree::Token(Token { kind: TokenKind::Comma, .. }, _) - }; -} - -/// Parse the token stream inside an attribute (like `kanitool::modifies`) as a comma separated -/// sequence of function parameter names on `local_def_id` (must refer to a function). Then -/// translates the names into [`Local`]s. -fn parse_modify_values<'a>( - tcx: TyCtxt<'a>, - local_def_id: LocalDefId, - t: &'a TokenStream, -) -> impl Iterator + 'a { - let mir = tcx.optimized_mir(local_def_id); - let mut iter = t.trees(); - std::iter::from_fn(move || { - let tree = iter.next()?; - let wrong_token_err = - || tcx.sess.dcx().span_err(tree.span(), "Unexpected token. Expected identifier."); - let result = match tree { - TokenTree::Token(token, _) => { - if let TokenKind::Ident(id, _) = &token.kind { - let hir = tcx.hir(); - let bid = hir.body_owned_by(local_def_id).id(); - Some( - hir.body_param_names(bid) - .zip(mir.args_iter()) - .find(|(name, _decl)| name.name == *id) - .unwrap() - .1 - .as_usize(), - ) - } else { - wrong_token_err(); - None - } - } - _ => { - wrong_token_err(); - None - } - }; - match iter.next() { - None | Some(comma_tok!()) => (), - Some(not_comma) => { - tcx.sess.dcx().span_err( - not_comma.span(), - "Unexpected token, expected end of attribute or comma", - ); - iter.by_ref().skip_while(|t| !matches!(t, comma_tok!())).count(); - } - } - result - }) -} - /// An efficient check for the existence for a particular [`KaniAttributeKind`]. /// Unlike querying [`KaniAttributes`] this method builds no new heap data /// structures and has short circuiting. diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 6c6bea6ea223..99fab29a9d84 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -11,11 +11,11 @@ use crate::args::ReachabilityType; use crate::kani_middle::attributes::is_proof_harness; use crate::kani_middle::metadata::gen_proof_metadata; use crate::kani_middle::reachability::filter_crate_items; -use crate::kani_middle::resolve::{expect_resolve_fn, resolve_fn}; +use crate::kani_middle::resolve::expect_resolve_fn; use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; use crate::kani_queries::QueryDb; use kani_metadata::{ArtifactType, AssignsContract, HarnessMetadata, KaniMetadata}; -use rustc_hir::def_id::{DefId, DefPathHash}; +use rustc_hir::def_id::DefId; use rustc_middle::ty::TyCtxt; use rustc_session::config::OutputType; use rustc_smir::rustc_internal; diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 6e4d071ea501..ca4e8e749b75 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -20,7 +20,7 @@ use rustc_hir::def_id::{DefId, LocalDefId, LocalModDefId, CRATE_DEF_INDEX, LOCAL use rustc_hir::{ItemKind, UseKind}; use rustc_middle::ty::TyCtxt; use stable_mir::ty::{FnDef, RigidTy, TyKind}; -use stable_mir::{CrateDef, DefId as StableDefId}; +use stable_mir::CrateDef; use tracing::debug; /// Attempts to resolve a simple path (in the form of a string) to a function / method `DefId`. diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index e99436bd745d..db21aeea6b62 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -7,14 +7,10 @@ use crate::kani_middle::find_fn_def; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::mir::*; -use stable_mir::ty::{GenericArgs, MirConst, Region, RegionKind, Span, Ty, UintTy}; +use stable_mir::ty::{GenericArgs, MirConst, Span, Ty, UintTy}; use std::fmt::Debug; use std::mem; -pub const fn re_erased() -> Region { - Region { kind: RegionKind::ReErased } -} - /// This structure mimics a Body that can actually be modified. pub struct MutableBody { blocks: Vec, @@ -455,11 +451,6 @@ impl SourceInstruction { } } -/// Create a new operand that moves local. -pub fn new_move_operand(local: Local) -> Operand { - Operand::Move(Place::from(Local::from(local))) -} - fn find_instance(tcx: TyCtxt, diagnostic: &str) -> Option { Instance::resolve(find_fn_def(tcx, diagnostic)?, &GenericArgs(vec![])).ok() } diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 73d8893c7464..72ced0905f51 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -4,9 +4,7 @@ use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::find_fn_def; -use crate::kani_middle::transform::body::{ - new_move_operand, re_erased, CheckType, InsertPosition, MutableBody, SourceInstruction, -}; +use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use cbmc::{InternString, InternedString}; @@ -16,16 +14,12 @@ use rustc_smir::rustc_internal; use rustc_span::Symbol; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ - AggregateKind, Body, BorrowKind, ConstOperand, Local, Mutability, Operand, Place, Rvalue, - Terminator, TerminatorKind, UnwindAction, VarDebugInfo, VarDebugInfoContents, -}; -use stable_mir::ty::{ - ClosureDef, ClosureKind, FnDef, GenericArgs, MirConst, Region, RigidTy, Ty, TyKind, UintTy, + Body, ConstOperand, Operand, Rvalue, Terminator, TerminatorKind, VarDebugInfoContents, }; -use stable_mir::{CrateDef, DefId}; +use stable_mir::ty::{ClosureDef, FnDef, MirConst, RigidTy, TyKind, UintTy}; +use stable_mir::CrateDef; use std::collections::HashSet; use std::fmt::Debug; -use std::io::{stdout, Stdout}; use tracing::{debug, trace}; /// Check if we can replace calls to any_modifies. @@ -36,7 +30,6 @@ use tracing::{debug, trace}; pub struct AnyModifiesPass { kani_any: Option, kani_any_modifies: Option, - stubbed: HashSet, target_fn: Option, } @@ -89,15 +82,15 @@ impl AnyModifiesPass { let kani_any_modifies = tcx .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies")) .map(item_fn_def); - let (target_fn, stubbed) = if let Some(harness) = unit.harnesses.first() { + let target_fn = if let Some(harness) = unit.harnesses.first() { let attributes = KaniAttributes::for_instance(tcx, *harness); let target_fn = attributes.proof_for_contract().map(|symbol| symbol.unwrap().as_str().intern()); - (target_fn, unit.stubs.keys().map(|from| from.def_id()).collect::>()) + target_fn } else { - (None, HashSet::new()) + None }; - AnyModifiesPass { kani_any, kani_any_modifies, target_fn, stubbed } + AnyModifiesPass { kani_any, kani_any_modifies, target_fn } } /// Replace calls to `any_modifies` by calls to `any`. @@ -231,7 +224,7 @@ impl TransformPass for FunctionWithContractPass { (false, body) } } - other => { + _ => { /* static variables case */ (false, body) } @@ -245,11 +238,11 @@ impl FunctionWithContractPass { pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> FunctionWithContractPass { let harness = unit.harnesses.first().unwrap(); let attrs = KaniAttributes::for_instance(tcx, *harness); - let check_fn = attrs.interpret_for_contract_attribute().map(|(_, def_id, span)| def_id); + let check_fn = attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id); let replace_fns: HashSet<_> = attrs .interpret_stub_verified_attribute() .iter() - .map(|(_, def_id, span)| *def_id) + .map(|(_, def_id, _)| *def_id) .collect(); FunctionWithContractPass { check_fn, replace_fns, unused_closures: Default::default() } } @@ -358,21 +351,21 @@ impl FunctionWithContractPass { match mode { ContractMode::Original => { // No contract instrumentation needed. Add all closures to the list of unused. - self.unused_closures.insert(recursion_closure.def); - self.unused_closures.insert(check_closure.def); - self.unused_closures.insert(replace_closure.def); + self.unused_closures.insert(recursion_closure); + self.unused_closures.insert(check_closure); + self.unused_closures.insert(replace_closure); } ContractMode::RecursiveCheck => { - self.unused_closures.insert(replace_closure.def); - self.unused_closures.insert(check_closure.def); + self.unused_closures.insert(replace_closure); + self.unused_closures.insert(check_closure); } ContractMode::SimpleCheck => { - self.unused_closures.insert(replace_closure.def); - self.unused_closures.insert(recursion_closure.def); + self.unused_closures.insert(replace_closure); + self.unused_closures.insert(recursion_closure); } ContractMode::Replace => { - self.unused_closures.insert(recursion_closure.def); - self.unused_closures.insert(check_closure.def); + self.unused_closures.insert(recursion_closure); + self.unused_closures.insert(check_closure); } } } @@ -389,15 +382,7 @@ enum ContractMode { Replace = 3, } -/// Information about a closure. -#[derive(Clone, Debug)] -struct ClosureInfo { - ty: Ty, - def: ClosureDef, - args: GenericArgs, -} - -fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureInfo { +fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureDef { body.var_debug_info .iter() .find_map(|var_info| { @@ -406,8 +391,8 @@ fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureI VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(), VarDebugInfoContents::Const(const_op) => const_op.ty(), }; - if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() { - return Some(ClosureInfo { ty, def, args }); + if let TyKind::RigidTy(RigidTy::Closure(def, _args)) = ty.kind() { + return Some(def); } } None diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 49abcaba2c0a..69f280ad9335 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -6,11 +6,7 @@ use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::quote; use std::mem; -use syn::punctuated::Punctuated; -use syn::token::{Comma, SelfValue}; -use syn::{ - parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, PatType, ReturnType, Stmt, -}; +use syn::{parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt}; use super::{ helpers::*, shared::build_ensures, ContractConditionsData, ContractConditionsHandler, diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index 32f083216192..410c2d971c44 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -5,12 +5,9 @@ //! specific to Kani and contracts. use proc_macro2::{Ident, Span}; -use quote::ToTokens; use std::borrow::Cow; -use syn::punctuated::Punctuated; use syn::spanned::Spanned; -use syn::token::Comma; -use syn::{parse_quote, Attribute, Expr, ExprBlock, FnArg, Local, LocalInit, PatIdent, Stmt}; +use syn::{parse_quote, Attribute, Expr, ExprBlock, Local, LocalInit, PatIdent, Stmt}; /// If an explicit return type was provided it is returned, otherwise `()`. pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { @@ -23,20 +20,6 @@ pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { } } -/// Extract the closure parameters by excluding the receiver if one exists. -pub fn closure_inputs(inputs: &Punctuated) -> Punctuated { - inputs - .iter() - .filter_map(|arg| { - if let FnArg::Typed(typed_pat) = arg { - Some(syn::Pat::Type(typed_pat.clone())) - } else { - None - } - }) - .collect() -} - #[derive(Copy, Clone, Eq, PartialEq)] pub enum MutBinding { Mut, @@ -56,7 +39,7 @@ pub fn pat_to_bindings(pat: &syn::Pat) -> Vec<(MutBinding, &Ident)> { unreachable!() }; match pat { - Pat::Const(c) => vec![], + Pat::Const(_) => vec![], Pat::Ident(PatIdent { ident, subpat: Some(subpat), mutability, .. }) => { let mut idents = pat_to_bindings(subpat.1.as_ref()); idents.push((mutability.map_or(MutBinding::NotMut, |_| MutBinding::Mut), ident)); @@ -65,11 +48,11 @@ pub fn pat_to_bindings(pat: &syn::Pat) -> Vec<(MutBinding, &Ident)> { Pat::Ident(PatIdent { ident, mutability, .. }) => { vec![(mutability.map_or(MutBinding::NotMut, |_| MutBinding::Mut), ident)] } - Pat::Lit(lit) => vec![], - Pat::Reference(rf) => vec![], + Pat::Lit(_) => vec![], + Pat::Reference(_) => vec![], Pat::Tuple(tup) => tup.elems.iter().flat_map(pat_to_bindings).collect(), Pat::Slice(slice) => slice.elems.iter().flat_map(pat_to_bindings).collect(), - Pat::Path(pth) => { + Pat::Path(_) => { vec![] } Pat::Or(pat_or) => { diff --git a/tests/expected/function-contract/trait_impls/methods.expected b/tests/expected/function-contract/trait_impls/methods.expected new file mode 100644 index 000000000000..3906a6fd7a10 --- /dev/null +++ b/tests/expected/function-contract/trait_impls/methods.expected @@ -0,0 +1,17 @@ +Checking harness check_next_y... + +Status: SUCCESS\ +Description: "|result| result.y == old(self.y) + 1"\ +in function Point::next_y + +VERIFICATION:- SUCCESSFUL + +Checking harness check_add_x... + +Status: SUCCESS\ +Description: "|_| val < 0 || self.x >= old(self.x)"\ +in function Point::add_x + +VERIFICATION:- SUCCESSFUL + +Complete - 2 successfully verified harnesses, 0 failures, 2 total. From d89ad4548d5be21a5cde2e1155650f7fee318312 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 18 Jul 2024 23:37:06 -0700 Subject: [PATCH 09/18] Update code documentation --- .../src/kani_middle/transform/contracts.rs | 45 +- .../kani_macros/src/sysroot/contracts/mod.rs | 386 +++++++++++------- 2 files changed, 289 insertions(+), 142 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 72ced0905f51..b64b1b1177bd 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -162,10 +162,49 @@ impl AnyModifiesPass { /// This pass will transform functions annotated with contracts based on the harness configuration. /// -/// For functions that are being checked, change the body to invoke the "check" closure. -/// For functions that are being stubbed, change the body to invoke the "replace" closure. +/// Functions with contract will always follow the same structure: /// -/// Functions with contract contains +/// ```ignore +/// #[kanitool::recursion_check = "__kani_recursion_check_modify"] +/// #[kanitool::checked_with = "__kani_check_modify"] +/// #[kanitool::replaced_with = "__kani_replace_modify"] +/// #[kanitool::inner_check = "__kani_modifies_modify"] +/// fn name_fn(ptr: &mut u32) { +/// #[kanitool::fn_marker = "kani_register_contract"] +/// pub const fn kani_register_contract T>(f: F) -> T { +/// kani::panic("internal error: entered unreachable code: ") +/// } +/// let kani_contract_mode = kani::internal::mode(); +/// match kani_contract_mode { +/// kani::internal::RECURSION_CHECK => { +/// #[kanitool::is_contract_generated(recursion_check)] +/// let mut __kani_recursion_check_name_fn = || { /* recursion check body */ }; +/// kani_register_contract(__kani_recursion_check_modify) +/// } +/// kani::internal::REPLACE => { +/// #[kanitool::is_contract_generated(replace)] +/// let mut __kani_replace_name_fn = || { /* replace body */ }; +/// kani_register_contract(__kani_replace_name_fn) +/// } +/// kani::internal::SIMPLE_CHECK => { +/// #[kanitool::is_contract_generated(check)] +/// let mut __kani_check_name_fn = || { /* check body */ }; +/// kani_register_contract(__kani_check_name_fn) +/// } +/// _ => { /* original body */ } +/// } +/// } +/// ``` +/// +/// This pass will perform the following operations: +/// 1. For functions with contract that are not being used for check or replacement: +/// - Set `kani_contract_mode` to the value ORIGINAL. +/// - Replace the generated closures body with unreachable. +/// 2. For functions with contract that are being used: +/// - Set `kani_contract_mode` to the value corresponding to the expected usage. +/// - Replace the non-used generated closures body with unreachable. +/// 3. Replace the body of `kani_register_contract` by `kani::internal::run_contract_fn` to +/// invoke the closure. #[derive(Debug)] pub struct FunctionWithContractPass { /// Function that is being checked, if any. diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index ad2246375e13..ef7b88dc87d1 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -31,26 +31,26 @@ //! addition, we also want to make sure to support non-contract attributes on //! functions with contracts. //! -//! To this end we use a state machine. The initial state is an "untouched" +//! To this end we use a state machine with two states. The initial state is an "untouched" //! function with possibly multiple contract attributes, none of which have been //! expanded. When we expand the first (outermost) contract //! attribute on such a function we re-emit the function with a few closures defined -//! in their body, which correspond to the "check" and "replace" that enforce the condition -//! carried by the attribute currently being expanded. +//! in their body, which correspond to the "check", "recursive" and "replace" that enforce the +//! condition carried by the attribute currently being expanded. //! //! We also add new marker attributes to the original function to -//! advance the state machine. The "check" closure gets a -//! `kanitool::is_contract_generated(check)` attributes and analogous for -//! replace. The re-emitted original meanwhile is decorated with +//! advance the state machine. The re-emitted original meanwhile is decorated with //! `kanitool::checked_with(name_of_generated_check_variable)` and an analogous -//! `kanittool::replaced_with` attribute also. The next contract attribute that +//! `kanittool::replaced_with` attribute also. +//! Each closure gets a `kanitool::is_contract_generated()` attributes. +//! The next contract attribute that //! is expanded will detect the presence of these markers in the attributes of //! the item and be able to determine their position in the state machine this -//! way. If the state is either a "check" or "replace" then the body of the -//! function is augmented with the additional conditions carried by the macro. -//! If the state is the "original" function, no changes are performed. +//! way. //! -//! We place marker attributes at the bottom of the attribute stack (innermost), +//! Subsequent run, will expand the existing definitions with the condition being processed. +//! +//! Note: We place marker attributes at the bottom of the attribute stack (innermost), //! otherwise they would not be visible to the future macro expansions. //! //! Below you can see a graphical rendering where boxes are states and each @@ -85,8 +85,8 @@ //! //! The check function is a copy of the original function with preconditions //! added before the body and postconditions after as well as injected before -//! every `return` (see [`PostconditionInjector`]). Attributes on the original -//! function are also copied to the check function. +//! every `return` (see [`PostconditionInjector`]). All arguments are captured +//! by the closure. //! //! ## Replace Function //! @@ -98,10 +98,6 @@ //! Decorates the original function with `#[kanitool::replaced_by = //! "__kani_replace_"]`. //! -//! The replace closure has the same signature as the original function but its -//! body is replaced by `kani::any_modifies()`, which generates a non-deterministic -//! value. -//! //! ## Inductive Verification //! //! To efficiently check recursive functions we verify them inductively. To @@ -128,25 +124,26 @@ //! more than once in its harness. //! //! To facilitate all this we generate a `__kani_recursion_check_` -//! function with the following shape: +//! closure with the following shape: //! //! ```ignored -//! let __kani_recursion_check_func = |(args ...)| { +//! let __kani_recursion_check_func = || { //! static mut REENTRY: bool = false; //! //! if unsafe { REENTRY } { -//! call_replace(fn args...) +//! let __kani_replace_func = || { /* replace body */ } +//! __kani_replace_func() //! } else { //! unsafe { reentry = true }; -//! let result_kani_internal = call_check(fn args...); +//! let __kani_check_func = || { /* check body */ } +//! let result_kani_internal = __kani_check_func(); //! unsafe { reentry = false }; //! result_kani_internal //! } //! }; //! ``` //! -//! We register this closure as `#[kanitool::checked_with = "__kani_recursion_..."]` instead of the -//! check function. +//! We register this closure as `#[kanitool::recursion_check = "__kani_recursion_..."]`. //! //! # Complete example //! @@ -159,56 +156,106 @@ //! ``` //! //! Turns into -//! TODO: Update this //! ``` -//! #[kanitool::checked_with = "div_recursion_check_965916"] -//! #[kanitool::replaced_with = "div_replace_965916"] -//! fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } -//! -//! #[allow(dead_code, unused_variables)] -//! #[kanitool :: is_contract_generated(check)] fn -//! div_check_b97df2(dividend : u32, divisor : u32) -> u32 -//! { -//! let dividend_renamed = kani::internal::untracked_deref(& dividend); -//! let divisor_renamed = kani::internal::untracked_deref(& divisor); -//! kani::assume(divisor != 0); -//! let result_kani_internal : u32 = div_wrapper_b97df2(dividend, divisor); -//! kani::assert( -//! (| result : & u32 | *result <= dividend_renamed)(& result_kani_internal), -//! stringify!(|result : &u32| *result <= dividend)); -//! std::mem::forget(dividend_renamed); -//! std::mem::forget(divisor_renamed); -//! result_kani_internal -//! } -//! -//! #[allow(dead_code, unused_variables)] -//! #[kanitool :: is_contract_generated(replace)] fn -//! div_replace_b97df2(dividend : u32, divisor : u32) -> u32 -//! { -//! let divisor_renamed = kani::internal::untracked_deref(& divisor); -//! let dividend_renamed = kani::internal::untracked_deref(& dividend); -//! kani::assert(divisor != 0, stringify! (divisor != 0)); -//! let result_kani_internal : u32 = kani::any_modifies(); -//! kani::assume( -//! (|result : & u32| *result <= dividend_renamed)(&result_kani_internal)); -//! std::mem::forget(divisor_renamed); -//! std::mem::forget(dividend_renamed); -//! result_kani_internal -//! } -//! -//! #[allow(dead_code)] -//! #[allow(unused_variables)] -//! #[kanitool::is_contract_generated(recursion_check)] -//! fn div_recursion_check_965916(dividend: u32, divisor: u32) -> u32 { -//! static mut REENTRY: bool = false; -//! -//! if unsafe { REENTRY } { -//! div_replace_b97df2(dividend, divisor) -//! } else { -//! unsafe { reentry = true }; -//! let result_kani_internal = div_check_b97df2(dividend, divisor); -//! unsafe { reentry = false }; -//! result_kani_internal +//! #[kanitool::recursion_check = "__kani_recursion_check_div"] +//! #[kanitool::checked_with = "__kani_check_div"] +//! #[kanitool::replaced_with = "__kani_replace_div"] +//! #[kanitool::inner_check = "__kani_modifies_div"] +//! fn div(dividend: u32, divisor: u32) -> u32 { +//! #[inline(never)] +//! #[kanitool::fn_marker = "kani_register_contract"] +//! pub const fn kani_register_contract T>(f: F) -> T { +//! kani::panic("internal error: entered unreachable code: ") +//! } +//! let kani_contract_mode = kani::internal::mode(); +//! match kani_contract_mode { +//! kani::internal::RECURSION_CHECK => { +//! #[kanitool::is_contract_generated(recursion_check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_recursion_check_div = +//! || -> u32 +//! { +//! #[kanitool::recursion_tracker] +//! static mut REENTRY: bool = false; +//! if unsafe { REENTRY } { +//! #[kanitool::is_contract_generated(replace)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_replace_div = +//! || -> u32 +//! { +//! kani::assert(divisor != 0, "divisor != 0"); +//! let result_kani_internal: u32 = kani::any_modifies(); +//! kani::assume(kani::internal::apply_closure(|result: &u32| +//! *result <= dividend, &result_kani_internal)); +//! result_kani_internal +//! }; +//! __kani_replace_div() +//! } else { +//! unsafe { REENTRY = true }; +//! #[kanitool::is_contract_generated(check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_check_div = +//! || -> u32 +//! { +//! kani::assume(divisor != 0); +//! let _wrapper_arg = (); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_div = +//! |_wrapper_arg| -> u32 { dividend / divisor }; +//! let result_kani_internal: u32 = +//! __kani_modifies_div(_wrapper_arg); +//! kani::assert(kani::internal::apply_closure(|result: &u32| +//! *result <= dividend, &result_kani_internal), +//! "|result : &u32| *result <= dividend"); +//! result_kani_internal +//! }; +//! let result_kani_internal = __kani_check_div(); +//! unsafe { REENTRY = false }; +//! result_kani_internal +//! } +//! }; +//! ; +//! kani_register_contract(__kani_recursion_check_div) +//! } +//! kani::internal::REPLACE => { +//! #[kanitool::is_contract_generated(replace)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_replace_div = +//! || -> u32 +//! { +//! kani::assert(divisor != 0, "divisor != 0"); +//! let result_kani_internal: u32 = kani::any_modifies(); +//! kani::assume(kani::internal::apply_closure(|result: &u32| +//! *result <= dividend, &result_kani_internal)); +//! result_kani_internal +//! }; +//! ; +//! kani_register_contract(__kani_replace_div) +//! } +//! kani::internal::SIMPLE_CHECK => { +//! #[kanitool::is_contract_generated(check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_check_div = +//! || -> u32 +//! { +//! kani::assume(divisor != 0); +//! let _wrapper_arg = (); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_div = +//! |_wrapper_arg| -> u32 { dividend / divisor }; +//! let result_kani_internal: u32 = +//! __kani_modifies_div(_wrapper_arg); +//! kani::assert(kani::internal::apply_closure(|result: &u32| +//! *result <= dividend, &result_kani_internal), +//! "|result : &u32| *result <= dividend"); +//! result_kani_internal +//! }; +//! ; +//! kani_register_contract(__kani_check_div) +//! } +//! _ => { dividend / divisor } //! } //! } //! ``` @@ -241,75 +288,136 @@ //! ``` //! //! This expands to -//! TODO: Update this //! //! ``` -//! #[kanitool::checked_with = "modify_recursion_check_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_check)] -//! fn modify_recursion_check_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); } +//! #[kanitool::recursion_check = "__kani_recursion_check_modify"] +//! #[kanitool::checked_with = "__kani_check_modify"] +//! #[kanitool::replaced_with = "__kani_replace_modify"] +//! #[kanitool::inner_check = "__kani_modifies_modify"] +//! fn modify(ptr: &mut u32) { +//! #[inline(never)] +//! #[kanitool::fn_marker = "kani_register_contract"] +//! pub const fn kani_register_contract T>(f: F) -> T { +//! kani::panic("internal error: entered unreachable code: ") +//! } +//! let kani_contract_mode = kani::internal::mode(); +//! match kani_contract_mode { +//! kani::internal::RECURSION_CHECK => { +//! #[kanitool::is_contract_generated(recursion_check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_recursion_check_modify = +//! || +//! { +//! #[kanitool::recursion_tracker] +//! static mut REENTRY: bool = false; +//! if unsafe { REENTRY } { +//! #[kanitool::is_contract_generated(replace)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_replace_modify = +//! || +//! { +//! 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(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal)); +//! kani::assume(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal)); +//! result_kani_internal +//! }; +//! __kani_replace_modify() +//! } else { +//! unsafe { REENTRY = true }; +//! #[kanitool::is_contract_generated(check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_check_modify = +//! || +//! { +//! kani::assume(*ptr < 100); +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let _wrapper_arg = (ptr as *const _,); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_modify = +//! |_wrapper_arg| { *ptr += 1; }; +//! let result_kani_internal: () = +//! __kani_modifies_modify(_wrapper_arg); +//! kani::assert(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! kani::assert(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! result_kani_internal +//! }; +//! let result_kani_internal = __kani_check_modify(); +//! unsafe { REENTRY = false }; +//! result_kani_internal +//! } +//! }; +//! ; +//! kani_register_contract(__kani_recursion_check_modify) +//! } +//! kani::internal::REPLACE => { +//! #[kanitool::is_contract_generated(replace)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_replace_modify = +//! || +//! { +//! 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(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal)); +//! kani::assume(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal)); +//! result_kani_internal +//! }; +//! ; +//! kani_register_contract(__kani_replace_modify) +//! } +//! kani::internal::SIMPLE_CHECK => { +//! #[kanitool::is_contract_generated(check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_check_modify = +//! || +//! { +//! kani::assume(*ptr < 100); +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let _wrapper_arg = (ptr as *const _,); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_modify = +//! |_wrapper_arg| { *ptr += 1; }; +//! let result_kani_internal: () = +//! __kani_modifies_modify(_wrapper_arg); +//! kani::assert(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! kani::assert(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! result_kani_internal +//! }; +//! ; +//! kani_register_contract(__kani_check_modify) +//! } +//! _ => { *ptr += 1; } +//! } //! } //! ``` From 7e411d6469bb50f82fad0966ab77804d90d2ba77 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 19 Jul 2024 17:08:38 -0700 Subject: [PATCH 10/18] Fix other reachability modes --- .../src/kani_middle/transform/contracts.rs | 24 +++++++++++-------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index b64b1b1177bd..5baeb86995d1 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -205,7 +205,7 @@ impl AnyModifiesPass { /// - Replace the non-used generated closures body with unreachable. /// 3. Replace the body of `kani_register_contract` by `kani::internal::run_contract_fn` to /// invoke the closure. -#[derive(Debug)] +#[derive(Debug, Default)] pub struct FunctionWithContractPass { /// Function that is being checked, if any. check_fn: Option, @@ -275,15 +275,19 @@ impl FunctionWithContractPass { /// Build the pass by collecting which functions we are stubbing and which ones we are /// verifying. pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> FunctionWithContractPass { - let harness = unit.harnesses.first().unwrap(); - let attrs = KaniAttributes::for_instance(tcx, *harness); - let check_fn = attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id); - let replace_fns: HashSet<_> = attrs - .interpret_stub_verified_attribute() - .iter() - .map(|(_, def_id, _)| *def_id) - .collect(); - FunctionWithContractPass { check_fn, replace_fns, unused_closures: Default::default() } + if let Some(harness) = unit.harnesses.first() { + let attrs = KaniAttributes::for_instance(tcx, *harness); + let check_fn = attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id); + let replace_fns: HashSet<_> = attrs + .interpret_stub_verified_attribute() + .iter() + .map(|(_, def_id, _)| *def_id) + .collect(); + FunctionWithContractPass { check_fn, replace_fns, unused_closures: Default::default() } + } else { + // Building the model for tests or public functions. + FunctionWithContractPass::default() + } } /// Functions with contract have the following structure: From ccf6a9d3eb2429f89940f7d62cdec649bf769784 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Sat, 20 Jul 2024 11:47:43 -0700 Subject: [PATCH 11/18] Include new functions in kani_core Note that we were missing the `write_any*` functions too --- library/kani/src/internal.rs | 5 +++ library/kani/src/lib.rs | 4 ++ library/kani_core/src/lib.rs | 83 ++++++++++++++++++++++++++++++++++++ 3 files changed, 92 insertions(+) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 19d56e0c6b66..595a5dd10fed 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -155,6 +155,11 @@ pub unsafe fn write_any_str(_s: *mut str) { #[doc(hidden)] #[allow(dead_code)] #[rustc_diagnostic_item = "KaniRunContract"] +#[crate::unstable( + feature = "function-contracts", + issue = "none", + reason = "internal function required to run contract closure" +)] fn run_contract_fn T>(func: F) -> T { func() } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 7487cc26b186..9ea47a8f35c2 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -21,6 +21,10 @@ #![feature(f16)] #![feature(f128)] +// Allow us to use `kani::` instead of `crate::`. +#[allow(unused_extern_crates)] +extern crate self as kani; + pub mod arbitrary; #[cfg(feature = "concrete_playback")] mod concrete_playback; diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 68a8e79658f1..d3fedf4fb442 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -60,6 +60,7 @@ macro_rules! kani_lib { /// such as core in rust's std library itself. /// /// TODO: Use this inside kani library so that we dont have to maintain two copies of the same intrinsics. +#[allow(clippy::crate_in_macro_def)] #[macro_export] macro_rules! kani_intrinsics { ($core:tt) => { @@ -294,6 +295,7 @@ macro_rules! kani_intrinsics { } pub mod internal { + use crate::kani::Arbitrary; /// Helper trait for code generation for `modifies` contracts. /// @@ -384,6 +386,87 @@ macro_rules! kani_intrinsics { #[doc(hidden)] #[rustc_diagnostic_item = "KaniInitContracts"] pub fn init_contracts() {} + + /// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object. + /// Only for use within function contracts and will not be replaced if the recursive or function stub + /// replace contracts are not used. + #[rustc_diagnostic_item = "KaniWriteAny"] + #[inline(never)] + #[doc(hidden)] + pub unsafe fn write_any(_pointer: *mut T) { + // This function should not be reacheable. + // Users must include `#[kani::recursion]` in any function contracts for recursive functions; + // otherwise, this might not be properly instantiate. We mark this as unreachable to make + // sure Kani doesn't report any false positives. + unreachable!() + } + + /// Fill in a slice with kani::any. + /// Intended as a post compilation replacement for write_any + #[rustc_diagnostic_item = "KaniWriteAnySlice"] + #[inline(always)] + pub unsafe fn write_any_slice(slice: *mut [T]) { + (*slice).fill_with(T::any) + } + + /// Fill in a pointer with kani::any. + /// Intended as a post compilation replacement for write_any + #[rustc_diagnostic_item = "KaniWriteAnySlim"] + #[inline(always)] + pub unsafe fn write_any_slim(pointer: *mut T) { + $core::ptr::write(pointer, T::any()) + } + + /// Fill in a str with kani::any. + /// Intended as a post compilation replacement for write_any. + /// Not yet implemented + #[rustc_diagnostic_item = "KaniWriteAnyStr"] + #[inline(always)] + pub unsafe fn write_any_str(_s: *mut str) { + //TODO: strings introduce new UB + //(*s).as_bytes_mut().fill_with(u8::any) + //TODO: String validation + unimplemented!("Kani does not support creating arbitrary `str`") + } + + /// Function that calls a closure used to implement contracts. + /// + /// In contracts, we cannot invoke the generated closures directly, instead, we call register + /// contract. This function is a no-op. However, in the reality, we do want to call the closure, + /// so we swap the register body by this function body. + #[doc(hidden)] + #[allow(dead_code)] + #[rustc_diagnostic_item = "KaniRunContract"] + fn run_contract_fn T>(func: F) -> T { + func() + } + + /// This is used for documentation's sake of which implementation to keep during contract verification. + #[doc(hidden)] + type Mode = u8; + + /// Keep the original body. + pub const ORIGINAL: Mode = 0; + + /// Run the check with recursion support. + pub const RECURSION_CHECK: Mode = 1; + + /// Run the simple check with no recursion support. + pub const SIMPLE_CHECK: Mode = 2; + + /// Stub the body with its contract. + pub const REPLACE: Mode = 3; + + /// This function is only used to help with contract instrumentation. + /// + /// It should be removed from the end user code during contract transformation. + /// By default, return the original code (used in concrete playback). + #[doc(hidden)] + #[inline(never)] + #[rustc_diagnostic_item = "KaniContractMode"] + pub const fn mode() -> Mode { + ORIGINAL + } } }; } From 9831c89ccf62d7609af059827e8de9a331891276 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 22 Jul 2024 10:23:55 -0700 Subject: [PATCH 12/18] Fix s2n-quic submodule --- tests/perf/s2n-quic | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 37335c196fb5..71f8d9f5aafb 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 37335c196fb5755dcbe2532e5a3820e46906d5ea +Subproject commit 71f8d9f5aafbf59f31ad85eeb7b4b67a7564a685 From e246bc989309ee2f6fc384a49e850df80d30f91f Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 22 Jul 2024 11:36:30 -0700 Subject: [PATCH 13/18] Remove `decouple_lifetime` function --- library/kani/src/internal.rs | 23 ----------------------- library/kani_core/src/lib.rs | 22 ---------------------- 2 files changed, 45 deletions(-) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 595a5dd10fed..6f90b171eb70 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -12,21 +12,11 @@ pub trait Pointer<'a> { /// Type of the pointed-to data type Inner: ?Sized; - /// Used for checking assigns contracts where we pass immutable references to the function. - /// - /// We're using a reference to self here, because the user can use just a plain function - /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it. - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner; - unsafe fn assignable(self) -> *mut Self::Inner; } impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - std::mem::transmute(*self) - } - unsafe fn assignable(self) -> *mut Self::Inner { std::mem::transmute(self as *const T) } @@ -35,11 +25,6 @@ impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { type Inner = T; - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - std::mem::transmute::<_, &&'a T>(self) - } - unsafe fn assignable(self) -> *mut Self::Inner { self as *mut T } @@ -47,10 +32,6 @@ impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { impl<'a, T: ?Sized> Pointer<'a> for *const T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - &**self as &'a T - } - unsafe fn assignable(self) -> *mut Self::Inner { std::mem::transmute(self) } @@ -58,10 +39,6 @@ impl<'a, T: ?Sized> Pointer<'a> for *const T { impl<'a, T: ?Sized> Pointer<'a> for *mut T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - &**self as &'a T - } - unsafe fn assignable(self) -> *mut Self::Inner { self } diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index d3fedf4fb442..e2d9e2c8156d 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -305,22 +305,12 @@ macro_rules! kani_intrinsics { /// Type of the pointed-to data type Inner; - /// Used for checking assigns contracts where we pass immutable references to the function. - /// - /// We're using a reference to self here, because the user can use just a plain function - /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it. - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner; - /// used for havocking on replecement of a `modifies` clause. unsafe fn assignable(self) -> &'a mut Self::Inner; } impl<'a, 'b, T> Pointer<'a> for &'b T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - $core::mem::transmute(*self) - } - #[allow(clippy::transmute_ptr_to_ref)] unsafe fn assignable(self) -> &'a mut Self::Inner { $core::mem::transmute(self as *const T) @@ -330,11 +320,6 @@ macro_rules! kani_intrinsics { impl<'a, 'b, T> Pointer<'a> for &'b mut T { type Inner = T; - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - $core::mem::transmute::<_, &&'a T>(self) - } - unsafe fn assignable(self) -> &'a mut Self::Inner { $core::mem::transmute(self) } @@ -342,9 +327,6 @@ macro_rules! kani_intrinsics { impl<'a, T> Pointer<'a> for *const T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - &**self as &'a T - } #[allow(clippy::transmute_ptr_to_ref)] unsafe fn assignable(self) -> &'a mut Self::Inner { @@ -354,10 +336,6 @@ macro_rules! kani_intrinsics { impl<'a, T> Pointer<'a> for *mut T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - &**self as &'a T - } - #[allow(clippy::transmute_ptr_to_ref)] unsafe fn assignable(self) -> &'a mut Self::Inner { $core::mem::transmute(self) From 5ad1b05638f766ca4b33114316b62b5871c811f0 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 22 Jul 2024 13:15:37 -0700 Subject: [PATCH 14/18] Test contract support to parameter patterns --- tests/kani/FunctionContracts/fn_params.rs | 72 +++++++++ .../FunctionContracts/receiver_contracts.rs | 147 ++++++++++++++++++ 2 files changed, 219 insertions(+) create mode 100644 tests/kani/FunctionContracts/fn_params.rs create mode 100644 tests/kani/FunctionContracts/receiver_contracts.rs diff --git a/tests/kani/FunctionContracts/fn_params.rs b/tests/kani/FunctionContracts/fn_params.rs new file mode 100644 index 000000000000..34b9d54771d6 --- /dev/null +++ b/tests/kani/FunctionContracts/fn_params.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Checks that function contracts work with different type of parameter expressions: +//! Source: +//! +//! Note: See `receiver_contracts` for receiver parameters. + +extern crate kani; +use std::convert::TryFrom; + +/// Dummy structure to check different patterns in contract. +#[derive(Copy, Clone, PartialEq, Eq, kani::Arbitrary)] +struct MyStruct { + c: char, + u: u32, +} + +/// Add contracts to ensure that all parameters are representing the same pair (char, u32). +#[kani::requires(val.u == second)] +#[kani::requires(val.u == tup_u)] +#[kani::requires(Ok(val.c) == char::try_from(first))] +#[kani::requires(val.c == tup_c)] +/// We need this extra clause due to . +#[kani::requires(char::try_from(first).is_ok())] +pub fn odd_parameters_eq( + [first, second]: [u32; 2], + (tup_c, tup_u): (char, u32), + val @ MyStruct { c: val_c, u }: MyStruct, +) { + assert_eq!(tup_c, char::try_from(first).unwrap()); + assert_eq!(tup_c, val_c); + + assert_eq!(tup_u, second); + assert_eq!(tup_u, u); + assert_eq!(val, MyStruct { c: val_c, u }); +} + +/// Similar to the function above, but with one requirement missing. +#[kani::requires(val.u == second)] +#[kani::requires(val.u == tup_u)] +#[kani::requires(Ok(val.c) == char::try_from(first))] +// MISSING: #[kani::requires(val.c == tup_c)] +// We need this extra clause due to . +#[kani::requires(char::try_from(first).is_ok())] +pub fn odd_parameters_eq_wrong( + [first, second]: [u32; 2], + (tup_c, tup_u): (char, u32), + val @ MyStruct { c: val_c, u }: MyStruct, +) { + assert_eq!(tup_c, char::try_from(first).unwrap()); + assert_eq!(tup_c, val_c); + + assert_eq!(tup_u, second); + assert_eq!(tup_u, u); + assert_eq!(val, MyStruct { c: val_c, u }); +} + +mod verify { + use super::*; + use kani::Arbitrary; + + #[kani::proof_for_contract(odd_parameters_eq)] + fn check_params() { + odd_parameters_eq(kani::any(), kani::any(), kani::any()) + } + + #[kani::should_panic] + #[kani::proof_for_contract(odd_parameters_eq_wrong)] + fn check_params_wrong() { + odd_parameters_eq_wrong(kani::any(), kani::any(), kani::any()) + } +} diff --git a/tests/kani/FunctionContracts/receiver_contracts.rs b/tests/kani/FunctionContracts/receiver_contracts.rs new file mode 100644 index 000000000000..3a70aff37475 --- /dev/null +++ b/tests/kani/FunctionContracts/receiver_contracts.rs @@ -0,0 +1,147 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Checks that function contracts work with different types of receivers. I.e.: +//! - &Self (i.e. &self) +//! - &mut Self (i.e &mut self) +//! - Box +//! - Rc +//! - Arc +//! - Pin

where P is one of the types above +//! Source: +// compile-flags: --edition 2021 + +#![feature(rustc_attrs)] + +extern crate kani; + +use std::boxed::Box; +use std::pin::Pin; +use std::rc::Rc; +use std::sync::Arc; + +/// Type representing a valid ASCII value going from `0..=128`. +#[derive(Copy, Clone, PartialEq, Eq)] +#[rustc_layout_scalar_valid_range_start(0)] +#[rustc_layout_scalar_valid_range_end(128)] +struct CharASCII(u8); + +impl kani::Arbitrary for CharASCII { + fn any() -> CharASCII { + let val = kani::any_where(|inner: &u8| *inner <= 128); + unsafe { CharASCII(val) } + } +} + +/// This type contains unsafe setter functions with the same contract but different type of +/// receivers. +impl CharASCII { + #[kani::modifies(&self.0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.0 == new_val)] + unsafe fn set_val(&mut self, new_val: u8) { + self.0 = new_val + } + + #[kani::modifies(&self.0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.0 == new_val)] + unsafe fn set_mut_ref(self: &mut Self, new_val: u8) { + self.0 = new_val + } + + #[kani::modifies(&self.as_ref().0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.as_ref().0 == new_val)] + unsafe fn set_box(mut self: Box, new_val: u8) { + self.as_mut().0 = new_val + } + + #[kani::modifies(&self.as_ref().0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.as_ref().0 == new_val)] + unsafe fn set_rc(mut self: Rc, new_val: u8) { + Rc::<_>::get_mut(&mut self).unwrap().0 = new_val + } + + #[kani::modifies(&self.as_ref().0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.as_ref().0 == new_val)] + unsafe fn set_arc(mut self: Arc, new_val: u8) { + Arc::<_>::get_mut(&mut self).unwrap().0 = new_val; + } + + #[kani::modifies(&self.0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.0 == new_val)] + unsafe fn set_pin(mut self: Pin<&mut Self>, new_val: u8) { + self.0 = new_val + } + + #[kani::modifies(&self.0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.0 == new_val)] + unsafe fn set_pin_box(mut self: Pin>, new_val: u8) { + self.0 = new_val + } +} + +mod verify { + use super::*; + use kani::Arbitrary; + + #[kani::proof_for_contract(CharASCII::set_val)] + fn check_set_val() { + let mut obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { obj.set_val(new_val) }; + } + + #[kani::proof_for_contract(CharASCII::set_mut_ref)] + fn check_mut_ref() { + let mut obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { obj.set_mut_ref(new_val) }; + } + + #[kani::proof_for_contract(CharASCII::set_box)] + fn check_box() { + let obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { Box::new(obj).set_box(new_val) }; + } + + #[kani::proof_for_contract(CharASCII::set_rc)] + fn check_rc() { + let obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { Rc::new(obj).set_rc(new_val) }; + } + + #[kani::proof_for_contract(CharASCII::set_arc)] + fn check_arc() { + let obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { Arc::new(obj).set_arc(new_val) }; + } + + #[kani::proof_for_contract(CharASCII::set_pin)] + fn check_pin() { + let mut obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { Pin::new(&mut obj).set_pin(new_val) }; + } + + #[kani::proof_for_contract(CharASCII::set_pin_box)] + fn check_pin_box() { + let obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { Pin::new(Box::new(obj)).set_pin_box(new_val) }; + } +} From e3d907f10aa1541dd773533942aa2dcc6f036db5 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 25 Jul 2024 15:45:17 -0700 Subject: [PATCH 15/18] Fix tests to include -Zfunction-contracts Also disable the Arc harness. --- tests/kani/FunctionContracts/fn_params.rs | 1 + tests/kani/FunctionContracts/receiver_contracts.rs | 8 ++++++++ 2 files changed, 9 insertions(+) diff --git a/tests/kani/FunctionContracts/fn_params.rs b/tests/kani/FunctionContracts/fn_params.rs index 34b9d54771d6..b485ddf2b32b 100644 --- a/tests/kani/FunctionContracts/fn_params.rs +++ b/tests/kani/FunctionContracts/fn_params.rs @@ -4,6 +4,7 @@ //! Source: //! //! Note: See `receiver_contracts` for receiver parameters. +// kani-flags: -Zfunction-contracts extern crate kani; use std::convert::TryFrom; diff --git a/tests/kani/FunctionContracts/receiver_contracts.rs b/tests/kani/FunctionContracts/receiver_contracts.rs index 3a70aff37475..5ca63f1558c3 100644 --- a/tests/kani/FunctionContracts/receiver_contracts.rs +++ b/tests/kani/FunctionContracts/receiver_contracts.rs @@ -9,6 +9,7 @@ //! - Pin

where P is one of the types above //! Source: // compile-flags: --edition 2021 +// kani-flags: -Zfunction-contracts #![feature(rustc_attrs)] @@ -63,6 +64,8 @@ impl CharASCII { Rc::<_>::get_mut(&mut self).unwrap().0 = new_val } + /// We cannot specify the counter today which is modified in this function. + /// #[kani::modifies(&self.as_ref().0)] #[kani::requires(new_val <= 128)] #[kani::ensures(|_| self.as_ref().0 == new_val)] @@ -121,6 +124,11 @@ mod verify { unsafe { Rc::new(obj).set_rc(new_val) }; } + /// This test currently fails because we cannot specify that the counter will be modified. + /// The counter is behind a pointer, but `Arc` only provide access to the data portion of + /// the allocation. + /// + #[cfg(arc_fails)] #[kani::proof_for_contract(CharASCII::set_arc)] fn check_arc() { let obj = CharASCII::any(); From 5d28e225408aaa48bf6260ef0ddddd63a6257bb7 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 25 Jul 2024 16:33:05 -0700 Subject: [PATCH 16/18] Fix regression after merge - Simplify the Pointer structure a bit more --- library/kani/src/internal.rs | 16 +++++++++------- library/kani_core/src/lib.rs | 30 +++++++++++++++--------------- 2 files changed, 24 insertions(+), 22 deletions(-) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 6f90b171eb70..a6f2291cea08 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -8,21 +8,22 @@ use std::ptr; /// /// We allow the user to provide us with a pointer-like object that we convert as needed. #[doc(hidden)] -pub trait Pointer<'a> { +pub trait Pointer { /// Type of the pointed-to data type Inner: ?Sized; + /// used for havocking on replecement of a `modifies` clause. unsafe fn assignable(self) -> *mut Self::Inner; } -impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { +impl Pointer for &T { type Inner = T; unsafe fn assignable(self) -> *mut Self::Inner { - std::mem::transmute(self as *const T) + self as *const T as *mut T } } -impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { +impl Pointer for &mut T { type Inner = T; unsafe fn assignable(self) -> *mut Self::Inner { @@ -30,14 +31,15 @@ impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { } } -impl<'a, T: ?Sized> Pointer<'a> for *const T { +impl Pointer for *const T { type Inner = T; + unsafe fn assignable(self) -> *mut Self::Inner { - std::mem::transmute(self) + self as *mut T } } -impl<'a, T: ?Sized> Pointer<'a> for *mut T { +impl Pointer for *mut T { type Inner = T; unsafe fn assignable(self) -> *mut Self::Inner { self diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index df026fce0ac1..d5ff9e3458ff 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -295,48 +295,48 @@ macro_rules! kani_intrinsics { } pub mod internal { + use crate::kani::Arbitrary; + use core::ptr; /// Helper trait for code generation for `modifies` contracts. /// /// We allow the user to provide us with a pointer-like object that we convert as needed. #[doc(hidden)] - pub trait Pointer<'a> { + pub trait Pointer { /// Type of the pointed-to data type Inner: ?Sized; /// used for havocking on replecement of a `modifies` clause. - unsafe fn assignable(self) -> &'a mut Self::Inner; + unsafe fn assignable(self) -> *mut Self::Inner; } - impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { + impl Pointer for &T { type Inner = T; - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - $core::mem::transmute(self as *const T) + unsafe fn assignable(self) -> *mut Self::Inner { + self as *const T as *mut T } } - impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { + impl Pointer for &mut T { type Inner = T; - unsafe fn assignable(self) -> &'a mut Self::Inner { - $core::mem::transmute(self) + unsafe fn assignable(self) -> *mut Self::Inner { + self as *mut T } } - impl<'a, T: ?Sized> Pointer<'a> for *const T { + impl Pointer for *const T { type Inner = T; unsafe fn assignable(self) -> *mut Self::Inner { - core::mem::transmute(self) + self as *mut T } } - impl<'a, T: ?Sized> Pointer<'a> for *mut T { + impl Pointer for *mut T { type Inner = T; - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - $core::mem::transmute(self) + unsafe fn assignable(self) -> *mut Self::Inner { + self } } From 3582b35426043aa5f5d18f827a6ccacbf164f484 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 26 Jul 2024 12:49:54 -0700 Subject: [PATCH 17/18] Fix contract for std constant functions Stable constant functions in the standard library can only invoke stable constant functions. Instead of adding the wrapper in the Kani library, expand it as an internal function which inherit the attributes of the function being annotated. --- .../src/kani_middle/transform/contracts.rs | 13 ++++++------ library/kani/src/internal.rs | 20 ++----------------- library/kani_core/src/lib.rs | 15 ++------------ .../src/sysroot/contracts/bootstrap.rs | 11 ++++++++-- 4 files changed, 19 insertions(+), 40 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 0a32099b88a0..2d1a34d49a2f 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -400,7 +400,6 @@ impl FunctionWithContractPass { /// 2. Replace `kani_register_contract` by the call to the closure. fn set_mode(&self, tcx: TyCtxt, body: Body, mode: ContractMode) -> Body { debug!(?mode, "set_mode"); - let mode_fn = find_fn_def(tcx, "KaniContractMode").unwrap(); let mut new_body = MutableBody::from(body); let (mut mode_call, ret, target) = new_body .blocks() @@ -410,16 +409,16 @@ impl FunctionWithContractPass { if let TerminatorKind::Call { func, target, destination, .. } = &bb.terminator.kind { let (callee, _) = func.ty(new_body.locals()).unwrap().kind().fn_def()?; - (callee == mode_fn).then(|| { - ( + let marker = KaniAttributes::for_def_id(tcx, callee.def_id()).fn_marker(); + if marker.is_some_and(|s| s.as_str() == "kani_contract_mode") { + return Some(( SourceInstruction::Terminator { bb: bb_idx }, destination.clone(), target.unwrap(), - ) - }) - } else { - None + )); + } } + None }) .unwrap(); diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index a6f2291cea08..56eddc657eb3 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -143,9 +143,9 @@ fn run_contract_fn T>(func: F) -> T { func() } -/// This is used for documentation's sake of which implementation to keep during contract verification. +/// This is used by contracts to select which version of the contract to use during codegen. #[doc(hidden)] -type Mode = u8; +pub type Mode = u8; /// Keep the original body. pub const ORIGINAL: Mode = 0; @@ -158,19 +158,3 @@ pub const SIMPLE_CHECK: Mode = 2; /// Stub the body with its contract. pub const REPLACE: Mode = 3; - -/// This function is only used to help with contract instrumentation. -/// -/// It should be removed from the end user code during contract transformation. -/// By default, return the original code (used in concrete playback). -#[doc(hidden)] -#[inline(never)] -#[crate::unstable( - feature = "function-contracts", - issue = 2652, - reason = "experimental support for function contracts" -)] -#[rustc_diagnostic_item = "KaniContractMode"] -pub const fn mode() -> Mode { - ORIGINAL -} diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index d5ff9e3458ff..11a3e70b416b 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -424,9 +424,9 @@ macro_rules! kani_intrinsics { func() } - /// This is used for documentation's sake of which implementation to keep during contract verification. + /// This is used by contracts to select which version of the contract to use during codegen. #[doc(hidden)] - type Mode = u8; + pub type Mode = u8; /// Keep the original body. pub const ORIGINAL: Mode = 0; @@ -439,17 +439,6 @@ macro_rules! kani_intrinsics { /// Stub the body with its contract. pub const REPLACE: Mode = 3; - - /// This function is only used to help with contract instrumentation. - /// - /// It should be removed from the end user code during contract transformation. - /// By default, return the original code (used in concrete playback). - #[doc(hidden)] - #[inline(never)] - #[rustc_diagnostic_item = "KaniContractMode"] - pub const fn mode() -> Mode { - ORIGINAL - } } }; } diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index a5b009563954..f7f150570ae3 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -48,10 +48,17 @@ impl<'a> ContractConditionsHandler<'a> { // This function gets replaced by `kani::internal::call_closure`. #[inline(never)] #[kanitool::fn_marker = "kani_register_contract"] - pub const fn kani_register_contract T>(f: F) -> T { + const fn kani_register_contract T>(f: F) -> T { unreachable!() } - let kani_contract_mode = kani::internal::mode(); + // Dummy function that we replace to pick the contract mode. + // By default, return ORIGINAL + #[inline(never)] + #[kanitool::fn_marker = "kani_contract_mode"] + const fn kani_contract_mode() -> kani::internal::Mode { + kani::internal::ORIGINAL + } + let kani_contract_mode = kani_contract_mode(); match kani_contract_mode { kani::internal::RECURSION_CHECK => { #recursion_closure; From 954ecbf090dd6d9775e9bf82af200eda9273c7bf Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 31 Jul 2024 16:27:32 -0700 Subject: [PATCH 18/18] Address PR comments --- .../codegen_cprover_gotoc/codegen/contract.rs | 14 ++--- kani-compiler/src/kani_middle/attributes.rs | 18 +++--- .../src/kani_middle/transform/contracts.rs | 50 +++++++---------- library/kani/src/internal.rs | 2 +- .../src/sysroot/contracts/bootstrap.rs | 2 +- .../kani_macros/src/sysroot/contracts/mod.rs | 55 +++++-------------- 6 files changed, 51 insertions(+), 90 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 4d6bab5ca2a3..b210b2c9333e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -17,8 +17,8 @@ impl<'tcx> GotocCtx<'tcx> { /// find or create the `AssignsContract` that needs to be enforced and attach it to the symbol /// for which it needs to be enforced. /// - /// 1. Gets the `#[kanitool::inner_check = "..."]` target, then resolves exactly one instance - /// of it. Panics if there are more or less than one instance. + /// 1. Gets the `#[kanitool::modifies_wrapper = "..."]` target, then resolves exactly one + /// instance of it. Panics if there are more or less than one instance. /// 2. The additional arguments for the inner checks are locations that may be modified. /// Add them to the list of CBMC's assigns. /// 3. Returns the mangled name of the symbol it attached the contract to. @@ -107,13 +107,13 @@ impl<'tcx> GotocCtx<'tcx> { None }) }; - let outside_check = if contract_attrs.has_recursion { - find_closure(instance, contract_attrs.recursion_check.as_str())? + let check_instance = if contract_attrs.has_recursion { + let recursion_check = find_closure(instance, contract_attrs.recursion_check.as_str())?; + find_closure(recursion_check, contract_attrs.checked_with.as_str())? } else { - instance + find_closure(instance, contract_attrs.checked_with.as_str())? }; - let check = find_closure(outside_check, contract_attrs.checked_with.as_str())?; - find_closure(check, contract_attrs.inner_check.as_str()) + find_closure(check_instance, contract_attrs.modifies_wrapper.as_str()) } /// Convert the Kani level contract into a CBMC level contract by creating a diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 6a1af75f3643..19cbba59cb83 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -54,12 +54,12 @@ enum KaniAttributeKind { /// Attribute on a function that was auto-generated from expanding a /// function contract. IsContractGenerated, - /// A function used as the inner code of a contract check. + /// A function with contract expanded to include the write set as arguments. /// /// Contains the original body of the contracted function. The signature is /// expanded with additional pointer arguments that are not used in the function /// but referenced by the `modifies` annotation. - InnerCheck, + ModifiesWrapper, /// Attribute used to mark contracts for functions with recursion. /// We use this attribute to properly instantiate `kani::any_modifies` in /// cases when recursion is present given our contracts instrumentation. @@ -92,7 +92,7 @@ impl KaniAttributeKind { | KaniAttributeKind::ReplacedWith | KaniAttributeKind::RecursionCheck | KaniAttributeKind::CheckedWith - | KaniAttributeKind::InnerCheck + | KaniAttributeKind::ModifiesWrapper | KaniAttributeKind::IsContractGenerated | KaniAttributeKind::DisableChecks => false, } @@ -134,7 +134,7 @@ pub struct ContractAttributes { /// The name of the contract replacement. pub replaced_with: Symbol, /// The name of the inner check used to modify clauses. - pub inner_check: Symbol, + pub modifies_wrapper: Symbol, } impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> { @@ -262,13 +262,13 @@ impl<'tcx> KaniAttributes<'tcx> { let recursion_check = self.attribute_value(KaniAttributeKind::RecursionCheck); let checked_with = self.attribute_value(KaniAttributeKind::CheckedWith); let replace_with = self.attribute_value(KaniAttributeKind::ReplacedWith); - let inner_check = self.attribute_value(KaniAttributeKind::InnerCheck); + let modifies_wrapper = self.attribute_value(KaniAttributeKind::ModifiesWrapper); let total = recursion_check .iter() .chain(&checked_with) .chain(&replace_with) - .chain(&inner_check) + .chain(&modifies_wrapper) .count(); if total != 0 && total != 4 { self.tcx.sess.dcx().err(format!( @@ -282,7 +282,7 @@ impl<'tcx> KaniAttributes<'tcx> { recursion_check: recursion_check?, checked_with: checked_with?, replaced_with: replace_with?, - inner_check: inner_check?, + modifies_wrapper: modifies_wrapper?, }) } @@ -373,7 +373,7 @@ impl<'tcx> KaniAttributes<'tcx> { } KaniAttributeKind::FnMarker | KaniAttributeKind::CheckedWith - | KaniAttributeKind::InnerCheck + | KaniAttributeKind::ModifiesWrapper | KaniAttributeKind::RecursionCheck | KaniAttributeKind::ReplacedWith => { self.attribute_value(kind); @@ -505,7 +505,7 @@ impl<'tcx> KaniAttributes<'tcx> { } KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated - | KaniAttributeKind::InnerCheck + | KaniAttributeKind::ModifiesWrapper | KaniAttributeKind::RecursionCheck | KaniAttributeKind::RecursionTracker | KaniAttributeKind::ReplacedWith => { diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 2d1a34d49a2f..71e06f5c49cd 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -78,31 +78,12 @@ impl TransformPass for AnyModifiesPass { impl AnyModifiesPass { /// Build the pass with non-extern function stubs. pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> AnyModifiesPass { - let item_fn_def = |item| { - let TyKind::RigidTy(RigidTy::FnDef(def, _)) = - rustc_internal::stable(tcx.type_of(item)).value.kind() - else { - unreachable!("Expected function, but found `{:?}`", tcx.def_path_str(item)) - }; - def - }; - let kani_any = - tcx.get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAny")).map(item_fn_def); - let kani_any_modifies = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies")) - .map(item_fn_def); - let kani_write_any = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAny")) - .map(item_fn_def); - let kani_write_any_slim = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnySlim")) - .map(item_fn_def); - let kani_write_any_slice = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnySlice")) - .map(item_fn_def); - let kani_write_any_str = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnyStr")) - .map(item_fn_def); + let kani_any = find_fn_def(tcx, "KaniAny"); + let kani_any_modifies = find_fn_def(tcx, "KaniAnyModifies"); + let kani_write_any = find_fn_def(tcx, "KaniWriteAny"); + let kani_write_any_slim = find_fn_def(tcx, "KaniWriteAnySlim"); + let kani_write_any_slice = find_fn_def(tcx, "KaniWriteAnySlice"); + let kani_write_any_str = find_fn_def(tcx, "KaniWriteAnyStr"); let target_fn = if let Some(harness) = unit.harnesses.first() { let attributes = KaniAttributes::for_instance(tcx, *harness); let target_fn = @@ -242,7 +223,7 @@ impl AnyModifiesPass { /// #[kanitool::recursion_check = "__kani_recursion_check_modify"] /// #[kanitool::checked_with = "__kani_check_modify"] /// #[kanitool::replaced_with = "__kani_replace_modify"] -/// #[kanitool::inner_check = "__kani_modifies_modify"] +/// #[kanitool::modifies_wrapper = "__kani_modifies_modify"] /// fn name_fn(ptr: &mut u32) { /// #[kanitool::fn_marker = "kani_register_contract"] /// pub const fn kani_register_contract T>(f: F) -> T { @@ -289,6 +270,8 @@ pub struct FunctionWithContractPass { /// are not to be used in this harness. /// In order to avoid bringing unnecessary logic, we clear their body. unused_closures: HashSet, + /// Cache KaniRunContract function used to implement contracts. + run_contract_fn: Option, } impl TransformPass for FunctionWithContractPass { @@ -318,8 +301,7 @@ impl TransformPass for FunctionWithContractPass { } else if KaniAttributes::for_instance(tcx, instance).fn_marker() == Some(Symbol::intern("kani_register_contract")) { - let run = Instance::resolve(find_fn_def(tcx, "KaniRunContract").unwrap(), args) - .unwrap(); + let run = Instance::resolve(self.run_contract_fn.unwrap(), args).unwrap(); (true, run.body().unwrap()) } else { // Not a contract annotated function @@ -357,9 +339,17 @@ impl FunctionWithContractPass { .iter() .map(|(_, def_id, _)| *def_id) .collect(); - FunctionWithContractPass { check_fn, replace_fns, unused_closures: Default::default() } + let run_contract_fn = find_fn_def(tcx, "KaniRunContract"); + assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function"); + FunctionWithContractPass { + check_fn, + replace_fns, + unused_closures: Default::default(), + run_contract_fn, + } } else { - // Building the model for tests or public functions. + // If reachability mode is PubFns or Tests, we just remove any contract logic. + // Note that in this path there is no proof harness. FunctionWithContractPass::default() } } diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 56eddc657eb3..68b15316b4c1 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -49,7 +49,7 @@ impl Pointer for *mut T { /// A way to break the ownerhip rules. Only used by contracts where we can /// guarantee it is done safely. /// TODO: Remove this! This is not safe. Users should be able to use `ptr::read` and `old` if -/// they really need to. +/// they really need to. See . #[inline(never)] #[doc(hidden)] #[rustc_diagnostic_item = "KaniUntrackedDeref"] diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index f7f150570ae3..8ad21e8a9c6b 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -41,7 +41,7 @@ impl<'a> ContractConditionsHandler<'a> { #[kanitool::recursion_check = #recursion_name] #[kanitool::checked_with = #check_name] #[kanitool::replaced_with = #replace_name] - #[kanitool::inner_check = #modifies_name] + #[kanitool::modifies_wrapper = #modifies_name] #vis #sig { // Dummy function used to force the compiler to capture the environment. // We cannot call closures inside constant functions. diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index ef7b88dc87d1..c7c7a4bb1598 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -10,7 +10,7 @@ //! implements a state machine in order to be able to handle multiple attributes //! on the same function correctly. //! -//! ## How the handling for `requires` and `ensures` works. +//! ## How the handling for `requires`, `modifies`, and `ensures` works. //! //! Our aim is to generate a "check" function that can be used to verify the //! validity of the contract and a "replace" function that can be used as a @@ -31,49 +31,20 @@ //! addition, we also want to make sure to support non-contract attributes on //! functions with contracts. //! -//! To this end we use a state machine with two states. The initial state is an "untouched" -//! function with possibly multiple contract attributes, none of which have been -//! expanded. When we expand the first (outermost) contract -//! attribute on such a function we re-emit the function with a few closures defined -//! in their body, which correspond to the "check", "recursive" and "replace" that enforce the -//! condition carried by the attribute currently being expanded. -//! -//! We also add new marker attributes to the original function to -//! advance the state machine. The re-emitted original meanwhile is decorated with -//! `kanitool::checked_with(name_of_generated_check_variable)` and an analogous -//! `kanittool::replaced_with` attribute also. -//! Each closure gets a `kanitool::is_contract_generated()` attributes. -//! The next contract attribute that -//! is expanded will detect the presence of these markers in the attributes of -//! the item and be able to determine their position in the state machine this -//! way. -//! -//! Subsequent run, will expand the existing definitions with the condition being processed. +//! To this end we generate attributes in a two-phase approach: initial and subsequent expansions. +//! +//! The initial expansion modifies the original function to contains all necessary instrumentation +//! contracts need to be analyzed. It will do the following: +//! 1. Annotate the function with extra `kanitool` attributes +//! 2. Generate closures for each contract processing scenario (recursive check, simple check, +//! replacement, and regular execution). +//! +//! Subsequent expansions will detect the existence of the extra `kanitool` attributes, +//! and they will only expand the body of the closures generated in the initial phase. //! //! Note: We place marker attributes at the bottom of the attribute stack (innermost), //! otherwise they would not be visible to the future macro expansions. //! -//! Below you can see a graphical rendering where boxes are states and each -//! arrow represents the expansion of a `requires` or `ensures` macro. -//! -//! ```plain -//! │ Start -//! ▼ -//! ┌───────────┐ -//! │ Untouched │ -//! │ Function │ -//! └─────┬─────┘ -//! │ -//! │ Annotate original + generate closures -//! │ -//! ▼ -//! ┌──────────┐ -//! │ Original │◄─┐ -//! └──┬───────┘ │ -//! │ │ Expand -//! └──────────┘ closures -//! ``` -//! //! ## Check closure //! //! Generates a `__kani__check` closure that assumes preconditions @@ -160,7 +131,7 @@ //! #[kanitool::recursion_check = "__kani_recursion_check_div"] //! #[kanitool::checked_with = "__kani_check_div"] //! #[kanitool::replaced_with = "__kani_replace_div"] -//! #[kanitool::inner_check = "__kani_modifies_div"] +//! #[kanitool::modifies_wrapper = "__kani_modifies_div"] //! fn div(dividend: u32, divisor: u32) -> u32 { //! #[inline(never)] //! #[kanitool::fn_marker = "kani_register_contract"] @@ -293,7 +264,7 @@ //! #[kanitool::recursion_check = "__kani_recursion_check_modify"] //! #[kanitool::checked_with = "__kani_check_modify"] //! #[kanitool::replaced_with = "__kani_replace_modify"] -//! #[kanitool::inner_check = "__kani_modifies_modify"] +//! #[kanitool::modifies_wrapper = "__kani_modifies_modify"] //! fn modify(ptr: &mut u32) { //! #[inline(never)] //! #[kanitool::fn_marker = "kani_register_contract"]