From fb013fb486542eb8aae3c5162c631124d873a770 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 5 Aug 2026 15:04:41 +0000 Subject: [PATCH] Autoharness: assume layout niches of generated scalar values A layout niche (rustc_layout_scalar_valid_range, as used by std's NonZero and core::time::Duration's Nanoseconds field) is a language-level validity invariant: a value outside the niche is as invalid as a bool holding 3, and rustc packs enum variants into the invalid patterns. Nondeterministic-value generation for types without an Arbitrary implementation previously produced such values, which is unsound in the garbage-in sense and causes false alarms in every harness generating the type. After each generated value of a scalar-ABI type whose valid range is restricted, emit kani::assume( in valid_range), handling wrapping ranges (NonZero's 1..=0). Sound by construction: no flag or report marker needed. Verified on the time crate: fixes the InstantExt/SystemTimeExt signed_duration_since harnesses (std Duration receivers); the regression test's covers confirm no over-constraining. Co-authored-by: Kiro --- kani-compiler/src/kani_middle/mod.rs | 43 +++++++ .../src/kani_middle/transform/automatic.rs | 105 +++++++++++++++++- .../autoharness_niche/config.yml | 4 + .../autoharness_niche/expected | 9 ++ .../autoharness_niche/niche_probe.rs | 76 +++++++++++++ .../script-based-pre/autoharness_niche/run.sh | 9 ++ 6 files changed, 241 insertions(+), 5 deletions(-) create mode 100644 tests/script-based-pre/autoharness_niche/config.yml create mode 100644 tests/script-based-pre/autoharness_niche/expected create mode 100644 tests/script-based-pre/autoharness_niche/niche_probe.rs create mode 100755 tests/script-based-pre/autoharness_niche/run.sh diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index dc76e5644e9..3f67136fe09 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/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 { + 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::()` (c.f. `KaniModel::AssumeSafe`) instantiation to determine if /// `T: Invariant`. The model looks like: /// ```rust diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 52a6570032a..6a703b8a98c 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -14,7 +14,7 @@ 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; @@ -22,12 +22,13 @@ 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( 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 diff --git a/tests/script-based-pre/autoharness_niche/config.yml b/tests/script-based-pre/autoharness_niche/config.yml new file mode 100644 index 00000000000..ce281b64090 --- /dev/null +++ b/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 diff --git a/tests/script-based-pre/autoharness_niche/expected b/tests/script-based-pre/autoharness_niche/expected new file mode 100644 index 00000000000..b65bd3d93cc --- /dev/null +++ b/tests/script-based-pre/autoharness_niche/expected @@ -0,0 +1,9 @@ +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 new file mode 100644 index 00000000000..6d0c12470ca --- /dev/null +++ b/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: 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 +} diff --git a/tests/script-based-pre/autoharness_niche/run.sh b/tests/script-based-pre/autoharness_niche/run.sh new file mode 100755 index 00000000000..2839af901d9 --- /dev/null +++ b/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