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