From df99a58674e968e96dce00c476fe865726142944 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 5 Aug 2026 15:51:00 +0000 Subject: [PATCH 1/2] 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 | 18 ++ kani-compiler/src/args.rs | 4 + .../src/kani_middle/codegen_units.rs | 40 ++- kani-compiler/src/kani_middle/metadata.rs | 3 + kani-compiler/src/kani_middle/mod.rs | 227 ++++++++++++++++++ .../src/kani_middle/transform/automatic.rs | 195 ++++++++++++++- kani-driver/src/args/autoharness_args.rs | 8 + kani-driver/src/autoharness/mod.rs | 23 +- kani-driver/src/frontend/schema_utils.rs | 1 + .../src/frontend/tests/schema_utils_test.rs | 11 +- 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 | 17 ++ .../constructor.sh | 13 + .../cargo_autoharness_constructor/src/lib.rs | 69 ++++++ 18 files changed, 632 insertions(+), 14 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 560638283ce..312a5cfdc37 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -98,6 +98,24 @@ To override the default: In parallel runs each harness result line is prefixed with the thread that produced it, and results arrive in nondeterministic order; the summary table printed at the end is always sorted. +### 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. Note also that a constructor which itself panics for some of its inputs (rather than +rejecting them via `Option`/`Result`) turns those inputs into harness failures, so this option +can trade one class of false alarm for another. + ## 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 aae1b0169c3..c8f31f0dedb 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -122,6 +122,10 @@ pub struct Arguments { /// 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 f1618be1446..3e0ef9f8c31 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -373,13 +373,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<(Instance, bool)>, + verifiable_fns: Vec<(Instance, AutoHarnessCaveats)>, kani_harness_intrinsic: FnDef, base_filename: &Path, ) -> HashMap { verifiable_fns .into_iter() - .map(|(fn_to_verify, is_bounded)| { + .map(|(fn_to_verify, caveats)| { // 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. @@ -393,7 +393,8 @@ fn get_all_automatic_harnesses( base_filename, &fn_to_verify, harness.mangled_name(), - is_bounded, + caveats.is_bounded, + caveats.is_ctor_based, ); (harness, metadata) }) @@ -659,6 +660,16 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result (Vec<(Instance, bool)>, BTreeMap) { +) -> (Vec<(Instance, AutoHarnessCaveats)>, 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) @@ -685,6 +696,9 @@ fn automatic_harness_partition( // Cache whether a type implements or can derive Arbitrary let mut ty_arbitrary_cache: FxHashMap = FxHashMap::default(); + // The constructor search needs the same predicate, but `skip_reason` borrows the cache above + // for the whole loop, so give the `--constructor-args` check its own. + let mut ty_arbitrary_cache_ctor: FxHashMap = FxHashMap::default(); // If `instance` is not eligible for an automatic harness, return the reason why (`Err`); if it // is eligible, return whether its harness requires *bounded* nondeterministic arguments @@ -825,7 +839,23 @@ fn automatic_harness_partition( skipped .insert(crate::kani_middle::strip_local_crate_prefix(instance.name()), reason); } - Ok(is_bounded) => chosen.push((instance, is_bounded)), + Ok(is_bounded) => { + // Whether any generated value will come from a type's public constructor + // rather than raw field synthesis, which the summary reports as "(ctor)". + 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 ty_arbitrary_cache_ctor, + &mut vec![], + ) + }) + }); + chosen.push((instance, AutoHarnessCaveats { is_bounded, is_ctor_based })); + } } } diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index d24248898ab..657756ed8e1 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -43,6 +43,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> has_loop_contracts: false, is_automatically_generated: false, is_bounded: false, + is_ctor_based: false, } } @@ -123,6 +124,7 @@ pub fn gen_automatic_proof_metadata( fn_to_verify: &Instance, harness_mangled_name: String, is_bounded: bool, + is_ctor_based: bool, ) -> HarnessMetadata { let def = fn_to_verify.def; let pretty_name = readable_name(*fn_to_verify); @@ -166,5 +168,6 @@ pub fn gen_automatic_proof_metadata( has_loop_contracts: false, is_automatically_generated: true, is_bounded, + is_ctor_based, } } diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 3f67136fe09..a54ca17fdc0 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -323,6 +323,233 @@ 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; + } + // Deliberately the *same* predicate the generation path uses + // (`AutomaticArbitraryPass` calls `find_arbitrary_constructor`), so that the + // "(ctor)" marker and its under-approximation caveat cannot claim a constructor + // was used when generation actually fell back to raw field synthesis. + if def.kind() == AdtKind::Struct + && adt_has_private_field_check(tcx, def) + && 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 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 6a703b8a98c..bf45b918c8b 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -13,8 +13,9 @@ 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::{ - FmtTrait, SmartPointerModels, can_derive_arbitrary, fmt_impl_self_ty, implements_arbitrary, - implements_invariant, scalar_niche, smart_pointer_model_instance, + CtorReturn, FmtTrait, SmartPointerModels, adt_has_private_field_check, can_derive_arbitrary, + find_arbitrary_constructor, fmt_impl_self_ty, implements_arbitrary, implements_invariant, + scalar_niche, smart_pointer_model_instance, }; use crate::kani_queries::QueryDb; use rustc_data_structures::fx::FxHashMap; @@ -78,11 +79,17 @@ impl AnyModels { pub struct AutomaticArbitraryPass { /// The Kani model functions used to construct nondeterministic values. models: AnyModels, + /// 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 { - Self { models: AnyModels::new(query_db) } + Self { + models: AnyModels::new(query_db), + constructor_args: query_db.args().autoharness_constructor_args, + } } } @@ -157,6 +164,23 @@ 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.models.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)), @@ -629,6 +653,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 mut invariant_cache = FxHashMap::default(); + let arg_ops: Vec = ctor_sig + .inputs() + .iter() + .map(|input_ty| { + let lcl = call_kani_any_for_ty( + tcx, + self.models, + &mut new_body, + *input_ty, + Mutability::Not, + &mut source, + &mut invariant_cache, + ); + 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(..)) = 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!(), + }; + // `VariantDef::idx` is no longer publicly accessible, so reconstruct it from the + // enumeration order, as `generate_enum_body` does. + let ok_variant_idx = VariantIdx::to_val(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.models.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_idx 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 634fd8c0a08..074add862d0 100644 --- a/kani-driver/src/args/autoharness_args.rs +++ b/kani-driver/src/args/autoharness_args.rs @@ -30,6 +30,14 @@ pub struct CommonAutoharnessArgs { #[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 6edd62d769c..1eb1b2b1f64 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -62,6 +62,7 @@ fn setup_session(session: &mut KaniSession, common_autoharness_args: &CommonAuto &common_autoharness_args.include_pattern, &common_autoharness_args.exclude_pattern, common_autoharness_args.bounded_arguments, + common_autoharness_args.constructor_args, ); } @@ -173,6 +174,7 @@ impl KaniSession { included: &[String], excluded: &[String], bounded_arguments: bool, + constructor_args: bool, ) { let mut args = vec![]; for pattern in included { @@ -184,6 +186,9 @@ impl KaniSession { if bounded_arguments { args.push("--autoharness-bounded-arguments".to_string()); } + if constructor_args { + args.push("--autoharness-constructor-args".to_string()); + } self.autoharness_compiler_flags = Some(args); } @@ -223,16 +228,21 @@ impl KaniSession { ]); let harness_kind = |harness: &HarnessMetadata| { + let mut kind = harness.attributes.kind.to_string(); if harness.is_bounded { - format!("{} (bounded)", harness.attributes.kind) - } else { - harness.attributes.kind.to_string() + kind.push_str(" (bounded)"); + } + if harness.is_ctor_based { + kind.push_str(" (ctor)"); } + kind }; let mut any_bounded = false; + let mut any_ctor = false; for success in successes { any_bounded |= success.harness.is_bounded; + any_ctor |= success.harness.is_ctor_based; verified_fns.add_row(vec![ success.harness.crate_name.clone(), success.harness.pretty_name.clone(), @@ -243,6 +253,7 @@ impl KaniSession { for failure in failures { any_bounded |= failure.harness.is_bounded; + any_ctor |= failure.harness.is_ctor_based; verified_fns.add_row(vec![ failure.harness.crate_name.clone(), failure.harness.pretty_name.clone(), @@ -261,6 +272,12 @@ impl KaniSession { their verification results only hold up to the bounds, i.e., bugs that require larger input values may be missed." ); } + 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!( diff --git a/kani-driver/src/frontend/schema_utils.rs b/kani-driver/src/frontend/schema_utils.rs index 1c7cad662e7..e1433183dd4 100644 --- a/kani-driver/src/frontend/schema_utils.rs +++ b/kani-driver/src/frontend/schema_utils.rs @@ -236,6 +236,7 @@ pub fn create_harness_metadata_json(h: &HarnessMetadata) -> Value { "has_loop_contracts": h.has_loop_contracts, "is_automatically_generated": h.is_automatically_generated, "is_bounded": h.is_bounded, + "is_ctor_based": h.is_ctor_based, }) } diff --git a/kani-driver/src/frontend/tests/schema_utils_test.rs b/kani-driver/src/frontend/tests/schema_utils_test.rs index 9d2fbfbcbf7..2898c1896b8 100644 --- a/kani-driver/src/frontend/tests/schema_utils_test.rs +++ b/kani-driver/src/frontend/tests/schema_utils_test.rs @@ -61,11 +61,12 @@ fn test_create_harness_metadata_json() { attributes: HarnessAttributes::new(HarnessKind::Proof), contract: None, has_loop_contracts: true, - // A bounded harness is always automatically generated; check that both flags are - // serialized so that JSON consumers can tell a bounded autoharness run apart from an - // unbounded one. + // Bounded and constructor-based harnesses are always automatically generated; check + // that all three flags are serialized so that JSON consumers can tell an autoharness + // run that under-approximates apart from one that does not. is_automatically_generated: true, is_bounded: true, + is_ctor_based: true, }; let json = create_harness_metadata_json(&harness); @@ -78,6 +79,7 @@ fn test_create_harness_metadata_json() { assert_eq!(json["has_loop_contracts"], true); assert_eq!(json["is_automatically_generated"], true); assert_eq!(json["is_bounded"], true); + assert_eq!(json["is_ctor_based"], true); } #[test] @@ -95,6 +97,7 @@ fn test_create_verification_result_json() { has_loop_contracts: false, is_automatically_generated: false, is_bounded: false, + is_ctor_based: false, }; let properties = vec![ @@ -175,6 +178,7 @@ fn test_create_verification_summary_json_real() { has_loop_contracts: false, is_automatically_generated: false, is_bounded: false, + is_ctor_based: false, }; // Create a VerificationResult @@ -207,6 +211,7 @@ fn test_add_runner_results_to_json_real() { has_loop_contracts: false, is_automatically_generated: false, is_bounded: false, + is_ctor_based: false, }; let verification_result = VerificationResult { diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index f37b2773648..45616915f7a 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -180,6 +180,7 @@ pub mod tests { has_loop_contracts: false, is_automatically_generated: false, is_bounded: false, + is_ctor_based: false, } } diff --git a/kani-driver/src/sarif.rs b/kani-driver/src/sarif.rs index cedf4e4e5c0..d64a9b9a5ab 100644 --- a/kani-driver/src/sarif.rs +++ b/kani-driver/src/sarif.rs @@ -297,6 +297,7 @@ mod tests { has_loop_contracts: false, is_automatically_generated: false, is_bounded: false, + is_ctor_based: false, } } diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 9a8434b3051..4d75ebed9f2 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -47,6 +47,11 @@ pub struct HarnessMetadata { /// holds up to the bounds, c.f. the autoharness --bounded-arguments option. #[serde(default)] pub is_bounded: 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 00000000000..c9dde3e2d2e --- /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 00000000000..6e5869b999e --- /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 00000000000..9d54944cd29 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected @@ -0,0 +1,17 @@ +=== 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 | +| cargo_autoharness_constructor | OnlyUnchecked::get | #[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 | +| cargo_autoharness_constructor | OnlyUnchecked::get | #[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 00000000000..1a7861fe673 --- /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 00000000000..44ff4ac2fa7 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs @@ -0,0 +1,69 @@ +// 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 + } +} + +// A private-field type whose only constructor is an `_unchecked` builder asserting its +// preconditions. Generation cannot use it (such constructors are excluded, since calling them +// with nondeterministic arguments manufactures false alarms), so it must fall back to raw +// field synthesis -- and must NOT be marked "(ctor)", which would claim an under-approximation +// that did not happen. +pub struct OnlyUnchecked { + v: u16, +} + +impl OnlyUnchecked { + #[doc(hidden)] + pub fn from_parts_unchecked(v: u16) -> OnlyUnchecked { + assert!(v >= 1 && v <= 366, "precondition"); + OnlyUnchecked { v } + } + pub fn get(&self) -> u16 { + self.v + } +} From 6f13089d84cd67bd44e01e5929860071da3d9575 Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Tue, 25 Aug 2026 16:11:03 +0000 Subject: [PATCH 2/2] Fix toolchain drift: stabilize EarlyBinder before accessing type in to_fn_def The merge of main upgraded to nightly-2026-05-01, where tcx.type_of(def_id).instantiate_identity() yields an Unnormalized wrapper that no longer implements Stable. Match the rest of the codebase by stabilizing the EarlyBinder and taking its .value. --- kani-compiler/src/kani_middle/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 5e13d42263d..20f61c90a40 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -545,7 +545,7 @@ pub fn find_arbitrary_constructor( /// 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()); + let ty = rustc_internal::stable(tcx.type_of(def_id)).value; match ty.kind() { TyKind::RigidTy(RigidTy::FnDef(def, _)) => Some(def), _ => None,