Autoharness: support slice and string arguments (bounded)

docs/src/reference/experimental/autoharness.md

@@ -145,15 +145,53 @@ Note that automatic harnesses do not *assert* type invariants, e.g., they do not
 To verify that a function preserves an invariant, add a [function contract](contracts.md) such as `#[kani::ensures(|result| result.is_safe())]`;
 autoharness verifies a function against its contract if it has one.
 
+## Bounded Arguments (opt-in: `--bounded-arguments`)
+By default, autoharness only generates harnesses whose nondeterministic inputs cover *all*
+possible values, so that a successful result carries Kani's usual guarantee. Some argument
+types (e.g. slices) can only be generated in a *bounded* fashion; because a bug that requires
+a larger input would then be missed, these are **disabled by default** and require the
+`--bounded-arguments` option. Functions that would become eligible with the option are
+reported in the skipped-functions table with reason "Requires --bounded-arguments". Harnesses
+that use bounded values are marked **"(bounded)"** in the summary table, and a note after the
+table repeats the caveat.
+
+With `--bounded-arguments`, for a function with `&[T]`/`&mut [T]` arguments (where `T`
+implements or can derive `Arbitrary`) or `&str` arguments, the generated harness produces a
+slice of nondeterministic length, backed by nondeterministic storage that lives for the entire
+harness: **up to 16 elements** for slices and **up to 4 bytes** for strings. Strings cover all
+valid UTF-8 contents up to the bound (the generated string is the longest valid-UTF-8 prefix of
+nondeterministic bytes, the same approach as `String`'s `BoundedArbitrary` implementation); the
+smaller bound reflects the cost of reasoning about UTF-8 for symbolic execution. The bounds are
+chosen to stay below the default loop-unwinding bound of 20, so that loops over the slice can
+be fully unwound by default.
+
+Nested slice references (e.g. `&&[u8]`) and slices inside user-defined types remain unsupported.
+
 ## Limitations
 ### Arguments Implementing Arbitrary
-Kani will only generate an automatic harness for a function if it can represent each of its arguments nondeterministically, without bounds.
+Kani will only generate an automatic harness for a function if it can represent each of its arguments nondeterministically.
+By default, it must be able to do so *without bounds*; the `--bounded-arguments` option (see above) relaxes this to
+additionally allow argument types that can only be represented up to a bound, such as slice (`&[T]`/`&mut [T]`) and
+string (`&str`) references.
 In technical terms, each of the arguments needs to implement the `Arbitrary`
 trait or be capable of deriving it, or be a reference (mutable or immutable)
 where any of the prior requirements is fulfilled by the referenced type.
 Kani will detect if a struct or enum could implement `Arbitrary` and derive it automatically.
 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
+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
+[#4750](https://github.com/model-checking/kani/issues/4750).
+
 ### Generic Functions
 For a generic function, Kani generates a harness for a single monomorphic instantiation of the function:
 it substitutes every type parameter with the first candidate from a fixed list of primitive types

kani-compiler/src/args.rs

@@ -117,6 +117,11 @@ pub struct Arguments {
     /// See kani_driver::autoharness_args for documentation.
     #[arg(long = "autoharness-exclude-pattern", num_args(1))]
     pub autoharness_excluded_patterns: Vec<String>,
+    /// If we are running the autoharness subcommand, whether to generate harnesses for
+    /// functions whose arguments require bounded nondeterministic values (e.g. slice
+    /// references). See kani_driver::autoharness_args for documentation.
+    #[arg(long = "autoharness-bounded-arguments")]
+    pub autoharness_bounded_arguments: bool,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]

kani-compiler/src/kani_middle/codegen_units.rs

@@ -9,13 +9,13 @@
 
 use crate::args::{Arguments, ReachabilityType};
 use crate::kani_middle::attributes::{KaniAttributes, is_proof_harness};
-use crate::kani_middle::autoharness_supported_arg_ty;
 use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel};
 use crate::kani_middle::metadata::{
     gen_automatic_proof_metadata, gen_contracts_metadata, gen_proof_metadata,
 };
 use crate::kani_middle::reachability::filter_crate_items;
 use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map};
