Skip to content

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

Merged
feliperodri merged 1 commit into
model-checking:mainfrom
tautschnig:unbounded-pr
Aug 25, 2026
Merged

Autoharness: unbounded slice, mutable slice and Vec arguments#4721
feliperodri merged 1 commit into
model-checking:mainfrom
tautschnig:unbounded-pr

Conversation

@tautschnig

@tautschnig tautschnig commented Aug 6, 2026

Copy link
Copy Markdown
Member

Description

Stacked on #4716/#4717/#4718 (review only the last commit).

Adds autoharness support for &[T], &mut [T] and Vec<T> arguments with primitive integer/float element types, generated unbounded: fresh allocations of nondeterministic size, so verification results hold for all lengths. Loops that cannot be fully unwound surface as visible unwinding-assertion failures instead of silently bounded successes — the soundness-signaling design validated in the top-500 evaluations (#3832).

  • &mut [T]: each call leaks a fresh allocation, so the slice is exclusive by construction.
  • Vec<T>: from_raw_parts with capacity matching the allocation layout (freed on drop); ZST elements use the documented dangling-pointer pattern (loop-free, as generation code must be).
  • The models are optional (require alloc), following the smart-pointer-model precedent: absent in verify-std's no-core flow, where these argument types simply stay unsupported.
  • Element scope: only types where raw nondeterministic memory is valid as-is. The companion SliceValidityAssume hook (lowered directly to pure quantified goto expressions, bypassing the closure-based quantifier path) exists for niched element types, but CBMC's SAT backend silently drops symbolic-bound quantifiers (Fail verification when the solver backend drops quantifiers #4719), so bool/NonZero* elements remain unsupported until the in-progress CBMC quantifier-instantiation work lands — at which point slice_elem_unbounded_ok re-admits them.

Corpus measurement (top-500, full-stack sweep): zero ICEs; the expected shift of silently-bounded loop successes into visible unwinding failures (http 6→18, prost 0→14, encoding_rs 26→35) with loop-free properties over slices/Vecs verifying for all lengths (covers pin lengths beyond 100,000).

Testing

New cargo_autoharness_vec_unbounded test: loop-free accessors pass for all lengths, covers verify large lengths/extreme contents/empty values reachable, a looping consumer pins the visible unwinding-failure contract, and a mutable-slice writer verifies. Constructor/niche/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.

@tautschnig
tautschnig requested a review from a team as a code owner August 6, 2026 09:24
Copilot AI lite review requested due to automatic review settings August 6, 2026 09:24
@github-actions 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 AI reviewed Aug 6, 2026
View reviewed changes

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

Extends Kani’s autoharness value generation to cover more real-world argument shapes by adding (1) unbounded models for slice references/mutable slices and Vec<T> (for qualifying element types) and (2) constructor-based generation for private-field structs to avoid invariant-violating raw field synthesis, plus supporting metadata/reporting and regression tests.

Changes:

  • Add optional alloc-backed unbounded models for &[T], &mut [T], and Vec<T> plus a hook for element validity assumptions.
  • Add --constructor-args plumbing and metadata (is_ctor_based) to mark under-approximating constructor-based harnesses.
  • Add new script-based regression tests and docs updates for the new autoharness behaviors.

Reviewed changes

Copilot reviewed 30 out of 31 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 Runs new unbounded-Vec autoharness regression.
tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.expected Pins expected autoharness output including unwinding failure.
tests/script-based-pre/cargo_autoharness_vec_unbounded/src/lib.rs Test crate covering unbounded Vec<T> + mutable slice behavior.
tests/script-based-pre/cargo_autoharness_vec_unbounded/config.yml Script-based test configuration (expects failure).
tests/script-based-pre/cargo_autoharness_vec_unbounded/Cargo.toml New test crate manifest.
tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs Test crate for ctor-based generation and assert-mined filtering.
tests/script-based-pre/cargo_autoharness_constructor/constructor.sh Runs autoharness with/without --constructor-args and normalizes output.
tests/script-based-pre/cargo_autoharness_constructor/constructor.expected Expected output demonstrating ctor-marked harnesses.
tests/script-based-pre/cargo_autoharness_constructor/config.yml Script-based test configuration.
tests/script-based-pre/cargo_autoharness_constructor/Cargo.toml New test crate manifest.
tests/script-based-pre/autoharness_niche/run.sh Runs niche validity regression via autoharness.
tests/script-based-pre/autoharness_niche/niche_probe.rs Defines a niche-ranged scalar type used to validate niche assumptions.
tests/script-based-pre/autoharness_niche/expected Expected success output for niche regression.
tests/script-based-pre/autoharness_niche/config.yml Script-based test configuration.
library/kani/src/arbitrary.rs Adds unbounded slice/vec models and the slice_validity_assume hook stub.
kani-driver/src/sarif.rs Updates SARIF test scaffolding for new harness metadata field.
kani-driver/src/metadata.rs Updates metadata test scaffolding for new harness metadata field.
kani-driver/src/autoharness/mod.rs Adds ctor-harness marker rendering and passes ctor flag into compiler args.
kani-driver/src/args/autoharness_args.rs Adds --constructor-args (and documents --bounded-arguments).
kani-compiler/src/kani_middle/transform/body.rs Adds basic-block helpers used for inlining.
kani-compiler/src/kani_middle/transform/automatic.rs Adds constructor-based generation, inlining with mined assertions, scalar niche assumptions, and unbounded model routing.
kani-compiler/src/kani_middle/mod.rs Adds ctor selection logic, scalar niche extraction, and slice/vec element qualification logic.
kani-compiler/src/kani_middle/metadata.rs Adds is_ctor_based plumbing to autoharness metadata generation.
kani-compiler/src/kani_middle/kani_functions.rs Adds new models/hooks and marks alloc-backed models as optional.
kani-compiler/src/kani_middle/codegen_units.rs Threads ctor-based marking into harness selection; admits unbounded slice/vec args when models exist.
kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs Lowers slice_validity_assume into a quantified assumption in goto.
kani-compiler/src/args.rs Adds compiler-side flags for bounded-args and ctor-args autoharness options.
kani_metadata/src/harness.rs Adds persisted is_ctor_based field to harness metadata.
docs/src/reference/experimental/autoharness.md Documents --constructor-args behavior and its under-approximation.
Cargo.lock Updates the locked charon version entry.

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

Comment thread kani-driver/src/args/autoharness_args.rs Resolved
Comment thread kani-compiler/src/kani_middle/transform/automatic.rs Resolved
Comment thread kani-compiler/src/kani_middle/codegen_units.rs Resolved
Comment thread kani-compiler/src/kani_middle/transform/automatic.rs Resolved
Comment thread library/kani/src/arbitrary.rs Resolved
@tautschnig tautschnig mentioned this pull request Aug 6, 2026
Merged
@feliperodri feliperodri added the Z-Autoharness Issue related to autoharness subcommand label Aug 6, 2026
@tautschnig tautschnig mentioned this pull request Aug 7, 2026
Merged
@feliperodri feliperodri added this to the Autoharness milestone Aug 18, 2026
@feliperodri
feliperodri requested a review from a team as a code owner August 25, 2026 20:56
@feliperodri
feliperodri enabled auto-merge August 25, 2026 21:00
@tautschnig @kiro-agent @feliperodri
Autoharness: unbounded slice, mutable slice and Vec arguments
7018ed7 
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.

Rebased onto the mining-constructor PR (model-checking#4718): folds `unbounded_models` into
the `AnyModels` bundle and registers `cfg(kani)` for the library build. Also
folds in review-driven hardening: require all three unbounded models present
before admitting slice/Vec args in partitioning (so eligibility cannot diverge
from generation), verify the resolved model's return type matches the argument
type in `instance_for`, and match the `Global` allocator exactly rather than by
substring in `vec_elem_ty`.

Update existing autoharness .expected tests (slices, bounded, filter) for
the new unbounded behavior: `&[T]`/`&mut [T]`/`Vec<T>` of primitive
integer/float elements are now generated unbounded (no "(bounded)" marker)
and are eligible without --bounded-arguments. In particular vec_sum now
overflows u64 with an unbounded Vec (Failure), and filter's no_harness
slice/Vec functions are now selected (47 -> 50).

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@feliperodri
feliperodri added this pull request to the merge queue Aug 25, 2026
Merged via the queue into model-checking:main with commit 5da96e5 Aug 25, 2026
33 of 34 checks passed
feliperodri pushed a commit to tautschnig/kani that referenced this pull request Aug 26, 2026
@tautschnig @kiro-agent @feliperodri
Autoharness: mine type invariants from a type's own assertions
37dc8e4 
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.

Rebased onto the unbounded-args PR (model-checking#4721): folds `constructor_args` into
the `AnyModels` bundle and threads a `mined_cache` for memoization. Also
folds in review-driven hardening and toolchain-drift fixes: make
`build_guarded_conjunct` bail (skip) rather than emit an unguarded enum
conjunct, skip the `--check-invariants` payload check when its wrapper
discriminant guard cannot be built, and treat unmodeled terminators (e.g.
InlineAsm with a normal successor) conservatively in `postdominates`. The
docs now cover `--check-invariants` and the generalized `(ctor)` marker,
and note the heuristic-assume caveat (tracked in model-checking#4763). Clippy/doc lint
fixes for the new module round it out.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
feliperodri pushed a commit to tautschnig/kani that referenced this pull request Aug 26, 2026
@tautschnig @kiro-agent
Autoharness: mine type invariants from a type's own assertions (model…
e43ae2c 
…-checking#4722)

### Description

Stacked on model-checking#4716/model-checking#4717/model-checking#4718/model-checking#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 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>
feliperodri added a commit to feliperodri/kani that referenced this pull request Aug 27, 2026
@tautschnig @kiro-agent @feliperodri
Autoharness: instantiate Fn-bounded type parameters with nondet closu…
3c30080 
…res (model-checking#4726)

Stacked on model-checking#4706 (per-parameter generic instantiation); only the last
commit is new. Marked draft until model-checking#4706 merges. Part of model-checking#3832.

Fn-bound generic functions outnumber Iterator-bound ones 4:1 in the
top-500 crates.io corpus (2,373 vs 612 signatures), and no primitive
candidate can satisfy an `Fn` bound — these functions were all skipped.

### Approach
`Fn`/`FnMut`/`FnOnce`-bounded type parameters are instantiated with the
**function item type** of a matching `nondet_fn*` model: fn items
implement all three Fn traits and are zero-sized (materialized as a
constant in the harness), and each call returns a fresh nondeterministic
value — over-approximating every real closure with that signature,
including stateful `FnMut` ones. Harness names are self-documenting:
`apply::<fn(u8) -> u8 {kani::arbitrary::nondet_fn1::<u8, u8>}>`.

### Design points (each validated on the crate that motivated it)
- **Shape-based model selection**: by-value models bind input regions
early and cannot satisfy HRTB bounds like `for<'a> Fn(&'a T)`; the four
dominant by-ref shapes (96% of ref-involving corpus bounds) get
region-polymorphic models with late-bound regions.
- **Binder handling**: candidate derivation erases late-bound regions
instead of skipping binders (escaping bound vars panic the trait solver
— tap).
- **Param-referencing signatures** (`fn apply<T, F: Fn(T) -> T>`):
deferred specs substituted per candidate choice, normalized (tap), and
admission-checked against the model's own `R: Arbitrary` bound (syn).
- **Vacant vtable slots**: concrete instantiations may leave an HRTB
method slot vacant where the vtable struct type declares a pointer; pad
with typed null, mirroring rustc's layout (reqwest).
- **Arity ceiling 3, by data**: 98.5% of corpus Fn-bound signatures.

Iterator/IntoIterator-bounded parameters are a follow-up PR (the
iterator model rides on the unbounded-Vec generation of model-checking#4721).

In the crates.io sweep this converted 3,867 generic functions from
skipped to attempted, with closure-instantiated harnesses in 76 crates.

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>
Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>
@srivatsansamraj srivatsansamraj mentioned this pull request Sep 18, 2026
Open
@feliperodri feliperodri mentioned this pull request Oct 6, 2026
Closed
@feliperodri feliperodri added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Nov 6, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

Copilot code review Copilot
Copilot review effort
Applies to this pull request for everyone.Learn more about Copilot code review.
Copilot left review comments
@feliperodri feliperodri feliperodri approved these changes

Assignees

No one assigned

Labels

[C] Feature / Enhancement A new feature request or enhancement to an existing feature. Z-Autoharness Issue related to autoharness subcommand Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Milestone

Autoharness

Development

Successfully merging this pull request may close these issues.

3 participants

@tautschnig @feliperodri