From dba16744ee1d9299b379d9f876c28a8d07376933 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 27 Sep 2023 14:05:30 -0400 Subject: [PATCH] Simple Stubbing with Contracts (#2746) ### Description of changes: Expands the contract features introduced in #2655 by completing the checking with stubbing/replacement capabilities. ### Resolved issues: Resolves #2621 ### Related RFC: [0009 Function Contracts](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val Co-authored-by: Felipe R. Monteiro --- kani-compiler/src/kani_middle/attributes.rs | 185 ++++- library/kani/src/contracts.rs | 173 ++++ library/kani/src/lib.rs | 4 +- library/kani_macros/src/lib.rs | 60 +- library/kani_macros/src/sysroot/contracts.rs | 767 +++++++++++++----- .../gcd_replacement_fail.expected | 17 + .../function-contract/gcd_replacement_fail.rs | 67 ++ .../gcd_replacement_pass.expected | 17 + .../function-contract/gcd_replacement_pass.rs | 67 ++ .../missing_contract_for_check.expected | 9 + .../missing_contract_for_check.rs | 10 + .../missing_contract_for_replace.expected | 9 + .../missing_contract_for_replace.rs | 11 + .../allowed_mut_return_ref.rs | 17 +- .../prohibit-pointers/return_pointer.rs | 12 +- .../simple_replace_fail.expected | 3 + .../function-contract/simple_replace_fail.rs | 15 + .../simple_replace_pass.expected | 9 + .../function-contract/simple_replace_pass.rs | 15 + .../type_annotation_needed.expected | 1 + .../type_annotation_needed.rs | 14 + 21 files changed, 1225 insertions(+), 257 deletions(-) create mode 100644 library/kani/src/contracts.rs 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/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 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 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/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index d1ef8fdf33e3..2c9c6d7ee54c 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")] @@ -31,6 +31,9 @@ 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 /// before the the verification runs. @@ -38,6 +41,10 @@ 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. IsContractGenerated, @@ -52,8 +59,10 @@ impl KaniAttributeKind { | KaniAttributeKind::Solver | KaniAttributeKind::Stub | KaniAttributeKind::ProofForContract + | KaniAttributeKind::StubVerified | KaniAttributeKind::Unwind => true, KaniAttributeKind::Unstable + | KaniAttributeKind::ReplacedWith | KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => false, } @@ -134,6 +143,30 @@ impl<'tcx> KaniAttributes<'tcx> { } } + /// 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) + .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!("Failed to resolve replacement function {}: {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). @@ -142,30 +175,50 @@ 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 checking function {} because {resolve_err}", + name.as_str() + ), + ) + }, + ) }) } - /// 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, + 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. @@ -223,7 +276,10 @@ impl<'tcx> KaniAttributes<'tcx> { } expect_single(self.tcx, kind, &attrs); } - KaniAttributeKind::CheckedWith => { + 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)); } @@ -325,38 +381,87 @@ 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 - .span_err(span, "Target function for this check has no contract"); - return harness; - }; - 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!() } - KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => { - todo!("Contract attributes are not supported on proofs") + KaniAttributeKind::CheckedWith + | KaniAttributeKind::IsContractGenerated + | KaniAttributeKind::ReplacedWith => { + 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 }) } + 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), "Try adding a contract to this function.") + .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), + format!( + "Try adding a contract to this function or use the unsound `{}` attribute instead.", + KaniAttributeKind::Stub.as_ref(), + ) + ) + .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/library/kani/src/contracts.rs b/library/kani/src/contracts.rs new file mode 100644 index 000000000000..8a99f4892b0a --- /dev/null +++ b/library/kani/src/contracts.rs @@ -0,0 +1,173 @@ +// 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 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. +//! +//! 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 3b4ea87636f3..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,24 +142,31 @@ 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`][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`. +/// +/// 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. +/// +/// 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) +} + /// 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,7 @@ 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 +349,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..242d3e4deba0 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -1,15 +1,182 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use std::collections::{HashMap, HashSet}; - -use proc_macro::TokenStream; - -use { - quote::{quote, ToTokens}, - syn::{parse_macro_input, spanned::Spanned, visit::Visit, Expr, ItemFn}, -}; +//! 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. +//! +//! 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. +//! +//! Below you can see a graphical rendering where boxes are states and each +//! arrow represents the expansion of a `requires` or `ensures` macro. +//! +//! ```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. 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 +//! +//! 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 +//! +//! ``` +//! #[kani::requires(divisor != 0)] +//! #[kani::ensures(result <= dividend)] +//! fn div(dividend: u32, divisor: u32) -> u32 { +//! dividend / divisor +//! } +//! ``` +//! +//! Turns into +//! +//! ``` +//! #[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 proc_macro::{Diagnostic, TokenStream}; use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; +use quote::{quote, ToTokens}; +use std::{ + borrow::Cow, + collections::{HashMap, HashSet}, +}; +use syn::{ + parse_macro_input, spanned::Spanned, visit::Visit, visit_mut::VisitMut, Attribute, Expr, + ItemFn, PredicateType, ReturnType, Signature, TraitBound, TypeParamBound, WhereClause, +}; /// Create a unique hash for a token stream (basically a [`std::hash::Hash`] /// impl for `proc_macro2::TokenStream`). @@ -29,8 +196,6 @@ fn hash_of_token_stream(hasher: &mut H, stream: proc_macro } } -use syn::visit_mut::VisitMut; - /// 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 { @@ -50,11 +215,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. @@ -92,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(); @@ -120,7 +285,7 @@ where && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) } -/// Classifies the state a function is in the contract handling pipeline. +/// 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,34 +296,62 @@ 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 { +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(); + 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"))) } - Ok(ident) => { - if ident.to_string() == "check" { - return Some(Self::Check); - } else { - lst.span().unwrap().error("Expected `check` ident").emit(); - } - } - } + }; } } 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 + /// generated function(s)? + fn emit_tag_attr(self) -> bool { + matches!(self, ContractFunctionState::Untouched) } } @@ -183,7 +376,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) {} @@ -218,7 +411,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,179 +430,382 @@ fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap< arg_idents } -/// The main meat of handling requires/ensures contracts. -/// -/// 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. 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. -/// -/// # Complete example +/// The information needed to generate the bodies of check and replacement +/// functions that integrate the conditions from this contract attribute. +struct ContractConditionsHandler<'a> { + function_state: ContractFunctionState, + /// Information specific to the type of contract attribute we're expanding. + condition_type: ContractConditionsType, + /// The contents of the attribute. + attr: Expr, + /// Body of the function this attribute was found on. + 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 +/// contract attributes. +enum ContractConditionsType { + Requires, + 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 argument_names = rename_argument_occurrences(sig, attr); + ContractConditionsType::Ensures { argument_names } + } +} + +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, + annotated_fn: &'a ItemFn, + attr_copy: TokenStream2, + output: &'a mut TokenStream2, + ) -> Self { + let condition_type = if is_requires { + ContractConditionsType::Requires + } else { + ContractConditionsType::new_ensures(&annotated_fn.sig, &mut attr) + }; + + 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) -> TokenStream2 { + 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); + #block + ), + ContractConditionsType::Ensures { argument_names } => { + let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); + + // The code that enforces the postconditions and cleans up the shallow + // argument copies (with `mem::forget`). + let exec_postconditions = quote!( + kani::assert(#attr, stringify!(#attr_copy)); + #copy_clean + ); + + // 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 = 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; + #exec_postconditions + result + ) + } + } + } + + /// Create the body of a stub for this contract. + /// + /// Wraps the conditions from this attribute around a prior call. If + /// `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 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)); + #call_to_prior + ), + ContractConditionsType::Ensures { argument_names } => { + let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); + quote!( + #arg_copies + let result: #return_type = #call_to_prior; + kani::assume(#attr); + #copy_clean + result + ) + } + } + } + + /// 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, is_first_emit: 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(); + 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. + 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 { + paren_token: syn::token::Paren::default(), + elems: Default::default(), + })), + syn::ReturnType::Type(_, typ) => Cow::Borrowed(typ.as_ref()), + } +} + +/// 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. /// -/// ```rs -/// #[kani::requires(divisor != 0)] -/// #[kani::ensures(result <= dividend)] -/// fn div(dividend: u32, divisor: u32) -> u32 { -/// dividend / divisor -/// } -/// ``` +/// Very simple example: `fn foo() -> usize { .. }` would be rewritten `fn foo() +/// -> usize where usize: kani::Arbitrary { .. }`. /// -/// Turns into +/// 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. /// -/// ```rs -/// #[kanitool::checked_with = "div_check_965916"] -/// fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } +/// 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. /// -/// #[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 -/// } -/// ``` -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); +/// 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 item_fn = &mut 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. - let function_state = item_fn - .attrs - .iter() - .find_map(ContractFunctionState::from_attribute) - .unwrap_or(ContractFunctionState::Untouched); + let function_state = ContractFunctionState::from_attributes(&item_fn.attrs); if matches!(function_state, ContractFunctionState::Original) { // If we're the original function that means we're *not* the first time // that a contract attribute is handled on this function. This means // there must exist a generated check function somewhere onto which the // attributes have been copied and where they will be expanded into more - // checks. So we just return 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 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 - - #[allow(dead_code)] - #[allow(unused_variables)] - )); - item_fn.sig.ident = check_fn_name; - } + 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 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); + + // 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 + } + )); - 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 - ) - }; - - let sig = &item_fn.sig; - - // Prepare emitting the check function by emitting the rest of the - // attributes. - output.extend(quote!( - #(#attrs)* - )); - - if matches!(function_state, ContractFunctionState::Untouched) { - // 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); + } } - // Finally emit the check function itself. - output.extend(quote!( - #sig { - #check_body - } - )); output.into() } @@ -436,4 +832,5 @@ 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 new file mode 100644 index 000000000000..a993325bd5e5 --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_fail.expected @@ -0,0 +1,17 @@ +Frac::check_equals.assertion\ +- 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" + +Frac::check_equals.assertion\ +- 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 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..8bd59c5c14fe --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_fail.rs @@ -0,0 +1,67 @@ +// 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() { + 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..48d3565ef9f1 --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_pass.expected @@ -0,0 +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/gcd_replacement_pass.rs b/tests/expected/function-contract/gcd_replacement_pass.rs new file mode 100644 index 000000000000..9827dd3a1512 --- /dev/null +++ b/tests/expected/function-contract/gcd_replacement_pass.rs @@ -0,0 +1,67 @@ +// 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() { + 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/missing_contract_for_check.expected b/tests/expected/function-contract/missing_contract_for_check.expected new file mode 100644 index 000000000000..6836fb06f0a6 --- /dev/null +++ b/tests/expected/function-contract/missing_contract_for_check.expected @@ -0,0 +1,9 @@ +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. + | +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..29f3fa955307 --- /dev/null +++ b/tests/expected/function-contract/missing_contract_for_replace.expected @@ -0,0 +1,9 @@ +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 or use the unsound `stub` attribute instead. + | +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(); +} 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!() } 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..b6806befc22c --- /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"" 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..33a531a3aef7 --- /dev/null +++ b/tests/expected/function-contract/simple_replace_fail.rs @@ -0,0 +1,15 @@ +// 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() { + 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..e1fc78ca462f --- /dev/null +++ b/tests/expected/function-contract/simple_replace_pass.expected @@ -0,0 +1,9 @@ +div.assertion\ +- Status: SUCCESS\ +- Description: "divisor != 0" + +main.assertion\ +- Status: SUCCESS\ +- Description: ""contract guarantees smallness"" + +VERIFICATION:- SUCCESSFUL 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..0dcc6cd59fe3 --- /dev/null +++ b/tests/expected/function-contract/simple_replace_pass.rs @@ -0,0 +1,15 @@ +// 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() { + assert!(div(9, 1) != 10, "contract guarantees smallness"); +} 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..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/type_annotation_needed.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL 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..09b20443d47b --- /dev/null +++ b/tests/expected/function-contract/type_annotation_needed.rs @@ -0,0 +1,14 @@ +// 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); +}