Autoharness: support BoundedArbitrary argument types

[tautschnig]

Description

Stacked on #4691 (only the last commit is new; review that one).

Autoharness can now generate harnesses for arguments whose types implement BoundedArbitrary rather than Arbitrary — reusing Kani's existing machinery (the trait, its Vec<T>/String/Box<[T]> implementations, and #[derive(BoundedArbitrary)]) directly: the generated harness calls kani::bounded_any::<T, 4>(). Detection uses the same Instance-resolution approach as implements_arbitrary, enabled by a new fn_marker on kani::bounded_any.

Like the slice/string support in #4691, this is gated behind --bounded-arguments and reported: without the flag, eligible functions are skipped with Requires --bounded-arguments for argument(s) ...; with it, harnesses are marked (bounded) in the summary table and the post-table note spells out that results only hold up to the bound.

The bound of 4 is measured, not guessed: BoundedArbitrary values are heap allocated, and String's implementation reasons about UTF-8 validity — at bound 8, even a trivial String-consuming harness exceeds the default 60s harness timeout.

Follow-up work is planned to explore unbounded generation for container types.

Testing

New script-based test cargo_autoharness_bounded exercising both modes: the skip-reason hint without the flag; with the flag, Vec<u8>/String consumption (passes), OOB indexing on possibly-empty values (fails, correctly), a user struct deriving BoundedArbitrary with a #[bounded] field (passes), a cover check proving max-length vectors with specific contents are generated (SATISFIED), and graceful skipping of Vec<Vec<u8>>.

Full autoharness suite, verify_std_cmd/std_codegen, and compiler/driver/metadata unit tests 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

This PR extends Kani’s autoharness generation to support argument types that implement BoundedArbitrary (e.g., Vec<T>, String, and user types deriving BoundedArbitrary) in addition to existing Arbitrary/compiler-derived Arbitrary support. It does so by adding model detection for kani::bounded_any (via a new fn_marker) and updating autoharness eligibility + MIR generation to call kani::bounded_any::<T, 4>() when appropriate, alongside the already-bounded slice/&str support.

Changes:

• Add BoundedAnyModel marker and compiler-side support to detect and generate harness arguments via kani::bounded_any::<T, 4>() when T: BoundedArbitrary.
• Introduce/extend Kani model functions for bounded slice and string references (AnySliceRefModel, AnyStrRefModel) and wire them into autoharness MIR generation.
• Add script-based regression tests for bounded arguments and for slice/&str arguments; update autoharness filter expectations/docs accordingly.

Reviewed changes

Copilot reviewed 19 out of 19 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
tests/script-based-pre/cargo_autoharness_slices/src/lib.rs	New test crate exercising autoharness support for &[T]/&mut [T] and &str, including cover checks and expected failures.
tests/script-based-pre/cargo_autoharness_slices/slices.sh	Runs the new slices autoharness test.
tests/script-based-pre/cargo_autoharness_slices/slices.expected	Expected output for the slices autoharness run (incl. skip + cover statuses).
tests/script-based-pre/cargo_autoharness_slices/config.yml	Script-based test harness config for the slices test.
tests/script-based-pre/cargo_autoharness_slices/Cargo.toml	Cargo manifest for the slices test crate.
tests/script-based-pre/cargo_autoharness_filter/src/lib.rs	Updates the filter test to include a slice argument case as eligible.
tests/script-based-pre/cargo_autoharness_filter/filter.expected	Updates expected output for the filter test (now including slice eligibility).
tests/script-based-pre/cargo_autoharness_bounded/src/lib.rs	New test crate exercising autoharness support for BoundedArbitrary arguments (Vec, String, derived user type), plus skip for nested Vec<Vec<u8>>.
tests/script-based-pre/cargo_autoharness_bounded/config.yml	Script-based test harness config for the bounded test.
tests/script-based-pre/cargo_autoharness_bounded/Cargo.toml	Cargo manifest for the bounded test crate.
tests/script-based-pre/cargo_autoharness_bounded/bounded.sh	Runs the new bounded autoharness test.
tests/script-based-pre/cargo_autoharness_bounded/bounded.expected	Expected output for the bounded autoharness run (incl. skip + cover status).
library/kani_core/src/lib.rs	Adds fn_marker for kani::bounded_any so the compiler can detect BoundedArbitrary support.
library/kani_core/src/arbitrary.rs	Adds model helpers and markers for slice and &str generation (any_slice_ref, any_str_ref).
kani-compiler/src/kani_middle/transform/automatic.rs	Extends autoharness MIR generation to use slice/str models and fall back to bounded generation for T: BoundedArbitrary.
kani-compiler/src/kani_middle/mod.rs	Adds implements_bounded_arbitrary and extends argument-type eligibility to include BoundedArbitrary.
kani-compiler/src/kani_middle/kani_functions.rs	Registers new KaniModel entries: AnySliceRef, AnyStrRef, BoundedAny.
kani-compiler/src/kani_middle/codegen_units.rs	Updates autoharness partitioning logic to use the new unified “supported arg type” check and avoid cache poisoning.
docs/src/reference/experimental/autoharness.md	Documents bounded slice/str support and bounded BoundedArbitrary argument generation + caveats.

---

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

[Copilot]

Pull request overview

Copilot reviewed 12 out of 12 changed files in this pull request and generated 2 comments.

[Copilot]

Pull request overview

Copilot reviewed 12 out of 12 changed files in this pull request and generated no new comments.