Autoharness: mine constructor assertions into value filters by tautschnig · Pull Request #4718 · model-checking/kani

tautschnig · 2026-08-05T15:53:15Z

Description

Stacked on #4716 and #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_asserts): fails without --constructor-args, passes with it. Niche and autoderive suites 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

Extends Kani’s autoharness value-generation pipeline to (optionally) generate values via constructors for private-field structs, and further improves coverage by mining validity assertions from “unchecked” representation constructors into assume-style filters during inlining. This targets reducing false alarms caused by invariant-violating nondeterministic inputs in automatically generated harnesses.

Changes:

Add --constructor-args plumbing and reporting for constructor-based autoharness generation, including (ctor) harness marking.
Implement MIR inlining + “assert mining” to convert constructor validity checks (asserts/panics/overflow asserts) into assumptions over nondeterministic constructor arguments (including limited recursive inlining).
Add new script-based regression tests for constructor-based generation and scalar layout niche constraints; update autoharness docs accordingly.

Reviewed changes

Copilot reviewed 22 out of 23 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs	New regression crate exercising constructor-based generation + nested unchecked constructors.
tests/script-based-pre/cargo_autoharness_constructor/constructor.sh	Script to compare autoharness results with/without `--constructor-args`.
tests/script-based-pre/cargo_autoharness_constructor/constructor.expected	Expected output capturing `(ctor)` marking and result deltas.
tests/script-based-pre/cargo_autoharness_constructor/config.yml	Registers the new script-based-pre test.
tests/script-based-pre/cargo_autoharness_constructor/Cargo.toml	New test crate manifest.
tests/script-based-pre/autoharness_niche/run.sh	Script-based test for scalar valid-range niche assumptions.
tests/script-based-pre/autoharness_niche/niche_probe.rs	New niche-probe test code (valid-range + cover checks).
tests/script-based-pre/autoharness_niche/expected	Expected output for niche-probe run.
tests/script-based-pre/autoharness_niche/config.yml	Registers the niche script-based-pre test.
kani-driver/src/sarif.rs	Updates SARIF test scaffolding for new harness metadata field.
kani-driver/src/metadata.rs	Updates driver metadata test scaffolding for new harness metadata field.
kani-driver/src/autoharness/mod.rs	Forwards `--constructor-args` and prints `(ctor)`/note in summary output.
kani-driver/src/args/autoharness_args.rs	Adds CLI flags for autoharness options (incl. constructor args).
kani-compiler/src/kani_middle/transform/body.rs	Adds utilities for appending/splitting basic blocks used by inlining.
kani-compiler/src/kani_middle/transform/automatic.rs	Core implementation: niche assumptions + constructor generation + assert-mining inlining.
kani-compiler/src/kani_middle/mod.rs	Adds constructor discovery, ctor-based harness marking detection, and scalar niche computation.
kani-compiler/src/kani_middle/metadata.rs	Plumbs `is_ctor_based` into generated harness metadata.
kani-compiler/src/kani_middle/codegen_units.rs	Carries `is_ctor_based` through autoharness selection/codegen metadata.
kani-compiler/src/args.rs	Adds compiler-side flags for autoharness options.
kani_metadata/src/harness.rs	Adds `is_ctor_based` to harness metadata (serde defaulted).
docs/src/reference/experimental/autoharness.md	Documents constructor-based generation option.
Cargo.lock	Updates locked dependency version(s) (notably `charon`).

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