+use crate::kani_middle::{ArgSupport, autoharness_supported_arg_ty};
 use crate::kani_queries::QueryDb;
 use kani_metadata::{
     ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessMetadata,
@@ -113,7 +113,9 @@ impl CodegenUnits {
                     .set(AutoHarnessMetadata {
                         chosen: chosen
                             .iter()
-                            .map(|func| crate::kani_middle::strip_local_crate_prefix(func.name()))
+                            .map(|(func, _)| {
+                                crate::kani_middle::strip_local_crate_prefix(func.name())
+                            })
                             .collect::<BTreeSet<_>>(),
                         skipped,
                     })
@@ -366,13 +368,13 @@ fn determine_targets(
 /// the AutomaticHarnessPass will later transform the bodies of these instances to actually verify the function.
 fn get_all_automatic_harnesses(
     tcx: TyCtxt,
-    verifiable_fns: Vec<Instance>,
+    verifiable_fns: Vec<(Instance, bool)>,
     kani_harness_intrinsic: FnDef,
     base_filename: &Path,
 ) -> HashMap<Harness, HarnessMetadata> {
     verifiable_fns
         .into_iter()
-        .map(|fn_to_verify| {
+        .map(|(fn_to_verify, is_bounded)| {
             // Set the generic arguments of the harness to be the function it is verifying
             // so that later, in AutomaticHarnessPass, we can retrieve the function to verify
             // and generate the harness body accordingly.
@@ -386,6 +388,7 @@ fn get_all_automatic_harnesses(
                 base_filename,
                 &fn_to_verify,
                 harness.mangled_name(),
+                is_bounded,
             );
             (harness, metadata)
         })
@@ -521,7 +524,7 @@ fn automatic_harness_partition(
     args: &Arguments,
     crate_name: &str,
     kani_any_def: FnDef,
-) -> (Vec<Instance>, BTreeMap<String, AutoHarnessSkipReason>) {
+) -> (Vec<(Instance, bool)>, BTreeMap<String, AutoHarnessSkipReason>) {
     let crate_fn_defs = rustc_public::local_crate().fn_defs().into_iter().collect::<FxHashSet<_>>();
     // Filter out CrateItems that are functions, but not functions defined in the crate itself, i.e., rustc-inserted functions
     // (c.f. https://github.com/model-checking/kani/issues/4189)
@@ -539,12 +542,14 @@ fn automatic_harness_partition(
     // Cache whether a type implements or can derive Arbitrary
     let mut ty_arbitrary_cache: FxHashMap<Ty, bool> = FxHashMap::default();
 
-    // If `instance` is not eligible for an automatic harness, return the reason why; if it is eligible, return None.
+    // If `instance` is not eligible for an automatic harness, return the reason why (`Err`); if it
+    // is eligible, return whether its harness requires *bounded* nondeterministic arguments
+    // (`Ok(true)` iff so).
     // Note that we only return one reason for ineligiblity, when there could be multiple;
     // we can revisit this implementation choice in the future if users request more verbose output.
-    let mut skip_reason = |instance: Instance| -> Option<AutoHarnessSkipReason> {
+    let mut skip_reason = |instance: Instance| -> Result<bool, AutoHarnessSkipReason> {
         if !instance.has_body() {
-            return Some(AutoHarnessSkipReason::NoBody);
+            return Err(AutoHarnessSkipReason::NoBody);
         }
 
         // Preprend the crate name so that users can filter out entire crates using the existing function filter flags.
@@ -560,55 +565,58 @@ fn automatic_harness_partition(
             || name.contains("kani::Arbitrary")
             || name.contains("kani::Invariant")
         {
-            return Some(AutoHarnessSkipReason::KaniImpl);
+            return Err(AutoHarnessSkipReason::KaniImpl);
         }
 
         if autoharness_filtered_out(&name, &included_set, &excluded_set) {
-            return Some(AutoHarnessSkipReason::UserFilter);
+            return Err(AutoHarnessSkipReason::UserFilter);
         }
 
         // Each argument of `instance` must be supported by automatic harness generation, i.e.,
-        // implement Arbitrary (or be capable of deriving it), or be a raw pointer,
+        // implement Arbitrary (or be capable of deriving it), be a raw pointer, or -- if the user
+        // opted in via --bounded-arguments -- be a supported slice/string reference,
         // c.f. `autoharness_supported_arg_ty`.
         // Note that generic functions have been instantiated with concrete types at this point,
         // so we know that each of these arguments has a concrete type.
         let mut problematic_args = vec![];
+        let mut bounded_args = vec![];
         for (idx, arg) in body.arg_locals().iter().enumerate() {
-            // Do not cache raw pointer types: `ty_arbitrary_cache` stores whether a type
-            // implements (or can derive) Arbitrary, which is false for raw pointers --
-            // `implements_arbitrary` inserts that verdict when it encounters a raw pointer as an
-            // ADT field. Raw pointers are nevertheless supported as harness arguments, so caching
-            // the argument-position verdict under the same key would poison the cache in one
-            // direction or the other (c.f. `autoharness_supported_arg_ty`).
-            let impls_arbitrary = if matches!(arg.ty.kind(), TyKind::RigidTy(RigidTy::RawPtr(..))) {
-                autoharness_supported_arg_ty(arg.ty, kani_any_def, &mut ty_arbitrary_cache)
-            } else {
-                if !ty_arbitrary_cache.contains_key(&arg.ty) {
-                    let supported =
-                        autoharness_supported_arg_ty(arg.ty, kani_any_def, &mut ty_arbitrary_cache);
-                    ty_arbitrary_cache.insert(arg.ty, supported);
-                }
-                *ty_arbitrary_cache.get(&arg.ty).unwrap()
-            };
-
-            if !impls_arbitrary {
-                // Find the name of the argument by referencing var_debug_info.
-                // Note that enumerate() starts at 0, while rustc_public argument_index starts at 1, hence the idx+1.
-                let arg_name = body
-                    .var_debug_info
-                    .iter()
-                    .find(|var| {
-                        var.argument_index.is_some_and(|arg_idx| idx + 1 == usize::from(arg_idx))
-                    })
-                    .map_or("_".to_string(), |debug_info| debug_info.name.to_string());
-                let arg_type = format!("{}", arg.ty);
-                problematic_args.push((arg_name, arg_type))
+            // Note: we deliberately do not insert the verdict into `ty_arbitrary_cache` here.
+            // The cache stores whether a type implements (or can derive) Arbitrary, which is the
+            // wrong semantics for types that are supported in argument position only (raw
+            // pointers, and slice/string references whose backing storage the harness owns):
+            // caching the argument-position verdict under the same key would poison the cache for
+            // the ADT-field checks. `implements_arbitrary` memoizes its own recursion internally,
+            // so repeated argument types stay cheap.
+            let support =
+                autoharness_supported_arg_ty(arg.ty, kani_any_def, &mut ty_arbitrary_cache);
+
+            if support == ArgSupport::Arbitrary {
+                continue;
+            }
+            // Find the name of the argument by referencing var_debug_info.
+            // Note that enumerate() starts at 0, while rustc_public argument_index starts at 1, hence the idx+1.
+            let arg_name = body
+                .var_debug_info
+                .iter()
+                .find(|var| {
+                    var.argument_index.is_some_and(|arg_idx| idx + 1 == usize::from(arg_idx))
+                })
+                .map_or("_".to_string(), |debug_info| debug_info.name.to_string());
+            let arg_type = format!("{}", arg.ty);
+            match support {
+                ArgSupport::Arbitrary => unreachable!(),
+                ArgSupport::Bounded => bounded_args.push((arg_name, arg_type)),
+                ArgSupport::Unsupported => problematic_args.push((arg_name, arg_type)),
             }
         }
         if !problematic_args.is_empty() {
-            return Some(AutoHarnessSkipReason::MissingArbitraryImpl(problematic_args));
+            return Err(AutoHarnessSkipReason::MissingArbitraryImpl(problematic_args));
         }
-        None
+        if !bounded_args.is_empty() && !args.autoharness_bounded_arguments {
+            return Err(AutoHarnessSkipReason::RequiresBoundedArguments(bounded_args));
+        }
+        Ok(!bounded_args.is_empty())
     };
 
     let mut chosen = vec![];
@@ -640,10 +648,12 @@ fn automatic_harness_partition(
             },
         };
 
-        if let Some(reason) = skip_reason(instance) {
-            skipped.insert(crate::kani_middle::strip_local_crate_prefix(instance.name()), reason);
-        } else {
-            chosen.push(instance);
+        match skip_reason(instance) {
+            Err(reason) => {
+                skipped
+                    .insert(crate::kani_middle::strip_local_crate_prefix(instance.name()), reason);
+            }
+            Ok(is_bounded) => chosen.push((instance, is_bounded)),
         }
     }
 

kani-compiler/src/kani_middle/kani_functions.rs

@@ -69,6 +69,10 @@ pub enum KaniModel {
     Any,
     #[strum(serialize = "AnyPtrModel")]
     AnyPtr,
+    #[strum(serialize = "AnySliceRefModel")]
+    AnySliceRef,
+    #[strum(serialize = "AnyStrRefModel")]
+    AnyStrRef,
     #[strum(serialize = "AssumeSafeModel")]
     AssumeSafe,
     #[strum(serialize = "CopyInitStateModel")]

kani-compiler/src/kani_middle/metadata.rs

@@ -42,6 +42,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
         contract: Default::default(),
         has_loop_contracts: false,
         is_automatically_generated: false,
+        is_bounded: false,
     }
 }
 
@@ -121,6 +122,7 @@ pub fn gen_automatic_proof_metadata(
     base_name: &Path,
     fn_to_verify: &Instance,
     harness_mangled_name: String,
+    is_bounded: bool,
 ) -> HarnessMetadata {
     let def = fn_to_verify.def;
     let pretty_name = readable_name(*fn_to_verify);
@@ -163,5 +165,6 @@ pub fn gen_automatic_proof_metadata(
         contract: Default::default(),
         has_loop_contracts: false,
         is_automatically_generated: true,
+        is_bounded,
     }
 }