Autoharness: support smart pointers of compiler-derivable pointees

kani-compiler/src/kani_middle/codegen_units.rs

@@ -15,7 +15,7 @@ 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::{can_derive_arbitrary, implements_arbitrary};
+use crate::kani_middle::{SmartPointerModels, autoharness_supported_arg_ty};
 use crate::kani_queries::QueryDb;
 use kani_metadata::{
     ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessMetadata,
@@ -103,6 +103,7 @@ impl CodegenUnits {
                     args,
                     &crate_info.name,
                     *kani_fns.get(&KaniModel::Any.into()).unwrap(),
+                    SmartPointerModels::from_kani_functions(kani_fns),
                 );
                 AUTOHARNESS_MD
                     .set(AutoHarnessMetadata {
@@ -417,6 +418,7 @@ fn automatic_harness_partition(
     args: &Arguments,
     crate_name: &str,
     kani_any_def: FnDef,
+    smart_pointer_models: SmartPointerModels,
 ) -> (Vec<Instance>, 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
@@ -474,17 +476,24 @@ fn automatic_harness_partition(
             return Some(AutoHarnessSkipReason::UserFilter);
         }
 
-        // Each argument of `instance` must implement Arbitrary.
+        // Each argument of `instance` must be supported by automatic harness generation, i.e.,
+        // implement Arbitrary (or be capable of deriving it), or be a supported smart pointer,
+        // c.f. `autoharness_supported_arg_ty`.
         // Note that we've already filtered out generic functions, so we know that each of these arguments has a concrete type.
+        // 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 (smart pointers of
+        // derivable pointees); `implements_arbitrary` memoizes its own recursion internally,
+        // so repeated argument types stay cheap.
         let mut problematic_args = vec![];
         for (idx, arg) in body.arg_locals().iter().enumerate() {
-            if !ty_arbitrary_cache.contains_key(&arg.ty) {
-                let impls_arbitrary =
-                    implements_arbitrary(arg.ty, kani_any_def, &mut ty_arbitrary_cache)
-                        || can_derive_arbitrary(arg.ty, kani_any_def, &mut ty_arbitrary_cache);
-                ty_arbitrary_cache.insert(arg.ty, impls_arbitrary);
-            }
-            let impls_arbitrary = ty_arbitrary_cache.get(&arg.ty).unwrap();
+            let impls_arbitrary = &autoharness_supported_arg_ty(
+                tcx,
+                arg.ty,
+                kani_any_def,
+                &smart_pointer_models,
+                &mut ty_arbitrary_cache,
+            );
 
             if !impls_arbitrary {
                 // Find the name of the argument by referencing var_debug_info.

kani-compiler/src/kani_middle/kani_functions.rs

@@ -67,6 +67,12 @@ pub enum KaniModel {
     AlignOfVal,
     #[strum(serialize = "AnyModel")]
     Any,
+    #[strum(serialize = "AnyArcModel")]
+    AnyArc,
+    #[strum(serialize = "AnyBoxModel")]
+    AnyBox,
+    #[strum(serialize = "AnyRcModel")]
+    AnyRc,
     #[strum(serialize = "CopyInitStateModel")]
     CopyInitState,
     #[strum(serialize = "CopyInitStateSingleModel")]
@@ -162,6 +168,15 @@ pub enum KaniHook {
     UntrackedDeref,
 }
 
+impl KaniModel {
+    /// Whether this model may legitimately be absent. The smart-pointer models require `alloc`
+    /// and are only defined in the `kani` library, not in `core::kani` (the `no_core` flow used
+    /// by `kani verify-std`). Code retrieving optional models must handle their absence.
+    pub fn is_optional(&self) -> bool {
+        matches!(self, KaniModel::AnyArc | KaniModel::AnyBox | KaniModel::AnyRc)
+    }
+}
+
 impl From<KaniIntrinsic> for KaniFunction {
     fn from(value: KaniIntrinsic) -> Self {
         KaniFunction::Intrinsic(value)
@@ -271,7 +286,7 @@ pub fn validate_kani_functions(kani_funcs: &HashMap<KaniFunction, FnDef>) {
     {
         if let Some(fn_def) = kani_funcs.get(&func) {
             assert_eq!(KaniFunction::try_from(*fn_def), Ok(func), "Unexpected function marker");
-        } else {
+        } else if !matches!(func, KaniFunction::Model(model) if model.is_optional()) {
             tracing::error!(?func, "Missing kani function");
             missing += 1;
         }

kani-compiler/src/kani_middle/mod.rs

@@ -300,6 +300,123 @@ fn implements_arbitrary(
     false
 }
 
+/// The smart-pointer types for which automatic harnesses can generate nondeterministic values
+/// via dedicated (optional) models, c.f. `KaniModel::is_optional`.
+#[derive(Copy, Clone, Debug, Eq, PartialEq)]
+pub enum SmartPointerKind {
+    Arc,
+    Box,
+    Rc,
+}
+
+/// If `ty` is `Box<T>`, `Rc<T>`, or `Arc<T>`, return the pointer kind and the pointee type `T`.
+/// Note that `Box<T, A>`/`Rc<T, A>`/`Arc<T, A>` with a non-default allocator are not
+/// recognized, and unsized pointees (e.g. `Box<[T]>`) are rejected by the caller's
+/// Arbitrary check on the pointee.
+fn smart_pointer_pointee(tcx: TyCtxt, ty: Ty) -> Option<(SmartPointerKind, Ty)> {
+    let TyKind::RigidTy(RigidTy::Adt(def, args)) = ty.kind() else {
+        return None;
+    };
+
+    let kind = if def.is_box() {
+        SmartPointerKind::Box
+    } else {
+        let def_id = rustc_internal::internal(tcx, def.def_id());
+        if tcx.get_diagnostic_item(rustc_span::sym::Rc) == Some(def_id) {
+            SmartPointerKind::Rc
+        } else if tcx.get_diagnostic_item(rustc_span::sym::Arc) == Some(def_id) {
+            SmartPointerKind::Arc
+        } else {
+            return None;
+        }
+    };
+
+    // The first generic argument is the pointee. (The remaining argument is the allocator,
+    // which is validated by the model return-type check in `smart_pointer_model_instance`.)
+    let pointee = args.0.iter().find_map(|arg| match arg {
+        GenericArgKind::Type(ty) => Some(*ty),
+        _ => None,
+    })?;
+    Some((kind, pointee))
+}
+
+/// If `ty` is a supported smart-pointer type whose generation model is available, resolve the
+/// model for the pointee and return it together with the pointee type. Returns `None` if the
+/// model's return type does not match `ty` exactly (e.g. for a non-default allocator).
+fn smart_pointer_model_instance(
+    tcx: TyCtxt,
+    ty: Ty,
+    smart_pointer_models: &SmartPointerModels,
+) -> Option<(Instance, Ty)> {
+    let (kind, pointee) = smart_pointer_pointee(tcx, ty)?;
+    let model = smart_pointer_models.for_kind(kind)?;
+    let instance =
+        Instance::resolve(model, &GenericArgs(vec![GenericArgKind::Type(pointee)])).ok()?;
+    let TyKind::RigidTy(RigidTy::FnDef(..)) = instance.ty().kind() else {
+        return None;
+    };
+    let ret_ty = instance.ty().kind().fn_sig()?.skip_binder().output();
+    (ret_ty == ty).then_some((instance, pointee))
+}
+
+/// The (optional) smart-pointer generation models, c.f. `smart_pointer_pointee`.
+/// `None` entries mean the model is unavailable (e.g. in the `no_core` flow, which has no
+/// `alloc`), in which case the corresponding smart-pointer types are not supported.
+#[derive(Copy, Clone, Debug)]
+pub struct SmartPointerModels {
+    pub any_arc: Option<FnDef>,
+    pub any_box: Option<FnDef>,
+    pub any_rc: Option<FnDef>,
+}
+
+impl SmartPointerModels {
+    pub fn from_kani_functions(
+        kani_fns: &std::collections::HashMap<
+            crate::kani_middle::kani_functions::KaniFunction,
+            FnDef,
+        >,
+    ) -> Self {
+        use crate::kani_middle::kani_functions::KaniModel;
+        SmartPointerModels {
+            any_arc: kani_fns.get(&KaniModel::AnyArc.into()).copied(),
+            any_box: kani_fns.get(&KaniModel::AnyBox.into()).copied(),
+            any_rc: kani_fns.get(&KaniModel::AnyRc.into()).copied(),
+        }
+    }
+
+    pub fn for_kind(&self, kind: SmartPointerKind) -> Option<FnDef> {
+        match kind {
+            SmartPointerKind::Arc => self.any_arc,
+            SmartPointerKind::Box => self.any_box,
+            SmartPointerKind::Rc => self.any_rc,
+        }
+    }
+}
+
+/// Can an automatic harness generate a nondeterministic value of type `ty` for a harness
+/// argument? In addition to the types that implement or can derive `Arbitrary`, automatic
+/// harnesses support `Box<T>`/`Rc<T>`/`Arc<T>` where `T` itself implements or can derive
+/// `Arbitrary`, provided the corresponding generation model is available,
+/// c.f. `smart_pointer_pointee`.
+fn autoharness_supported_arg_ty(
+    tcx: TyCtxt,
+    ty: Ty,
+    kani_any_def: FnDef,
+    smart_pointer_models: &SmartPointerModels,
+    ty_arbitrary_cache: &mut FxHashMap<Ty, bool>,
+) -> bool {
+    if implements_arbitrary(ty, kani_any_def, ty_arbitrary_cache)
+        || can_derive_arbitrary(ty, kani_any_def, ty_arbitrary_cache)
+    {
+        return true;
+    }
+    if let Some((_, pointee)) = smart_pointer_model_instance(tcx, ty, smart_pointer_models) {
+        return implements_arbitrary(pointee, kani_any_def, ty_arbitrary_cache)
+            || can_derive_arbitrary(pointee, kani_any_def, ty_arbitrary_cache);
+    }
+    false
+}
+
 /// Is `ty` a struct or enum whose fields/variants implement Arbitrary, or a reference to such a
 /// type?
 fn can_derive_arbitrary(