Autoharness: constructor-based value generation (--constructor-args) - #4717
Open
tautschnig wants to merge 2 commits into
Open
Autoharness: constructor-based value generation (--constructor-args)#4717tautschnig wants to merge 2 commits into
tautschnig wants to merge 2 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>
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
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_rangeniche viakani::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.
Comment on lines
+165
to
+170
| pub fn add_auto_harness_args( | ||
| &mut self, | ||
| included: &[String], | ||
| excluded: &[String], | ||
| constructor_args: bool, | ||
| ) { |
Comment on lines
+334
to
+339
| if def.kind() == AdtKind::Struct | ||
| && adt_has_private_field_check(tcx, def) | ||
| && (find_unchecked_constructor(tcx, ty, kani_any_def, ty_arbitrary_cache).is_some() | ||
| || find_arbitrary_constructor(tcx, ty, kani_any_def, ty_arbitrary_cache) | ||
| .is_some()) | ||
| { |
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 (review only the last commit).
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
Datepacks 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-argsflag,kani::any::<T>for private-field structs is synthesized as: generate nondeterministic constructor arguments, call one ofT's public constructors, assume success (switching on the discriminant forOption<Self>/Result<Self, E>returns), and return the payload. Constructor search prefersSelfoverOption<Self>overResult<Self, E>returns, then more arguments over fewer; it excludes non-public, doc-hidden (_uncheckedmacro exports that assert preconditions), unsafe, zero-argument (Instant::now()reaches unsupportedclock_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_basedmetadata, 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).
Testing
New
cargo_autoharness_constructortest runs the same crate with and without the flag: without, the invariant-violating false alarms appear; with it, they disappear and harnesses carry the "(ctor)" marker. Existing autoharness 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.