improve documentation for generics

Author: carolynzech

docs/src/reference/experimental/autoharness.md

@@ -10,7 +10,7 @@ Many proof harnesses follow this predictable format—to verify a function `foo`
 
 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:
@@ -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/kani_middle/codegen_units.rs

@@ -366,7 +366,9 @@ fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst:
         return false;
     }
 
-    // Each non-generic argument of `instance`` must implement Arbitrary.
+    // Each argument of `instance` must implement Arbitrary.
+    // Note that this function operates on StableMIR `Instance`s, which are eagerly monomorphized,
+    // so none of these arguments are generic.
     body.arg_locals().iter().all(|arg| {
         let kani_any_body =
             Instance::resolve(any_inst, &GenericArgs(vec![GenericArgKind::Type(arg.ty)]))