[CYJ904]

This PR is a first step on #4750.

Towards #4750

Problem

Autoharness generates every reference and pointer argument from its own storage, so two arguments never alias. For example, the automatic harness for

fn bump(a: &Cell<u8>, b: &Cell<u8>) {
    let old = b.get();
    a.set(old.wrapping_add(1));
    assert!(b.get() == old);
}

succeeds today, even though bump(&c, &c) violates the assertion.

Change

This adds an opt-in flag, --alias-arguments. With it, a shared reference (&T, &[T], &str) or raw pointer argument is nondeterministically either generated from its own storage, as before, or the same reference or pointer as an earlier argument of the same type.

1. A new any_alias model in kani_core (next to any_ptr) chooses between the two values.
2. AutomaticHarnessPass inserts one any_alias call per pair of compatible arguments, after all arguments are generated. The calls are chained, so with three arguments of one type every grouping is covered.
3. &mut T arguments never alias.
4. Without the flag, the generated harnesses are unchanged.
5. For functions with contracts, a precondition such as #[kani::requires(!core::ptr::eq(a, b))] excludes the aliasing case.

Not covered yet

These are documented as remaining limitations and still tracked in #4750:

1. Arguments of different types (&T with *const T, *const T with *mut T).
2. Partial overlap, such as sub-slices or a pointer into the middle of another argument.
3. References and pointers nested inside an argument.

Testing

1. cargo_autoharness_alias_arguments runs 19 functions with and without the flag. It checks each result row, the exit status, and that every failure is the intended assertion.
2. autoharness_std_alias_arguments does the same check in the --std flow.
3. All 42 autoharness tests in script-based-pre pass locally, and kani-fmt.sh --check and clippy are clean.
4. &str arguments were checked manually (Success without the flag, Failure with it) but are not in the test, since a &str harness takes about 40 seconds with or without the flag.

One note on the diff: add_auto_harness_args now takes &CommonAutoharnessArgs instead of individual flags, because one more parameter tripped clippy::too_many_arguments. Behavior is unchanged.

I kept this opt-in as the issue suggested. Happy to rename the flag, change the default, or split the remaining cases into follow-up issues if you'd prefer. Thanks for taking a look!

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Copilot review overview

🔵 Needs a closer look

The soundness-sensitive MIR instrumentation and pointer-aliasing semantics warrant final human review despite comprehensive tests.

Review effort: Balanced
Findings: None

What changed in this PR

Adds opt-in autoharness modeling for caller-controlled aliasing between compatible shared-reference and raw-pointer arguments.

Changes:

• Adds --alias-arguments across the driver and compiler.
• Generates nondeterministic alias choices using a new any_alias model.
• Documents and tests supported cases, contracts, exclusions, and --std.

File	Description
tests/​script-based-pre/​cargo_autoharness_alias_arguments/​src/​lib.rs	Defines aliasing test functions.
tests/​script-based-pre/​cargo_autoharness_alias_arguments/​config.yml	Configures the regression test.
tests/​script-based-pre/​cargo_autoharness_alias_arguments/​Cargo.toml	Defines the test crate.
tests/​script-based-pre/​cargo_autoharness_alias_arguments/​alias-arguments.sh	Runs independent and aliasing modes.
tests/​script-based-pre/​cargo_autoharness_alias_arguments/​alias-arguments.expected	Records expected verification results.
tests/​script-based-pre/​autoharness_std_alias_arguments/​verify_alias_arguments.rs	Adds standard-library test targets.
tests/​script-based-pre/​autoharness_std_alias_arguments/​config.yml	Configures the --std test.
tests/​script-based-pre/​autoharness_std_alias_arguments/​autoharness_std_alias_arguments.sh	Exercises aliasing during --std verification.
tests/​script-based-pre/​autoharness_std_alias_arguments/​autoharness_std_alias_arguments.expected	Records expected --std results.
library/​kani_core/​src/​arbitrary.rs	Adds the nondeterministic alias model.
kani-driver/​src/​autoharness/​mod.rs	Forwards the new compiler option.
kani-driver/​src/​args/​autoharness_args.rs	Exposes the user-facing flag.
kani-compiler/​src/​kani_middle/​transform/​automatic.rs	Inserts compatible argument alias choices.
kani-compiler/​src/​kani_middle/​kani_functions.rs	Registers the alias model marker.
kani-compiler/​src/​args.rs	Adds the internal compiler flag.
docs/​src/​reference/​experimental/​autoharness.md	Documents behavior and limitations.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Thanks for this. I'm approving. The comments below are suggestions, nothing blocking.

The soundness question was whether the option could generate aliasing the type system forbids. It doesn't: only &T with &T and raw pointers of the same mutability alias, and &mut T and Box never do. I built it and ran your two tests. I also ran a probe crate with and without the flag covering *mut/*mut behind a contract, &self receivers with interior mutability, &mut next to two &T, &mut [u8], Box, &&mut u8, generic functions (::<i32> and ::<i32, i32>) and --constructor-args. Every result came out where Rust's rules say it should. The aliasing bugs show up as the intended assertion failure, not as an assigns or pointer check. Cost is modest: a six-slice function went from 14.6 s to 22.3 s, and a twelve-argument function with 66 alias pairs stayed under a second.

Two things I'd like your take on:

• The output doesn't say which harnesses actually explored aliasing. A (aliasing) marker next to (bounded) and (ctor) would fix that (inline comment on mod.rs).
• *mut T with *const T is the most common shape for this kind of bug (dst/src), and it isn't covered yet. It would fit in this PR, but a follow-up under #4750 also works for me.

