Support for inductively verifying contracts of recursive functions

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_<fn_name>_<fn_hash>` function that assumes preconditions
+//! Generates a `<fn_name>_check_<fn_hash>` 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_<fn_name>_<fn_hash>"]`.
+//! "<fn_name>_check_<fn_hash>"]`.
 //!
 //! 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_<fn_name>_<fn_hash>`
+//! As the mirror to that also generates a `<fn_name>_replace_<fn_hash>`
 //! 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_<fn_name>_<fn_hash>"]`.
+//! "<fn_name>_replace_<fn_hash>"]`.
 //!
 //! 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 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 one in it's harness.
+//!
+//! To facilitate all this we generate a `<fn_name>_recursion_wrapper_<fn_hash>`
+//! function with the following shape:
+//!
+//! ```ignored
+//! fn recursion_wrapper_...(fn args ...) {
+//! static 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 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
@@ -794,13 +861,41 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool
  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::<Vec<_>>();
+ let also_args = args.iter();
+ let (call_check, call_replace) = if is_probably_impl_fn(sig) {
+ (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 +904,40 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool
  output.into()
 }
 
+fn pats_to_idents<P>(
+ sig: &mut syn::punctuated::Punctuated<syn::FnArg, P>,
+) -> impl Iterator<Item = Ident> + '_ {
+ sig.iter_mut().enumerate().map(|(i, arg)| match arg {
+ syn::FnArg::Receiver(_) => Ident::new("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
+ }
+ })
+}
+
+struct SelfDetector(bool);
+
+impl<'ast> Visit<'ast> for SelfDetector {
+ fn visit_path(&mut self, i: &'ast syn::Path) {
+ self.0 |= i.get_ident().map_or(false, |i| i == "self")
+ || i.get_ident().map_or(false, |i| i == "Self")
+ }
+}
+
+fn is_probably_impl_fn(sig: &Signature) -> bool {
+ let mut self_detector = SelfDetector(false);
+ self_detector.visit_signature(sig);
+ 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 {

tests/expected/function-contract/arbitrary_ensures_fail.expected

@@ -1,4 +1,4 @@
-max.assertion\
+assertion\
 - Status: FAILURE\
 - Description: "result == x"\
 in function max 

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

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

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

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\

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

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());
+}

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