Autoharness: per-parameter and trait-impl-derived generic instantiation - #4706
Merged
feliperodri merged 1 commit intoAug 25, 2026
Merged
Conversation
github-actions
Bot
added
Z-EndToEndBenchCI
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>
feliperodri
force-pushed
the
autoharness-generics-c5
branch
from
August 25, 2026 02:40
7e81251 to
836682a
Compare
feliperodri
approved these changes
Aug 25, 2026
feliperodri
enabled auto-merge
August 25, 2026 02:56
feliperodri
pushed a commit
to tautschnig/kani
that referenced
this pull request
Aug 25, 2026
…hecking#4716) ### Description A layout niche (`rustc_layout_scalar_valid_range`, as used by std's `NonZero` and `core::time::Duration`'s `Nanoseconds` field) is a language-level validity invariant: a value outside the niche is as invalid as a `bool` holding 3, and rustc packs enum variants into the invalid bit patterns. Autoharness's compiler-derived generation for types without an `Arbitrary` implementation previously produced such values — unsound in the garbage-in sense, and a source of false alarms in every harness generating the type (found in the top-100/500 crates.io evaluations for model-checking#3832: e.g. `std::time::Duration` receivers via time's `InstantExt::signed_duration_since`). After each generated value of a scalar-ABI type with a restricted valid range, emit `kani::assume(<raw bits> in valid_range)` (transmute to the width-matched uint; wrapping ranges like `NonZero`'s `1..=0` handled). The assumption is sound by construction — assuming a *necessary* condition of language-level validity keeps every valid value in the explored set — so no flag or report marker is needed. Scope: both autoharness passes are gated on `ReachabilityType::AllFns`, so plain `kani`/`cargo kani` verification is unaffected. `scalar_niche` bails out if the layout size does not match the scalar width, rather than emitting an ill-sized `Transmute`. rustc is not known to report a `Scalar` ABI with padding (verified: a `#[repr(align(4))]` wrapper around a ranged newtype gets `BackendRepr::Memory`, and its inner field is constrained anyway), but the asymmetry matters: losing a constraint can only cause a *visible* false alarm, whereas comparing the wrong bits could assume `false` and silently make the harness vacuous. The `Assume` hook now lives in the shared `AnyModels` struct alongside the other model `FnDef`s, so both passes pick it up without separate fields. ### Testing New `autoharness_niche` test covering: - a `rustc_layout_scalar_valid_range` ranged newtype reached through a struct field — the function asserting the range now verifies (previously a false alarm); - cover checks pinning that both range extremes remain reachable (no over-constraining); - `std::time::Duration`, the motivating real-world case from the evaluation; - `NonZeroU8`, exercising the *wrapping* range where the check must be a disjunction; - a niche on a *signed* scalar, exercising that the comparison is on raw bit patterns (unsigned); - a niche reached through *generic instantiation* (`check_monthly::<Month>`), where the candidate type is derived from the trait's only implementor by model-checking#4706's instantiation search rather than named in the signature — the two features compose, and this pins that. Counterfactual verified: the test fails against a build without the compiler change, and passes with it. Also verified by hand, beyond the checked-in test: a niche type behind `#[repr(align(4))]`, a niche nested in an enum variant, and a niche type with a `Drop` impl (the assume reads the value with `Operand::Copy`, which must not introduce a double drop). Measured the cost of the redundant assume on primitives that carry niches but whose `Arbitrary` impls already respect them (`bool`, `char`): +3% program-expression steps with identical VCC counts, all simplified away — not worth gating the assume on ADTs. Rebased onto main after model-checking#4706 landed and re-ran the autoharness suite on the combined tree. Full `script-based-pre` suite (67 tests, including all 22 autoharness tests), `cargo test -p kani-compiler`, `clippy --all-targets`, and `kani-fmt --check` pass. Towards model-checking#3832. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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.
Description
The top-100 crates.io evaluation (#3832) showed ~8,700 functions skipped as "Generic Function: no candidate type satisfies the function's trait bounds". This PR extends the instantiation search in three ways:
u8,i64,u64,f64,f32. The float candidates alone unlock the numerousFloat/FloatCore-bounded functions in num-traits and its dependents. The existing candidates keep their positions (i32first), so instantiations that already worked are unchanged.fn cast<T: Float, U: PrimInt>) are instantiated. Capped at 256 trait-solver queries per function.Candidate collection walks the parent chain of the predicate list, so bounds on an impl's type parameters count too: for
impl<W: Frobnicate> Container<W> { fn mix<T: FloatLike>(..) },W: Frobnicateis a predicate of the parent rather than ofmix, and without walking the chainWwould be left with primitive candidates only and the method skipped. (args_satisfy_predicatesalready sees parent predicates, viaGenericPredicates::instantiate, so this was a missed opportunity rather than a source of bogus instantiations.)Measured impact (with
--bounded-arguments,-j 16): num-traits 75 generic skips → 0 (2,107 → 2,154 harnesses; every public function now harnessed); serde_json 594 → 276; syn 167 → 41.Note that this only widens the search; each candidate is still accepted only if the trait solver confirms it satisfies every predicate, and verifying one monomorphic instantiation remains an underapproximation, as documented.
Testing
cargo_autoharness_genericsgains a case for each capability:halve::<f64>),frob_it::<Widget>),mixed::<f64, Widget>),Container::<Widget>::mix::<f64>).needs_exotic(a trait with no implementations at all) remains skipped, with the candidate list in the message updated.All 21 script-based autoharness tests pass, as do
cargo test -p kani-compiler/-p kani-driver,clippy --all-targetsandkani-fmt --check.Rebased onto main now that #4679 has landed, so this is a single commit.
Towards #3832.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.