Automatic Harness Generation

Recall the harness for estimate_size that we wrote in First Steps:

#[cfg(kani)]
#[kani::proof]
fn check_estimate_size() {
    let x: u32 = kani::any();
    estimate_size(x);
}

This harness first declares a local variable x using kani::any(), then calls estimate_size with argument x. Many proof harnesses follow this predictable format—to verify a function foo, we create arbitrary values for each of foo's arguments, then call foo on those arguments.

The autoharness subcommand leverages this observation to automatically generate harnesses and run Kani against them. Kani scans the crate for functions whose arguments all implement the kani::Arbitrary trait, generates harnesses for them, then runs them. These harnesses are internal to Kani—i.e., Kani does not make any changes to your source code.

Usage

Run either:

# cargo kani autoharness -Z autoharness

# kani autoharness -Z autoharness <FILE>

If Kani detects that all of a function foo's arguments implement kani::Arbitrary, it will generate and run a #[kani::proof] harness, which prints:

Autoharness: Checking function foo against all possible inputs...
<VERIFICATION RESULTS>

However, if Kani detects that foo has a function contract, it will instead generate a #[kani::proof_for_contract] harness and verify the contract:

Autoharness: Checking function foo's contract against all possible inputs...
<VERIFICATION RESULTS>

Similarly, Kani will detect the presence of loop contracts and verify them.

Thus, -Z autoharness implies -Z function-contracts and -Z loop-contracts, i.e., opting into the experimental autoharness feature means that you are also opting into the function contracts and loop contracts features.

Kani generates and runs these harnesses internally—the user only sees the verification results.

Options

The autoharness subcommand has options --include-pattern and --exclude-pattern to include and exclude particular functions. These flags look for partial matches against the fully qualified name of a function.

For example, if a module my_module has many functions, but we are only interested in my_module::foo and my_module::bar, we can run:

cargo run autoharness -Z autoharness --include-pattern my_module::foo --include-pattern my_module::bar

To exclude my_module entirely, run:

cargo run autoharness -Z autoharness --exclude-pattern my_module

The selection algorithm is as follows:

If only --include-patterns are provided, include a function if it matches any of the provided patterns.
If only --exclude-patterns are provided, include a function if it does not match any of the provided patterns.
If both are provided, include a function if it matches an include pattern and does not match any of the exclude patterns. Note that this implies that the exclude pattern takes precedence, i.e., if a function matches both an include pattern and an exclude pattern, it will be excluded.

Here are some more examples:

# Include functions whose paths contain the substring foo or baz, but not foo::bar
kani autoharness -Z autoharness --include-pattern foo --include-pattern baz --exclude-pattern foo::bar

# Include functions whose paths contain the substring foo, but not bar.
kani autoharness -Z autoharness --include-pattern foo --exclude-pattern bar

# Include functions whose paths contain the substring foo::bar, but not bar.
# This ends up including nothing, since all foo::bar matches will also contain bar.
# Kani will emit a warning that these flags conflict.
kani autoharness -Z autoharness --include-pattern foo::bar --exclude-pattern bar

# Include functions whose paths contain the substring foo, but not foo.
# This ends up including nothing, and Kani will emit a warning that these flags conflict.
kani autoharness -Z autoharness --include-pattern foo --exclude--pattern foo

Currently, the only supported "patterns" are substrings of the fully qualified path of the function. However, if more sophisticated patterns (e.g., regular expressions) would be useful for you, please let us know in a comment on this GitHub issue.

Example

Using the estimate_size example from First Steps again:

fn estimate_size(x: u32) -> u32 {
    if x < 256 {
        if x < 128 {
            return 1;
        } else {
            return 3;
        }
    } else if x < 1024 {
        if x > 1022 {
            panic!("Oh no, a failing corner case!");
        } else {
            return 5;
        }
    } else {
        if x < 2048 {
            return 7;
        } else {
            return 9;
        }
    }
}

We get:

# cargo kani autoharness -Z autoharness
Autoharness: Checking function estimate_size against all possible inputs...
RESULTS:
Check 3: estimate_size.assertion.1
         - Status: FAILURE
         - Description: "Oh no, a failing corner case!"
[...]

Verification failed for - estimate_size
Complete - 0 successfully verified functions, 1 failures, 1 total.

Request for comments

This feature is experimental and is therefore subject to change. If you have ideas for improving the user experience of this feature, please add them to this GitHub issue.

Limitations

Arguments Implementing Arbitrary

Kani will only generate an automatic harness for a function if it can determine that all of the function's arguments implement Arbitrary. It does not attempt to derive/implement Arbitrary for any types, even if those types could implement Arbitrary. For example, imagine a user defines struct MyStruct { x: u8, y: u8}, but does not derive or implement Arbitrary for MyStruct. Kani does not attempt to add such derivations itself, so it will not generate a harness for a function that takes MyStruct as input.

Generic Functions

The current implementation does not generate harnesses for generic functions. For example, given:

fn foo<T: Eq>(x: T, y: T) {
    if x == y {
        panic!("x and y are equal");
    }
}

Kani would report that no functions were eligible for automatic harness generation.

If, however, some caller of foo is eligible for an automatic harness, then a monomorphized version of foo may still be reachable during verification. For instance, if we add main:

fn main() {
    let x: u8 = 2;
    let y: u8 = 2;
    foo(x, y);
}

and run the autoharness subcommand, we get:

Autoharness: Checking function main against all possible inputs...

Failed Checks: x and y are equal
 File: "src/lib.rs", line 3, in foo::<u8>

VERIFICATION:- FAILED

The Kani Rust Verifier