From 2d32361cb1b8f960c119279e429a58bb295d14e3 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 17 Oct 2023 19:50:59 -0400 Subject: [PATCH] Support for inductively verifying contracts of recursive functions (#2809) This adds support for verifying the contracts of recursive functions inductively. The idea is quite simple. We use a global variable to track whether we're reentering a function and depending on that value we either continue with checking the contract or assume the hypothesis by using its replacement. The precise mechanism that I implemented is explained in the documentation [here](https://github.com/JustusAdam/kani/blob/a31176c79098205ca0b2c2b199cdf06653754551/library/kani_macros/src/sysroot/contracts.rs#L126) Resolves #2724 **Open Question:** to facilitate induction the return type of the function must implement `kani::Arbitrary`. Since we can't discriminate between recursive and non-recursive functions in the proc-macro this means that this applies to all functions with contracts, not just recursive ones. This may be an unacceptable restriction. We could consider making inductive verification explicit with an annotation like `#[kani::inductive]` or conversely make inductive the default and let users opt-out with `#[kani::no_inductive]`. This is now tracked in #2823 I had to remove the names of the functions in which the messages occur in the test cases, since they are now generated, hard to read names 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: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/kani/src/contracts.rs | 23 +- library/kani_macros/src/sysroot/contracts.rs | 302 ++++++++++++++++-- scripts/kani-regression.sh | 3 + .../arbitrary_ensures_fail.expected | 2 +- .../arbitrary_ensures_pass.expected | 2 +- .../arbitrary_requires_pass.expected | 2 +- .../function-contract/fail_on_two.expected | 12 + .../expected/function-contract/fail_on_two.rs | 44 +++ .../gcd_failure_code.expected | 2 +- .../gcd_failure_contract.expected | 2 +- .../gcd_rec_code_fail.expected | 3 + .../function-contract/gcd_rec_code_fail.rs | 24 ++ .../gcd_rec_comparison_pass.expected | 9 + .../gcd_rec_comparison_pass.rs | 68 ++++ .../gcd_rec_contract_fail.expected | 3 + .../gcd_rec_contract_fail.rs | 25 ++ .../gcd_rec_replacement_pass.expected | 17 + .../gcd_rec_replacement_pass.rs | 68 ++++ .../gcd_rec_simple_pass.expected | 9 + .../function-contract/gcd_rec_simple_pass.rs | 25 ++ .../function-contract/gcd_success.expected | 2 +- .../simple_ensures_fail.expected | 2 +- .../simple_ensures_pass.expected | 2 +- 23 files changed, 611 insertions(+), 40 deletions(-) create mode 100644 tests/expected/function-contract/fail_on_two.expected create mode 100644 tests/expected/function-contract/fail_on_two.rs create mode 100644 tests/expected/function-contract/gcd_rec_code_fail.expected create mode 100644 tests/expected/function-contract/gcd_rec_code_fail.rs create mode 100644 tests/expected/function-contract/gcd_rec_comparison_pass.expected create mode 100644 tests/expected/function-contract/gcd_rec_comparison_pass.rs create mode 100644 tests/expected/function-contract/gcd_rec_contract_fail.expected create mode 100644 tests/expected/function-contract/gcd_rec_contract_fail.rs create mode 100644 tests/expected/function-contract/gcd_rec_replacement_pass.expected create mode 100644 tests/expected/function-contract/gcd_rec_replacement_pass.rs create mode 100644 tests/expected/function-contract/gcd_rec_simple_pass.expected create mode 100644 tests/expected/function-contract/gcd_rec_simple_pass.rs diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index 8a99f4892b0a..a211a8ba905c 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -134,8 +134,8 @@ //! 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 +//! 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 @@ -170,4 +170,23 @@ //! //! Unlike `proof_for_contract` multiple `stub_verified` attributes are allowed //! on the same proof harness though they must target different functions. +//! +//! ## Inductive Verification +//! +//! Function contracts by default use inductive verification to efficiently +//! verify recursive functions. In inductive verification a recursive function +//! is executed once and every recursive call instead uses the contract +//! replacement. In this way many recursive calls can be checked with a +//! single verification pass. +//! +//! The downside of inductive verification is that the return value of a +//! contracted function must implement `kani::Arbitrary`. Due to restrictions to +//! code generation in proc macros, the contract macros cannot determine reliably +//! in all cases whether a given function with a contract is recursive. As a +//! result it conservatively sets up inductive verification for every function +//! and requires the `kani::Arbitrary` constraint for contract checks. +//! +//! If you feel strongly about this issue you can join the discussion on issue +//! [#2823](https://github.com/model-checking/kani/issues/2823) to enable +//! opt-out of inductive verification. pub use super::{ensures, proof_for_contract, requires, stub_verified}; diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 242d3e4deba0..a497e0ca8cee 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -60,29 +60,31 @@ //! 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 +//! │ Start +//! ▼ +//! ┌───────────┐ +//! │ Untouched │ +//! │ Function │ +//! └─────┬─────┘ +//! │ +//! Emit │ Generate + Copy Attributes +//! ┌─────────────────┴─────┬──────────┬─────────────────┐ +//! │ │ │ │ +//! │ │ │ │ +//! ▼ ▼ ▼ ▼ +//! ┌──────────┐ ┌───────────┐ ┌───────┐ ┌─────────┐ +//! │ Original │◄─┐ │ Recursion │ │ Check │◄─┐ │ Replace │◄─┐ +//! └──┬───────┘ │ │ Wrapper │ └───┬───┘ │ └────┬────┘ │ +//! │ │ Ignore └───────────┘ │ │ Augment │ │ Augment +//! └──────────┘ └──────┘ └───────┘ +//! +//! │ │ │ │ +//! └───────────────┘ └─────────────────────────────────────────────┘ +//! +//! Presence of Presence of +//! "checked_with" "is_contract_generated" +//! +//! State is detected via //! ``` //! //! All named arguments of the annotated function are unsafely shallow-copied @@ -95,12 +97,12 @@ //! //! ## Check function //! -//! Generates a `check__` function that assumes preconditions +//! 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 @@ -109,18 +111,64 @@ //! //! ## Replace Function //! -//! As the mirror to that also generates a `replace__` +//! 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__"]`. +//! "_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. //! +//! ## Inductive Verification +//! +//! To efficiently check recursive functions we verify them inductively. To +//! be able to do this we need both the check and replace functions we have seen +//! before. +//! +//! Inductive verification is comprised of a hypothesis and an induction step. +//! The hypothesis in this case is the replace function. It represents the +//! assumption that the contracts holds if the preconditions are satisfied. The +//! induction step is the check function, which ensures that the contract holds, +//! assuming the preconditions hold. +//! +//! Since the induction revolves around the recursive call we can simply set it +//! up upon entry into the body of the function under verification. We use a +//! global variable that tracks whether we are re-entering the function +//! recursively and starts off as `false`. On entry to the function we flip the +//! variable to `true` and dispatch to the check (induction step). If the check +//! recursively calls our function our re-entry tracker now reads `true` and we +//! dispatch to the replacement (application of induction hypothesis). Because +//! the replacement function only checks the conditions and does not perform +//! other computation we will only ever go "one recursion level deep", making +//! inductive verification very efficient. Once the check function returns we +//! flip the tracker variable back to `false` in case the function is called +//! more than once in its harness. +//! +//! To facilitate all this we generate a `_recursion_wrapper_` +//! function with the following shape: +//! +//! ```ignored +//! fn recursion_wrapper_...(fn args ...) { +//! static mut REENTRY: bool = false; +//! +//! if unsafe { REENTRY } { +//! call_replace(fn args...) +//! } else { +//! unsafe { reentry = true }; +//! let result = call_check(fn args...); +//! unsafe { reentry = false }; +//! result +//! } +//! } +//! ``` +//! +//! We register this function as `#[kanitool::checked_with = +//! "recursion_wrapper_..."]` instead of the check function. +//! //! # Complete example //! //! ``` @@ -134,7 +182,7 @@ //! Turns into //! //! ``` -//! #[kanitool::checked_with = "div_check_965916"] +//! #[kanitool::checked_with = "div_recursion_wrapper_965916"] //! #[kanitool::replaced_with = "div_replace_965916"] //! fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } //! @@ -164,6 +212,22 @@ //! std::mem::forget(divisor_renamed); //! result //! } +//! +//! #[allow(dead_code)] +//! #[allow(unused_variables)] +//! #[kanitool::is_contract_generated(recursion_wrapper)] +//! fn div_recursion_wrapper_965916(dividend: u32, divisor: u32) -> u32 { +//! static mut REENTRY: bool = false; +//! +//! if unsafe { REENTRY } { +//! div_replace_965916(dividend, divisor) +//! } else { +//! unsafe { reentry = true }; +//! let result = div_check_965916(dividend, divisor); +//! unsafe { reentry = false }; +//! result +//! } +//! } //! ``` use proc_macro::{Diagnostic, TokenStream}; @@ -772,6 +836,8 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool 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 recursion_wrapper_name = + identifier_for_generated_function(&item_fn, "recursion_wrapper", item_hash); // Constructing string literals explicitly here, because `stringify!` // doesn't work. Let's say we have an identifier `check_fn` and we were @@ -781,7 +847,8 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool // 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()); + let recursion_wrapper_name_str = + syn::LitStr::new(&recursion_wrapper_name.to_string(), Span::call_site()); // The order of `attrs` and `kanitool::{checked_with, // is_contract_generated}` is important here, because macros are @@ -791,16 +858,45 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool // // The same care is taken when we emit check and replace functions. // emit the check function. + let is_impl_fn = is_probably_impl_fn(&item_fn); let ItemFn { attrs, vis, sig, block } = &item_fn; handler.output.extend(quote!( #(#attrs)* - #[kanitool::checked_with = #check_fn_name_str] + #[kanitool::checked_with = #recursion_wrapper_name_str] #[kanitool::replaced_with = #replace_fn_name_str] #vis #sig { #block } )); + let mut wrapper_sig = sig.clone(); + attach_require_kani_any(&mut wrapper_sig); + wrapper_sig.ident = recursion_wrapper_name; + + let args = pats_to_idents(&mut wrapper_sig.inputs).collect::>(); + let also_args = args.iter(); + let (call_check, call_replace) = if is_impl_fn { + (quote!(Self::#check_fn_name), quote!(Self::#replace_fn_name)) + } else { + (quote!(#check_fn_name), quote!(#replace_fn_name)) + }; + + handler.output.extend(quote!( + #[allow(dead_code, unused_variables)] + #[kanitool::is_contract_generated(recursion_wrapper)] + #wrapper_sig { + static mut REENTRY: bool = false; + if unsafe { REENTRY } { + #call_replace(#(#args),*) + } else { + unsafe { REENTRY = true }; + let result = #call_check(#(#also_args),*); + unsafe { REENTRY = false }; + result + } + } + )); + handler.emit_check_function(check_fn_name); handler.emit_replace_function(replace_fn_name, true); } @@ -809,6 +905,97 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool output.into() } +/// Convert every use of a pattern in this signature to a simple, fresh, binding-only +/// argument ([`syn::PatIdent`]) and return the [`Ident`] that was generated. +fn pats_to_idents

( + sig: &mut syn::punctuated::Punctuated, +) -> impl Iterator + '_ { + sig.iter_mut().enumerate().map(|(i, arg)| match arg { + syn::FnArg::Receiver(_) => Ident::from(syn::Token![self](Span::call_site())), + syn::FnArg::Typed(syn::PatType { pat, .. }) => { + let ident = Ident::new(&format!("arg{i}"), Span::mixed_site()); + *pat.as_mut() = syn::Pat::Ident(syn::PatIdent { + attrs: vec![], + by_ref: None, + mutability: None, + ident: ident.clone(), + subpat: None, + }); + ident + } + }) +} + +/// The visitor used by [`is_probably_impl_fn`]. See function documentation for +/// more information. +struct SelfDetector(bool); + +impl<'ast> Visit<'ast> for SelfDetector { + fn visit_ident(&mut self, i: &'ast syn::Ident) { + self.0 |= i == &Ident::from(syn::Token![Self](Span::mixed_site())) + } + + fn visit_receiver(&mut self, _node: &'ast syn::Receiver) { + self.0 = true; + } +} + +/// Try to determine if this function is part of an `impl`. +/// +/// Detects *methods* by the presence of a receiver argument. Heuristically +/// detects *associated functions* by the use of `Self` anywhere. +/// +/// Why do we need this? It's because if we want to call this `fn`, or any other +/// `fn` we generate into the same context we need to use `foo()` or +/// `Self::foo()` respectively depending on whether this is a plain or +/// associated function or Rust will complain. For the contract machinery we +/// need to generate and then call various functions we generate as well as the +/// original contracted function and so we need to determine how to call them +/// correctly. +/// +/// We can only solve this heuristically. The fundamental problem with Rust +/// macros is that they only see the syntax that's given to them and no other +/// context. It is however that context (of an `impl` block) that definitively +/// determines whether the `fn` is a plain function or an associated function. +/// +/// The heuristic itself is flawed, but it's the best we can do. For instance +/// this is perfectly legal +/// +/// ``` +/// struct S; +/// impl S { +/// #[i_want_to_call_you] +/// fn helper(u: usize) -> bool { +/// u < 8 +/// } +/// } +/// ``` +/// +/// This function would have to be called `S::helper()` but to the +/// `#[i_want_to_call_you]` attribute this function looks just like a bare +/// function because it never mentions `self` or `Self`. While this is a rare +/// case, the following is much more likely and suffers from the same problem, +/// because we can't know that `Vec == Self`. +/// +/// ``` +/// impl Vec { +/// fn new() -> Vec { +/// Vec { cap: 0, buf: NonNull::dangling() } +/// } +/// } +/// ``` +/// +/// **Side note:** You may be tempted to suggest that we could try and parse +/// `syn::ImplItemFn` and distinguish that from `syn::ItemFn` to distinguish +/// associated function from plain functions. However parsing in an attribute +/// placed on *any* `fn` will always succeed for *both* `syn::ImplItemFn` and +/// `syn::ItemFn`, thus not letting us distinguish between the two. +fn is_probably_impl_fn(fun: &ItemFn) -> bool { + let mut self_detector = SelfDetector(false); + self_detector.visit_item_fn(fun); + self_detector.0 +} + /// This is very similar to the kani_attribute macro, but it instead creates /// key-value style attributes which I find a little easier to parse. macro_rules! passthrough { @@ -834,3 +1021,58 @@ macro_rules! passthrough { passthrough!(stub_verified, false); passthrough!(proof_for_contract, true); + +#[cfg(test)] +mod test { + macro_rules! detect_impl_fn { + ($expect_pass:expr, $($tt:tt)*) => {{ + let syntax = stringify!($($tt)*); + let ast = syn::parse_str(syntax).unwrap(); + assert!($expect_pass == super::is_probably_impl_fn(&ast), + "Incorrect detection.\nExpected is_impl_fun: {}\nInput Expr; {}\nParsed: {:?}", + $expect_pass, + syntax, + ast + ); + }} + } + + #[test] + fn detect_impl_fn_by_receiver() { + detect_impl_fn!(true, fn self_by_ref(&self, u: usize) -> bool {}); + + detect_impl_fn!(true, fn self_by_self(self, u: usize) -> bool {}); + } + + #[test] + fn detect_impl_fn_by_self_ty() { + detect_impl_fn!(true, fn self_by_construct(u: usize) -> Self {}); + detect_impl_fn!(true, fn self_by_wrapped_construct(u: usize) -> Arc {}); + + detect_impl_fn!(true, fn self_by_other_arg(u: usize, slf: Self) {}); + + detect_impl_fn!(true, fn self_by_other_wrapped_arg(u: usize, slf: Vec) {}) + } + + #[test] + fn detect_impl_fn_by_qself() { + detect_impl_fn!( + true, + fn self_by_mention(u: usize) { + Self::other(u) + } + ); + } + + #[test] + fn detect_no_impl_fn() { + detect_impl_fn!( + false, + fn self_by_mention(u: usize) { + let self_name = 18; + let self_lit = "self"; + let self_lit = "Self"; + } + ); + } +} diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 1ec94af1192b..74210a8e4731 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -42,6 +42,9 @@ cargo test -p kani-compiler cargo test -p kani-driver cargo test -p kani_metadata cargo test -p kani --lib # skip doc tests. +# Test the actual macros, skipping doc tests and enabling extra traits for "syn" +# so we can debug print AST +RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-traits --lib # Declare testing suite information (suite and mode) TESTS=( diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected index 587dc3f46975..0a59d2cea5eb 100644 --- a/tests/expected/function-contract/arbitrary_ensures_fail.expected +++ b/tests/expected/function-contract/arbitrary_ensures_fail.expected @@ -1,4 +1,4 @@ -max.assertion\ +assertion\ - Status: FAILURE\ - Description: "result == x"\ in function max diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.expected b/tests/expected/function-contract/arbitrary_ensures_pass.expected index af1e09d1fe62..85619fa84c22 100644 --- a/tests/expected/function-contract/arbitrary_ensures_pass.expected +++ b/tests/expected/function-contract/arbitrary_ensures_pass.expected @@ -1,4 +1,4 @@ -max.assertion\ +assertion\ - Status: SUCCESS\ - Description: "result == x || result == y"\ in function max diff --git a/tests/expected/function-contract/arbitrary_requires_pass.expected b/tests/expected/function-contract/arbitrary_requires_pass.expected index 814fe6757ca3..d7560355afe3 100644 --- a/tests/expected/function-contract/arbitrary_requires_pass.expected +++ b/tests/expected/function-contract/arbitrary_requires_pass.expected @@ -1,4 +1,4 @@ -div.arithmetic_overflow\ +arithmetic_overflow\ - Status: SUCCESS\ - Description: "attempt to divide by zero"\ in function div diff --git a/tests/expected/function-contract/fail_on_two.expected b/tests/expected/function-contract/fail_on_two.expected new file mode 100644 index 000000000000..32fc28012d3a --- /dev/null +++ b/tests/expected/function-contract/fail_on_two.expected @@ -0,0 +1,12 @@ +assertion\ +- Status: FAILURE\ +- Description: "internal error: entered unreachable code: fail on two" + +Failed Checks: internal error: entered unreachable code: fail on two + + +assertion\ +- Status: FAILURE\ +- Description: "result < 3" + +Failed Checks: result < 3 diff --git a/tests/expected/function-contract/fail_on_two.rs b/tests/expected/function-contract/fail_on_two.rs new file mode 100644 index 000000000000..4302cdc7da33 --- /dev/null +++ b/tests/expected/function-contract/fail_on_two.rs @@ -0,0 +1,44 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +//! The test cases try to ensure applying the hypothesis is only done in +//! inductive verification of a function call. E.g. on every second encounter of +//! the called function in its own call stack rather than globally in the +//! program. +//! +//! In each case we have a recursive function that is called and we expect that +//! the recursive call within the first call has the hypothesis applied. (That's +//! not actually tested here but separately.) +//! +//! Then we call the function again and we've set up the cases such that *if* +//! the actual body is used then that call with fail (once because of panic, +//! once because the postcondition is violated). If instead the hypothesis (e.g. +//! contract replacement) is used we'd expect the verification to succeed. + +#[kani::ensures(result < 3)] +fn fail_on_two(i: i32) -> i32 { + match i { + 0 => fail_on_two(i + 1), + 1 => 2, + _ => unreachable!("fail on two"), + } +} + +#[kani::proof_for_contract(fail_on_two)] +fn harness() { + let first = fail_on_two(0); + let _ = fail_on_two(first); +} + +#[kani::ensures(result < 3)] +fn fail_on_two_in_postcondition(i: i32) -> i32 { + let j = i + 1; + if i < 2 { fail_on_two_in_postcondition(j) } else { j } +} + +#[kani::proof_for_contract(fail_on_two_in_postcondition)] +fn harness2() { + let first = fail_on_two_in_postcondition(1); + let _ = fail_on_two_in_postcondition(first); +} diff --git a/tests/expected/function-contract/gcd_failure_code.expected b/tests/expected/function-contract/gcd_failure_code.expected index 9488e9dcac9a..c7fe5a721abb 100644 --- a/tests/expected/function-contract/gcd_failure_code.expected +++ b/tests/expected/function-contract/gcd_failure_code.expected @@ -1,4 +1,4 @@ -gcd.assertion\ +assertion\ - Status: FAILURE\ - Description: "result != 0 && x % result == 0 && y % result == 0"\ in function gcd diff --git a/tests/expected/function-contract/gcd_failure_contract.expected b/tests/expected/function-contract/gcd_failure_contract.expected index 3ae94b199d6e..aeadfb563ab9 100644 --- a/tests/expected/function-contract/gcd_failure_contract.expected +++ b/tests/expected/function-contract/gcd_failure_contract.expected @@ -1,4 +1,4 @@ -gcd.assertion\ +assertion\ - Status: FAILURE\ - Description: "result != 0 && x % result == 1 && y % result == 0"\ in function gcd\ diff --git a/tests/expected/function-contract/gcd_rec_code_fail.expected b/tests/expected/function-contract/gcd_rec_code_fail.expected new file mode 100644 index 000000000000..80dbaadbf4c7 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_code_fail.expected @@ -0,0 +1,3 @@ +Failed Checks: result != 0 && x % result == 0 && y % result == 0 + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_rec_code_fail.rs b/tests/expected/function-contract/gcd_rec_code_fail.rs new file mode 100644 index 000000000000..5f63cb247ebf --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_code_fail.rs @@ -0,0 +1,24 @@ +// 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; + } + let res = max % min; + if res == 0 { min } else { gcd(min, res + 1) } +} + +#[kani::proof_for_contract(gcd)] +fn simple_harness() { + let _ = gcd(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.expected b/tests/expected/function-contract/gcd_rec_comparison_pass.expected new file mode 100644 index 000000000000..da647dfd40aa --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_comparison_pass.expected @@ -0,0 +1,9 @@ +assertion\ +- Status: SUCCESS\ +- Description: "x != 0 && y != 0" + +assertion\ +- Status: SUCCESS\ +- Description: "result != 0 && x % result == 0 && y % result == 0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_rec_comparison_pass.rs b/tests/expected/function-contract/gcd_rec_comparison_pass.rs new file mode 100644 index 000000000000..b08d94504bf7 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_comparison_pass.rs @@ -0,0 +1,68 @@ +// 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; + } + + let res = max % min; + if res == 0 { min } else { gcd(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_for_contract(gcd)] +#[kani::unwind(12)] +fn harness_as_check() { + gcd_harness() +} + +fn gcd_harness() { + // 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_rec_contract_fail.expected b/tests/expected/function-contract/gcd_rec_contract_fail.expected new file mode 100644 index 000000000000..bfb470192a39 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_contract_fail.expected @@ -0,0 +1,3 @@ +Failed Checks: result != 0 && x % result == 1 && y % result == 0 + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_rec_contract_fail.rs b/tests/expected/function-contract/gcd_rec_contract_fail.rs new file mode 100644 index 000000000000..3fe34cb2effc --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_contract_fail.rs @@ -0,0 +1,25 @@ +// 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)] +// Changed `0` to `1` in `x % result == 0` to mess with this contract +#[kani::ensures(result != 0 && x % result == 1 && 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; + } + + let res = max % min; + if res == 0 { min } else { gcd(min, res) } +} +#[kani::proof_for_contract(gcd)] +fn simple_harness() { + let _ = gcd(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.expected b/tests/expected/function-contract/gcd_rec_replacement_pass.expected new file mode 100644 index 000000000000..29c61cf9437c --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_replacement_pass.expected @@ -0,0 +1,17 @@ +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" + +gcd.assertion\ +- Status: SUCCESS\ +- Description: "x != 0 && y != 0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.rs b/tests/expected/function-contract/gcd_rec_replacement_pass.rs new file mode 100644 index 000000000000..d8a5bbd234ed --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_replacement_pass.rs @@ -0,0 +1,68 @@ +// 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; + } + + let res = max % min; + if res == 0 { min } else { gcd(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 gcd_as_replace() { + gcd_harness() +} + +fn gcd_harness() { + // 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_rec_simple_pass.expected b/tests/expected/function-contract/gcd_rec_simple_pass.expected new file mode 100644 index 000000000000..da647dfd40aa --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_simple_pass.expected @@ -0,0 +1,9 @@ +assertion\ +- Status: SUCCESS\ +- Description: "x != 0 && y != 0" + +assertion\ +- Status: SUCCESS\ +- Description: "result != 0 && x % result == 0 && y % result == 0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_rec_simple_pass.rs b/tests/expected/function-contract/gcd_rec_simple_pass.rs new file mode 100644 index 000000000000..ae55efa62b45 --- /dev/null +++ b/tests/expected/function-contract/gcd_rec_simple_pass.rs @@ -0,0 +1,25 @@ +// 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; + } + + let res = max % min; + if res == 0 { min } else { gcd(min, res) } +} + +#[kani::proof_for_contract(gcd)] +fn simple_harness() { + let _ = gcd(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/gcd_success.expected b/tests/expected/function-contract/gcd_success.expected index d75b31b151df..73b531d424b9 100644 --- a/tests/expected/function-contract/gcd_success.expected +++ b/tests/expected/function-contract/gcd_success.expected @@ -1,4 +1,4 @@ -gcd.assertion\ +assertion\ - Status: SUCCESS\ - Description: "result != 0 && x % result == 0 && y % result == 0"\ in function gcd diff --git a/tests/expected/function-contract/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected index a65fff824ea6..8e9b42d42640 100644 --- a/tests/expected/function-contract/simple_ensures_fail.expected +++ b/tests/expected/function-contract/simple_ensures_fail.expected @@ -1,4 +1,4 @@ -max.assertion\ +assertion\ - Status: FAILURE\ - Description: "result == x"\ in function max diff --git a/tests/expected/function-contract/simple_ensures_pass.expected b/tests/expected/function-contract/simple_ensures_pass.expected index b3e15aefcb9d..5a7874964413 100644 --- a/tests/expected/function-contract/simple_ensures_pass.expected +++ b/tests/expected/function-contract/simple_ensures_pass.expected @@ -1,4 +1,4 @@ -max.assertion\ +assertion\ - Status: SUCCESS\ - Description: "(result == x) | (result == y)"\ in function max