Autoharness: per-parameter and trait-impl-derived generic instantiation

docs/src/reference/experimental/autoharness.md

@@ -247,8 +247,14 @@ Modeling caller-controlled aliasing between arguments is tracked in
 
 ### Generic Functions
 For a generic function, Kani generates a harness for a single monomorphic instantiation of the function:
-it substitutes every type parameter with the first candidate from a fixed list of primitive types
-(starting with `i32`) such that all of the function's trait bounds are satisfied, and erases lifetime parameters.
+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) {

kani-compiler/src/kani_middle/codegen_units.rs

@@ -32,8 +32,8 @@ use rustc_middle::ty::{self, TyCtxt, TypingMode};
 use rustc_public::mir::mono::Instance;
 use rustc_public::rustc_internal;
 use rustc_public::ty::{
-    FnDef, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyConst, TyKind,
-    UintTy,
+    FloatTy, FnDef, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyConst,
+    TyKind, UintTy,
 };
 use rustc_public::{CrateDef, CrateItem};
 use rustc_public_bridge::IndexedVal;
@@ -438,11 +438,69 @@ fn generic_instantiation_candidates() -> Vec<Ty> {
         Ty::from_rigid_kind(RigidTy::Int(IntTy::I32)),
         Ty::from_rigid_kind(RigidTy::Uint(UintTy::U32)),
         Ty::from_rigid_kind(RigidTy::Uint(UintTy::Usize)),
+        Ty::from_rigid_kind(RigidTy::Uint(UintTy::U8)),
+        Ty::from_rigid_kind(RigidTy::Int(IntTy::I64)),
+        Ty::from_rigid_kind(RigidTy::Uint(UintTy::U64)),
+        Ty::from_rigid_kind(RigidTy::Float(FloatTy::F64)),
+        Ty::from_rigid_kind(RigidTy::Float(FloatTy::F32)),
         Ty::from_rigid_kind(RigidTy::Bool),
         Ty::from_rigid_kind(RigidTy::Char),
     ]
 }
 
+/// Cap on trait-solver queries per function when searching for a satisfying instantiation,
+/// so that functions with many type parameters do not blow up partitioning time.
+const GENERIC_INSTANTIATION_ATTEMPT_LIMIT: usize = 256;
+
+/// Cap on the number of trait-impl-derived candidate types collected per type parameter.
+const IMPL_DERIVED_CANDIDATE_LIMIT: usize = 16;
+
+/// For each type parameter of `def` (keyed by its index in the generic parameter list),
+/// collect concrete types that implement the parameter's trait bounds, by enumerating the
+/// non-blanket implementations of each trait the parameter is bound by. This finds candidates
+/// for parameters bound by crate-local or third-party traits (e.g. num-traits' `Float`),
+/// which no primitive candidate may satisfy.
+/// Candidates are deduplicated, restricted to fully concrete types, and sorted for
+/// determinism; each parameter's list is capped at [IMPL_DERIVED_CANDIDATE_LIMIT].
+fn impl_derived_candidates(tcx: TyCtxt, def: FnDef) -> FxHashMap<usize, Vec<Ty>> {
+    let mut candidates: FxHashMap<usize, Vec<Ty>> = FxHashMap::default();
+    // Walk the parent chain: `GenericPredicates::predicates` holds only the item's *own*
+    // predicates, so for an associated function the bounds on the impl's type parameters (e.g.
+    // `T` in `impl<T: Frob> Holder<T> { fn combine<U: Nizzle>(..) }`) live on the parent. They
+    // constrain the same argument list, and `args_satisfy_predicates` checks them (via
+    // `GenericPredicates::instantiate`, which does recurse into the parent), so missing them
+    // here would leave such a parameter with primitive candidates only.
+    let mut next = Some(rustc_internal::internal(tcx, def.def_id()));
+    while let Some(def_id) = next {
+        let generic_predicates = tcx.predicates_of(def_id);
+        next = generic_predicates.parent;
+        for (predicate, _span) in generic_predicates.predicates {
+            let Some(trait_pred) = predicate.as_trait_clause() else { continue };
+            let trait_pred = trait_pred.skip_binder();
+            let ty::Param(param_ty) = trait_pred.self_ty().kind() else { continue };
+            let slot = candidates.entry(param_ty.index as usize).or_default();
+            for impls in tcx.trait_impls_of(trait_pred.def_id()).non_blanket_impls().values() {
+                for &impl_def_id in impls {
+                    let self_ty = tcx.type_of(impl_def_id).instantiate_identity();
+                    // Only fully concrete self types can be substituted directly.
+                    if rustc_middle::ty::TypeVisitableExt::has_param(&self_ty) {
+                        continue;
+                    }
+                    let stable_ty = rustc_internal::stable(self_ty);
+                    if !slot.contains(&stable_ty) {
+                        slot.push(stable_ty);
+                    }
+                }
+            }
+        }
+    }
+    for slot in candidates.values_mut() {
+        slot.sort_by_key(|ty| ty.to_string());
+        slot.truncate(IMPL_DERIVED_CANDIDATE_LIMIT);
+    }
+    candidates
+}
+
 /// Check whether instantiating the generic parameters of `def` with `args` satisfies all of
 /// `def`'s predicates (trait bounds and where clauses).
 /// `args` must be fully monomorphic.
