Support for inductively verifying contracts of recursive functions

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};

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=(

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/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

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

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

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

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

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

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

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

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

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

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