Autoharness: assume layout niches of generated scalar values

[tautschnig]

Description

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 bit patterns. Autoharness's compiler-derived generation for types without an Arbitrary implementation previously produced such values — unsound in the garbage-in sense, and a source of false alarms in every harness generating the type (found in the top-100/500 crates.io evaluations for #3832: e.g. std::time::Duration receivers via time's InstantExt::signed_duration_since).

After each generated value of a scalar-ABI type with a restricted valid range, emit kani::assume(<raw bits> in valid_range) (transmute to the width-matched uint; wrapping ranges like NonZero's 1..=0 handled). The assumption is sound by construction — assuming a necessary condition of language-level validity keeps every valid value in the explored set — so no flag or report marker is needed.

Testing

New autoharness_niche test: a rustc_layout_scalar_valid_range ranged type; the function asserting the range now verifies (previously a false alarm), and cover checks pin that both range extremes remain reachable (no over-constraining). Counterfactual verified against the pre-change build (Failure -> Success). Autoderive suites pass.

Towards #3832.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

This PR tightens autoharness value generation for scalar-ABI types that have compiler-defined validity ranges (“layout niches”, e.g., rustc_layout_scalar_valid_range_*), by constraining generated values to the type’s valid bit-pattern range via kani::assume. This addresses unsound “garbage-in” generation that can produce language-level invalid values and trigger false alarms (e.g., ranged newtypes similar to NonZero).

Changes:

• Add scalar-niche detection (scalar_niche) based on rustc layout metadata, and use it to emit kani::assume range constraints during automatic generation.
• Thread KaniHook::Assume through automatic harness / arbitrary generation so niche assumptions can be injected.
• Add a new script-based regression test (autoharness_niche) validating both soundness (no out-of-range false alarm) and non-overconstraint (range extremes still reachable).

Reviewed changes

Copilot reviewed 7 out of 8 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
tests/script-based-pre/autoharness_niche/run.sh	Runs the new niche regression via kani autoharness.
tests/script-based-pre/autoharness_niche/niche_probe.rs	Defines a ranged scalar newtype and coverage/assertion checks for niche behavior.
tests/script-based-pre/autoharness_niche/expected	Expected successful verification output for the new test.
tests/script-based-pre/autoharness_niche/config.yml	Wires the script-based-pre test into the harness.
kani-compiler/src/kani_middle/transform/automatic.rs	Injects niche assumptions into automatic generation by calling kani::assume on computed range predicates.
kani-compiler/src/kani_middle/mod.rs	Introduces ScalarNiche + scalar_niche() helper using rustc layout to detect restricted valid ranges.
Cargo.lock	Updates the charon package version entry.

Suppressed comments (1)

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

• If place_local is moved to obtain raw bits (needed to support non-Copy niche types), place_local must be re-initialized so the caller can still use/move it later. You can restore it from the already-computed raw_lcl in the continuation block after the kani::assume call (which also ensures reconstruction only happens on assumed-valid paths).

    body.insert_call(
        &assume_inst,
        source,
        InsertPosition::Before,
        vec![Operand::Move(Place::from(cond_lcl))],

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.