Autoharness: support BoundedArbitrary argument types

docs/src/reference/experimental/autoharness.md

@@ -165,17 +165,26 @@ smaller bound reflects the cost of reasoning about UTF-8 for symbolic execution.
 chosen to stay below the default loop-unwinding bound of 20, so that loops over the slice can
 be fully unwound by default.
 
+Additionally (also requiring `--bounded-arguments`), for arguments whose type implements
+[`BoundedArbitrary`](../bounded_arbitrary.md)
+(e.g. `Vec<T>`, `String`, or user types deriving it), the harness generates a bounded
+nondeterministic value with **bound 4** (via `kani::bounded_any`). The same caveat applies:
+verification results only hold up to the bound. The smaller bound reflects that these values are
+heap allocated and, for `String`, involve UTF-8 reasoning, both of which are costly for symbolic
+execution.
+
 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.
-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`
+By default, it must be able to do so *without bounds*: each argument 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.
+The `--bounded-arguments` option (see above) relaxes this to
+additionally allow argument types that can only be represented up to a bound: slice (`&[T]`/`&mut [T]`) and
+string (`&str`) references, and types implementing [`BoundedArbitrary`](../bounded_arbitrary.md)
+(e.g. `Vec<T>`, `String`, or user types deriving it).
 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.
 

kani-compiler/src/kani_middle/codegen_units.rs

@@ -108,6 +108,7 @@ impl CodegenUnits {
                     args,
                     &crate_info.name,
                     *kani_fns.get(&KaniModel::Any.into()).unwrap(),
+                    *kani_fns.get(&KaniModel::BoundedAny.into()).unwrap(),
                 );
                 AUTOHARNESS_MD
                     .set(AutoHarnessMetadata {
@@ -524,6 +525,7 @@ fn automatic_harness_partition(
     args: &Arguments,
     crate_name: &str,
     kani_any_def: FnDef,
+    kani_bounded_any_def: FnDef,
 ) -> (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
@@ -563,6 +565,7 @@ fn automatic_harness_partition(
 
         if is_proof_harness(tcx, instance)
             || name.contains("kani::Arbitrary")
+            || name.contains("kani::BoundedArbitrary")
             || name.contains("kani::Invariant")
         {
             return Err(AutoHarnessSkipReason::KaniImpl);
@@ -574,8 +577,8 @@ fn automatic_harness_partition(
 
         // Each argument of `instance` must be supported by automatic harness generation, i.e.,
         // 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`.
