Autoharness: assume layout niches of generated scalar values by tautschnig · Pull Request #4716 · model-checking/kani

tautschnig · 2026-08-05T15:04:51Z

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 #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 FnDefs, 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 Autoharness: per-parameter and trait-impl-derived generic instantiation #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 #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 #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

Pull request overview

This PR tightens autoharness value generation for scalar-ABI types that have compiler-defined validity ranges (“layout niches”, e.g., rustc_layout_scalar_valid_range_*), by constraining generated values to the type’s valid bit-pattern range via kani::assume. This addresses unsound “garbage-in” generation that can produce language-level invalid values and trigger false alarms (e.g., ranged newtypes similar to NonZero).

Changes:

Add scalar-niche detection (scalar_niche) based on rustc layout metadata, and use it to emit kani::assume range constraints during automatic generation.
Thread KaniHook::Assume through automatic harness / arbitrary generation so niche assumptions can be injected.
Add a new script-based regression test (autoharness_niche) validating both soundness (no out-of-range false alarm) and non-overconstraint (range extremes still reachable).

Reviewed changes

Copilot reviewed 7 out of 8 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
tests/script-based-pre/autoharness_niche/run.sh	Runs the new niche regression via `kani autoharness`.
tests/script-based-pre/autoharness_niche/niche_probe.rs	Defines a ranged scalar newtype and coverage/assertion checks for niche behavior.
tests/script-based-pre/autoharness_niche/expected	Expected successful verification output for the new test.
tests/script-based-pre/autoharness_niche/config.yml	Wires the script-based-pre test into the harness.
kani-compiler/src/kani_middle/transform/automatic.rs	Injects niche assumptions into automatic generation by calling `kani::assume` on computed range predicates.
kani-compiler/src/kani_middle/mod.rs	Introduces `ScalarNiche` + `scalar_niche()` helper using rustc layout to detect restricted valid ranges.
Cargo.lock	Updates the `charon` package version entry.

Suppressed comments (1)

kani-compiler/src/kani_middle/transform/automatic.rs:212

