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

[tautschnig]

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.

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