Autoharness: add --alias-arguments to model aliasing between arguments

docs/src/reference/experimental/autoharness.md

@@ -219,7 +219,9 @@ precondition, which excludes the invalid pointer states.
 Current limitations of the generated pointers:
 - Pointers are always aligned; misaligned-pointer bugs are not covered.
 - No pointers to deallocated objects are generated (Kani's memory predicates cannot reason about those).
-- Distinct pointer arguments never alias each other, and the pointee is always initialized in the valid state.
+- By default, distinct pointer arguments never alias each other; pass `--alias-arguments` to let them alias,
+  c.f. [Reference and Pointer Arguments](#reference-and-pointer-arguments).
+- The pointee is always initialized in the valid state.
 - Raw pointers are only supported as direct arguments (possibly nested in other raw pointers), not behind
   references or inside user-defined types.
 
@@ -326,15 +328,78 @@ Note that this automatic derivation feature is only available for autoharness.
 
 ### Reference and Pointer Arguments
 Each reference, pointer, slice, or string argument is generated from its own independent
-nondeterministic storage. Autoharness therefore does *not* explore aliasing *between* distinct
-arguments: for example, given `fn f(a: &T, b: &T)`, the generated harness always passes two
+nondeterministic storage. By default, autoharness therefore does *not* explore aliasing *between*
+distinct arguments: for example, given `fn f(a: &T, b: &T)`, the generated harness always passes two
 references to separate allocations, so `a` and `b` never share an address (`core::ptr::eq(a, b)`
 is always `false`), even though a caller could pass the same reference twice. A successful
 automatic harness is thus an underapproximation with respect to caller-controlled aliasing, in
 the same way that verifying a single monomorphization is an underapproximation for [generic
 functions](#generic-functions). This applies to all reference/pointer arguments and is
 independent of the length bound that `--bounded-arguments` introduces.
-Modeling caller-controlled aliasing between arguments is tracked in
+
+The `--alias-arguments` option makes Kani explore some of this aliasing. With it, an argument that
+is a shared reference (`&T`, including `&[T]` and `&str`) or a raw pointer (`*const T`, `*mut T`) is
+nondeterministically either generated from its own storage, as above, or the very same reference or
+pointer as an earlier argument of the same type. Raw pointers alias whatever their mutability: a
+`*const T` and a `*mut T` may be the same pointer, as in `fn copy(dst: *mut T, src: *const T)`.
+`&mut T` arguments never alias anything: a `&mut T` is exclusive, so a caller cannot pass aliasing
+ones without undefined behavior. For `fn f(a: &T, b: &T)`, `a` and `b` then either refer to separate
+allocations or are the same reference, and for three arguments of one type every combination is
+covered: none aliasing, any two aliasing, and all three aliasing. For example, given:
+```rust
+fn bump(a: &Cell<u8>, b: &Cell<u8>) {
+    let old = b.get();
+    a.set(old.wrapping_add(1));
+    assert!(b.get() == old);
+}
+```
+the automatic harness for `bump` succeeds by default and fails with `--alias-arguments`, since the
+assertion does not hold if a caller passes the same `Cell` twice. The option does not change which
+functions get a harness, and the harness of a function that does not have at least two arguments
+that may alias each other is unaffected.
+
+Harnesses in which some argument may alias an earlier one are marked **"(aliasing)"** in the
+"Kind of Automatic Harness" column of the summary table, and a note after the table explains the
+marker. Unlike "(bounded)" and "(ctor)", the marker does not restrict a result: it tells you that
+the result of that harness, success or failure, also accounts for callers that pass the same
+reference or pointer for those arguments. A harness without the marker is the same one that Kani
+generates without the option.
+
+If a function is not meant to be called with aliasing arguments, say so in a [function
+contract](./contracts.md): the automatic contract harness assumes the precondition, so the
+aliasing arguments it excludes are not considered. For example, the harness for the following
+function succeeds with `--alias-arguments` as well:
+```rust
+#[kani::requires(!core::ptr::eq(a, b))]
+#[kani::modifies(a)]
+fn bump(a: &Cell<u8>, b: &Cell<u8>) {
+    let old = b.get();
+    a.set(old.wrapping_add(1));
+    assert!(b.get() == old);
+}
+```
+(The `modifies` clause is needed with or without the option, since the function writes through
+`a`.)
+
+The following limitations remain, so a successful harness is still an underapproximation with
+respect to aliasing:
+- A shared reference only aliases shared references of the same type, and a raw pointer only
+  aliases raw pointers to the same pointee type (of either mutability). References and pointers
+  to different types never share an address. Types that differ only in lifetimes count as the
+  same type.
+- A `&T` does not alias a raw pointer. For a `*mut T` this is deliberate: while the `&T` is
+  live, a write through the `*mut T` to the same value is undefined behavior under Rust's
+  aliasing model. Aliasing between a `&T` and a `*const T` is not modeled yet.
+- Smart pointer arguments (`Rc<T>`, `Arc<T>`) do not alias each other, even though a caller can pass
+  two clones of the same `Rc`.
+- Aliasing arguments are identical: slices and strings do not partially overlap, and an argument
+  never points into the middle of another one (e.g. a `&u8` into a `&[u8]`, or to a field of a
+  struct that another argument refers to).
+- Only the arguments themselves are considered. References and pointers nested in an argument, such
+  as the pointee of a `*const *const T`, always refer to their own storage, and so does the `self`
+  value of a [formatting trait implementation](#formatting-trait-implementations).
+
+Modeling the remaining cases is tracked in
 [#4750](https://github.com/model-checking/kani/issues/4750).
 
 ### Generic Functions

kani-compiler/src/args.rs

@@ -145,6 +145,11 @@ pub struct Arguments {
     /// Check mined type invariants on values returned by autoharness-verified functions.
     #[arg(long = "autoharness-check-invariants")]
     pub autoharness_check_invariants: bool,
+
+    /// Model caller-controlled aliasing between the shared reference and raw pointer
+    /// arguments of autoharness-verified functions.
+    #[arg(long = "autoharness-alias-arguments")]
+    pub autoharness_alias_arguments: bool,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]

kani-compiler/src/kani_middle/codegen_units.rs

@@ -17,8 +17,8 @@ use crate::kani_middle::metadata::{
 use crate::kani_middle::reachability::filter_crate_items;
 use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map};
 use crate::kani_middle::{
-    ArgSupport, SmartPointerModels, autoharness_supported_arg_ty, can_derive_arbitrary,
-    fmt_impl_self_ty, implements_arbitrary,
+    ArgSupport, SmartPointerModels, aliasable_arg_pairs, autoharness_supported_arg_ty,
+    can_derive_arbitrary, fmt_impl_self_ty, implements_arbitrary,
 };
 use crate::kani_queries::QueryDb;
 use kani_metadata::{
@@ -421,6 +421,7 @@ fn get_all_automatic_harnesses(
                 harness.mangled_name(),
                 caveats.is_bounded,
                 caveats.is_ctor_based,
+                caveats.is_aliasing,
             );
             (harness, metadata)
         })
@@ -1159,13 +1160,16 @@ fn choose_generic_instantiation(
 }
 
 /// The caveats that apply to a generated harness, reported in the summary table and stored in
-/// its metadata. They are independent: a harness can be both bounded and constructor-based.
+/// its metadata. They are independent: a harness can be bounded, constructor-based and aliasing
+/// at once.
 #[derive(Clone, Copy, Debug, Default)]
 struct AutoHarnessCaveats {
     /// Some argument uses *bounded* nondeterministic values, c.f. `--bounded-arguments`.
     is_bounded: bool,
     /// Some value is generated through a type's public constructor, c.f. `--constructor-args`.
     is_ctor_based: bool,
+    /// Some argument may alias an earlier one, c.f. `--alias-arguments`.
+    is_aliasing: bool,
 }
 
 /// Partition every function in the crate into (chosen, skipped), where `chosen` is a vector of the Instances for which we'll generate automatic harnesses,
@@ -1403,7 +1407,15 @@ fn automatic_harness_partition(
                             )
                         })
                     });