If place_local is moved to obtain raw bits (needed to support non-Copy niche types), place_local must be re-initialized so the caller can still use/move it later. You can restore it from the already-computed raw_lcl in the continuation block after the kani::assume call (which also ensures reconstruction only happens on assumed-valid paths).

    body.insert_call(
        &assume_inst,
        source,
        InsertPosition::Before,
        vec![Operand::Move(Place::from(cond_lcl))],

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

feliperodri · 2026-08-25T03:43:26Z

Rebased onto main and reviewed. Two things worth flagging:

Dropped an accidental submodule downgrade. The commit also moved charon from 607f5683a back to dee660306 (Cargo.lock: 0.1.88 → 0.1.73). That looked unintended, so I dropped both files and kept main's pointer (b250680ab, 0.1.91). The PR is now 6 files instead of 8.

Added a size guard to scalar_niche. It now returns None when layout.size does not match the scalar width, instead of emitting a Transmute of mismatched width. I could not get rustc to report a Scalar ABI with padding — a #[repr(align(4))] wrapper around a ranged newtype gets BackendRepr::Memory, and its inner field is constrained anyway — so this is defensive. It seemed worth it because the two failure directions are not symmetric: losing a constraint can only cause a false alarm, which is visible, whereas comparing the wrong bits could assume false and silently make the harness vacuous.

Also folded the Assume hook into the shared AnyModels struct rather than adding a field to each pass, since main now threads that struct through call_kani_any_for_ty.

Extended the test with the cases I used to check the approach: std::time::Duration (the motivating example from the description, which the test did not previously cover), NonZeroU8 for the wrapping range, and a signed-scalar niche for the raw-bits comparison. I verified the counterfactual myself — the test does fail without the compiler change.

Additional cases I checked by hand and did not check in: a niche behind #[repr(align(4))], a niche nested in an enum variant, and a niche type with a Drop impl (the assume reads via Operand::Copy, so I wanted to confirm no double drop). All verify. I also measured the redundant assume on bool/char, whose Arbitrary impls already respect their niches: +3% program-expression steps, identical VCC counts, all simplified away — so gating the assume on ADTs (as the Invariant assumption just below it does) is not worth it.

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 patterns. Nondeterministic-value generation for types without an Arbitrary implementation previously produced such values, which is unsound in the garbage-in sense and causes false alarms in every harness generating the type. After each generated value of a scalar-ABI type whose valid range is restricted, emit kani::assume(<raw bits> in valid_range), handling wrapping ranges (NonZero's 1..=0). Sound by construction: no flag or report marker needed. Verified on the time crate: fixes the InstantExt/SystemTimeExt signed_duration_since harnesses (std Duration receivers); the regression test's covers confirm no over-constraining. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Four upstream changes drive most of this. **Retag moved onto `Rvalue::Use`.** `StatementKind::Retag` and `RetagKind` are gone; `Rvalue::Use` now carries a `WithRetag` flag instead. Kani never modelled retags (they are Stacked-Borrows/Miri only), so the statement arms are dropped, the flag is ignored when reading a `Use`, and synthesized `Use`s pass `WithRetag::No`. `internal_mir`'s `RetagKind` conversion becomes a `WithRetag` one. **`Variants::Multiple` stores a `VariantLayout`, not a `LayoutData`.** The new type carries only per-field offsets -- no `FieldsShape` (so no field order) and no alignment. Variant layouts now come from `Layout::for_variant`, which is what `rustc_codegen_ssa` does and restores the field order; a new `variant_layout` helper is used by both the type side (`codegen_enum_cases`) and the value side (`codegen_aggregate`) so the goto struct's components and the operands initializing them cannot disagree. `for_variant` reports the *enum's* align for a variant (`align: parent.align`), which would over-pad every variant and inflate the enum -- caught by `check_vtable_size` on `tests/cargo-kani/iss2857` (48 vs 55 bytes). So `codegen_struct_fields`/`codegen_alignment_padding` now take the align explicitly, and a variant's own align is computed as the maximum of its fields' aligns, which is what the per-variant `LayoutData` used to carry. **`rustc_layout_scalar_valid_range_start`/`_end` were removed** in favour of pattern types, the same move `core::num::niche_types` made. The tests that define ranged scalar newtypes are converted to `std::pat::pattern_type!`. Note the consequence for autoharness: a pattern type is not an ADT and has no `Arbitrary` implementation, so `can_derive_arbitrary` cannot synthesize a struct that has one as a field, and locally-defined ranged types are now skipped rather than harnessed. The niche assumption added in model-checking#4716 is still exercised end to end through `std::time::Duration`; `tests/script-based-pre/autoharness_niche` pins both halves so the reduced reach is asserted rather than silent. **New `Rvalue::Reborrow`** (user-definable reborrowing of ADTs via `CoerceShared`). It is documented as a bitwise copy today, but the same docs anticipate it changing memory layout, so codegen reports it as an unsupported construct rather than silently modelling it as a copy. The points-to analysis treats it as pointing wherever its place does. Also adapts to: the `CodegenBackend` trait moving `CrateInfo` from `codegen_crate` to `join_codegen` (both backends), `rustc_data_structures:: stable_hasher` being renamed to `stable_hash` with `HashStable`/`hash_stable` becoming `StableHash`/`stable_hash`, the `normalize` callback of `ptr_metadata_ty{,_or_tail}` now taking `Unnormalized`, more `FieldDef::ty` and `instantiate*` sites needing `.skip_normalization()`, `TagEncoding::Niche`'s `niche_variants` becoming the lang `RangeInclusive` (public `start`/`last` fields), and the new `useless_borrows_in_formatting` clippy lint. The `vtable_size_align_drop` test no longer asserts the exact identity of the vtable's drop pointer: the drop-glue shim is now `core::ptr::drop_glue::<T>` rather than `core::ptr::drop_in_place::<T>`, and `drop_glue` is not nameable from source. It checks the slot is populated instead; the size and align fields that the test is named for are unchanged.

…ecking#4718) ### Description Stacked on model-checking#4716 and model-checking#4717 (review only the last commit). Extends `--constructor-args` with assert mining: the constructor search now prefers assert-guarded *representation constructors* (unsafe / doc-hidden / `_unchecked`-named, returning `Self`), which are inlined into the synthesized `kani::any` body with every validity statement converted into a *filter* on the nondeterministic arguments: - `kani::assert(cond, msg)` calls (Kani's macro overrides have already rewritten user asserts/panics into these) become `kani::assume(cond)`; - `hint::assert_unchecked(cond)` (UB-hint contracts, e.g. deranged's `new_unchecked`) becomes `kani::assume(cond)`; - raw panic-entry calls become `assume(false); unreachable`; - MIR `Assert` terminators (overflow checks) become `assume(cond == expected)`. Calls within the inlined body whose callees contain such validity statements are recursively inlined (depth ≤ 3, ≤ 32 blocks per callee, plain-call fallback otherwise) — this covers nested patterns like time's `Time::__from_hms_nanos_unchecked` calling deranged's `RangedU32::new_unchecked`. The insight: an unchecked representation constructor's assertions state the type's validity contract *exactly* (they were written as the caller's proof obligations), and the constructor is surjective onto the valid value space — so the generated set is precisely the values passing the type's own validity assertions. This is strictly better than assuming a checked constructor's success (which may reach only a subset of valid values and interferes with functions' own `Result` paths). Measured on time-0.3.54 (baseline 341 verified / 500 failing): checked-ctor assumption gives 538/315, hand-written `Invariant` impls for three types give 490/363, **assert mining gives 595/258** (251 harnesses fixed, 8 regressed — predominantly CBMC 60-second timeouts from formula growth of inlined generation, logged as a refinement). ### Testing The `cargo_autoharness_constructor` test gains a nested-unchecked-constructor case (a wrapper constructor calling an inner `new_unchecked` with `debug_assert`s): fails without `--constructor-args`, passes with it. Niche and autoderive suites 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>

Four upstream changes drive most of this. **Retag moved onto `Rvalue::Use`.** `StatementKind::Retag` and `RetagKind` are gone; `Rvalue::Use` now carries a `WithRetag` flag instead. Kani never modelled retags (they are Stacked-Borrows/Miri only), so the statement arms are dropped, the flag is ignored when reading a `Use`, and synthesized `Use`s pass `WithRetag::No`. `internal_mir`'s `RetagKind` conversion becomes a `WithRetag` one. **`Variants::Multiple` stores a `VariantLayout`, not a `LayoutData`.** The new type carries only per-field offsets -- no `FieldsShape` (so no field order) and no alignment. Variant layouts now come from `Layout::for_variant`, which is what `rustc_codegen_ssa` does and restores the field order; a new `variant_layout` helper is used by both the type side (`codegen_enum_cases`) and the value side (`codegen_aggregate`) so the goto struct's components and the operands initializing them cannot disagree. `for_variant` reports the *enum's* align for a variant (`align: parent.align`), which would over-pad every variant and inflate the enum -- caught by `check_vtable_size` on `tests/cargo-kani/iss2857` (48 vs 55 bytes). So `codegen_struct_fields`/`codegen_alignment_padding` now take the align explicitly, and a variant's own align is computed as the maximum of its fields' aligns, which is what the per-variant `LayoutData` used to carry. **`rustc_layout_scalar_valid_range_start`/`_end` were removed** in favour of pattern types, the same move `core::num::niche_types` made. The tests that define ranged scalar newtypes are converted to `std::pat::pattern_type!`. Note the consequence for autoharness: a pattern type is not an ADT and has no `Arbitrary` implementation, so `can_derive_arbitrary` cannot synthesize a struct that has one as a field, and locally-defined ranged types are now skipped rather than harnessed. The niche assumption added in model-checking#4716 is still exercised end to end through `std::time::Duration`; `tests/script-based-pre/autoharness_niche` pins both halves so the reduced reach is asserted rather than silent. **New `Rvalue::Reborrow`** (user-definable reborrowing of ADTs via `CoerceShared`). It is documented as a bitwise copy today, but the same docs anticipate it changing memory layout, so codegen reports it as an unsupported construct rather than silently modelling it as a copy. The points-to analysis treats it as pointing wherever its place does. Also adapts to: the `CodegenBackend` trait moving `CrateInfo` from `codegen_crate` to `join_codegen` (both backends), `rustc_data_structures:: stable_hasher` being renamed to `stable_hash` with `HashStable`/`hash_stable` becoming `StableHash`/`stable_hash`, the `normalize` callback of `ptr_metadata_ty{,_or_tail}` now taking `Unnormalized`, more `FieldDef::ty` and `instantiate*` sites needing `.skip_normalization()`, `TagEncoding::Niche`'s `niche_variants` becoming the lang `RangeInclusive` (public `start`/`last` fields), and the new `useless_borrows_in_formatting` clippy lint. The `vtable_size_align_drop` test no longer asserts the exact identity of the vtable's drop pointer: the drop-glue shim is now `core::ptr::drop_glue::<T>` rather than `core::ptr::drop_in_place::<T>`, and `drop_glue` is not nameable from source. It checks the slot is populated instead; the size and align fields that the test is named for are unchanged.

…checking#4721) ### Description Stacked on model-checking#4716/model-checking#4717/model-checking#4718 (review only the last commit). Adds autoharness support for `&[T]`, `&mut [T]` and `Vec<T>` arguments with primitive integer/float element types, generated **unbounded**: fresh allocations of nondeterministic size, so verification results hold for **all** lengths. Loops that cannot be fully unwound surface as *visible* unwinding-assertion failures instead of silently bounded successes — the soundness-signaling design validated in the top-500 evaluations (model-checking#3832). - `&mut [T]`: each call leaks a fresh allocation, so the slice is exclusive by construction. - `Vec<T>`: `from_raw_parts` with capacity matching the allocation layout (freed on drop); ZST elements use the documented dangling-pointer pattern (loop-free, as generation code must be). - The models are optional (require `alloc`), following the smart-pointer-model precedent: absent in `verify-std`'s no-core flow, where these argument types simply stay unsupported. - Element scope: only types where raw nondeterministic memory is valid as-is. The companion `SliceValidityAssume` hook (lowered directly to pure quantified goto expressions, bypassing the closure-based quantifier path) exists for niched element types, but CBMC's SAT backend silently drops symbolic-bound quantifiers (model-checking#4719), so `bool`/`NonZero*` elements remain unsupported until the in-progress CBMC quantifier-instantiation work lands — at which point `slice_elem_unbounded_ok` re-admits them. Corpus measurement (top-500, full-stack sweep): zero ICEs; the expected shift of silently-bounded loop successes into visible unwinding failures (http 6→18, prost 0→14, encoding_rs 26→35) with loop-free properties over slices/Vecs verifying for all lengths (covers pin lengths beyond 100,000). ### Testing New `cargo_autoharness_vec_unbounded` test: loop-free accessors pass for all lengths, covers verify large lengths/extreme contents/empty values reachable, a looping consumer pins the visible unwinding-failure contract, and a mutable-slice writer verifies. Constructor/niche/autoderive suites 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>

…-checking#4722) ### Description Stacked on model-checking#4716/model-checking#4717/model-checking#4718/model-checking#4721 (review only the last commit). Mines type invariants from a type's *own assertions*: conditions over the receiver's fields asserted on every normal return path of **at least two** distinct methods (a frequency filter against method-local preconditions). Corpus grounding: 1,977 such assertion sites across 131 of the top-500 crates. Admission is conservative — post-dominance (per match-arm for enums, yielding variant-guarded conjuncts), call-free single-assignment backward slices (one-level pure-getter inlining excepted), extraction into a pure expression AST that re-materializes as total, loop-free MIR. Two consumers: - under `--constructor-args` (same heuristic umbrella, same "(ctor)" marker): generated values **assume** the mined conjuncts — covering types with no viable constructor, at lower formula cost than constructor inlining; - new `--check-invariants`: values returned by verified functions are **checked** against the mined conjuncts — through `&T` and `Option`/`Result` payloads (`None`/`Err` pass vacuously) — with a distinct property message naming the asserting methods. This turns autoharness into an automatic invariant-preservation checker: the classic "constructors establish, methods preserve" obligation, with zero annotations. ### Testing The regression test pins eight behaviors: struct and enum (variant-guarded) invariants assumed for generated values (false alarms eliminated, markers attached); getter-mined conditions; a buggy producer returning an invariant-violating value caught by the output check (direct and `Result`-wrapped); correct producers and `Err` paths passing; and a single-method precondition honestly *not* mined. Constructor/niche/vec/autoderive suites 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>

tautschnig requested a review from a team as a code owner August 5, 2026 15:04

Copilot AI lite review requested due to automatic review settings August 5, 2026 15:04

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

Copilot started reviewing on behalf of tautschnig August 5, 2026 15:05 View session

Copilot AI reviewed Aug 5, 2026

View reviewed changes

Comment thread kani-compiler/src/kani_middle/transform/automatic.rs

This was referenced Aug 5, 2026

Autoharness: constructor-based value generation (--constructor-args) #4717

Merged

Autoharness: mine constructor assertions into value filters #4718

Merged

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

This was referenced Aug 6, 2026

Autoharness: unbounded slice, mutable slice and Vec arguments #4721

Merged

Autoharness: mine type invariants from a type's own assertions #4722

Merged

feliperodri added this to the Autoharness milestone Aug 18, 2026

feliperodri force-pushed the niche-pr branch from ff8ffe5 to 89bcefd Compare August 25, 2026 03:42

feliperodri requested a review from a team as a code owner August 25, 2026 03:42

feliperodri force-pushed the niche-pr branch from 89bcefd to fb013fb Compare August 25, 2026 04:21

feliperodri approved these changes Aug 25, 2026

View reviewed changes

feliperodri enabled auto-merge August 25, 2026 04:34

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

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

feliperodri mentioned this pull request Aug 25, 2026

Autoharness: generate values for pattern-type fields, restoring layout-niche coverage for user-defined ranged types #4758

Open

feliperodri mentioned this pull request Aug 25, 2026

Upgrade Rust toolchain to nightly-2026-06-01 #4760

Open

Navigation Menu

Uh oh!

Autoharness: assume layout niches of generated scalar values - #4716

Autoharness: assume layout niches of generated scalar values#4716
feliperodri merged 1 commit into
model-checking:mainfrom
tautschnig:niche-pr

tautschnig commented Aug 5, 2026 •

edited by feliperodri

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

feliperodri commented Aug 25, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

tautschnig commented Aug 5, 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

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

feliperodri commented Aug 25, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

tautschnig commented Aug 5, 2026 •

edited by feliperodri

Loading