From 836682aed9a51bd6e13a95b556482c5ecbbd7860 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 31 Jul 2026 21:13:12 +0000 Subject: [PATCH] Autoharness: per-parameter and trait-impl-derived generic instantiation Extend the generic-instantiation search in three ways, found by evaluating autoharness on the top-100 crates.io crates, where ~8,700 functions were skipped because no candidate type satisfied their trait bounds: 1. Widen the primitive candidate list with u8, i64, u64, f64 and f32; float candidates alone unlock the numerous Float/FloatCore-bounded functions in num-traits and its dependents. 2. Search per-parameter candidate combinations (after the cheap uniform pass), so functions whose parameters need different types, e.g. fn cast, are instantiated. The search is capped at 256 trait-solver queries per function. 3. Derive additional per-parameter candidates from the concrete implementations of the traits each parameter is bound by (capped at 16 per parameter), so parameters bound by crate-local traits can be instantiated with the crate's own types implementing them. Co-authored-by: Kiro --- .../src/reference/experimental/autoharness.md | 10 +- .../src/kani_middle/codegen_units.rs | 157 ++++++++++++++++-- .../generics.expected | 31 ++-- .../cargo_autoharness_generics/src/lib.rs | 61 ++++++- 4 files changed, 234 insertions(+), 25 deletions(-) diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index 6a5750de9dbf..560638283ceb 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/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(x: T, y: T) { diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index c20e37b7705c..f1618be1446a 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/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::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> { + let mut candidates: FxHashMap> = 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 Holder { fn combine(..) }`) 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 = identity_args + .0 + .iter() + .enumerate() + .filter_map(|(idx, arg)| matches!(arg, GenericArgKind::Type(_)).then_some(idx)) + .collect(); + let slot_candidates: Vec> = 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 Option { + 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`) 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 = + 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::>() - .join(", ") + .join(", "), + if n_impl_derived > 0 { + format!(" and {n_impl_derived} types implementing the required traits") + } else { + String::new() + } )) } diff --git a/tests/script-based-pre/cargo_autoharness_generics/generics.expected b/tests/script-based-pre/cargo_autoharness_generics/generics.expected index 4aebef62731c..8b8a7420a798 100644 --- a/tests/script-based-pre/cargo_autoharness_generics/generics.expected +++ b/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::::get | #[kani::proof] | Success | -| cargo_autoharness_generics | contracted:: | #[kani::proof_for_contract] | Success | -| cargo_autoharness_generics | first:: | #[kani::proof] | Success | -| cargo_autoharness_generics | identity:: | #[kani::proof] | Success | -| cargo_autoharness_generics | max3:: | #[kani::proof] | Success | -| cargo_autoharness_generics | pair:: | #[kani::proof] | Success | -| cargo_autoharness_generics | takes_impl:: | #[kani::proof] | Success | -| cargo_autoharness_generics | with_const::<2> | #[kani::proof] | Success | -| cargo_autoharness_generics | buggy_add:: | #[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 | ::frob | #[kani::proof] | Success | +| cargo_autoharness_generics | ::half | #[kani::proof] | Success | +| cargo_autoharness_generics | ::half | #[kani::proof] | Success | +| cargo_autoharness_generics | Container::::mix:: | #[kani::proof] | Success | +| cargo_autoharness_generics | Wrapper::::get | #[kani::proof] | Success | +| cargo_autoharness_generics | contracted:: | #[kani::proof_for_contract] | Success | +| cargo_autoharness_generics | first:: | #[kani::proof] | Success | +| cargo_autoharness_generics | frob_it:: | #[kani::proof] | Success | +| cargo_autoharness_generics | halve:: | #[kani::proof] | Success | +| cargo_autoharness_generics | identity:: | #[kani::proof] | Success | +| cargo_autoharness_generics | max3:: | #[kani::proof] | Success | +| cargo_autoharness_generics | mixed:: | #[kani::proof] | Success | +| cargo_autoharness_generics | pair:: | #[kani::proof] | Success | +| cargo_autoharness_generics | takes_impl:: | #[kani::proof] | Success | +| cargo_autoharness_generics | with_const::<2> | #[kani::proof] | Success | +| cargo_autoharness_generics | buggy_add:: | #[kani::proof] | Failure | +Complete - 15 successfully verified functions, 1 failures, 16 total. diff --git a/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs index b690193d2da5..93a2cbe1863f 100644 --- a/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs @@ -46,7 +46,8 @@ pub fn takes_impl(x: impl Into + 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; } @@ -54,6 +55,64 @@ pub fn needs_exotic(x: T) -> u8 { x.exotic() } +// TEST NOTE: verified as `halve::`; 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(x: T) -> T { + x.half() +} + +// TEST NOTE: verified as `frob_it::`; 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: W) -> u32 { + w.frob() +} + +// TEST NOTE: verified as `mixed::`; the parameters require *different* +// candidate types, found by the per-parameter search. +pub fn mixed(x: T, w: U) -> u32 { + let _ = x.half(); + w.frob() +} + +// TEST NOTE: verified as `Container::::mix::`. 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 { + pub w: W, +} +impl Container { + pub fn mix(&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(x: [u8; N]) -> usize {