-                chosen.push((instance, AutoHarnessCaveats { is_bounded, is_ctor_based }));
+                // Whether the harness lets some argument alias an earlier one, which the
+                // summary reports as "(aliasing)". The harness generation inserts its aliasing
+                // choices for exactly these pairs.
+                let is_aliasing = args.autoharness_alias_arguments
+                    && !aliasable_arg_pairs(tcx, instance).is_empty();
+                chosen.push((
+                    instance,
+                    AutoHarnessCaveats { is_bounded, is_ctor_based, is_aliasing },
+                ));
             }
         }
     }

kani-compiler/src/kani_middle/kani_functions.rs

@@ -99,6 +99,8 @@ pub enum KaniModel {
     AnyCStrRef,
     #[strum(serialize = "AnyFormatterModel")]
     AnyFormatter,
+    #[strum(serialize = "AnyAliasModel")]
+    AnyAlias,
     #[strum(serialize = "AnyPtrModel")]
     AnyPtr,
     #[strum(serialize = "AnyRcModel")]

kani-compiler/src/kani_middle/metadata.rs

@@ -44,6 +44,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
         is_automatically_generated: false,
         is_bounded: false,
         is_ctor_based: false,
+        is_aliasing: false,
     }
 }
 
@@ -125,6 +126,7 @@ pub fn gen_automatic_proof_metadata(
     harness_mangled_name: String,
     is_bounded: bool,
     is_ctor_based: bool,
+    is_aliasing: bool,
 ) -> HarnessMetadata {
     let def = fn_to_verify.def;
     let pretty_name = readable_name(*fn_to_verify);
@@ -169,5 +171,6 @@ pub fn gen_automatic_proof_metadata(
         is_automatically_generated: true,
         is_bounded,
         is_ctor_based,
+        is_aliasing,
     }
 }

