kani icon indicating copy to clipboard operation
kani copied to clipboard

Autoharness: Derive `Arbitrary` for structs and enums

Open carolynzech opened this issue 7 months ago • 1 comments

While generating automatic harnesses, derive Arbitrary implementations for structs and enums that don't have implementations.

Implementation Overview

  1. In automatic_harness_partition, we mark a function as eligible for autoharness if its arguments either: a. implement Arbitrary, or b. are structs/enums whose fields implement Arbitrary.
  2. AutomaticHarnessPass runs as before, but now may generate harnesses that call kani::any() for structs/enums that do not actually implement Arbitrary. See the definition of kani::any(): https://github.com/model-checking/kani/blob/b64e59de669cd77b625cc8c0b9a94f29117a0ff7/library/kani_core/src/lib.rs#L274-L276 The initial kani::any() call resolves fine, but the compiler would ICE if it tried to resolve T::any().
  3. To avoid the ICE, we add a new AutomaticArbitraryPass that runs after the AutomaticHarnessPass. This pass detects the calls to nonexistent T::any()s and replaces them with inlined T::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.

carolynzech avatar Jun 19 '25 20:06 carolynzech

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.

carolynzech avatar Jun 20 '25 01:06 carolynzech