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