Autoharness: assume layout niches of generated scalar values

kani-compiler/src/kani_middle/mod.rs

@@ -323,6 +323,49 @@ fn implements_arbitrary(
     false
 }
 
+/// 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.
+///
+/// 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
+/// values outside it -- they are as invalid as a `bool` holding 3. Assuming the range is
+/// therefore sound by construction and requires no reporting caveat.
+pub struct ScalarNiche {
+    /// Width of the scalar in bits (8, 16, 32, 64 or 128).
+    pub bits: u64,
+    /// Inclusive start of the valid range (bit pattern).
+    pub start: u128,
+    /// Inclusive end of the valid range (bit pattern). If `end < start`, the range wraps.
+    pub end: u128,
+}
+
+pub fn scalar_niche(tcx: TyCtxt, ty: Ty) -> Option<ScalarNiche> {
+    use rustc_abi::{BackendRepr, Primitive, Scalar};
+    let internal_ty = rustc_internal::internal(tcx, ty);
+    let layout = tcx
+        .layout_of(rustc_middle::ty::TypingEnv::fully_monomorphized().as_query_input(internal_ty))
+        .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 full = if bits == 128 { u128::MAX } else { (1u128 << bits) - 1 };
+    if valid_range.start == 0 && valid_range.end == full {
+        return None;
+    }
+    // A `Transmute` to the width-matched uint is only well-formed if the type occupies exactly
+    // the scalar's bytes. rustc is not known to report a `Scalar` ABI with padding, but bail out
+    // rather than emit an ill-sized cast: losing the constraint can only cause a (visible) false
+    // alarm, whereas comparing the wrong bits could assume `false` and silently make the harness
+    // vacuous.
+    if layout.size.bits() != bits {
+        return None;
+    }
+    Some(ScalarNiche { bits, start: valid_range.start, end: valid_range.end })
+}
+
 /// Inspect an `assume_safe::<T>()` (c.f. `KaniModel::AssumeSafe`) instantiation to determine if
 /// `T: Invariant`. The model looks like:
 /// ```rust

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

@@ -14,20 +14,21 @@ use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceIns
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_middle::{
     FmtTrait, SmartPointerModels, can_derive_arbitrary, fmt_impl_self_ty, implements_arbitrary,
-    implements_invariant, smart_pointer_model_instance,
+    implements_invariant, scalar_niche, smart_pointer_model_instance,
 };
 use crate::kani_queries::QueryDb;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::ty::TyCtxt;
 use rustc_public::CrateDef;
 use rustc_public::mir::mono::Instance;
 use rustc_public::mir::{
-    AggregateKind, BasicBlockIdx, Body, BorrowKind, CastKind, Local, MutBorrowKind, Mutability,
-    Operand, Place, ProjectionElem, Rvalue, SwitchTargets, Terminator, TerminatorKind,
+    AggregateKind, BasicBlockIdx, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local,
+    MutBorrowKind, Mutability, Operand, Place, ProjectionElem, Rvalue, SwitchTargets, Terminator,
+    TerminatorKind,
 };
 use rustc_public::ty::{
-    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, Region, RegionKind, RigidTy, Ty, TyConst,
-    TyKind, UintTy, VariantDef, VariantIdx,
+    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, MirConst, Region, RegionKind, RigidTy, Ty,
+    TyConst, TyKind, UintTy, VariantDef, VariantIdx,
 };
 use rustc_public_bridge::IndexedVal;
 use tracing::debug;
