Autoharness: instantiate Fn-bounded type parameters with nondet closures

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

@@ -1652,7 +1652,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

kani-compiler/src/kani_middle/kani_functions.rs

@@ -63,6 +63,22 @@ pub enum KaniIntrinsic {
 pub enum KaniModel {
     #[strum(serialize = "AlignOfDynObjectModel")]
     AlignOfDynObject,
+    #[strum(serialize = "NondetFn0Model")]
+    NondetFn0,
+    #[strum(serialize = "NondetFn1Model")]
+    NondetFn1,
+    #[strum(serialize = "NondetFn1RefModel")]
+    NondetFn1Ref,
+    #[strum(serialize = "NondetFn2Model")]
+    NondetFn2,
+    #[strum(serialize = "NondetFn2RefRefModel")]
+    NondetFn2RefRef,
+    #[strum(serialize = "NondetFn2RefValModel")]
+    NondetFn2RefVal,
+    #[strum(serialize = "NondetFn2ValRefModel")]
+    NondetFn2ValRef,
+    #[strum(serialize = "NondetFn3Model")]
+    NondetFn3,
     #[strum(serialize = "AlignOfValRawModel")]
     AlignOfVal,
     #[strum(serialize = "AnySliceMutUnboundedModel")]
@@ -211,6 +227,14 @@ impl KaniModel {
                 | KaniModel::AnySliceMutUnbounded
                 | KaniModel::AnySliceRefUnbounded
                 | KaniModel::AnyVecUnbounded
+                | KaniModel::NondetFn0
+                | KaniModel::NondetFn1
+                | KaniModel::NondetFn1Ref
+                | KaniModel::NondetFn2
+                | KaniModel::NondetFn2RefRef
+                | KaniModel::NondetFn2RefVal
+                | KaniModel::NondetFn2ValRef
+                | KaniModel::NondetFn3
         )
     }
 }

kani-compiler/src/kani_middle/transform/automatic.rs

