Skip to content

Autoharness: generate values for pattern-type fields, restoring layout-niche coverage for user-defined ranged types #4758

Description

@feliperodri

Context

#4716 added an assumption of a type's layout niche after each nondeterministically generated value, so that autoharness stops producing language-level-invalid values for ranged scalar types (e.g. a date type packing a validated ordinal) and stops reporting the resulting false alarms.

The toolchain upgrade to nightly-2026-06-01 (#4757) removed rustc_layout_scalar_valid_range_start/_end in favour of pattern types — the same move core::num::niche_types made upstream. A ranged scalar newtype is now written as:

#[repr(transparent)]
pub struct Month(std::pat::pattern_type!(u8 is 1..=12));

Problem

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. Every locally-defined ranged newtype is therefore skipped rather than harnessed:

| 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   |

So the niche assumption, which is the thing #4716 added, no longer applies to the user-defined types it was aimed at. It still works end to end for std::time::Duration, whose Nanoseconds field carries the same kind of range and which does get harnessed — that is the motivating real-world case from the #3832 triage, so the feature is not dead, just much narrower than intended.

tests/script-based-pre/autoharness_niche pins both halves (the working Duration/NonZeroU8 cases and the skipped local ones) so this limitation is asserted by a test rather than silently regressing further.

Proposed fix

Teach autoharness to generate values for pattern-type fields. The pieces already exist:

  • scalar_niche (added in Autoharness: assume layout niches of generated scalar values #4716, kani-compiler/src/kani_middle/mod.rs) already computes the (bits, start, end) valid range from the layout, and a pattern type's layout carries exactly that restricted range.
  • call_kani_any_for_ty already knows how to generate a base integer and how to emit kani::assume for a niche.

So generating a pattern_type!(u8 is 1..=12) is: generate the base integer with kani::any, assume scalar_niche's range, and transmute. Concretely that means:

  1. can_derive_arbitrary accepting RigidTy::Pat whose base type is generatable.
  2. call_kani_any_for_ty gaining a RigidTy::Pat arm that generates the base type and applies assume_scalar_niche to the result.

Both are sound in the same sense #4716 argued: the assumed range is a necessary condition of the pattern type's validity, so no valid value is excluded.

Acceptance

tests/script-based-pre/autoharness_niche should move its local ranged types (Month, Schedule, PosI8, and check_monthly::<Month>) out of the skipped table and back into the verified table, with the cover checks still confirming the range extremes remain reachable (i.e. no over-constraining).

Metadata

Metadata

Assignees

No one assigned

    Labels

    Z-AutoharnessIssue related to autoharness subcommand[C] Feature / EnhancementA new feature request or enhancement to an existing feature.

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions