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>

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

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