@@ -1154,6 +1154,27 @@ fn call_kani_any_for_ty(
     invariant_cache: &mut FxHashMap<Ty, bool>,
     mined_cache: &mut FxHashMap<Ty, Vec<MinedConjunct>>,
 ) -> Local {
+    // Function items (Fn-bound instantiations, c.f. fn_bound_candidates) are zero-sized:
+    // materialize the value as a zero-sized constant.
+    if matches!(ty.kind(), TyKind::RigidTy(RigidTy::FnDef(..))) {
+        let span = source.span(body.blocks());
+        let lcl = body.new_local(ty, span, mutability);
+        body.assign_to(
+            Place::from(lcl),
+            Rvalue::Use(
+                Operand::Constant(ConstOperand {
+                    span,
+                    user_ty: None,
+                    const_: MirConst::try_new_zero_sized(ty)
+                        .expect("function item types are zero-sized"),
+                }),
+                WithRetag::No,
+            ),
+            source,
+            InsertPosition::Before,
+        );
+        return lcl;
+    }
     // Unbounded generation for slices (&[T]/&mut [T]) and Vec<T> of primitive
     // integer/float elements: fresh allocations of nondeterministic size, so results hold
     // for all lengths (mirrors the eligibility decision in automatic_harness_partition).

library/kani/src/arbitrary.rs

@@ -172,3 +172,71 @@ pub fn slice_validity_assume<T>(_ptr: *const u8, _len: usize) {
     #[cfg(not(kani))]
     unreachable!("kani::slice_validity_assume is a verification-only hook");
 }
+
+/// Nondeterministic functions for instantiating `Fn`/`FnMut`/`FnOnce`-bounded type
+/// parameters of automatic harnesses: the parameter is instantiated with the *function
+/// item type* of the matching-arity model below (function items implement all three `Fn`
+/// traits and are zero-sized, so generating the value is trivial). Each call returns a
+/// fresh nondeterministic value, which over-approximates the behavior of every real
+/// closure with that signature (including stateful `FnMut` closures); verifying the
+/// harness against this instantiation therefore covers the function-under-test's own code
+/// for any closure behavior.
+///
+/// These models are *optional* (c.f. `KaniModel::is_optional`).
+#[kanitool::fn_marker = "NondetFn0Model"]
+#[inline(never)]
+#[doc(hidden)]
+pub fn nondet_fn0<R: Arbitrary>() -> R {
+    crate::any()
+}
+
+#[kanitool::fn_marker = "NondetFn1Model"]
+#[inline(never)]
+#[doc(hidden)]
+pub fn nondet_fn1<A, R: Arbitrary>(_a: A) -> R {
+    crate::any()
+}
+
+#[kanitool::fn_marker = "NondetFn1RefModel"]
+#[inline(never)]
+#[doc(hidden)]
+/// Region-polymorphic: the fn item's late-bound lifetime lets it satisfy HRTB bounds
+/// like `for<'a> Fn(&'a T) -> R` that the early-bound by-value models cannot.
+pub fn nondet_fn1_ref<T, R: Arbitrary>(_a: &T) -> R {
+    crate::any()
+}
+
+#[kanitool::fn_marker = "NondetFn2RefRefModel"]
+#[inline(never)]
+#[doc(hidden)]
+pub fn nondet_fn2_ref_ref<A, B, R: Arbitrary>(_a: &A, _b: &B) -> R {
+    crate::any()
+}
+
+#[kanitool::fn_marker = "NondetFn2RefValModel"]
+#[inline(never)]
+#[doc(hidden)]
+pub fn nondet_fn2_ref_val<A, B, R: Arbitrary>(_a: &A, _b: B) -> R {
+    crate::any()
+}
+
+#[kanitool::fn_marker = "NondetFn2ValRefModel"]
+#[inline(never)]
+#[doc(hidden)]
+pub fn nondet_fn2_val_ref<A, B, R: Arbitrary>(_a: A, _b: &B) -> R {
+    crate::any()
+}
+
+#[kanitool::fn_marker = "NondetFn2Model"]
+#[inline(never)]
+#[doc(hidden)]
+pub fn nondet_fn2<A, B, R: Arbitrary>(_a: A, _b: B) -> R {
+    crate::any()
+}
+
+#[kanitool::fn_marker = "NondetFn3Model"]
+#[inline(never)]
+#[doc(hidden)]
+pub fn nondet_fn3<A, B, C, R: Arbitrary>(_a: A, _b: B, _c: C) -> R {
+    crate::any()
+}

tests/script-based-pre/cargo_autoharness_fn_bounds/Cargo.toml

@@ -0,0 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "cargo_autoharness_fn_bounds"
+version = "0.1.0"
+edition = "2021"

tests/script-based-pre/cargo_autoharness_fn_bounds/config.yml

@@ -0,0 +1,5 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: fn_bounds.sh
+expected: fn_bounds.expected
+exit_code: 1

tests/script-based-pre/cargo_autoharness_fn_bounds/fn_bounds.expected

@@ -0,0 +1,11 @@
+	 - Status: SATISFIED
+| cargo_autoharness_fn_bounds | apply::<fn(u8) -> u8 {kani::arbitrary::nondet_fn1::<u8, u8>}>                      | #[kani::proof]            | Success             |
+| cargo_autoharness_fn_bounds | apply_generic::<i32, fn(i32) -> i32 {kani::arbitrary::nondet_fn1::<i32, i32>}>     | #[kani::proof]            | Success             |
+| cargo_autoharness_fn_bounds | branches::<fn(u8) -> bool {kani::arbitrary::nondet_fn1::<u8, bool>}>               | #[kani::proof]            | Success             |
+| cargo_autoharness_fn_bounds | inspect_with::<for<'a> fn(&'a u32) {kani::arbitrary::nondet_fn1_ref::<u32, ()>}>   | #[kani::proof]            | Success             |
+| cargo_autoharness_fn_bounds | packet_size                                                                        | #[kani::proof]            | Success             |
+| cargo_autoharness_fn_bounds | run_once::<fn() {kani::arbitrary::nondet_fn0::<()>}>                               | #[kani::proof]            | Success             |
+| cargo_autoharness_fn_bounds | scoped::<for<'a> fn(&'a u8) -> bool {kani::arbitrary::nondet_fn1_ref::<u8, bool>}> | #[kani::proof]            | Success             |
+| cargo_autoharness_fn_bounds | tuple_arg                                                                          | #[kani::proof]            | Success             |
+| cargo_autoharness_fn_bounds | apply_buggy::<fn(u8) -> u8 {kani::arbitrary::nondet_fn1::<u8, u8>}>                | #[kani::proof]            | Failure             |
+| cargo_autoharness_fn_bounds | fold2::<fn(u32, u32) -> u32 {kani::arbitrary::nondet_fn2::<u32, u32, u32>}>        | #[kani::proof]            | Failure             |