@@ -485,13 +543,43 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result<Insta
         return Err("non-usize const generic parameters are not supported yet".to_string());
     }
 
-    for candidate in generic_instantiation_candidates() {
-        let args = GenericArgs(
+    // Positions of the type parameters among the identity arguments, and the candidate list
+    // for each: the shared primitive candidates, plus types derived from the parameter's own
+    // trait bounds (concrete implementors of the traits it must satisfy).
+    let impl_derived = impl_derived_candidates(tcx, def);
+    let type_slots: Vec<usize> = identity_args
+        .0
+        .iter()
+        .enumerate()
+        .filter_map(|(idx, arg)| matches!(arg, GenericArgKind::Type(_)).then_some(idx))
+        .collect();
+    let slot_candidates: Vec<Vec<Ty>> = type_slots
+        .iter()
+        .map(|&idx| {
+            let mut cands = generic_instantiation_candidates();
+            for ty in impl_derived.get(&idx).into_iter().flatten() {
+                if !cands.contains(ty) {
+                    cands.push(*ty);
+                }
+            }
+            cands
+        })
+        .collect();
+    let n_impl_derived: usize = impl_derived.values().map(|v| v.len()).sum();
+
+    // Build the argument list substituting `choice[i]` for the i-th type parameter.
+    let build_args = |choice: &[Ty]| {
+        let mut next_type = 0;
+        GenericArgs(
             identity_args
                 .0
                 .iter()
                 .map(|arg| match arg {
-                    GenericArgKind::Type(_) => GenericArgKind::Type(candidate),
+                    GenericArgKind::Type(_) => {
+                        let ty = choice[next_type];
+                        next_type += 1;
+                        GenericArgKind::Type(ty)
+                    }
                     GenericArgKind::Lifetime(_) => {
                         GenericArgKind::Lifetime(Region { kind: RegionKind::ReErased })
                     }
@@ -500,25 +588,74 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result<Insta
                     ),
                 })
                 .collect(),
-        );
+        )
+    };
+
+    let attempts = std::cell::Cell::new(0usize);
+    let try_choice = |choice: &[Ty]| -> Option<Instance> {
+        attempts.set(attempts.get() + 1);
+        let args = build_args(choice);
         if !args_satisfy_predicates(tcx, def, &args) {
-            continue;
+            return None;
         }
         // Return the resolved instance regardless of whether it has a body: a body-less
         // instance (e.g. a generic trait method without a default) is then reported accurately
         // as `NoBody` by `skip_reason`, rather than falling through to a generic-function skip
         // reason here.
-        if let Ok(instance) = Instance::resolve(def, &args) {
+        Instance::resolve(def, &args).ok()
+    };
+
+    // First pass: the same primitive candidate for every type parameter (the common case,
+    // and cheap). Second pass: the cartesian product of the per-parameter candidate lists,
+    // capped at GENERIC_INSTANTIATION_ATTEMPT_LIMIT trait-solver queries, which finds
+    // instantiations for functions whose parameters need *different* types (e.g.
+    // `fn cast<T: Float, U: PrimInt>`) or types implementing non-primitive-friendly bounds.
+    for candidate in generic_instantiation_candidates() {
+        if let Some(instance) = try_choice(&vec![candidate; type_slots.len()]) {
             return Ok(instance);
         }
     }
+    if !type_slots.is_empty() {
+        let mut odometer = vec![0usize; type_slots.len()];
+        'product: loop {
+            let choice: Vec<Ty> =
+                odometer.iter().enumerate().map(|(i, &c)| slot_candidates[i][c]).collect();
+            // Skip choices already tried in the uniform pass.
+            let uniform = choice.iter().all(|ty| *ty == choice[0])
+                && generic_instantiation_candidates().contains(&choice[0]);
+            if !uniform {
+                if let Some(instance) = try_choice(&choice) {
+                    return Ok(instance);
+                }
+                if attempts.get() >= GENERIC_INSTANTIATION_ATTEMPT_LIMIT {
+                    break;
+                }
+            }
+            // Advance the odometer.
+            for i in (0..odometer.len()).rev() {
+                odometer[i] += 1;
+                if odometer[i] < slot_candidates[i].len() {
+                    continue 'product;
+                }
+                odometer[i] = 0;
+                if i == 0 {
+                    break 'product;
+                }
+            }
+        }
+    }
     Err(format!(
-        "no candidate type ({}) satisfies the function's trait bounds",
+        "no candidate type ({}{}) satisfies the function's trait bounds",
         generic_instantiation_candidates()
             .iter()
             .map(|ty| ty.to_string())
             .collect::<Vec<_>>()
-            .join(", ")
+            .join(", "),
+        if n_impl_derived > 0 {
+            format!(" and {n_impl_derived} types implementing the required traits")
+        } else {
+            String::new()
+        }
     ))
 }
 

tests/script-based-pre/cargo_autoharness_generics/generics.expected

@@ -1,12 +1,19 @@
-| cargo_autoharness_generics | needs_exotic     | Generic Function: no candidate type (i32, u32, usize, bool, char) satisfies the function's trait bounds |
-| cargo_autoharness_generics | with_bool_const  | Generic Function: non-usize const generic parameters are not supported yet                              |
-| cargo_autoharness_generics | Wrapper::<i32>::get | #[kani::proof]              | Success             |
-| cargo_autoharness_generics | contracted::<u32>   | #[kani::proof_for_contract] | Success             |
-| cargo_autoharness_generics | first::<i32>        | #[kani::proof]              | Success             |
-| cargo_autoharness_generics | identity::<i32>     | #[kani::proof]              | Success             |
-| cargo_autoharness_generics | max3::<i32>         | #[kani::proof]              | Success             |
-| cargo_autoharness_generics | pair::<i32, i32>    | #[kani::proof]              | Success             |
-| cargo_autoharness_generics | takes_impl::<u32>   | #[kani::proof]              | Success             |
-| cargo_autoharness_generics | with_const::<2>     | #[kani::proof]              | Success             |
-| cargo_autoharness_generics | buggy_add::<i32>    | #[kani::proof]              | Failure             |
-Complete - 8 successfully verified functions, 1 failures, 9 total.
+| cargo_autoharness_generics | needs_exotic     | Generic Function: no candidate type (i32, u32, usize, u8, i64, u64, f64, f32, bool, char) satisfies the function's trait bounds |
+| cargo_autoharness_generics | with_bool_const  | Generic Function: non-usize const generic parameters are not supported yet                                                      |
+| cargo_autoharness_generics | <Widget as Frobnicate>::frob    | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | <f32 as FloatLike>::half        | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | <f64 as FloatLike>::half        | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | Container::<Widget>::mix::<f64> | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | Wrapper::<i32>::get             | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | contracted::<u32>               | #[kani::proof_for_contract] | Success             |
+| cargo_autoharness_generics | first::<i32>                    | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | frob_it::<Widget>               | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | halve::<f64>                    | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | identity::<i32>                 | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | max3::<i32>                     | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | mixed::<f64, Widget>            | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | pair::<i32, i32>                | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | takes_impl::<u32>               | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | with_const::<2>                 | #[kani::proof]              | Success             |
+| cargo_autoharness_generics | buggy_add::<i32>                | #[kani::proof]              | Failure             |
+Complete - 15 successfully verified functions, 1 failures, 16 total.

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

