Autoharness: mine constructor assertions into value filters - #4718
Open
tautschnig wants to merge 3 commits into
Open
Autoharness: mine constructor assertions into value filters#4718tautschnig wants to merge 3 commits into
tautschnig wants to merge 3 commits into
Conversation
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>
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>
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; a whitelist 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). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
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-argsplumbing 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.
Comment on lines
+27
to
+31
| /// nondeterministic values, e.g. slice references (`&[T]`, `&str`). Such harnesses are | ||
| /// marked "(bounded)" in the output, and their verification results only hold up to the | ||
| /// bounds; a bug that requires a larger input will not be found. | ||
| #[arg(long)] | ||
| pub bounded_arguments: bool, |
| pub bounded_arguments: bool, | ||
|
|
||
| /// Generate nondeterministic values for types without an Arbitrary implementation by | ||
| /// calling one of the type's own public constructors with nondeterministic arguments |
Comment on lines
+114
to
+118
| /// If we are running the autoharness subcommand, whether to generate harnesses for | ||
| /// functions whose arguments require bounded nondeterministic values (e.g. slice | ||
| /// references). See kani_driver::autoharness_args for documentation. | ||
| #[arg(long = "autoharness-bounded-arguments")] | ||
| pub autoharness_bounded_arguments: bool, |
Comment on lines
+87
to
+91
| causing false alarms in every harness that generates the type. With `--constructor-args`, Kani | ||
| instead generates values of private-field struct types by calling one of the type's public | ||
| constructors with nondeterministic arguments, assuming success for constructors returning | ||
| `Option<Self>` or `Result<Self, E>`. Constructors that are doc-hidden, unsafe, zero-argument, | ||
| or generic are not considered. |
Comment on lines
+252
to
+256
| if any_ctor { | ||
| println!( | ||
| "Note: harnesses marked \"(ctor)\" generate some values through a type's public constructor (--constructor-args);\n\ | ||
| their verification results only cover values reachable through that constructor." | ||
| ); |
This was referenced Aug 6, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Stacked on #4716 and #4717 (review only the last commit).
Extends
--constructor-argswith assert mining: the constructor search now prefers assert-guarded representation constructors (unsafe / doc-hidden /_unchecked-named, returningSelf), which are inlined into the synthesizedkani::anybody 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) becomekani::assume(cond);hint::assert_unchecked(cond)(UB-hint contracts, e.g. deranged'snew_unchecked) becomeskani::assume(cond);assume(false); unreachable;Assertterminators (overflow checks) becomeassume(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_uncheckedcalling deranged'sRangedU32::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
Resultpaths).Measured on time-0.3.54 (baseline 341 verified / 500 failing): checked-ctor assumption gives 538/315, hand-written
Invariantimpls 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_constructortest gains a nested-unchecked-constructor case (a wrapper constructor calling an innernew_uncheckedwithdebug_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.