From ff8ffe5d01fe498ecc5d4112ca0ed326f9059973 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 5 Aug 2026 15:04:41 +0000 Subject: [PATCH 1/4] 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 --- Cargo.lock | 2 +- charon | 2 +- kani-compiler/src/kani_middle/mod.rs | 35 ++++ .../src/kani_middle/transform/automatic.rs | 158 ++++++++++++++++-- .../autoharness_niche/config.yml | 4 + .../autoharness_niche/expected | 4 + .../autoharness_niche/niche_probe.rs | 35 ++++ .../script-based-pre/autoharness_niche/run.sh | 9 + 8 files changed, 231 insertions(+), 18 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/Cargo.lock b/Cargo.lock index 0ba3f8aaab89..482bf84cbf83 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -288,7 +288,7 @@ checksum = "f079e83a288787bcd14a6aea84cee5c87a67c5a3e660c30f557a3d24761b3527" [[package]] name = "charon" -version = "0.1.88" +version = "0.1.73" dependencies = [ "annotate-snippets", "anstream 0.6.21", diff --git a/charon b/charon index 607f5683aee3..dee6603064c2 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit 607f5683aee39a427267f8cdc1aa15735b096a1a +Subproject commit dee6603064c23aa331efc58802e7b511eb405f35 diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 2f7aedf59663..94b78e3ff84a 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -300,6 +300,41 @@ 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; + } + Some(ScalarNiche { bits, start: valid_range.start, end: valid_range.end }) +} + /// Is `ty` a struct or enum whose fields/variants implement Arbitrary, or a reference to such a /// type? fn can_derive_arbitrary( diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 59ca3bd34abf..0bc14fdd38e9 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -9,21 +9,22 @@ use crate::args::ReachabilityType; use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; -use crate::kani_middle::implements_arbitrary; use crate::kani_middle::kani_functions::{KaniHook, KaniIntrinsic, KaniModel}; use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use crate::kani_middle::transform::{TransformPass, TransformationType}; +use crate::kani_middle::{implements_arbitrary, scalar_niche}; 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, Local, MutBorrowKind, Mutability, Operand, - Place, Rvalue, SwitchTargets, Terminator, TerminatorKind, + AggregateKind, BasicBlockIdx, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, + MutBorrowKind, Mutability, Operand, Place, Rvalue, SwitchTargets, Terminator, TerminatorKind, }; use rustc_public::ty::{ - AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Ty, TyKind, UintTy, VariantDef, + AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyKind, UintTy, + VariantDef, }; use rustc_public_bridge::IndexedVal; use tracing::debug; @@ -34,13 +35,16 @@ use tracing::debug; pub struct AutomaticArbitraryPass { /// The FnDef of KaniModel::Any kani_any: FnDef, + /// The FnDef of KaniHook::Assume (used for layout-niche assumptions). + kani_assume: FnDef, } impl AutomaticArbitraryPass { pub fn new(_unit: &CodegenUnit, query_db: &QueryDb) -> Self { let kani_fns = query_db.kani_functions(); let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap(); - Self { kani_any } + let kani_assume = *kani_fns.get(&KaniHook::Assume.into()).unwrap(); + Self { kani_any, kani_assume } } } @@ -93,7 +97,7 @@ impl TransformPass for AutomaticArbitraryPass { /// ``` /// We match the implementations that kani_macros::derive creates for structs and enums, /// so see that module for full documentation of what the generated bodies look like. - fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { debug!(function=?instance.name(), "AutomaticArbitraryPass::transform"); let unexpected_ty = |ty: &Ty| { @@ -116,8 +120,8 @@ impl TransformPass for AutomaticArbitraryPass { if let TyKind::RigidTy(RigidTy::Adt(def, args)) = ty.kind() { match def.kind() { - AdtKind::Enum => (true, self.generate_enum_body(def, args, body)), - AdtKind::Struct => (true, self.generate_struct_body(def, args, body)), + AdtKind::Enum => (true, self.generate_enum_body(tcx, def, args, body)), + AdtKind::Struct => (true, self.generate_struct_body(tcx, def, args, body)), AdtKind::Union => unexpected_ty(ty), } } else { @@ -128,15 +132,107 @@ impl TransformPass for AutomaticArbitraryPass { /// Insert a call to kani::any::() in `body`; return the local storing the result. /// Panics if `ty` does not implement Arbitrary. +/// If `ty` has a scalar layout with a restricted valid range (a niche), append +/// `kani::assume( in valid_range)`. +/// Values outside the niche are language-level invalid (rustc packs enum variants into the +/// invalid patterns), so nondeterministic-value generation must 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 false alarms in every harness generating the type. +/// The assumption is sound by construction and requires no 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, kani_any: FnDef, + kani_assume: FnDef, body: &mut MutableBody, ty: Ty, mutability: Mutability, source: &mut SourceInstruction, ) -> Local { if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind() { - let inner_lcl = call_kani_any_for_ty(kani_any, body, inner_ty, inner_mutability, source); + let inner_lcl = call_kani_any_for_ty( + tcx, + kani_any, + kani_assume, + body, + inner_ty, + inner_mutability, + source, + ); let ref_lcl = body.new_local(ty, source.span(body.blocks()), mutability); let borrow_kind = if inner_mutability == Mutability::Not { BorrowKind::Shared @@ -156,6 +252,8 @@ fn call_kani_any_for_ty( .unwrap_or_else(|_| panic!("expected a ty that implements Arbitrary, got {ty}")); let lcl = body.new_local(ty, source.span(body.blocks()), mutability); body.insert_call(&kani_any_inst, source, InsertPosition::Before, vec![], Place::from(lcl)); + // Constrain the value to the type's layout niche, if any. + assume_scalar_niche(tcx, kani_assume, body, source, lcl, ty); lcl } } @@ -170,6 +268,7 @@ impl AutomaticArbitraryPass { /// This function will panic if a field type does not implement Arbitrary. fn call_kani_any_for_variant( &self, + tcx: TyCtxt, adt_def: AdtDef, adt_args: &GenericArgs, body: &mut MutableBody, @@ -181,7 +280,15 @@ impl AutomaticArbitraryPass { // Construct nondeterministic values for each of the variant's fields for ty in fields.iter().map(|field| field.ty_with_args(adt_args)) { - let lcl = call_kani_any_for_ty(self.kani_any, body, ty, Mutability::Not, source); + let lcl = call_kani_any_for_ty( + tcx, + self.kani_any, + self.kani_assume, + body, + ty, + Mutability::Not, + source, + ); field_locals.push(lcl); } @@ -213,7 +320,7 @@ impl AutomaticArbitraryPass { /// _ => Enum::LastVariant /// } /// ``` - fn generate_enum_body(&self, def: AdtDef, args: GenericArgs, body: Body) -> Body { + fn generate_enum_body(&self, tcx: TyCtxt, def: AdtDef, args: GenericArgs, body: Body) -> Body { // Autoharness only deems a function with an enum eligible if it has at least one variant, c.f. `can_derive_arbitrary` assert!(def.num_variants() > 0); @@ -223,7 +330,9 @@ impl AutomaticArbitraryPass { // Generate a nondet u128 to switch on let discr_lcl = call_kani_any_for_ty( + tcx, self.kani_any, + self.kani_assume, &mut new_body, Ty::from_rigid_kind(RigidTy::Uint(UintTy::U128)), Mutability::Not, @@ -241,8 +350,14 @@ impl AutomaticArbitraryPass { let mut branches: Vec<(u128, BasicBlockIdx)> = vec![]; for variant in def.variants_iter() { - let target_bb = - self.call_kani_any_for_variant(def, &args, &mut new_body, &mut source, variant); + let target_bb = self.call_kani_any_for_variant( + tcx, + def, + &args, + &mut new_body, + &mut source, + variant, + ); branches.push((variant.idx.to_index() as u128, target_bb)); } @@ -268,7 +383,13 @@ impl AutomaticArbitraryPass { /// ... /// } /// ``` - fn generate_struct_body(&self, def: AdtDef, args: GenericArgs, body: Body) -> Body { + fn generate_struct_body( + &self, + tcx: TyCtxt, + def: AdtDef, + args: GenericArgs, + body: Body, + ) -> Body { assert_eq!(def.num_variants(), 1); let mut new_body = MutableBody::from(body); @@ -276,7 +397,7 @@ impl AutomaticArbitraryPass { let mut source = SourceInstruction::Terminator { bb: 0 }; let variant = def.variants()[0]; - self.call_kani_any_for_variant(def, &args, &mut new_body, &mut source, variant); + self.call_kani_any_for_variant(tcx, def, &args, &mut new_body, &mut source, variant); new_body.into() } @@ -284,6 +405,8 @@ impl AutomaticArbitraryPass { /// Transform the dummy body of an automatic_harness Kani intrinsic to be a proof harness for a given function. #[derive(Debug, Clone)] pub struct AutomaticHarnessPass { + /// The FnDef of KaniHook::Assume (used for layout-niche assumptions). + kani_assume: FnDef, kani_any: FnDef, init_contracts_hook: Instance, kani_autoharness_intrinsic: FnDef, @@ -292,13 +415,14 @@ pub struct AutomaticHarnessPass { impl AutomaticHarnessPass { pub fn new(query_db: &QueryDb) -> Self { let kani_fns = query_db.kani_functions(); + let kani_assume = *kani_fns.get(&KaniHook::Assume.into()).unwrap(); let kani_autoharness_intrinsic = *kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap(); let init_contracts_hook = *kani_fns.get(&KaniHook::InitContracts.into()).unwrap(); let init_contracts_hook = Instance::resolve(init_contracts_hook, &GenericArgs(vec![])).unwrap(); - Self { kani_any, init_contracts_hook, kani_autoharness_intrinsic } + Self { kani_assume, kani_any, init_contracts_hook, kani_autoharness_intrinsic } } } @@ -359,7 +483,9 @@ impl TransformPass for AutomaticHarnessPass { .iter() .map(|local_decl| { call_kani_any_for_ty( + tcx, self.kani_any, + self.kani_assume, &mut harness_body, local_decl.ty, local_decl.mutability, 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 000000000000..ce281b640905 --- /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 000000000000..77f8b21e79d5 --- /dev/null +++ b/tests/script-based-pre/autoharness_niche/expected @@ -0,0 +1,4 @@ +Status: SATISFIED +Status: SATISFIED +| niche_probe | cover_extremes | #[kani::proof] | Success | +| niche_probe | days_left_in_year | #[kani::proof] | Success | 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 000000000000..7c7e0724d25c --- /dev/null +++ b/tests/script-based-pre/autoharness_niche/niche_probe.rs @@ -0,0 +1,35 @@ +// 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"); +} 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 000000000000..2839af901d99 --- /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 From 00b63ea393a4de4e0c55a1c19c5b0a243282403e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 5 Aug 2026 15:51:00 +0000 Subject: [PATCH 2/4] Autoharness: constructor-based value generation (--constructor-args) The top-100 crates.io failure triage (#3832) showed the largest class of genuine false alarms is generated receivers violating private type invariants (e.g. time's Date packs a validated ordinal; raw field synthesis produces invalid dates, failing every method harness). Under the new opt-in --constructor-args flag, kani::any:: for private-field structs is synthesized as: generate nondeterministic constructor arguments, call one of T's public constructors, assume success (switching on the discriminant for Option/Result returns), and return the payload. Constructor search excludes non-public, doc-hidden (commonly _unchecked variants exported for macros that assert preconditions), unsafe, zero-argument (single-point coverage; Instant::now() reaches unsupported clock_gettime), and generic constructors; it prefers Self over Option over Result returns, then more arguments over fewer. The option is opt-in because it under-approximates (only constructor-reachable values are explored): harnesses are marked "(ctor)" via new is_ctor_based metadata, with an explanatory note in the summary. Measured on time-0.3.54: 341 -> 538 verified, 500 -> 315 failures. Co-authored-by: Kiro --- .../src/reference/experimental/autoharness.md | 16 + kani-compiler/src/args.rs | 9 + .../src/kani_middle/codegen_units.rs | 26 +- kani-compiler/src/kani_middle/metadata.rs | 3 + kani-compiler/src/kani_middle/mod.rs | 300 ++++++++++++++++++ .../src/kani_middle/transform/automatic.rs | 195 +++++++++++- kani-driver/src/args/autoharness_args.rs | 15 + kani-driver/src/autoharness/mod.rs | 35 +- kani-driver/src/metadata.rs | 1 + kani-driver/src/sarif.rs | 1 + kani_metadata/src/harness.rs | 5 + .../cargo_autoharness_constructor/Cargo.toml | 6 + .../cargo_autoharness_constructor/config.yml | 4 + .../constructor.expected | 15 + .../constructor.sh | 13 + .../cargo_autoharness_constructor/src/lib.rs | 49 +++ 16 files changed, 680 insertions(+), 13 deletions(-) create mode 100644 tests/script-based-pre/cargo_autoharness_constructor/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoharness_constructor/config.yml create mode 100644 tests/script-based-pre/cargo_autoharness_constructor/constructor.expected create mode 100755 tests/script-based-pre/cargo_autoharness_constructor/constructor.sh create mode 100644 tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index a57ca448f1d1..8f05949e07f2 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -79,6 +79,22 @@ Autoharness also accepts a `--list` argument, which runs the [list subcommand](. For a full list of options, run `kani autoharness --help`. +### Constructor-based generation (--constructor-args) + +By default, when a type does not implement `Arbitrary`, Kani synthesizes values field by field. +For types whose private fields carry a representation invariant (e.g. a date type storing a +packed, validated ordinal), raw field synthesis can produce values that violate the invariant, +causing false alarms in every harness that generates the type. With `--constructor-args`, Kani +instead generates values of private-field struct types by calling one of the type's public +constructors with nondeterministic arguments, assuming success for constructors returning +`Option` or `Result`. Constructors that are doc-hidden, unsafe, zero-argument, +or generic are not considered. + +This option is opt-in because it under-approximates: harnesses whose values are generated this +way are marked "(ctor)" in the output, and their verification results only cover values +reachable through the chosen constructor; a bug that requires a different value will not be +found. + ## Example Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again: ```rust diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index f20dd8318fe6..9f673c1c9781 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -111,6 +111,15 @@ pub struct Arguments { /// See kani_driver::autoharness_args for documentation. #[arg(long = "autoharness-exclude-pattern", num_args(1))] pub autoharness_excluded_patterns: Vec, + /// If we are running the autoharness subcommand, whether to generate harnesses for + /// functions whose arguments require bounded nondeterministic values (e.g. slice + /// references). See kani_driver::autoharness_args for documentation. + #[arg(long = "autoharness-bounded-arguments")] + pub autoharness_bounded_arguments: bool, + + /// Enable constructor-based nondeterministic value generation for autoharness. + #[arg(long = "autoharness-constructor-args")] + pub autoharness_constructor_args: bool, } #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 4b9236c5d45c..573318df568e 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -108,7 +108,9 @@ impl CodegenUnits { .set(AutoHarnessMetadata { chosen: chosen .iter() - .map(|func| crate::kani_middle::strip_local_crate_prefix(func.name())) + .map(|(func, _)| { + crate::kani_middle::strip_local_crate_prefix(func.name()) + }) .collect::>(), skipped, }) @@ -361,13 +363,13 @@ fn determine_targets( /// the AutomaticHarnessPass will later transform the bodies of these instances to actually verify the function. fn get_all_automatic_harnesses( tcx: TyCtxt, - verifiable_fns: Vec, + verifiable_fns: Vec<(Instance, bool)>, kani_harness_intrinsic: FnDef, base_filename: &Path, ) -> HashMap { verifiable_fns .into_iter() - .map(|fn_to_verify| { + .map(|(fn_to_verify, is_ctor_based)| { // Set the generic arguments of the harness to be the function it is verifying // so that later, in AutomaticHarnessPass, we can retrieve the function to verify // and generate the harness body accordingly. @@ -381,6 +383,7 @@ fn get_all_automatic_harnesses( base_filename, &fn_to_verify, harness.mangled_name(), + is_ctor_based, ); (harness, metadata) }) @@ -417,7 +420,7 @@ fn automatic_harness_partition( args: &Arguments, crate_name: &str, kani_any_def: FnDef, -) -> (Vec, BTreeMap) { +) -> (Vec<(Instance, bool)>, BTreeMap) { let crate_fn_defs = rustc_public::local_crate().fn_defs().into_iter().collect::>(); // Filter out CrateItems that are functions, but not functions defined in the crate itself, i.e., rustc-inserted functions // (c.f. https://github.com/model-checking/kani/issues/4189) @@ -513,7 +516,20 @@ fn automatic_harness_partition( if let Some(reason) = skip_reason(func) { skipped.insert(crate::kani_middle::strip_local_crate_prefix(func.name()), reason); } else { - chosen.push(Instance::try_from(func).unwrap()); + let instance = Instance::try_from(func).unwrap(); + let is_ctor_based = args.autoharness_constructor_args + && instance.body().is_some_and(|body| { + body.arg_locals().iter().any(|arg| { + crate::kani_middle::uses_ctor_generation( + tcx, + arg.ty, + kani_any_def, + &mut FxHashMap::default(), + &mut vec![], + ) + }) + }); + chosen.push((instance, is_ctor_based)); } } diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index d2348ab7b132..78ae41d4d823 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -42,6 +42,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> contract: Default::default(), has_loop_contracts: false, is_automatically_generated: false, + is_ctor_based: false, } } @@ -121,6 +122,7 @@ pub fn gen_automatic_proof_metadata( base_name: &Path, fn_to_verify: &Instance, harness_mangled_name: String, + is_ctor_based: bool, ) -> HarnessMetadata { let def = fn_to_verify.def; let pretty_name = readable_name(*fn_to_verify); @@ -159,5 +161,6 @@ pub fn gen_automatic_proof_metadata( contract: Default::default(), has_loop_contracts: false, is_automatically_generated: true, + is_ctor_based, } } diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 94b78e3ff84a..858bb88c769a 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -300,6 +300,306 @@ fn implements_arbitrary( false } +/// Whether generating a value of `ty` (under `--constructor-args`) would use constructor-based +/// generation for some ADT reachable in `ty`'s type tree: an ADT with a private field and a +/// viable public constructor. Used to mark such harnesses "(ctor)" in reports, since their +/// verification results only cover constructor-reachable values. +pub fn uses_ctor_generation( + tcx: TyCtxt, + ty: Ty, + kani_any_def: FnDef, + ty_arbitrary_cache: &mut FxHashMap, + visited: &mut Vec, +) -> bool { + if visited.contains(&ty) || visited.len() > 32 { + return false; + } + visited.push(ty); + match ty.kind() { + TyKind::RigidTy(RigidTy::Ref(_, inner, _)) | TyKind::RigidTy(RigidTy::RawPtr(inner, _)) => { + uses_ctor_generation(tcx, inner, kani_any_def, ty_arbitrary_cache, visited) + } + TyKind::RigidTy(RigidTy::Array(inner, _)) | TyKind::RigidTy(RigidTy::Slice(inner)) => { + uses_ctor_generation(tcx, inner, kani_any_def, ty_arbitrary_cache, visited) + } + TyKind::RigidTy(RigidTy::Tuple(elems)) => elems.iter().any(|elem| { + uses_ctor_generation(tcx, *elem, kani_any_def, ty_arbitrary_cache, visited) + }), + TyKind::RigidTy(RigidTy::Adt(def, args)) => { + // Hand-written Arbitrary implementations take precedence over ctor generation + // in the transform (it only rewrites unresolvable kani::any calls). + if implements_arbitrary_directly(ty, kani_any_def) { + return false; + } + if def.kind() == AdtKind::Struct + && adt_has_private_field_check(tcx, def) + && (find_unchecked_constructor(tcx, ty, kani_any_def, ty_arbitrary_cache).is_some() + || find_arbitrary_constructor(tcx, ty, kani_any_def, ty_arbitrary_cache) + .is_some()) + { + return true; + } + def.variants_iter().any(|variant| { + variant.fields().iter().any(|field| { + uses_ctor_generation( + tcx, + field.ty_with_args(&args), + kani_any_def, + ty_arbitrary_cache, + visited, + ) + }) + }) || args.0.iter().any(|arg| match arg { + GenericArgKind::Type(t) => { + uses_ctor_generation(tcx, *t, kani_any_def, ty_arbitrary_cache, visited) + } + _ => false, + }) + } + _ => false, + } +} + +/// Whether the ADT has at least one non-public field (in any variant). +pub fn adt_has_private_field_check(tcx: TyCtxt, def: AdtDef) -> bool { + let did = rustc_internal::internal(tcx, def.def_id()); + tcx.adt_def(did).all_fields().any(|field| !tcx.visibility(field.did).is_public()) +} + +/// Whether `ty` has a resolvable `::any` (a hand-written or derived source +/// implementation), without considering compiler-side derivation. Mirrors the resolvability +/// test in `implements_arbitrary`: `kani::any::` itself always resolves (it is a concrete +/// generic function); what distinguishes a source implementation is whether the `T::any()` +/// call in its body resolves. +fn implements_arbitrary_directly(ty: Ty, kani_any_def: FnDef) -> bool { + let Ok(inst) = Instance::resolve(kani_any_def, &GenericArgs(vec![GenericArgKind::Type(ty)])) + else { + return false; + }; + let Some(kani_any_body) = inst.body() else { return false }; + for bb in kani_any_body.blocks.iter() { + let TerminatorKind::Call { func, .. } = &bb.terminator.kind else { + continue; + }; + if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = + func.ty(kani_any_body.arg_locals()).unwrap().kind() + { + return Instance::resolve(def, &args).is_ok(); + } + } + false +} + +/// The outcome of searching for a viable public constructor for a type without an Arbitrary +/// implementation (`--constructor-args`): the constructor's instance, and how its return value +/// wraps `Self` (directly, or inside `Option`/`Result`, in which case generated harnesses +/// assume success). +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum CtorReturn { + Direct, + OptionOf, + ResultOf, +} + +/// Search `ty`'s inherent impls for an assert-guarded *representation constructor*: an +/// associated function returning `Self` directly whose preconditions are stated as +/// (debug_)asserts rather than validated returns — typically `unsafe`, doc-hidden or +/// `_unchecked`-named builders exported for macro use (e.g. time's `Date::from_parts`). +/// Under `--constructor-args`, such a constructor is inlined with panic paths converted to +/// assumptions (c.f. `automatic::inline_with_assumed_panics`), so its own assertions filter +/// the nondeterministic arguments down to exactly the values the crate considers valid. +/// Visibility is irrelevant (the body is inlined, not called). Prefers more arguments over +/// fewer; ties broken by definition order. +pub fn find_unchecked_constructor( + tcx: TyCtxt, + ty: Ty, + kani_any_def: FnDef, + ty_arbitrary_cache: &mut FxHashMap, +) -> Option { + let TyKind::RigidTy(RigidTy::Adt(adt_def, ref adt_args)) = ty.kind() else { + return None; + }; + let adt_did = rustc_internal::internal(tcx, adt_def.def_id()); + let mut best: Option<(Instance, usize)> = None; + for &impl_did in tcx.inherent_impls(adt_did) { + for &item in tcx.associated_item_def_ids(impl_did) { + if !tcx.def_kind(item).is_fn_like() || tcx.associated_item(item).is_method() { + continue; + } + if tcx + .generics_of(item) + .own_params + .iter() + .any(|p| !matches!(p.kind, rustc_middle::ty::GenericParamDefKind::Lifetime)) + { + continue; + } + let Some(ctor_def) = to_fn_def(tcx, item) else { continue }; + // For generic ADTs (e.g. deranged's RangedI32), instantiate the + // constructor with the ADT's own generic arguments: for inherent impls whose + // parameters mirror the type's, this is the correct substitution; when it is + // not, resolution fails and the constructor is skipped. + let Ok(instance) = Instance::resolve(ctor_def, adt_args) else { + continue; + }; + if !instance.has_body() { + continue; + } + let TyKind::RigidTy(RigidTy::FnDef(..)) = instance.ty().kind() else { continue }; + let Some(binder) = instance.ty().kind().fn_sig() else { continue }; + let fn_sig = binder.skip_binder(); + if fn_sig.output() != ty { + continue; + } + // The unchecked-builder heuristic: unsafe, doc-hidden, or *_unchecked-named. + let name = tcx.item_name(item).to_string(); + let is_unchecked = fn_sig.safety == rustc_public::mir::Safety::Unsafe + || tcx.is_doc_hidden(item) + || name.contains("unchecked"); + if !is_unchecked { + continue; + } + if fn_sig.inputs().is_empty() + || !fn_sig + .inputs() + .iter() + .all(|input| implements_arbitrary(*input, kani_any_def, ty_arbitrary_cache)) + { + continue; + } + let n_args = fn_sig.inputs().len(); + if best.as_ref().is_none_or(|(_, best_n)| n_args > *best_n) { + best = Some((instance, n_args)); + } + } + } + best.map(|(inst, _)| inst) +} + +/// Search `ty`'s inherent impls for a public associated function usable as a constructor: +/// one that returns `Self`, `Option` or `Result`, takes no `self` argument, +/// has no remaining generic parameters of its own, and whose every argument implements (or +/// can derive) Arbitrary. Prefer `Self` over `Option` over `Result` returns +/// (fewer assumptions), and among equal shapes, prefer the constructor with the most +/// arguments (heuristically the least-constrained coverage of the value space); ties are +/// broken by definition order for determinism. +pub fn find_arbitrary_constructor( + tcx: TyCtxt, + ty: Ty, + kani_any_def: FnDef, + ty_arbitrary_cache: &mut FxHashMap, +) -> Option<(Instance, CtorReturn)> { + let TyKind::RigidTy(RigidTy::Adt(adt_def, ref adt_args)) = ty.kind() else { + return None; + }; + let adt_did = rustc_internal::internal(tcx, adt_def.def_id()); + let mut best: Option<(Instance, CtorReturn, usize)> = None; + for &impl_did in tcx.inherent_impls(adt_did) { + for &item in tcx.associated_item_def_ids(impl_did) { + if !tcx.def_kind(item).is_fn_like() || tcx.associated_item(item).is_method() { + continue; + } + if !tcx.visibility(item).is_public() { + continue; + } + // Exclude doc-hidden constructors: they are de-facto internal (commonly + // `_unchecked` variants exported for macro use that assert their preconditions + // instead of validating, e.g. time's `Date::__from_ordinal_date_unchecked`), + // and calling them with nondeterministic arguments manufactures false alarms + // in every harness that generates the type. Unsafe constructors are excluded + // for the same reason: their preconditions are the caller's obligation. + if tcx.is_doc_hidden(item) { + continue; + } + // The constructor may only use the ADT's own generic parameters (inherited via + // the impl); reject constructors introducing their own generics. + if tcx + .generics_of(item) + .own_params + .iter() + .any(|p| !matches!(p.kind, rustc_middle::ty::GenericParamDefKind::Lifetime)) + { + continue; + } + let Some(ctor_def) = to_fn_def(tcx, item) else { continue }; + // Instantiate the impl's generics with the ADT instantiation's arguments. For + // phase 1, only support non-generic ADTs (no substitution needed). + if !adt_args.0.is_empty() { + continue; + } + let fn_sig = ctor_def.fn_sig().skip_binder(); + if fn_sig.safety == rustc_public::mir::Safety::Unsafe { + continue; + } + // Zero-argument constructors produce a single value, which destroys the coverage + // a nondeterministic harness is meant to provide, and is actively harmful for + // environment-reading constructors (e.g. Instant::now() reaches clock_gettime, + // which Kani does not support, failing every harness that generates the type). + if fn_sig.inputs().is_empty() { + continue; + } + let ret = fn_sig.output(); + let shape = if ret == ty { + CtorReturn::Direct + } else if let TyKind::RigidTy(RigidTy::Adt(wrap_def, wrap_args)) = ret.kind() { + let name = wrap_def.name(); + let payload = wrap_args.0.first().and_then(|a| match a { + GenericArgKind::Type(t) => Some(*t), + _ => None, + }); + if payload != Some(ty) { + continue; + } else if name == "core::option::Option" || name == "std::option::Option" { + CtorReturn::OptionOf + } else if name == "core::result::Result" || name == "std::result::Result" { + CtorReturn::ResultOf + } else { + continue; + } + } else { + continue; + }; + // Every constructor argument must be plainly generatable (implements or derives + // Arbitrary); constructor arguments do not get the argument-position extensions + // (slices, smart pointers, nested constructors) in phase 1. + if !fn_sig + .inputs() + .iter() + .all(|input| implements_arbitrary(*input, kani_any_def, ty_arbitrary_cache)) + { + continue; + } + let Ok(instance) = Instance::resolve(ctor_def, &GenericArgs(vec![])) else { + continue; + }; + if !instance.has_body() { + continue; + } + let n_args = fn_sig.inputs().len(); + let better = match &best { + None => true, + Some((_, best_shape, best_n)) => { + (shape as u8, std::cmp::Reverse(n_args)) + < (*best_shape as u8, std::cmp::Reverse(*best_n)) + } + }; + if better { + best = Some((instance, shape, n_args)); + } + } + } + best.map(|(inst, shape, _)| (inst, shape)) +} + +/// Convert an internal DefId of a function-like item to a stable FnDef. +fn to_fn_def(tcx: TyCtxt, def_id: rustc_span::def_id::DefId) -> Option { + let ty = rustc_internal::stable(tcx.type_of(def_id).instantiate_identity()); + match ty.kind() { + TyKind::RigidTy(RigidTy::FnDef(def, _)) => Some(def), + _ => None, + } +} + /// 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 diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 0bc14fdd38e9..b48febcd8df1 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -12,7 +12,10 @@ use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::kani_functions::{KaniHook, KaniIntrinsic, KaniModel}; use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use crate::kani_middle::transform::{TransformPass, TransformationType}; -use crate::kani_middle::{implements_arbitrary, scalar_niche}; +use crate::kani_middle::{ + CtorReturn, adt_has_private_field_check, find_arbitrary_constructor, implements_arbitrary, + scalar_niche, +}; use crate::kani_queries::QueryDb; use rustc_data_structures::fx::FxHashMap; use rustc_middle::ty::TyCtxt; @@ -20,7 +23,8 @@ use rustc_public::CrateDef; use rustc_public::mir::mono::Instance; use rustc_public::mir::{ AggregateKind, BasicBlockIdx, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, - MutBorrowKind, Mutability, Operand, Place, Rvalue, SwitchTargets, Terminator, TerminatorKind, + MutBorrowKind, Mutability, Operand, Place, ProjectionElem, Rvalue, SwitchTargets, Terminator, + TerminatorKind, }; use rustc_public::ty::{ AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyKind, UintTy, @@ -35,8 +39,12 @@ use tracing::debug; pub struct AutomaticArbitraryPass { /// The FnDef of KaniModel::Any kani_any: FnDef, - /// The FnDef of KaniHook::Assume (used for layout-niche assumptions). + /// The FnDef of KaniHook::Assume (used for layout-niche assumptions and constructor + /// success). kani_assume: FnDef, + /// Whether --constructor-args is enabled: generate values of private-field types through + /// their public constructors instead of raw field synthesis. + constructor_args: bool, } impl AutomaticArbitraryPass { @@ -44,7 +52,8 @@ impl AutomaticArbitraryPass { let kani_fns = query_db.kani_functions(); let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap(); let kani_assume = *kani_fns.get(&KaniHook::Assume.into()).unwrap(); - Self { kani_any, kani_assume } + let constructor_args = query_db.args().autoharness_constructor_args; + Self { kani_any, kani_assume, constructor_args } } } @@ -119,6 +128,19 @@ impl TransformPass for AutomaticArbitraryPass { } if let TyKind::RigidTy(RigidTy::Adt(def, args)) = ty.kind() { + // Under --constructor-args, generate values of structs with private fields + // through one of their public constructors (raw field synthesis can violate the + // type's representation invariant, producing false alarms); fall through to + // field synthesis when no viable constructor exists. + if self.constructor_args + && def.kind() == AdtKind::Struct + && adt_has_private_field_check(tcx, def) + && let Some((ctor, shape)) = + find_arbitrary_constructor(tcx, *ty, self.kani_any, &mut FxHashMap::default()) + { + debug!(?ty, ctor=?ctor.name(), ?shape, "generate_ctor_body"); + return (true, self.generate_ctor_body(tcx, ctor, shape, *ty, body)); + } match def.kind() { AdtKind::Enum => (true, self.generate_enum_body(tcx, def, args, body)), AdtKind::Struct => (true, self.generate_struct_body(tcx, def, args, body)), @@ -309,6 +331,171 @@ impl AutomaticArbitraryPass { source.bb() - (fields.len() + 1) } + /// Overwrite the default `kani::any()` implementation `body` for a struct with private + /// fields by calling a public constructor with nondeterministic arguments + /// (`--constructor-args`). The returned body is equivalent to: + /// ```ignore + /// // ctor returning Self: + /// Ty::ctor(kani::any(), ..) + /// // ctor returning Option (Result analogously): + /// match Ty::ctor(kani::any(), ..) { + /// Some(v) => v, + /// None => { kani::assume(false); unreachable!() } + /// } + /// ``` + fn generate_ctor_body( + &self, + tcx: TyCtxt, + ctor: Instance, + shape: CtorReturn, + ty: Ty, + body: Body, + ) -> Body { + let mut new_body = MutableBody::from(body); + new_body.clear_body(TerminatorKind::Unreachable); + let mut source = SourceInstruction::Terminator { bb: 0 }; + + let ctor_sig = ctor.ty().kind().fn_sig().unwrap().skip_binder(); + + // Generate a nondeterministic value for every constructor argument. + let arg_ops: Vec = ctor_sig + .inputs() + .iter() + .map(|input_ty| { + let lcl = call_kani_any_for_ty( + tcx, + self.kani_any, + self.kani_assume, + &mut new_body, + *input_ty, + Mutability::Not, + &mut source, + ); + Operand::Move(Place::from(lcl)) + }) + .collect(); + + if shape == CtorReturn::Direct { + // RETURN_LOCAL = ctor(args); return + new_body.insert_call( + &ctor, + &mut source, + InsertPosition::Before, + arg_ops, + Place::from(0), + ); + let ret_span = source.span(new_body.blocks()); + new_body.insert_terminator( + &mut source, + InsertPosition::Before, + Terminator { kind: TerminatorKind::Return, span: ret_span }, + ); + return new_body.into(); + } + + // Option / Result: call, switch on the discriminant, assume success. + let ret_ty = ctor_sig.output(); + let TyKind::RigidTy(RigidTy::Adt(wrap_def, _)) = ret_ty.kind() else { + unreachable!("constructor return shape guaranteed by find_arbitrary_constructor") + }; + // Some = variant 1 of Option; Ok = variant 0 of Result. Both have discriminant + // values equal to their variant indices. + let ok_idx = match shape { + CtorReturn::OptionOf => 1usize, + CtorReturn::ResultOf => 0usize, + CtorReturn::Direct => unreachable!(), + }; + let ok_variant = wrap_def.variants()[ok_idx]; + + let span = source.span(new_body.blocks()); + let ret_lcl = new_body.new_local(ret_ty, span, Mutability::Not); + new_body.insert_call( + &ctor, + &mut source, + InsertPosition::Before, + arg_ops, + Place::from(ret_lcl), + ); + + // Read the discriminant. + let discr_ty = ret_ty.kind().discriminant_ty().unwrap(); + let discr_lcl = new_body.new_local(discr_ty, span, Mutability::Not); + new_body.assign_to( + Place::from(discr_lcl), + Rvalue::Discriminant(Place::from(ret_lcl)), + &mut source, + InsertPosition::Before, + ); + + // Placeholder for the SwitchInt terminator. + let span = source.span(new_body.blocks()); + new_body.insert_terminator( + &mut source, + InsertPosition::Before, + Terminator { kind: TerminatorKind::Unreachable, span }, + ); + let switch_instr = SourceInstruction::Terminator { bb: source.bb() - 1 }; + + // Failure branch: kani::assume(false); unreachable. + let assume_inst = Instance::resolve(self.kani_assume, &GenericArgs(vec![])).unwrap(); + let false_op = Operand::Constant(ConstOperand { + span, + user_ty: None, + const_: MirConst::from_bool(false), + }); + let unit_lcl = new_body.new_local(Ty::new_tuple(&[]), span, Mutability::Not); + new_body.insert_call( + &assume_inst, + &mut source, + InsertPosition::Before, + vec![false_op], + Place::from(unit_lcl), + ); + new_body.insert_terminator( + &mut source, + InsertPosition::Before, + Terminator { kind: TerminatorKind::Unreachable, span }, + ); + // insert_call + terminator added two blocks; the failure branch starts at the first. + let bad_bb = source.bb() - 2; + + // Success branch: RETURN_LOCAL = move (ret as OkVariant).0; return. + let payload_place = Place { + local: ret_lcl, + projection: vec![ + ProjectionElem::Downcast(ok_variant.idx), + ProjectionElem::Field(0, ty), + ], + }; + new_body.insert_terminator( + &mut source, + InsertPosition::Before, + Terminator { kind: TerminatorKind::Return, span }, + ); + let ok_bb = source.bb() - 1; + let mut assign_instr = SourceInstruction::Terminator { bb: ok_bb }; + new_body.assign_to( + Place::from(0), + Rvalue::Use(Operand::Move(payload_place)), + &mut assign_instr, + InsertPosition::Before, + ); + + let switch = Terminator { + kind: TerminatorKind::SwitchInt { + discr: Operand::Copy(Place::from(discr_lcl)), + targets: SwitchTargets::new( + vec![(ok_variant.idx.to_index() as u128, ok_bb)], + bad_bb, + ), + }, + span, + }; + new_body.replace_terminator(&switch_instr, switch); + + new_body.into() + } + /// Overwrite the default kani::any() implementation `body` for the enum described by `def`. /// The returned body is equivalent to: /// ```ignore diff --git a/kani-driver/src/args/autoharness_args.rs b/kani-driver/src/args/autoharness_args.rs index 93d9eb439127..074add862d0d 100644 --- a/kani-driver/src/args/autoharness_args.rs +++ b/kani-driver/src/args/autoharness_args.rs @@ -23,6 +23,21 @@ pub struct CommonAutoharnessArgs { #[arg(long = "exclude-pattern", num_args(1), value_name = "PATTERN")] pub exclude_pattern: Vec, + /// Also create automatic harnesses for functions whose arguments require *bounded* + /// nondeterministic values, e.g. slice references (`&[T]`, `&str`). Such harnesses are + /// marked "(bounded)" in the output, and their verification results only hold up to the + /// bounds; a bug that requires a larger input will not be found. + #[arg(long)] + pub bounded_arguments: bool, + + /// Generate nondeterministic values for types without an Arbitrary implementation by + /// calling one of the type's own public constructors with nondeterministic arguments + /// (assuming the constructor succeeds). Such harnesses are marked "(ctor)" in the output, + /// and their verification results only cover values reachable through that constructor; + /// a bug that requires a different value will not be found. + #[arg(long)] + pub constructor_args: bool, + /// Run the `list` subcommand after generating the automatic harnesses. Note that this option implies --only-codegen. #[arg(long)] pub list: bool, diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 01904bb786d6..13d9b2fc9802 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -17,7 +17,7 @@ use crate::session::KaniSession; use crate::{InvocationType, print_kani_version, project, verify_project}; use anyhow::Result; use comfy_table::Table as PrettyTable; -use kani_metadata::{AutoHarnessSkipReason, KaniMetadata}; +use kani_metadata::{AutoHarnessSkipReason, HarnessMetadata, KaniMetadata}; const AUTOHARNESS_TIMEOUT: &str = "60s"; const LOOP_UNWIND_DEFAULT: u32 = 20; @@ -57,6 +57,7 @@ fn setup_session(session: &mut KaniSession, common_autoharness_args: &CommonAuto session.add_auto_harness_args( &common_autoharness_args.include_pattern, &common_autoharness_args.exclude_pattern, + common_autoharness_args.constructor_args, ); } @@ -161,7 +162,12 @@ impl KaniSession { } /// Add the compiler arguments specific to the `autoharness` subcommand. - pub fn add_auto_harness_args(&mut self, included: &[String], excluded: &[String]) { + pub fn add_auto_harness_args( + &mut self, + included: &[String], + excluded: &[String], + constructor_args: bool, + ) { let mut args = vec![]; for pattern in included { args.push(format!("--autoharness-include-pattern {pattern}")); @@ -169,6 +175,9 @@ impl KaniSession { for pattern in excluded { args.push(format!("--autoharness-exclude-pattern {pattern}")); } + if constructor_args { + args.push("--autoharness-constructor-args".to_string()); + } self.autoharness_compiler_flags = Some(args); } @@ -207,20 +216,31 @@ impl KaniSession { "Verification Result", ]); + let harness_kind = |harness: &HarnessMetadata| { + let mut kind = harness.attributes.kind.to_string(); + if harness.is_ctor_based { + kind.push_str(" (ctor)"); + } + kind + }; + let mut any_ctor = false; + for success in successes { + any_ctor |= success.harness.is_ctor_based; verified_fns.add_row(vec![ success.harness.crate_name.clone(), success.harness.pretty_name.clone(), - success.harness.attributes.kind.to_string(), + harness_kind(&success.harness), success.result.status.to_string(), ]); } for failure in failures { + any_ctor |= failure.harness.is_ctor_based; verified_fns.add_row(vec![ failure.harness.crate_name.clone(), failure.harness.pretty_name.clone(), - failure.harness.attributes.kind.to_string(), + harness_kind(&failure.harness), failure.result.status.to_string(), ]); } @@ -229,6 +249,13 @@ impl KaniSession { println!("{verified_fns}"); } + if any_ctor { + println!( + "Note: harnesses marked \"(ctor)\" generate some values through a type's public constructor (--constructor-args);\n\ + their verification results only cover values reachable through that constructor." + ); + } + if failing > 0 { println!( "Note that `kani autoharness` sets default --harness-timeout of {AUTOHARNESS_TIMEOUT} and --default-unwind of {LOOP_UNWIND_DEFAULT}." diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index ef9472f4a9cf..17295f8de2d0 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -172,6 +172,7 @@ pub mod tests { contract: Default::default(), has_loop_contracts: false, is_automatically_generated: false, + is_ctor_based: false, } } diff --git a/kani-driver/src/sarif.rs b/kani-driver/src/sarif.rs index 849c48c7c2db..4e5a2525ce3f 100644 --- a/kani-driver/src/sarif.rs +++ b/kani-driver/src/sarif.rs @@ -296,6 +296,7 @@ mod tests { contract: None, has_loop_contracts: false, is_automatically_generated: false, + is_ctor_based: false, } } diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 6c90dc269c92..556b65c7fa51 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -42,6 +42,11 @@ pub struct HarnessMetadata { pub has_loop_contracts: bool, /// If the harness was automatically generated or manually written. pub is_automatically_generated: bool, + /// Whether the (automatically generated) harness generates some values through a type's + /// public constructor (c.f. the autoharness --constructor-args option), in which case its + /// verification result only covers constructor-reachable values. + #[serde(default)] + pub is_ctor_based: bool, } /// The attributes added by the user to control how a harness is executed. diff --git a/tests/script-based-pre/cargo_autoharness_constructor/Cargo.toml b/tests/script-based-pre/cargo_autoharness_constructor/Cargo.toml new file mode 100644 index 000000000000..c9dde3e2d2eb --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_constructor/Cargo.toml @@ -0,0 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "cargo_autoharness_constructor" +version = "0.1.0" +edition = "2021" diff --git a/tests/script-based-pre/cargo_autoharness_constructor/config.yml b/tests/script-based-pre/cargo_autoharness_constructor/config.yml new file mode 100644 index 000000000000..6e5869b999ef --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_constructor/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: constructor.sh +expected: constructor.expected diff --git a/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected b/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected new file mode 100644 index 000000000000..f8d0f088bb95 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected @@ -0,0 +1,15 @@ +=== without flag === +| cargo_autoharness_constructor | Celsius::from_milli | #[kani::proof] | Success | +| cargo_autoharness_constructor | Celsius::get | #[kani::proof] | Success | +| cargo_autoharness_constructor | Day::new | #[kani::proof] | Success | +| cargo_autoharness_constructor | Day::ordinal0 | #[kani::proof] | Failure | +| cargo_autoharness_constructor | Even::half | #[kani::proof] | Failure | +| cargo_autoharness_constructor | Even::try_new | #[kani::proof] | Success | +=== with flag === +Note: harnesses marked "(ctor)" generate some values through a type's public constructor (--constructor-args); +| cargo_autoharness_constructor | Celsius::from_milli | #[kani::proof] | Success | +| cargo_autoharness_constructor | Celsius::get | #[kani::proof] (ctor) | Success | +| cargo_autoharness_constructor | Day::new | #[kani::proof] | Success | +| cargo_autoharness_constructor | Day::ordinal0 | #[kani::proof] (ctor) | Success | +| cargo_autoharness_constructor | Even::half | #[kani::proof] (ctor) | Success | +| cargo_autoharness_constructor | Even::try_new | #[kani::proof] | Success | diff --git a/tests/script-based-pre/cargo_autoharness_constructor/constructor.sh b/tests/script-based-pre/cargo_autoharness_constructor/constructor.sh new file mode 100755 index 000000000000..1a7861fe673e --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_constructor/constructor.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Without --constructor-args, raw field synthesis violates the private types' representation +# invariants and reports false alarms; with it, values are generated through the types' +# public constructors and the false alarms disappear (harnesses are marked "(ctor)"). +echo "=== without flag ===" +cargo kani autoharness -Z autoharness --output-format=regular 2>&1 \ + | grep -E '^\| cargo_autoharness_constructor \| .*(Success|Failure)' | tr -s ' ' | sort +echo "=== with flag ===" +cargo kani autoharness -Z autoharness --constructor-args --output-format=regular 2>&1 \ + | grep -E '^\| cargo_autoharness_constructor \| .*(Success|Failure)|Note: harnesses marked \"\(ctor\)\"' | tr -s ' ' | sort diff --git a/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs b/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs new file mode 100644 index 000000000000..d78b655c990e --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs @@ -0,0 +1,49 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Mimics time::Date: private packed field whose raw values violate the type invariant. +pub struct Day { + value: u16, // invariant: 1..=366 +} + +impl Day { + pub fn new(d: u16) -> Option { + if d >= 1 && d <= 366 { Some(Day { value: d }) } else { None } + } + + // Without --constructor-args, raw field synthesis reaches the debug_assert-style branch + // below and reports a false alarm; with it, only valid Days are generated. + pub fn ordinal0(&self) -> u16 { + assert!(self.value >= 1, "invariant violated"); + self.value - 1 + } +} + +// Direct-returning constructor case. +pub struct Celsius { + milli: i32, +} + +impl Celsius { + pub fn from_milli(m: i32) -> Celsius { + Celsius { milli: m } + } + pub fn get(&self) -> i32 { + self.milli + } +} + +// Result-returning constructor case. +pub struct Even { + n: u32, +} + +impl Even { + pub fn try_new(n: u32) -> Result { + if n % 2 == 0 { Ok(Even { n }) } else { Err(()) } + } + pub fn half(&self) -> u32 { + assert!(self.n % 2 == 0); + self.n / 2 + } +} From 47f83f86523a76bef979d39e819c8b2955a18588 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 5 Aug 2026 15:53:13 +0000 Subject: [PATCH 3/4] Autoharness: mine constructor assertions into value filters Extend --constructor-args with assert mining: prefer assert-guarded representation constructors (unsafe / doc-hidden / _unchecked-named, returning Self; generic ADTs instantiated with their own args), inlined into the synthesized kani::any body with every validity statement converted into a filter on the nondeterministic arguments: - kani::assert(cond, msg) calls (Kani's macro overrides have already rewritten user asserts/panics into these) -> kani::assume(cond); - hint::assert_unchecked(cond) (UB-hint contracts, e.g. deranged's new_unchecked) -> kani::assume(cond); - raw panic-entry calls -> assume(false) + unreachable; - MIR Assert terminators (overflow checks) -> assume(cond == expected). Calls within the inlined body whose callees contain such validity statements are recursively inlined (depth <= 3, <= 32 blocks per callee, plain-call fallback), covering nested patterns like time's Time::__from_hms_nanos_unchecked calling deranged's new_unchecked. Such a constructor is typically the raw representation builder whose asserts state the type's validity contract exactly, and is surjective onto the valid value space; the generated set is then precisely the values passing the type's own validity assertions. New MutableBody primitives push_raw_bb/split_with_terminator support the inlining; a whitelist remapper bails out (falling back to checked-constructor generation) on unsupported constructs. Measured on time-0.3.54 (vs. 341 ok / 500 fail baseline): checked-ctor assumption 538/315; hand-written invariants 490/363; assert mining 595/258 (251 fixed, 8 broke -- predominantly CBMC 60s-timeouts from formula growth, a logged refinement). Co-authored-by: Kiro --- .../src/kani_middle/transform/automatic.rs | 482 +++++++++++++++++- .../src/kani_middle/transform/body.rs | 22 + .../constructor.expected | 6 + .../cargo_autoharness_constructor/src/lib.rs | 34 ++ 4 files changed, 536 insertions(+), 8 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index b48febcd8df1..d87a5a775184 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -22,9 +22,10 @@ use rustc_middle::ty::TyCtxt; use rustc_public::CrateDef; use rustc_public::mir::mono::Instance; use rustc_public::mir::{ - AggregateKind, BasicBlockIdx, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, - MutBorrowKind, Mutability, Operand, Place, ProjectionElem, Rvalue, SwitchTargets, Terminator, - TerminatorKind, + AggregateKind, BasicBlock, BasicBlockIdx, BinOp, Body, BorrowKind, CastKind, ConstOperand, + Local, MutBorrowKind, Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, + Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, UnOp, + UnwindAction, }; use rustc_public::ty::{ AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyKind, UintTy, @@ -42,6 +43,9 @@ pub struct AutomaticArbitraryPass { /// The FnDef of KaniHook::Assume (used for layout-niche assumptions and constructor /// success). kani_assume: FnDef, + /// The FnDef of KaniHook::Assert (rewritten into assumptions when inlining + /// assert-guarded constructors). + kani_assert: FnDef, /// Whether --constructor-args is enabled: generate values of private-field types through /// their public constructors instead of raw field synthesis. constructor_args: bool, @@ -52,8 +56,9 @@ impl AutomaticArbitraryPass { let kani_fns = query_db.kani_functions(); let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap(); let kani_assume = *kani_fns.get(&KaniHook::Assume.into()).unwrap(); + let kani_assert = *kani_fns.get(&KaniHook::Assert.into()).unwrap(); let constructor_args = query_db.args().autoharness_constructor_args; - Self { kani_any, kani_assume, constructor_args } + Self { kani_any, kani_assume, kani_assert, constructor_args } } } @@ -135,11 +140,28 @@ impl TransformPass for AutomaticArbitraryPass { if self.constructor_args && def.kind() == AdtKind::Struct && adt_has_private_field_check(tcx, def) - && let Some((ctor, shape)) = - find_arbitrary_constructor(tcx, *ty, self.kani_any, &mut FxHashMap::default()) { - debug!(?ty, ctor=?ctor.name(), ?shape, "generate_ctor_body"); - return (true, self.generate_ctor_body(tcx, ctor, shape, *ty, body)); + // Prefer assert-guarded representation constructors, inlined with panic + // paths converted to assumptions: their own assertions state the type's + // validity contract, and they are typically surjective onto the valid value + // space (unlike checked constructors, which may reach only a subset). + if let Some(ctor) = crate::kani_middle::find_unchecked_constructor( + tcx, + *ty, + self.kani_any, + &mut FxHashMap::default(), + ) && let Some(new_body) = + self.generate_unchecked_ctor_body(tcx, ctor, *ty, body.clone()) + { + debug!(?ty, ctor=?ctor.name(), "generate_unchecked_ctor_body"); + return (true, new_body); + } + if let Some((ctor, shape)) = + find_arbitrary_constructor(tcx, *ty, self.kani_any, &mut FxHashMap::default()) + { + debug!(?ty, ctor=?ctor.name(), ?shape, "generate_ctor_body"); + return (true, self.generate_ctor_body(tcx, ctor, shape, *ty, body)); + } } match def.kind() { AdtKind::Enum => (true, self.generate_enum_body(tcx, def, args, body)), @@ -154,6 +176,393 @@ impl TransformPass for AutomaticArbitraryPass { /// Insert a call to kani::any::() in `body`; return the local storing the result. /// Panics if `ty` does not implement Arbitrary. +/// Remap all locals and block targets of an inlined basic block. Returns false (bail out) +/// when the block contains a construct the remapper does not support; the caller then falls +/// back to non-inlined generation. The whitelist covers everything rustc emits for +/// assert-guarded field-packing constructors (the C14 mining target). +fn remap_block(bb: &mut BasicBlock, local_map: &[Local], block_offset: usize) -> bool { + let remap_place = |p: &mut Place| { + p.local = local_map[p.local]; + for elem in p.projection.iter_mut() { + if let ProjectionElem::Index(l) = elem { + *l = local_map[*l]; + } + } + }; + let remap_operand = |op: &mut Operand| match op { + Operand::Copy(p) | Operand::Move(p) => remap_place(p), + Operand::Constant(_) | Operand::RuntimeChecks(_) => {} + }; + for stmt in bb.statements.iter_mut() { + match &mut stmt.kind { + StatementKind::Assign(place, rvalue) => { + remap_place(place); + match rvalue { + Rvalue::Use(op) | Rvalue::Repeat(op, _) | Rvalue::Cast(_, op, _) => { + remap_operand(op) + } + Rvalue::BinaryOp(_, a, b) | Rvalue::CheckedBinaryOp(_, a, b) => { + remap_operand(a); + remap_operand(b); + } + Rvalue::UnaryOp(_, op) => remap_operand(op), + Rvalue::Ref(_, _, p) + | Rvalue::AddressOf(_, p) + | Rvalue::CopyForDeref(p) + | Rvalue::Discriminant(p) + | Rvalue::Len(p) => remap_place(p), + Rvalue::Aggregate(_, ops) => ops.iter_mut().for_each(remap_operand), + Rvalue::ShallowInitBox(op, _) => remap_operand(op), + Rvalue::ThreadLocalRef(_) => return false, + } + } + StatementKind::StorageLive(l) | StatementKind::StorageDead(l) => { + *l = local_map[*l]; + } + StatementKind::SetDiscriminant { place, .. } + | StatementKind::PlaceMention(place) + | StatementKind::FakeRead(_, place) => remap_place(place), + StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(op)) => remap_operand(op), + StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(cp)) => { + remap_operand(&mut cp.src); + remap_operand(&mut cp.dst); + remap_operand(&mut cp.count); + } + StatementKind::AscribeUserType { .. } + | StatementKind::Coverage(_) + | StatementKind::ConstEvalCounter + | StatementKind::Retag(..) + | StatementKind::Nop => {} + } + } + match &mut bb.terminator.kind { + TerminatorKind::Goto { target } => *target += block_offset, + TerminatorKind::SwitchInt { discr, targets } => { + remap_operand(discr); + let branches: Vec<_> = targets.branches().map(|(v, t)| (v, t + block_offset)).collect(); + *targets = SwitchTargets::new(branches, targets.otherwise() + block_offset); + } + TerminatorKind::Call { func, args, destination, target, .. } => { + remap_operand(func); + args.iter_mut().for_each(remap_operand); + remap_place(destination); + if let Some(t) = target { + *t += block_offset; + } + } + TerminatorKind::Assert { cond, target, .. } => { + remap_operand(cond); + *target += block_offset; + } + TerminatorKind::Drop { place, target, .. } => { + remap_place(place); + *target += block_offset; + } + TerminatorKind::Return + | TerminatorKind::Unreachable + | TerminatorKind::Resume + | TerminatorKind::Abort => {} + TerminatorKind::InlineAsm { .. } => return false, + } + true +} + +/// C14 (assert mining, dynamic form): inline `callee`'s monomorphic body into `body` at +/// `source`, with every validity statement converted into a filter on the nondeterministic +/// inputs: +/// - `kani::assert(cond, msg)` calls (Kani's macro overrides have already rewritten user +/// asserts/panics into these) become `kani::assume(cond)`; +/// - `hint::assert_unchecked(cond)` calls (UB-hint contracts, e.g. deranged's +/// `new_unchecked`) become `kani::assume(cond)`; +/// - raw panic-entry calls become `assume(false); unreachable`; +/// - MIR `Assert` terminators (overflow checks) become `assume(cond == expected)`. +/// +/// Calls *within* the inlined body whose callees themselves contain such validity statements +/// (e.g. time's `Time::__from_hms_nanos_unchecked` calling deranged's `new_unchecked`) are +/// recursively inlined, up to [INLINE_MAX_DEPTH] levels and [INLINE_MAX_BLOCKS] blocks per +/// callee; other calls are kept as plain calls. +/// +/// `arg_locals` must hold fully-initialized constructor arguments. Returns the local holding +/// the constructed value, or None (caller falls back to a plain call) if the outer callee +/// body contains unsupported constructs. (A bail-out mid-way leaves only unused locals +/// behind, which is harmless.) +const INLINE_MAX_DEPTH: usize = 3; +const INLINE_MAX_BLOCKS: usize = 32; + +fn inline_with_assumed_panics( + tcx: TyCtxt, + kani_assume: FnDef, + kani_assert: FnDef, + body: &mut MutableBody, + source: &mut SourceInstruction, + callee: Instance, + arg_locals: &[Local], + ret_ty: Ty, +) -> Option { + let callee_body = callee.body()?; + let span = source.span(body.blocks()); + let ret_lcl = body.new_local(ret_ty, span, Mutability::Mut); + + // All blocks from `block_offset` onward are planned into `planned`; slots are allocated + // (possibly ahead of being filled) so that nested inlining can interleave with the outer + // walk without breaking target indices. + let continuation = body.blocks().len(); + let block_offset = continuation + 1; + let assume_inst = Instance::resolve(kani_assume, &GenericArgs(vec![])).unwrap(); + + struct Ctx<'tcx, 'a> { + tcx: TyCtxt<'tcx>, + kani_assert: FnDef, + assume_inst: Instance, + body: &'a mut MutableBody, + planned: Vec>, + block_offset: usize, + span: rustc_public::ty::Span, + } + + impl Ctx<'_, '_> { + fn alloc(&mut self, n: usize) -> usize { + let base = self.block_offset + self.planned.len(); + self.planned.extend(std::iter::repeat_with(|| None).take(n)); + base + } + + fn set(&mut self, idx: usize, bb: BasicBlock) { + self.planned[idx - self.block_offset] = Some(bb); + } + + fn assume_call_terminator( + &mut self, + cond: Operand, + target: BasicBlockIdx, + ) -> TerminatorKind { + let func_lcl = self.body.new_local(self.assume_inst.ty(), self.span, Mutability::Not); + let unit_lcl = self.body.new_local(Ty::new_tuple(&[]), self.span, Mutability::Mut); + TerminatorKind::Call { + func: Operand::Copy(Place::from(func_lcl)), + args: vec![cond], + destination: Place::from(unit_lcl), + target: Some(target), + unwind: UnwindAction::Terminate, + } + } + + /// Does `fn_body` directly contain a validity statement worth mining? + fn worth_inlining(&self, fn_body: &Body) -> bool { + fn_body.blocks.iter().any(|bb| match &bb.terminator.kind { + TerminatorKind::Assert { .. } => true, + TerminatorKind::Call { func, .. } => { + match func.ty(fn_body.locals()).map(|t| t.kind()) { + Ok(TyKind::RigidTy(RigidTy::FnDef(def, _))) => { + def == self.kani_assert + || def.name().contains("assert_unchecked") + || is_panic_def(self.tcx, def) + } + _ => false, + } + } + _ => false, + }) + } + + /// Plan `fn_body` (of `n` blocks) into slots `base..base+n`, remapping via + /// `local_map`, converting validity statements, recursively inlining qualifying + /// callees. Returns false to bail out (unsupported construct at depth 0; at deeper + /// levels callers pre-check with `worth_inlining` and blocks are conservative). + fn plan_body( + &mut self, + fn_body: &Body, + local_map: &[Local], + base: usize, + ret_target: BasicBlockIdx, + depth: usize, + ) -> bool { + for (i, callee_bb) in fn_body.blocks.iter().enumerate() { + let mut bb = callee_bb.clone(); + if !remap_block(&mut bb, local_map, base) { + return false; + } + match &mut bb.terminator.kind { + TerminatorKind::Return => { + bb.terminator.kind = TerminatorKind::Goto { target: ret_target }; + } + TerminatorKind::Resume | TerminatorKind::Abort => { + bb.terminator.kind = TerminatorKind::Unreachable; + } + TerminatorKind::Assert { cond, expected, target, .. } => { + let (cond, expected, target) = (cond.clone(), *expected, *target); + let cond_lcl = + self.body.new_local(Ty::bool_ty(), self.span, Mutability::Mut); + let rv = if expected { + Rvalue::Use(cond) + } else { + Rvalue::UnaryOp(UnOp::Not, cond) + }; + bb.statements.push(Statement { + kind: StatementKind::Assign(Place::from(cond_lcl), rv), + span: self.span, + }); + bb.terminator.kind = self + .assume_call_terminator(Operand::Move(Place::from(cond_lcl)), target); + } + TerminatorKind::Call { func, args, destination, target, .. } => { + let fn_def = match func.ty(self.body.locals()).map(|t| t.kind()) { + Ok(TyKind::RigidTy(RigidTy::FnDef(def, fn_args))) => { + Some((def, fn_args)) + } + _ => None, + }; + if let Some((def, _)) = &fn_def + && (*def == self.kani_assert || def.name().contains("assert_unchecked")) + { + // kani::assert(cond, msg) / assert_unchecked(cond) -> assume(cond) + let cond = args[0].clone(); + let target = target.expect("assert has a return target"); + bb.terminator.kind = self.assume_call_terminator(cond, target); + } else if let Some((def, _)) = &fn_def + && is_panic_def(self.tcx, *def) + { + // panic -> assume(false); unreachable + let unreach = self.alloc(1); + self.set( + unreach, + BasicBlock { + statements: vec![], + terminator: Terminator { + kind: TerminatorKind::Unreachable, + span: self.span, + }, + }, + ); + let false_op = Operand::Constant(ConstOperand { + span: self.span, + user_ty: None, + const_: MirConst::from_bool(false), + }); + bb.terminator.kind = self.assume_call_terminator(false_op, unreach); + } else if depth < INLINE_MAX_DEPTH + && let Some((def, fn_args)) = &fn_def + && let Ok(inst) = Instance::resolve(*def, fn_args) + && let Some(inner_body) = inst.body() + && inner_body.blocks.len() <= INLINE_MAX_BLOCKS + && self.worth_inlining(&inner_body) + { + // Recursively inline: materialize args into fresh locals, + // stitch the return value into the call's destination. + let target = target.expect("inlined callee has a return target"); + let inner_ret_ty = inner_body.locals()[0].ty; + let inner_ret_lcl = + self.body.new_local(inner_ret_ty, self.span, Mutability::Mut); + let mut inner_map = vec![inner_ret_lcl]; + for (arg_op, decl) in args.iter().zip(inner_body.arg_locals().iter()) { + let a = self.body.new_local(decl.ty, self.span, Mutability::Mut); + bb.statements.push(Statement { + kind: StatementKind::Assign( + Place::from(a), + Rvalue::Use(arg_op.clone()), + ), + span: self.span, + }); + inner_map.push(a); + } + for decl in inner_body.locals().iter().skip(1 + args.len()) { + inner_map.push(self.body.new_local( + decl.ty, + self.span, + Mutability::Mut, + )); + } + let stitch = self.alloc(1); + let inner_base = self.alloc(inner_body.blocks.len()); + self.set( + stitch, + BasicBlock { + statements: vec![Statement { + kind: StatementKind::Assign( + destination.clone(), + Rvalue::Use(Operand::Move(Place::from(inner_ret_lcl))), + ), + span: self.span, + }], + terminator: Terminator { + kind: TerminatorKind::Goto { target }, + span: self.span, + }, + }, + ); + if self.plan_body( + &inner_body, + &inner_map, + inner_base, + stitch, + depth + 1, + ) { + bb.terminator.kind = TerminatorKind::Goto { target: inner_base }; + } else { + // Nested bail-out: keep the plain call; fill the reserved + // slots with unreachable stubs (never targeted). + for j in 0..inner_body.blocks.len() { + if self.planned[inner_base + j - self.block_offset].is_none() { + self.set( + inner_base + j, + BasicBlock { + statements: vec![], + terminator: Terminator { + kind: TerminatorKind::Unreachable, + span: self.span, + }, + }, + ); + } + } + } + } + // else: keep the plain (already remapped) call. + } + _ => {} + } + self.set(base + i, bb); + } + true + } + } + + // Map callee locals: _0 -> ret_lcl, _1..=argc -> arg_locals, rest -> fresh. + let mut local_map: Vec = Vec::with_capacity(callee_body.locals().len()); + local_map.push(ret_lcl); + let argc = callee_body.arg_locals().len(); + assert_eq!(argc, arg_locals.len()); + local_map.extend_from_slice(arg_locals); + for decl in callee_body.locals().iter().skip(1 + argc) { + local_map.push(body.new_local(decl.ty, span, Mutability::Mut)); + } + + let mut ctx = Ctx { tcx, kani_assert, assume_inst, body, planned: vec![], block_offset, span }; + let outer_base = ctx.alloc(callee_body.blocks.len()); + if !ctx.plan_body(&callee_body, &local_map, outer_base, continuation, 0) { + return None; + } + let planned = ctx.planned; + + // Commit: split the caller and append all planned blocks at their precomputed indices. + let placeholder = Terminator { kind: TerminatorKind::Goto { target: outer_base }, span }; + let (_goto_bb, actual_continuation) = body.split_with_terminator(source, placeholder); + assert_eq!(actual_continuation, continuation); + for bb in planned { + body.push_raw_bb(bb.expect("all planned slots must be filled")); + } + Some(ret_lcl) +} + +/// Whether `def` is a panic entry point. +fn is_panic_def(tcx: TyCtxt, def: FnDef) -> bool { + let def_id = rustc_public::rustc_internal::internal(tcx, def.def_id()); + Some(def_id) == tcx.lang_items().panic_fn() + || Some(def_id) == tcx.lang_items().panic_fmt() + || Some(def_id) == tcx.lang_items().begin_panic_fn() + || def.name().starts_with("core::panicking::") +} + /// If `ty` has a scalar layout with a restricted valid range (a niche), append /// `kani::assume( in valid_range)`. /// Values outside the niche are language-level invalid (rustc packs enum variants into the @@ -331,6 +740,63 @@ impl AutomaticArbitraryPass { source.bb() - (fields.len() + 1) } + /// Overwrite the default `kani::any()` implementation `body` for a struct with private + /// fields by inlining an assert-guarded representation constructor with nondeterministic + /// arguments and panic paths converted into assumptions + /// (c.f. [find_unchecked_constructor][crate::kani_middle::find_unchecked_constructor]). + /// Returns None if the constructor body contains constructs the inliner does not support. + fn generate_unchecked_ctor_body( + &self, + tcx: TyCtxt, + ctor: Instance, + ty: Ty, + body: Body, + ) -> Option { + let mut new_body = MutableBody::from(body); + new_body.clear_body(TerminatorKind::Unreachable); + let mut source = SourceInstruction::Terminator { bb: 0 }; + let ctor_sig = ctor.ty().kind().fn_sig().unwrap().skip_binder(); + let arg_locals: Vec = ctor_sig + .inputs() + .iter() + .map(|input_ty| { + call_kani_any_for_ty( + tcx, + self.kani_any, + self.kani_assume, + &mut new_body, + *input_ty, + Mutability::Not, + &mut source, + ) + }) + .collect(); + let ret_lcl = inline_with_assumed_panics( + tcx, + self.kani_assume, + self.kani_assert, + &mut new_body, + &mut source, + ctor, + &arg_locals, + ty, + )?; + // RETURN_LOCAL = move ret; return + new_body.assign_to( + Place::from(0), + Rvalue::Use(Operand::Move(Place::from(ret_lcl))), + &mut source, + InsertPosition::Before, + ); + let span = source.span(new_body.blocks()); + new_body.insert_terminator( + &mut source, + InsertPosition::Before, + Terminator { kind: TerminatorKind::Return, span }, + ); + Some(new_body.into()) + } + /// Overwrite the default `kani::any()` implementation `body` for a struct with private /// fields by calling a public constructor with nondeterministic arguments /// (`--constructor-args`). The returned body is equivalent to: diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 9d36caadcd73..360aa3829ef5 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -359,6 +359,28 @@ impl MutableBody { self.split_bb(source, position, terminator); } + /// Append a fully-formed basic block (whose targets the caller has already remapped into + /// this body's index space) and return its index. Building block for inlining callee + /// bodies, c.f. `automatic::inline_with_assumed_panics`. + pub fn push_raw_bb(&mut self, bb: BasicBlock) -> BasicBlockIdx { + self.blocks.push(bb); + self.blocks.len() - 1 + } + + /// Split the block at `source`, terminating the first half with `terminator` (whose + /// targets may still be placeholders), and return (index of the terminator's block, + /// index of the remainder block). Building block for inlining callee bodies. + pub fn split_with_terminator( + &mut self, + source: &mut SourceInstruction, + terminator: Terminator, + ) -> (BasicBlockIdx, BasicBlockIdx) { + let remainder_idx = self.blocks.len(); + let term_bb_idx = source.bb(); + self.split_bb(source, InsertPosition::Before, terminator); + (term_bb_idx, remainder_idx) + } + /// Insert statement before or after the source instruction and update the source as needed. If /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the diff --git a/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected b/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected index f8d0f088bb95..6d34194a2e6c 100644 --- a/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected +++ b/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected @@ -5,6 +5,9 @@ | cargo_autoharness_constructor | Day::ordinal0 | #[kani::proof] | Failure | | cargo_autoharness_constructor | Even::half | #[kani::proof] | Failure | | cargo_autoharness_constructor | Even::try_new | #[kani::proof] | Success | +| cargo_autoharness_constructor | Ranged::new_unchecked | #[kani::proof] | Failure | +| cargo_autoharness_constructor | Wrapper::from_raw_unchecked | #[kani::proof] | Failure | +| cargo_autoharness_constructor | wrapped_ordinal0 | #[kani::proof] | Failure | === with flag === Note: harnesses marked "(ctor)" generate some values through a type's public constructor (--constructor-args); | cargo_autoharness_constructor | Celsius::from_milli | #[kani::proof] | Success | @@ -13,3 +16,6 @@ Note: harnesses marked "(ctor)" generate some values through a type's public con | cargo_autoharness_constructor | Day::ordinal0 | #[kani::proof] (ctor) | Success | | cargo_autoharness_constructor | Even::half | #[kani::proof] (ctor) | Success | | cargo_autoharness_constructor | Even::try_new | #[kani::proof] | Success | +| cargo_autoharness_constructor | Ranged::new_unchecked | #[kani::proof] | Failure | +| cargo_autoharness_constructor | Wrapper::from_raw_unchecked | #[kani::proof] | Failure | +| cargo_autoharness_constructor | wrapped_ordinal0 | #[kani::proof] (ctor) | Success | diff --git a/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs b/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs index d78b655c990e..b228bac1014a 100644 --- a/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs @@ -47,3 +47,37 @@ impl Even { self.n / 2 } } + +// Assert-guarded representation constructors (unsafe/doc-hidden/_unchecked) are inlined +// with their validity assertions converted into filters — including one level of nesting +// (Wrapper's ctor calls Ranged's). +pub struct Ranged { + value: u16, // invariant 1..=366, stated by new_unchecked's debug_asserts +} + +impl Ranged { + #[doc(hidden)] + pub const fn new_unchecked(v: u16) -> Ranged { + debug_assert!(v >= 1); + debug_assert!(v <= 366); + Ranged { value: v } + } +} + +pub struct Wrapper { + inner: Ranged, +} + +impl Wrapper { + #[doc(hidden)] + pub const fn from_raw_unchecked(v: u16) -> Wrapper { + Wrapper { inner: Ranged::new_unchecked(v) } + } +} + +// TEST NOTE: should PASS with --constructor-args (the nested debug_asserts filter the +// generated values); FAILS without. +pub fn wrapped_ordinal0(w: Wrapper) -> u16 { + assert!(w.inner.value >= 1, "invariant violated"); + w.inner.value - 1 +} From 08a000cec3231dc9cb4bb3f423251a1ac1821556 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 6 Aug 2026 09:24:09 +0000 Subject: [PATCH 4/4] Autoharness: unbounded slice, mutable slice and Vec arguments Arguments of type &[T], &mut [T] and Vec whose element type is a primitive integer or float are now supported, generated UNBOUNDED: the new optional (alloc-requiring) models allocate nondeterministic-size storage, so verification results hold for ALL lengths. Functions that iterate over the data surface insufficient loop bounds as visible unwinding-assertion failures rather than silently bounded successes. Mutable slices are exclusive by construction (each call leaks a fresh allocation); Vec uses from_raw_parts with capacity matching the allocation layout and frees on drop (ZST elements use the documented dangling-pointer pattern, loop-free). Element types are restricted to those where raw nondeterministic memory needs NO validity assumption (every bit pattern valid): the companion SliceValidityAssume hook, lowered directly to pure quantified goto expressions, exists for niched element types (bool, NonZero*), but CBMC's SAT backend only instantiates constant-bound quantifiers and silently drops symbolic-bound ones (see #4719), so those element types remain unsupported until the in-progress CBMC quantifier work lands. Co-authored-by: Kiro --- .../codegen_cprover_gotoc/overrides/hooks.rs | 89 ++++++++++++++++ .../src/kani_middle/codegen_units.rs | 21 ++++ .../src/kani_middle/kani_functions.rs | 24 ++++- kani-compiler/src/kani_middle/mod.rs | 47 ++++++++ .../src/kani_middle/transform/automatic.rs | 74 ++++++++++++- library/kani/src/arbitrary.rs | 100 ++++++++++++++++++ .../Cargo.toml | 6 ++ .../config.yml | 5 + .../src/lib.rs | 35 ++++++ .../vec.expected | 9 ++ .../cargo_autoharness_vec_unbounded/vec.sh | 5 + 11 files changed, 411 insertions(+), 4 deletions(-) create mode 100644 tests/script-based-pre/cargo_autoharness_vec_unbounded/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoharness_vec_unbounded/config.yml create mode 100644 tests/script-based-pre/cargo_autoharness_vec_unbounded/src/lib.rs create mode 100644 tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.expected create mode 100755 tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.sh diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 6790c5642c8d..5063cf3622a9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -899,6 +899,94 @@ impl GotocHook for LoopInvariantRegister { } } +/// Lower `kani::slice_validity_assume::(ptr, len)` (KaniHook::SliceValidityAssume) to a +/// quantified assumption constraining every element's raw bits to `T`'s layout niche: +/// `assume(forall i. i < len ==> lo <= *(uN*)ptr + i <= hi)` (wrapping ranges use `||`). +/// A no-op for element types without a niche (every bit pattern valid). +/// +/// This is lowered directly to pure goto expressions rather than through `kani::forall!`: +/// the closure-based quantifier lowering cannot substitute bodies containing checked +/// arithmetic or bounds checks (it falls back to an unconstrained predicate), whereas the +/// expressions built here are side-effect-free by construction. +struct SliceValidityAssume; +impl GotocHook for SliceValidityAssume { + fn hook_applies( + &self, + _tcx: TyCtxt, + _instance: Instance, + _instance_name: &str, + _kani_tool_attr: Option<&String>, + ) -> bool { + unreachable!("{UNEXPECTED_CALL}") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + instance: Instance, + mut fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 2); + let loc = gcx.codegen_span_stable(span); + let target = target.unwrap(); + let goto_target = Stmt::goto(bb_label(target), loc); + + let elem_ty = instance.args().0[0].expect_ty().to_owned(); + let Some(niche) = crate::kani_middle::scalar_niche(gcx.tcx, elem_ty) else { + // Every bit pattern is valid: nothing to assume. + return goto_target; + }; + let len = fargs.remove(1); + let ptr = fargs.remove(0); + + // Fresh quantified variable of the same type as `len`. + let base_name = "kani_slice_validity_var".to_string(); + let mut counter = 0; + let mut unique_name = format!("{base_name}_{counter}"); + while gcx.symbol_table.lookup(&unique_name).is_some() { + counter += 1; + unique_name = format!("{base_name}_{counter}"); + } + let qvar = { + let sym = + GotoSymbol::variable(unique_name.clone(), unique_name, len.typ().clone(), loc); + gcx.symbol_table.insert(sym.clone()); + sym.to_expr() + }; + + // CBMC's quantifier handling binds byte-granularity dereferences reliably, but not + // wider ones (byte_extract at a symbolic index under a forall does not propagate), + // so the validity predicate is expressed over bytes: + // - 8-bit niches (bool, u8-based ranged types): direct range check on the byte; + // - NonZero-style niches (excluded zero, full top): OR over "some byte nonzero". + // Wider general ranges are not byte-decomposable this simply; the element classifier + // (kani_middle::slice_elem_unbounded_ok) never routes such types to this hook. + let byte_ty = Type::unsigned_int(8u64); + let byte_ptr = ptr.clone().cast_to(byte_ty.clone().to_pointer()); + let valid = if niche.bits == 8 { + let elem = byte_ptr.plus(qvar.clone()).dereference(); + let lo = Expr::int_constant(niche.start, byte_ty.clone()); + let hi = Expr::int_constant(niche.end, byte_ty.clone()); + if niche.start <= niche.end { + lo.le(elem.clone()).and(elem.le(hi)) + } else { + lo.le(elem.clone()).or(elem.le(hi)) + } + } else { + unreachable!( + "slice_validity_assume: element type with non-byte-decomposable niche should have been rejected by the classifier" + ) + }; + let domain = qvar.clone().lt(len).implies(valid); + let quantified = Expr::forall_expr(Type::Bool, qvar, domain); + + Stmt::block(vec![gcx.codegen_assume(quantified, loc), goto_target], loc) + } +} + struct Forall; struct Exists; @@ -1339,6 +1427,7 @@ pub fn fn_hooks() -> GotocHooks { let kani_lib_hooks = [ (KaniHook::Assert, Rc::new(Assert) as Rc), (KaniHook::Assume, Rc::new(Assume)), + (KaniHook::SliceValidityAssume, Rc::new(SliceValidityAssume)), (KaniHook::Exists, Rc::new(Exists)), (KaniHook::Forall, Rc::new(Forall)), (KaniHook::Panic, Rc::new(Panic)), diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 573318df568e..959d84c60660 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -103,6 +103,7 @@ impl CodegenUnits { args, &crate_info.name, *kani_fns.get(&KaniModel::Any.into()).unwrap(), + kani_fns.contains_key(&KaniModel::AnySliceRefUnbounded.into()), ); AUTOHARNESS_MD .set(AutoHarnessMetadata { @@ -420,6 +421,7 @@ fn automatic_harness_partition( args: &Arguments, crate_name: &str, kani_any_def: FnDef, + unbounded_slice_available: bool, ) -> (Vec<(Instance, bool)>, BTreeMap) { let crate_fn_defs = rustc_public::local_crate().fn_defs().into_iter().collect::>(); // Filter out CrateItems that are functions, but not functions defined in the crate itself, i.e., rustc-inserted functions @@ -481,6 +483,25 @@ fn automatic_harness_partition( // Note that we've already filtered out generic functions, so we know that each of these arguments has a concrete type. let mut problematic_args = vec![]; for (idx, arg) in body.arg_locals().iter().enumerate() { + // Unbounded generation: slices (&[T], &mut [T]) and Vec of primitive + // integer/float elements are generated as fresh allocations of + // nondeterministic size (results hold for all lengths), when the optional + // alloc-requiring models are present. + if unbounded_slice_available { + let slice_ok = match arg.ty.kind() { + TyKind::RigidTy(RigidTy::Ref(_, inner, _)) => match inner.kind() { + TyKind::RigidTy(RigidTy::Slice(elem)) => { + crate::kani_middle::slice_elem_unbounded_ok(tcx, elem) + } + _ => false, + }, + _ => crate::kani_middle::vec_elem_ty(arg.ty) + .is_some_and(|elem| crate::kani_middle::slice_elem_unbounded_ok(tcx, elem)), + }; + if slice_ok { + continue; + } + } if !ty_arbitrary_cache.contains_key(&arg.ty) { let impls_arbitrary = implements_arbitrary(arg.ty, kani_any_def, &mut ty_arbitrary_cache) diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index d5b97aa5406c..28889e57814d 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -65,6 +65,12 @@ pub enum KaniModel { AlignOfDynObject, #[strum(serialize = "AlignOfValRawModel")] AlignOfVal, + #[strum(serialize = "AnySliceMutUnboundedModel")] + AnySliceMutUnbounded, + #[strum(serialize = "AnySliceRefUnboundedModel")] + AnySliceRefUnbounded, + #[strum(serialize = "AnyVecUnboundedModel")] + AnyVecUnbounded, #[strum(serialize = "AnyModel")] Any, #[strum(serialize = "CopyInitStateModel")] @@ -129,6 +135,8 @@ pub enum KaniHook { AnyRaw, #[strum(serialize = "AssertHook")] Assert, + #[strum(serialize = "SliceValidityAssumeHook")] + SliceValidityAssume, #[strum(serialize = "AssumeHook")] Assume, #[strum(serialize = "CheckHook")] @@ -162,6 +170,20 @@ pub enum KaniHook { UntrackedDeref, } +impl KaniModel { + /// Whether this model may legitimately be absent. These models require `alloc` and are + /// only defined in the `kani` library, not in `core::kani` (the `no_core` flow used by + /// `kani verify-std`). Code retrieving optional models must handle their absence. + pub fn is_optional(&self) -> bool { + matches!( + self, + KaniModel::AnySliceMutUnbounded + | KaniModel::AnySliceRefUnbounded + | KaniModel::AnyVecUnbounded + ) + } +} + impl From for KaniFunction { fn from(value: KaniIntrinsic) -> Self { KaniFunction::Intrinsic(value) @@ -271,7 +293,7 @@ pub fn validate_kani_functions(kani_funcs: &HashMap) { { if let Some(fn_def) = kani_funcs.get(&func) { assert_eq!(KaniFunction::try_from(*fn_def), Ok(func), "Unexpected function marker"); - } else { + } else if !matches!(func, KaniFunction::Model(model) if model.is_optional()) { tracing::error!(?func, "Missing kani function"); missing += 1; } diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 858bb88c769a..710f4131da84 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -600,6 +600,53 @@ fn to_fn_def(tcx: TyCtxt, def_id: rustc_span::def_id::DefId) -> Option { } } +/// If `ty` is `Vec` with the default allocator, return `T`. +pub fn vec_elem_ty(ty: Ty) -> Option { + let TyKind::RigidTy(RigidTy::Adt(def, ref args)) = ty.kind() else { return None }; + let name = def.name(); + if name != "std::vec::Vec" && name != "alloc::vec::Vec" { + return None; + } + // Vec: only the default allocator is supported (the model allocates via + // the global allocator). The allocator parameter is defaulted, so a crate naming a + // custom allocator produces a second type argument != Global. + let mut ty_args = args.0.iter().filter_map(|a| match a { + GenericArgKind::Type(t) => Some(*t), + _ => None, + }); + let elem = ty_args.next()?; + if let Some(alloc_ty) = ty_args.next() + && !alloc_ty.to_string().contains("Global") + { + return None; + } + Some(elem) +} + +/// Whether `&[T]` arguments with this element type qualify for *unbounded* generation +/// (`KaniModel::AnySliceRefUnbounded`): raw nondeterministic memory must be a sound AND +/// complete model of the element's values *without any validity assumption*, i.e. every bit +/// pattern must be a valid element. This holds exactly for the primitive integer and float +/// types. +/// +/// Types with validity constraints (bool, char, NonZero, ranged newtypes) are excluded even +/// though the `SliceValidityAssume` hook can express byte-width niche constraints: CBMC's +/// default (SAT) backend only instantiates quantifiers with *constant* bounds, and silently +/// degrades symbolic-bound quantifiers to unconstrained free variables +/// (`boolbvt::finish_eager_conversion_quantifiers` -> `conversion_failed`), which would make +/// the validity assumption vacuous. SMT backends (e.g. `--solver z3`) handle the quantified +/// assumption, including multi-byte elements; routing niched element types here can be +/// revisited when CBMC's SAT backend learns symbolic-bound instantiation or Kani selects +/// backends per harness. +pub fn slice_elem_unbounded_ok(_tcx: TyCtxt, ty: Ty) -> bool { + matches!( + ty.kind(), + TyKind::RigidTy(RigidTy::Int(_)) + | TyKind::RigidTy(RigidTy::Uint(_)) + | TyKind::RigidTy(RigidTy::Float(_)) + ) +} + /// 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 diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index d87a5a775184..7842b04c420b 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -9,7 +9,7 @@ use crate::args::ReachabilityType; use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; -use crate::kani_middle::kani_functions::{KaniHook, KaniIntrinsic, KaniModel}; +use crate::kani_middle::kani_functions::{KaniFunction, KaniHook, KaniIntrinsic, KaniModel}; use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_middle::{ @@ -49,6 +49,8 @@ pub struct AutomaticArbitraryPass { /// Whether --constructor-args is enabled: generate values of private-field types through /// their public constructors instead of raw field synthesis. constructor_args: bool, + /// The (optional) unbounded generation models. + unbounded_models: UnboundedModels, } impl AutomaticArbitraryPass { @@ -58,7 +60,8 @@ impl AutomaticArbitraryPass { let kani_assume = *kani_fns.get(&KaniHook::Assume.into()).unwrap(); let kani_assert = *kani_fns.get(&KaniHook::Assert.into()).unwrap(); let constructor_args = query_db.args().autoharness_constructor_args; - Self { kani_any, kani_assume, kani_assert, constructor_args } + let unbounded_models = UnboundedModels::from_kani_functions(kani_fns); + Self { kani_any, kani_assume, kani_assert, constructor_args, unbounded_models } } } @@ -645,20 +648,72 @@ fn assume_scalar_niche( ); } +/// The (optional, alloc-requiring) unbounded generation models, resolved per argument type. +#[derive(Debug, Clone, Default)] +pub struct UnboundedModels { + slice_ref: Option, + slice_mut: Option, + vec: Option, +} + +impl UnboundedModels { + pub fn from_kani_functions(kani_fns: &std::collections::HashMap) -> Self { + UnboundedModels { + slice_ref: kani_fns.get(&KaniModel::AnySliceRefUnbounded.into()).copied(), + slice_mut: kani_fns.get(&KaniModel::AnySliceMutUnbounded.into()).copied(), + vec: kani_fns.get(&KaniModel::AnyVecUnbounded.into()).copied(), + } + } + + /// The model instance generating `ty` unbounded, if `ty` qualifies. + fn instance_for(&self, tcx: TyCtxt, ty: Ty) -> Option { + let (def, elem) = match ty.kind() { + TyKind::RigidTy(RigidTy::Ref(_, inner, mutability)) => match inner.kind() { + TyKind::RigidTy(RigidTy::Slice(elem)) + if crate::kani_middle::slice_elem_unbounded_ok(tcx, elem) => + { + let def = + if mutability == Mutability::Not { self.slice_ref } else { self.slice_mut }; + (def?, elem) + } + _ => return None, + }, + _ => { + let elem = crate::kani_middle::vec_elem_ty(ty)?; + if !crate::kani_middle::slice_elem_unbounded_ok(tcx, elem) { + return None; + } + (self.vec?, elem) + } + }; + Instance::resolve(def, &GenericArgs(vec![GenericArgKind::Type(elem)])).ok() + } +} + fn call_kani_any_for_ty( tcx: TyCtxt, kani_any: FnDef, kani_assume: FnDef, + unbounded_models: &UnboundedModels, body: &mut MutableBody, ty: Ty, mutability: Mutability, source: &mut SourceInstruction, ) -> Local { + // Unbounded generation for slices (&[T]/&mut [T]) and Vec of primitive + // integer/float elements: fresh allocations of nondeterministic size, so results hold + // for all lengths (mirrors the eligibility decision in automatic_harness_partition). + if let Some(model_inst) = unbounded_models.instance_for(tcx, ty) { + let lcl = body.new_local(ty, source.span(body.blocks()), mutability); + body.insert_call(&model_inst, source, InsertPosition::Before, vec![], Place::from(lcl)); + return lcl; + } if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind() { let inner_lcl = call_kani_any_for_ty( tcx, kani_any, kani_assume, + unbounded_models, body, inner_ty, inner_mutability, @@ -715,6 +770,7 @@ impl AutomaticArbitraryPass { tcx, self.kani_any, self.kani_assume, + &self.unbounded_models, body, ty, Mutability::Not, @@ -764,6 +820,7 @@ impl AutomaticArbitraryPass { tcx, self.kani_any, self.kani_assume, + &self.unbounded_models, &mut new_body, *input_ty, Mutability::Not, @@ -832,6 +889,7 @@ impl AutomaticArbitraryPass { tcx, self.kani_any, self.kani_assume, + &self.unbounded_models, &mut new_body, *input_ty, Mutability::Not, @@ -986,6 +1044,7 @@ impl AutomaticArbitraryPass { tcx, self.kani_any, self.kani_assume, + &self.unbounded_models, &mut new_body, Ty::from_rigid_kind(RigidTy::Uint(UintTy::U128)), Mutability::Not, @@ -1063,6 +1122,7 @@ pub struct AutomaticHarnessPass { kani_any: FnDef, init_contracts_hook: Instance, kani_autoharness_intrinsic: FnDef, + unbounded_models: UnboundedModels, } impl AutomaticHarnessPass { @@ -1072,10 +1132,17 @@ impl AutomaticHarnessPass { let kani_autoharness_intrinsic = *kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap(); + let unbounded_models = UnboundedModels::from_kani_functions(kani_fns); let init_contracts_hook = *kani_fns.get(&KaniHook::InitContracts.into()).unwrap(); let init_contracts_hook = Instance::resolve(init_contracts_hook, &GenericArgs(vec![])).unwrap(); - Self { kani_assume, kani_any, init_contracts_hook, kani_autoharness_intrinsic } + Self { + kani_assume, + kani_any, + unbounded_models, + init_contracts_hook, + kani_autoharness_intrinsic, + } } } @@ -1139,6 +1206,7 @@ impl TransformPass for AutomaticHarnessPass { tcx, self.kani_any, self.kani_assume, + &self.unbounded_models, &mut harness_body, local_decl.ty, local_decl.mutability, diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 0b3fb5084091..3916a4793d4d 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -41,3 +41,103 @@ impl Arbitrary for std::time::Duration { std::time::Duration::new(u64::any(), nanos) } } + +/// Generate a slice of *unbounded* nondeterministic length: a fresh allocation of +/// nondeterministic size whose contents are nondeterministic, with element validity +/// established by `slice_validity_assume` (a compiler hook that emits a quantified +/// assumption constraining each element's raw bits to the element type's layout niche; +/// a no-op for element types whose every bit pattern is valid, e.g. integers). +/// +/// This model is used by the compiler to generate nondeterministic `&[T]` arguments for +/// automatic harnesses (`kani autoharness`) when the element type qualifies; verification +/// results hold for ALL slice lengths (functions that iterate over the slice surface any +/// insufficient loop bound as an unwinding-assertion failure rather than passing silently). +/// +/// This model is *optional*: it requires `alloc` and thus has no `core::kani` counterpart, +/// c.f. `KaniModel::is_optional`. +#[kanitool::fn_marker = "AnySliceRefUnboundedModel"] +#[inline(never)] +#[doc(hidden)] +pub fn any_slice_ref_unbounded() -> &'static [T] { + let len: usize = crate::any(); + let elem = std::mem::size_of::(); + if elem == 0 { + // ZST slices: no storage needed, any length is fine. + return unsafe { std::slice::from_raw_parts(std::ptr::NonNull::dangling().as_ptr(), len) }; + } + crate::assume(len <= (isize::MAX as usize) / elem); + let layout = std::alloc::Layout::array::(len.max(1)).unwrap(); + let ptr = unsafe { std::alloc::alloc(layout) }; + crate::assume(!ptr.is_null()); + slice_validity_assume::(ptr, len); + unsafe { std::slice::from_raw_parts(ptr as *const T, len) } +} + +/// Generate a mutable slice of *unbounded* nondeterministic length: as +/// `any_slice_ref_unbounded`, but returning `&mut [T]`. Each call produces a fresh (leaked) +/// allocation, so the returned slice is exclusive by construction; writes through it are +/// unconstrained by other generated values. +/// +/// This model is *optional*: it requires `alloc`, c.f. `KaniModel::is_optional`. +#[kanitool::fn_marker = "AnySliceMutUnboundedModel"] +#[inline(never)] +#[doc(hidden)] +pub fn any_slice_mut_unbounded() -> &'static mut [T] { + let len: usize = crate::any(); + let elem = std::mem::size_of::(); + if elem == 0 { + return unsafe { + std::slice::from_raw_parts_mut(std::ptr::NonNull::dangling().as_ptr(), len) + }; + } + crate::assume(len <= (isize::MAX as usize) / elem); + let layout = std::alloc::Layout::array::(len.max(1)).unwrap(); + let ptr = unsafe { std::alloc::alloc(layout) }; + crate::assume(!ptr.is_null()); + slice_validity_assume::(ptr, len); + unsafe { std::slice::from_raw_parts_mut(ptr as *mut T, len) } +} + +/// Generate a `Vec` of *unbounded* nondeterministic length: a fresh allocation of +/// nondeterministic size whose contents are nondeterministic, with element validity +/// established by `slice_validity_assume` (c.f. `any_slice_ref_unbounded`), handed to +/// `Vec::from_raw_parts` with `capacity == len` (the allocation came from the global +/// allocator with exactly that layout, as `Vec`'s safety contract requires; `Vec` frees it +/// on drop). +/// +/// This model is used by the compiler to generate nondeterministic `Vec` arguments for +/// automatic harnesses (`kani autoharness`) when the element type qualifies; verification +/// results hold for ALL lengths. Optional: requires `alloc`. +#[kanitool::fn_marker = "AnyVecUnboundedModel"] +#[inline(never)] +#[doc(hidden)] +pub fn any_vec_unbounded() -> Vec { + let len: usize = crate::any(); + let elem = std::mem::size_of::(); + if elem == 0 { + // For ZSTs, Vec never allocates and uses a dangling pointer; constructing from a + // dangling pointer with any len is the documented pattern (and loop-free, which + // matters: generation code must not itself be bounded by unwinding). + return unsafe { + Vec::from_raw_parts(std::ptr::NonNull::dangling().as_ptr(), len, usize::MAX) + }; + } + crate::assume(len <= (isize::MAX as usize) / elem); + let layout = std::alloc::Layout::array::(len.max(1)).unwrap(); + let ptr = unsafe { std::alloc::alloc(layout) }; + crate::assume(!ptr.is_null()); + slice_validity_assume::(ptr, len); + unsafe { Vec::from_raw_parts(ptr as *mut T, len, len.max(1)) } +} + +/// Compiler hook (c.f. `KaniHook::SliceValidityAssume`): assume that every element of the +/// `len`-element `T`-array at `ptr` has raw bits within `T`'s layout niche. Lowered directly +/// to a quantified goto assumption; a no-op when `T` has no niche. The default body is +/// unreachable: calls are always intercepted during code generation. +#[kanitool::fn_marker = "SliceValidityAssumeHook"] +#[inline(never)] +#[doc(hidden)] +pub fn slice_validity_assume(_ptr: *const u8, _len: usize) { + #[cfg(not(kani))] + unreachable!("kani::slice_validity_assume is a verification-only hook"); +} diff --git a/tests/script-based-pre/cargo_autoharness_vec_unbounded/Cargo.toml b/tests/script-based-pre/cargo_autoharness_vec_unbounded/Cargo.toml new file mode 100644 index 000000000000..94fdfd354943 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_vec_unbounded/Cargo.toml @@ -0,0 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "cargo_autoharness_vec_unbounded" +version = "0.1.0" +edition = "2021" diff --git a/tests/script-based-pre/cargo_autoharness_vec_unbounded/config.yml b/tests/script-based-pre/cargo_autoharness_vec_unbounded/config.yml new file mode 100644 index 000000000000..0f091d17fae0 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_vec_unbounded/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: vec.sh +expected: vec.expected +exit_code: 1 diff --git a/tests/script-based-pre/cargo_autoharness_vec_unbounded/src/lib.rs b/tests/script-based-pre/cargo_autoharness_vec_unbounded/src/lib.rs new file mode 100644 index 000000000000..66d4a8632e12 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_vec_unbounded/src/lib.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Vec arguments with qualifying element types (integers/floats) are generated +//! *unbounded*: results hold for all lengths, without --bounded-arguments and without the +//! "(bounded)" marker. Loops over the Vec surface insufficient unwinding bounds as +//! unwinding-assertion failures (c.f. `total`). Other element types keep needing +//! BoundedArbitrary support. + +// TEST NOTE: should PASS for ALL lengths (loop-free). +pub fn head(v: Vec) -> Option { + v.first().copied() +} + +// TEST NOTE: should PASS, and all cover checks must be SATISFIED (lengths beyond any +// bound and full content ranges are generated). +pub fn coverage(v: Vec) { + kani::cover!(v.len() > 100_000, "large lengths reachable"); + kani::cover!(!v.is_empty() && v[0] == i32::MIN, "extreme content reachable"); + kani::cover!(v.is_empty(), "empty vec reachable"); +} + +// TEST NOTE: should FAIL with an unwinding assertion: the Vec is unbounded, so the default +// loop bound cannot cover it — the incompleteness is signaled rather than silent. +pub fn total(v: Vec) -> u64 { + v.iter().map(|&b| b as u64).sum() +} + +// TEST NOTE: should PASS for ALL lengths: mutable slices are also unbounded (fresh +// exclusive allocations), and writes through them verify. +pub fn set_first(s: &mut [u8]) { + if !s.is_empty() { + s[0] = 42; + assert_eq!(s[0], 42); + } +} diff --git a/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.expected b/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.expected new file mode 100644 index 000000000000..78aff92666e3 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.expected @@ -0,0 +1,9 @@ +- Status: SATISFIED +- Status: SATISFIED +- Status: SATISFIED +Failed Checks: unwinding assertion loop 0 +| cargo_autoharness_vec_unbounded | coverage | #[kani::proof] | Success | +| cargo_autoharness_vec_unbounded | head | #[kani::proof] | Success | +| cargo_autoharness_vec_unbounded | set_first | #[kani::proof] | Success | +| cargo_autoharness_vec_unbounded | total | #[kani::proof] | Failure | +Complete - 3 successfully verified functions, 1 failures, 4 total. diff --git a/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.sh b/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.sh new file mode 100755 index 000000000000..16060e2fd373 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoharness -Z autoharness --output-format=regular