Autoharness: support raw pointer arguments

[tautschnig]

Description

Autoharness now generates harnesses for functions with raw pointer arguments (*const T/*mut T, including nested raw pointers), provided the pointee type implements or can derive Arbitrary. Previously such functions were skipped with "Missing Arbitrary implementation".

The generated harness produces each pointer in a nondeterministic allocation state via a new AnyPtr model:

• null,
• out of bounds (one past the end of the allocation, aligned but invalid for reads/writes), or
• valid: pointing to a nondeterministic value of the pointee type, stored in a dedicated harness local so it stays allocated for the entire harness.

Key design decision: all generated pointers are aligned and carry valid provenance, so that Kani's memory predicates can reason about them. A function with a contract such as #[kani::requires(kani::mem::can_dereference(p))] verifies successfully, because the automatic contract harness assumes the precondition, which excludes the invalid states. I validated empirically that the two obvious alternatives break this property: both pointers cast from arbitrary integer addresses and pointers to deallocated objects make kani::mem::can_dereference fail with "Kani does not support reasoning about pointer to unallocated memory", so every dereferencing function would fail even with a correct contract. Consequently those states are not generated, and this and the other limitations (always aligned, no aliasing between distinct pointer arguments, initialized pointee, pointers only as immediate arguments rather than behind references or inside ADTs) are documented in the autoharness reference.

For functions without contracts, a dereference that cannot rule out the null/out-of-bounds states fails verification, with a counterexample showing the offending pointer state — for safe functions this is a genuine robustness finding, and the documentation points users to contracts with memory predicates for functions with caller obligations.

Testing

New script-based test cargo_autoharness_raw_pointers covering: unchecked dereference (fails), null-check-only dereference (fails: out-of-bounds state remains), address-only manipulation (passes), contract harnesses with can_dereference/can_write + modifies (pass), nested pointers (address-only passes, double-deref fails), and a cover check proving the valid state is reachable and readable.

Updated cargo_autoharness_filter since raw-pointer functions are now supported rather than skipped.

Manually verified no regressions in all autoharness and autoderive script-based tests, verify_std_cmd/std_codegen (the kani_core macro is shared with no_core mode), and kani-compiler unit tests.

Towards #3832 (ticks the "Pointers" box).

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 functions that take raw pointer arguments by introducing a dedicated AnyPtr model and using it during automatic harness construction, plus adding documentation and regression tests to validate expected success/failure behavior.

Changes:

• Added an AnyPtrModel in kani_core to generate raw pointers in a controlled nondeterministic allocation state.
• Updated autoharness eligibility and harness construction to generate raw pointer arguments via AnyPtrModel (including nested raw pointers).
• Added a new script-based test crate for raw-pointer autoharness behavior and updated the existing autoharness filter test output accordingly; documented the new raw-pointer behavior and limitations.

Reviewed changes

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

Show a summary per file

File	Description
tests/script-based-pre/cargo_autoharness_raw_pointers/src/lib.rs	New test functions covering passing/failing cases for raw-pointer arguments and contract-based filtering via mem predicates.
tests/script-based-pre/cargo_autoharness_raw_pointers/raw-pointers.sh	Script-based test entrypoint invoking cargo kani autoharness with required unstable flags.
tests/script-based-pre/cargo_autoharness_raw_pointers/raw-pointers.expected	Expected output validating the new harness outcomes (success/failure + cover satisfaction).
tests/script-based-pre/cargo_autoharness_raw_pointers/config.yml	Registers the new script-based test with expected output and non-zero exit code.
tests/script-based-pre/cargo_autoharness_raw_pointers/Cargo.toml	Defines the new test crate used by the script-based test.
tests/script-based-pre/cargo_autoharness_filter/src/lib.rs	Updates the filter test to treat raw-pointer arguments as supported (moves pointer cases into the “yes harness” set).
tests/script-based-pre/cargo_autoharness_filter/filter.expected	Updates expected harness counts/rows/log ordering to reflect new raw-pointer support.
library/kani_core/src/arbitrary.rs	Introduces any_ptr<T>(storage: &mut T) -> *mut T as the AnyPtrModel used by the compiler for autoharness generation.
kani-compiler/src/kani_middle/transform/automatic.rs	Generates raw-pointer arguments using AnyPtrModel instead of kani::any() when building automatic harnesses.
kani-compiler/src/kani_middle/mod.rs	Adds autoharness_supported_arg_ty to treat raw pointers as eligible when the pointee supports Arbitrary (or derivation).
kani-compiler/src/kani_middle/kani_functions.rs	Registers the new KaniModel::AnyPtr function marker for lookup via QueryDb::kani_functions().
kani-compiler/src/kani_middle/codegen_units.rs	Switches eligibility checking to the new autoharness_supported_arg_ty logic to include raw pointers.
docs/src/reference/experimental/autoharness.md	Documents raw-pointer harness generation semantics and current limitations.

Comments suppressed due to low confidence (2)

kani-compiler/src/kani_middle/transform/automatic.rs:167

• This comment assumes the storage local “stays alive for the entire harness”, but this helper is also used while constructing derived kani::any::<T>() bodies (AutomaticArbitraryPass). In that context, the local only lives until the end of the generated kani::any call, so the comment should avoid implying a harness-wide lifetime.

        // Generate the storage for the valid-pointer case: a local with a nondeterministic value
        // of the pointee type. Since it is a local of the harness body, it stays alive for the
        // entire harness.

kani-compiler/src/kani_middle/transform/automatic.rs:172

• The comment describing the AnyPtr return states lists “dangling” and “dead object”, but AnyPtrModel only produces null, one-past-end (out-of-bounds), or a pointer to the provided storage. Keeping the terminology consistent helps readers understand what cases the harness actually explores.

        // Pass a mutable reference to the storage to the AnyPtr model, which returns a `*mut T`
        // that is either null, dangling, pointing to a dead object, or pointing to the storage.

---

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