Autoharness: mine type invariants from a type's own assertions by tautschnig · Pull Request #4722 · model-checking/kani

tautschnig · 2026-08-06T09:33:19Z

Description

Stacked on #4716/#4717/#4718/#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 #3832.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

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>

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. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Corpus grounding: 1,977 methods across 131 of the top-500 crates assert conditions over their own receiver's fields — a rich, directly-usable invariant source. The new kani_middle::mined_invariants module extracts such assertions into a pure expression AST. Admission requires: the assert executes on every normal return (post-dominance; for enums, post-dominance of a match arm on self's discriminant, yielding variant-guarded conjuncts), the condition's backward slice is call-free and single-assignment (one-level pure-getter inlining excepted; match-ergonomics reference bindings cancelled), and the conjunct is asserted in at least two distinct methods (rejecting method-local preconditions). The AST doubles as the canonical form for that cross-method filter and re-materializes as total, loop-free MIR (variant-guarded conjuncts emit implications over the discriminant). Consumers: - under --constructor-args (same heuristic-filter umbrella and '(ctor)' marker): generated ADT 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 the payloads of Option<T>/Result<T, E> (None/Err pass vacuously via a discriminant guard) — with a distinct property message naming the asserting methods: automatic invariant-preservation checking. The regression test pins eight behaviors incl. struct/enum invariants assumed, getter-mined conditions, buggy direct and Result producers caught, and single-method preconditions honestly not mined. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Copilot

Pull request overview

Extends Kani’s autoharness pipeline to reduce false alarms from invalid autogenerated inputs by (1) generating/ filtering values using constructor- and assertion-derived heuristics, and (2) adding optional invariant checking on function return values; it also introduces unbounded generation models for qualifying slice/Vec arguments to make results hold for all lengths.

Changes:

Add mining of type invariants from a type’s own assert-style conditions and use them as (a) generation filters and (b) return-value checks (--check-invariants).
Add unbounded argument generation models for &[T], &mut [T], and Vec<T> when element types qualify, plus a compiler hook for element validity assumptions.
Plumb new autoharness CLI/compiler flags and metadata (is_ctor_based) through reporting (including the “(ctor)” marker).

Reviewed changes

Copilot reviewed 36 out of 37 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.sh	Scripted regression driver for unbounded `Vec`/slice argument generation.
tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.expected	Expected output for the unbounded `Vec`/slice regression.
tests/script-based-pre/cargo_autoharness_vec_unbounded/src/lib.rs	Test crate exercising unbounded `Vec`/slice behaviors (coverage + unwinding failures).
tests/script-based-pre/cargo_autoharness_vec_unbounded/config.yml	Script-based test config (expects non-zero exit due to unwinding failure).
tests/script-based-pre/cargo_autoharness_vec_unbounded/Cargo.toml	Test crate manifest for the unbounded `Vec`/slice regression.
tests/script-based-pre/cargo_autoharness_mined_invariants/src/lib.rs	Test crate covering invariant mining frequency filter, getter mining, enum variant guards, and return checking.
tests/script-based-pre/cargo_autoharness_mined_invariants/mined.sh	Scripted regression driver enabling `--constructor-args` and `--check-invariants`.
tests/script-based-pre/cargo_autoharness_mined_invariants/mined.expected	Expected output including the distinct “mined invariant … violated” property.
tests/script-based-pre/cargo_autoharness_mined_invariants/config.yml	Script-based test config for mined invariants.
tests/script-based-pre/cargo_autoharness_mined_invariants/Cargo.toml	Test crate manifest for mined invariants regression.
tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs	Test crate for constructor-based generation and nested unchecked constructor inlining.
tests/script-based-pre/cargo_autoharness_constructor/constructor.sh	Script comparing outputs with/without `--constructor-args`.
tests/script-based-pre/cargo_autoharness_constructor/constructor.expected	Expected output for constructor-based generation, including “(ctor)” markers.
tests/script-based-pre/cargo_autoharness_constructor/config.yml	Script-based test config for constructor generation.
tests/script-based-pre/cargo_autoharness_constructor/Cargo.toml	Test crate manifest for constructor generation regression.
tests/script-based-pre/autoharness_niche/run.sh	Scripted regression driver for scalar niche validity assumptions.
tests/script-based-pre/autoharness_niche/niche_probe.rs	Test crate probing `rustc_layout_scalar_valid_range` niches.
tests/script-based-pre/autoharness_niche/expected	Expected output for niche validity regression.
tests/script-based-pre/autoharness_niche/config.yml	Script-based test config for niche regression.
library/kani/src/arbitrary.rs	Adds unbounded slice/`Vec` generation models plus the `slice_validity_assume` compiler hook marker.
kani-driver/src/sarif.rs	Updates test scaffolding to include new `is_ctor_based` metadata field.
kani-driver/src/metadata.rs	Updates test scaffolding to include new `is_ctor_based` metadata field.
kani-driver/src/autoharness/mod.rs	Forwards new autoharness flags into compiler args and renders “(ctor)” marker in summary output.
kani-driver/src/args/autoharness_args.rs	Adds CLI flags for constructor-based generation and mined-invariant checking (and bounded arguments).
kani-compiler/src/kani_middle/transform/body.rs	Adds MIR body utilities used by constructor inlining.
kani-compiler/src/kani_middle/transform/automatic.rs	Implements constructor-arg generation, unchecked-constructor inlining with assumed panics, mined invariant assume/check, and unbounded models integration.
kani-compiler/src/kani_middle/mod.rs	Adds constructor discovery, ctor-based marker detection, unbounded element qualification, and scalar niche extraction utilities.
kani-compiler/src/kani_middle/mined_invariants.rs	New module implementing invariant mining from a type’s own assertions.
kani-compiler/src/kani_middle/metadata.rs	Threads `is_ctor_based` into automatic harness metadata generation.
kani-compiler/src/kani_middle/kani_functions.rs	Adds optional unbounded models and the `SliceValidityAssume` hook marker; relaxes validation for optional models.
kani-compiler/src/kani_middle/codegen_units.rs	Extends harness selection pipeline to compute/store ctor-based marker and admit unbounded slice/`Vec` arguments when models are present.
kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs	Lowers `slice_validity_assume` hook to a quantified CBMC assumption.
kani-compiler/src/args.rs	Adds compiler-side autoharness flags for bounded args, constructor args, and invariant checking.
kani_metadata/src/harness.rs	Adds serialized `is_ctor_based` field to harness metadata.
docs/src/reference/experimental/autoharness.md	Documents `--constructor-args` (but not yet `--check-invariants`).
Cargo.lock	Updates dependency lockfile (includes a `charon` version change).

