Autoharness: Derive Arbitrary for structs and enums

[carolynzech]

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():
   

   kani/library/kani_core/src/lib.rs

   Lines 274 to 276 in b64e59d

   	pubfn any<T:Arbitrary>() -> T{
   	T::any()
   	}

   
   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:

structFoo(u32)fnfunction_with_foo(foo:Foo){ ...}// pretend this is an autoharness, just written in source code for the example#[kani::proof]fnfoo_harness(){let foo = kani::any();function_with_foo(foo);}

AutomaticArbitraryPass will rewrite kani::any():

pubfnany() -> Foo{Foo::any()}

as:

pubfnany() -> 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 #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]

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.