Autoharness: instantiate Fn-bounded type parameters with nondet closures - #4726
Draft
tautschnig wants to merge 5 commits into
Draft
Autoharness: instantiate Fn-bounded type parameters with nondet closures#4726tautschnig wants to merge 5 commits into
tautschnig wants to merge 5 commits into
Conversation
Previously, autoharness skipped all generic functions. Now, it generates a harness for a single monomorphic instantiation: each type parameter is substituted with the first candidate from a fixed list of primitive types (i32, u32, usize, bool, char) such that all of the function's trait bounds are satisfied, checked with the trait solver (rustc_trait_selection::ObligationCtxt). Lifetime parameters are erased. Functions whose bounds no candidate satisfies, or with const generic parameters, are still skipped as 'Generic Function'. The generated harness's name reflects the chosen instantiation (e.g. foo::<i32>), making explicit that verification covers only that instantiation; the documentation spells out this underapproximation. Functions with any number of type, lifetime, and (unsupported) const parameters are handled, including methods of generic impl blocks, impl-Trait arguments, and functions with contracts. For contract harnesses, harness metadata now stores the definition-level name of the target function rather than the instantiated one, since gen_contracts_metadata matches it against definition-level ContractedFunction names. This addresses the 'Generics' item of the automatic harness generation tracking issue, the last unchecked entry together with the invariants and pointers work. Towards model-checking#3832 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Rather than the single 'Generic Function' skip reason, attach a detail explaining what prevented instantiation: const generic parameters, or that no candidate type satisfies the function's trait bounds. This makes the skipped-functions table actionable and allows corpus evaluations to classify the generic-function gap precisely. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Instantiate usize const generic parameters (by far the most common case, e.g. array lengths) with the value 2, alongside the existing type-parameter instantiation; the summary table shows the chosen value as part of the instantiated name (e.g. with_const::<2>). Non-usize const parameters are still skipped, now with a precise reason; the check consults the internal generics since the public identity arguments do not carry the parameter's type. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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<T: Float, U: PrimInt>, 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 <kiro-agent@users.noreply.github.com>
Corpus data (top-500 crates.io): Fn-bound generic functions outnumber Iterator-bound ones 4:1 (2,373 vs 612 signatures); no primitive candidate can ever satisfy an Fn bound, so these functions were all skipped. Fn/FnMut/FnOnce-bounded type parameters are instantiated with the function item type of a matching nondet model (kani::arbitrary:: nondet_fn*): function items implement all three Fn traits and are zero-sized (the harness materializes the value as a zero-sized constant), and each call returns a fresh nondeterministic value, over-approximating every real closure with that signature -- including stateful FnMut ones. Design points, each validated on the crate that motivated it: - Models are selected by input SHAPE, not just arity: by-value models bind their input regions early-bound and cannot satisfy HRTB bounds like for<'a> Fn(&'a T), so the four dominant by-ref shapes (96% of the 3,768 ref-involving Fn bounds in the corpus) get region-polymorphic models (nondet_fn1_ref etc.) whose fn items carry late-bound regions. - Candidate derivation reads the Fn trait predicates (tupled inputs) and the FnOnce::Output projection, erasing late-bound regions rather than skipping binders (escaping bound vars panic the trait solver; tap). - Signatures referencing other generic parameters (fn apply<T, F: Fn(T) -> T>) are collected as deferred specs: their slots carry a placeholder through the candidate search and are substituted per candidate choice (EarlyBinder::instantiate), normalized (unnormalizable projections such as <i32 as Tap>::Val abort the choice; tap), and admission-checked against the model's own R: Arbitrary bound (Instance::resolve does not check bounds; syn). - Vtables built for a concrete type may mark a method slot Vacant where the trait's vtable struct type declares a method pointer (an HRTB predicate the concrete fn item does not satisfy): pad the slot with a typed null, mirroring rustc's vtable layout (reqwest). Dispatchable methods use real slots via the region-polymorphic models. - Arity ceiling of 3 justified by data: 98.5% of corpus Fn-bound signatures have arity <= 3. The regression test pins bug-finding through nondet closures (overflow on unconstrained results at arities 1 and 2), cover-based reachability of closure-dependent branches, HRTB closures plain and dyn-coerced through a wrapper struct, param-referencing signatures, and tuple arguments. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
github-actions
Bot
added
Z-EndToEndBenchCI
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #4706 (per-parameter generic instantiation); only the last commit is new. Marked draft until #4706 merges. Part of #3832.
Fn-bound generic functions outnumber Iterator-bound ones 4:1 in the top-500 crates.io corpus (2,373 vs 612 signatures), and no primitive candidate can satisfy an
Fnbound — these functions were all skipped.Approach
Fn/FnMut/FnOnce-bounded type parameters are instantiated with the function item type of a matchingnondet_fn*model: fn items implement all three Fn traits and are zero-sized (materialized as a constant in the harness), and each call returns a fresh nondeterministic value — over-approximating every real closure with that signature, including statefulFnMutones. Harness names are self-documenting:apply::<fn(u8) -> u8 {kani::arbitrary::nondet_fn1::<u8, u8>}>.Design points (each validated on the crate that motivated it)
for<'a> Fn(&'a T); the four dominant by-ref shapes (96% of ref-involving corpus bounds) get region-polymorphic models with late-bound regions.fn apply<T, F: Fn(T) -> T>): deferred specs substituted per candidate choice, normalized (tap), and admission-checked against the model's ownR: Arbitrarybound (syn).Iterator/IntoIterator-bounded parameters are a follow-up PR (the iterator model rides on the unbounded-Vec generation of #4721).
In the crates.io sweep this converted 3,867 generic functions from skipped to attempted, with closure-instantiated harnesses in 76 crates.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.