Extend --constructor-args with assert mining: prefer assert-guarded representation constructors (unsafe / doc-hidden / _unchecked-named, returning Self; generic ADTs instantiated with their own args), 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) -> kani::assume(cond); - hint::assert_unchecked(cond) (UB-hint contracts, e.g. deranged's new_unchecked) -> kani::assume(cond); - raw panic-entry calls -> assume(false) + unreachable; - MIR Assert terminators (overflow checks) -> 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), covering nested patterns like time's Time::__from_hms_nanos_unchecked calling deranged's new_unchecked. Such a constructor is typically the raw representation builder whose asserts state the type's validity contract exactly, and is surjective onto the valid value space; the generated set is then precisely the values passing the type's own validity assertions. New MutableBody primitives push_raw_bb/split_with_terminator support the inlining; an allowlist remapper bails out (falling back to checked-constructor generation) on unsupported constructs. Measured on time-0.3.54 (vs. 341 ok / 500 fail baseline): checked-ctor assumption 538/315; hand-written invariants 490/363; assert mining 595/258 (251 fixed, 8 broke -- predominantly CBMC 60s-timeouts from formula growth, a logged refinement). Rebased onto the constructor-args PR (model-checking#4717): re-introduces find_unchecked_constructor (removed there) and adapts to the AnyModels refactor. Also folds in review-driven robustness fixes -- match hint::assert_unchecked by exact path rather than substring, guard the assert-argument access, remap `unwind: Cleanup` targets on inlined Call/Assert/Drop terminators (not just the normal target) -- and documents the vacuous-harness caveat for an unsatisfiable constructor (tracked in model-checking#4757). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Arguments of type &[T], &mut [T] and Vec<T> whose element type is a primitive integer or float are now supported, generated UNBOUNDED: the new optional (alloc-requiring) models allocate nondeterministic-size storage, so verification results hold for ALL lengths. Functions that iterate over the data surface insufficient loop bounds as visible unwinding-assertion failures rather than silently bounded successes. Mutable slices are exclusive by construction (each call leaks a fresh allocation); Vec uses from_raw_parts with capacity matching the allocation layout and frees on drop (ZST elements use the documented dangling-pointer pattern, loop-free). Element types are restricted to those where raw nondeterministic memory needs NO validity assumption (every bit pattern valid): the companion SliceValidityAssume hook, lowered directly to pure quantified goto expressions, exists for niched element types (bool, NonZero*), but CBMC's SAT backend only instantiates constant-bound quantifiers and silently drops symbolic-bound ones (see model-checking#4719), so those element types remain unsupported until the in-progress CBMC quantifier work lands. Rebased onto the mining-constructor PR (model-checking#4718): folds `unbounded_models` into the `AnyModels` bundle and registers `cfg(kani)` for the library build. Also folds in review-driven hardening: require all three unbounded models present before admitting slice/Vec args in partitioning (so eligibility cannot diverge from generation), verify the resolved model's return type matches the argument type in `instance_for`, and match the `Global` allocator exactly rather than by substring in `vec_elem_ty`. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Arguments of type &[T], &mut [T] and Vec<T> whose element type is a primitive integer or float are now supported, generated UNBOUNDED: the new optional (alloc-requiring) models allocate nondeterministic-size storage, so verification results hold for ALL lengths. Functions that iterate over the data surface insufficient loop bounds as visible unwinding-assertion failures rather than silently bounded successes. Mutable slices are exclusive by construction (each call leaks a fresh allocation); Vec uses from_raw_parts with capacity matching the allocation layout and frees on drop (ZST elements use the documented dangling-pointer pattern, loop-free). Element types are restricted to those where raw nondeterministic memory needs NO validity assumption (every bit pattern valid): the companion SliceValidityAssume hook, lowered directly to pure quantified goto expressions, exists for niched element types (bool, NonZero*), but CBMC's SAT backend only instantiates constant-bound quantifiers and silently drops symbolic-bound ones (see model-checking#4719), so those element types remain unsupported until the in-progress CBMC quantifier work lands. Rebased onto the mining-constructor PR (model-checking#4718): folds `unbounded_models` into the `AnyModels` bundle and registers `cfg(kani)` for the library build. Also folds in review-driven hardening: require all three unbounded models present before admitting slice/Vec args in partitioning (so eligibility cannot diverge from generation), verify the resolved model's return type matches the argument type in `instance_for`, and match the `Global` allocator exactly rather than by substring in `vec_elem_ty`. Update existing autoharness .expected tests (slices, bounded, filter) for the new unbounded behavior: `&[T]`/`&mut [T]`/`Vec<T>` of primitive integer/float elements are now generated unbounded (no "(bounded)" marker) and are eligible without --bounded-arguments. In particular vec_sum now overflows u64 with an unbounded Vec (Failure), and filter's no_harness slice/Vec functions are now selected (47 -> 50). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

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

### 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.

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

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

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:53 View session

Copilot AI reviewed Aug 5, 2026

View reviewed changes

Comment thread kani-driver/src/args/autoharness_args.rs

Comment thread kani-driver/src/args/autoharness_args.rs Outdated

Comment thread kani-compiler/src/args.rs

Comment thread docs/src/reference/experimental/autoharness.md Outdated

Comment thread kani-driver/src/autoharness/mod.rs

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 mentioned this pull request Aug 25, 2026

Autoharness --constructor-args: an unsatisfiable constructor yields a vacuous (always-Success) harness #4757

Open

feliperodri force-pushed the mining-pr branch from 47f83f8 to f5828db Compare August 25, 2026 18:02

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

feliperodri approved these changes Aug 25, 2026

View reviewed changes

feliperodri enabled auto-merge August 25, 2026 18:09

feliperodri force-pushed the mining-pr branch from f5828db to 7274f2c Compare August 25, 2026 18:37

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

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

feliperodri mentioned this pull request Aug 25, 2026

Autoharness --constructor-args: assumed mined invariants may exclude valid values (heuristic under-approximation) #4763

Open

rbeauchamp mentioned this pull request Aug 26, 2026

Merge current upstream Kani main into qualified fork rbeauchamp/kani#3

Merged

feliperodri mentioned this pull request Aug 27, 2026

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

Merged

Navigation Menu

Uh oh!

Autoharness: mine constructor assertions into value filters - #4718

Autoharness: mine constructor assertions into value filters#4718
feliperodri merged 1 commit into
model-checking:mainfrom
tautschnig:mining-pr

tautschnig commented Aug 5, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

tautschnig commented Aug 5, 2026

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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants