From db8ac8857ef02477ab530ec44800833590ccb571 Mon Sep 17 00:00:00 2001 From: Tianshu Huang Date: Thu, 3 Sep 2026 15:59:20 -0700 Subject: [PATCH 1/4] Autoharness: support pattern types (RigidTy::Pat) Teach autoharness to recognize and generate values for pattern types, since nightly-2026-04-01. Without this, any function taking a NonNull argument (or a struct containing one) is skipped with 'Missing Arbitrary'. Resolves #4758 --- kani-compiler/src/kani_middle/mod.rs | 23 ++++++++++++++++ .../src/kani_middle/transform/automatic.rs | 16 +++++++++++ .../autoharness_niche/expected | 14 ++++++---- .../autoharness_niche/niche_probe.rs | 10 ++----- .../autoharness_pattern_type/config.yml | 4 +++ .../autoharness_pattern_type/expected | 5 ++++ .../pattern_type_probe.rs | 27 +++++++++++++++++++ .../autoharness_pattern_type/run.sh | 8 ++++++ 8 files changed, 94 insertions(+), 13 deletions(-) create mode 100644 tests/script-based-pre/autoharness_pattern_type/config.yml create mode 100644 tests/script-based-pre/autoharness_pattern_type/expected create mode 100644 tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs create mode 100755 tests/script-based-pre/autoharness_pattern_type/run.sh diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index f3376274697..12fcef2a769 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -1073,6 +1073,23 @@ 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`. +/// For raw-pointer bases (`*const T` / `*mut T`), the pointee `T` must itself be +/// generatable because the raw-pointer codegen allocates storage for it. For any other +/// base (integers, booleans, etc.) the base itself must implement or derive Arbitrary. +fn pat_base_is_derivable( + base_ty: Ty, + kani_any_def: FnDef, + ty_arbitrary_cache: &mut FxHashMap, +) -> bool { + let ty_to_check = match base_ty.kind() { + TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) => pointee_ty, + _ => base_ty, + }; + implements_arbitrary(ty_to_check, kani_any_def, ty_arbitrary_cache) + || can_derive_arbitrary(ty_to_check, 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 +1120,10 @@ 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 +1156,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 } diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 3b730ba83d2..157b6ad7d8d 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -1378,6 +1378,22 @@ 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!(*const T is !null)`) is layout-compatible with its + // base type. Generate an arbitrary value of the base type, transmute it to the pattern + // type, then constrain it to the pattern's validity range via `assume_scalar_niche`. + let base_lcl = call_kani_any_for_ty( + tcx, models, body, base_ty, mutability, source, invariant_cache, mined_cache, + ); + 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, + ); + assume_scalar_niche(tcx, models.kani_assume, body, source, pat_lcl, ty); + 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) diff --git a/tests/script-based-pre/autoharness_niche/expected b/tests/script-based-pre/autoharness_niche/expected index b7a2c61c5d3..64548011f53 100644 --- a/tests/script-based-pre/autoharness_niche/expected +++ b/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:: | #[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. diff --git a/tests/script-based-pre/autoharness_niche/niche_probe.rs b/tests/script-based-pre/autoharness_niche/niche_probe.rs index a1275cf6b03..e8df21072eb 100644 --- a/tests/script-based-pre/autoharness_niche/niche_probe.rs +++ b/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)] diff --git a/tests/script-based-pre/autoharness_pattern_type/config.yml b/tests/script-based-pre/autoharness_pattern_type/config.yml new file mode 100644 index 00000000000..ce281b64090 --- /dev/null +++ b/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 diff --git a/tests/script-based-pre/autoharness_pattern_type/expected b/tests/script-based-pre/autoharness_pattern_type/expected new file mode 100644 index 00000000000..317ac4e763d --- /dev/null +++ b/tests/script-based-pre/autoharness_pattern_type/expected @@ -0,0 +1,5 @@ +Status: SATISFIED +| pattern_type_probe | nonnull_as_ptr | #[kani::proof] | Success | +| pattern_type_probe | nonnull_is_not_null | #[kani::proof] | Success | +| pattern_type_probe | wrapper_get_ptr | #[kani::proof] | Success | +Complete - 3 successfully verified functions, 0 failures, 3 total. diff --git a/tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs b/tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs new file mode 100644 index 00000000000..72cf1db1e96 --- /dev/null +++ b/tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// `NonNull` wraps a `pattern_type!(*const T is !null)` (since nightly-2026-04-01). +// Autoharness must be able to derive Arbitrary for this pattern type so that +// functions taking NonNull arguments can be verified. +use std::ptr::NonNull; + +// Top-level NonNull argument: the generated value must be non-null. +pub fn nonnull_as_ptr(p: NonNull) -> *mut u8 { + p.as_ptr() +} + +// NonNull inside a struct: the pattern type appears as an ADT field. +pub struct Wrapper { + inner: NonNull, + tag: u8, +} + +pub fn wrapper_get_ptr(w: Wrapper) -> *mut u32 { + w.inner.as_ptr() +} + +// Cover check: the generated NonNull must actually be non-null. +pub fn nonnull_is_not_null(p: NonNull) { + kani::cover!(p.as_ptr() as usize != 0, "non-null pointer"); +} diff --git a/tests/script-based-pre/autoharness_pattern_type/run.sh b/tests/script-based-pre/autoharness_pattern_type/run.sh new file mode 100755 index 00000000000..4e898a2494d --- /dev/null +++ b/tests/script-based-pre/autoharness_pattern_type/run.sh @@ -0,0 +1,8 @@ +#!/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!(*const T is !null)` for NonNull). Autoharness must recognize +# them as derivable and constrain generated values to the pattern's valid range. +kani autoharness -Z autoharness --output-format=regular pattern_type_probe.rs From 60a17ccfea09f616ec0abe739f853244a110802d Mon Sep 17 00:00:00 2001 From: Tianshu Huang Date: Mon, 7 Sep 2026 20:40:40 -0700 Subject: [PATCH 2/4] fix rustfmt formatting --- kani-compiler/src/kani_middle/mod.rs | 5 ++--- kani-compiler/src/kani_middle/transform/automatic.rs | 9 ++++++++- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 12fcef2a769..2c63a08f1c0 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -1121,9 +1121,8 @@ fn can_derive_arbitrary( // 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, - ); + 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); diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 157b6ad7d8d..3d469024af0 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -1383,7 +1383,14 @@ fn call_kani_any_for_ty( // base type. Generate an arbitrary value of the base type, transmute it to the pattern // type, then constrain it to the pattern's validity range via `assume_scalar_niche`. let base_lcl = call_kani_any_for_ty( - tcx, models, body, base_ty, mutability, source, invariant_cache, mined_cache, + tcx, + models, + body, + base_ty, + mutability, + source, + invariant_cache, + mined_cache, ); let pat_lcl = body.new_local(ty, source.span(body.blocks()), mutability); body.assign_to( From e54cefefe1ebbdd112702f0cea9908a5dcbe8625 Mon Sep 17 00:00:00 2001 From: Tianshu Huang Date: Tue, 8 Sep 2026 16:16:33 -0700 Subject: [PATCH 3/4] Fix scalar_niche for pointer pattern types; add assert for NonNull --- kani-compiler/src/kani_middle/mod.rs | 7 +++++-- .../autoharness_pattern_type/pattern_type_probe.rs | 4 +++- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 2c63a08f1c0..65e2cbb438d 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -817,8 +817,11 @@ pub fn scalar_niche(tcx: TyCtxt, ty: Ty) -> Option { .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; diff --git a/tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs b/tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs index 72cf1db1e96..50e20f15524 100644 --- a/tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs +++ b/tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs @@ -21,7 +21,9 @@ pub fn wrapper_get_ptr(w: Wrapper) -> *mut u32 { w.inner.as_ptr() } -// Cover check: the generated NonNull must actually be non-null. +// The generated NonNull must actually be non-null: assert proves null is never +// generated, cover proves a non-null value is reachable. pub fn nonnull_is_not_null(p: NonNull) { + kani::assert(p.as_ptr() as usize != 0, "generated pointer must be non-null"); kani::cover!(p.as_ptr() as usize != 0, "non-null pointer"); } From 52a97d84e6ee3f21ccabd0d50aee26a14ccc50a1 Mon Sep 17 00:00:00 2001 From: Tianshu Huang Date: Fri, 18 Sep 2026 00:27:19 -0700 Subject: [PATCH 4/4] Reject raw-pointer pattern bases; assume niche before transmute; test integer patterns --- kani-compiler/src/kani_middle/mod.rs | 27 ++++++------ .../src/kani_middle/transform/automatic.rs | 10 +++-- .../autoharness_pattern_type/expected | 7 ++- .../pattern_type_probe.rs | 43 +++++++++++-------- .../autoharness_pattern_type/run.sh | 8 ++-- 5 files changed, 53 insertions(+), 42 deletions(-) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 65e2cbb438d..8cf12dc6abd 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -793,8 +793,9 @@ pub fn scalar_width_bits(tcx: TyCtxt, ty: Ty) -> Option { /// 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`'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 @@ -1076,21 +1077,23 @@ 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`. -/// For raw-pointer bases (`*const T` / `*mut T`), the pointee `T` must itself be -/// generatable because the raw-pointer codegen allocates storage for it. For any other -/// base (integers, booleans, etc.) the base itself must implement or derive Arbitrary. +/// 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`'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, ) -> bool { - let ty_to_check = match base_ty.kind() { - TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) => pointee_ty, - _ => base_ty, - }; - implements_arbitrary(ty_to_check, kani_any_def, ty_arbitrary_cache) - || can_derive_arbitrary(ty_to_check, kani_any_def, ty_arbitrary_cache) + 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 diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 3d469024af0..5b0c92b00a1 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -1379,9 +1379,11 @@ fn call_kani_any_for_ty( ptr_lcl } } else if let TyKind::RigidTy(RigidTy::Pat(base_ty, _)) = ty.kind() { - // A pattern type (e.g. `pattern_type!(*const T is !null)`) is layout-compatible with its - // base type. Generate an arbitrary value of the base type, transmute it to the pattern - // type, then constrain it to the pattern's validity range via `assume_scalar_niche`. + // 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, @@ -1392,6 +1394,7 @@ fn call_kani_any_for_ty( 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), @@ -1399,7 +1402,6 @@ fn call_kani_any_for_ty( source, InsertPosition::Before, ); - assume_scalar_niche(tcx, models.kani_assume, body, source, pat_lcl, ty); pat_lcl } else { // Prefer an unbounded nondeterministic value via (implemented or compiler-derived) diff --git a/tests/script-based-pre/autoharness_pattern_type/expected b/tests/script-based-pre/autoharness_pattern_type/expected index 317ac4e763d..baefd956930 100644 --- a/tests/script-based-pre/autoharness_pattern_type/expected +++ b/tests/script-based-pre/autoharness_pattern_type/expected @@ -1,5 +1,4 @@ Status: SATISFIED -| pattern_type_probe | nonnull_as_ptr | #[kani::proof] | Success | -| pattern_type_probe | nonnull_is_not_null | #[kani::proof] | Success | -| pattern_type_probe | wrapper_get_ptr | #[kani::proof] | Success | -Complete - 3 successfully verified functions, 0 failures, 3 total. +| 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. diff --git a/tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs b/tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs index 50e20f15524..f620a333c62 100644 --- a/tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs +++ b/tests/script-based-pre/autoharness_pattern_type/pattern_type_probe.rs @@ -1,29 +1,34 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// `NonNull` wraps a `pattern_type!(*const T is !null)` (since nightly-2026-04-01). -// Autoharness must be able to derive Arbitrary for this pattern type so that -// functions taking NonNull arguments can be verified. -use std::ptr::NonNull; +// 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; -// Top-level NonNull argument: the generated value must be non-null. -pub fn nonnull_as_ptr(p: NonNull) -> *mut u8 { - p.as_ptr() -} - -// NonNull inside a struct: the pattern type appears as an ADT field. -pub struct Wrapper { - inner: NonNull, +pub struct Percent { + value: pattern_type!(u8 is 0..=100), tag: u8, } -pub fn wrapper_get_ptr(w: Wrapper) -> *mut u32 { - w.inner.as_ptr() +// 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"); } -// The generated NonNull must actually be non-null: assert proves null is never -// generated, cover proves a non-null value is reachable. -pub fn nonnull_is_not_null(p: NonNull) { - kani::assert(p.as_ptr() as usize != 0, "generated pointer must be non-null"); - kani::cover!(p.as_ptr() as usize != 0, "non-null pointer"); +// 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"); } diff --git a/tests/script-based-pre/autoharness_pattern_type/run.sh b/tests/script-based-pre/autoharness_pattern_type/run.sh index 4e898a2494d..bb29223444d 100755 --- a/tests/script-based-pre/autoharness_pattern_type/run.sh +++ b/tests/script-based-pre/autoharness_pattern_type/run.sh @@ -3,6 +3,8 @@ # 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!(*const T is !null)` for NonNull). Autoharness must recognize -# them as derivable and constrain generated values to the pattern's valid range. -kani autoharness -Z autoharness --output-format=regular pattern_type_probe.rs +# (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