kani-compiler/src/kani_middle/mod.rs

@@ -1188,6 +1188,56 @@ fn fmt_impl_self_ty(tcx: TyCtxt, instance: Instance) -> Option<(FmtTrait, Ty)> {
     Some((fmt_trait, self_ty))
 }
 
+/// Whether an argument of type `later` may alias an earlier argument of type `earlier` under
+/// --alias-arguments. This is deliberately conservative: both must be shared references, or both
+/// raw pointers (of either mutability), to the same pointee type. The region of a reference is
+/// not compared, so the lifetimes the function declares do not matter.
+///
+/// A `&mut T` never aliases anything, since it is exclusive. A shared reference does not alias
+/// a raw pointer either: a write through a `*mut T` while a `&T` to the same value is live is
+/// undefined behavior, so a harness passing both for one allocation would report failures that
+/// no caller can soundly trigger. References and pointers to different types, partially
+/// overlapping slices, and references nested in other types are not modeled.
+fn can_alias_args(earlier: Ty, later: Ty) -> bool {
+    match (earlier.kind(), later.kind()) {
+        (
+            TyKind::RigidTy(RigidTy::Ref(_, earlier_pointee, Mutability::Not)),
+            TyKind::RigidTy(RigidTy::Ref(_, later_pointee, Mutability::Not)),
+        ) => earlier_pointee == later_pointee,
+        (
+            TyKind::RigidTy(RigidTy::RawPtr(earlier_pointee, _)),
+            TyKind::RigidTy(RigidTy::RawPtr(later_pointee, _)),
+        ) => earlier_pointee == later_pointee,
+        _ => false,
+    }
+}
+
+/// The pairs `(earlier, later)` of argument positions of `fn_to_verify` for which the automatic
+/// harness lets the later argument alias the earlier one under --alias-arguments, c.f.
+/// `can_alias_args`. The harness contains one `KaniModel::AnyAlias` call per pair.
+///
+/// Both the reporting of the aliasing caveat (`automatic_harness_partition`) and the harness
+/// generation (`AutomaticHarnessPass`) go through this function, so that a harness is marked
+/// as aliasing exactly if its body models aliasing. In particular, there are no such pairs for
+/// the functions handled by the formatting models (c.f. `fmt_impl_self_ty`), whose harnesses do
+/// not generate the arguments of `fn_to_verify`.
+pub fn aliasable_arg_pairs(tcx: TyCtxt, fn_to_verify: Instance) -> Vec<(usize, usize)> {
+    if fmt_impl_self_ty(tcx, fn_to_verify).is_some() {
+        return vec![];
+    }
+    let Some(body) = fn_to_verify.body() else { return vec![] };
+    let arg_tys = body.arg_locals().iter().map(|decl| decl.ty).collect::<Vec<_>>();
+    let mut pairs = vec![];
+    for later in 1..arg_tys.len() {
+        for earlier in 0..later {
+            if can_alias_args(arg_tys[earlier], arg_tys[later]) {
+                pairs.push((earlier, later));
+            }
+        }
+    }
+    pairs
+}
+
 /// Whether a pattern type's base can be generated by `call_kani_any_for_ty`: the base
 /// (an integer, bool, etc.) must implement or derive Arbitrary.
 ///

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

