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
  • Harnesses for closures
• 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.