One doc fix outside the diff: the "Current limitations of the generated pointers" list in autoharness.md (line 222 on the head commit) still says "Distinct pointer arguments never alias each other". That should now point to --alias-arguments.

[feliperodri]

Suggestion: *const T and *mut T can alias in any caller without UB (f(p, p as *const T)), and (dst: *mut T, src: *const T) is the most common shape for an aliasing bug: it's the copy_nonoverlapping signature. I checked a probe with that signature:

#[kani::requires(kani::mem::can_dereference(dst) && kani::mem::can_dereference(src))]
#[kani::modifies(dst)]
pub unsafe fn add_one_mut_const(dst: *mut u32, src: *const u32) {
    let s = *src;
    *dst = s.wrapping_add(1);
    assert!(*src == s);
}

It verifies with --alias-arguments. The *mut u32, *mut u32 version fails as expected. Supporting it here looks small: accept raw pointers of either mutability with equal pointees, and when they differ, cast the earlier pointer with CastKind::PtrToPtr before passing it to any_alias. I'd keep &T with *mut T out, since a write through the *mut while the &T argument is live is UB under the aliasing model, so it gets more subtle. I'm fine with this landing as a follow-up under #4750 if you'd rather keep the PR as is.

[CYJ904]

Done in 4641fd3. Raw pointers to the same pointee type now alias regardless of mutability, with a PtrToPtr cast of the earlier pointer when the two differ. Your add_one_mut_const probe went from Success to Failure with the flag, and I added it to the test. &T with a raw pointer stays out as you suggested, and ref_and_mut_ptr_distinct pins that down.

[feliperodri]

Suggestion: right now there's no way to tell from the output which harnesses explored aliasing. With the flag, every row still says #[kani::proof], so a user who sees Success for fn f(a: &u8, b: &u16) can't tell that aliasing was never considered for it. --bounded-arguments and --constructor-args already solve this with AutoHarnessCaveats in codegen_units.rs, a (bounded)/(ctor) suffix, and a note under the table. An is_aliasing caveat, set when at least one any_alias call is inserted, plus an (aliasing) suffix would make "the harness of a function that does not have at least two such arguments of the same type is unaffected" visible in the results instead of only in the docs.

[CYJ904]

Good point! And also added in 4641fd3. A harness that gets at least one any_alias call is now marked (aliasing), with an is_aliasing field in the metadata and a note under the table, following how (ctor) was added in #4717. The marker and the harness generation both go through one function, aliasable_arg_pairs, so they can't disagree. In the test, different_types_distinct and muts_distinct stay unmarked, and I added two generic functions to check the marker matches after instantiation.

[feliperodri]

Suggestion: could this bullet also say that smart pointers are never aliased? fn rcs(a: Rc<Cell<u8>>, b: Rc<Cell<u8>>) { assert!(!Rc::ptr_eq(&a, &b)); } verifies with --alias-arguments, but a caller passing Rc::clone(&x) twice breaks it. The bullet only talks about references and raw pointers, so a reader could assume Rc/Arc behave like &T.

[CYJ904]

Added. The limitations list now says Rc<T> and Arc<T> arguments don't alias each other, and there's an rcs_distinct test for it. I also fixed the "Current limitations of the generated pointers" list you pointed out in the summary, so it now refers to --alias-arguments.

[feliperodri]

Praise: counting the failed checks that are not assertion failed: means a harness that starts failing for the wrong reason (a pointer check, an assigns failure in the contract cases) changes the expected output, even when its row still says Failure. The negative cases (muts_distinct, ref_and_mut_distinct, different_ptr_mutability_distinct, ref_and_ptr_distinct) pin down where aliasing must not be introduced, which matters more here than the positive ones.

[CYJ904]

Thank you, that's really encouraging! One note on the negative cases: different_ptr_mutability_distinct is now const_and_mut_ptrs_distinct and fails with the flag, since *const T and *mut T alias after your other suggestion. ref_and_mut_ptr_distinct and rcs_distinct joined the negative cases in its place.

[CYJ904]

Thanks for the thorough review, and for running all those extra probes! I've addressed the four suggestions in 4641fd3 and replied inline. Could you take another look when you have a moment?

@srivatsansamraj @Tianshu-Huang @wodex1nhaoIeng @acearyanarun I'd appreciate your eyes on this too if you have time. It adds an opt-in --alias-arguments flag for #4750, and the second commit covers the review feedback.

[feliperodri]

could you rebase this PR, @CYJ904?

[CYJ904]

Thanks, Felipe! Rebased onto the latest main. A few notes:

1. The merge commit is gone, so the branch now has the two commits you reviewed, plus one new commit on top.
2. The only conflict came from Migrate --export-json to the RFC 0015 document shape #4941, which replaced the old JSON writer. I resolved it by taking the new schema_utils.rs as is. The two reviewed commits are otherwise unchanged.
3. The new third commit adds harnesses[].is_aliasing to the RFC 0015 export, next to is_bounded, with a short "Aliased arguments" note in the RFC and the schema template and fixtures updated. The old export already carried is_aliasing, so this keeps that information in the new format. If you'd rather review it separately, I'm happy to drop it from this PR and open a follow-up.
4. I left schema_version at 0.1.0, since 0.1.0 isn't in a release yet, but adding a field is a minor change under the compatibility policy. Happy to bump it if you prefer.

The CI workflows need your approval to run again. Thanks!