@@ -16,9 +16,10 @@ use crate::kani_middle::transform::body::{
 };
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_middle::{
-    CtorReturn, FmtTrait, SmartPointerModels, adt_has_private_field_check, can_derive_arbitrary,
-    find_arbitrary_constructor, fmt_impl_self_ty, implements_arbitrary, implements_invariant,
-    is_byte_str, is_c_str, is_formatter, is_wtf8, scalar_niche, smart_pointer_model_instance,
+    CtorReturn, FmtTrait, SmartPointerModels, adt_has_private_field_check, aliasable_arg_pairs,
+    can_derive_arbitrary, find_arbitrary_constructor, fmt_impl_self_ty, implements_arbitrary,
+    implements_invariant, is_byte_str, is_c_str, is_formatter, is_wtf8, scalar_niche,
+    smart_pointer_model_instance,
 };
 use crate::kani_queries::QueryDb;
 use rustc_data_structures::fx::FxHashMap;
@@ -2014,6 +2015,7 @@ impl AutomaticArbitraryPass {
         new_body.into()
     }
 }
+
 /// Transform the dummy body of an automatic_harness Kani intrinsic to be a proof harness for a given function.
 #[derive(Debug, Clone)]
 pub struct AutomaticHarnessPass {
@@ -2027,6 +2029,11 @@ pub struct AutomaticHarnessPass {
     /// Whether --check-invariants is enabled: check values returned by verified functions
     /// against the type's mined invariant conjuncts.
     check_invariants: bool,
+    /// The FnDef of KaniModel::AnyAlias
+    kani_any_alias: FnDef,
+    /// Whether --alias-arguments is enabled: let shared reference and raw pointer arguments
+    /// alias the earlier arguments they can alias, c.f. `aliasable_arg_pairs`.
+    alias_arguments: bool,
 }
 
 impl AutomaticHarnessPass {
@@ -2045,13 +2052,17 @@ impl AutomaticHarnessPass {
         let reset_clause_depth =
             Instance::resolve(reset_clause_depth, &GenericArgs(vec![])).unwrap();
         let check_invariants = query_db.args().autoharness_check_invariants;
+        let kani_any_alias = *kani_fns.get(&KaniModel::AnyAlias.into()).unwrap();
+        let alias_arguments = query_db.args().autoharness_alias_arguments;
         Self {
             models: AnyModels::new(query_db),
             check_fmt_models,
             init_contracts_hook,
             reset_clause_depth,
             kani_autoharness_intrinsic,
             check_invariants,
+            kani_any_alias,
+            alias_arguments,
         }
     }
 }
@@ -2177,7 +2188,7 @@ impl TransformPass for AutomaticHarnessPass {
         // nondeterministic value respects the type's safety invariant,
         // c.f. `call_kani_any_for_ty`.
         let mut invariant_cache = FxHashMap::default();
-        let arg_locals = fn_to_verify_body
+        let mut arg_locals = fn_to_verify_body
             .arg_locals()
             .iter()
             .map(|local_decl| {
@@ -2194,6 +2205,59 @@ impl TransformPass for AutomaticHarnessPass {
             })
             .collect::<Vec<_>>();
 
+        // Under --alias-arguments, model caller-controlled aliasing: each argument may
+        // additionally be the same reference or pointer as any earlier argument it can alias,
+        // c.f. `aliasable_arg_pairs`. The values generated above stay as they are, so each
+        // argument still covers the non-aliasing case through its own storage.
+        if self.alias_arguments {
+            let arg_tys =
+                fn_to_verify_body.arg_locals().iter().map(|decl| decl.ty).collect::<Vec<_>>();
+            for (earlier, later) in aliasable_arg_pairs(tcx, fn_to_verify) {
+                let ty = arg_tys[later];
+                // Raw pointers alias regardless of their mutability: cast the earlier pointer
+                // to the type of the later one, which is what the model returns.
+                let is_raw_ptr = matches!(ty.kind(), TyKind::RigidTy(RigidTy::RawPtr(..)));
+                let earlier_lcl = if !is_raw_ptr || arg_tys[earlier] == ty {
+                    arg_locals[earlier]
+                } else {
+                    let cast_lcl = harness_body.new_local(
+                        ty,
+                        source.span(harness_body.blocks()),
+                        Mutability::Not,
+                    );
+                    harness_body.assign_to(
+                        Place::from(cast_lcl),
+                        Rvalue::Cast(
+                            CastKind::PtrToPtr,
+                            Operand::Copy(Place::from(arg_locals[earlier])),
+                            ty,
+                        ),
+                        &mut source,
+                        InsertPosition::Before,
+                    );
+                    cast_lcl
+                };
+                let any_alias_inst = Instance::resolve(
+                    self.kani_any_alias,
+                    &GenericArgs(vec![GenericArgKind::Type(ty)]),
+                )
+                .unwrap();
+                let alias_lcl =
+                    harness_body.new_local(ty, source.span(harness_body.blocks()), Mutability::Not);
+                harness_body.insert_call(
+                    &any_alias_inst,
+                    &mut source,
+                    InsertPosition::Before,
+                    vec![
+                        Operand::Copy(Place::from(arg_locals[later])),
+                        Operand::Copy(Place::from(earlier_lcl)),
+                    ],
+                    Place::from(alias_lcl),
+                );
+                arg_locals[later] = alias_lcl;
+            }
+        }
+
         let func_to_verify_ret = fn_to_verify_body.ret_local();
         let ret_lcl = harness_body.new_local(
             func_to_verify_ret.ty,

kani-driver/src/args/autoharness_args.rs

@@ -82,6 +82,16 @@ pub struct CommonAutoharnessArgs {
     #[arg(long)]
     pub check_invariants: bool,
 
+    /// Model caller-controlled aliasing between arguments: an argument that is a shared
+    /// reference (`&T`, including `&[T]` and `&str`) or a raw pointer may additionally be the
+    /// very same reference or pointer as an earlier argument of the same type, as when a
+    /// caller passes one value twice; a `*const T` and a `*mut T` may be the same pointer,
+    /// too. Without this option, every such argument refers to its own allocation, so a bug
+    /// that requires two arguments to alias will not be found. Harnesses in which some
+    /// argument may alias another one are marked "(aliasing)" in the output.
+    #[arg(long)]
+    pub alias_arguments: bool,
+
     /// Run the `list` subcommand after generating the automatic harnesses. Note that this option implies --only-codegen.
     #[arg(long)]
     pub list: bool,