Autoharness: constructor-based value generation (--constructor-args) by tautschnig · Pull Request #4717 · model-checking/kani

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

Description

The top-100/500 crates.io failure triage (#3832) showed the largest class of genuine false alarms is nondeterministic receivers violating private type invariants: e.g. time's Date packs a validated ordinal into a private field, so raw field synthesis produces invalid dates and fails every method harness (194+ harnesses in the top-100 triage attributed to this class).

Under the new opt-in --constructor-args flag, kani::any::<T> for private-field structs is synthesized as: generate nondeterministic constructor arguments, call one of T's public constructors, assume success (switching on the discriminant for Option<Self>/Result<Self, E> returns), and return the payload. Constructor search prefers Self over Option<Self> over Result<Self, E> returns, then more arguments over fewer; it excludes non-public, doc-hidden (_unchecked macro exports that assert preconditions), unsafe, zero-argument (Instant::now() reaches unsupported clock_gettime; single-point coverage regardless), and generic constructors — each exclusion was validated empirically on the time crate.

Per the bounded-features policy (#4691 discussion), the option is opt-in because it under-approximates (only constructor-reachable values are explored): harnesses are marked "(ctor)" via new is_ctor_based metadata, with an explanatory note in the summary. The sound successor (mining the type's own validity assertions into filters) is a follow-up PR building on this one.

Measured on time-0.3.54: 341 -> 538 verified, 500 -> 315 failures (203 false alarms eliminated; 17 new failures from constructors with documented panics, a logged refinement).

Note that constructor arguments must themselves already implement Arbitrary (they do not get the argument-position extensions — slices, smart pointers, nested constructors). Besides keeping phase 1 small, that requirement is what makes recursive and mutually-recursive constructors (fn combine(a: Node, b: u32) -> Node, or A::from_b/B::from_a) structurally unreachable, so generation cannot recurse forever. Verified by hand.

Changes from the original branch (rebase onto main)

main gained --bounded-arguments, per-parameter generic instantiation and the JSON frontend since this branch was cut, which surfaced three defects:

--bounded-arguments was silently ignored. The branch replaced the bounded_arguments parameter of add_auto_harness_args with constructor_args instead of adding to it. Both are now forwarded and compose: a harness that is both reads #[kani::proof] (bounded) (ctor) and both explanatory notes print independently. The compiler side carries an AutoHarnessCaveats { is_bounded, is_ctor_based } struct rather than reusing main's single bool slot, so the two independent flags cannot be swapped at a call site.
The "(ctor)" marker could lie. uses_ctor_generation also accepted find_unchecked_constructor, but nothing in AutomaticArbitraryPass used that search — and automatic::inline_with_assumed_panics, the consumer named in its doc comment, does not exist. A type whose only constructor was an _unchecked builder was therefore marked "(ctor)" and given the under-approximation caveat while generation actually fell back to raw field synthesis. Reproduced, then fixed by making the marking predicate test exactly what generation tests; find_unchecked_constructor (75 lines, no remaining callers) was removed rather than shipped as dead code, and the follow-up should reintroduce it with its consumer. Pinned by a new OnlyUnchecked case in the test.
is_ctor_based was missing from the JSON export. frontend/schema_utils.rs emitted is_bounded only, so a JSON consumer could tell a bounded run apart but not a constructor-based one. Added and asserted in schema_utils_test.rs.

Also adapted to VariantDef::idx no longer being public (reconstructed via VariantIdx::to_val, as generate_enum_body already does) and routed the pass through main's shared AnyModels instead of duplicating kani_any/kani_assume fields.

Testing

cargo_autoharness_constructor runs the same crate with and without the flag: without, the invariant-violating false alarms appear; with it, they disappear and the affected harnesses carry the "(ctor)" marker. It covers a Option<Self>-returning constructor (Day), a direct-returning one (Celsius), a Result<Self, E>-returning one (Even), and a type with only an _unchecked constructor (OnlyUnchecked) that must not be marked.

All 23 script-based autoharness tests pass, as does the full script-based-pre suite, cargo test -p kani-driver/-p kani-compiler/-p kani_metadata, clippy --workspace --tests, and kani-fmt --check.

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 extends Kani’s autoharness generation to reduce false alarms from invalid synthesized values by (a) optionally generating private-field struct values via public constructors (--constructor-args, with “(ctor)” reporting) and (b) constraining synthesized scalar values to rustc-valid layout niches. It also adds script-based regression tests and updates documentation.

Changes:

Add opt-in constructor-based value generation for private-field structs under --constructor-args, and mark affected harnesses as “(ctor)” with an explanatory note.
Constrain synthesized scalar-ABI values to their rustc_layout_scalar_valid_range niche via kani::assume.
Add script-based regression tests for both the niche handling and constructor-based generation, plus user documentation.

Reviewed changes

Copilot reviewed 21 out of 22 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs	Adds a minimal crate with private-field invariants and constructors to exercise ctor-based generation.
tests/script-based-pre/cargo_autoharness_constructor/constructor.sh	Script-based test invoking autoharness with/without `--constructor-args` and filtering output.
tests/script-based-pre/cargo_autoharness_constructor/constructor.expected	Expected output showing failures without the flag and “(ctor)” successes with it.
tests/script-based-pre/cargo_autoharness_constructor/config.yml	Wires the constructor script test into the script-based test harness.
tests/script-based-pre/cargo_autoharness_constructor/Cargo.toml	Declares the new script-based test crate.
tests/script-based-pre/autoharness_niche/run.sh	Script test driver for niche-constrained scalar generation.
tests/script-based-pre/autoharness_niche/niche_probe.rs	Defines a `rustc_layout_scalar_valid_range` type and checks both correctness and coverage reachability.
tests/script-based-pre/autoharness_niche/expected	Expected output for the niche probe.
tests/script-based-pre/autoharness_niche/config.yml	Wires the niche script test into the script-based test harness.
kani-driver/src/sarif.rs	Updates test metadata initialization for the new `is_ctor_based` field.
kani-driver/src/metadata.rs	Updates test metadata initialization for the new `is_ctor_based` field.
kani-driver/src/autoharness/mod.rs	Adds `--constructor-args` plumbing, “(ctor)” rendering, and the summary note.
kani-driver/src/args/autoharness_args.rs	Adds CLI flags/docs for `--constructor-args` (and `--bounded-arguments`).
kani-compiler/src/kani_middle/transform/automatic.rs	Implements ctor-based `kani::any` synthesis for private-field structs and niche assumptions for scalar values.
kani-compiler/src/kani_middle/mod.rs	Adds constructor discovery utilities, niche inspection, and ctor-based harness-marking support.
kani-compiler/src/kani_middle/metadata.rs	Threads `is_ctor_based` into generated harness metadata.
kani-compiler/src/kani_middle/codegen_units.rs	Computes and propagates `is_ctor_based` for automatic harness metadata.
kani-compiler/src/args.rs	Adds compiler-side flags `--autoharness-constructor-args` (and `--autoharness-bounded-arguments`).
kani_metadata/src/harness.rs	Adds `HarnessMetadata::is_ctor_based` with serde defaulting.
docs/src/reference/experimental/autoharness.md	Documents `--constructor-args` behavior and its under-approximation caveat.
Cargo.lock	Changes the locked `charon` version.

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

The top-100 crates.io failure triage (model-checking#3832) showed the largest class of genuine false alarms is generated receivers violating private type invariants (e.g. time's Date packs a validated ordinal; raw field synthesis produces invalid dates, failing every method harness). Under the new opt-in --constructor-args flag, kani::any::<T> for private-field structs is synthesized as: generate nondeterministic constructor arguments, call one of T's public constructors, assume success (switching on the discriminant for Option<Self>/Result<Self, E> returns), and return the payload. Constructor search excludes non-public, doc-hidden (commonly _unchecked variants exported for macros that assert preconditions), unsafe, zero-argument (single-point coverage; Instant::now() reaches unsupported clock_gettime), and generic constructors; it prefers Self over Option<Self> over Result<Self, E> returns, then more arguments over fewer. The option is opt-in because it under-approximates (only constructor-reachable values are explored): harnesses are marked "(ctor)" via new is_ctor_based metadata, with an explanatory note in the summary. Measured on time-0.3.54: 341 -> 538 verified, 500 -> 315 failures. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…o_fn_def The merge of main upgraded to nightly-2026-05-01, where tcx.type_of(def_id).instantiate_identity() yields an Unnormalized wrapper that no longer implements Stable. Match the rest of the codebase by stabilizing the EarlyBinder and taking its .value.

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

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>

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

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

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

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

tautschnig mentioned this pull request Aug 5, 2026

Autoharness: mine constructor assertions into value filters #4718

Merged

Copilot AI reviewed Aug 5, 2026

View reviewed changes

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

Comment thread kani-compiler/src/kani_middle/mod.rs

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

This was referenced Aug 6, 2026

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

Open

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

Open

Fix three constructor-discovery ICEs from the crates.io sweep #4725

Open

feliperodri added this to the Autoharness milestone Aug 18, 2026

feliperodri force-pushed the ctor-pr branch from 00b63ea to df99a58 Compare August 25, 2026 14:24

feliperodri requested a review from a team as a code owner August 25, 2026 14:24

feliperodri approved these changes Aug 25, 2026

View reviewed changes

feliperodri enabled auto-merge August 25, 2026 14:42

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

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 25, 2026

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

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 25, 2026

feliperodri added 2 commits August 25, 2026 12:03

Merge branch 'main' into ctor-pr

8dfba40

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

feliperodri mentioned this pull request Aug 25, 2026

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

Open

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

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

feliperodri mentioned this pull request Aug 25, 2026

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

Open

Navigation Menu

Uh oh!

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

Autoharness: constructor-based value generation (--constructor-args)#4717
feliperodri merged 3 commits into
model-checking:mainfrom
tautschnig:ctor-pr

tautschnig commented Aug 5, 2026 •

edited by feliperodri

Loading

Uh oh!

Copilot AI left a comment

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 • edited by feliperodri Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Changes from the original branch (rebase onto main)

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

tautschnig commented Aug 5, 2026 •

edited by feliperodri

Loading