Autoharness: support pattern types (RigidTy::Pat)

kani-compiler/src/kani_middle/mod.rs

@@ -793,8 +793,9 @@ pub fn scalar_width_bits(tcx: TyCtxt, ty: Ty) -> Option<u64> {
 
 /// 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
-/// covers every bit pattern.
+/// Returns None for non-scalar ABIs, float scalars, and scalars whose valid range covers every
+/// bit pattern. Pointer scalars are supported (their width is the target's pointer size), which
+/// is what lets `!null` pattern types such as `NonNull<T>`'s field report their niche.
 ///
 /// Rationale: a layout niche is a language-level validity invariant (rustc packs enum
 /// variants into the invalid patterns), so a synthesized `kani::any` body must not produce
@@ -817,8 +818,11 @@ pub fn scalar_niche(tcx: TyCtxt, ty: Ty) -> Option<ScalarNiche> {
         .ok()?;
     let BackendRepr::Scalar(scalar) = layout.backend_repr else { return None };
     let Scalar::Initialized { value, valid_range } = scalar else { return None };
-    let Primitive::Int(int, _signed) = value else { return None };
-    let bits = int.size().bits();
+    let bits = match value {
+        Primitive::Int(int, _) => int.size().bits(),
+        Primitive::Pointer(_) => tcx.data_layout.pointer_size().bits(),
+        Primitive::Float(_) => return None,
+    };
     let full = if bits == 128 { u128::MAX } else { (1u128 << bits) - 1 };
     if valid_range.start == 0 && valid_range.end == full {
         return None;
@@ -1073,6 +1077,25 @@ fn fmt_impl_self_ty(tcx: TyCtxt, instance: Instance) -> Option<(FmtTrait, Ty)> {
     Some((fmt_trait, self_ty))
 }
 
+/// Whether a pattern type's base can be generated by `call_kani_any_for_ty`: the base
+/// (an integer, bool, etc.) must implement or derive Arbitrary.
+///
+/// Raw-pointer bases (`*const T is !null`, as in `NonNull<T>`'s field) are not supported: the
+/// pointee storage the raw-pointer codegen allocates is a local of whatever body generates the
+/// value, and for a struct field that is a synthesized `any()` body -- the pointer would dangle
+/// once it returns (the same reason reference fields are rejected in `can_derive_arbitrary`).
+fn pat_base_is_derivable(
+    base_ty: Ty,
+    kani_any_def: FnDef,
+    ty_arbitrary_cache: &mut FxHashMap<Ty, bool>,
+) -> bool {
+    if matches!(base_ty.kind(), TyKind::RigidTy(RigidTy::RawPtr(..))) {
+        return false;
+    }
+    implements_arbitrary(base_ty, kani_any_def, ty_arbitrary_cache)
+        || can_derive_arbitrary(base_ty, kani_any_def, ty_arbitrary_cache)
+}
+
 /// Is `ty` a struct or enum whose fields/variants implement Arbitrary, or a reference to such a
 /// type?
 fn can_derive_arbitrary(
@@ -1103,6 +1126,9 @@ fn can_derive_arbitrary(
                     // Note that this differs from *top-level argument* references, for which
                     // the harness itself owns the storage.
                     fields_impl_arbitrary = false;
+                } else if let TyKind::RigidTy(RigidTy::Pat(base_ty, _)) = ty.kind() {
+                    fields_impl_arbitrary &=
+                        pat_base_is_derivable(base_ty, kani_any_def, ty_arbitrary_cache);
                 } else {
                     fields_impl_arbitrary &=
                         implements_arbitrary(ty, kani_any_def, ty_arbitrary_cache);
@@ -1135,6 +1161,8 @@ fn can_derive_arbitrary(
         }
     } else if let TyKind::RigidTy(RigidTy::Ref(_, inner_ty, _)) = ty.kind() {
         can_derive_arbitrary(inner_ty, kani_any_def, ty_arbitrary_cache)
+    } else if let TyKind::RigidTy(RigidTy::Pat(base_ty, _)) = ty.kind() {
+        pat_base_is_derivable(base_ty, kani_any_def, ty_arbitrary_cache)
     } else {
         false
     }

kani-compiler/src/kani_middle/transform/automatic.rs

@@ -1362,6 +1362,31 @@ fn call_kani_any_for_ty(
         } else {
             ptr_lcl
         }
+    } else if let TyKind::RigidTy(RigidTy::Pat(base_ty, _)) = ty.kind() {
+        // A pattern type (e.g. `pattern_type!(u8 is 1..=12)`) is layout-compatible with its base
+        // type. Generate an arbitrary value of the base type, constrain it to the pattern's
+        // validity range via `assume_scalar_niche`, then transmute it to the pattern type. The
+        // assumption must come first: with `-Z valid-value-checks` the transmute itself is
+        // checked, so the value has to be valid before the pattern-typed local ever exists.
+        let base_lcl = call_kani_any_for_ty(
+            tcx,
+            models,
+            body,
+            base_ty,
+            mutability,
+            source,
+            invariant_cache,
+            mined_cache,
+        );
+        assume_scalar_niche(tcx, models.kani_assume, body, source, base_lcl, ty);
+        let pat_lcl = body.new_local(ty, source.span(body.blocks()), mutability);
+        body.assign_to(
+            Place::from(pat_lcl),
+            Rvalue::Cast(CastKind::Transmute, Operand::Move(Place::from(base_lcl)), ty),
+            source,
+            InsertPosition::Before,
+        );
+        pat_lcl
     } else {
         // Prefer an unbounded nondeterministic value via (implemented or compiler-derived)
         // Arbitrary; fall back to a smart-pointer model (`Box`/`Rc`/`Arc` of a derivable pointee)

tests/script-based-pre/autoharness_niche/expected

@@ -1,5 +1,9 @@
-| niche_probe | days_left_in_year                   | Missing Arbitrary implementation for argument(s) s: Schedule  |
-| niche_probe | signed_niche                        | Missing Arbitrary implementation for argument(s) p: PosI8     |
-| niche_probe | duration_nanos    | #[kani::proof]            | Success             |
-| niche_probe | nonzero           | #[kani::proof]            | Success             |
-Complete - 2 successfully verified functions, 0 failures, 2 total.
+Status: SATISFIED
+Status: SATISFIED
+| niche_probe | check_monthly::<Month>              | #[kani::proof]            | Success             |
+| niche_probe | cover_extremes                      | #[kani::proof]            | Success             |
+| niche_probe | days_left_in_year                   | #[kani::proof]            | Success             |
+| niche_probe | duration_nanos                      | #[kani::proof]            | Success             |
+| niche_probe | nonzero                             | #[kani::proof]            | Success             |
+| niche_probe | signed_niche                        | #[kani::proof]            | Success             |
+Complete - 10 successfully verified functions, 0 failures, 10 total.

tests/script-based-pre/autoharness_niche/niche_probe.rs

@@ -2,14 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // Ranged scalar newtypes are expressed with pattern types since nightly-2026-06-01 removed
 // `rustc_layout_scalar_valid_range_start`/`_end`; `core::num::niche_types` made the same move.
-//
-// Note the consequence for autoharness: a pattern type is not an ADT and has no `Arbitrary`
-// implementation, so `can_derive_arbitrary` cannot synthesize a struct that has one as a field.
-// The locally-defined ranged types below are therefore *skipped* rather than harnessed, which the
-// expected output pins. The niche assumption itself is still exercised end to end through
-// `std::time::Duration`, whose `Nanoseconds` field carries the same kind of range. Teaching
-// autoharness to generate pattern-type fields (generate the base integer, assume the layout
-// niche that `scalar_niche` already computes) would restore the wider reach.
+// Autoharness generates values for pattern-type fields by producing the base integer, assuming
+// the layout niche that `scalar_niche` computes, and transmuting to the pattern type.
 #![feature(pattern_types)]
 #![feature(pattern_type_macro)]
 

tests/script-based-pre/autoharness_pattern_type/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: run.sh
+expected: expected

tests/script-based-pre/autoharness_pattern_type/expected

@@ -0,0 +1,4 @@
+Status: SATISFIED
+| pattern_type_probe | nonzero_arg       | #[kani::proof]            | Success             |
+| pattern_type_probe | percent_in_range  | #[kani::proof]            | Success             |
+Complete - 2 successfully verified functions, 0 failures, 2 total.

tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs

@@ -0,0 +1,34 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Pattern types (`RigidTy::Pat`) wrap a base type with a validity constraint, e.g.
+// `pattern_type!(u8 is 0..=100)`. std builds its niche types on them (`NonZero`'s inner
+// type, `Duration`'s nanoseconds, wtf8 code points, ...). Autoharness must derive
+// Arbitrary for integer-based pattern types -- both as struct fields and as top-level
+// arguments -- and constrain the generated values to the pattern's range.
+#![feature(pattern_types, pattern_type_macro)]
+#![allow(internal_features)]
+use std::pat::pattern_type;
+
+pub struct Percent {
+    value: pattern_type!(u8 is 0..=100),
+    tag: u8,
+}
+
+// Field position: `Percent` is derived through a synthesized `any()`. The generated
+// value must respect the range (assert) and both bounds must be reachable (cover).
+pub fn percent_in_range(p: Percent) {
+    // SAFETY: a pattern type is layout-compatible with its base type.
+    let v: u8 = unsafe { std::mem::transmute(p.value) };
+    kani::assert(v <= 100, "generated value must be within the pattern's range");
+    kani::cover!(v == 0 && p.tag == 0, "lower bound reachable");
+    kani::cover!(v == 100, "upper bound reachable");
+}
+
+// Top-level argument position.
+pub fn nonzero_arg(x: pattern_type!(u8 is 1..)) {
+    // SAFETY: as above.
+    let v: u8 = unsafe { std::mem::transmute(x) };
+    kani::assert(v != 0, "generated value must be within the pattern's range");
+    kani::cover!(v == 255, "upper bound reachable");
+}

tests/script-based-pre/autoharness_pattern_type/run.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Pattern types (`RigidTy::Pat`) wrap a base scalar type with a validity constraint
+# (e.g. `pattern_type!(u8 is 0..=100)`; std's niche types are built on them). Autoharness
+# must recognize them as derivable and constrain generated values to the pattern's range.
+# `-Z valid-value-checks` verifies the range is assumed *before* the value is transmuted to
+# the pattern type (the transmute itself is validity-checked under that flag).
+kani autoharness -Z autoharness -Z valid-value-checks --output-format=regular pattern_type_probe.rs