Autoharness: per-parameter and trait-impl-derived generic instantiation by tautschnig · Pull Request #4706 · model-checking/kani

tautschnig · 2026-07-31T21:49:10Z

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:

Wider primitive candidates: add u8, i64, u64, f64, f32. The float candidates alone unlock the numerous Float/FloatCore-bounded functions in num-traits and its dependents. The existing candidates keep their positions (i32 first), so instantiations that already worked are unchanged.
Per-parameter search: after the cheap uniform pass (same candidate for every parameter), search per-parameter combinations, so functions whose parameters need different types (e.g. fn cast<T: Float, U: PrimInt>) are instantiated. Capped at 256 trait-solver queries per function.
Trait-impl-derived candidates: for each type parameter, derive additional candidates from the concrete implementations of the traits it is bound by (capped at 16 per parameter). A parameter bound by a crate-local trait can thus be instantiated with a crate-local type implementing it.

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: Frobnicate is a predicate of the parent rather than of mix, and without walking the chain W would be left with primitive candidates only and the method skipped. (args_satisfy_predicates already sees parent predicates, via GenericPredicates::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_generics gains a case for each capability:

a float-only trait bound (halve::<f64>),
a crate-local trait satisfied only by a struct (frob_it::<Widget>),
parameters needing different types (mixed::<f64, Widget>),
an impl method whose impl-level parameter needs an impl-derived candidate, i.e. the parent-predicate case (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-targets and kani-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.

Copilot

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

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>

…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>

…res (model-checking#4726) Stacked on model-checking#4706 (per-parameter generic instantiation); only the last commit is new. Marked draft until model-checking#4706 merges. Part of model-checking#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 `Fn` bound — these functions were all skipped. ### Approach `Fn`/`FnMut`/`FnOnce`-bounded type parameters are instantiated with the **function item type** of a matching `nondet_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 stateful `FnMut` ones. 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) - **Shape-based model selection**: by-value models bind input regions early and cannot satisfy HRTB bounds like `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. - **Binder handling**: candidate derivation erases late-bound regions instead of skipping binders (escaping bound vars panic the trait solver — tap). - **Param-referencing signatures** (`fn apply<T, F: Fn(T) -> T>`): deferred specs substituted per candidate choice, normalized (tap), and admission-checked against the model's own `R: Arbitrary` bound (syn). - **Vacant vtable slots**: concrete instantiations may leave an HRTB method slot vacant where the vtable struct type declares a pointer; pad with typed null, mirroring rustc's layout (reqwest). - **Arity ceiling 3, by data**: 98.5% of corpus Fn-bound signatures. Iterator/IntoIterator-bounded parameters are a follow-up PR (the iterator model rides on the unbounded-Vec generation of model-checking#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. --------- Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>

### Description Bumps `rust-toolchain.toml` from `nightly-2026-07-01` to `nightly-2026-08-01`, the first 1.99 nightly. 91 compile errors came with it. #### 1. `Statement`/`Terminator` carry a `SourceInfo`, not a bare `Span` (78 of the 91 errors) ```rust // nightly-2026-07-01 pub struct Statement<'tcx> { pub source_info: SourceInfo, .. } // Terminator: span only // nightly-2026-08-01 -- both carry SourceInfo (span + source scope) ``` A new helper in `transform/body.rs` keeps the choice of scope in one documented place rather than spreading a bare `scope: 0` across ~78 sites: ```rust /// The `SourceInfo` for a statement or terminator that Kani synthesizes at `span`. /// /// As of nightly-2026-08-01 `Statement` and `Terminator` carry a `SourceInfo` (span plus source /// scope) instead of a bare `Span`. Kani-synthesized MIR does not belong to any inlined scope, so /// it uses the outermost one -- scope 0, which `Body::new` always allocates. pub fn synthetic_source_info(span: Span) -> SourceInfo { SourceInfo { span, scope: 0 } } ``` Reads become `.source_info.span`. #### 2. `predicates_of` became `clauses_of` Returns `GenericClauses` (`parent` + `clauses`) instead of `GenericPredicates` (`parent` + `predicates`). Same shape and same `instantiate`, so this is a rename at four call sites — three in `codegen_units.rs` from model-checking#4706/model-checking#4718, one in the LLBC backend. #### 3. `ty::FnDef`'s generic args are bound Three `Instance::{try,expect}_resolve` call sites need `.skip_binder()`. #### 4. `ValueAbi::ScalarPair` became a struct variant With a new `b_offset` field. #### 5. Two new enum variants - `AssertMessage::NullReferenceConstructed` — handled like `NullPointerDereference`: same property class, description taken from `rustc_public` rather than hardcoded. - `InstanceKind::LlvmIntrinsic` — codegens like any other item, and has no Rust body for reachability to collect. Plus `LocalModDefId` renamed to `LocalModId`, and `Region::new_early_param` moving to the `RegionExt` extension trait. ### Test changes (5 files) **`std::intrinsics::{size_of,align_of}` are now comptime fns** and cannot be called at runtime, which affected four tests: - `tests/kani/DynTrait/{nested_boxes,vtable_size_align_drop}.rs` used `size_of` incidentally, to compare a vtable field against a type's size — switched to `std::mem::size_of`. - `tests/kani/Intrinsics/ConstEval/{size_of,align_of}.rs` exist to check the intrinsics themselves, so each call is bound to a `const` — which is what that directory is about, and the only way now legal. **`expected/issue-3571` — a genuine behaviour change worth flagging.** Constructing a null reference (`&*(0 as *const u32)`) used to report `null pointer dereference occurred`; rustc now distinguishes constructing a null reference from dereferencing a null pointer and reports `null reference produced`. rustc also emits a new `misaligned pointer to reference cast` check at the same site. The UB is still caught and the harness still fails — only the wording is more precise — so the expectation follows rustc's message rather than pinning the old one. No other test needed adjusting, and no verification behaviour changed. ### Testing Local, macOS aarch64, CBMC 6.10.0 (`cbmc-6.9.0-214-g45436eea34`), on the stack rebased onto current `main` (which now includes model-checking#4760): | Suite | Result | |---|---| | `kani` | **607 passed, 0 failed** | | `cargo-kani` | **71 passed, 0 failed** | | `cargo-ui` | **30 passed, 0 failed** | | `expected` | 471 passed, 2 failed — see below | | `ui` | 151 passed, 2 failed — environmental, see below | Also clean: both the CPROVER and LLBC builds, `cargo clippy --workspace --tests -- -D warnings`, `RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings`, and `./scripts/kani-fmt.sh --check`. The two `expected` failures were run before the fix above and are accounted for: - `expected/issue-3571` — the null-reference wording change; **fixed in this PR**, verified passing. - `expected/shadow/slices/slice_split` — I interrupted this one to let the suite finish. It is **not** an 08-01 regression: I timed it on the 07-01 branch as a control and it is equally slow there (>20 min in CBMC's SAT solver on both), so it is a slow test on this machine rather than anything this upgrade introduced. CI covers it. The two `ui` failures are `solver-attribute/cadical` and `solver-option/cadical`, both expecting `Solving with CaDiCaL`. My local CBMC build reports `The specified solver, 'cadical', is not available. The default solver will be used instead.` — a missing solver in my environment, independent of the Rust toolchain. - Was this change tested? **Yes** - Is this a breaking change? **No** By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

tautschnig requested a review from a team as a code owner July 31, 2026 21:49

Copilot AI review requested due to automatic review settings July 31, 2026 21:49

Copilot AI reviewed Jul 31, 2026

github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Jul 31, 2026

feliperodri added the Z-Autoharness Issue related to autoharness subcommand label Aug 1, 2026

tautschnig mentioned this pull request Aug 7, 2026

Autoharness: instantiate Fn-bounded type parameters with nondet closures #4726

Merged

feliperodri added this to the Autoharness milestone Aug 18, 2026

feliperodri force-pushed the autoharness-generics-c5 branch from 7e81251 to 836682a Compare August 25, 2026 02:40

feliperodri requested a review from a team as a code owner August 25, 2026 02:40

feliperodri approved these changes Aug 25, 2026

View reviewed changes

feliperodri enabled auto-merge August 25, 2026 02:56

feliperodri added this pull request to the merge queue Aug 25, 2026

Merged via the queue into model-checking:main with commit 2457093 Aug 25, 2026
34 checks passed

feliperodri mentioned this pull request Aug 25, 2026

Autoharness: assume layout niches of generated scalar values #4716

Merged

feliperodri mentioned this pull request Aug 27, 2026

Upgrade Rust toolchain to nightly-2026-08-01 #4767

Merged

This was referenced Sep 26, 2026

Autoharness: umbrella issue classifying open issues by skip reason #4879

Open

Autoharness umbrella: generic function with no candidate type (GenericFn) #4888

Open

Navigation Menu

Repository navigation

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

Autoharness: per-parameter and trait-impl-derived generic instantiation#4706
feliperodri merged 1 commit into
model-checking:mainfrom
tautschnig:autoharness-generics-c5

tautschnig commented Jul 31, 2026 •

edited by feliperodri

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

tautschnig commented Jul 31, 2026 • edited by feliperodri Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Testing

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

tautschnig commented Jul 31, 2026 •

edited by feliperodri

Loading