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/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 2f7aedf59663..858bb88c769a 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -300,6 +300,341 @@ 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 +/// 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..b48febcd8df1 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -9,21 +9,26 @@ 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::{ + 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; 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, ProjectionElem, 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 +39,21 @@ use tracing::debug; pub struct AutomaticArbitraryPass { /// The FnDef of KaniModel::Any kani_any: FnDef, + /// 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 { 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(); + let constructor_args = query_db.args().autoharness_constructor_args; + Self { kani_any, kani_assume, constructor_args } } } @@ -93,7 +106,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| { @@ -115,9 +128,22 @@ 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(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 +154,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 +274,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 +290,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 +302,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); } @@ -202,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 @@ -213,7 +507,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 +517,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 +537,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 +570,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 +584,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 +592,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 +602,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 +670,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/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/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 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 + } +}