Autoharness: Derive `Arbitrary` for structs and enums
While generating automatic harnesses, derive Arbitrary implementations for structs and enums that don't have implementations.
Implementation Overview
- In
automatic_harness_partition, we mark a function as eligible for autoharness if its arguments either: a. implementArbitrary, or b. are structs/enums whose fields implementArbitrary. -
AutomaticHarnessPassruns as before, but now may generate harnesses that callkani::any()for structs/enums that do not actually implementArbitrary. See the definition ofkani::any(): https://github.com/model-checking/kani/blob/b64e59de669cd77b625cc8c0b9a94f29117a0ff7/library/kani_core/src/lib.rs#L274-L276 The initialkani::any()call resolves fine, but the compiler would ICE if it tried to resolveT::any(). - To avoid the ICE, we add a new
AutomaticArbitraryPassthat runs after theAutomaticHarnessPass. This pass detects the calls to nonexistentT::any()s and replaces them with inlinedT::any()implementations. These implementations are based on what Kani's derive macros for structs and enums produce.
Example
Given the automatic harness foo_harness produced by AutomaticHarnessPass:
struct Foo(u32)
fn function_with_foo(foo: Foo) { ... }
// pretend this is an autoharness, just written in source code for the example
#[kani::proof]
fn foo_harness() {
let foo = kani::any();
function_with_foo(foo);
}
AutomaticArbitraryPass will rewrite kani::any():
pub fn any() -> Foo {
Foo::any()
}
as:
pub fn any() -> Foo {
Self(kani::any())
}
i.e., replace the call to Foo::any() with what the derive macro would have produced for the body of Foo::any() (had the programmer used the derive macro instead).
Limitations
The fields need to have Arbitrary implementations; there is no support for recursive derivation. See the tests for examples; this should be resolvable through further engineering effort.
Towards https://github.com/model-checking/kani/issues/3832
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
I recommend reviewing commit-by-commit. In the first commit, review in execution order: i.e., first look at the changes in codegen_units.rs, then kani_middle::mod.rs, then automatic.rs.