Autoharness Misc. Improvements (#3922)

Follow up to #3874
implementing the features requested during review. Hopefully reviewing
commit-by-commit makes the size manageable (most of the changes come
from the additional metadata logging) but happy to split this into
multiple PRs if not.

The list below maps each commit to the review comment on
#3874 that inspired it.

- 8685925:
#3874 (comment)
- f060d66:
#3874 (comment)
- 7a7f654:
#3874 (comment)
- 4f3add8:
#3874 (comment)
- 212b0ff:
#3874 (comment)
- f105a9c:
#3874 (review)
and
- 6a8dc61:
#3874 (review)
- 6f946bb and
6997afb:
#3874 (comment)

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.

Author: Carolyn Zech

docs/src/reference/experimental/autoharness.md

@@ -8,18 +8,18 @@ Recall the harness for `estimate_size` that we wrote in [First Steps](../../tuto
 This harness first declares a local variable `x` using `kani::any()`, then calls `estimate_size` with argument `x`.
 Many proof harnesses follow this predictable format—to verify a function `foo`, we create arbitrary values for each of `foo`'s arguments, then call `foo` on those arguments.
 
-The `autoharness` subcommand leverages this observation to automatically generate and run harnesses.
+The `autoharness` subcommand leverages this observation to automatically generate harnesses and run Kani against them.
 Kani scans the crate for functions whose arguments all implement the `kani::Arbitrary` trait, generates harnesses for them, then runs them.
-These harnesses are internal to Kani--i.e., Kani does not make any changes to your source code.
+These harnesses are internal to Kani—i.e., Kani does not make any changes to your source code.
 
 ## Usage
 Run either:
 ```
-# cargo kani autoharness -Z unstable-options
+# cargo kani autoharness -Z autoharness
 ```
 or
 ```
-# kani autoharness -Z unstable-options <FILE>
+# kani autoharness -Z autoharness <FILE>
 ```
 
 If Kani detects that all of a function `foo`'s arguments implement `kani::Arbitrary`, it will generate and run a `#[kani::proof]` harness, which prints:
@@ -42,11 +42,11 @@ These flags look for partial matches against the fully qualified name of a funct
 
 For example, if a module `my_module` has many functions, but we are only interested in `my_module::foo` and `my_module::bar`, we can run:
 ```
-cargo run autoharness -Z unstable-options --include-function foo include-function bar
+cargo run autoharness -Z autoharness --include-function foo --include-function bar
 ```
 To exclude `my_module` entirely, run:
 ```
-cargo run autoharness -Z unstable-options --exclude-function my_module
+cargo run autoharness -Z autoharness --exclude-function my_module
 ```
 
 ## Example
@@ -58,7 +58,7 @@ Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.
 We get:
 
 ```
-# cargo kani autoharness -Z unstable-options
+# cargo kani autoharness -Z autoharness
 Autoharness: Checking function estimate_size against all possible inputs...
 RESULTS:
 Check 3: estimate_size.assertion.1
@@ -76,9 +76,44 @@ If you have ideas for improving the user experience of this feature,
 please add them to [this GitHub issue](https://github.com/model-checking/kani/issues/3832).
 
 ## Limitations
+### Arguments Implementing Arbitrary
 Kani will only generate an automatic harness for a function if it can determine that all of the function's arguments implement Arbitrary.
 It does not attempt to derive/implement Arbitrary for any types, even if those types could implement Arbitrary.
+For example, imagine a user defines `struct MyStruct { x: u8, y: u8}`, but does not derive or implement Arbitrary for `MyStruct`.
+Kani does not attempt to add such derivations itself, so it will not generate a harness for a function that takes `MyStruct` as input.
 
+### Generic Functions
+The current implementation does not generate harnesses for generic functions.
+For example, given:
+```rust
+fn foo<T: Eq>(x: T, y: T) {
+    if x == y {
+        panic!("x and y are equal");
+    }
+}
+```
+Kani would report that no functions were eligible for automatic harness generation.
+
+If, however, some caller of `foo` is eligible for an automatic harness, then a monomorphized version of `foo` may still be reachable during verification.
+For instance, if we add `main`:
+```rust
+fn main() {
+    let x: u8 = 2;
+    let y: u8 = 2;
+    foo(x, y);
+}
+```
+and run the autoharness subcommand, we get:
+```
+Autoharness: Checking function main against all possible inputs...
+
+Failed Checks: x and y are equal
+ File: "src/lib.rs", line 3, in foo::<u8>
+
+VERIFICATION:- FAILED
+```
+
+### Loop Contracts
 If a function contains a loop with a loop contract, Kani will detect the presence of a loop contract and verify that contract.
 If, however, the loop does not have a contract, then there is currently no way to specify an unwinding bound for the function, meaning that Kani may hang as it tries to unwind the loop.
 We recommend using the `--exclude-function` option to exclude any functions that have this issue (or `--harness-timeout` to bail after attempting verification for some amount of time).

kani-compiler/src/args.rs

@@ -91,10 +91,14 @@ pub struct Arguments {
     /// Print the final LLBC file to stdout.
     #[clap(long)]
     pub print_llbc: bool,
-    /// If we are running the autoharness subcommand, the functions to autoharness
-    #[arg(long = "autoharness-include-function", num_args(1))]
+    /// If we are running the autoharness subcommand, the functions to include
+    #[arg(
+        long = "autoharness-include-function",
+        num_args(1),
+        conflicts_with = "autoharness_excluded_functions"
+    )]
     pub autoharness_included_functions: Vec<String>,
-    /// If we are running the autoharness subcommand, the functions to exclude from autoverification
+    /// If we are running the autoharness subcommand, the functions to exclude
     #[arg(long = "autoharness-exclude-function", num_args(1))]
     pub autoharness_excluded_functions: Vec<String>,
 }

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -613,6 +613,7 @@ impl GotoCodegenResults {
             // removes any contracts logic for ReachabilityType::Test or ReachabilityType::PubFns,
             // which are the two ReachabilityTypes under which the compiler calls this function.
             contracted_functions: vec![],
+            autoharness_skipped_fns: None,
         }
     }
 

kani-compiler/src/kani_middle/attributes.rs

@@ -310,6 +310,17 @@ impl<'tcx> KaniAttributes<'tcx> {
         })
     }
 
+    // Is this a function inserted by Kani instrumentation?
+    pub fn is_kani_instrumentation(&self) -> bool {
+        self.fn_marker().is_some() || self.is_contract_generated()
+    }
+
+    // Is this a contract-generated function?
+    // Note that this function currently always returns false because of https://github.com/model-checking/kani/issues/3921
+    fn is_contract_generated(&self) -> bool {
+        self.map.contains_key(&KaniAttributeKind::IsContractGenerated)
+    }
+
     /// Return a function marker if any.
     pub fn fn_marker(&self) -> Option<Symbol> {
         self.attribute_value(KaniAttributeKind::FnMarker)