From e6db205df86679a1895412690b6c06a7f8a911b1 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 7 Sep 2023 14:56:43 -0700 Subject: [PATCH 01/26] Replacement basics --- kani-compiler/src/kani_middle/attributes.rs | 54 ++- library/kani_macros/src/lib.rs | 10 +- library/kani_macros/src/sysroot/contracts.rs | 346 +++++++++++++----- .../gcd_replacement_fail.expected | 20 + .../function-contract/gcd_replacement_fail.rs | 71 ++++ .../gcd_replacement_pass.expected | 1 + .../function-contract/gcd_replacement_pass.rs | 71 ++++ .../simple_replace_fail.expected | 3 + .../function-contract/simple_replace_fail.rs | 19 + .../simple_replace_pass.expected | 2 + .../function-contract/simple_replace_pass.rs | 17 + 11 files changed, 521 insertions(+), 93 deletions(-) create mode 100644 tests/expected/function-contract/gcd_replacement_fail.expected create mode 100644 tests/expected/function-contract/gcd_replacement_fail.rs create mode 100644 tests/expected/function-contract/gcd_replacement_pass.expected create mode 100644 tests/expected/function-contract/gcd_replacement_pass.rs create mode 100644 tests/expected/function-contract/simple_replace_fail.expected create mode 100644 tests/expected/function-contract/simple_replace_fail.rs create mode 100644 tests/expected/function-contract/simple_replace_pass.expected create mode 100644 tests/expected/function-contract/simple_replace_pass.rs diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index d1ef8fdf33e3..18d2261797ca 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -31,6 +31,7 @@ enum KaniAttributeKind { /// Attribute used to mark unstable APIs. Unstable, Unwind, + StubVerified, /// A harness, similar to [`Self::Proof`], but for checking a function /// contract, e.g. the contract check is substituted for the target function /// before the the verification runs. @@ -38,6 +39,7 @@ enum KaniAttributeKind { /// Attribute on a function with a contract that identifies the code /// implementing the check for this contract. CheckedWith, + ReplacedWith, /// Attribute on a function that was auto-generated from expanding a /// function contract. IsContractGenerated, @@ -52,8 +54,10 @@ impl KaniAttributeKind { | KaniAttributeKind::Solver | KaniAttributeKind::Stub | KaniAttributeKind::ProofForContract + | KaniAttributeKind::StubVerified | KaniAttributeKind::Unwind => true, KaniAttributeKind::Unstable + | KaniAttributeKind::ReplacedWith | KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => false, } @@ -134,10 +138,29 @@ impl<'tcx> KaniAttributes<'tcx> { } } + pub fn use_contract(&self) -> Vec> { + 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.sess.span_err( + attr.span, + format!( + "Sould not resolve replacement function {} because {e}", + name.as_str() + ), + ))?; + Ok((name, ok, attr.span)) + }) + .collect() + } + /// 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). - fn interpret_the_for_contract_attribute( + pub fn interpret_the_for_contract_attribute( &self, ) -> Option> { self.expect_maybe_one(KaniAttributeKind::ProofForContract).map(|target| { @@ -166,6 +189,11 @@ impl<'tcx> KaniAttributes<'tcx> { .map(|target| expect_key_string_value(self.tcx.sess, target)) } + pub fn replaced_with(&self) -> Option> { + self.expect_maybe_one(KaniAttributeKind::ReplacedWith) + .map(|target| expect_key_string_value(self.tcx.sess, target)) + } + /// Check that all attributes assigned to an item is valid. /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate /// the session and emit all errors found. @@ -223,7 +251,9 @@ impl<'tcx> KaniAttributes<'tcx> { } expect_single(self.tcx, kind, &attrs); } - KaniAttributeKind::CheckedWith => { + KaniAttributeKind::StubVerified => {} + KaniAttributeKind::CheckedWith + | KaniAttributeKind::ReplacedWith => { self.expect_maybe_one(kind) .map(|attr| expect_key_string_value(&self.tcx.sess, attr)); } @@ -345,12 +375,26 @@ impl<'tcx> KaniAttributes<'tcx> { }; harness.stubs.push(self.stub_for_relative_item(name, replacement_name)); } + KaniAttributeKind::StubVerified => { + for contract in self.use_contract() { + let Ok((name, def_id, _span)) = contract else { continue; }; + let Some(Ok(replacement_name)) = KaniAttributes::for_item(self.tcx, def_id).replaced_with() else { + // TODO report errors + continue; + }; + harness.stubs.push( + self.stub_for_relative_item(name, replacement_name)) + } + } KaniAttributeKind::Unstable => { // Internal attribute which shouldn't exist here. unreachable!() } - KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => { - todo!("Contract attributes are not supported on proofs") + KaniAttributeKind::CheckedWith + | KaniAttributeKind::IsContractGenerated + | KaniAttributeKind::ReplacedWith => { + // TODO better error + panic!("Contract attributes are not supported on proofs") } }; harness @@ -694,7 +738,7 @@ fn parse_paths(attr: &Attribute) -> Result, Span> { .iter() .map(|arg| match arg { NestedMetaItem::Lit(item) => Err(item.span), - NestedMetaItem::MetaItem(item) => parse_path(item).ok_or(item.span), + NestedMetaItem::MetaItem(item) => parse_path(&item).ok_or(item.span), }) .collect() } diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 3b4ea87636f3..2c6386334e76 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -162,6 +162,11 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::proof_for_contract(attr, item) } +#[proc_macro_attribute] +pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::stub_verified(attr, item) +} + /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. #[cfg(kani_sysroot)] @@ -170,7 +175,9 @@ mod sysroot { mod contracts; - pub use contracts::{ensures, proof_for_contract, requires}; + pub use contracts::{ + ensures, proof_for_contract, requires, stub_verified, + }; use super::*; @@ -344,4 +351,5 @@ mod regular { no_op!(requires); no_op!(ensures); no_op!(proof_for_contract); + no_op!(stub_verified); } diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 856f25b7d597..1b2ae894e061 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -120,7 +120,16 @@ where && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) } -/// Classifies the state a function is in the contract handling pipeline. +macro_rules! swapped { + ($src:expr, $target:expr, $code:expr) => {{ + std::mem::swap($src, $target); + let result = $code; + std::mem::swap($src, $target); + result + }}; +} + +/// 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. @@ -131,6 +140,9 @@ enum ContractFunctionState { /// 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, } impl ContractFunctionState { @@ -144,11 +156,15 @@ impl ContractFunctionState { lst.span().unwrap().error(format!("{e}")).emit(); } Ok(ident) => { - if ident.to_string() == "check" { - return Some(Self::Check); - } else { + let ident_str = ident.to_string(); + return match ident_str.as_str() { + "check" => Some(Self::Check), + "replace" => Some(Self::Replace), + _ => { lst.span().unwrap().error("Expected `check` ident").emit(); + None } + }; } } } @@ -160,6 +176,97 @@ impl ContractFunctionState { } None } + + fn emit_tag_attr(self) -> bool { + matches!(self, ContractFunctionState::Untouched) + } + + /// This function decides whether we will be emitting a check function, a + /// replace function or both and emit a header into `output` if necessary. + /// + /// The return of this function essentially configures all the later parts + /// of code generation and is structured as follows: + /// `Some((Some((replace_function_name, use_dummy_function)), + /// Some(check_function_name)))`. Either function name being present tells + /// the codegen that that type of function should be emitted with the + /// respective name. `use_dummy_function` indicates whether we should use + /// the body of this function (`false`) or `kani::any` (`true`) as the + /// nested body of the replace function. `kani::any` is only used when we + /// generate a replace function for the first time. + /// + /// The following is going to happen depending on the state of `self` + /// + /// - On [`ContractFunctionState::Original`] we return an overall [`None`] + /// indicating to short circuit the code generation. + /// - On [`ContractFunctionState::Replace`] and + /// [`ContractFunctionState::Check`] we return [`Some`] for one of the + /// tuple fields, indicating that only this type of function should be + /// emitted. + /// - On [`ContractFunctionState::Untouched`] we return [`Some`] for both + /// tuple fields, indicating that both functions need to be emitted. We + /// also emit the original function with the `checked_with` and + /// `replaced_with` attributes added. + /// + /// The only reason the `item_fn` is mutable is I'm using `std::mem::swap` + /// to avoid making copies. + fn prepare_header( + self, + item_fn: &mut ItemFn, + output: &mut TokenStream2, + a_short_hash: u64, + ) -> Option<(Option<(Ident, bool)>, Option)> { + match self { + ContractFunctionState::Untouched => { + // We are the first time a contract is handled on this function, so + // we're responsible for + // + // 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 + + let check_fn_name = + identifier_for_generated_function(item_fn, "check", a_short_hash); + let replace_fn_name = + identifier_for_generated_function(item_fn, "replace", a_short_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 check_fn_name_str = + syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); + + // 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`. + // + // We're emitting the original here but the same applies later when we + // emit the check function. + let mut attrs = vec![]; + swapped!(&mut item_fn.attrs, &mut attrs, { + output.extend(quote!( + #(#attrs)* + #[kanitool::inner_check = #check_fn_name_str] + #[kanitool::replaced_with = #replace_fn_name_str] + #item_fn + )); + }); + Some((Some((replace_fn_name, true)), Some(check_fn_name))) + } + ContractFunctionState::Original | Self::ReplaceDummy => None, + ContractFunctionState::Check => Some((None, Some(item_fn.sig.ident.clone()))), + ContractFunctionState::Replace => Some((Some((item_fn.sig.ident.clone(), false)), None)), + } + } } /// A visitor which injects a copy of the token stream it holds before every @@ -218,7 +325,7 @@ impl VisitMut for PostconditionInjector { /// - Creates new names for them; /// - Replaces all occurrences of those idents in `attrs` with the new names and; /// - Returns the mapping of old names to new names. -fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap { +fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap { let mut arg_ident_collector = ArgumentIdentCollector::new(); arg_ident_collector.visit_signature(&sig); @@ -237,6 +344,110 @@ fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap< arg_idents } +struct ContractConditionsHandler<'a> { + condition_type: ContractConditionsType, + attr: Expr, + body: Block, +} + +enum ContractConditionsType { + Requires, + Ensures { arg_idents: HashMap }, +} + +impl ContractConditionsType { + fn new_ensures(sig: &Signature, attr: &mut Expr) -> Self { + + let arg_idents = rename_argument_occurrences(sig, attr); + + ContractConditionsType::Ensures { arg_idents } + } +} + +impl<'a> ContractConditionsHandler<'a> { + fn new( + is_requires: bool, + mut attr: Expr, + fn_sig: &Signature, + fn_body: Block, + ) -> Self { + let condition_type = if is_requires { + ContractConditionsType::Requires + } else { + ContractConditionsType::new_ensures(sig, attr) + }; + + Self { condition_type, attr, body: fn_body } + } + + fn make_check_body(&self) -> TokenStream2 { + let attr = &self.attr; + let call_to_prior = &self.body; + match &self.condition_type { + ContractConditionsType::Requires => quote!( + kani::assume(#attr); + #call_to_prior + ), + ContractConditionsType::Ensures => { + let arg_names = arg_idents.values(); + let arg_names_2 = arg_names.clone(); + let arg_idents = arg_idents.keys(); + let attr = &self.attr; + + // The code that enforces the postconditions and cleans up the shallow + // argument copies (with `mem::forget`). + let exec_postconditions = quote!( + kani::assert(#attr, stringify!(#attr)); + #(std::mem::forget(#arg_names_2);)* + ); + + // We make a copy here because we'll modify it. Technically not + // necessary but could lead to weird results if + // `make_replace_body` were called after this if we modified in + // place. + let mut call = call_to_prior.clone(); + + let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); + inject_conditions.visit_block_mut(&mut call); + quote!( + #(let #arg_names = kani::untracked_deref(&#arg_idents);)* + let result = #call; + #exec_postconditions + result + ) + } + } + } + + fn make_replace_body(&self, sig: &Signature, use_dummy_fn_call: bool) -> TokenStream2 { + let attr = &self.attr; + let call_to_prior = if use_dummy_fn_call { + quote!(kani::any()) + } else { + self.body.to_token_stream() + }; + match &self.condition_type { + ContractConditionsType::Requires => quote!( + kani::assert(#attr, stringify!(#attr)); + #call_to_prior + ), + ContractConditionsType::Ensures { arg_idents } => { + let arg_names = arg_idents.values(); + let arg_values = arg_idents.keys(); + quote!( + #(let #arg_names = kani::untracked_deref(&#arg_values);)* + let result = #call_to_prior; + kani::assume(#attr); + result + ) + } + } + } +} + +} + + /// The main meat of handling requires/ensures contracts. /// /// Generates a `check__` function that assumes preconditions @@ -293,12 +504,12 @@ fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap< /// ``` fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { let attr_copy = proc_macro2::TokenStream::from(attr.clone()); - let mut attr = parse_macro_input!(attr as Expr); + let attr = parse_macro_input!(attr as Expr); let mut output = proc_macro2::TokenStream::new(); let a_short_hash = short_hash_of_token_stream(&item); - let item_fn = &mut parse_macro_input!(item as ItemFn); + let mut item_fn = parse_macro_input!(item as ItemFn); // If we didn't find any other contract handling related attributes we // assume this function has not been touched by a contract before. @@ -308,108 +519,68 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) .find_map(ContractFunctionState::from_attribute) .unwrap_or(ContractFunctionState::Untouched); - if matches!(function_state, ContractFunctionState::Original) { + let Some((emit_replace, emit_check)) = + function_state.prepare_header(&mut item_fn, &mut output, a_short_hash) + else { // 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 outselves unchanged. return item_fn.into_token_stream().into(); - } + }; - let attrs = std::mem::replace(&mut item_fn.attrs, vec![]); - - if matches!(function_state, ContractFunctionState::Untouched) { - // We are the first time a contract is handled on this function, so - // we're responsible for: - // 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. - - let check_fn_name = identifier_for_generated_function(item_fn, "check", a_short_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 check_fn_name_str = syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); - - // 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 attribuites and can use them to determine - // `function_state`. - // - // We're emitting the original here but the same applies later when we - // emit the check function. - output.extend(quote!( - #(#attrs)* - #[kanitool::checked_with = #check_fn_name_str] - #item_fn + let ItemFn { attrs, vis: _, mut sig, block } = item_fn; + + let handler = ContractConditionsHandler::new(is_requires, attr, &sig, *block); - #[allow(dead_code)] - #[allow(unused_variables)] + let emit_common_header = |output: &mut TokenStream2| { + if function_state.emit_tag_attr() { + output.extend(quote!( + #[allow(dead_code, unused_variables)] )); - item_fn.sig.ident = check_fn_name; } - - let call_to_prior = &mut item_fn.block; - - let check_body = if is_requires { - quote!( - kani::assume(#attr); - #call_to_prior - ) - } else { - let arg_idents = rename_argument_occurences(&item_fn.sig, &mut attr); - - let arg_copy_names = arg_idents.values(); - let also_arg_copy_names = arg_copy_names.clone(); - let arg_idents = arg_idents.keys(); - - // The code that enforces the postconditions and cleans up the shallow - // argument copies (with `mem::forget`). - let exec_postconditions = quote!( - kani::assert(#attr, stringify!(#attr_copy)); - #(std::mem::forget(#also_arg_copy_names);)* - ); - - let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); - inject_conditions.visit_block_mut(&mut *call_to_prior); - - quote!( - #(let #arg_copy_names = kani::untracked_deref(&#arg_idents);)* - let result = #call_to_prior; - #exec_postconditions - result - ) + output.extend(attrs.iter().flat_map(Attribute::to_token_stream)); }; - let sig = &item_fn.sig; + if let Some((replace_name, dummy)) = emit_replace { + emit_common_header(&mut output); + + if 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. + output.extend(quote!(#[kanitool::is_contract_generated(replace)])); + } + + let body = handler.make_replace_body(&sig, dummy); - // Prepare emitting the check function by emitting the rest of the - // attributes. + sig.ident = replace_name; + + // Finally emit the check function itself. output.extend(quote!( - #(#attrs)* + #sig { + #body + } )); + } - if matches!(function_state, ContractFunctionState::Untouched) { + if let Some(check_name) = emit_check { + emit_common_header(&mut output); + + if 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. output.extend(quote!(#[kanitool::is_contract_generated(check)])); } - - // Finally emit the check function itself. + let body = handler.make_check_body(); + sig.ident = check_name; output.extend(quote!( #sig { - #check_body + #body } - )); + )) + } + output.into() } @@ -436,4 +607,5 @@ macro_rules! passthrough { } } -passthrough!(proof_for_contract, true); + +passthrough!(stub_verified, false); diff --git a/tests/expected/function-contract/gcd_replacement_fail.expected b/tests/expected/function-contract/gcd_replacement_fail.expected new file mode 100644 index 000000000000..88df38788eb0 --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_fail.expected @@ -0,0 +1,20 @@ +Frac::check_equals.assertion\ + - Status: FAILURE\ + - Description: "attempt to calculate the remainder with a divisor of zero"\ + gcd_replacement_fail.rs:50:20 in function Frac::check_equals + +Frac::check_equals.assertion\ + - Status: FAILURE\ + - Description: "assertion failed: self.den % f2.den == 0"\ + gcd_replacement_fail.rs:50:9 in function Frac::check_equals + +Frac::check_equals.assertion\ + - Status: FAILURE\ + - Description: "assertion failed: gcd1 == gcd2"\ + gcd_replacement_fail.rs:53:9 in function Frac::check_equals + +Failed Checks: attempt to calculate the remainder with a divisor of zero +Failed Checks: assertion failed: self.den % f2.den == 0 +Failed Checks: assertion failed: gcd1 == gcd2 + +VERIFICATION:- FAILED \ No newline at end of file diff --git a/tests/expected/function-contract/gcd_replacement_fail.rs b/tests/expected/function-contract/gcd_replacement_fail.rs new file mode 100644 index 000000000000..b73d20cba46a --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_fail.rs @@ -0,0 +1,71 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + loop { + let res = max % min; + if res == 0 { + return min; + } + + max = min; + min = res; + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof] +#[kani::stub_verified(gcd)] +fn main() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/gcd_replacement_pass.expected b/tests/expected/function-contract/gcd_replacement_pass.expected new file mode 100644 index 000000000000..880f00714b32 --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_pass.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/gcd_replacement_pass.rs b/tests/expected/function-contract/gcd_replacement_pass.rs new file mode 100644 index 000000000000..86fd59ad5618 --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_pass.rs @@ -0,0 +1,71 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + loop { + let res = max % min; + if res == 0 { + return min; + } + + max = min; + min = res; + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof] +#[kani::stub_verified(gcd)] +fn main() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/simple_replace_fail.expected b/tests/expected/function-contract/simple_replace_fail.expected new file mode 100644 index 000000000000..575a73ce9c26 --- /dev/null +++ b/tests/expected/function-contract/simple_replace_fail.expected @@ -0,0 +1,3 @@ +main.assertion + - Status: FAILURE + - Description: ""contract doesn't guarantee equality"" \ No newline at end of file diff --git a/tests/expected/function-contract/simple_replace_fail.rs b/tests/expected/function-contract/simple_replace_fail.rs new file mode 100644 index 000000000000..afa3265659f4 --- /dev/null +++ b/tests/expected/function-contract/simple_replace_fail.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::requires(divisor != 0)] +#[kani::ensures(result <= dividend)] +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + + + +#[kani::proof] +#[kani::stub_verified(div)] +fn main() { + let _ = Box::new(()); + + assert!(div(9, 4) == 2, "contract doesn't guarantee equality"); +} diff --git a/tests/expected/function-contract/simple_replace_pass.expected b/tests/expected/function-contract/simple_replace_pass.expected new file mode 100644 index 000000000000..f1d50a57ff31 --- /dev/null +++ b/tests/expected/function-contract/simple_replace_pass.expected @@ -0,0 +1,2 @@ + +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/simple_replace_pass.rs b/tests/expected/function-contract/simple_replace_pass.rs new file mode 100644 index 000000000000..0f1367528b72 --- /dev/null +++ b/tests/expected/function-contract/simple_replace_pass.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::requires(divisor != 0)] +#[kani::ensures(result <= dividend)] +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[kani::proof] +#[kani::stub_verified(div)] +fn main() { + let _ = Box::new(()); + + assert!(div(9, 1) != 10, "contract guarantees smallness"); +} From ff344b6b9df79311d27002b3ea05bdace3b947b1 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 7 Sep 2023 15:02:39 -0700 Subject: [PATCH 02/26] Fixing errors and formatting --- kani-compiler/src/kani_middle/attributes.rs | 71 +++++++++++-------- library/kani_macros/src/lib.rs | 4 +- library/kani_macros/src/sysroot/contracts.rs | 57 ++++++--------- .../function-contract/simple_replace_fail.rs | 2 - 4 files changed, 64 insertions(+), 70 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 18d2261797ca..624f01af71e7 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -19,7 +19,7 @@ use strum_macros::{AsRefStr, EnumString}; use tracing::{debug, trace}; -use super::resolve::{self, resolve_fn}; +use super::resolve::{self, resolve_fn, ResolveError}; #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)] #[strum(serialize_all = "snake_case")] @@ -139,19 +139,21 @@ impl<'tcx> KaniAttributes<'tcx> { } pub fn use_contract(&self) -> Vec> { - self.map.get(&KaniAttributeKind::StubVerified).map_or([].as_slice(), Vec::as_slice) + 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.sess.span_err( - attr.span, - format!( - "Sould not resolve replacement function {} because {e}", - name.as_str() - ), - ))?; + let ok = self.resolve_sibling(name.as_str()).map_err(|e| { + self.tcx.sess.span_err( + attr.span, + format!( + "Sould not resolve replacement function {} because {e}", + name.as_str() + ), + ) + })?; Ok((name, ok, attr.span)) }) .collect() @@ -165,20 +167,17 @@ impl<'tcx> KaniAttributes<'tcx> { ) -> Option> { self.expect_maybe_one(KaniAttributeKind::ProofForContract).map(|target| { let name = expect_key_string_value(self.tcx.sess, target)?; - let resolved = resolve_fn( - self.tcx, - self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(), - name.as_str(), - ); - resolved.map(|ok| (name, ok, target.span)).map_err(|resolve_err| { - self.tcx.sess.span_err( - target.span, - format!( - "Failed to resolve replacement function {} because {resolve_err}", - name.as_str() - ), - ) - }) + self.resolve_sibling(name.as_str()).map(|ok| (name, ok, target.span)).map_err( + |resolve_err| { + self.tcx.sess.span_err( + target.span, + format!( + "Failed to resolve replacement function {} because {resolve_err}", + name.as_str() + ), + ) + }, + ) }) } @@ -194,6 +193,14 @@ impl<'tcx> KaniAttributes<'tcx> { .map(|target| expect_key_string_value(self.tcx.sess, target)) } + fn resolve_sibling(&self, path_str: &str) -> Result> { + resolve_fn( + self.tcx, + self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(), + path_str, + ) + } + /// Check that all attributes assigned to an item is valid. /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate /// the session and emit all errors found. @@ -252,8 +259,7 @@ impl<'tcx> KaniAttributes<'tcx> { expect_single(self.tcx, kind, &attrs); } KaniAttributeKind::StubVerified => {} - KaniAttributeKind::CheckedWith - | KaniAttributeKind::ReplacedWith => { + KaniAttributeKind::CheckedWith | KaniAttributeKind::ReplacedWith => { self.expect_maybe_one(kind) .map(|attr| expect_key_string_value(&self.tcx.sess, attr)); } @@ -377,13 +383,16 @@ impl<'tcx> KaniAttributes<'tcx> { } KaniAttributeKind::StubVerified => { for contract in self.use_contract() { - let Ok((name, def_id, _span)) = contract else { continue; }; - let Some(Ok(replacement_name)) = KaniAttributes::for_item(self.tcx, def_id).replaced_with() else { + let Ok((name, def_id, _span)) = contract else { + continue; + }; + let Some(Ok(replacement_name)) = + KaniAttributes::for_item(self.tcx, def_id).replaced_with() + else { // TODO report errors continue; }; - harness.stubs.push( - self.stub_for_relative_item(name, replacement_name)) + harness.stubs.push(self.stub_for_relative_item(name, replacement_name)) } } KaniAttributeKind::Unstable => { diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 2c6386334e76..93546e3fd7d6 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -175,9 +175,7 @@ mod sysroot { mod contracts; - pub use contracts::{ - ensures, proof_for_contract, requires, stub_verified, - }; + pub use contracts::{ensures, proof_for_contract, requires, stub_verified}; use super::*; diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 1b2ae894e061..e42202bd16ad 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -161,9 +161,9 @@ impl ContractFunctionState { "check" => Some(Self::Check), "replace" => Some(Self::Replace), _ => { - lst.span().unwrap().error("Expected `check` ident").emit(); + lst.span().unwrap().error("Expected `check` ident").emit(); None - } + } }; } } @@ -206,7 +206,7 @@ impl ContractFunctionState { /// tuple fields, indicating that both functions need to be emitted. We /// also emit the original function with the `checked_with` and /// `replaced_with` attributes added. - /// + /// /// The only reason the `item_fn` is mutable is I'm using `std::mem::swap` /// to avoid making copies. fn prepare_header( @@ -264,7 +264,9 @@ impl ContractFunctionState { } ContractFunctionState::Original | Self::ReplaceDummy => None, ContractFunctionState::Check => Some((None, Some(item_fn.sig.ident.clone()))), - ContractFunctionState::Replace => Some((Some((item_fn.sig.ident.clone(), false)), None)), + ContractFunctionState::Replace => { + Some((Some((item_fn.sig.ident.clone(), false)), None)) + } } } } @@ -357,7 +359,6 @@ enum ContractConditionsType { impl ContractConditionsType { fn new_ensures(sig: &Signature, attr: &mut Expr) -> Self { - let arg_idents = rename_argument_occurrences(sig, attr); ContractConditionsType::Ensures { arg_idents } @@ -365,12 +366,7 @@ impl ContractConditionsType { } impl<'a> ContractConditionsHandler<'a> { - fn new( - is_requires: bool, - mut attr: Expr, - fn_sig: &Signature, - fn_body: Block, - ) -> Self { + fn new(is_requires: bool, mut attr: Expr, fn_sig: &Signature, fn_body: Block) -> Self { let condition_type = if is_requires { ContractConditionsType::Requires } else { @@ -421,11 +417,8 @@ impl<'a> ContractConditionsHandler<'a> { fn make_replace_body(&self, sig: &Signature, use_dummy_fn_call: bool) -> TokenStream2 { let attr = &self.attr; - let call_to_prior = if use_dummy_fn_call { - quote!(kani::any()) - } else { - self.body.to_token_stream() - }; + let call_to_prior = + if use_dummy_fn_call { quote!(kani::any()) } else { self.body.to_token_stream() }; match &self.condition_type { ContractConditionsType::Requires => quote!( kani::assert(#attr, stringify!(#attr)); @@ -445,9 +438,6 @@ impl<'a> ContractConditionsHandler<'a> { } } -} - - /// The main meat of handling requires/ensures contracts. /// /// Generates a `check__` function that assumes preconditions @@ -536,10 +526,10 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) let emit_common_header = |output: &mut TokenStream2| { if function_state.emit_tag_attr() { - output.extend(quote!( - #[allow(dead_code, unused_variables)] - )); - } + output.extend(quote!( + #[allow(dead_code, unused_variables)] + )); + } output.extend(attrs.iter().flat_map(Attribute::to_token_stream)); }; @@ -557,24 +547,24 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) sig.ident = replace_name; // Finally emit the check function itself. - output.extend(quote!( - #sig { - #body - } - )); + output.extend(quote!( + #sig { + #body + } + )); } if let Some(check_name) = emit_check { emit_common_header(&mut output); if 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. - output.extend(quote!(#[kanitool::is_contract_generated(check)])); - } + // If it's the first time we also emit this marker. Again, order is + // important so this happens as the last emitted attribute. + output.extend(quote!(#[kanitool::is_contract_generated(check)])); + } let body = handler.make_check_body(); sig.ident = check_name; - output.extend(quote!( + output.extend(quote!( #sig { #body } @@ -607,5 +597,4 @@ macro_rules! passthrough { } } - passthrough!(stub_verified, false); diff --git a/tests/expected/function-contract/simple_replace_fail.rs b/tests/expected/function-contract/simple_replace_fail.rs index afa3265659f4..e2d65a6aeee7 100644 --- a/tests/expected/function-contract/simple_replace_fail.rs +++ b/tests/expected/function-contract/simple_replace_fail.rs @@ -8,8 +8,6 @@ fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } - - #[kani::proof] #[kani::stub_verified(div)] fn main() { From 16d6e507ab3af60aff23d6cdbb0615100eadf3c5 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 7 Sep 2023 15:48:15 -0700 Subject: [PATCH 03/26] Documentation and general fixes --- kani-compiler/src/kani_middle/attributes.rs | 32 +++++--- library/kani_macros/src/lib.rs | 15 ++++ library/kani_macros/src/sysroot/contracts.rs | 79 ++++++++++++------- .../gcd_replacement_fail.expected | 17 ++-- .../gcd_replacement_pass.expected | 2 +- .../simple_replace_fail.expected | 6 +- .../function-contract/simple_replace_fail.rs | 2 - .../simple_replace_pass.expected | 3 +- .../function-contract/simple_replace_pass.rs | 2 - 9 files changed, 101 insertions(+), 57 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 624f01af71e7..d67d17ce7205 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -138,7 +138,7 @@ impl<'tcx> KaniAttributes<'tcx> { } } - pub fn use_contract(&self) -> Vec> { + fn use_contract(&self) -> Vec> { self.map .get(&KaniAttributeKind::StubVerified) .map_or([].as_slice(), Vec::as_slice) @@ -162,7 +162,7 @@ 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 fn interpret_the_for_contract_attribute( + fn interpret_the_for_contract_attribute( &self, ) -> Option> { self.expect_maybe_one(KaniAttributeKind::ProofForContract).map(|target| { @@ -172,7 +172,7 @@ impl<'tcx> KaniAttributes<'tcx> { self.tcx.sess.span_err( target.span, format!( - "Failed to resolve replacement function {} because {resolve_err}", + "Failed to resolve checking function {} because {resolve_err}", name.as_str() ), ) @@ -181,18 +181,28 @@ impl<'tcx> KaniAttributes<'tcx> { }) } - /// Extract the name of the sibling function this contract is checked with - /// (if any). + /// 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)) } + /// Extract the name of the sibling function this function's contract is + /// stubbed as (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 replaced_with(&self) -> Option> { self.expect_maybe_one(KaniAttributeKind::ReplacedWith) .map(|target| expect_key_string_value(self.tcx.sess, target)) } + /// Resolve a function that is known to reside in the same module as the one + /// these attributes belong to (`self.item`). fn resolve_sibling(&self, path_str: &str) -> Result> { resolve_fn( self.tcx, @@ -258,7 +268,9 @@ impl<'tcx> KaniAttributes<'tcx> { } expect_single(self.tcx, kind, &attrs); } - KaniAttributeKind::StubVerified => {} + 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)); @@ -389,7 +401,10 @@ impl<'tcx> KaniAttributes<'tcx> { let Some(Ok(replacement_name)) = KaniAttributes::for_item(self.tcx, def_id).replaced_with() else { - // TODO report errors + self.tcx.sess.span_err( + self.tcx.def_span(self.item), + format!("Invalid `{}` attribute format", kind.as_ref()), + ); continue; }; harness.stubs.push(self.stub_for_relative_item(name, replacement_name)) @@ -402,8 +417,7 @@ impl<'tcx> KaniAttributes<'tcx> { KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated | KaniAttributeKind::ReplacedWith => { - // TODO better error - panic!("Contract attributes are not supported on proofs") + self.tcx.sess.span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref())); } }; harness diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 93546e3fd7d6..15cd9b5f4c3f 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -162,6 +162,21 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::proof_for_contract(attr, item) } +/// `stub_verified(TARGET)` is a harness attribute (to be used on [`proof`] or +/// [`proof_for_contract`] function) that replaces all occurrences of `TARGET` +/// reachable from this harness with a stub generated from the contract on +/// `TARGET`. +/// +/// To create a contract for `TARGET` you must decorate it with at least one +/// [`requires`] or [`ensures`] attribute. +/// +/// You may use multiple `stub_verified` attributes on a single harness. +/// +/// For more information see the [function contract +/// RFC](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html). +/// +/// This attribute is part of the unstable contracts API and requires +/// `-Zfunction-contracts` flag to be used. #[proc_macro_attribute] pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::stub_verified(attr, item) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index e42202bd16ad..d4f89e28f9f1 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -29,7 +29,7 @@ fn hash_of_token_stream(hasher: &mut H, stream: proc_macro } } -use syn::visit_mut::VisitMut; +use syn::{visit_mut::VisitMut, Block, Signature, Attribute}; /// Hash this `TokenStream` and return an integer that is at most digits /// long when hex formatted. @@ -120,6 +120,8 @@ where && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) } +/// Temporarily swap `$src` and `$target` using `std::mem::swap` for the +/// execution of `$code`, then swap them back. macro_rules! swapped { ($src:expr, $target:expr, $code:expr) => {{ std::mem::swap($src, $target); @@ -141,7 +143,7 @@ enum ContractFunctionState { /// of a contract attribute. Check, /// This is a replace function that was generated from a previous evaluation - /// of a contract attribute + /// of a contract attribute. Replace, } @@ -161,7 +163,7 @@ impl ContractFunctionState { "check" => Some(Self::Check), "replace" => Some(Self::Replace), _ => { - lst.span().unwrap().error("Expected `check` ident").emit(); + lst.span().unwrap().error("Expected `check` or `replace` ident").emit(); None } }; @@ -177,6 +179,8 @@ impl ContractFunctionState { None } + /// Do we need to emit the `is_contract_generated` tag attribute on the + /// generated function(s)? fn emit_tag_attr(self) -> bool { matches!(self, ContractFunctionState::Untouched) } @@ -262,7 +266,7 @@ impl ContractFunctionState { }); Some((Some((replace_fn_name, true)), Some(check_fn_name))) } - ContractFunctionState::Original | Self::ReplaceDummy => None, + ContractFunctionState::Original => None, ContractFunctionState::Check => Some((None, Some(item_fn.sig.ident.clone()))), ContractFunctionState::Replace => { Some((Some((item_fn.sig.ident.clone(), false)), None)) @@ -332,7 +336,7 @@ fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap arg_ident_collector.visit_signature(&sig); let mk_new_ident_for = |id: &Ident| Ident::new(&format!("{}_renamed", id), Span::mixed_site()); - let arg_idents = arg_ident_collector + let argument_names = arg_ident_collector .0 .into_iter() .map(|i| { @@ -341,41 +345,55 @@ fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap }) .collect::>(); - let mut ident_rewriter = Renamer(&arg_idents); + let mut ident_rewriter = Renamer(&argument_names); ident_rewriter.visit_expr_mut(attr); - arg_idents + argument_names } -struct ContractConditionsHandler<'a> { +/// +struct ContractConditionsHandler { condition_type: ContractConditionsType, attr: Expr, body: Block, } +/// Information needed for generating check and replace handlers for different +/// contract attributes. enum ContractConditionsType { Requires, - Ensures { arg_idents: HashMap }, + Ensures { + /// Translation map from original argument names to names of the copies + /// we will be emitting. + argument_names: HashMap + }, } impl ContractConditionsType { + /// Constructs a [`Self::Ensures`] from the signature of the decorated + /// function and the contents of the decorating attribute. + /// + /// Renames the [`Ident`]s used in `attr` and stores the translation map in + /// `argument_names`. fn new_ensures(sig: &Signature, attr: &mut Expr) -> Self { - let arg_idents = rename_argument_occurrences(sig, attr); + let argument_names = rename_argument_occurrences(sig, attr); - ContractConditionsType::Ensures { arg_idents } + ContractConditionsType::Ensures { argument_names } } } -impl<'a> ContractConditionsHandler<'a> { +impl ContractConditionsHandler { + /// Initialize the handler. Constructs the required [`ContractConditionsType`] fn new(is_requires: bool, mut attr: Expr, fn_sig: &Signature, fn_body: Block) -> Self { let condition_type = if is_requires { ContractConditionsType::Requires } else { - ContractConditionsType::new_ensures(sig, attr) + ContractConditionsType::new_ensures(fn_sig, &mut attr) }; Self { condition_type, attr, body: fn_body } } + /// Create the body of a check function. fn make_check_body(&self) -> TokenStream2 { let attr = &self.attr; let call_to_prior = &self.body; @@ -384,10 +402,10 @@ impl<'a> ContractConditionsHandler<'a> { kani::assume(#attr); #call_to_prior ), - ContractConditionsType::Ensures => { - let arg_names = arg_idents.values(); + ContractConditionsType::Ensures { argument_names } => { + let arg_names = argument_names.values(); let arg_names_2 = arg_names.clone(); - let arg_idents = arg_idents.keys(); + let argument_names = argument_names.keys(); let attr = &self.attr; // The code that enforces the postconditions and cleans up the shallow @@ -406,7 +424,7 @@ impl<'a> ContractConditionsHandler<'a> { let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); inject_conditions.visit_block_mut(&mut call); quote!( - #(let #arg_names = kani::untracked_deref(&#arg_idents);)* + #(let #arg_names = kani::untracked_deref(&#argument_names);)* let result = #call; #exec_postconditions result @@ -415,7 +433,12 @@ impl<'a> ContractConditionsHandler<'a> { } } - fn make_replace_body(&self, sig: &Signature, use_dummy_fn_call: bool) -> TokenStream2 { + /// Create the body of a stub for this contract. + /// + /// Wraps the conditions from this attribute around a prior call. If + /// `use_dummy_fn` is `true` the prior call we wrap is `kani::any`, + /// otherwise `self.body`. + fn make_replace_body(&self, use_dummy_fn_call: bool) -> TokenStream2 { let attr = &self.attr; let call_to_prior = if use_dummy_fn_call { quote!(kani::any()) } else { self.body.to_token_stream() }; @@ -424,9 +447,9 @@ impl<'a> ContractConditionsHandler<'a> { kani::assert(#attr, stringify!(#attr)); #call_to_prior ), - ContractConditionsType::Ensures { arg_idents } => { - let arg_names = arg_idents.values(); - let arg_values = arg_idents.keys(); + ContractConditionsType::Ensures { argument_names } => { + let arg_names = argument_names.values(); + let arg_values = argument_names.keys(); quote!( #(let #arg_names = kani::untracked_deref(&#arg_values);)* let result = #call_to_prior; @@ -493,7 +516,6 @@ impl<'a> ContractConditionsHandler<'a> { /// } /// ``` fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { - let attr_copy = proc_macro2::TokenStream::from(attr.clone()); let attr = parse_macro_input!(attr as Expr); let mut output = proc_macro2::TokenStream::new(); @@ -542,15 +564,15 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) output.extend(quote!(#[kanitool::is_contract_generated(replace)])); } - let body = handler.make_replace_body(&sig, dummy); + let body = handler.make_replace_body(dummy); sig.ident = replace_name; // Finally emit the check function itself. output.extend(quote!( - #sig { - #body - } + #sig { + #body + } )); } @@ -565,9 +587,9 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) let body = handler.make_check_body(); sig.ident = check_name; output.extend(quote!( - #sig { + #sig { #body - } + } )) } @@ -598,3 +620,4 @@ macro_rules! passthrough { } passthrough!(stub_verified, false); +passthrough!(proof_for_contract, true); diff --git a/tests/expected/function-contract/gcd_replacement_fail.expected b/tests/expected/function-contract/gcd_replacement_fail.expected index 88df38788eb0..a993325bd5e5 100644 --- a/tests/expected/function-contract/gcd_replacement_fail.expected +++ b/tests/expected/function-contract/gcd_replacement_fail.expected @@ -1,20 +1,17 @@ Frac::check_equals.assertion\ - - Status: FAILURE\ - - Description: "attempt to calculate the remainder with a divisor of zero"\ - gcd_replacement_fail.rs:50:20 in function Frac::check_equals +- Status: FAILURE\ +- Description: "attempt to calculate the remainder with a divisor of zero" Frac::check_equals.assertion\ - - Status: FAILURE\ - - Description: "assertion failed: self.den % f2.den == 0"\ - gcd_replacement_fail.rs:50:9 in function Frac::check_equals +- Status: FAILURE\ +- Description: "assertion failed: self.den % f2.den == 0" Frac::check_equals.assertion\ - - Status: FAILURE\ - - Description: "assertion failed: gcd1 == gcd2"\ - gcd_replacement_fail.rs:53:9 in function Frac::check_equals +- Status: FAILURE\ +- Description: "assertion failed: gcd1 == gcd2" Failed Checks: attempt to calculate the remainder with a divisor of zero Failed Checks: assertion failed: self.den % f2.den == 0 Failed Checks: assertion failed: gcd1 == gcd2 -VERIFICATION:- FAILED \ No newline at end of file +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_replacement_pass.expected b/tests/expected/function-contract/gcd_replacement_pass.expected index 880f00714b32..34c886c358cb 100644 --- a/tests/expected/function-contract/gcd_replacement_pass.expected +++ b/tests/expected/function-contract/gcd_replacement_pass.expected @@ -1 +1 @@ -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/simple_replace_fail.expected b/tests/expected/function-contract/simple_replace_fail.expected index 575a73ce9c26..b6806befc22c 100644 --- a/tests/expected/function-contract/simple_replace_fail.expected +++ b/tests/expected/function-contract/simple_replace_fail.expected @@ -1,3 +1,3 @@ -main.assertion - - Status: FAILURE - - Description: ""contract doesn't guarantee equality"" \ No newline at end of file +main.assertion\ +- Status: FAILURE\ +- Description: ""contract doesn't guarantee equality"" diff --git a/tests/expected/function-contract/simple_replace_fail.rs b/tests/expected/function-contract/simple_replace_fail.rs index e2d65a6aeee7..33a531a3aef7 100644 --- a/tests/expected/function-contract/simple_replace_fail.rs +++ b/tests/expected/function-contract/simple_replace_fail.rs @@ -11,7 +11,5 @@ fn div(dividend: u32, divisor: u32) -> u32 { #[kani::proof] #[kani::stub_verified(div)] fn main() { - let _ = Box::new(()); - assert!(div(9, 4) == 2, "contract doesn't guarantee equality"); } diff --git a/tests/expected/function-contract/simple_replace_pass.expected b/tests/expected/function-contract/simple_replace_pass.expected index f1d50a57ff31..34c886c358cb 100644 --- a/tests/expected/function-contract/simple_replace_pass.expected +++ b/tests/expected/function-contract/simple_replace_pass.expected @@ -1,2 +1 @@ - -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/simple_replace_pass.rs b/tests/expected/function-contract/simple_replace_pass.rs index 0f1367528b72..0dcc6cd59fe3 100644 --- a/tests/expected/function-contract/simple_replace_pass.rs +++ b/tests/expected/function-contract/simple_replace_pass.rs @@ -11,7 +11,5 @@ fn div(dividend: u32, divisor: u32) -> u32 { #[kani::proof] #[kani::stub_verified(div)] fn main() { - let _ = Box::new(()); - assert!(div(9, 1) != 10, "contract guarantees smallness"); } From 6ab4834e11a897dc0ad901e40d593ad7f7199f5d Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 7 Sep 2023 16:07:14 -0700 Subject: [PATCH 04/26] More docs, more fixes --- kani-compiler/src/kani_middle/attributes.rs | 16 ++-- library/kani_macros/src/lib.rs | 8 +- library/kani_macros/src/sysroot/contracts.rs | 81 +++++++++++++------ .../function-contract/gcd_replacement_fail.rs | 4 - .../function-contract/gcd_replacement_pass.rs | 4 - 5 files changed, 73 insertions(+), 40 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index d67d17ce7205..566e6a8e7ad3 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -138,7 +138,13 @@ impl<'tcx> KaniAttributes<'tcx> { } } - fn use_contract(&self) -> Vec> { + /// Parse, extract and resolve the target of `stub_verified(TARGET)`. The + /// 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> { self.map .get(&KaniAttributeKind::StubVerified) .map_or([].as_slice(), Vec::as_slice) @@ -183,7 +189,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// 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> { @@ -192,8 +198,8 @@ impl<'tcx> KaniAttributes<'tcx> { } /// Extract the name of the sibling function this function's contract is - /// stubbed as (if any). - /// + /// stubbed as (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 replaced_with(&self) -> Option> { @@ -394,7 +400,7 @@ impl<'tcx> KaniAttributes<'tcx> { harness.stubs.push(self.stub_for_relative_item(name, replacement_name)); } KaniAttributeKind::StubVerified => { - for contract in self.use_contract() { + for contract in self.interpret_stub_verified_attribute() { let Ok((name, def_id, _span)) = contract else { continue; }; diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 15cd9b5f4c3f..bb104145ee04 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -166,15 +166,15 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { /// [`proof_for_contract`] function) that replaces all occurrences of `TARGET` /// reachable from this harness with a stub generated from the contract on /// `TARGET`. -/// +/// /// To create a contract for `TARGET` you must decorate it with at least one /// [`requires`] or [`ensures`] attribute. -/// +/// /// You may use multiple `stub_verified` attributes on a single harness. -/// +/// /// For more information see the [function contract /// RFC](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html). -/// +/// /// This attribute is part of the unstable contracts API and requires /// `-Zfunction-contracts` flag to be used. #[proc_macro_attribute] diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index d4f89e28f9f1..709414fb617d 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -29,7 +29,7 @@ fn hash_of_token_stream(hasher: &mut H, stream: proc_macro } } -use syn::{visit_mut::VisitMut, Block, Signature, Attribute}; +use syn::{visit_mut::VisitMut, Attribute, Block, Signature}; /// Hash this `TokenStream` and return an integer that is at most digits /// long when hex formatted. @@ -163,7 +163,10 @@ impl ContractFunctionState { "check" => Some(Self::Check), "replace" => Some(Self::Replace), _ => { - lst.span().unwrap().error("Expected `check` or `replace` ident").emit(); + lst.span() + .unwrap() + .error("Expected `check` or `replace` ident") + .emit(); None } }; @@ -336,7 +339,7 @@ fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap arg_ident_collector.visit_signature(&sig); let mk_new_ident_for = |id: &Ident| Ident::new(&format!("{}_renamed", id), Span::mixed_site()); - let argument_names = arg_ident_collector + let arg_idents = arg_ident_collector .0 .into_iter() .map(|i| { @@ -345,15 +348,19 @@ fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap }) .collect::>(); - let mut ident_rewriter = Renamer(&argument_names); + let mut ident_rewriter = Renamer(&arg_idents); ident_rewriter.visit_expr_mut(attr); - argument_names + arg_idents } -/// +/// The information needed to generate the bodies of check and replacement +/// functions that integrate the conditions from this contract attribute. struct ContractConditionsHandler { + /// Information specific to the type of contract attribute we're expanding. condition_type: ContractConditionsType, + /// The contents of the attribute. attr: Expr, + /// Body of the function this attribute was found on. body: Block, } @@ -361,17 +368,17 @@ struct ContractConditionsHandler { /// contract attributes. enum ContractConditionsType { Requires, - Ensures { + Ensures { /// Translation map from original argument names to names of the copies /// we will be emitting. - argument_names: HashMap + argument_names: HashMap, }, } impl ContractConditionsType { /// Constructs a [`Self::Ensures`] from the signature of the decorated /// function and the contents of the decorating attribute. - /// + /// /// Renames the [`Ident`]s used in `attr` and stores the translation map in /// `argument_names`. fn new_ensures(sig: &Signature, attr: &mut Expr) -> Self { @@ -382,7 +389,8 @@ impl ContractConditionsType { } impl ContractConditionsHandler { - /// Initialize the handler. Constructs the required [`ContractConditionsType`] + /// Initialize the handler. Constructs the required + /// [`ContractConditionsType`] depending on `is_requires`. fn new(is_requires: bool, mut attr: Expr, fn_sig: &Signature, fn_body: Block) -> Self { let condition_type = if is_requires { ContractConditionsType::Requires @@ -394,6 +402,8 @@ impl ContractConditionsHandler { } /// Create the body of a check function. + /// + /// Wraps the conditions from this attribute around `self.body`. fn make_check_body(&self) -> TokenStream2 { let attr = &self.attr; let call_to_prior = &self.body; @@ -403,16 +413,14 @@ impl ContractConditionsHandler { #call_to_prior ), ContractConditionsType::Ensures { argument_names } => { - let arg_names = argument_names.values(); - let arg_names_2 = arg_names.clone(); - let argument_names = argument_names.keys(); + let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); let attr = &self.attr; // The code that enforces the postconditions and cleans up the shallow // argument copies (with `mem::forget`). let exec_postconditions = quote!( kani::assert(#attr, stringify!(#attr)); - #(std::mem::forget(#arg_names_2);)* + #copy_clean ); // We make a copy here because we'll modify it. Technically not @@ -424,7 +432,7 @@ impl ContractConditionsHandler { let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); inject_conditions.visit_block_mut(&mut call); quote!( - #(let #arg_names = kani::untracked_deref(&#argument_names);)* + #arg_copies let result = #call; #exec_postconditions result @@ -434,7 +442,7 @@ impl ContractConditionsHandler { } /// Create the body of a stub for this contract. - /// + /// /// Wraps the conditions from this attribute around a prior call. If /// `use_dummy_fn` is `true` the prior call we wrap is `kani::any`, /// otherwise `self.body`. @@ -448,12 +456,12 @@ impl ContractConditionsHandler { #call_to_prior ), ContractConditionsType::Ensures { argument_names } => { - let arg_names = argument_names.values(); - let arg_values = argument_names.keys(); + let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); quote!( - #(let #arg_names = kani::untracked_deref(&#arg_values);)* + #arg_copies let result = #call_to_prior; kani::assume(#attr); + #copy_clean result ) } @@ -461,6 +469,23 @@ impl ContractConditionsHandler { } } +/// We make shallow copies of the argument for the postconditions in both +/// `requires` and `ensures` clauses and later clean them up. +/// +/// This function creates the code necessary to both make the copies (first +/// tuple elem) and to clean them (second tuple elem). +fn make_unsafe_argument_copies( + renaming_map: &HashMap, +) -> (TokenStream2, TokenStream2) { + let arg_names = renaming_map.values(); + let also_arg_names = renaming_map.values(); + let arg_values = renaming_map.keys(); + ( + quote!(#(let #arg_names = kani::untracked_deref(&#arg_values);)*), + quote!(#(std::mem::forget(#also_arg_names);)*), + ) +} + /// The main meat of handling requires/ensures contracts. /// /// Generates a `check__` function that assumes preconditions @@ -514,6 +539,20 @@ impl ContractConditionsHandler { /// std::mem::forget(divisor_renamed); /// result /// } +/// +/// #[allow(dead_code)] +/// #[allow(unused_variables)] +/// #[kanitool::is_contract_generated(replace)] +/// fn div_replace_965916(dividend: u32, divisor: u32) -> u32 { +/// kani::assert(divisor != 0, "divisor != 0"); +/// let dividend_renamed = kani::untracked_deref(÷nd); +/// let divisor_renamed = kani::untracked_deref(&divisor); +/// let result = kani::any(); +/// kani::assume(result <= dividend_renamed, "result <= dividend"); +/// std::mem::forget(dividend_renamed); +/// std::mem::forget(divisor_renamed); +/// result +/// } /// ``` fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { let attr = parse_macro_input!(attr as Expr); @@ -543,9 +582,7 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) }; let ItemFn { attrs, vis: _, mut sig, block } = item_fn; - let handler = ContractConditionsHandler::new(is_requires, attr, &sig, *block); - let emit_common_header = |output: &mut TokenStream2| { if function_state.emit_tag_attr() { output.extend(quote!( @@ -563,9 +600,7 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) // important so this happens as the last emitted attribute. output.extend(quote!(#[kanitool::is_contract_generated(replace)])); } - let body = handler.make_replace_body(dummy); - sig.ident = replace_name; // Finally emit the check function itself. diff --git a/tests/expected/function-contract/gcd_replacement_fail.rs b/tests/expected/function-contract/gcd_replacement_fail.rs index b73d20cba46a..8bd59c5c14fe 100644 --- a/tests/expected/function-contract/gcd_replacement_fail.rs +++ b/tests/expected/function-contract/gcd_replacement_fail.rs @@ -57,10 +57,6 @@ impl Frac { #[kani::proof] #[kani::stub_verified(gcd)] fn main() { - // Needed to avoid having `free` be removed as unused function. This is - // because DFCC contract enforcement assumes that a definition for `free` - // exists. - let _ = Box::new(9_usize); let num: T = kani::any(); let den: T = kani::any(); kani::assume(num != 0); diff --git a/tests/expected/function-contract/gcd_replacement_pass.rs b/tests/expected/function-contract/gcd_replacement_pass.rs index 86fd59ad5618..9827dd3a1512 100644 --- a/tests/expected/function-contract/gcd_replacement_pass.rs +++ b/tests/expected/function-contract/gcd_replacement_pass.rs @@ -57,10 +57,6 @@ impl Frac { #[kani::proof] #[kani::stub_verified(gcd)] fn main() { - // Needed to avoid having `free` be removed as unused function. This is - // because DFCC contract enforcement assumes that a definition for `free` - // exists. - let _ = Box::new(9_usize); let num: T = kani::any(); let den: T = kani::any(); kani::assume(num != 0); From 3347515e9d4c0dc6d5c6ddd8aa067292db718c58 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 7 Sep 2023 16:24:47 -0700 Subject: [PATCH 05/26] Mostly expanding the test case conditions --- kani-compiler/src/kani_middle/attributes.rs | 7 ++- library/kani_macros/src/sysroot/contracts.rs | 52 +++++++++++++------ .../gcd_replacement_pass.expected | 16 ++++++ .../simple_replace_pass.expected | 8 +++ 4 files changed, 67 insertions(+), 16 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 566e6a8e7ad3..fadf05400b7f 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -31,6 +31,8 @@ enum KaniAttributeKind { /// Attribute used to mark unstable APIs. Unstable, Unwind, + /// A sound [`Self::Stub`] that replaces a function by a stub generated from + /// its contract. StubVerified, /// A harness, similar to [`Self::Proof`], but for checking a function /// contract, e.g. the contract check is substituted for the target function @@ -39,6 +41,9 @@ enum KaniAttributeKind { /// Attribute on a function with a contract that identifies the code /// implementing the check for this contract. CheckedWith, + /// Internal attribute of the contracts implementation that identifies the + /// name of the function which was generated as the sound stub from the + /// contract of this function. ReplacedWith, /// Attribute on a function that was auto-generated from expanding a /// function contract. @@ -767,7 +772,7 @@ fn parse_paths(attr: &Attribute) -> Result, Span> { .iter() .map(|arg| match arg { NestedMetaItem::Lit(item) => Err(item.span), - NestedMetaItem::MetaItem(item) => parse_path(&item).ok_or(item.span), + NestedMetaItem::MetaItem(item) => parse_path(item).ok_or(item.span), }) .collect() } diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 709414fb617d..4c96bf415171 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -262,7 +262,7 @@ impl ContractFunctionState { swapped!(&mut item_fn.attrs, &mut attrs, { output.extend(quote!( #(#attrs)* - #[kanitool::inner_check = #check_fn_name_str] + #[kanitool::checked_with = #check_fn_name_str] #[kanitool::replaced_with = #replace_fn_name_str] #item_fn )); @@ -487,30 +487,51 @@ fn make_unsafe_argument_copies( } /// The main meat of handling requires/ensures contracts. +/// +/// Generates a "check" function used to verify the validity of the contract and +/// a "replace" function that can be used as a stub, generated from the contract +/// that can be used instead of the original function. +/// +/// Each clause (requires or ensures) after the first clause will be ignored on +/// the original function (detected by finding the `kanitool::checked_with` +/// attribute). On the check function (detected by finding the +/// `kanitool::is_contract_generated` attribute) it expands into a new layer of +/// pre- or postconditions. This state machine is also explained in more detail +/// in comments in the body of this macro. +/// +/// All named arguments of the function are unsafely shallow-copied with the +/// `kani::untracked_deref` function to circumvent the borrow checker for +/// postconditions. 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 function +/// /// Generates a `check__` function that assumes preconditions /// and asserts postconditions. The check function is also marked as generated /// with the `#[kanitool::is_contract_generated(check)]` attribute. -/// +/// /// Decorates the original function with `#[kanitool::checked_by = -/// "check__"] +/// "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 /// every `return` (see [`PostconditionInjector`]). Attributes on the original -/// function are also copied to the check function. Each clause (requires or -/// ensures) after the first clause will be ignored on the original function -/// (detected by finding the `kanitool::checked_with` attribute). On the check -/// function (detected by finding the `kanitool::is_contract_generated` -/// attribute) it expands into a new layer of pre- or postconditions. This state -/// machine is also explained in more detail in comments in the body of this -/// macro. -/// -/// In the check function all named arguments of the function are unsafely -/// shallow-copied with the `kani::untracked_deref` function to circumvent the -/// borrow checker for postconditions. We must ensure that those copies are not -/// dropped so after the postconditions we call `mem::forget` on each copy. +/// function are also copied to the check function. +/// +/// ## Replace Function +/// +/// As the mirror to that also generates a `replace__` +/// function 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__"]`. +/// +/// The replace function has the same signature as the original function but its +/// body is replaced by `kani::any()`, which generates a non-deterministic +/// value. +/// /// # Complete example /// /// ```rs @@ -525,6 +546,7 @@ fn make_unsafe_argument_copies( /// /// ```rs /// #[kanitool::checked_with = "div_check_965916"] +/// #[kanitool::replaced_with = "div_replace_965916"] /// fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } /// /// #[allow(dead_code)] diff --git a/tests/expected/function-contract/gcd_replacement_pass.expected b/tests/expected/function-contract/gcd_replacement_pass.expected index 34c886c358cb..48d3565ef9f1 100644 --- a/tests/expected/function-contract/gcd_replacement_pass.expected +++ b/tests/expected/function-contract/gcd_replacement_pass.expected @@ -1 +1,17 @@ +gcd.assertion\ +- Status: SUCCESS\ +- Description: "x != 0 && y != 0" + +Frac::check_equals.assertion\ +- Status: SUCCESS\ +- Description: "assertion failed: self.num % f2.num == 0" + +Frac::check_equals.assertion\ +- Status: SUCCESS\ +- Description: "assertion failed: self.den % f2.den == 0" + +Frac::check_equals.assertion\ +- Status: SUCCESS\ +- Description: "assertion failed: gcd1 == gcd2" + VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/simple_replace_pass.expected b/tests/expected/function-contract/simple_replace_pass.expected index 34c886c358cb..e1fc78ca462f 100644 --- a/tests/expected/function-contract/simple_replace_pass.expected +++ b/tests/expected/function-contract/simple_replace_pass.expected @@ -1 +1,9 @@ +div.assertion\ +- Status: SUCCESS\ +- Description: "divisor != 0" + +main.assertion\ +- Status: SUCCESS\ +- Description: ""contract guarantees smallness"" + VERIFICATION:- SUCCESSFUL From a1f12be91a4fb0f2d88669ce67900d667f8fbaed Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 7 Sep 2023 16:33:31 -0700 Subject: [PATCH 06/26] Stupid whitespace --- library/kani_macros/src/sysroot/contracts.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 4c96bf415171..d3b74e20ed2c 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -487,29 +487,29 @@ fn make_unsafe_argument_copies( } /// The main meat of handling requires/ensures contracts. -/// +/// /// Generates a "check" function used to verify the validity of the contract and /// a "replace" function that can be used as a stub, generated from the contract /// that can be used instead of the original function. -/// +/// /// Each clause (requires or ensures) after the first clause will be ignored on /// the original function (detected by finding the `kanitool::checked_with` /// attribute). On the check function (detected by finding the /// `kanitool::is_contract_generated` attribute) it expands into a new layer of /// pre- or postconditions. This state machine is also explained in more detail /// in comments in the body of this macro. -/// +/// /// All named arguments of the function are unsafely shallow-copied with the /// `kani::untracked_deref` function to circumvent the borrow checker for /// postconditions. 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 function -/// +/// /// Generates a `check__` function that assumes preconditions /// and asserts postconditions. The check function is also marked as generated /// with the `#[kanitool::is_contract_generated(check)]` attribute. -/// +/// /// Decorates the original function with `#[kanitool::checked_by = /// "check__"]`. /// @@ -517,9 +517,9 @@ fn make_unsafe_argument_copies( /// 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. -/// +/// /// ## Replace Function -/// +/// /// As the mirror to that also generates a `replace__` /// function that asserts preconditions and assumes postconditions. The replace /// function is also marked as generated with the @@ -527,11 +527,11 @@ fn make_unsafe_argument_copies( /// /// Decorates the original function with `#[kanitool::replaced_by = /// "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 /// value. -/// +/// /// # Complete example /// /// ```rs From 2c6abd6eccd3674988371da21d27f81ee887eb1c Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 7 Sep 2023 17:25:44 -0700 Subject: [PATCH 07/26] Turns out I did need the copies. --- library/kani_macros/src/sysroot/contracts.rs | 21 +++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index d3b74e20ed2c..ac2dec18555e 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -362,6 +362,8 @@ struct ContractConditionsHandler { attr: Expr, /// Body of the function this attribute was found on. body: Block, + /// An unparsed, unmodified copy of `attr`, used in the error messages. + attr_copy: TokenStream2, } /// Information needed for generating check and replace handlers for different @@ -391,14 +393,20 @@ impl ContractConditionsType { impl ContractConditionsHandler { /// Initialize the handler. Constructs the required /// [`ContractConditionsType`] depending on `is_requires`. - fn new(is_requires: bool, mut attr: Expr, fn_sig: &Signature, fn_body: Block) -> Self { + fn new( + is_requires: bool, + mut attr: Expr, + fn_sig: &Signature, + fn_body: Block, + attr_copy: TokenStream2, + ) -> Self { let condition_type = if is_requires { ContractConditionsType::Requires } else { ContractConditionsType::new_ensures(fn_sig, &mut attr) }; - Self { condition_type, attr, body: fn_body } + Self { condition_type, attr, body: fn_body, attr_copy } } /// Create the body of a check function. @@ -406,6 +414,7 @@ impl ContractConditionsHandler { /// Wraps the conditions from this attribute around `self.body`. fn make_check_body(&self) -> TokenStream2 { let attr = &self.attr; + let attr_copy = &self.attr_copy; let call_to_prior = &self.body; match &self.condition_type { ContractConditionsType::Requires => quote!( @@ -419,7 +428,7 @@ impl ContractConditionsHandler { // The code that enforces the postconditions and cleans up the shallow // argument copies (with `mem::forget`). let exec_postconditions = quote!( - kani::assert(#attr, stringify!(#attr)); + kani::assert(#attr, stringify!(#attr_copy)); #copy_clean ); @@ -448,11 +457,12 @@ impl ContractConditionsHandler { /// otherwise `self.body`. fn make_replace_body(&self, use_dummy_fn_call: bool) -> TokenStream2 { let attr = &self.attr; + let attr_copy = &self.attr_copy; let call_to_prior = if use_dummy_fn_call { quote!(kani::any()) } else { self.body.to_token_stream() }; match &self.condition_type { ContractConditionsType::Requires => quote!( - kani::assert(#attr, stringify!(#attr)); + kani::assert(#attr, stringify!(#attr_copy)); #call_to_prior ), ContractConditionsType::Ensures { argument_names } => { @@ -577,6 +587,7 @@ fn make_unsafe_argument_copies( /// } /// ``` fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { + let attr_copy = TokenStream2::from(attr.clone()); let attr = parse_macro_input!(attr as Expr); let mut output = proc_macro2::TokenStream::new(); @@ -604,7 +615,7 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) }; let ItemFn { attrs, vis: _, mut sig, block } = item_fn; - let handler = ContractConditionsHandler::new(is_requires, attr, &sig, *block); + let handler = ContractConditionsHandler::new(is_requires, attr, &sig, *block, attr_copy); let emit_common_header = |output: &mut TokenStream2| { if function_state.emit_tag_attr() { output.extend(quote!( From 4f3c633b67cc9b02f96b1b7ded3becacf5dd3107 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 7 Sep 2023 18:06:24 -0700 Subject: [PATCH 08/26] Fix test cases --- .../prohibit-pointers/allowed_mut_return_ref.rs | 17 ++++++++++++++--- .../prohibit-pointers/return_pointer.rs | 12 +++++++++++- 2 files changed, 25 insertions(+), 4 deletions(-) diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs index 07da23e907a3..e5151396898d 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs @@ -1,14 +1,25 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts - #![allow(unreachable_code, unused_variables)] +extern crate kani; + static mut B: bool = false; +/// This only exists so I can fake a [`kani::Arbitrary`] instance for `&mut +/// bool`. +struct ArbitraryPointer

(P); + +impl<'a> kani::Arbitrary for ArbitraryPointer<&'a mut bool> { + fn any() -> Self { + ArbitraryPointer(unsafe { &mut B as &'a mut bool }) + } +} + #[kani::ensures(true)] -fn allowed_mut_return_ref<'a>() -> &'a mut bool { - unsafe { &mut B as &'a mut bool } +fn allowed_mut_return_ref<'a>() -> ArbitraryPointer<&'a mut bool> { + ArbitraryPointer(unsafe { &mut B as &'a mut bool }) } #[kani::proof_for_contract(allowed_mut_return_ref)] diff --git a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs index 44e57ed9bc9d..fc279667ad13 100644 --- a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs +++ b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs @@ -4,8 +4,18 @@ #![allow(unreachable_code, unused_variables)] +/// This only exists so I can fake a [`kani::Arbitrary`] instance for `*const +/// usize`. +struct ArbitraryPointer

(P); + +impl kani::Arbitrary for ArbitraryPointer<*const usize> { + fn any() -> Self { + unreachable!() + } +} + #[kani::ensures(true)] -fn return_pointer() -> *const usize { +fn return_pointer() -> ArbitraryPointer<*const usize> { unreachable!() } From a847af274d9f6a3fc1fc51f608bcc0dc8686d181 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Sat, 9 Sep 2023 17:48:45 -0700 Subject: [PATCH 09/26] Added nicer errors + tests for missing contracts --- kani-compiler/src/kani_middle/attributes.rs | 21 ++++++++++--------- .../missing_contract_for_check.expected | 8 +++++++ .../missing_contract_for_check.rs | 10 +++++++++ .../missing_contract_for_replace.expected | 8 +++++++ .../missing_contract_for_replace.rs | 11 ++++++++++ 5 files changed, 48 insertions(+), 10 deletions(-) create mode 100644 tests/expected/function-contract/missing_contract_for_check.expected create mode 100644 tests/expected/function-contract/missing_contract_for_check.rs create mode 100644 tests/expected/function-contract/missing_contract_for_replace.expected create mode 100644 tests/expected/function-contract/missing_contract_for_replace.rs diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index fadf05400b7f..d86a83f42943 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -399,24 +399,25 @@ impl<'tcx> KaniAttributes<'tcx> { else { self.tcx .sess - .span_err(span, "Target function for this check has no contract"); + .struct_span_err(span, format!("Could not find a contract to check for target of `{}` attribute", kind.as_ref())) + .span_note(self.tcx.def_span(id), "Expected a contract on this function") + .emit(); return harness; }; harness.stubs.push(self.stub_for_relative_item(name, replacement_name)); } KaniAttributeKind::StubVerified => { for contract in self.interpret_stub_verified_attribute() { - let Ok((name, def_id, _span)) = contract else { + let Ok((name, def_id, span)) = contract else { continue; }; - let Some(Ok(replacement_name)) = - KaniAttributes::for_item(self.tcx, def_id).replaced_with() - else { - self.tcx.sess.span_err( - self.tcx.def_span(self.item), - format!("Invalid `{}` attribute format", kind.as_ref()), - ); - continue; + let replacement_name = match KaniAttributes::for_item(self.tcx, def_id).replaced_with() { + None => { + self.tcx.sess.struct_span_err(span, format!("Could not find a contract for stubbing on target of `{}` attribute.", kind.as_ref())).span_note(self.tcx.def_span(def_id), "Expected a contract on this function.").emit(); + continue + }, + Some(Ok(replacement_name)) => replacement_name, + Some(Err(_)) => continue, }; harness.stubs.push(self.stub_for_relative_item(name, replacement_name)) } diff --git a/tests/expected/function-contract/missing_contract_for_check.expected b/tests/expected/function-contract/missing_contract_for_check.expected new file mode 100644 index 000000000000..c736590ec15f --- /dev/null +++ b/tests/expected/function-contract/missing_contract_for_check.expected @@ -0,0 +1,8 @@ +error: Could not find a contract to check for target of `proof_for_contract` attribute + | +7 | #[kani::proof_for_contract(no_contract)] + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | +note: Expected a contract on this function + | +5 | fn no_contract() {} diff --git a/tests/expected/function-contract/missing_contract_for_check.rs b/tests/expected/function-contract/missing_contract_for_check.rs new file mode 100644 index 000000000000..1fccd1ed7448 --- /dev/null +++ b/tests/expected/function-contract/missing_contract_for_check.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +fn no_contract() {} + +#[kani::proof_for_contract(no_contract)] +fn harness() { + no_contract(); +} diff --git a/tests/expected/function-contract/missing_contract_for_replace.expected b/tests/expected/function-contract/missing_contract_for_replace.expected new file mode 100644 index 000000000000..59a2a6f9cbdd --- /dev/null +++ b/tests/expected/function-contract/missing_contract_for_replace.expected @@ -0,0 +1,8 @@ +error: Could not find a contract for stubbing on target of `stub_verified` attribute. + | +8 | #[kani::stub_verified(no_contract)] + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | +note: Expected a contract on this function. + | +5 | fn no_contract() {} diff --git a/tests/expected/function-contract/missing_contract_for_replace.rs b/tests/expected/function-contract/missing_contract_for_replace.rs new file mode 100644 index 000000000000..25abe89bb80e --- /dev/null +++ b/tests/expected/function-contract/missing_contract_for_replace.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +fn no_contract() {} + +#[kani::proof] +#[kani::stub_verified(no_contract)] +fn harness() { + no_contract(); +} From 29b128a7101a7c14926e9aa14407d725c0e3bdf0 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 15 Sep 2023 16:10:50 -0700 Subject: [PATCH 10/26] Incorporating suggestions --- kani-compiler/src/kani_middle/attributes.rs | 105 +++++++++++------- .../missing_contract_for_check.expected | 6 +- .../missing_contract_for_replace.expected | 6 +- 3 files changed, 75 insertions(+), 42 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index d86a83f42943..2c9f2266368b 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -384,44 +384,8 @@ impl<'tcx> KaniAttributes<'tcx> { harness.unwind_value = parse_unwind(self.tcx, attributes[0]) } KaniAttributeKind::Proof => harness.proof = true, - KaniAttributeKind::ProofForContract => { - harness.proof = true; - let Some(Ok((name, id, span))) = self.interpret_the_for_contract_attribute() - else { - self.tcx.sess.span_err( - self.tcx.def_span(self.item), - format!("Invalid `{}` attribute format", kind.as_ref()), - ); - return harness; - }; - let Some(Ok(replacement_name)) = - KaniAttributes::for_item(self.tcx, id).checked_with() - else { - self.tcx - .sess - .struct_span_err(span, format!("Could not find a contract to check for target of `{}` attribute", kind.as_ref())) - .span_note(self.tcx.def_span(id), "Expected a contract on this function") - .emit(); - return harness; - }; - harness.stubs.push(self.stub_for_relative_item(name, replacement_name)); - } - KaniAttributeKind::StubVerified => { - for contract in self.interpret_stub_verified_attribute() { - let Ok((name, def_id, span)) = contract else { - continue; - }; - let replacement_name = match KaniAttributes::for_item(self.tcx, def_id).replaced_with() { - None => { - self.tcx.sess.struct_span_err(span, format!("Could not find a contract for stubbing on target of `{}` attribute.", kind.as_ref())).span_note(self.tcx.def_span(def_id), "Expected a contract on this function.").emit(); - continue - }, - Some(Ok(replacement_name)) => replacement_name, - Some(Err(_)) => continue, - }; - harness.stubs.push(self.stub_for_relative_item(name, replacement_name)) - } - } + KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness), + KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness), KaniAttributeKind::Unstable => { // Internal attribute which shouldn't exist here. unreachable!() @@ -436,6 +400,71 @@ impl<'tcx> KaniAttributes<'tcx> { }) } + fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes) { + let sess = self.tcx.sess; + 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 Some(Ok(replacement_name)) = KaniAttributes::for_item(self.tcx, id).checked_with() + else { + sess.struct_span_err( + span, + format!( + "Failed to check contract: Function `{}` has no contract.", + self.item_name(), + ), + ) + .span_note( + self.tcx.def_span(id), + format!( + "Try adding a contract to this function or use the unsound `{}` attribute instead.", + KaniAttributeKind::Stub.as_ref(), + ) + ) + .emit(); + return; + }; + harness.stubs.push(self.stub_for_relative_item(name, replacement_name)); + } + + fn handle_stub_verified(&self, harness: &mut HarnessAttributes) { + let sess = self.tcx.sess; + 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 => { + sess.struct_span_err( + span, + format!( + "Failed to generate verified stub: Function `{}` has no contract.", + self.item_name(), + ), + ) + .span_note(self.tcx.def_span(def_id), "Try adding a contract to this function.") + .emit(); + continue; + } + Some(Ok(replacement_name)) => replacement_name, + Some(Err(_)) => continue, + }; + harness.stubs.push(self.stub_for_relative_item(name, replacement_name)) + } + } + + fn item_name(&self) -> Symbol { + self.tcx.item_name(self.item) + } + /// Check that if this item is tagged with a proof_attribute, it is a valid harness. fn check_proof_attribute(&self, proof_attribute: &Attribute) { let span = proof_attribute.span; diff --git a/tests/expected/function-contract/missing_contract_for_check.expected b/tests/expected/function-contract/missing_contract_for_check.expected index c736590ec15f..f0f12e833450 100644 --- a/tests/expected/function-contract/missing_contract_for_check.expected +++ b/tests/expected/function-contract/missing_contract_for_check.expected @@ -1,8 +1,10 @@ -error: Could not find a contract to check for target of `proof_for_contract` attribute +error: Failed to check contract: Function `harness` has no contract. | 7 | #[kani::proof_for_contract(no_contract)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | -note: Expected a contract on this function +note: Try adding a contract to this function or use the unsound `stub` attribute instead. | 5 | fn no_contract() {} + | ^^^^^^^^^^^^^^^^ + \ No newline at end of file diff --git a/tests/expected/function-contract/missing_contract_for_replace.expected b/tests/expected/function-contract/missing_contract_for_replace.expected index 59a2a6f9cbdd..d3a2559307ae 100644 --- a/tests/expected/function-contract/missing_contract_for_replace.expected +++ b/tests/expected/function-contract/missing_contract_for_replace.expected @@ -1,8 +1,10 @@ -error: Could not find a contract for stubbing on target of `stub_verified` attribute. +error: Failed to generate verified stub: Function `harness` has no contract. | 8 | #[kani::stub_verified(no_contract)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | -note: Expected a contract on this function. +note: Try adding a contract to this function. | 5 | fn no_contract() {} + | ^^^^^^^^^^^^^^^^ + \ No newline at end of file From 56511465fc0222fe549e31940248dbfde011c49d Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 15 Sep 2023 16:11:15 -0700 Subject: [PATCH 11/26] Apply suggestions from code review Co-authored-by: Celina G. Val --- kani-compiler/src/kani_middle/attributes.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 2c9f2266368b..9bb862ded2ff 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -160,7 +160,7 @@ impl<'tcx> KaniAttributes<'tcx> { self.tcx.sess.span_err( attr.span, format!( - "Sould not resolve replacement function {} because {e}", + "Could not resolve replacement function {}: {e}", name.as_str() ), ) From cf9e4a55dc12840933aeb2f35b12abb9be8ff086 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Mon, 18 Sep 2023 10:22:58 -0700 Subject: [PATCH 12/26] Format --- kani-compiler/src/kani_middle/attributes.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 9bb862ded2ff..83e2247dc03b 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -159,10 +159,7 @@ impl<'tcx> KaniAttributes<'tcx> { let ok = self.resolve_sibling(name.as_str()).map_err(|e| { self.tcx.sess.span_err( attr.span, - format!( - "Could not resolve replacement function {}: {e}", - name.as_str() - ), + format!("Could not resolve replacement function {}: {e}", name.as_str()), ) })?; Ok((name, ok, attr.span)) From a6dc2825e8cc63e2767abd81fc6e743ce72ffcb2 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 19 Sep 2023 08:18:15 -0700 Subject: [PATCH 13/26] Switch the notes --- kani-compiler/src/kani_middle/attributes.rs | 18 +++++++++--------- .../missing_contract_for_check.expected | 2 +- .../missing_contract_for_replace.expected | 2 +- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 83e2247dc03b..d6d5929d10a9 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -411,17 +411,11 @@ impl<'tcx> KaniAttributes<'tcx> { sess.struct_span_err( span, format!( - "Failed to check contract: Function `{}` has no contract.", + "Failed to check contract: Function `{}` has no contract.", self.item_name(), ), ) - .span_note( - self.tcx.def_span(id), - format!( - "Try adding a contract to this function or use the unsound `{}` attribute instead.", - KaniAttributeKind::Stub.as_ref(), - ) - ) + .span_note(self.tcx.def_span(id), "Try adding a contract to this function.") .emit(); return; }; @@ -447,7 +441,13 @@ impl<'tcx> KaniAttributes<'tcx> { self.item_name(), ), ) - .span_note(self.tcx.def_span(def_id), "Try adding a contract to this function.") + .span_note( + self.tcx.def_span(def_id), + format!( + "Try adding a contract to this function or use the unsound `{}` attribute instead.", + KaniAttributeKind::Stub.as_ref(), + ) + ) .emit(); continue; } diff --git a/tests/expected/function-contract/missing_contract_for_check.expected b/tests/expected/function-contract/missing_contract_for_check.expected index f0f12e833450..0b2f20cac7f7 100644 --- a/tests/expected/function-contract/missing_contract_for_check.expected +++ b/tests/expected/function-contract/missing_contract_for_check.expected @@ -3,7 +3,7 @@ error: Failed to check contract: Function `harness` has no contract. 7 | #[kani::proof_for_contract(no_contract)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | -note: Try adding a contract to this function or use the unsound `stub` attribute instead. +note: Try adding a contract to this function. | 5 | fn no_contract() {} | ^^^^^^^^^^^^^^^^ diff --git a/tests/expected/function-contract/missing_contract_for_replace.expected b/tests/expected/function-contract/missing_contract_for_replace.expected index d3a2559307ae..d34061fff160 100644 --- a/tests/expected/function-contract/missing_contract_for_replace.expected +++ b/tests/expected/function-contract/missing_contract_for_replace.expected @@ -3,7 +3,7 @@ error: Failed to generate verified stub: Function `harness` has no contract. 8 | #[kani::stub_verified(no_contract)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | -note: Try adding a contract to this function. +note: Try adding a contract to this function or use the unsound `stub` attribute instead. | 5 | fn no_contract() {} | ^^^^^^^^^^^^^^^^ From 05abe4dc7b9f6bf3a53d42735d22677d46c66be2 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 19 Sep 2023 08:48:50 -0700 Subject: [PATCH 14/26] Added type annotation --- library/kani_macros/src/sysroot/contracts.rs | 29 ++++++++++++++----- .../type_annotation_needed.expected | 1 + .../type_annotation_needed.rs | 15 ++++++++++ 3 files changed, 38 insertions(+), 7 deletions(-) create mode 100644 tests/expected/function-contract/type_annotation_needed.expected create mode 100644 tests/expected/function-contract/type_annotation_needed.rs diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index ac2dec18555e..293af333f77f 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -1,6 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use std::collections::{HashMap, HashSet}; +use std::{ + borrow::Cow, + collections::{HashMap, HashSet}, +}; use proc_macro::TokenStream; @@ -412,10 +415,11 @@ impl ContractConditionsHandler { /// Create the body of a check function. /// /// Wraps the conditions from this attribute around `self.body`. - fn make_check_body(&self) -> TokenStream2 { + fn make_check_body(&self, sig: &Signature) -> TokenStream2 { let attr = &self.attr; let attr_copy = &self.attr_copy; let call_to_prior = &self.body; + let return_type = return_type_to_type(&sig.output); match &self.condition_type { ContractConditionsType::Requires => quote!( kani::assume(#attr); @@ -442,7 +446,7 @@ impl ContractConditionsHandler { inject_conditions.visit_block_mut(&mut call); quote!( #arg_copies - let result = #call; + let result : #return_type = #call; #exec_postconditions result ) @@ -455,11 +459,12 @@ impl ContractConditionsHandler { /// Wraps the conditions from this attribute around a prior call. If /// `use_dummy_fn` is `true` the prior call we wrap is `kani::any`, /// otherwise `self.body`. - fn make_replace_body(&self, use_dummy_fn_call: bool) -> TokenStream2 { + fn make_replace_body(&self, sig: &syn::Signature, use_dummy_fn_call: bool) -> TokenStream2 { let attr = &self.attr; let attr_copy = &self.attr_copy; let call_to_prior = if use_dummy_fn_call { quote!(kani::any()) } else { self.body.to_token_stream() }; + let return_type = return_type_to_type(&sig.output); match &self.condition_type { ContractConditionsType::Requires => quote!( kani::assert(#attr, stringify!(#attr_copy)); @@ -469,7 +474,7 @@ impl ContractConditionsHandler { let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); quote!( #arg_copies - let result = #call_to_prior; + let result: #return_type = #call_to_prior; kani::assume(#attr); #copy_clean result @@ -479,6 +484,16 @@ impl ContractConditionsHandler { } } +fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { + match return_type { + syn::ReturnType::Default => Cow::Owned(syn::Type::Tuple(syn::TypeTuple { + paren_token: syn::token::Paren::default(), + elems: Default::default(), + })), + syn::ReturnType::Type(_, typ) => Cow::Borrowed(typ.as_ref()), + } +} + /// We make shallow copies of the argument for the postconditions in both /// `requires` and `ensures` clauses and later clean them up. /// @@ -633,7 +648,7 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) // important so this happens as the last emitted attribute. output.extend(quote!(#[kanitool::is_contract_generated(replace)])); } - let body = handler.make_replace_body(dummy); + let body = handler.make_replace_body(&sig, dummy); sig.ident = replace_name; // Finally emit the check function itself. @@ -652,7 +667,7 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) // important so this happens as the last emitted attribute. output.extend(quote!(#[kanitool::is_contract_generated(check)])); } - let body = handler.make_check_body(); + let body = handler.make_check_body(&sig); sig.ident = check_name; output.extend(quote!( #sig { diff --git a/tests/expected/function-contract/type_annotation_needed.expected b/tests/expected/function-contract/type_annotation_needed.expected new file mode 100644 index 000000000000..880f00714b32 --- /dev/null +++ b/tests/expected/function-contract/type_annotation_needed.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/type_annotation_needed.rs b/tests/expected/function-contract/type_annotation_needed.rs new file mode 100644 index 000000000000..7160a0f31bb5 --- /dev/null +++ b/tests/expected/function-contract/type_annotation_needed.rs @@ -0,0 +1,15 @@ + +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result.is_some())] +fn or_default(opt: Option) -> Option { + opt.or(Some(T::default())) +} + +#[kani::proof_for_contract(or_default)] +fn harness() { + let input: Option = kani::any(); + or_default(input); +} \ No newline at end of file From 05071f18e6a54e2f3fd8ac1c723bd9b296947513 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 19 Sep 2023 11:03:21 -0700 Subject: [PATCH 15/26] Sketch for module-level contracts documentation. --- library/kani/src/contracts.rs | 171 +++++++++++++++++++++++++++++++++ library/kani/src/lib.rs | 4 +- library/kani_macros/src/lib.rs | 59 +++++------- 3 files changed, 196 insertions(+), 38 deletions(-) create mode 100644 library/kani/src/contracts.rs diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs new file mode 100644 index 000000000000..230f39682659 --- /dev/null +++ b/library/kani/src/contracts.rs @@ -0,0 +1,171 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Kani implementation of function contracts. +//! +//! Function contracts are still under development. Using the APIs therefore +//! requires the unstable `-Zfunction-contracts` flag to be passed. You can join +//! the discussion on contract design by commenting on [the +//! RFC](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html). +//! +//! The function contract API is expressed as proc-macro attributes, and there +//! are two parts to it. +//! +//! 1. [Contract specification attributes](#specification-attributes-overview): +//! [`requires`][macro@requires] and [`ensures`][macro@ensures]. +//! 2. [Contract use attributes](#contract-use-attributes-overview): +//! [`proof_for_contract`][macro@proof_for_contract] and +//! [`stub_verified`][macro@stub_verified]. +//! +//! ## Step-by-step Guide +//! +//! Let us explore using a workflow involving contracts on the example of a +//! simple division function `my_div`: +//! +//! ``` +//! fn my_div(dividend: u32, divisor: u32) -> u32 { +//! dividend / divisor +//! } +//! ``` +//! +//! With the contract specification attributes we can specify the behavior of +//! this function declaratively. The [`requires`][macro@requires] attribute +//! allows us to declare constraints on what constitutes valid inputs to our +//! function. In this case we would want to disallow a divisor that is `0`. +//! +//! ```ignore +//! #[requires(divisor != 0)] +//! ``` +//! +//! This is called a precondition, because it is enforced before (pre-) the +//! function call. As you can see attribute has access to the functions +//! arguments. The condition itself is just regular Rust code. You can use any +//! Rust code, including calling functions and methods. However you may not +//! perform I/O (like [`println!`]) or mutate memory (like [`Vec::push`]). +//! +//! The [`ensures`][macro@ensures] attribute on the other hand lets us describe +//! the output value in terms of the inputs. You may be as (im)precise as you +//! like in the [`ensures`][macro@ensures] clause, depending on your needs. One +//! approximation of the result of division for instance could be this: +//! +//! ``` +//! #[ensures(result <= dividend)] +//! ``` +//! +//! This is called a postcondition and it also has access to the arguments and +//! is expressed in regular Rust code. The same restrictions apply as did for +//! [`requires`][macro@requires]. In addition to the arguments the postcondition +//! also has access to the value returned from the function in a variable called +//! `result`. +//! +//! You may combine as many [`requires`][macro@requires] and +//! [`ensures`][macro@ensures] attributes on a single function as you please. +//! They all get enforced (as if their conditions were `&&`ed together) and the +//! order does not matter. In our example putting them together looks like this: +//! +//! ``` +//! #[kani::requires(divisor != 0)] +//! #[kani::ensures(result <= dividend)] +//! fn my_div(dividend: u32, divisor: u32) -> u32 { +//! dividend / divisor +//! } +//! ``` +//! +//! Once we are finished specifying our contract we can ask kani to check it's +//! validity. For this we need to provide a proof harness that exercises the +//! function. The harness is created like any other, e.g. as a test-like +//! function with inputs and using `kani::any` to create arbitrary values. +//! However we do not need to add any assertions or assumptions about the +//! inputs, Kani will use the pre- and postconditions we have specified for that +//! and we use the [`proof_for_contract`][macro@proof_for_contract] attribute +//! instead of [`proof`](crate::proof) and provide it with the path to the +//! function we want to check. +//! +//! ``` +//! #[kani::proof_for_contract(my_div)] +//! fn my_div_harness() { +//! my_div(kani::any(), kani::any()) } +//! ``` +//! +//! The harness is checked like any other by running `cargo kani` and can be +//! specifically selected with `--harness my_div_harness`. +//! +//! Once we have verified that our contract holds, we can use perhaps it's +//! coolest feature: verified stubbing. This allows us to use the conditions of +//! the contract *instead* of it's implementation. This can be very powerful for +//! expensive implementations (involving loops for instance). +//! +//! Verified stubbing is available to any harness via the +//! [`stub_verified`][macro@stub_verified] harness attribute. We must provide +//! the attribute with the path to the function to stub, but unlike with +//! [`stub`](crate::stub) we do not need to provide a function to replace with, +//! the contract will be used automatically. +//! +//! ``` +//! #[kani::proof] +//! #[kani::stub_verified(my_div)] +//! fn use_div() { +//! let v = vec![...]; +//! let some_idx = my_div(v.len() - 1, 3); +//! v[some_idx]; +//! } +//! ``` +//! +//! In this example the contract is sufficient to prove that the element access +//! in the last line cannot be out-of-bounds. +//! +//! ## Specification Attributes Overview +//! +//! There are currently two specification attributes available for describing +//! function behavior: [`requires`][macro@requires] for preconditions and +//! [`ensures`][macro@ensures] for postconditions. Both admit arbitrary Rust +//! expressions as their bodies which may also reference the function arguments +//! but must not mutate memory or perform I/O. The postcondition may +//! additionally reference the return value of the function as the variable +//! `result`. +//! +//! During verified stubbing the return value of a function with a contract is +//! replaced by a call to `kani::any`. As such the return value must implement +//! the `kani::Arbitrary` trait. +//! +//! In Kani, function contracts are optional. As such a function with at least +//! one specification attribute is considered to "have a contract" and any +//! absent specification type defaults to its most general interpretation +//! (`true`). All functions with not a single specification attribute are +//! considered " not to "have a contract" and are ineligible for use as the +//! target of a [`proof_for_contract`][macro@proof_for_contract] of +//! [`stub_verified`][macro@stub_verified] attribute. +//! +//! ## Contract Use Attributes Overview +//! +//! Contract are used both to verify function behavior and to leverage the +//! verification result as a sound abstraction. +//! +//! Verifying function behavior currently requires the designation of at least +//! one checking harness with the +//! [`proof_for_contract`](macro@proof_for_contract) attribute. A harness may +//! only have one `proof_for_contract` attribute and it may not also have a +//! `proof` attribute. +//! +//! The checking harness is expected to set up the arguments that `foo` should +//! be called with and initialized any `static mut` globals that are reachable. +//! All of these should be initialized to as general value as possible, usually +//! achieved using `kani::any`. The harness must call e.g. `foo` at least once +//! and if `foo` has type parameters, only one instantiation of those parameters +//! is admissible. Violating either results in a compile error. +//! +//! If any inputs have special invariants you *can* use `kani::assume` to +//! enforce them but this may introduce unsoundness. In general all restrictions +//! on input parameters should be part of the [`requires`](macro@requires) +//! clause of the function contract. +//! +//! Once the contract has been verified it may be used as a verified stub. For +//! this the [`stub_verified`](macro@stub_verified) attribute is used. +//! `stub_verified` is a harness attribute, like +//! [`unwind`](macro@crate::unwind), meaning it is used on functions that are +//! annotated with [`proof`](macro@crate::proof). It may also be used on a +//! `proof_for_contract` proof. +//! +//! Unlike `proof_for_contract` multiple `stub_verified` attributes are allowed +//! on the same proof harness though they must target different functions. +pub use super::{ensures, proof_for_contract, requires, stub_verified}; diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 6125c589a957..1da6a4655018 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -294,5 +294,7 @@ macro_rules! cover { }; } -/// Kani proc macros must be in a separate crate +// Kani proc macros must be in a separate crate pub use kani_macros::*; + +pub mod contracts; diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index bb104145ee04..89482a6266ca 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -97,9 +97,10 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } -/// Add a precondition to this function. +/// Add a precondition to this function. /// -/// This is part of the function contract API, together with [`ensures`]. +/// This is part of the function contract API, for more general information see +/// the [module-level documentation](../kani/contracts/index.html). /// /// The contents of the attribute is a condition over the input values to the /// annotated function. All Rust syntax is supported, even calling other @@ -107,11 +108,9 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// perform I/O or use mutable memory. /// /// Kani requires each function that uses a contract (this attribute or -/// [`ensures`]) to have at least one designated [`proof_for_contract`] harness -/// for checking the contract. -/// -/// This attribute is part of the unstable contracts API and requires -/// `-Zfunction-contracts` flag to be used. +/// [`ensures`][macro@ensures]) to have at least one designated +/// [`proof_for_contract`][macro@proof_for_contract] harness for checking the +/// contract. #[proc_macro_attribute] pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::requires(attr, item) @@ -119,7 +118,8 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { /// Add a postcondition to this function. /// -/// This is part of the function contract API, together with [`requires`]. +/// This is part of the function contract API, for more general information see +/// the [module-level documentation](../kani/contracts/index.html). /// /// The contents of the attribute is a condition over the input values to the /// annotated function *and* its return value, accessible as a variable called @@ -128,11 +128,9 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { /// mutable memory. /// /// Kani requires each function that uses a contract (this attribute or -/// [`requires`]) to have at least one designated [`proof_for_contract`] harness -/// for checking the contract. -/// -/// This attribute is part of the unstable contracts API and requires -/// `-Zfunction-contracts` flag to be used. +/// [`requires`][macro@requires]) to have at least one designated +/// [`proof_for_contract`][macro@proof_for_contract] harness for checking the +/// contract. #[proc_macro_attribute] pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::ensures(attr, item) @@ -144,39 +142,26 @@ pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { /// `super::some_mod::foo` or `crate::SomeStruct::foo`) to the function, the /// contract of which should be checked. /// -/// The harness is expected to set up the arguments that `foo` should be called -/// with and initialzied any `static mut` globals that are reachable. All of -/// these should be initialized to as general value as possible, usually -/// achieved using `kani::any`. The harness must call e.g. `foo` at least once -/// and if `foo` has type parameters, only one instantiation of those parameters -/// is admissible. Violating either results in a compile error. -/// -/// If any of those types have special invariants you can use `kani::assume` to -/// enforce them, but other than condition on inputs and checks of outputs -/// should be in the contract, not the harness for maximum soundness. -/// -/// This attribute is part of the unstable contracts API and requires -/// `-Zfunction-contracts` flag to be used. +/// This is part of the function contract API, for more general information see +/// the [module-level documentation](../kani/contracts/index.html). #[proc_macro_attribute] pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::proof_for_contract(attr, item) } -/// `stub_verified(TARGET)` is a harness attribute (to be used on [`proof`] or -/// [`proof_for_contract`] function) that replaces all occurrences of `TARGET` -/// reachable from this harness with a stub generated from the contract on -/// `TARGET`. +/// `stub_verified(TARGET)` is a harness attribute (to be used on +/// [`proof`][macro@proof] or [`proof_for_contract`][macro@proof_for_contract] +/// function) that replaces all occurrences of `TARGET` reachable from this +/// harness with a stub generated from the contract on `TARGET`. /// -/// To create a contract for `TARGET` you must decorate it with at least one -/// [`requires`] or [`ensures`] attribute. +/// The target of `stub_verified` *must* have a contract. More information about +/// how to specify a contract for your function can be found +/// [here](../contracts/index.html#specification-attributes-overview). /// /// You may use multiple `stub_verified` attributes on a single harness. /// -/// For more information see the [function contract -/// RFC](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html). -/// -/// This attribute is part of the unstable contracts API and requires -/// `-Zfunction-contracts` flag to be used. +/// This is part of the function contract API, for more general information see +/// the [module-level documentation](../kani/contracts/index.html). #[proc_macro_attribute] pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::stub_verified(attr, item) From 0777d0d4832fde4cddf935c0f305fa5c4eb5a05c Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 19 Sep 2023 11:11:49 -0700 Subject: [PATCH 16/26] Formatting --- tests/expected/function-contract/type_annotation_needed.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/expected/function-contract/type_annotation_needed.rs b/tests/expected/function-contract/type_annotation_needed.rs index 7160a0f31bb5..2123162fdded 100644 --- a/tests/expected/function-contract/type_annotation_needed.rs +++ b/tests/expected/function-contract/type_annotation_needed.rs @@ -1,4 +1,3 @@ - // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts @@ -12,4 +11,4 @@ fn or_default(opt: Option) -> Option { fn harness() { let input: Option = kani::any(); or_default(input); -} \ No newline at end of file +} From 272326a65a8d6e3ab81e86fc4497746dfab197b5 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 21 Sep 2023 11:37:02 -0700 Subject: [PATCH 17/26] Change code structure --- library/kani_macros/src/sysroot/contracts.rs | 594 ++++++++++--------- 1 file changed, 306 insertions(+), 288 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 293af333f77f..97dd089756fb 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -1,11 +1,113 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Implementation of the function contracts code generation. +//! +//! The most exciting part is the handling of `requires` and `ensures`, the main +//! entry point to which is [`requires_ensures_main`]. Most of the code +//! generation for that is implemented on [`ContractConditionsHandler`] with +//! [`ContractFunctionState`] steering the code generation. The function state +//! 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. +//! +//! We generate a "check" function used to verify the validity of the contract +//! and a "replace" function that can be used as a stub, generated from the +//! contract that can be used instead of the original function. +//! +//! Each clause (requires or ensures) after the first clause will be ignored on +//! the original function (detected by finding the `kanitool::checked_with` +//! attribute). On the check function (detected by finding the +//! `kanitool::is_contract_generated` attribute) it expands into a new layer of +//! pre- or postconditions. This state machine is also explained in more detail +//! in code comments. +//! +//! All named arguments of the annotated function are unsafely shallow-copied +//! with the `kani::untracked_deref` function to circumvent the borrow checker +//! for postconditions. 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 function +//! +//! Generates a `check__` function that assumes preconditions +//! and asserts postconditions. The check function is also marked as generated +//! with the `#[kanitool::is_contract_generated(check)]` attribute. +//! +//! Decorates the original function with `#[kanitool::checked_by = +//! "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 +//! every `return` (see [`PostconditionInjector`]). Attributes on the original +//! function are also copied to the check function. +//! +//! ## Replace Function +//! +//! As the mirror to that also generates a `replace__` +//! function 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__"]`. +//! +//! The replace function has the same signature as the original function but its +//! body is replaced by `kani::any()`, which generates a non-deterministic +//! value. +//! +//! # Complete example +//! +//! ```rs +//! #[kani::requires(divisor != 0)] +//! #[kani::ensures(result <= dividend)] +//! fn div(dividend: u32, divisor: u32) -> u32 { +//! dividend / divisor +//! } +//! ``` +//! +//! Turns into +//! +//! ```rs +//! #[kanitool::checked_with = "div_check_965916"] +//! #[kanitool::replaced_with = "div_replace_965916"] +//! fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } +//! +//! #[allow(dead_code)] +//! #[allow(unused_variables)] +//! #[kanitool::is_contract_generated(check)] +//! fn div_check_965916(dividend: u32, divisor: u32) -> u32 { +//! let dividend_renamed = kani::untracked_deref(÷nd); +//! let divisor_renamed = kani::untracked_deref(&divisor); +//! let result = { kani::assume(divisor != 0); { dividend / divisor } }; +//! kani::assert(result <= dividend_renamed, "result <= dividend"); +//! std::mem::forget(dividend_renamed); +//! std::mem::forget(divisor_renamed); +//! result +//! } +//! +//! #[allow(dead_code)] +//! #[allow(unused_variables)] +//! #[kanitool::is_contract_generated(replace)] +//! fn div_replace_965916(dividend: u32, divisor: u32) -> u32 { +//! kani::assert(divisor != 0, "divisor != 0"); +//! let dividend_renamed = kani::untracked_deref(÷nd); +//! let divisor_renamed = kani::untracked_deref(&divisor); +//! let result = kani::any(); +//! kani::assume(result <= dividend_renamed, "result <= dividend"); +//! std::mem::forget(dividend_renamed); +//! std::mem::forget(divisor_renamed); +//! result +//! } +//! ``` + use std::{ borrow::Cow, collections::{HashMap, HashSet}, }; -use proc_macro::TokenStream; +use proc_macro::{Diagnostic, TokenStream}; use { quote::{quote, ToTokens}, @@ -32,7 +134,7 @@ fn hash_of_token_stream(hasher: &mut H, stream: proc_macro } } -use syn::{visit_mut::VisitMut, Attribute, Block, Signature}; +use syn::{visit_mut::VisitMut, Attribute, Signature}; /// Hash this `TokenStream` and return an integer that is at most digits /// long when hex formatted. @@ -53,11 +155,11 @@ fn identifier_for_generated_function(related_function: &ItemFn, purpose: &str, h } pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { - requires_ensures_alt(attr, item, true) + requires_ensures_main(attr, item, true) } pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { - requires_ensures_alt(attr, item, false) + requires_ensures_main(attr, item, false) } /// Collect all named identifiers used in the argument patterns of a function. @@ -123,17 +225,6 @@ where && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) } -/// Temporarily swap `$src` and `$target` using `std::mem::swap` for the -/// execution of `$code`, then swap them back. -macro_rules! swapped { - ($src:expr, $target:expr, $code:expr) => {{ - std::mem::swap($src, $target); - let result = $code; - std::mem::swap($src, $target); - result - }}; -} - /// Classifies the state a function is in in the contract handling pipeline. #[derive(Clone, Copy, PartialEq, Eq)] enum ContractFunctionState { @@ -150,39 +241,51 @@ enum ContractFunctionState { Replace, } -impl ContractFunctionState { +impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState { + type Error = Option; + /// Find out if this attribute could be describing a "contract handling" /// state and if so return it. - fn from_attribute(attribute: &syn::Attribute) -> Option { + 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"]) { - match syn::parse2::(lst.tokens.clone()) { - Err(e) => { - lst.span().unwrap().error(format!("{e}")).emit(); - } - Ok(ident) => { - let ident_str = ident.to_string(); - return match ident_str.as_str() { - "check" => Some(Self::Check), - "replace" => Some(Self::Replace), - _ => { - lst.span() - .unwrap() - .error("Expected `check` or `replace` ident") - .emit(); - None - } - }; + 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), + _ => { + 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 Some(ContractFunctionState::Original); + return Ok(ContractFunctionState::Original); } } - None + Err(None) + } +} + +impl ContractFunctionState { + // If we didn't find any other contract handling related attributes we + // assume this function has not been touched by a contract before. + fn from_attributes(attributes: &[syn::Attribute]) -> Self { + attributes + .iter() + .find_map(|attr| { + let state = ContractFunctionState::try_from(attr); + if let Err(Some(diag)) = state { + diag.emit(); + None + } else { + state.ok() + } + }) + .unwrap_or(ContractFunctionState::Untouched) } /// Do we need to emit the `is_contract_generated` tag attribute on the @@ -190,95 +293,6 @@ impl ContractFunctionState { fn emit_tag_attr(self) -> bool { matches!(self, ContractFunctionState::Untouched) } - - /// This function decides whether we will be emitting a check function, a - /// replace function or both and emit a header into `output` if necessary. - /// - /// The return of this function essentially configures all the later parts - /// of code generation and is structured as follows: - /// `Some((Some((replace_function_name, use_dummy_function)), - /// Some(check_function_name)))`. Either function name being present tells - /// the codegen that that type of function should be emitted with the - /// respective name. `use_dummy_function` indicates whether we should use - /// the body of this function (`false`) or `kani::any` (`true`) as the - /// nested body of the replace function. `kani::any` is only used when we - /// generate a replace function for the first time. - /// - /// The following is going to happen depending on the state of `self` - /// - /// - On [`ContractFunctionState::Original`] we return an overall [`None`] - /// indicating to short circuit the code generation. - /// - On [`ContractFunctionState::Replace`] and - /// [`ContractFunctionState::Check`] we return [`Some`] for one of the - /// tuple fields, indicating that only this type of function should be - /// emitted. - /// - On [`ContractFunctionState::Untouched`] we return [`Some`] for both - /// tuple fields, indicating that both functions need to be emitted. We - /// also emit the original function with the `checked_with` and - /// `replaced_with` attributes added. - /// - /// The only reason the `item_fn` is mutable is I'm using `std::mem::swap` - /// to avoid making copies. - fn prepare_header( - self, - item_fn: &mut ItemFn, - output: &mut TokenStream2, - a_short_hash: u64, - ) -> Option<(Option<(Ident, bool)>, Option)> { - match self { - ContractFunctionState::Untouched => { - // We are the first time a contract is handled on this function, so - // we're responsible for - // - // 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 - - let check_fn_name = - identifier_for_generated_function(item_fn, "check", a_short_hash); - let replace_fn_name = - identifier_for_generated_function(item_fn, "replace", a_short_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 check_fn_name_str = - syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); - - // 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`. - // - // We're emitting the original here but the same applies later when we - // emit the check function. - let mut attrs = vec![]; - swapped!(&mut item_fn.attrs, &mut attrs, { - output.extend(quote!( - #(#attrs)* - #[kanitool::checked_with = #check_fn_name_str] - #[kanitool::replaced_with = #replace_fn_name_str] - #item_fn - )); - }); - Some((Some((replace_fn_name, true)), Some(check_fn_name))) - } - ContractFunctionState::Original => None, - ContractFunctionState::Check => Some((None, Some(item_fn.sig.ident.clone()))), - ContractFunctionState::Replace => { - Some((Some((item_fn.sig.ident.clone(), false)), None)) - } - } - } } /// A visitor which injects a copy of the token stream it holds before every @@ -358,15 +372,18 @@ fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap /// The information needed to generate the bodies of check and replacement /// functions that integrate the conditions from this contract attribute. -struct ContractConditionsHandler { +struct ContractConditionsHandler<'a> { + function_state: ContractFunctionState, /// Information specific to the type of contract attribute we're expanding. condition_type: ContractConditionsType, /// The contents of the attribute. attr: Expr, /// Body of the function this attribute was found on. - body: Block, + 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: &'a mut TokenStream2, } /// Information needed for generating check and replace handlers for different @@ -388,42 +405,42 @@ impl ContractConditionsType { /// `argument_names`. fn new_ensures(sig: &Signature, attr: &mut Expr) -> Self { let argument_names = rename_argument_occurrences(sig, attr); - ContractConditionsType::Ensures { argument_names } } } -impl ContractConditionsHandler { +impl<'a> ContractConditionsHandler<'a> { /// Initialize the handler. Constructs the required /// [`ContractConditionsType`] depending on `is_requires`. fn new( + function_state: ContractFunctionState, is_requires: bool, mut attr: Expr, - fn_sig: &Signature, - fn_body: Block, + annotated_fn: &'a ItemFn, attr_copy: TokenStream2, + output: &'a mut TokenStream2, ) -> Self { let condition_type = if is_requires { ContractConditionsType::Requires } else { - ContractConditionsType::new_ensures(fn_sig, &mut attr) + ContractConditionsType::new_ensures(&annotated_fn.sig, &mut attr) }; - Self { condition_type, attr, body: fn_body, attr_copy } + Self { function_state, condition_type, attr, annotated_fn, attr_copy, output } } /// Create the body of a check function. /// /// Wraps the conditions from this attribute around `self.body`. - fn make_check_body(&self, sig: &Signature) -> TokenStream2 { + fn make_check_body(&self) -> TokenStream2 { let attr = &self.attr; let attr_copy = &self.attr_copy; - let call_to_prior = &self.body; + let ItemFn { sig, block, .. } = self.annotated_fn; let return_type = return_type_to_type(&sig.output); match &self.condition_type { ContractConditionsType::Requires => quote!( kani::assume(#attr); - #call_to_prior + #block ), ContractConditionsType::Ensures { argument_names } => { let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); @@ -440,7 +457,7 @@ impl ContractConditionsHandler { // necessary but could lead to weird results if // `make_replace_body` were called after this if we modified in // place. - let mut call = call_to_prior.clone(); + let mut call = block.clone(); let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); inject_conditions.visit_block_mut(&mut call); @@ -457,13 +474,17 @@ impl ContractConditionsHandler { /// Create the body of a stub for this contract. /// /// Wraps the conditions from this attribute around a prior call. If - /// `use_dummy_fn` is `true` the prior call we wrap is `kani::any`, - /// otherwise `self.body`. - fn make_replace_body(&self, sig: &syn::Signature, use_dummy_fn_call: bool) -> TokenStream2 { + /// `use_nondet_result` is `true` we will use `kani::any()` to create a + /// result, otherwise whatever the `body` of our annotated function was. + /// + /// `use_nondet_result` will only be true if this is the first time we are + /// generating a replace function. + fn make_replace_body(&self, use_nondet_result: bool) -> TokenStream2 { let attr = &self.attr; let attr_copy = &self.attr_copy; + let ItemFn { sig, block, .. } = self.annotated_fn; let call_to_prior = - if use_dummy_fn_call { quote!(kani::any()) } else { self.body.to_token_stream() }; + if use_nondet_result { quote!(kani::any()) } else { block.to_token_stream() }; let return_type = return_type_to_type(&sig.output); match &self.condition_type { ContractConditionsType::Requires => quote!( @@ -482,8 +503,66 @@ impl ContractConditionsHandler { } } } + + /// Emit the check function into the output stream. + /// + /// See [`Self::make_check_body`] for the most interesting parts of this + /// function. + fn emit_check_function(&mut self, check_function_ident: Ident) { + 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)])); + } + let body = self.make_check_body(); + let mut sig = self.annotated_fn.sig.clone(); + sig.ident = check_function_ident; + self.output.extend(quote!( + #sig { + #body + } + )) + } + + /// Emit the replace funtion into the output stream. + /// + /// See [`Self::make_replace_body`] for the most interesting parts of this + /// function. + fn emit_replace_function(&mut self, replace_function_ident: Ident, use_nondet_result: bool) { + 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(); + let body = self.make_replace_body(use_nondet_result); + sig.ident = replace_function_ident; + + // Finally emit the check function itself. + self.output.extend(quote!( + #sig { + #body + } + )); + } + + /// Emit attributes common to check or replace function into the output + /// stream. + fn emit_common_header(&mut self) { + if self.function_state.emit_tag_attr() { + self.output.extend(quote!( + #[allow(dead_code, unused_variables)] + )); + } + self.output.extend(self.annotated_fn.attrs.iter().flat_map(Attribute::to_token_stream)); + } } +/// If an explicit return type was provided it is returned, otherwise `()`. fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { match return_type { syn::ReturnType::Default => Cow::Owned(syn::Type::Tuple(syn::TypeTuple { @@ -513,167 +592,106 @@ fn make_unsafe_argument_copies( /// The main meat of handling requires/ensures contracts. /// -/// Generates a "check" function used to verify the validity of the contract and -/// a "replace" function that can be used as a stub, generated from the contract -/// that can be used instead of the original function. -/// -/// Each clause (requires or ensures) after the first clause will be ignored on -/// the original function (detected by finding the `kanitool::checked_with` -/// attribute). On the check function (detected by finding the -/// `kanitool::is_contract_generated` attribute) it expands into a new layer of -/// pre- or postconditions. This state machine is also explained in more detail -/// in comments in the body of this macro. -/// -/// All named arguments of the function are unsafely shallow-copied with the -/// `kani::untracked_deref` function to circumvent the borrow checker for -/// postconditions. 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 function -/// -/// Generates a `check__` function that assumes preconditions -/// and asserts postconditions. The check function is also marked as generated -/// with the `#[kanitool::is_contract_generated(check)]` attribute. -/// -/// Decorates the original function with `#[kanitool::checked_by = -/// "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 -/// every `return` (see [`PostconditionInjector`]). Attributes on the original -/// function are also copied to the check function. -/// -/// ## Replace Function -/// -/// As the mirror to that also generates a `replace__` -/// function 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__"]`. -/// -/// The replace function has the same signature as the original function but its -/// body is replaced by `kani::any()`, which generates a non-deterministic -/// value. -/// -/// # Complete example -/// -/// ```rs -/// #[kani::requires(divisor != 0)] -/// #[kani::ensures(result <= dividend)] -/// fn div(dividend: u32, divisor: u32) -> u32 { -/// dividend / divisor -/// } -/// ``` -/// -/// Turns into -/// -/// ```rs -/// #[kanitool::checked_with = "div_check_965916"] -/// #[kanitool::replaced_with = "div_replace_965916"] -/// fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } -/// -/// #[allow(dead_code)] -/// #[allow(unused_variables)] -/// #[kanitool::is_contract_generated(check)] -/// fn div_check_965916(dividend: u32, divisor: u32) -> u32 { -/// let dividend_renamed = kani::untracked_deref(÷nd); -/// let divisor_renamed = kani::untracked_deref(&divisor); -/// let result = { kani::assume(divisor != 0); { dividend / divisor } }; -/// kani::assert(result <= dividend_renamed, "result <= dividend"); -/// std::mem::forget(dividend_renamed); -/// std::mem::forget(divisor_renamed); -/// result -/// } -/// -/// #[allow(dead_code)] -/// #[allow(unused_variables)] -/// #[kanitool::is_contract_generated(replace)] -/// fn div_replace_965916(dividend: u32, divisor: u32) -> u32 { -/// kani::assert(divisor != 0, "divisor != 0"); -/// let dividend_renamed = kani::untracked_deref(÷nd); -/// let divisor_renamed = kani::untracked_deref(&divisor); -/// let result = kani::any(); -/// kani::assume(result <= dividend_renamed, "result <= dividend"); -/// std::mem::forget(dividend_renamed); -/// std::mem::forget(divisor_renamed); -/// result -/// } -/// ``` -fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { +/// See the [module level documentation][self] for a description of how the code +/// generation works. +fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { let attr_copy = TokenStream2::from(attr.clone()); let attr = parse_macro_input!(attr as Expr); let mut output = proc_macro2::TokenStream::new(); + let item_stream_clone = item.clone(); + let item_fn = parse_macro_input!(item as ItemFn); - let a_short_hash = short_hash_of_token_stream(&item); - let mut item_fn = parse_macro_input!(item as ItemFn); + let function_state = ContractFunctionState::from_attributes(&item_fn.attrs); - // If we didn't find any other contract handling related attributes we - // assume this function has not been touched by a contract before. - let function_state = item_fn - .attrs - .iter() - .find_map(ContractFunctionState::from_attribute) - .unwrap_or(ContractFunctionState::Untouched); - - let Some((emit_replace, emit_check)) = - function_state.prepare_header(&mut item_fn, &mut output, a_short_hash) - else { + 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 outselves unchanged. + // 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 ItemFn { attrs, vis: _, mut sig, block } = item_fn; - let handler = ContractConditionsHandler::new(is_requires, attr, &sig, *block, attr_copy); - let emit_common_header = |output: &mut TokenStream2| { - if function_state.emit_tag_attr() { - output.extend(quote!( - #[allow(dead_code, unused_variables)] - )); - } - output.extend(attrs.iter().flat_map(Attribute::to_token_stream)); - }; - - if let Some((replace_name, dummy)) = emit_replace { - emit_common_header(&mut output); - - if 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. - output.extend(quote!(#[kanitool::is_contract_generated(replace)])); - } - let body = handler.make_replace_body(&sig, dummy); - sig.ident = replace_name; - - // Finally emit the check function itself. - output.extend(quote!( - #sig { - #body - } - )); } - if let Some(check_name) = emit_check { - emit_common_header(&mut output); + let mut handler = ContractConditionsHandler::new( + function_state, + is_requires, + attr, + &item_fn, + attr_copy, + &mut output, + ); + + match function_state { + 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. + handler.emit_check_function(item_fn.sig.ident.clone()); + } + ContractFunctionState::Replace => { + // Analogous to above + handler.emit_replace_function(item_fn.sig.ident.clone(), false); + } + ContractFunctionState::Original => { + unreachable!("Impossible: This is handled via short circuiting earlier.") + } + ContractFunctionState::Untouched => { + // The complex case. We are the first time a contract is handled on this function, so + // we're responsible for + // + // 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 + + // We'll be using this to postfix the generated names for the "check" + // and "replace" functions. + let a_short_hash = short_hash_of_token_stream(&item_stream_clone); + + let check_fn_name = identifier_for_generated_function(&item_fn, "check", a_short_hash); + let replace_fn_name = + identifier_for_generated_function(&item_fn, "replace", a_short_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 check_fn_name_str = syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); + + // 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 ItemFn { attrs, vis, sig, block } = &item_fn; + handler.output.extend(quote!( + #(#attrs)* + #[kanitool::checked_with = #check_fn_name_str] + #[kanitool::replaced_with = #replace_fn_name_str] + #vis #sig { + #block + } + )); - if 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. - output.extend(quote!(#[kanitool::is_contract_generated(check)])); + handler.emit_check_function(check_fn_name); + handler.emit_replace_function(replace_fn_name, true); } - let body = handler.make_check_body(&sig); - sig.ident = check_name; - output.extend(quote!( - #sig { - #body - } - )) } output.into() From 686b626061b6a2263ef48d37b797a53309faa80d Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 21 Sep 2023 11:48:56 -0700 Subject: [PATCH 18/26] Adding code review suggestions --- library/kani/src/contracts.rs | 6 ++++-- library/kani_macros/src/sysroot/contracts.rs | 6 +++--- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index 230f39682659..231eb9b8ca88 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -5,8 +5,10 @@ //! //! Function contracts are still under development. Using the APIs therefore //! requires the unstable `-Zfunction-contracts` flag to be passed. You can join -//! the discussion on contract design by commenting on [the -//! RFC](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html). +//! the discussion on contract design by reading our +//! [RFC](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html) +//! and [commenting on the tracking +//! issue](https://github.com/model-checking/kani/issues/2652). //! //! The function contract API is expressed as proc-macro attributes, and there //! are two parts to it. diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 97dd089756fb..bfc2a74d9e9f 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -655,11 +655,11 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool // We'll be using this to postfix the generated names for the "check" // and "replace" functions. - let a_short_hash = short_hash_of_token_stream(&item_stream_clone); + let item_hash = short_hash_of_token_stream(&item_stream_clone); - let check_fn_name = identifier_for_generated_function(&item_fn, "check", a_short_hash); + let check_fn_name = identifier_for_generated_function(&item_fn, "check", item_hash); let replace_fn_name = - identifier_for_generated_function(&item_fn, "replace", a_short_hash); + identifier_for_generated_function(&item_fn, "replace", item_hash); // Constructing string literals explicitly here, because `stringify!` // doesn't work. Let's say we have an identifier `check_fn` and we were From 5dc470bf353a3cdca185c4ee6667dd26db672d82 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 21 Sep 2023 12:12:46 -0700 Subject: [PATCH 19/26] Make the macro emit an `Arbitrary` bound for return types. --- library/kani_macros/src/lib.rs | 2 +- library/kani_macros/src/sysroot/contracts.rs | 77 +++++++++++++++---- .../type_annotation_needed.expected | 2 +- .../type_annotation_needed.rs | 2 +- 4 files changed, 66 insertions(+), 17 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 89482a6266ca..0ca34d521230 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -169,7 +169,7 @@ pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream { /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. -#[cfg(kani_sysroot)] +//#[cfg(kani_sysroot)] mod sysroot { use proc_macro_error::{abort, abort_call_site}; diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index bfc2a74d9e9f..1852d3871400 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -102,20 +102,18 @@ //! } //! ``` +use proc_macro::{Diagnostic, TokenStream}; +use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; +use quote::{quote, ToTokens}; use std::{ borrow::Cow, collections::{HashMap, HashSet}, }; - -use proc_macro::{Diagnostic, TokenStream}; - -use { - quote::{quote, ToTokens}, - syn::{parse_macro_input, spanned::Spanned, visit::Visit, Expr, ItemFn}, +use syn::{ + parse_macro_input, spanned::Spanned, visit::Visit, visit_mut::VisitMut, Attribute, Expr, + ItemFn, PredicateType, ReturnType, Signature, TraitBound, TypeParamBound, WhereClause, }; -use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; - /// 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) { @@ -134,8 +132,6 @@ fn hash_of_token_stream(hasher: &mut H, stream: proc_macro } } -use syn::{visit_mut::VisitMut, Attribute, Signature}; - /// Hash this `TokenStream` and return an integer that is at most digits /// long when hex formatted. fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 { @@ -530,7 +526,7 @@ impl<'a> ContractConditionsHandler<'a> { /// /// See [`Self::make_replace_body`] for the most interesting parts of this /// function. - fn emit_replace_function(&mut self, replace_function_ident: Ident, use_nondet_result: bool) { + fn emit_replace_function(&mut self, replace_function_ident: Ident, is_first_emit: bool) { self.emit_common_header(); if self.function_state.emit_tag_attr() { @@ -539,7 +535,10 @@ impl<'a> ContractConditionsHandler<'a> { self.output.extend(quote!(#[kanitool::is_contract_generated(replace)])); } let mut sig = self.annotated_fn.sig.clone(); - let body = self.make_replace_body(use_nondet_result); + if is_first_emit { + attach_require_kani_any(&mut sig); + } + let body = self.make_replace_body(is_first_emit); sig.ident = replace_function_ident; // Finally emit the check function itself. @@ -573,6 +572,57 @@ fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { } } +/// Looks complicated but does something very simple: attach a bound for +/// `kani::Arbitrary` on the return type to the provided signature. Pushes it +/// onto a preexisting where condition, initializing a new `where` condition if +/// it doesn't already exist. +/// +/// Very simple example: `fn foo() -> usize { .. }` would be rewritten `fn foo() +/// -> usize where usize: kani::Arbitrary { .. }`. +/// +/// This is called when we first emit a replace function. Later we can rely on +/// this bound already being present. +fn attach_require_kani_any(sig: &mut Signature) { + if matches!(sig.output, ReturnType::Default) { + // It's the default return type, e.g. `()` so we can skip adding the + // constraint. + return; + } + let return_ty = return_type_to_type(&sig.output); + let where_clause = sig.generics.where_clause.get_or_insert_with(|| WhereClause { + where_token: syn::Token![where](Span::call_site()), + predicates: Default::default(), + }); + + where_clause.predicates.push(syn::WherePredicate::Type(PredicateType { + lifetimes: None, + bounded_ty: return_ty.into_owned(), + colon_token: syn::Token![:](Span::call_site()), + bounds: [TypeParamBound::Trait(TraitBound { + paren_token: None, + modifier: syn::TraitBoundModifier::None, + lifetimes: None, + path: syn::Path { + leading_colon: None, + segments: [ + syn::PathSegment { + ident: Ident::new("kani", Span::call_site()), + arguments: syn::PathArguments::None, + }, + syn::PathSegment { + ident: Ident::new("Arbitrary", Span::call_site()), + arguments: syn::PathArguments::None, + }, + ] + .into_iter() + .collect(), + }, + })] + .into_iter() + .collect(), + })) +} + /// We make shallow copies of the argument for the postconditions in both /// `requires` and `ensures` clauses and later clean them up. /// @@ -658,8 +708,7 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool let item_hash = short_hash_of_token_stream(&item_stream_clone); let check_fn_name = identifier_for_generated_function(&item_fn, "check", item_hash); - let replace_fn_name = - identifier_for_generated_function(&item_fn, "replace", item_hash); + let replace_fn_name = identifier_for_generated_function(&item_fn, "replace", item_hash); // Constructing string literals explicitly here, because `stringify!` // doesn't work. Let's say we have an identifier `check_fn` and we were diff --git a/tests/expected/function-contract/type_annotation_needed.expected b/tests/expected/function-contract/type_annotation_needed.expected index 880f00714b32..34c886c358cb 100644 --- a/tests/expected/function-contract/type_annotation_needed.expected +++ b/tests/expected/function-contract/type_annotation_needed.expected @@ -1 +1 @@ -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/type_annotation_needed.rs b/tests/expected/function-contract/type_annotation_needed.rs index 2123162fdded..09b20443d47b 100644 --- a/tests/expected/function-contract/type_annotation_needed.rs +++ b/tests/expected/function-contract/type_annotation_needed.rs @@ -3,7 +3,7 @@ // kani-flags: -Zfunction-contracts #[kani::ensures(result.is_some())] -fn or_default(opt: Option) -> Option { +fn or_default(opt: Option) -> Option { opt.or(Some(T::default())) } From 9ae06e4c39855815245c3bffed1277d8fce77263 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 21 Sep 2023 12:23:14 -0700 Subject: [PATCH 20/26] Hehe --- library/kani_macros/src/lib.rs | 2 +- library/kani_macros/src/sysroot/contracts.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 0ca34d521230..89482a6266ca 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -169,7 +169,7 @@ pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream { /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. -//#[cfg(kani_sysroot)] +#[cfg(kani_sysroot)] mod sysroot { use proc_macro_error::{abort, abort_call_site}; diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 1852d3871400..b2c60da2a47f 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -576,10 +576,10 @@ fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { /// `kani::Arbitrary` on the return type to the provided signature. Pushes it /// onto a preexisting where condition, initializing a new `where` condition if /// it doesn't already exist. -/// +/// /// Very simple example: `fn foo() -> usize { .. }` would be rewritten `fn foo() /// -> usize where usize: kani::Arbitrary { .. }`. -/// +/// /// This is called when we first emit a replace function. Later we can rely on /// this bound already being present. fn attach_require_kani_any(sig: &mut Signature) { From 82121c5bfd4a5a416411636a56c069ff1e093953 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 26 Sep 2023 09:25:03 -0400 Subject: [PATCH 21/26] Remove unused shadowing statement. --- library/kani_macros/src/sysroot/contracts.rs | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index b2c60da2a47f..6ae58feb449a 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -312,7 +312,7 @@ impl ContractFunctionState { struct PostconditionInjector(TokenStream2); impl VisitMut for PostconditionInjector { - /// We leave this emtpy to stop the recursion here. We don't want to look + /// We leave this empty to stop the recursion here. We don't want to look /// inside the closure, because the return statements contained within are /// for a different function. fn visit_expr_closure_mut(&mut self, _: &mut syn::ExprClosure) {} @@ -429,10 +429,10 @@ impl<'a> ContractConditionsHandler<'a> { /// /// Wraps the conditions from this attribute around `self.body`. fn make_check_body(&self) -> TokenStream2 { - let attr = &self.attr; - let attr_copy = &self.attr_copy; + let Self { attr, attr_copy, .. } = self; let ItemFn { sig, block, .. } = self.annotated_fn; let return_type = return_type_to_type(&sig.output); + match &self.condition_type { ContractConditionsType::Requires => quote!( kani::assume(#attr); @@ -440,7 +440,6 @@ impl<'a> ContractConditionsHandler<'a> { ), ContractConditionsType::Ensures { argument_names } => { let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); - let attr = &self.attr; // The code that enforces the postconditions and cleans up the shallow // argument copies (with `mem::forget`). @@ -454,9 +453,9 @@ impl<'a> ContractConditionsHandler<'a> { // `make_replace_body` were called after this if we modified in // place. let mut call = block.clone(); - let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); inject_conditions.visit_block_mut(&mut call); + quote!( #arg_copies let result : #return_type = #call; @@ -476,12 +475,12 @@ 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, use_nondet_result: bool) -> TokenStream2 { - let attr = &self.attr; - let attr_copy = &self.attr_copy; + let Self { attr, attr_copy, .. } = self; let ItemFn { sig, block, .. } = self.annotated_fn; let call_to_prior = if use_nondet_result { quote!(kani::any()) } else { block.to_token_stream() }; let return_type = return_type_to_type(&sig.output); + match &self.condition_type { ContractConditionsType::Requires => quote!( kani::assert(#attr, stringify!(#attr_copy)); From 54bdfeec5a86c061c7d0d8101c089b3ed9987458 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 26 Sep 2023 13:12:19 -0400 Subject: [PATCH 22/26] Expand the doc even more --- library/kani_macros/src/sysroot/contracts.rs | 94 ++++++++++++++++---- 1 file changed, 79 insertions(+), 15 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 6ae58feb449a..3a5f244c682e 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -11,23 +11,87 @@ //! on the same function correctly. //! //! ## How the handling for `requires` 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 +//! stub, generated from the contract that can be used instead of the original +//! function. +//! +//! Let me first introduce the constraints which we are operating under to +//! explain why we need the somewhat involved state machine to achieve this. +//! +//! Proc-macros are expanded one-at-a-time, outside-in and they can also be +//! renamed. Meaning the user can do `use kani::requires as precondition` and +//! then use `precondition` everywhere. We want to support this functionality +//! 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 +//! further contract attributes to compose with what was already generated. In +//! 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 +//! carried by the attribute currently being expanded. We copy all additional +//! attributes from the original function to both the "check" and the "replace". +//! This allows us to deal both with renaming and also support non-contract +//! attributes. +//! +//! In addition to copying attributes we also add new marker attributes to +//! advance the state machine. The "check" function 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 +//! `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 +//! 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. +//! +//! We place marker attributes at the bottom of the attribute stack (innermost), +//! otherwise they would not be visible to the future macro expansions. //! -//! We generate a "check" function used to verify the validity of the contract -//! and a "replace" function that can be used as a stub, generated from the -//! contract that can be used instead of the original function. +//! Below you can see a graphical rendering where boxes are states and each +//! arrow represents the expansion of a `requires` or `ensures` macro. //! -//! Each clause (requires or ensures) after the first clause will be ignored on -//! the original function (detected by finding the `kanitool::checked_with` -//! attribute). On the check function (detected by finding the -//! `kanitool::is_contract_generated` attribute) it expands into a new layer of -//! pre- or postconditions. This state machine is also explained in more detail -//! in code comments. +//! ```plain +//! v +//! +-----------+ +//! | Untouched | +//! | Function | +//! +-----+-----+ +//! | +//! Emit | Generate + Copy Attributes +//! +-----------------+------------------+ +//! | | | +//! | | | +//! v v v +//! +----------+ +-------+ +---------+ +//! | Original |<-+ | Check |<-+ | Replace |<-+ +//! +--+-------+ | +---+---+ | +----+----+ | +//! | | Ignore | | Augment | | Augment +//! +----------+ +------+ +-------+ +//! +//! | | | | +//! +--------------+ +------------------------------+ +//! Presence of Presence of +//! "checked_with" "is_contract_generated" +//! +//! State is detected via +//! ``` //! //! All named arguments of the annotated function are unsafely shallow-copied //! with the `kani::untracked_deref` function to circumvent the borrow checker -//! for postconditions. We must ensure that those copies are not dropped -//! (causing a double-free) so after the postconditions we call `mem::forget` on -//! each copy. +//! 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 function //! @@ -59,7 +123,7 @@ //! //! # Complete example //! -//! ```rs +//! ``` //! #[kani::requires(divisor != 0)] //! #[kani::ensures(result <= dividend)] //! fn div(dividend: u32, divisor: u32) -> u32 { @@ -69,7 +133,7 @@ //! //! Turns into //! -//! ```rs +//! ``` //! #[kanitool::checked_with = "div_check_965916"] //! #[kanitool::replaced_with = "div_replace_965916"] //! fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } @@ -193,7 +257,7 @@ impl<'a> VisitMut for Renamer<'a> { /// This restores shadowing. Without this we would rename all ident /// occurrences, but not rebinding location. This is because our - /// [`visit_expr_path_mut`] is scope-unaware. + /// [`Self::visit_expr_path_mut`] is scope-unaware. fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) { if let Some(new) = self.0.get(&i.ident) { i.ident = new.clone(); From 415a0f5f13e6d3d9a931316c6b93b5884dd9b87e Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 26 Sep 2023 15:18:01 -0400 Subject: [PATCH 23/26] Apply suggestions from code review Co-authored-by: Felipe R. Monteiro --- library/kani/src/contracts.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index 231eb9b8ca88..8a99f4892b0a 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -73,7 +73,7 @@ //! } //! ``` //! -//! Once we are finished specifying our contract we can ask kani to check it's +//! Once we are finished specifying our contract we can ask Kani to check it's //! validity. For this we need to provide a proof harness that exercises the //! function. The harness is created like any other, e.g. as a test-like //! function with inputs and using `kani::any` to create arbitrary values. @@ -134,7 +134,7 @@ //! one specification attribute is considered to "have a contract" and any //! absent specification type defaults to its most general interpretation //! (`true`). All functions with not a single specification attribute are -//! considered " not to "have a contract" and are ineligible for use as the +//! considered "not to have a contract" and are ineligible for use as the //! target of a [`proof_for_contract`][macro@proof_for_contract] of //! [`stub_verified`][macro@stub_verified] attribute. //! From f2a93de3c4d48942b374d78a6952b69e91e1912a Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 26 Sep 2023 15:18:16 -0400 Subject: [PATCH 24/26] Formatting --- kani-compiler/src/kani_middle/attributes.rs | 2 +- library/kani_macros/src/lib.rs | 2 +- library/kani_macros/src/sysroot/contracts.rs | 16 ++++++++-------- .../missing_contract_for_replace.expected | 1 - 4 files changed, 10 insertions(+), 11 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index d6d5929d10a9..2c9c6d7ee54c 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -159,7 +159,7 @@ impl<'tcx> KaniAttributes<'tcx> { let ok = self.resolve_sibling(name.as_str()).map_err(|e| { self.tcx.sess.span_err( attr.span, - format!("Could not resolve replacement function {}: {e}", name.as_str()), + format!("Failed to resolve replacement function {}: {e}", name.as_str()), ) })?; Ok((name, ok, attr.span)) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 89482a6266ca..0ca34d521230 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -169,7 +169,7 @@ pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream { /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. -#[cfg(kani_sysroot)] +//#[cfg(kani_sysroot)] mod sysroot { use proc_macro_error::{abort, abort_call_site}; diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 3a5f244c682e..7670bc0f2b33 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -11,15 +11,15 @@ //! on the same function correctly. //! //! ## How the handling for `requires` 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 //! stub, generated from the contract that can be used instead of the original //! function. -//! +//! //! Let me first introduce the constraints which we are operating under to //! explain why we need the somewhat involved state machine to achieve this. -//! +//! //! Proc-macros are expanded one-at-a-time, outside-in and they can also be //! renamed. Meaning the user can do `use kani::requires as precondition` and //! then use `precondition` everywhere. We want to support this functionality @@ -30,7 +30,7 @@ //! further contract attributes to compose with what was already generated. In //! 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` @@ -40,7 +40,7 @@ //! attributes from the original function to both the "check" and the "replace". //! This allows us to deal both with renaming and also support non-contract //! attributes. -//! +//! //! In addition to copying attributes we also add new marker attributes to //! advance the state machine. The "check" function gets a //! `kanitool::is_contract_generated(check)` attributes and analogous for @@ -52,7 +52,7 @@ //! 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. -//! +//! //! We place marker attributes at the bottom of the attribute stack (innermost), //! otherwise they would not be visible to the future macro expansions. //! @@ -76,12 +76,12 @@ //! +--+-------+ | +---+---+ | +----+----+ | //! | | Ignore | | Augment | | Augment //! +----------+ +------+ +-------+ -//! +//! //! | | | | //! +--------------+ +------------------------------+ //! Presence of Presence of //! "checked_with" "is_contract_generated" -//! +//! //! State is detected via //! ``` //! diff --git a/tests/expected/function-contract/missing_contract_for_replace.expected b/tests/expected/function-contract/missing_contract_for_replace.expected index d34061fff160..29f3fa955307 100644 --- a/tests/expected/function-contract/missing_contract_for_replace.expected +++ b/tests/expected/function-contract/missing_contract_for_replace.expected @@ -7,4 +7,3 @@ note: Try adding a contract to this function or use the unsound `stub` attribute | 5 | fn no_contract() {} | ^^^^^^^^^^^^^^^^ - \ No newline at end of file From 85f59c7bfbbd9ee6db5d3c1738ce9bae43202cc3 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 26 Sep 2023 15:20:03 -0400 Subject: [PATCH 25/26] Committed wrong file --- library/kani_macros/src/lib.rs | 2 +- .../function-contract/missing_contract_for_check.expected | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 0ca34d521230..89482a6266ca 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -169,7 +169,7 @@ pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream { /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. -//#[cfg(kani_sysroot)] +#[cfg(kani_sysroot)] mod sysroot { use proc_macro_error::{abort, abort_call_site}; diff --git a/tests/expected/function-contract/missing_contract_for_check.expected b/tests/expected/function-contract/missing_contract_for_check.expected index 0b2f20cac7f7..6836fb06f0a6 100644 --- a/tests/expected/function-contract/missing_contract_for_check.expected +++ b/tests/expected/function-contract/missing_contract_for_check.expected @@ -7,4 +7,3 @@ note: Try adding a contract to this function. | 5 | fn no_contract() {} | ^^^^^^^^^^^^^^^^ - \ No newline at end of file From d32e6514caec841b6dc49a2e7d1ab7883732e51d Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 26 Sep 2023 15:20:51 -0400 Subject: [PATCH 26/26] Update library/kani_macros/src/sysroot/contracts.rs Co-authored-by: Felipe R. Monteiro --- library/kani_macros/src/sysroot/contracts.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 7670bc0f2b33..242d3e4deba0 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -442,7 +442,7 @@ struct ContractConditionsHandler<'a> { 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 + /// The stream to which we should write the generated code. output: &'a mut TokenStream2, }