diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index 312a5cfdc37..dc60e76cf66 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -104,17 +104,38 @@ By default, when a type does not implement `Arbitrary`, Kani synthesizes values 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. +instead generates values of private-field struct types through one of the type's own +constructors, preferring (in order): + +1. An *assert-guarded representation constructor*: an `unsafe`, `#[doc(hidden)]`, or + `*_unchecked`-named associated function returning `Self` directly, whose preconditions are + stated as assertions (e.g. `debug_assert!`) rather than validated returns. Kani inlines its + body with nondeterministic arguments and converts every validity statement — `kani::assert` + and `assert_unchecked` calls, panic entry points, and overflow (`Assert`) checks — into an + assumption, so the constructor's own assertions filter the arguments down to the values the + crate considers valid. Calls the constructor makes to further assert-guarded helpers are + inlined recursively (bounded in depth and size). Visibility is irrelevant here, since the + body is inlined rather than called. +2. Otherwise, a *checked public constructor*: a public associated function returning `Self`, + `Option`, or `Result`, called with nondeterministic arguments (assuming + success for the `Option`/`Result` shapes). + +Zero-argument constructors, and constructors generic over their own parameters, 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. +found. Note also that a checked 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. + +> **Caveat:** if the chosen constructor is *unsatisfiable* for the generated type — an +> assert-guarded constructor every argument of which trips an assertion, or a checked +> constructor that always returns `None`/`Err` — the generated body assumes `false` on all +> paths and the harness becomes **vacuous**, reporting `Success` without checking anything. +> Kani does not yet detect this case; see +> [#4757](https://github.com/model-checking/kani/issues/4757). ## Example Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again: diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 20f61c90a40..ed05689f924 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -357,12 +357,15 @@ pub fn uses_ctor_generation( 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. + // (`AutomaticArbitraryPass` tries `find_unchecked_constructor`, then + // `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() + && (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; } @@ -428,6 +431,81 @@ pub enum CtorReturn { 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 diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index bf45b918c8b..e37361a6736 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -23,9 +23,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, Region, RegionKind, RigidTy, Ty, @@ -47,8 +48,12 @@ struct AnyModels { kani_any_slice_ref: FnDef, /// The FnDef of KaniModel::AnyStrRef kani_any_str_ref: FnDef, - /// The FnDef of KaniHook::Assume (used for layout-niche assumptions). + /// 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, /// The FnDef of KaniModel::AssumeSafe kani_assume_safe: FnDef, /// The FnDef of KaniModel::BoundedAny @@ -66,6 +71,7 @@ impl AnyModels { kani_any_slice_ref: *kani_fns.get(&KaniModel::AnySliceRef.into()).unwrap(), kani_any_str_ref: *kani_fns.get(&KaniModel::AnyStrRef.into()).unwrap(), kani_assume: *kani_fns.get(&KaniHook::Assume.into()).unwrap(), + kani_assert: *kani_fns.get(&KaniHook::Assert.into()).unwrap(), kani_assume_safe: *kani_fns.get(&KaniModel::AssumeSafe.into()).unwrap(), kani_bounded_any: *kani_fns.get(&KaniModel::BoundedAny.into()).unwrap(), smart_pointer_models: SmartPointerModels::from_kani_functions(kani_fns), @@ -171,15 +177,31 @@ 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( + { + // 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.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)); + ) && 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.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)), @@ -217,6 +239,411 @@ const AUTOHARNESS_STR_BOUND: u64 = 4; /// makes simple `String` harnesses exceed Kani's default 60s harness timeout. const AUTOHARNESS_BOUNDED_ANY_BOUND: u64 = 4; +/// 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 allowlist 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::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, unwind } => { + remap_operand(func); + args.iter_mut().for_each(remap_operand); + remap_place(destination); + if let Some(t) = target { + *t += block_offset; + } + if let UnwindAction::Cleanup(t) = unwind { + *t += block_offset; + } + } + TerminatorKind::Assert { cond, target, unwind, .. } => { + remap_operand(cond); + *target += block_offset; + if let UnwindAction::Cleanup(t) = unwind { + *t += block_offset; + } + } + TerminatorKind::Drop { place, target, unwind, .. } => { + remap_place(place); + *target += block_offset; + if let UnwindAction::Cleanup(t) = unwind { + *t += 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; + +#[allow(clippy::too_many_arguments)] +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 + || is_assert_unchecked_def(def) + || 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 || is_assert_unchecked_def(*def)) + && let Some(cond) = args.first() + { + // kani::assert(cond, msg) / assert_unchecked(cond) -> assume(cond) + let cond = cond.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::") +} + +/// Whether `def` is `core`/`std`'s `hint::assert_unchecked` (a UB-hint contract whose single +/// argument is a validity condition). Matched by exact path rather than substring, so an +/// unrelated user function whose name merely contains "assert_unchecked" is not misclassified +/// (which would drop its call and, if its first argument were not a `bool`, emit ill-typed MIR). +fn is_assert_unchecked_def(def: FnDef) -> bool { + matches!(def.name().as_str(), "core::hint::assert_unchecked" | "std::hint::assert_unchecked") +} + /// For raw pointer types, insert a call to the `KaniModel::AnyPtr` model instead, which generates /// a pointer in a nondeterministic allocation state (null, out of bounds, or valid); /// in the valid case, the pointer points to a nondeterministic value stored in a dedicated local @@ -653,6 +1080,69 @@ 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. + /// + /// Soundness caveat: if the constructor is unsatisfiable for `ty` (every argument trips an + /// assertion), the generated body assumes `false` on all paths and the harness becomes + /// vacuous, reporting Success without checking anything. Not yet detected; tracked in + /// . + 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 mut invariant_cache = FxHashMap::default(); + let arg_locals: Vec = ctor_sig + .inputs() + .iter() + .map(|input_ty| { + call_kani_any_for_ty( + tcx, + self.models, + &mut new_body, + *input_ty, + Mutability::Not, + &mut source, + &mut invariant_cache, + ) + }) + .collect(); + let ret_lcl = inline_with_assumed_panics( + tcx, + self.models.kani_assume, + self.models.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 5e770ed266e..c12712d61d9 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/kani-driver/src/args/autoharness_args.rs b/kani-driver/src/args/autoharness_args.rs index 074add862d0..3bd6485921b 100644 --- a/kani-driver/src/args/autoharness_args.rs +++ b/kani-driver/src/args/autoharness_args.rs @@ -30,11 +30,13 @@ 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. + /// Generate nondeterministic values for types without an Arbitrary implementation through + /// one of the type's own constructors with nondeterministic arguments: either an inlined + /// assert-guarded representation constructor (unsafe/doc-hidden/*_unchecked) whose + /// assertions filter the arguments, or a checked public constructor (assuming it 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, diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 1eb1b2b1f64..cb204ce6c39 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -274,7 +274,7 @@ impl KaniSession { } if any_ctor { println!( - "Note: harnesses marked \"(ctor)\" generate some values through a type's public constructor (--constructor-args);\n\ + "Note: harnesses marked \"(ctor)\" generate some values through one of a type's own constructors (--constructor-args);\n\ their verification results only cover values reachable through that constructor." ); } diff --git a/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected b/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected index 9d54944cd29..21108e3051f 100644 --- a/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected +++ b/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected @@ -5,13 +5,17 @@ | 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 | +| 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); +Note: harnesses marked "(ctor)" generate some values through one of a type's own constructors (--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 | +| 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/constructor.sh b/tests/script-based-pre/cargo_autoharness_constructor/constructor.sh index 1a7861fe673..cb9109342dd 100755 --- a/tests/script-based-pre/cargo_autoharness_constructor/constructor.sh +++ b/tests/script-based-pre/cargo_autoharness_constructor/constructor.sh @@ -3,8 +3,9 @@ # 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)"). +# invariants and reports false alarms; with it, values are generated through the types' own +# constructors (checked public ones, or inlined assert-guarded representation 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 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 44ff4ac2fa7..b228bac1014 100644 --- a/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs @@ -48,22 +48,36 @@ impl Even { } } -// 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, +// 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 OnlyUnchecked { +impl Ranged { #[doc(hidden)] - pub fn from_parts_unchecked(v: u16) -> OnlyUnchecked { - assert!(v >= 1 && v <= 366, "precondition"); - OnlyUnchecked { v } + pub const fn new_unchecked(v: u16) -> Ranged { + debug_assert!(v >= 1); + debug_assert!(v <= 366); + Ranged { value: v } } - pub fn get(&self) -> u16 { - self.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 +}