Autoharness: support slice and string arguments (bounded)

[tautschnig]

Description

Autoharness can now generate harnesses for functions with &[T]/&mut [T] arguments (where T implements or can derive Arbitrary) and &str arguments — strictly opt-in via a new --bounded-arguments option, since such inputs are necessarily bounded and a verification result then only holds up to the bound. In the top-100 crates.io evaluation, these argument types accounted for ~1,400 skipped functions.

Opt-in and reporting design (bounded results must never masquerade as unbounded ones):

• Without --bounded-arguments (the default), behavior only changes in that eligible functions are skipped with a new, actionable reason: Requires --bounded-arguments for argument(s) ....
• With it, such harnesses are marked (bounded) in the "Kind of Automatic Harness" column (via a new HarnessMetadata::is_bounded field), and a note after the summary table spells out the caveat.

Generation: AnySliceRef returns &mut storage[..len] with nondet len (reborrowed as shared for &[T]), bounded at 16 elements, backed by a harness-local nondet array; AnyStrRef returns the longest valid-UTF-8 prefix of nondet bytes, bounded at 8 — full UTF-8 coverage including multi-byte characters (cover-checked), reusing the algorithm of String's BoundedArbitrary impl. Measured: assuming from_utf8(..).is_ok() is intractable even at bound 4, while the prefix formulation costs 10s@4 / 28s@8 / 180s@16, so bound 8 stays within the default 60s harness timeout. Both bounds sit below the default unwind bound of 20.

Also eliminates the argument-position vs. field-position cache-poisoning hazard class outright: top-level argument verdicts are no longer inserted into the shared Arbitrary cache (implements_arbitrary memoizes its own recursion).

Follow-up work is planned to explore unbounded generation for these types (e.g. via loop contracts or CBMC's unbounded-array reasoning), at which point the flag could be retired for them.

Testing

New script-based test cargo_autoharness_slices exercising both modes: without the flag it asserts the Requires --bounded-arguments skip reason; with the flag it checks per-function results (safe consumption passes; OOB indexing on possibly-empty slices/strings fails, correctly), the (bounded) markers, the post-table note, and four cover checks proving non-vacuity (empty slice, max-length slice with specific contents, 3-byte string with specific prefix, string starting with a non-ASCII character — all SATISFIED).

Updated cargo_autoharness_filter. Full autoharness + autoderive suites, verify_std_cmd/std_codegen, and kani-compiler/kani-driver/kani_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 slice reference arguments (&[T], &mut [T]) and string slice arguments (&str) by generating bounded, harness-owned backing storage and returning a nondeterministic-length prefix (bounded at 16). It also documents the resulting soundness/coverage caveats (bounded length; ASCII-only strings) and adds a script-based regression test suite to exercise the new behavior.

Changes:

• Add AnySliceRefModel / AnyStrRefModel models in kani_core to produce bounded-length slice/&str references from harness-owned storage.
• Update the compiler’s automatic harness generation to recognize slice/&str arguments, allocate backing locals, and call the new models.
• Add a new script-based test (cargo_autoharness_slices) and update the autoharness filter expected output to reflect slice-arg support.

Reviewed changes

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

Show a summary per file

File	Description
tests/script-based-pre/cargo_autoharness_slices/src/lib.rs	New test crate with functions covering &[T], &mut [T], and &str argument handling (pass/fail/skip + cover checks).
tests/script-based-pre/cargo_autoharness_slices/slices.sh	Script invoking cargo kani autoharness -Z autoharness for the new test.
tests/script-based-pre/cargo_autoharness_slices/slices.expected	Expected summary output including cover satisfiability and per-function results.
tests/script-based-pre/cargo_autoharness_slices/config.yml	Script-based test configuration (expects nonzero exit due to intentional failures).
tests/script-based-pre/cargo_autoharness_slices/Cargo.toml	Test crate manifest (edition 2024 + kani cfg lint config).
tests/script-based-pre/cargo_autoharness_filter/src/lib.rs	Adjust filter test to include a slice-arg function as supported.
tests/script-based-pre/cargo_autoharness_filter/filter.expected	Update expected counts/output to account for the newly supported slice-arg function.
library/kani_core/src/arbitrary.rs	Add any_slice_ref and any_str_ref model functions used by compiler-generated harnesses.
kani-compiler/src/kani_middle/transform/automatic.rs	Teach call_kani_any_for_ty to synthesize bounded slice/&str arguments via backing locals + model calls; add bound constant and new model FnDefs.
kani-compiler/src/kani_middle/mod.rs	Add autoharness_supported_arg_ty helper that treats slice refs and &str as supported argument-position types.
kani-compiler/src/kani_middle/kani_functions.rs	Register new KaniModel variants for the slice/str reference models.
kani-compiler/src/kani_middle/codegen_units.rs	Use autoharness_supported_arg_ty for arg eligibility; avoid caching slice/str-ref verdicts to prevent cache poisoning.
docs/src/reference/experimental/autoharness.md	Document slice/&str support, including the bound and ASCII-only caveats.

---

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