Autoharness: constructor-based value generation (--constructor-args)

docs/src/reference/experimental/autoharness.md

@@ -98,6 +98,24 @@ To override the default:
 In parallel runs each harness result line is prefixed with the thread that produced it, and
 results arrive in nondeterministic order; the summary table printed at the end is always sorted.
 
+### Constructor-based generation (--constructor-args)
+
+By default, when a type does not implement `Arbitrary`, Kani synthesizes values field by field.
+For types whose private fields carry a representation invariant (e.g. a date type storing a
+packed, validated ordinal), raw field synthesis can produce values that violate the invariant,
+causing false alarms in every harness that generates the type. With `--constructor-args`, Kani
+instead generates values of private-field struct types by calling one of the type's public
+constructors with nondeterministic arguments, assuming success for constructors returning
+`Option<Self>` or `Result<Self, E>`. Constructors that are doc-hidden, unsafe, zero-argument,
+or generic are not considered.
+
+This option is opt-in because it under-approximates: harnesses whose values are generated this
+way are marked "(ctor)" in the output, and their verification results only cover values
+reachable through the chosen constructor; a bug that requires a different value will not be
+found. Note also that a constructor which itself panics for some of its inputs (rather than
+rejecting them via `Option`/`Result`) turns those inputs into harness failures, so this option
+can trade one class of false alarm for another.
+
 ## Example
 Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again:
 ```rust

kani-compiler/src/args.rs

@@ -122,6 +122,10 @@ pub struct Arguments {
     /// references). See kani_driver::autoharness_args for documentation.
     #[arg(long = "autoharness-bounded-arguments")]
     pub autoharness_bounded_arguments: bool,
+
+    /// Enable constructor-based nondeterministic value generation for autoharness.
+    #[arg(long = "autoharness-constructor-args")]
+    pub autoharness_constructor_args: bool,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]

kani-compiler/src/kani_middle/codegen_units.rs

@@ -373,13 +373,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, bool)>,
+    verifiable_fns: Vec<(Instance, AutoHarnessCaveats)>,
     kani_harness_intrinsic: FnDef,
     base_filename: &Path,
 ) -> HashMap<Harness, HarnessMetadata> {
     verifiable_fns
         .into_iter()
-        .map(|(fn_to_verify, is_bounded)| {
+        .map(|(fn_to_verify, caveats)| {
             // 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.
@@ -393,7 +393,8 @@ fn get_all_automatic_harnesses(
                 base_filename,
                 &fn_to_verify,
                 harness.mangled_name(),
-                is_bounded,
+                caveats.is_bounded,
+                caveats.is_ctor_based,
             );
             (harness, metadata)
         })
@@ -665,6 +666,16 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result<Insta
     ))
 }
 
+/// 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.
+#[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,
+}
+
 /// Partition every function in the crate into (chosen, skipped), where `chosen` is a vector of the Instances for which we'll generate automatic harnesses,
 /// and `skipped` is a map of function names to the reason why we skipped them.
 fn automatic_harness_partition(
@@ -674,7 +685,7 @@ fn automatic_harness_partition(
     kani_any_def: FnDef,
     kani_bounded_any_def: FnDef,
     smart_pointer_models: SmartPointerModels,
-) -> (Vec<(Instance, bool)>, BTreeMap<String, AutoHarnessSkipReason>) {
+) -> (Vec<(Instance, AutoHarnessCaveats)>, 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)
@@ -691,6 +702,9 @@ fn automatic_harness_partition(
 
     // Cache whether a type implements or can derive Arbitrary
     let mut ty_arbitrary_cache: FxHashMap<Ty, bool> = FxHashMap::default();
+    // The constructor search needs the same predicate, but `skip_reason` borrows the cache above
+    // for the whole loop, so give the `--constructor-args` check its own.
+    let mut ty_arbitrary_cache_ctor: FxHashMap<Ty, bool> = FxHashMap::default();
 
     // 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
@@ -831,7 +845,23 @@ fn automatic_harness_partition(
                 skipped
                     .insert(crate::kani_middle::strip_local_crate_prefix(instance.name()), reason);
             }
-            Ok(is_bounded) => chosen.push((instance, is_bounded)),
+            Ok(is_bounded) => {
+                // Whether any generated value will come from a type's public constructor
+                // rather than raw field synthesis, which the summary reports as "(ctor)".
+                let is_ctor_based = args.autoharness_constructor_args
+                    && instance.body().is_some_and(|body| {
+                        body.arg_locals().iter().any(|arg| {
+                            crate::kani_middle::uses_ctor_generation(
+                                tcx,
+                                arg.ty,
+                                kani_any_def,
+                                &mut ty_arbitrary_cache_ctor,
+                                &mut vec![],
+                            )
+                        })
+                    });
+                chosen.push((instance, AutoHarnessCaveats { is_bounded, is_ctor_based }));
+            }
         }
     }
 

kani-compiler/src/kani_middle/metadata.rs

@@ -43,6 +43,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
         has_loop_contracts: false,
         is_automatically_generated: false,
         is_bounded: false,
+        is_ctor_based: false,
     }
 }
 
@@ -123,6 +124,7 @@ pub fn gen_automatic_proof_metadata(
     fn_to_verify: &Instance,
     harness_mangled_name: String,
     is_bounded: bool,
+    is_ctor_based: bool,
 ) -> HarnessMetadata {
     let def = fn_to_verify.def;
     let pretty_name = readable_name(*fn_to_verify);
@@ -166,5 +168,6 @@ pub fn gen_automatic_proof_metadata(
         has_loop_contracts: false,
         is_automatically_generated: true,
         is_bounded,
+        is_ctor_based,
     }
 }

kani-compiler/src/kani_middle/mod.rs

@@ -325,6 +325,233 @@ fn implements_arbitrary(
     false
 }
 
+/// Whether generating a value of `ty` (under `--constructor-args`) would use constructor-based
+/// generation for some ADT reachable in `ty`'s type tree: an ADT with a private field and a
+/// viable public constructor. Used to mark such harnesses "(ctor)" in reports, since their
+/// verification results only cover constructor-reachable values.
+pub fn uses_ctor_generation(
+    tcx: TyCtxt,
+    ty: Ty,
+    kani_any_def: FnDef,
+    ty_arbitrary_cache: &mut FxHashMap<Ty, bool>,
+    visited: &mut Vec<Ty>,
+) -> bool {
+    if visited.contains(&ty) || visited.len() > 32 {
+        return false;
+    }
+    visited.push(ty);
+    match ty.kind() {
+        TyKind::RigidTy(RigidTy::Ref(_, inner, _)) | TyKind::RigidTy(RigidTy::RawPtr(inner, _)) => {
+            uses_ctor_generation(tcx, inner, kani_any_def, ty_arbitrary_cache, visited)
+        }
+        TyKind::RigidTy(RigidTy::Array(inner, _)) | TyKind::RigidTy(RigidTy::Slice(inner)) => {
+            uses_ctor_generation(tcx, inner, kani_any_def, ty_arbitrary_cache, visited)
+        }
+        TyKind::RigidTy(RigidTy::Tuple(elems)) => elems.iter().any(|elem| {
+            uses_ctor_generation(tcx, *elem, kani_any_def, ty_arbitrary_cache, visited)
+        }),
+        TyKind::RigidTy(RigidTy::Adt(def, args)) => {
+            // Hand-written Arbitrary implementations take precedence over ctor generation
+            // in the transform (it only rewrites unresolvable kani::any calls).
+            if implements_arbitrary_directly(ty, kani_any_def) {
+                return false;
+            }
+            // Deliberately the *same* predicate the generation path uses
+            // (`AutomaticArbitraryPass` calls `find_arbitrary_constructor`), so that the
+            // "(ctor)" marker and its under-approximation caveat cannot claim a constructor
+            // was used when generation actually fell back to raw field synthesis.
+            if def.kind() == AdtKind::Struct
+                && adt_has_private_field_check(tcx, def)
+                && find_arbitrary_constructor(tcx, ty, kani_any_def, ty_arbitrary_cache).is_some()
+            {
+                return true;
+            }
+            def.variants_iter().any(|variant| {
+                variant.fields().iter().any(|field| {
+                    uses_ctor_generation(
+                        tcx,
+                        field.ty_with_args(&args),
+                        kani_any_def,
+                        ty_arbitrary_cache,
+                        visited,
+                    )
+                })
+            }) || args.0.iter().any(|arg| match arg {
+                GenericArgKind::Type(t) => {
+                    uses_ctor_generation(tcx, *t, kani_any_def, ty_arbitrary_cache, visited)
+                }
+                _ => false,
+            })
+        }
+        _ => false,
+    }
+}
+
+/// Whether the ADT has at least one non-public field (in any variant).
+pub fn adt_has_private_field_check(tcx: TyCtxt, def: AdtDef) -> bool {
+    let did = rustc_internal::internal(tcx, def.def_id());
+    tcx.adt_def(did).all_fields().any(|field| !tcx.visibility(field.did).is_public())
+}
+
+/// Whether `ty` has a resolvable `<ty as Arbitrary>::any` (a hand-written or derived source
+/// implementation), without considering compiler-side derivation. Mirrors the resolvability
+/// test in `implements_arbitrary`: `kani::any::<T>` itself always resolves (it is a concrete
+/// generic function); what distinguishes a source implementation is whether the `T::any()`
+/// call in its body resolves.
+fn implements_arbitrary_directly(ty: Ty, kani_any_def: FnDef) -> bool {
+    let Ok(inst) = Instance::resolve(kani_any_def, &GenericArgs(vec![GenericArgKind::Type(ty)]))
+    else {
+        return false;
+    };
+    let Some(kani_any_body) = inst.body() else { return false };
+    for bb in kani_any_body.blocks.iter() {
+        let TerminatorKind::Call { func, .. } = &bb.terminator.kind else {
+            continue;
+        };
+        if let TyKind::RigidTy(RigidTy::FnDef(def, args)) =
+            func.ty(kani_any_body.arg_locals()).unwrap().kind()
+        {
+            return Instance::resolve(def, &args).is_ok();
+        }
+    }
+    false
+}
+
+/// The outcome of searching for a viable public constructor for a type without an Arbitrary
+/// implementation (`--constructor-args`): the constructor's instance, and how its return value
+/// wraps `Self` (directly, or inside `Option`/`Result`, in which case generated harnesses
+/// assume success).
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum CtorReturn {
+    Direct,
+    OptionOf,
+    ResultOf,
+}
+
+/// Search `ty`'s inherent impls for a public associated function usable as a constructor:
+/// one that returns `Self`, `Option<Self>` or `Result<Self, E>`, takes no `self` argument,
+/// has no remaining generic parameters of its own, and whose every argument implements (or
+/// can derive) Arbitrary. Prefer `Self` over `Option<Self>` over `Result<Self, E>` returns
+/// (fewer assumptions), and among equal shapes, prefer the constructor with the most
+/// arguments (heuristically the least-constrained coverage of the value space); ties are
+/// broken by definition order for determinism.
+pub fn find_arbitrary_constructor(
+    tcx: TyCtxt,
+    ty: Ty,
+    kani_any_def: FnDef,
+    ty_arbitrary_cache: &mut FxHashMap<Ty, bool>,
+) -> Option<(Instance, CtorReturn)> {
+    let TyKind::RigidTy(RigidTy::Adt(adt_def, ref adt_args)) = ty.kind() else {
+        return None;
+    };
+    let adt_did = rustc_internal::internal(tcx, adt_def.def_id());
+    let mut best: Option<(Instance, CtorReturn, usize)> = None;
+    for &impl_did in tcx.inherent_impls(adt_did) {
+        for &item in tcx.associated_item_def_ids(impl_did) {
+            if !tcx.def_kind(item).is_fn_like() || tcx.associated_item(item).is_method() {
+                continue;
+            }
+            if !tcx.visibility(item).is_public() {
+                continue;
+            }
+            // Exclude doc-hidden constructors: they are de-facto internal (commonly
+            // `_unchecked` variants exported for macro use that assert their preconditions
+            // instead of validating, e.g. time's `Date::__from_ordinal_date_unchecked`),
+            // and calling them with nondeterministic arguments manufactures false alarms
+            // in every harness that generates the type. Unsafe constructors are excluded
+            // for the same reason: their preconditions are the caller's obligation.
+            if tcx.is_doc_hidden(item) {
+                continue;
+            }
+            // The constructor may only use the ADT's own generic parameters (inherited via
+            // the impl); reject constructors introducing their own generics.
+            if tcx
+                .generics_of(item)
+                .own_params
+                .iter()
+                .any(|p| !matches!(p.kind, rustc_middle::ty::GenericParamDefKind::Lifetime))
+            {
+                continue;
+            }
+            let Some(ctor_def) = to_fn_def(tcx, item) else { continue };
+            // Instantiate the impl's generics with the ADT instantiation's arguments. For
+            // phase 1, only support non-generic ADTs (no substitution needed).
+            if !adt_args.0.is_empty() {
+                continue;
+            }
+            let fn_sig = ctor_def.fn_sig().skip_binder();
+            if fn_sig.safety == rustc_public::mir::Safety::Unsafe {
+                continue;
+            }
+            // Zero-argument constructors produce a single value, which destroys the coverage
+            // a nondeterministic harness is meant to provide, and is actively harmful for
+            // environment-reading constructors (e.g. Instant::now() reaches clock_gettime,
+            // which Kani does not support, failing every harness that generates the type).
+            if fn_sig.inputs().is_empty() {
+                continue;
+            }
+            let ret = fn_sig.output();
+            let shape = if ret == ty {
+                CtorReturn::Direct
+            } else if let TyKind::RigidTy(RigidTy::Adt(wrap_def, wrap_args)) = ret.kind() {
+                let name = wrap_def.name();
+                let payload = wrap_args.0.first().and_then(|a| match a {
+                    GenericArgKind::Type(t) => Some(*t),
+                    _ => None,
+                });
+                if payload != Some(ty) {
+                    continue;
+                } else if name == "core::option::Option" || name == "std::option::Option" {
+                    CtorReturn::OptionOf
+                } else if name == "core::result::Result" || name == "std::result::Result" {
+                    CtorReturn::ResultOf
+                } else {
+                    continue;
+                }
+            } else {
+                continue;
+            };
+            // Every constructor argument must be plainly generatable (implements or derives
+            // Arbitrary); constructor arguments do not get the argument-position extensions
+            // (slices, smart pointers, nested constructors) in phase 1.
+            if !fn_sig
+                .inputs()
+                .iter()
+                .all(|input| implements_arbitrary(*input, kani_any_def, ty_arbitrary_cache))
+            {
+                continue;
+            }
+            let Ok(instance) = Instance::resolve(ctor_def, &GenericArgs(vec![])) else {
+                continue;
+            };
+            if !instance.has_body() {
+                continue;
+            }
+            let n_args = fn_sig.inputs().len();
+            let better = match &best {
+                None => true,
+                Some((_, best_shape, best_n)) => {
+                    (shape as u8, std::cmp::Reverse(n_args))
+                        < (*best_shape as u8, std::cmp::Reverse(*best_n))
+                }
+            };
+            if better {
+                best = Some((instance, shape, n_args));
+            }
+        }
+    }
+    best.map(|(inst, shape, _)| (inst, shape))
+}
+
+/// Convert an internal DefId of a function-like item to a stable FnDef.
+fn to_fn_def(tcx: TyCtxt, def_id: rustc_span::def_id::DefId) -> Option<FnDef> {
+    let ty = rustc_internal::stable(tcx.type_of(def_id)).value;
+    match ty.kind() {
+        TyKind::RigidTy(RigidTy::FnDef(def, _)) => Some(def),
+        _ => None,
+    }
+}
+
 /// The niche constraint of a scalar-ABI type: the width of the scalar in bits, and the
 /// (possibly wrapping) inclusive range of valid bit patterns.
 /// Returns None for non-scalar ABIs, pointer/float scalars, and scalars whose valid range