Autoharness: mine constructor assertions into value filters

docs/src/reference/experimental/autoharness.md

@@ -104,17 +104,38 @@ By default, when a type does not implement `Arbitrary`, Kani synthesizes values
 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.
+instead generates values of private-field struct types through one of the type's own
+constructors, preferring (in order):
+
+1. An *assert-guarded representation constructor*: an `unsafe`, `#[doc(hidden)]`, or
+   `*_unchecked`-named associated function returning `Self` directly, whose preconditions are
+   stated as assertions (e.g. `debug_assert!`) rather than validated returns. Kani inlines its
+   body with nondeterministic arguments and converts every validity statement — `kani::assert`
+   and `assert_unchecked` calls, panic entry points, and overflow (`Assert`) checks — into an
+   assumption, so the constructor's own assertions filter the arguments down to the values the
+   crate considers valid. Calls the constructor makes to further assert-guarded helpers are
+   inlined recursively (bounded in depth and size). Visibility is irrelevant here, since the
+   body is inlined rather than called.
+2. Otherwise, a *checked public constructor*: a public associated function returning `Self`,
+   `Option<Self>`, or `Result<Self, E>`, called with nondeterministic arguments (assuming
+   success for the `Option<Self>`/`Result<Self, E>` shapes).
+
+Zero-argument constructors, and constructors generic over their own parameters, 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.
+found. Note also that a checked 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.
+
+> **Caveat:** if the chosen constructor is *unsatisfiable* for the generated type — an
+> assert-guarded constructor every argument of which trips an assertion, or a checked
+> constructor that always returns `None`/`Err` — the generated body assumes `false` on all
+> paths and the harness becomes **vacuous**, reporting `Success` without checking anything.
+> Kani does not yet detect this case; see
+> [#4757](https://github.com/model-checking/kani/issues/4757).
 
 ## Example
 Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again:

kani-compiler/src/kani_middle/mod.rs

@@ -357,12 +357,15 @@ pub fn uses_ctor_generation(
                 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.
+            // (`AutomaticArbitraryPass` tries `find_unchecked_constructor`, then
+            // `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()
+                && (find_unchecked_constructor(tcx, ty, kani_any_def, ty_arbitrary_cache).is_some()
+                    || find_arbitrary_constructor(tcx, ty, kani_any_def, ty_arbitrary_cache)
+                        .is_some())
             {
                 return true;
             }
@@ -428,6 +431,81 @@ pub enum CtorReturn {
     ResultOf,
 }
 
+/// Search `ty`'s inherent impls for an assert-guarded *representation constructor*: an
+/// associated function returning `Self` directly whose preconditions are stated as
+/// (debug_)asserts rather than validated returns — typically `unsafe`, doc-hidden or
+/// `_unchecked`-named builders exported for macro use (e.g. time's `Date::from_parts`).
+/// Under `--constructor-args`, such a constructor is inlined with panic paths converted to
+/// assumptions (c.f. `automatic::inline_with_assumed_panics`), so its own assertions filter
+/// the nondeterministic arguments down to exactly the values the crate considers valid.
+/// Visibility is irrelevant (the body is inlined, not called). Prefers more arguments over
+/// fewer; ties broken by definition order.
+pub fn find_unchecked_constructor(
+    tcx: TyCtxt,
+    ty: Ty,
+    kani_any_def: FnDef,
+    ty_arbitrary_cache: &mut FxHashMap<Ty, bool>,
+) -> Option<Instance> {
+    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, 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
+                .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 };
+            // For generic ADTs (e.g. deranged's RangedI32<MIN, MAX>), instantiate the
+            // constructor with the ADT's own generic arguments: for inherent impls whose
+            // parameters mirror the type's, this is the correct substitution; when it is
+            // not, resolution fails and the constructor is skipped.
+            let Ok(instance) = Instance::resolve(ctor_def, adt_args) else {
+                continue;
+            };
+            if !instance.has_body() {
+                continue;
+            }
+            let TyKind::RigidTy(RigidTy::FnDef(..)) = instance.ty().kind() else { continue };
+            let Some(binder) = instance.ty().kind().fn_sig() else { continue };
+            let fn_sig = binder.skip_binder();
+            if fn_sig.output() != ty {
+                continue;
+            }
+            // The unchecked-builder heuristic: unsafe, doc-hidden, or *_unchecked-named.
+            let name = tcx.item_name(item).to_string();
+            let is_unchecked = fn_sig.safety == rustc_public::mir::Safety::Unsafe
+                || tcx.is_doc_hidden(item)
+                || name.contains("unchecked");
+            if !is_unchecked {
+                continue;
+            }
+            if fn_sig.inputs().is_empty()
+                || !fn_sig
+                    .inputs()
+                    .iter()
+                    .all(|input| implements_arbitrary(*input, kani_any_def, ty_arbitrary_cache))
+            {
+                continue;
+            }
+            let n_args = fn_sig.inputs().len();
+            if best.as_ref().is_none_or(|(_, best_n)| n_args > *best_n) {
+                best = Some((instance, n_args));
+            }
+        }
+    }
+    best.map(|(inst, _)| inst)
+}
+
 /// 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