tests/script-based-pre/cargo_autoharness_fn_bounds/fn_bounds.sh

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Fn-bounded type parameters instantiate with nondeterministic function items
+# (fresh nondet result per call = over-approximation of every closure); Iterator-bounded
+# ones with std::vec::IntoIter over unbounded nondeterministic vectors.
+cargo kani autoharness -Z autoharness --output-format=regular

tests/script-based-pre/cargo_autoharness_fn_bounds/src/lib.rs

@@ -0,0 +1,83 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Fn-bounded generic functions: previously skipped ("no candidate type satisfies the
+// function's trait bounds"), now instantiated with nondeterministic function items.
+
+// TEST NOTE: harnessed as apply::<u8, nondet_fn1 item>; PASSES (wrapping arithmetic).
+pub fn apply<F: Fn(u8) -> u8>(f: F, x: u8) -> u8 {
+    f(x).wrapping_add(1)
+}
+
+// TEST NOTE: FAILS: the closure result is unconstrained, so the addition can overflow —
+// a real bug class in the generic function's own code, found for ANY closure behavior.
+pub fn apply_buggy<F: Fn(u8) -> u8>(f: F, x: u8) -> u8 {
+    f(x) + 1
+}
+
+// TEST NOTE: FnMut with two arguments; the fold-style accumulation overflows: FAILS.
+pub fn fold2<F: FnMut(u32, u32) -> u32>(mut f: F, a: u32, b: u32) -> u32 {
+    f(a, b) + f(b, a)
+}
+
+// TEST NOTE: FnOnce returning unit: PASSES (nothing to go wrong).
+pub fn run_once<F: FnOnce() -> ()>(f: F) {
+    f()
+}
+
+// TEST NOTE: cover check must be SATISFIED: the nondet closure's results genuinely cover
+// the range (both branches reachable).
+pub fn branches<F: Fn(u8) -> bool>(f: F, x: u8) {
+    if f(x) {
+        kani::cover!(true, "true branch reachable");
+    } else {
+        kani::cover!(true, "false branch reachable");
+    }
+}
+
+// TEST NOTE: harnessed as apply_generic::<i32, nondet_fn1<i32, i32>>: the closure
+// signature references another generic parameter, resolved per candidate choice.
+pub fn apply_generic<T, F: Fn(T) -> T>(f: F, x: T) -> T {
+    f(x)
+}
+
+// TEST NOTE (regression, tap ICE): HRTB closure bound (for<'a> via &Self sugar);
+// previously leaked escaping bound vars into the trait solver.
+pub fn inspect_with<F: FnOnce(&u32)>(f: F, v: u32) {
+    f(&v);
+}
+
+// TEST NOTE (regression, nom ICE): enum variant holding an anonymous tuple field;
+// previously the derive-style generator had no tuple vocabulary.
+pub enum Packet {
+    Pair((u8, u16)),
+    Empty,
+}
+pub fn packet_size(p: Packet) -> usize {
+    match p {
+        Packet::Pair((a, _)) => a as usize,
+        Packet::Empty => 0,
+    }
+}
+
+// TEST NOTE: top-level anonymous tuple argument, generated elementwise.
+pub fn tuple_arg(t: (u8, bool)) -> u8 {
+    if t.1 { t.0 } else { 0 }
+}
+
+// TEST NOTE (regression, reqwest ICE): HRTB closure param wrapped in a struct and
+// coerced to a trait object. Requires the region-polymorphic nondet_fn1_ref model
+// (an early-bound fn item leaves the method slot vacant in the concrete vtable).
+struct ScopeFn<F>(F);
+trait Scope {
+    fn run(&self) -> bool;
+}
+impl<F: Fn(&u8) -> bool> Scope for ScopeFn<F> {
+    fn run(&self) -> bool {
+        (self.0)(&7)
+    }
+}
+pub fn scoped<F: Fn(&u8) -> bool + 'static>(f: F) -> bool {
+    let s: Box<dyn Scope> = Box::new(ScopeFn(f));
+    s.run()
+}