Autoharness: unbounded slice, mutable slice and Vec arguments - #4721
Open
tautschnig wants to merge 4 commits into
Open
Autoharness: unbounded slice, mutable slice and Vec arguments#4721tautschnig wants to merge 4 commits into
tautschnig wants to merge 4 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>
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>
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
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], andVec<T>plus a hook for element validity assumptions. - Add
--constructor-argsplumbing 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 on lines
+26
to
+31
| /// Also create automatic harnesses for functions whose arguments require *bounded* | ||
| /// 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, |
Comment on lines
+248
to
+255
| TerminatorKind::Call { func, args, destination, target, .. } => { | ||
| remap_operand(func); | ||
| args.iter_mut().for_each(remap_operand); | ||
| remap_place(destination); | ||
| if let Some(t) = target { | ||
| *t += block_offset; | ||
| } | ||
| } |
Comment on lines
101
to
107
| let (chosen, skipped) = automatic_harness_partition( | ||
| tcx, | ||
| args, | ||
| &crate_info.name, | ||
| *kani_fns.get(&KaniModel::Any.into()).unwrap(), | ||
| kani_fns.contains_key(&KaniModel::AnySliceRefUnbounded.into()), | ||
| ); |
Comment on lines
+256
to
+263
| TerminatorKind::Assert { cond, target, .. } => { | ||
| remap_operand(cond); | ||
| *target += block_offset; | ||
| } | ||
| TerminatorKind::Drop { place, target, .. } => { | ||
| remap_place(place); | ||
| *target += block_offset; | ||
| } |
Comment on lines
+104
to
+106
| /// `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). |
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/#4717/#4718 (review only the last commit).
Adds autoharness support for
&[T],&mut [T]andVec<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_partswith capacity matching the allocation layout (freed on drop); ZST elements use the documented dangling-pointer pattern (loop-free, as generation code must be).alloc), following the smart-pointer-model precedent: absent inverify-std's no-core flow, where these argument types simply stay unsupported.SliceValidityAssumehook (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 (Warn prominently when the solver backend drops quantifiers #4719), sobool/NonZero*elements remain unsupported until the in-progress CBMC quantifier-instantiation work lands — at which pointslice_elem_unbounded_okre-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_unboundedtest: 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.