Suppressed comments (2)

kani-compiler/src/kani_middle/mined_invariants.rs:356

Duplicated text in this doc comment ("Whether p is a temp holding &self" appears twice) looks unintentional.

/// Whether `p` is a temp holding `&self`/// Whether `p` is a temp holding `&self` (defined once as `Ref(.., self-place)`).

kani-driver/src/autoharness/mod.rs:171

add_auto_harness_args currently forwards include/exclude patterns plus --autoharness-constructor-args/--autoharness-check-invariants, but it never forwards --autoharness-bounded-arguments, so kani autoharness --bounded-arguments won’t change compiler behavior.

        &mut self,
        included: &[String],
        excluded: &[String],
        constructor_args: bool,
        check_invariants: bool,

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

    session.add_auto_harness_args(
        &common_autoharness_args.include_pattern,
        &common_autoharness_args.exclude_pattern,
+        common_autoharness_args.constructor_args,
+        common_autoharness_args.check_invariants,
    );


+            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."
+            );


+### Constructor-based generation (--constructor-args)
+
+By default, when a type does not implement `Arbitrary`, Kani synthesizes values field by field.
+For types whose private fields carry a representation invariant (e.g. a date type storing a
+packed, validated ordinal), raw field synthesis can produce values that violate the invariant,
+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.
+
+This option is opt-in because it under-approximates: harnesses whose values are generated this
+way are marked "(ctor)" in the output, and their verification results only cover values
+reachable through the chosen constructor; a bug that requires a different value will not be
+found.
+


+/// `Vec::from_raw_parts` with `capacity == len` (the allocation came from the global
+/// allocator with exactly that layout, as `Vec`'s safety contract requires; `Vec` frees it
+/// on drop).


+    }
+}
+
+/// Whether `bb` post-dominates `from`/// Whether `bb` post-dominates `from` in `body` w.r.t. normal returns:


tautschnig and others added 5 commits August 5, 2026 15:04

Copilot AI lite review requested due to automatic review settings August 6, 2026 09:33

tautschnig requested a review from a team as a code owner August 6, 2026 09:33

github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Aug 6, 2026

Copilot started reviewing on behalf of tautschnig August 6, 2026 09:33 View session

Copilot AI reviewed Aug 6, 2026

View reviewed changes

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

Navigation Menu

Uh oh!

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

Autoharness: mine type invariants from a type's own assertions#4722
tautschnig wants to merge 5 commits into
model-checking:mainfrom
tautschnig:mined-pr

tautschnig commented Aug 6, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

tautschnig commented Aug 6, 2026

Description

Testing

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants