Autoharness: instantiate Fn-bounded type parameters with nondet closures

docs/src/reference/experimental/autoharness.md

@@ -115,7 +115,15 @@ Kani will detect if a struct or enum could implement `Arbitrary` and derive it a
 Note that this automatic derivation feature is only available for autoharness.
 
 ### Generic Functions
-The current implementation does not generate harnesses for generic functions.
+For a generic function, Kani generates a harness for a single monomorphic instantiation of the function:
+it substitutes the function's type parameters with concrete types such that all of the function's
+trait bounds are satisfied, and erases lifetime parameters. Kani first tries a fixed list of
+primitive types (starting with `i32`, and including the wider integer and float types) uniformly
+for all parameters; if that fails, it searches per-parameter combinations, drawing additional
+candidate types from the concrete implementations of the traits each parameter is bound by
+(so, e.g., a parameter bound by a crate-local trait can be instantiated with a crate-local struct
+implementing it). The search is capped, so functions with many type parameters or very complex
+bounds may still be skipped.
 For example, given:
 ```rust
 fn foo<T: Eq>(x: T, y: T) {
@@ -124,23 +132,21 @@ fn foo<T: Eq>(x: T, y: T) {
     }
 }
 ```
-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);
-}
+Kani generates and runs a harness that verifies `foo::<i32>`, and the summary table shows the
+instantiated name, e.g.:
 ```
-and run the autoharness subcommand, we get:
+| Crate    | Selected Function | Kind of Automatic Harness | Verification Result |
+| my_crate | foo::<i32>        | #[kani::proof]            | Failure             |
 ```
-Autoharness: Checking function main against all possible inputs...
+Note that verifying a single instantiation is an underapproximation of all of the function's possible behaviors:
+a successful result for `foo::<i32>` does not imply that other instantiations of `foo` are also safe.
+Kani makes this explicit by displaying the instantiated name of the verified function.
 
-Failed Checks: x and y are equal
- File: "src/lib.rs", line 3, in foo::<u8>
+`usize` const generic parameters (e.g. array lengths) are instantiated with the value 2.
 
-VERIFICATION:- FAILED
-```
+Kani skips a generic function (with skip reason "Generic Function") if:
+- no candidate type satisfies the function's trait bounds, or
+- the function has non-`usize` const generic parameters, which Kani does not instantiate yet.
+
+If some caller of a generic function is eligible for an automatic harness, then additional monomorphized
+versions of the generic function may still be reachable (and thus verified) through the caller's harness.

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -231,24 +231,28 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
                     // We could eventually expand this, but keep it simple for now. See:
                     // https://github.com/model-checking/kani/issues/2936
                     let overall_type = self.codegen_ty_stable(ty);
-                    let field_values: Vec<Expr> = field_types
-                        .iter()
-                        .map(|t| {
-                            if self.is_zst_stable(*t) {
-                                Some(Expr::init_unit(
-                                    self.codegen_ty_stable(*t),
-                                    &self.symbol_table,
-                                ))
-                            } else {
-                                self.try_codegen_constant(alloc, *t, loc)
-                            }
-                        })
-                        .collect::<Option<Vec<_>>>()?;
-                    Some(Expr::struct_expr_from_values(
-                        overall_type,
-                        field_values,
-                        &self.symbol_table,
-                    ))
+                    // Pair values with their field names (declaration indices): the goto
+                    // struct type is in LAYOUT order, which may differ from declaration
+                    // order (e.g. #[repr] optimizations reordering a (T, u16) pair), so a
+                    // positional struct_expr_from_values would mismatch.
+                    let field_values: std::collections::BTreeMap<cbmc::InternedString, Expr> =
+                        variant
+                            .fields()
+                            .iter()
+                            .zip(field_types.iter())
+                            .map(|(field, t)| {
+                                let value = if self.is_zst_stable(*t) {
+                                    Some(Expr::init_unit(
+                                        self.codegen_ty_stable(*t),
+                                        &self.symbol_table,
+                                    ))
+                                } else {
+                                    self.try_codegen_constant(alloc, *t, loc)
+                                };
+                                value.map(|v| (field.name.clone().into(), v))
+                            })
+                            .collect::<Option<_>>()?;
+                    Some(Expr::struct_expr(overall_type, field_values, &self.symbol_table))
                 } else {
                     // Structures with more than one non-ZST element are handled with an extra
                     // allocation.

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -955,7 +955,19 @@ impl GotocCtx<'_, '_> {
     pub fn codegen_get_discriminant(&mut self, e: Expr, ty: Ty, res_ty: Ty) -> Expr {
         let layout = self.layout_of_stable(ty);
         match &layout.variants {
-            Variants::Empty => unreachable!("Discriminant for uninhabited enum with no variants"),
+            Variants::Empty => {
+                // No value of an uninhabited enum can exist, so this read is dynamically
+                // dead code: emit an assert(false)-guarded nondet instead of ICEing (the
+                // MIR can still contain the read, e.g. matches on a Result<_, !>-like
+                // enum in dependencies).
+                let goto_res_ty = self.codegen_ty_stable(res_ty);
+                self.codegen_unimplemented_expr(
+                    "discriminant of uninhabited enum",
+                    goto_res_ty,
+                    Location::none(),
+                    "https://github.com/model-checking/kani/issues/3832",
+                )
+            }
             Variants::Single { index } => {
                 let discr_val = layout
                     .ty
@@ -1643,7 +1655,19 @@ impl GotocCtx<'_, '_> {
                         }
                         VtblEntry::MetadataSize => Some(vt_size.clone()),
                         VtblEntry::MetadataAlign => Some(vt_align.clone()),
-                        VtblEntry::Vacant => None,
+                        VtblEntry::Vacant => {
+                            // vtable_entries with the CONCRETE self type may mark a slot
+                            // vacant where the vtable struct type (built with dyn self in
+                            // trait_vtable_field_types) declares a method pointer: e.g. a
+                            // method with an HRTB predicate a fixed-region function item
+                            // does not satisfy. rustc pads such slots with null; mirror
+                            // that, typed as the declared field. If the type side skipped
+                            // the slot too, keep skipping it.
+                            let field_name = ctx.vtable_field_name(idx);
+                            Type::struct_tag(vtable_name)
+                                .lookup_field_type(field_name, &ctx.symbol_table)
+                                .map(|field_ty| Expr::pointer_constant(0, field_ty))
+                        }
                         VtblEntry::TraitVPtr(trait_ref) => {
                             let projections = match dst_mir_type.kind() {
                                 TyKind::RigidTy(RigidTy::Dynamic(predicates, ..)) => predicates