Autoharness: unbounded slice, mutable slice and Vec arguments

[tautschnig]

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.

[Copilot]

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.