+        // opted in via --bounded-arguments -- be a supported slice/string reference or a
+        // BoundedArbitrary container type, 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![];
@@ -584,12 +587,17 @@ fn automatic_harness_partition(
             // 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);
+            // pointers, slice/string references whose backing storage the harness owns, and
+            // BoundedArbitrary container types): 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(
+                tcx,
+                arg.ty,
+                kani_any_def,
+                kani_bounded_any_def,
+                &mut ty_arbitrary_cache,
+            );
 
             if support == ArgSupport::Arbitrary {
                 continue;

kani-compiler/src/kani_middle/kani_functions.rs

@@ -75,6 +75,8 @@ pub enum KaniModel {
     AnyStrRef,
     #[strum(serialize = "AssumeSafeModel")]
     AssumeSafe,
+    #[strum(serialize = "BoundedAnyModel")]
+    BoundedAny,
     #[strum(serialize = "CopyInitStateModel")]
     CopyInitState,
     #[strum(serialize = "CopyInitStateSingleModel")]

kani-compiler/src/kani_middle/mod.rs

@@ -13,7 +13,8 @@ use rustc_public::mir::mono::{Instance, MonoItem};
 use rustc_public::mir::{Mutability, TerminatorKind};
 use rustc_public::rustc_internal;
 use rustc_public::ty::{
-    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Span as SpanStable, Ty, TyKind,
+    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Span as SpanStable, Ty, TyConst,
+    TyKind,
 };
 use rustc_public::visitor::{Visitable, Visitor as TyVisitor};
 use rustc_public::{CrateDef, DefId, local_crate};
@@ -348,6 +349,53 @@ fn implements_invariant(
     res
 }
 
+/// Whether `ty` is statically sized. Nondeterministic-value generation (and the resolution
+/// checks probing for it) must not instantiate generic models with unsized types: apart from
+/// being ungeneratable, this can crash constant evaluation during body retrieval.
+fn ty_is_sized(tcx: TyCtxt, ty: Ty) -> bool {
+    rustc_internal::internal(tcx, ty)
+        .is_sized(*tcx.at(rustc_span::DUMMY_SP), rustc_middle::ty::TypingEnv::fully_monomorphized())
+}
+
+/// Inspect a `kani::bounded_any::<T, N>()` (c.f. `KaniModel::BoundedAny`) instantiation to
+/// determine if `T: BoundedArbitrary`. The model looks like:
+/// ```rust
+/// fn bounded_any<T: BoundedArbitrary, const N: usize>() -> T {
+///   T::bounded_any::<N>()
+/// }
+/// ```
+/// So we select the terminator that calls `T::bounded_any::<N>()`, then try to resolve it to an
+/// Instance; `T` implements `BoundedArbitrary` iff we successfully resolve the Instance
+/// (mirroring `implements_arbitrary`).
+fn implements_bounded_arbitrary(tcx: TyCtxt, ty: Ty, kani_bounded_any_def: FnDef) -> bool {
+    if ty.kind().rigid().is_none() || !ty_is_sized(tcx, ty) {
+        return false;
+    }
+
+    let args = GenericArgs(vec![
+        GenericArgKind::Type(ty),
+        GenericArgKind::Const(TyConst::try_from_target_usize(1).unwrap()),
+    ]);
+    let Ok(instance) = Instance::resolve(kani_bounded_any_def, &args) else {
+        return false;
+    };
+    let Some(body) = instance.body() else {
+        return false;
+    };
+
+    for bb in body.blocks.iter() {
+        let TerminatorKind::Call { func, .. } = &bb.terminator.kind else {
+            continue;
+        };
+        if let TyKind::RigidTy(RigidTy::FnDef(def, args)) =
+            func.ty(body.arg_locals()).unwrap().kind()
+        {
+            return Instance::resolve(def, &args).is_ok();
+        }
+    }
+    false
+}
+
 /// Is `ty` a struct or enum whose fields/variants implement Arbitrary, or a reference to such a
 /// type?
 fn can_derive_arbitrary(
@@ -422,15 +470,20 @@ pub enum ArgSupport {
 /// - slice references (`&[T]`/`&mut [T]`, provided `T` implements or can derive `Arbitrary`) and
 ///   string slices (`&str`): for those, the harness generates a slice of *bounded* nondeterministic
 ///   length backed by harness-local storage, c.f. `KaniModel::AnySliceRef` and
-///   `KaniModel::AnyStrRef`.
+///   `KaniModel::AnyStrRef` (reported as [ArgSupport::Bounded]);
+/// - types that implement `BoundedArbitrary` (e.g. `Vec<T>`, `String`, or user types deriving
+///   it): the harness generates a bounded nondeterministic value via `KaniModel::BoundedAny`
+///   (reported as [ArgSupport::Bounded]).
 ///
 /// Note that raw pointers and slice/string references are only supported as immediate harness
 /// arguments (raw pointers also through other raw pointers): such a type behind a reference or
 /// inside an ADT remains unsupported, since the pointee/backing storage that the generated harness
 /// allocates would not outlive the generated value.
 fn autoharness_supported_arg_ty(
+    tcx: TyCtxt,
     ty: Ty,
     kani_any_def: FnDef,
+    kani_bounded_any_def: FnDef,
     ty_arbitrary_cache: &mut FxHashMap<Ty, bool>,
 ) -> ArgSupport {
     let arbitrary_or_derive = |ty: Ty, cache: &mut FxHashMap<Ty, bool>| {
@@ -446,7 +499,13 @@ fn autoharness_supported_arg_ty(
     if let TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _)) = ty.kind() {
         // A raw pointer is supported as long as its pointee is: propagate the pointee's verdict,
         // so a pointer to a bounded pointee (e.g. `*mut &[T]`) is itself reported as bounded.
-        autoharness_supported_arg_ty(inner_ty, kani_any_def, ty_arbitrary_cache)
+        autoharness_supported_arg_ty(
+            tcx,
+            inner_ty,
+            kani_any_def,
+            kani_bounded_any_def,
+            ty_arbitrary_cache,
+        )
     } else if let TyKind::RigidTy(RigidTy::Ref(_, inner_ty, inner_mutability)) = ty.kind() {
         match inner_ty.kind() {
             TyKind::RigidTy(RigidTy::Slice(elem_ty)) => {
@@ -468,6 +527,12 @@ fn autoharness_supported_arg_ty(
             _ => arbitrary_or_derive(ty, ty_arbitrary_cache),
         }
     } else {
-        arbitrary_or_derive(ty, ty_arbitrary_cache)
+        if arbitrary_or_derive(ty, ty_arbitrary_cache) == ArgSupport::Arbitrary {
+            ArgSupport::Arbitrary
+        } else if implements_bounded_arbitrary(tcx, ty, kani_bounded_any_def) {
+            ArgSupport::Bounded
+        } else {
+            ArgSupport::Unsupported
+        }
     }
 }