@@ -46,14 +46,73 @@ pub fn takes_impl(x: impl Into<u64> + Copy) -> u64 {
     x.into()
 }
 
-// TEST NOTE: skipped (Generic Function), since no candidate type implements `Exotic`.
+// TEST NOTE: skipped (Generic Function), since no candidate type implements `Exotic`
+// (the trait has no implementations at all).
 pub trait Exotic {
     fn exotic(&self) -> u8;
 }
 pub fn needs_exotic<T: Exotic>(x: T) -> u8 {
     x.exotic()
 }
 
+// TEST NOTE: verified as `halve::<f64>`; no integral candidate satisfies the bound, but the
+// float candidates do (mimics num-traits' `Float`).
+pub trait FloatLike {
+    fn half(self) -> Self;
+}
+impl FloatLike for f64 {
+    fn half(self) -> Self {
+        self / 2.0
+    }
+}
+impl FloatLike for f32 {
+    fn half(self) -> Self {
+        self / 2.0
+    }
+}
+pub fn halve<T: FloatLike>(x: T) -> T {
+    x.half()
+}
+
+// TEST NOTE: verified as `frob_it::<Widget>`; no primitive implements `Frobnicate`, so the
+// candidate is derived from the trait's implementations.
+pub trait Frobnicate {
+    fn frob(&self) -> u32;
+}
+#[derive(kani::Arbitrary)]
+pub struct Widget {
+    pub id: u32,
+}
+impl Frobnicate for Widget {
+    fn frob(&self) -> u32 {
+        self.id.wrapping_add(1)
+    }
+}
+pub fn frob_it<W: Frobnicate>(w: W) -> u32 {
+    w.frob()
+}
+
+// TEST NOTE: verified as `mixed::<f64, Widget>`; the parameters require *different*
+// candidate types, found by the per-parameter search.
+pub fn mixed<T: FloatLike, U: Frobnicate>(x: T, w: U) -> u32 {
+    let _ = x.half();
+    w.frob()
+}
+
+// TEST NOTE: verified as `Container::<Widget>::mix::<f64>`. The bound that needs an
+// impl-derived candidate (`W: Frobnicate`) is on the *impl*, not on `mix` itself, so it is a
+// predicate of the parent rather than of the method; deriving candidates has to walk the
+// parent chain to see it.
+pub struct Container<W> {
+    pub w: W,
+}
+impl<W: Frobnicate> Container<W> {
+    pub fn mix<T: FloatLike>(&self, x: T) -> u32 {
+        let _ = x.half();
+        self.w.frob()
+    }
+}
+
 // TEST NOTE: verified as `with_const::<2>`; usize const generic parameters are instantiated
 // with the value 2.
 pub fn with_const<const N: usize>(x: [u8; N]) -> usize {