Tracking Issue: Make Harnesses Optional

[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

Open Questions

• UI: Support error messages where we say which function caused the problem, rather than which harness, with which inputs. Also, print which functions we couldn't automatically verify, and support a --function filter to only autoverify certain functions.

• How will this interplay with concrete playback?

• Performance: If we try to verify everything that we can verify, it may take quite a long time.

  • Should we try to be more discerning about what we verify, e.g., introducing some kind of ordering (e.g., look for unsafe functions first, then safe abstractions?)
  • Should this feature have an automatic harness timeout, or perhaps an attribute you can put on a function to opt out of automatic verification?
  • Can we detect if a harness we'd autogenerate would duplicate a manually written harness, and if so, skip generating it?

• Reasonable defaults: For types that do not trivially implement Arbitrary (e.g., pointers), we need to decide:

  • Do reasonable default values exist?
  • If so, what are they, and how do we communicate our default assumptions clearly so that users don't have a false sense of security if their code verifies?

  Similarly, for code with loops, we can statically detect the presence of the loop, but most of the time we won't be able to statically determine an unwinding bound. So we need to decide if it's worth it to pick an arbitrary number, or just leave loops out of this for now.