Tracking Issue: Automatic Harnesses

[carolynzech]

Requested feature: Make proof harnesses optional, when possible
Use case: There are plenty of "boilerplate harnesses" that look something like this:

fn foo(x: u8, y: u8) { ... }

#[kani::proof]
fn foo_proof() {
  let x = kani::any();
  let y = kani::any();
  foo(x, y);
}

There's nothing surprising in this harness--the user just creates arbitrary variables for each argument of the function they're verifying, and then calls the function. Ideally, the user shouldn't have to write this harness at all; Kani should detect that each of the arguments implements Arbitrary, then attempt to verify it automatically.

Tasks

(We define "standard harness" as a #[kani::proof] harness and a "contract harness" as a #[kani::proof_for_contract] harness).
I'll break these tasks down into subtasks as I start working, but a road map for now:

• Autogenerate standard harnesses for types that already implement Arbitrary (either provided by Kani or implemented by the user)
• Detect which functions have contracts and autogenerate contract harnesses for them.
• Try to derive/implement Arbitrary for other types in the crate if doing so would allow us to verify more functions
• Extend the harness autogeneration to support more complex use cases:
  • Types with invariants that the harnesses need to respect
  • Pointers
  • Loops
  • Generics
• Default timeout & loop unwinding bounds
• Filters to include/exclude certain functions
• Logging about which functions were skipped

[carolynzech]

Note from #3874 -- Should log metadata about which functions were skipped, then print those functions in the driver, ideally with a note about why they were skipped.

[carolynzech]

For now, we don't support automatic harnesses for closures for two reasons:

1. We can't tell if a closure comes from Kani instrumentation (#[kanitool::is_contract_generated] attribute is not detected #3921).
2. Generating an Instance from a closure CrateItem isn't working, i.e., the Instance::try_from(fn_item) call in #[kanitool::is_contract_generated] attribute is not detected #3921 fails on a closure like:

const MY_CLOSURE: fn(u8) -> u8 = |x: u8| x + 1;

whereas

const MY_CLOSURE: fn(u8) -> u8 = |x: u8| x + 1;

#[kani::proof]
fn harness() {
  MY_CLOSURE(kani::any());
}

runs fine--Kani finds the Instance for the closure just fine during its reachability analysis. I don't think this is necessarily worthy of a separate issue yet because it may just be something simple that I'm doing wrong, and it's a moot point as long as #3921 is still open.

[carolynzech]

Apparently for tuple structs, Rust will insert a constructor function in MIR, e.g.

struct TupleStruct(u32);

generates:

fn TupleStruct(_1: u32) -> TupleStruct {
    let mut _0: TupleStruct;

    bb0: {
        _0 = TupleStruct(move _1);
        return;
    }
}

(see playground).

This means that in autoharness, we find and verify this function:

Autoharness Summary:
+-------------------+---------------------------+---------------------+
| Selected Function | Kind of Automatic Harness | Verification Result |
+=====================================================================+
| TupleStruct       | #[kani::proof]            | Success             |
+-------------------+---------------------------+---------------------+
Complete - 1 successfully verified functions, 0 failures, 1 total.

More confusingly, with #3942 merged, if we have:

struct TupleStruct(Vec<u32>);

we get:

+------------------+-----------------------------------------------------+
| Skipped Function | Reason for Skipping                                 |
+========================================================================+
| TupleStruct      | Missing Arbitrary implementation for argument(s): _ |
+------------------+-----------------------------------------------------+

The correct behavior would be to skip over these constructors entirely, since they are inserted by the Rust compiler. I don't see a great way of doing that. We could do something hacky like "if the name of the function is the same as a struct in the same namespace, skip it," but I worry about a bug in that logic causing legitimate functions to be ignored.

[carolynzech]

Consider adding a flag e.g. --write-to-file that writes Rust harnesses back to the file.