Skip to content

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

Closed

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

Activity

  1. feliperodri commented on Aug 25, 2026

    @feliperodri
    MemberAuthor

    Surfaced by #4760 (the nightly-2026-06-01 upgrade), which converts the affected tests to pattern types and pins the reduced reach in tests/script-based-pre/autoharness_niche so it cannot regress further unnoticed.

  2. added this to the Autoharness milestone on Aug 26, 2026
  3. added 2 commits that reference this issue on Sep 3, 2026
    5d0f319
    db8ac88
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

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