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 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 `<fn_name>_recursion_wrapper_<fn_hash>`
+//! 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
@@ -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