@@ -45,6 +46,8 @@ struct AnyModels {
     kani_any_slice_ref: FnDef,
     /// The FnDef of KaniModel::AnyStrRef
     kani_any_str_ref: FnDef,
+    /// The FnDef of KaniHook::Assume (used for layout-niche assumptions).
+    kani_assume: FnDef,
     /// The FnDef of KaniModel::AssumeSafe
     kani_assume_safe: FnDef,
     /// The FnDef of KaniModel::BoundedAny
@@ -61,6 +64,7 @@ impl AnyModels {
             kani_any_ptr: *kani_fns.get(&KaniModel::AnyPtr.into()).unwrap(),
             kani_any_slice_ref: *kani_fns.get(&KaniModel::AnySliceRef.into()).unwrap(),
             kani_any_str_ref: *kani_fns.get(&KaniModel::AnyStrRef.into()).unwrap(),
+            kani_assume: *kani_fns.get(&KaniHook::Assume.into()).unwrap(),
             kani_assume_safe: *kani_fns.get(&KaniModel::AssumeSafe.into()).unwrap(),
             kani_bounded_any: *kani_fns.get(&KaniModel::BoundedAny.into()).unwrap(),
             smart_pointer_models: SmartPointerModels::from_kani_functions(kani_fns),
@@ -211,6 +215,93 @@ const AUTOHARNESS_BOUNDED_ANY_BOUND: u64 = 4;
 /// Panics if `ty` does not implement Arbitrary or BoundedArbitrary and is not a supported smart
 /// pointer (and is not a reference or raw pointer to such a type, or a reference to a slice or str
 /// of such a type).
+/// If `ty` has a scalar layout with a restricted valid range (a layout niche), emit
+/// `kani::assume(<raw bits of the value in place_local> in valid_range)`.
+///
+/// Values outside the niche are language-level invalid -- rustc packs enum variants into the
+/// invalid bit patterns, so such a value is as invalid as a `bool` holding 3. Nondeterministic
+/// value generation must therefore never produce them: e.g. std's `NonZero` niches, or
+/// `core::time::Duration`'s `Nanoseconds` field (`rustc_layout_scalar_valid_range` types),
+/// whose compiler-derived generation would otherwise produce invalid values and raise false
+/// alarms in every harness generating the type.
+///
+/// The assumption is sound by construction -- it assumes a *necessary* condition of
+/// language-level validity, so every valid value stays in the explored set -- and therefore
+/// needs no flag or reporting caveat.
+fn assume_scalar_niche(
+    tcx: TyCtxt,
+    kani_assume: FnDef,
+    body: &mut MutableBody,
+    source: &mut SourceInstruction,
+    place_local: Local,
+    ty: Ty,
+) {
+    let Some(niche) = scalar_niche(tcx, ty) else { return };
+    let span = source.span(body.blocks());
+    let uint_ty = match niche.bits {
+        8 => UintTy::U8,
+        16 => UintTy::U16,
+        32 => UintTy::U32,
+        64 => UintTy::U64,
+        128 => UintTy::U128,
+        _ => return,
+    };
+    let raw_ty = Ty::from_rigid_kind(RigidTy::Uint(uint_ty));
+    // let raw: uN = transmute(value);
+    let raw_lcl = body.new_local(raw_ty, span, Mutability::Not);
+    body.assign_to(
+        Place::from(raw_lcl),
+        Rvalue::Cast(CastKind::Transmute, Operand::Copy(Place::from(place_local)), raw_ty),
+        source,
+        InsertPosition::Before,
+    );
+    let uint_const = |v: u128| {
+        Operand::Constant(ConstOperand {
+            span,
+            user_ty: None,
+            const_: MirConst::try_from_uint(v, uint_ty).unwrap(),
+        })
+    };
+    let bool_ty = Ty::bool_ty();
+    let ge_lcl = body.new_local(bool_ty, span, Mutability::Not);
+    body.assign_to(
+        Place::from(ge_lcl),
+        Rvalue::BinaryOp(BinOp::Ge, Operand::Copy(Place::from(raw_lcl)), uint_const(niche.start)),
+        source,
+        InsertPosition::Before,
+    );
+    let le_lcl = body.new_local(bool_ty, span, Mutability::Not);
+    body.assign_to(
+        Place::from(le_lcl),
+        Rvalue::BinaryOp(BinOp::Le, Operand::Copy(Place::from(raw_lcl)), uint_const(niche.end)),
+        source,
+        InsertPosition::Before,
+    );
+    // Contiguous range (start <= end): raw >= start && raw <= end.
+    // Wrapping range (end < start, e.g. NonZero's 1..=0): raw >= start || raw <= end.
+    let combine = if niche.start <= niche.end { BinOp::BitAnd } else { BinOp::BitOr };
+    let cond_lcl = body.new_local(bool_ty, span, Mutability::Not);
+    body.assign_to(
+        Place::from(cond_lcl),
+        Rvalue::BinaryOp(
+            combine,
+            Operand::Move(Place::from(ge_lcl)),
+            Operand::Move(Place::from(le_lcl)),
+        ),
+        source,
+        InsertPosition::Before,
+    );
+    let assume_inst = Instance::resolve(kani_assume, &GenericArgs(vec![])).unwrap();
+    let unit_lcl = body.new_local(Ty::new_tuple(&[]), span, Mutability::Not);
+    body.insert_call(
+        &assume_inst,
+        source,
+        InsertPosition::Before,
+        vec![Operand::Move(Place::from(cond_lcl))],
+        Place::from(unit_lcl),
+    );
+}
+
 fn call_kani_any_for_ty(
     tcx: TyCtxt,
     models: AnyModels,
@@ -450,6 +541,10 @@ fn call_kani_any_for_ty(
         let lcl = body.new_local(ty, source.span(body.blocks()), mutability);
         body.insert_call(&any_inst, source, InsertPosition::Before, vec![], Place::from(lcl));
 
+        // Constrain the value to the type's layout niche, if any. This only reads `lcl`, so the
+        // invariant assumption below can still move out of it.
+        assume_scalar_niche(tcx, models.kani_assume, body, source, lcl, ty);
+
         // If the type has a safety invariant, assume that it holds for the nondeterministic value.
         // We only check ADTs since those are the only types for which users can implement
         // `Invariant` in a way that constrains the values (the library's implementations for

tests/script-based-pre/autoharness_niche/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_niche/expected

@@ -0,0 +1,9 @@
+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

@@ -0,0 +1,76 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(rustc_attrs)]
+#![allow(internal_features)]
+
+// A ranged scalar newtype, as the deranged crate (and std's NonZero) define them: the layout
+// niche IS the validity invariant.
+#[rustc_layout_scalar_valid_range_start(1)]
+#[rustc_layout_scalar_valid_range_end(12)]
+#[derive(Clone, Copy)]
+pub struct Month(u8);
+
+impl Month {
+    pub fn get(self) -> u8 {
+        self.0
+    }
+}
+
+pub struct Schedule {
+    month: Month,
+    day: u8,
+}
+
+// Previously a false alarm: raw field synthesis produced Month values outside 1..=12
+// (language-level invalid), tripping the assert.
+pub fn days_left_in_year(s: Schedule) -> u16 {
+    assert!(s.month.get() >= 1 && s.month.get() <= 12, "invalid month is UB");
+    (12 - s.month.get() as u16) * 31 + (31 - s.day.min(31) as u16)
+}
+
+// The assumption must not over-constrain: all valid months remain reachable.
+pub fn cover_extremes(m: Month) {
+    kani::cover!(m.get() == 1, "january reachable");
+    kani::cover!(m.get() == 12, "december reachable");
+}
+
+// The motivating real-world case (found in the crates.io evaluation): `Duration`'s
+// `Nanoseconds` field carries a 0..=999_999_999 niche, so raw field synthesis produced
+// durations whose subsec_nanos exceeded a second.
+pub fn duration_nanos(d: std::time::Duration) -> u32 {
+    assert!(d.subsec_nanos() < 1_000_000_000, "nanos out of range");
+    d.subsec_nanos()
+}
+
+// A *wrapping* niche: `NonZero`'s valid range is 1..=0, so the range check has to be a
+// disjunction rather than a conjunction.
+pub fn nonzero(v: std::num::NonZeroU8) -> u8 {
+    assert!(v.get() != 0, "NonZeroU8 was zero");
+    v.get()
+}
+
+// A niche reached through *generic instantiation*: the candidate type for `M` is derived from
+// `Monthly`'s only implementor, so the value is generated for a niche-carrying type chosen by
+// the instantiation search rather than named in the signature.
+pub trait Monthly {
+    fn month(&self) -> u8;
+}
+impl Monthly for Month {
+    fn month(&self) -> u8 {
+        self.0
+    }
+}
+pub fn check_monthly<M: Monthly>(m: M) -> u8 {
+    assert!(m.month() >= 1 && m.month() <= 12, "generic instantiation broke the niche");
+    m.month()
+}
+
+// A niche on a *signed* scalar: the valid range is expressed as raw bit patterns, so the
+// comparison must be unsigned (here start=1 with no end, i.e. every pattern but 0).
+#[rustc_layout_scalar_valid_range_start(1)]
+#[derive(Clone, Copy)]
+pub struct NonZeroI8(i8);
+pub fn signed_niche(p: NonZeroI8) -> i8 {
+    assert!(p.0 != 0, "NonZeroI8 was zero");
+    p.0
+}

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

@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Values generated for types with layout niches (rustc_layout_scalar_valid_range, as used by
+# std's NonZero and core::time::Nanoseconds) must respect the niche: it is a language-level
+# validity invariant. days_left_in_year previously failed on out-of-niche months; the covers
+# check the assumption does not over-constrain.
+kani autoharness -Z autoharness --output-format=regular niche_probe.rs