Autoharness: instantiate Fn-bounded type parameters with nondet closures - #4726
Merged
Merged
Conversation
github-actions
Bot
added
Z-EndToEndBenchCI
feliperodri
marked this pull request as ready for review
August 25, 2026 21:07
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>
feliperodri
force-pushed
the
c5p2-closures-pr
branch
from
August 26, 2026 14:25
4f66b60 to
f4f4c55
Compare
feliperodri
approved these changes
Aug 26, 2026
feliperodri
enabled auto-merge
August 26, 2026 14:30
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
Aug 26, 2026
feliperodri
enabled auto-merge
August 26, 2026 15:31
feliperodri
disabled auto-merge
August 26, 2026 21:29
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
Aug 26, 2026
feliperodri
enabled auto-merge
August 26, 2026 23:57
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
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.