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..24157fc01d4d 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -111,6 +111,19 @@ 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, + + /// Check mined type invariants on values returned by autoharness-verified functions. + #[arg(long = "autoharness-check-invariants")] + pub autoharness_check_invariants: bool, } #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 6790c5642c8d..5063cf3622a9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -899,6 +899,94 @@ impl GotocHook for LoopInvariantRegister { } } +/// Lower `kani::slice_validity_assume::(ptr, len)` (KaniHook::SliceValidityAssume) to a +/// quantified assumption constraining every element's raw bits to `T`'s layout niche: +/// `assume(forall i. i < len ==> lo <= *(uN*)ptr + i <= hi)` (wrapping ranges use `||`). +/// A no-op for element types without a niche (every bit pattern valid). +/// +/// This is lowered directly to pure goto expressions rather than through `kani::forall!`: +/// the closure-based quantifier lowering cannot substitute bodies containing checked +/// arithmetic or bounds checks (it falls back to an unconstrained predicate), whereas the +/// expressions built here are side-effect-free by construction. +struct SliceValidityAssume; +impl GotocHook for SliceValidityAssume { + fn hook_applies( + &self, + _tcx: TyCtxt, + _instance: Instance, + _instance_name: &str, + _kani_tool_attr: Option<&String>, + ) -> bool { + unreachable!("{UNEXPECTED_CALL}") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + instance: Instance, + mut fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 2); + let loc = gcx.codegen_span_stable(span); + let target = target.unwrap(); + let goto_target = Stmt::goto(bb_label(target), loc); + + let elem_ty = instance.args().0[0].expect_ty().to_owned(); + let Some(niche) = crate::kani_middle::scalar_niche(gcx.tcx, elem_ty) else { + // Every bit pattern is valid: nothing to assume. + return goto_target; + }; + let len = fargs.remove(1); + let ptr = fargs.remove(0); + + // Fresh quantified variable of the same type as `len`. + let base_name = "kani_slice_validity_var".to_string(); + let mut counter = 0; + let mut unique_name = format!("{base_name}_{counter}"); + while gcx.symbol_table.lookup(&unique_name).is_some() { + counter += 1; + unique_name = format!("{base_name}_{counter}"); + } + let qvar = { + let sym = + GotoSymbol::variable(unique_name.clone(), unique_name, len.typ().clone(), loc); + gcx.symbol_table.insert(sym.clone()); + sym.to_expr() + }; + + // CBMC's quantifier handling binds byte-granularity dereferences reliably, but not + // wider ones (byte_extract at a symbolic index under a forall does not propagate), + // so the validity predicate is expressed over bytes: + // - 8-bit niches (bool, u8-based ranged types): direct range check on the byte; + // - NonZero-style niches (excluded zero, full top): OR over "some byte nonzero". + // Wider general ranges are not byte-decomposable this simply; the element classifier + // (kani_middle::slice_elem_unbounded_ok) never routes such types to this hook. + let byte_ty = Type::unsigned_int(8u64); + let byte_ptr = ptr.clone().cast_to(byte_ty.clone().to_pointer()); + let valid = if niche.bits == 8 { + let elem = byte_ptr.plus(qvar.clone()).dereference(); + let lo = Expr::int_constant(niche.start, byte_ty.clone()); + let hi = Expr::int_constant(niche.end, byte_ty.clone()); + if niche.start <= niche.end { + lo.le(elem.clone()).and(elem.le(hi)) + } else { + lo.le(elem.clone()).or(elem.le(hi)) + } + } else { + unreachable!( + "slice_validity_assume: element type with non-byte-decomposable niche should have been rejected by the classifier" + ) + }; + let domain = qvar.clone().lt(len).implies(valid); + let quantified = Expr::forall_expr(Type::Bool, qvar, domain); + + Stmt::block(vec![gcx.codegen_assume(quantified, loc), goto_target], loc) + } +} + struct Forall; struct Exists; @@ -1339,6 +1427,7 @@ pub fn fn_hooks() -> GotocHooks { let kani_lib_hooks = [ (KaniHook::Assert, Rc::new(Assert) as Rc), (KaniHook::Assume, Rc::new(Assume)), + (KaniHook::SliceValidityAssume, Rc::new(SliceValidityAssume)), (KaniHook::Exists, Rc::new(Exists)), (KaniHook::Forall, Rc::new(Forall)), (KaniHook::Panic, Rc::new(Panic)), diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 4b9236c5d45c..a2cd0d772727 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -9,7 +9,7 @@ use crate::args::{Arguments, ReachabilityType}; use crate::kani_middle::attributes::{KaniAttributes, is_proof_harness}; -use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel}; +use crate::kani_middle::kani_functions::{KaniHook, KaniIntrinsic, KaniModel}; use crate::kani_middle::metadata::{ gen_automatic_proof_metadata, gen_contracts_metadata, gen_proof_metadata, }; @@ -103,12 +103,16 @@ impl CodegenUnits { args, &crate_info.name, *kani_fns.get(&KaniModel::Any.into()).unwrap(), + *kani_fns.get(&KaniHook::Assert.into()).unwrap(), + kani_fns.contains_key(&KaniModel::AnySliceRefUnbounded.into()), ); AUTOHARNESS_MD .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 +365,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 +385,7 @@ fn get_all_automatic_harnesses( base_filename, &fn_to_verify, harness.mangled_name(), + is_ctor_based, ); (harness, metadata) }) @@ -417,7 +422,9 @@ fn automatic_harness_partition( args: &Arguments, crate_name: &str, kani_any_def: FnDef, -) -> (Vec, BTreeMap) { + kani_assert_def: FnDef, + unbounded_slice_available: bool, +) -> (Vec<(Instance, bool)>, BTreeMap) { let crate_fn_defs = rustc_public::local_crate().fn_defs().into_iter().collect::>(); // Filter out CrateItems that are functions, but not functions defined in the crate itself, i.e., rustc-inserted functions // (c.f. https://github.com/model-checking/kani/issues/4189) @@ -478,6 +485,25 @@ fn automatic_harness_partition( // Note that we've already filtered out generic functions, so we know that each of these arguments has a concrete type. let mut problematic_args = vec![]; for (idx, arg) in body.arg_locals().iter().enumerate() { + // Unbounded generation: slices (&[T], &mut [T]) and Vec of primitive + // integer/float elements are generated as fresh allocations of + // nondeterministic size (results hold for all lengths), when the optional + // alloc-requiring models are present. + if unbounded_slice_available { + let slice_ok = match arg.ty.kind() { + TyKind::RigidTy(RigidTy::Ref(_, inner, _)) => match inner.kind() { + TyKind::RigidTy(RigidTy::Slice(elem)) => { + crate::kani_middle::slice_elem_unbounded_ok(tcx, elem) + } + _ => false, + }, + _ => crate::kani_middle::vec_elem_ty(arg.ty) + .is_some_and(|elem| crate::kani_middle::slice_elem_unbounded_ok(tcx, elem)), + }; + if slice_ok { + continue; + } + } if !ty_arbitrary_cache.contains_key(&arg.ty) { let impls_arbitrary = implements_arbitrary(arg.ty, kani_any_def, &mut ty_arbitrary_cache) @@ -513,7 +539,21 @@ 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, + kani_assert_def, + &mut FxHashMap::default(), + &mut vec![], + ) + }) + }); + chosen.push((instance, is_ctor_based)); } } diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index d5b97aa5406c..28889e57814d 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -65,6 +65,12 @@ pub enum KaniModel { AlignOfDynObject, #[strum(serialize = "AlignOfValRawModel")] AlignOfVal, + #[strum(serialize = "AnySliceMutUnboundedModel")] + AnySliceMutUnbounded, + #[strum(serialize = "AnySliceRefUnboundedModel")] + AnySliceRefUnbounded, + #[strum(serialize = "AnyVecUnboundedModel")] + AnyVecUnbounded, #[strum(serialize = "AnyModel")] Any, #[strum(serialize = "CopyInitStateModel")] @@ -129,6 +135,8 @@ pub enum KaniHook { AnyRaw, #[strum(serialize = "AssertHook")] Assert, + #[strum(serialize = "SliceValidityAssumeHook")] + SliceValidityAssume, #[strum(serialize = "AssumeHook")] Assume, #[strum(serialize = "CheckHook")] @@ -162,6 +170,20 @@ pub enum KaniHook { UntrackedDeref, } +impl KaniModel { + /// Whether this model may legitimately be absent. These models require `alloc` and are + /// only defined in the `kani` library, not in `core::kani` (the `no_core` flow used by + /// `kani verify-std`). Code retrieving optional models must handle their absence. + pub fn is_optional(&self) -> bool { + matches!( + self, + KaniModel::AnySliceMutUnbounded + | KaniModel::AnySliceRefUnbounded + | KaniModel::AnyVecUnbounded + ) + } +} + impl From for KaniFunction { fn from(value: KaniIntrinsic) -> Self { KaniFunction::Intrinsic(value) @@ -271,7 +293,7 @@ pub fn validate_kani_functions(kani_funcs: &HashMap) { { if let Some(fn_def) = kani_funcs.get(&func) { assert_eq!(KaniFunction::try_from(*fn_def), Ok(func), "Unexpected function marker"); - } else { + } else if !matches!(func, KaniFunction::Model(model) if model.is_optional()) { tracing::error!(?func, "Missing kani function"); missing += 1; } diff --git a/kani-compiler/src/kani_middle/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/mined_invariants.rs b/kani-compiler/src/kani_middle/mined_invariants.rs new file mode 100644 index 000000000000..9bcb7a9c033b --- /dev/null +++ b/kani-compiler/src/kani_middle/mined_invariants.rs @@ -0,0 +1,497 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Mine type invariants from a type's own assertions (C14 static form). +//! +//! Source: `&self` methods of the type's inherent impls whose `kani::assert` calls (Kani's +//! macro overrides have rewritten user asserts/panics into these) satisfy all of: +//! - the assert's block *post-dominates* the entry block (the claim holds on every normal +//! return, structurally rejecting mode-guarded asserts like `if ready { assert!(..) }`); +//! - the condition's backward slice is pure and call-free: leaves are field projections of +//! `self` or constants, interior nodes single-assignment temporaries combined with +//! whitelisted operators. +//! Conditions are extracted into a small expression AST ([MinedExpr]), which provides a +//! canonical form for the frequency filter (a conjunct must be asserted in at least +//! [MIN_ASSERTING_METHODS] distinct methods, guarding against method-local preconditions +//! masquerading as type invariants) and is trivially total when re-materialized as MIR. + +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::{ + BinOp, Body, ConstOperand, Operand, Place, Rvalue, StatementKind, TerminatorKind, UnOp, +}; +use rustc_public::ty::{FnDef, RigidTy, Ty, TyKind}; +use rustc_public_bridge::IndexedVal; + +/// A conjunct must be asserted in at least this many distinct methods to be considered a +/// type invariant rather than a method-local precondition. +pub const MIN_ASSERTING_METHODS: usize = 2; + +/// A pure expression over the fields of a value of the mined type. +#[derive(Clone, Debug)] +pub enum MinedExpr { + /// A chain of field projections starting at the value itself, with the field type. + Field(Vec<(usize, Ty)>), + /// A field chain under an enum variant downcast: only meaningful when the value's + /// discriminant equals the variant index (consumers guard with an implication). + DowncastField(usize, Vec<(usize, Ty)>), + /// A constant: the canonical token (for equality/hashing across methods) plus the + /// original operand (for re-materialization). + Const(String, ConstOperand), + BinOp(BinOp, Box, Box), + UnOp(UnOp, Box), +} + +impl PartialEq for MinedExpr { + fn eq(&self, other: &Self) -> bool { + match (self, other) { + (MinedExpr::Field(a), MinedExpr::Field(b)) => a == b, + (MinedExpr::DowncastField(v1, a), MinedExpr::DowncastField(v2, b)) => { + v1 == v2 && a == b + } + (MinedExpr::Const(a, _), MinedExpr::Const(b, _)) => a == b, + (MinedExpr::BinOp(o1, a1, b1), MinedExpr::BinOp(o2, a2, b2)) => { + o1 == o2 && a1 == a2 && b1 == b2 + } + (MinedExpr::UnOp(o1, a1), MinedExpr::UnOp(o2, a2)) => o1 == o2 && a1 == a2, + _ => false, + } + } +} +impl Eq for MinedExpr {} +impl std::hash::Hash for MinedExpr { + fn hash(&self, state: &mut H) { + std::mem::discriminant(self).hash(state); + match self { + MinedExpr::Field(path) => path.hash(state), + MinedExpr::DowncastField(v, path) => { + v.hash(state); + path.hash(state); + } + MinedExpr::Const(token, _) => token.hash(state), + MinedExpr::BinOp(op, a, b) => { + format!("{op:?}").hash(state); + a.hash(state); + b.hash(state); + } + MinedExpr::UnOp(op, a) => { + format!("{op:?}").hash(state); + a.hash(state); + } + } + } +} + +impl MinedExpr { + pub fn ty(&self) -> Option { + match self { + MinedExpr::Field(path) => path.last().map(|(_, t)| *t), + MinedExpr::DowncastField(_, path) => path.last().map(|(_, t)| *t), + MinedExpr::Const(_, c) => Some(c.const_.ty()), + MinedExpr::BinOp(op, a, _) => match op { + BinOp::Eq | BinOp::Ne | BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge => { + Some(Ty::bool_ty()) + } + _ => a.ty(), + }, + MinedExpr::UnOp(_, a) => a.ty(), + } + } +} + +/// A mined invariant conjunct: the boolean expression plus provenance for diagnostics. +#[derive(Clone, Debug)] +pub struct MinedConjunct { + pub expr: MinedExpr, + /// Methods (pretty names) that assert this conjunct. + pub asserted_in: Vec, +} + +/// Whether the expression contains a variant-downcast field read. +pub fn conjunct_has_downcast(expr: &MinedExpr) -> bool { + match expr { + MinedExpr::Field(_) | MinedExpr::Const(_, _) => false, + MinedExpr::DowncastField(..) => true, + MinedExpr::BinOp(_, a, b) => conjunct_has_downcast(a) || conjunct_has_downcast(b), + MinedExpr::UnOp(_, a) => conjunct_has_downcast(a), + } +} + +/// Whether `bb` post-dominates `from`/// Whether `bb` post-dominates `from` in `body` w.r.t. normal returns: +/// every path from `from` to a `Return` terminator passes through `bb`. +fn postdominates(body: &Body, from: usize, bb: usize) -> bool { + // BFS from `from` avoiding `bb`; if any Return block is reachable, `bb` does not + // post-dominate. + let mut seen = vec![false; body.blocks.len()]; + let mut queue = vec![from]; + seen[from] = true; + if bb == from { + return true; + } + while let Some(cur) = queue.pop() { + let term = &body.blocks[cur].terminator; + if matches!(term.kind, TerminatorKind::Return) { + return false; + } + let mut push = |t: usize| { + if t != bb && !seen[t] { + seen[t] = true; + queue.push(t); + } + }; + match &term.kind { + TerminatorKind::Goto { target } => push(*target), + TerminatorKind::SwitchInt { targets, .. } => { + for (_, t) in targets.branches() { + push(t); + } + push(targets.otherwise()); + } + TerminatorKind::Call { target, .. } => { + if let Some(t) = target { + push(*t); + } + } + TerminatorKind::Drop { target, .. } => push(*target), + TerminatorKind::Assert { target, .. } => push(*target), + _ => {} + } + } + true +} + +/// Extract a [MinedExpr] for `op` in `body`, where local `_1` is `&self` (or `self`). +/// Returns None (bail) when the slice leaves the pure/call-free/single-assignment fragment. +fn extract_expr(body: &Body, op: &Operand, depth: usize) -> Option { + if depth > 24 { + return None; + } + match op { + Operand::Constant(c) => extract_const(c), + Operand::Copy(place) | Operand::Move(place) => extract_place(body, place, depth), + Operand::RuntimeChecks(_) => None, + } +} + +fn extract_const(c: &ConstOperand) -> Option { + // The Debug rendering of the MIR constant is the canonical token for cross-method + // equality; the operand itself is kept for re-materialization. + Some(MinedExpr::Const(format!("{:?}", c.const_), c.clone())) +} + +/// `self` is local 1; a place rooted at it with Deref/Field projections is a field path +/// (an optional leading Downcast records the enum variant, for variant-guarded conjuncts). +fn extract_place(body: &Body, place: &Place, depth: usize) -> Option { + use rustc_public::mir::ProjectionElem; + if place.local == 1 { + let mut path = vec![]; + let mut variant: Option = None; + for elem in &place.projection { + match elem { + ProjectionElem::Deref => {} + ProjectionElem::Field(idx, ty) => path.push((*idx, *ty)), + ProjectionElem::Downcast(v) if path.is_empty() && variant.is_none() => { + variant = Some(v.to_index()); + } + _ => return None, + } + } + if path.is_empty() { + return None; // whole-self uses are not field conditions + } + return Some(match variant { + Some(v) => MinedExpr::DowncastField(v, path), + None => MinedExpr::Field(path), + }); + } + // A temporary dereferenced once: if it uniquely holds a reference, the deref cancels + // (match ergonomics bind payloads by reference: `v = &((*self) as Variant).0`). + if place.projection.len() == 1 && matches!(place.projection[0], ProjectionElem::Deref) { + let base = Place { local: place.local, projection: vec![] }; + if let Some(inner) = unique_ref_def(body, &base) { + return extract_place(body, &inner, depth + 1); + } + return None; + } + // A temporary: find its unique defining assignment or defining call. + if !place.projection.is_empty() { + return None; + } + let mut def: Option<&Rvalue> = None; + let mut call_def: Option<&rustc_public::mir::Terminator> = None; + for block in &body.blocks { + for stmt in &block.statements { + if let StatementKind::Assign(p, rv) = &stmt.kind + && p.local == place.local + { + if p.projection.is_empty() { + if def.is_some() || call_def.is_some() { + return None; // multiple assignments (e.g. short-circuit merge) + } + def = Some(rv); + } else { + return None; + } + } + } + if let TerminatorKind::Call { destination, .. } = &block.terminator.kind + && destination.local == place.local + { + if def.is_some() || call_def.is_some() { + return None; + } + call_def = Some(&block.terminator); + } + } + if let Some(term) = call_def { + // One-level getter inlining: a call to a pure accessor of `self` whose body is + // itself extractable (e.g. `self.len()` where len returns a field expression). + return extract_getter_call(body, term, depth); + } + match def? { + Rvalue::Use(inner) => extract_expr(body, inner, depth + 1), + Rvalue::BinaryOp(bop, a, b) => Some(MinedExpr::BinOp( + *bop, + Box::new(extract_expr(body, a, depth + 1)?), + Box::new(extract_expr(body, b, depth + 1)?), + )), + Rvalue::UnaryOp(uop, a) => { + Some(MinedExpr::UnOp(*uop, Box::new(extract_expr(body, a, depth + 1)?))) + } + Rvalue::CopyForDeref(p) => extract_place(body, p, depth + 1), + _ => None, + } +} + +/// Extract the expression computed by a getter call `self.m()`: the sole argument must be +/// (a reference to) `self`, and the callee's return local must have a unique, extractable +/// definition in terms of ITS `self` (which is the same value). Depth-limited. +fn extract_getter_call( + body: &Body, + term: &rustc_public::mir::Terminator, + depth: usize, +) -> Option { + if depth > 3 { + return None; + } + let TerminatorKind::Call { func, args, .. } = &term.kind else { return None }; + // Sole argument: self (possibly behind a fresh reference temp). + if args.len() != 1 { + return None; + } + let self_rooted = match &args[0] { + Operand::Copy(p) | Operand::Move(p) => p.local == 1 || place_is_ref_to_self(body, p), + _ => false, + }; + if !self_rooted { + return None; + } + let fn_ty = func.ty(body.locals()).ok()?; + let TyKind::RigidTy(RigidTy::FnDef(def, fn_args)) = fn_ty.kind() else { return None }; + let inst = Instance::resolve(def, &fn_args).ok()?; + let callee = inst.body()?; + // Unique assignment to the return local, extractable in the callee's own self frame. + let mut ret_def: Option = None; + for block in &callee.blocks { + for stmt in &block.statements { + if let StatementKind::Assign(p, rv) = &stmt.kind + && p.local == 0 + { + if ret_def.is_some() || !p.projection.is_empty() { + return None; + } + ret_def = Some(match rv { + Rvalue::Use(inner) => extract_expr(&callee, inner, depth + 1)?, + Rvalue::BinaryOp(bop, a, b) => MinedExpr::BinOp( + *bop, + Box::new(extract_expr(&callee, a, depth + 1)?), + Box::new(extract_expr(&callee, b, depth + 1)?), + ), + Rvalue::UnaryOp(uop, a) => { + MinedExpr::UnOp(*uop, Box::new(extract_expr(&callee, a, depth + 1)?)) + } + _ => return None, + }); + } + } + if let TerminatorKind::Call { destination, .. } = &block.terminator.kind + && destination.local == 0 + { + return None; + } + } + ret_def +} + +/// If `p` (a projection-free temp) is uniquely defined as `&`, return that place. +fn unique_ref_def(body: &Body, p: &Place) -> Option { + let mut found: Option = None; + for block in &body.blocks { + for stmt in &block.statements { + if let StatementKind::Assign(dest, rv) = &stmt.kind + && dest.local == p.local + && dest.projection.is_empty() + { + match rv { + Rvalue::Ref(_, _, inner) => { + if found.is_some() { + return None; + } + found = Some(inner.clone()); + } + _ => return None, + } + } + } + if let TerminatorKind::Call { destination, .. } = &block.terminator.kind + && destination.local == p.local + { + return None; + } + } + found +} + +/// Whether `p` is a temp holding `&self`/// Whether `p` is a temp holding `&self` (defined once as `Ref(.., self-place)`). +fn place_is_ref_to_self(body: &Body, p: &Place) -> bool { + if !p.projection.is_empty() { + return false; + } + let mut found = false; + for block in &body.blocks { + for stmt in &block.statements { + if let StatementKind::Assign(dest, rv) = &stmt.kind + && dest.local == p.local + { + match rv { + Rvalue::Ref(_, _, inner) if inner.local == 1 => { + if found { + return false; + } + found = true; + } + _ => return false, + } + } + } + } + found +} + +/// Mine the invariant conjuncts of `ty` (a struct ADT) from its inherent `&self` methods. +/// Results are cached by the caller. +pub fn mine_self_assert_conjuncts(tcx: TyCtxt, ty: Ty, kani_assert: FnDef) -> Vec { + let TyKind::RigidTy(RigidTy::Adt(adt_def, ref adt_args)) = ty.kind() else { + return vec![]; + }; + if !adt_args.0.is_empty() { + return vec![]; + } + let adt_did = rustc_public::rustc_internal::internal(tcx, adt_def.def_id()); + let mut by_expr: FxHashMap> = FxHashMap::default(); + 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; + } + // Skip generic methods; instantiate with no args. + if tcx + .generics_of(item) + .own_params + .iter() + .any(|p| !matches!(p.kind, rustc_middle::ty::GenericParamDefKind::Lifetime)) + { + continue; + } + let Some(fn_def) = crate::kani_middle::stable_fn_def(tcx, item) else { continue }; + let Ok(inst) = Instance::resolve(fn_def, &rustc_public::ty::GenericArgs(vec![])) else { + continue; + }; + let Some(body) = inst.body() else { continue }; + // First parameter must be self by-ref or by-value of our type. + let Some(self_decl) = body.arg_locals().first() else { continue }; + let self_ok = self_decl.ty == ty + || matches!(self_decl.ty.kind(), + TyKind::RigidTy(RigidTy::Ref(_, inner, _)) if inner == ty); + if !self_ok { + continue; + } + let method_name = fn_def.name(); + for (bb_idx, block) in body.blocks.iter().enumerate() { + let TerminatorKind::Call { func, args, .. } = &block.terminator.kind else { + continue; + }; + let Ok(fn_ty) = func.ty(body.locals()) else { continue }; + let TyKind::RigidTy(RigidTy::FnDef(def, _)) = fn_ty.kind() else { continue }; + if def != kani_assert { + continue; + } + // Unconditional claim (post-dominates entry), or a claim guarded by a + // match on self's discriminant (post-dominates that arm's entry): the + // latter yields a variant-guarded conjunct via the DowncastField reads in + // its expression. + let unconditional = postdominates(&body, 0, bb_idx); + let mut arm_guarded = false; + if !unconditional { + 'guard: for block in &body.blocks { + let TerminatorKind::SwitchInt { discr, targets } = &block.terminator.kind + else { + continue; + }; + // The switch must be on self's discriminant. + let is_self_discr = match discr { + Operand::Copy(p) | Operand::Move(p) => { + p.projection.is_empty() + && body.blocks.iter().any(|b| { + b.statements.iter().any(|st| { + matches!(&st.kind, + StatementKind::Assign(d, Rvalue::Discriminant(src)) + if d.local == p.local && src.local == 1) + }) + }) + } + _ => false, + }; + if !is_self_discr { + continue; + } + for (_, target) in targets.branches() { + if postdominates(&body, target, bb_idx) { + arm_guarded = true; + break 'guard; + } + } + if postdominates(&body, targets.otherwise(), bb_idx) { + arm_guarded = true; + break 'guard; + } + } + } + if !unconditional && !arm_guarded { + continue; + } + let Some(expr) = extract_expr(&body, &args[0], 0) else { continue }; + // Arm-guarded conjuncts must carry the variant via their downcast reads; + // unconditional conjuncts must not (a bare downcast read without its match + // would be under-guarded). + match (unconditional, conjunct_has_downcast(&expr)) { + (true, true) | (false, false) => continue, + _ => {} + } + if expr.ty() != Some(Ty::bool_ty()) { + continue; + } + let entry = by_expr.entry(expr).or_default(); + if !entry.contains(&method_name) { + entry.push(method_name.clone()); + } + } + } + } + by_expr + .into_iter() + .filter(|(_, methods)| methods.len() >= MIN_ASSERTING_METHODS) + .map(|(expr, asserted_in)| MinedConjunct { expr, asserted_in }) + .collect() +} diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 2f7aedf59663..c24f3e200100 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -86,6 +86,7 @@ pub mod coercion; mod intrinsics; pub mod kani_functions; pub mod metadata; +pub mod mined_invariants; pub mod points_to; pub mod provide; pub mod reachability; @@ -300,6 +301,434 @@ 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, + kani_assert_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, + kani_assert_def, + ty_arbitrary_cache, + visited, + ) + } + TyKind::RigidTy(RigidTy::Array(inner, _)) | TyKind::RigidTy(RigidTy::Slice(inner)) => { + uses_ctor_generation( + tcx, + inner, + kani_any_def, + kani_assert_def, + ty_arbitrary_cache, + visited, + ) + } + TyKind::RigidTy(RigidTy::Tuple(elems)) => elems.iter().any(|elem| { + uses_ctor_generation( + tcx, + *elem, + kani_any_def, + kani_assert_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; + } + // Mined-invariant assumptions are heuristic filters like constructor-based + // generation, so harnesses using them carry the same marker. + if !mined_invariants::mine_self_assert_conjuncts(tcx, ty, kani_assert_def).is_empty() { + return true; + } + def.variants_iter().any(|variant| { + variant.fields().iter().any(|field| { + uses_ctor_generation( + tcx, + field.ty_with_args(&args), + kani_any_def, + kani_assert_def, + ty_arbitrary_cache, + visited, + ) + }) + }) || args.0.iter().any(|arg| match arg { + GenericArgKind::Type(t) => uses_ctor_generation( + tcx, + *t, + kani_any_def, + kani_assert_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, + } +} + +/// If `ty` is `Vec` with the default allocator, return `T`. +pub fn vec_elem_ty(ty: Ty) -> Option { + let TyKind::RigidTy(RigidTy::Adt(def, ref args)) = ty.kind() else { return None }; + let name = def.name(); + if name != "std::vec::Vec" && name != "alloc::vec::Vec" { + return None; + } + // Vec: only the default allocator is supported (the model allocates via + // the global allocator). The allocator parameter is defaulted, so a crate naming a + // custom allocator produces a second type argument != Global. + let mut ty_args = args.0.iter().filter_map(|a| match a { + GenericArgKind::Type(t) => Some(*t), + _ => None, + }); + let elem = ty_args.next()?; + if let Some(alloc_ty) = ty_args.next() + && !alloc_ty.to_string().contains("Global") + { + return None; + } + Some(elem) +} + +/// Whether `&[T]` arguments with this element type qualify for *unbounded* generation +/// (`KaniModel::AnySliceRefUnbounded`): raw nondeterministic memory must be a sound AND +/// complete model of the element's values *without any validity assumption*, i.e. every bit +/// pattern must be a valid element. This holds exactly for the primitive integer and float +/// types. +/// +/// Types with validity constraints (bool, char, NonZero, ranged newtypes) are excluded even +/// though the `SliceValidityAssume` hook can express byte-width niche constraints: CBMC's +/// default (SAT) backend only instantiates quantifiers with *constant* bounds, and silently +/// degrades symbolic-bound quantifiers to unconstrained free variables +/// (`boolbvt::finish_eager_conversion_quantifiers` -> `conversion_failed`), which would make +/// the validity assumption vacuous. SMT backends (e.g. `--solver z3`) handle the quantified +/// assumption, including multi-byte elements; routing niched element types here can be +/// revisited when CBMC's SAT backend learns symbolic-bound instantiation or Kani selects +/// backends per harness. +pub fn slice_elem_unbounded_ok(_tcx: TyCtxt, ty: Ty) -> bool { + matches!( + ty.kind(), + TyKind::RigidTy(RigidTy::Int(_)) + | TyKind::RigidTy(RigidTy::Uint(_)) + | TyKind::RigidTy(RigidTy::Float(_)) + ) +} + +/// The bit width of a scalar-ABI type (integer primitives and enum discriminant types). +pub fn scalar_width_bits(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, .. } = scalar else { return None }; + let Primitive::Int(int, _) = value else { return None }; + Some(int.size().bits()) +} + +/// 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..2b43d1ddc438 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -9,21 +9,28 @@ 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::kani_functions::{KaniFunction, KaniHook, KaniIntrinsic, KaniModel}; +use crate::kani_middle::mined_invariants::{MinedConjunct, MinedExpr, mine_self_assert_conjuncts}; 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, 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, 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 +41,28 @@ 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, + /// The FnDef of KaniHook::Assert (rewritten into assumptions when inlining + /// assert-guarded constructors). + kani_assert: FnDef, + /// Whether --constructor-args is enabled: generate values of private-field types through + /// their public constructors instead of raw field synthesis. + constructor_args: bool, + /// The (optional) unbounded generation models. + unbounded_models: UnboundedModels, } 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 kani_assert = *kani_fns.get(&KaniHook::Assert.into()).unwrap(); + let constructor_args = query_db.args().autoharness_constructor_args; + let unbounded_models = UnboundedModels::from_kani_functions(kani_fns); + Self { kani_any, kani_assume, kani_assert, constructor_args, unbounded_models } } } @@ -93,7 +115,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 +137,39 @@ 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) + { + // Prefer assert-guarded representation constructors, inlined with panic + // paths converted to assumptions: their own assertions state the type's + // validity contract, and they are typically surjective onto the valid value + // space (unlike checked constructors, which may reach only a subset). + if let Some(ctor) = crate::kani_middle::find_unchecked_constructor( + tcx, + *ty, + self.kani_any, + &mut FxHashMap::default(), + ) && let Some(new_body) = + self.generate_unchecked_ctor_body(tcx, ctor, *ty, body.clone()) + { + debug!(?ty, ctor=?ctor.name(), "generate_unchecked_ctor_body"); + return (true, new_body); + } + if let Some((ctor, shape)) = + find_arbitrary_constructor(tcx, *ty, self.kani_any, &mut FxHashMap::default()) + { + debug!(?ty, ctor=?ctor.name(), ?shape, "generate_ctor_body"); + return (true, self.generate_ctor_body(tcx, ctor, shape, *ty, body)); + } + } match def.kind() { - AdtKind::Enum => (true, self.generate_enum_body(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 +180,861 @@ impl TransformPass for AutomaticArbitraryPass { /// Insert a call to kani::any::() in `body`; return the local storing the result. /// Panics if `ty` does not implement Arbitrary. +/// Remap all locals and block targets of an inlined basic block. Returns false (bail out) +/// when the block contains a construct the remapper does not support; the caller then falls +/// back to non-inlined generation. The whitelist covers everything rustc emits for +/// assert-guarded field-packing constructors (the C14 mining target). +fn remap_block(bb: &mut BasicBlock, local_map: &[Local], block_offset: usize) -> bool { + let remap_place = |p: &mut Place| { + p.local = local_map[p.local]; + for elem in p.projection.iter_mut() { + if let ProjectionElem::Index(l) = elem { + *l = local_map[*l]; + } + } + }; + let remap_operand = |op: &mut Operand| match op { + Operand::Copy(p) | Operand::Move(p) => remap_place(p), + Operand::Constant(_) | Operand::RuntimeChecks(_) => {} + }; + for stmt in bb.statements.iter_mut() { + match &mut stmt.kind { + StatementKind::Assign(place, rvalue) => { + remap_place(place); + match rvalue { + Rvalue::Use(op) | Rvalue::Repeat(op, _) | Rvalue::Cast(_, op, _) => { + remap_operand(op) + } + Rvalue::BinaryOp(_, a, b) | Rvalue::CheckedBinaryOp(_, a, b) => { + remap_operand(a); + remap_operand(b); + } + Rvalue::UnaryOp(_, op) => remap_operand(op), + Rvalue::Ref(_, _, p) + | Rvalue::AddressOf(_, p) + | Rvalue::CopyForDeref(p) + | Rvalue::Discriminant(p) + | Rvalue::Len(p) => remap_place(p), + Rvalue::Aggregate(_, ops) => ops.iter_mut().for_each(remap_operand), + Rvalue::ShallowInitBox(op, _) => remap_operand(op), + Rvalue::ThreadLocalRef(_) => return false, + } + } + StatementKind::StorageLive(l) | StatementKind::StorageDead(l) => { + *l = local_map[*l]; + } + StatementKind::SetDiscriminant { place, .. } + | StatementKind::PlaceMention(place) + | StatementKind::FakeRead(_, place) => remap_place(place), + StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(op)) => remap_operand(op), + StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(cp)) => { + remap_operand(&mut cp.src); + remap_operand(&mut cp.dst); + remap_operand(&mut cp.count); + } + StatementKind::AscribeUserType { .. } + | StatementKind::Coverage(_) + | StatementKind::ConstEvalCounter + | StatementKind::Retag(..) + | StatementKind::Nop => {} + } + } + match &mut bb.terminator.kind { + TerminatorKind::Goto { target } => *target += block_offset, + TerminatorKind::SwitchInt { discr, targets } => { + remap_operand(discr); + let branches: Vec<_> = targets.branches().map(|(v, t)| (v, t + block_offset)).collect(); + *targets = SwitchTargets::new(branches, targets.otherwise() + block_offset); + } + TerminatorKind::Call { func, args, destination, target, .. } => { + remap_operand(func); + args.iter_mut().for_each(remap_operand); + remap_place(destination); + if let Some(t) = target { + *t += block_offset; + } + } + TerminatorKind::Assert { cond, target, .. } => { + remap_operand(cond); + *target += block_offset; + } + TerminatorKind::Drop { place, target, .. } => { + remap_place(place); + *target += block_offset; + } + TerminatorKind::Return + | TerminatorKind::Unreachable + | TerminatorKind::Resume + | TerminatorKind::Abort => {} + TerminatorKind::InlineAsm { .. } => return false, + } + true +} + +/// C14 (assert mining, dynamic form): inline `callee`'s monomorphic body into `body` at +/// `source`, with every validity statement converted into a filter on the nondeterministic +/// inputs: +/// - `kani::assert(cond, msg)` calls (Kani's macro overrides have already rewritten user +/// asserts/panics into these) become `kani::assume(cond)`; +/// - `hint::assert_unchecked(cond)` calls (UB-hint contracts, e.g. deranged's +/// `new_unchecked`) become `kani::assume(cond)`; +/// - raw panic-entry calls become `assume(false); unreachable`; +/// - MIR `Assert` terminators (overflow checks) become `assume(cond == expected)`. +/// +/// Calls *within* the inlined body whose callees themselves contain such validity statements +/// (e.g. time's `Time::__from_hms_nanos_unchecked` calling deranged's `new_unchecked`) are +/// recursively inlined, up to [INLINE_MAX_DEPTH] levels and [INLINE_MAX_BLOCKS] blocks per +/// callee; other calls are kept as plain calls. +/// +/// `arg_locals` must hold fully-initialized constructor arguments. Returns the local holding +/// the constructed value, or None (caller falls back to a plain call) if the outer callee +/// body contains unsupported constructs. (A bail-out mid-way leaves only unused locals +/// behind, which is harmless.) +const INLINE_MAX_DEPTH: usize = 3; +const INLINE_MAX_BLOCKS: usize = 32; + +fn inline_with_assumed_panics( + tcx: TyCtxt, + kani_assume: FnDef, + kani_assert: FnDef, + body: &mut MutableBody, + source: &mut SourceInstruction, + callee: Instance, + arg_locals: &[Local], + ret_ty: Ty, +) -> Option { + let callee_body = callee.body()?; + let span = source.span(body.blocks()); + let ret_lcl = body.new_local(ret_ty, span, Mutability::Mut); + + // All blocks from `block_offset` onward are planned into `planned`; slots are allocated + // (possibly ahead of being filled) so that nested inlining can interleave with the outer + // walk without breaking target indices. + let continuation = body.blocks().len(); + let block_offset = continuation + 1; + let assume_inst = Instance::resolve(kani_assume, &GenericArgs(vec![])).unwrap(); + + struct Ctx<'tcx, 'a> { + tcx: TyCtxt<'tcx>, + kani_assert: FnDef, + assume_inst: Instance, + body: &'a mut MutableBody, + planned: Vec>, + block_offset: usize, + span: rustc_public::ty::Span, + } + + impl Ctx<'_, '_> { + fn alloc(&mut self, n: usize) -> usize { + let base = self.block_offset + self.planned.len(); + self.planned.extend(std::iter::repeat_with(|| None).take(n)); + base + } + + fn set(&mut self, idx: usize, bb: BasicBlock) { + self.planned[idx - self.block_offset] = Some(bb); + } + + fn assume_call_terminator( + &mut self, + cond: Operand, + target: BasicBlockIdx, + ) -> TerminatorKind { + let func_lcl = self.body.new_local(self.assume_inst.ty(), self.span, Mutability::Not); + let unit_lcl = self.body.new_local(Ty::new_tuple(&[]), self.span, Mutability::Mut); + TerminatorKind::Call { + func: Operand::Copy(Place::from(func_lcl)), + args: vec![cond], + destination: Place::from(unit_lcl), + target: Some(target), + unwind: UnwindAction::Terminate, + } + } + + /// Does `fn_body` directly contain a validity statement worth mining? + fn worth_inlining(&self, fn_body: &Body) -> bool { + fn_body.blocks.iter().any(|bb| match &bb.terminator.kind { + TerminatorKind::Assert { .. } => true, + TerminatorKind::Call { func, .. } => { + match func.ty(fn_body.locals()).map(|t| t.kind()) { + Ok(TyKind::RigidTy(RigidTy::FnDef(def, _))) => { + def == self.kani_assert + || def.name().contains("assert_unchecked") + || is_panic_def(self.tcx, def) + } + _ => false, + } + } + _ => false, + }) + } + + /// Plan `fn_body` (of `n` blocks) into slots `base..base+n`, remapping via + /// `local_map`, converting validity statements, recursively inlining qualifying + /// callees. Returns false to bail out (unsupported construct at depth 0; at deeper + /// levels callers pre-check with `worth_inlining` and blocks are conservative). + fn plan_body( + &mut self, + fn_body: &Body, + local_map: &[Local], + base: usize, + ret_target: BasicBlockIdx, + depth: usize, + ) -> bool { + for (i, callee_bb) in fn_body.blocks.iter().enumerate() { + let mut bb = callee_bb.clone(); + if !remap_block(&mut bb, local_map, base) { + return false; + } + match &mut bb.terminator.kind { + TerminatorKind::Return => { + bb.terminator.kind = TerminatorKind::Goto { target: ret_target }; + } + TerminatorKind::Resume | TerminatorKind::Abort => { + bb.terminator.kind = TerminatorKind::Unreachable; + } + TerminatorKind::Assert { cond, expected, target, .. } => { + let (cond, expected, target) = (cond.clone(), *expected, *target); + let cond_lcl = + self.body.new_local(Ty::bool_ty(), self.span, Mutability::Mut); + let rv = if expected { + Rvalue::Use(cond) + } else { + Rvalue::UnaryOp(UnOp::Not, cond) + }; + bb.statements.push(Statement { + kind: StatementKind::Assign(Place::from(cond_lcl), rv), + span: self.span, + }); + bb.terminator.kind = self + .assume_call_terminator(Operand::Move(Place::from(cond_lcl)), target); + } + TerminatorKind::Call { func, args, destination, target, .. } => { + let fn_def = match func.ty(self.body.locals()).map(|t| t.kind()) { + Ok(TyKind::RigidTy(RigidTy::FnDef(def, fn_args))) => { + Some((def, fn_args)) + } + _ => None, + }; + if let Some((def, _)) = &fn_def + && (*def == self.kani_assert || def.name().contains("assert_unchecked")) + { + // kani::assert(cond, msg) / assert_unchecked(cond) -> assume(cond) + let cond = args[0].clone(); + let target = target.expect("assert has a return target"); + bb.terminator.kind = self.assume_call_terminator(cond, target); + } else if let Some((def, _)) = &fn_def + && is_panic_def(self.tcx, *def) + { + // panic -> assume(false); unreachable + let unreach = self.alloc(1); + self.set( + unreach, + BasicBlock { + statements: vec![], + terminator: Terminator { + kind: TerminatorKind::Unreachable, + span: self.span, + }, + }, + ); + let false_op = Operand::Constant(ConstOperand { + span: self.span, + user_ty: None, + const_: MirConst::from_bool(false), + }); + bb.terminator.kind = self.assume_call_terminator(false_op, unreach); + } else if depth < INLINE_MAX_DEPTH + && let Some((def, fn_args)) = &fn_def + && let Ok(inst) = Instance::resolve(*def, fn_args) + && let Some(inner_body) = inst.body() + && inner_body.blocks.len() <= INLINE_MAX_BLOCKS + && self.worth_inlining(&inner_body) + { + // Recursively inline: materialize args into fresh locals, + // stitch the return value into the call's destination. + let target = target.expect("inlined callee has a return target"); + let inner_ret_ty = inner_body.locals()[0].ty; + let inner_ret_lcl = + self.body.new_local(inner_ret_ty, self.span, Mutability::Mut); + let mut inner_map = vec![inner_ret_lcl]; + for (arg_op, decl) in args.iter().zip(inner_body.arg_locals().iter()) { + let a = self.body.new_local(decl.ty, self.span, Mutability::Mut); + bb.statements.push(Statement { + kind: StatementKind::Assign( + Place::from(a), + Rvalue::Use(arg_op.clone()), + ), + span: self.span, + }); + inner_map.push(a); + } + for decl in inner_body.locals().iter().skip(1 + args.len()) { + inner_map.push(self.body.new_local( + decl.ty, + self.span, + Mutability::Mut, + )); + } + let stitch = self.alloc(1); + let inner_base = self.alloc(inner_body.blocks.len()); + self.set( + stitch, + BasicBlock { + statements: vec![Statement { + kind: StatementKind::Assign( + destination.clone(), + Rvalue::Use(Operand::Move(Place::from(inner_ret_lcl))), + ), + span: self.span, + }], + terminator: Terminator { + kind: TerminatorKind::Goto { target }, + span: self.span, + }, + }, + ); + if self.plan_body( + &inner_body, + &inner_map, + inner_base, + stitch, + depth + 1, + ) { + bb.terminator.kind = TerminatorKind::Goto { target: inner_base }; + } else { + // Nested bail-out: keep the plain call; fill the reserved + // slots with unreachable stubs (never targeted). + for j in 0..inner_body.blocks.len() { + if self.planned[inner_base + j - self.block_offset].is_none() { + self.set( + inner_base + j, + BasicBlock { + statements: vec![], + terminator: Terminator { + kind: TerminatorKind::Unreachable, + span: self.span, + }, + }, + ); + } + } + } + } + // else: keep the plain (already remapped) call. + } + _ => {} + } + self.set(base + i, bb); + } + true + } + } + + // Map callee locals: _0 -> ret_lcl, _1..=argc -> arg_locals, rest -> fresh. + let mut local_map: Vec = Vec::with_capacity(callee_body.locals().len()); + local_map.push(ret_lcl); + let argc = callee_body.arg_locals().len(); + assert_eq!(argc, arg_locals.len()); + local_map.extend_from_slice(arg_locals); + for decl in callee_body.locals().iter().skip(1 + argc) { + local_map.push(body.new_local(decl.ty, span, Mutability::Mut)); + } + + let mut ctx = Ctx { tcx, kani_assert, assume_inst, body, planned: vec![], block_offset, span }; + let outer_base = ctx.alloc(callee_body.blocks.len()); + if !ctx.plan_body(&callee_body, &local_map, outer_base, continuation, 0) { + return None; + } + let planned = ctx.planned; + + // Commit: split the caller and append all planned blocks at their precomputed indices. + let placeholder = Terminator { kind: TerminatorKind::Goto { target: outer_base }, span }; + let (_goto_bb, actual_continuation) = body.split_with_terminator(source, placeholder); + assert_eq!(actual_continuation, continuation); + for bb in planned { + body.push_raw_bb(bb.expect("all planned slots must be filled")); + } + Some(ret_lcl) +} + +/// Whether `def` is a panic entry point. +fn is_panic_def(tcx: TyCtxt, def: FnDef) -> bool { + let def_id = rustc_public::rustc_internal::internal(tcx, def.def_id()); + Some(def_id) == tcx.lang_items().panic_fn() + || Some(def_id) == tcx.lang_items().panic_fmt() + || Some(def_id) == tcx.lang_items().begin_panic_fn() + || def.name().starts_with("core::panicking::") +} + +/// Materialize a [MinedExpr] over the value in `value_local` (of the mined type) as MIR, +/// returning the local holding the expression's result. Total by construction: the AST +/// contains only field reads, constants, and pure operators. +fn build_mined_expr( + body: &mut MutableBody, + source: &mut SourceInstruction, + value_local: Local, + expr: &MinedExpr, +) -> Local { + let span = source.span(body.blocks()); + match expr { + MinedExpr::Field(path) => { + let (_, leaf_ty) = *path.last().unwrap(); + let place = Place { + local: value_local, + projection: path.iter().map(|(idx, ty)| ProjectionElem::Field(*idx, *ty)).collect(), + }; + let lcl = body.new_local(leaf_ty, span, Mutability::Not); + body.assign_to( + Place::from(lcl), + Rvalue::Use(Operand::Copy(place)), + source, + InsertPosition::Before, + ); + lcl + } + MinedExpr::DowncastField(variant, path) => { + // Reads the variant's field regardless of the actual discriminant; consumers + // guard the enclosing conjunct with `discriminant != variant || ...`, so the + // read value is irrelevant on other variants (the read itself is byte-level + // and harmless to CBMC). + let (_, leaf_ty) = *path.last().unwrap(); + let mut projection = + vec![ProjectionElem::Downcast(rustc_public::ty::VariantIdx::to_val(*variant))]; + projection.extend(path.iter().map(|(idx, ty)| ProjectionElem::Field(*idx, *ty))); + let place = Place { local: value_local, projection }; + let lcl = body.new_local(leaf_ty, span, Mutability::Not); + body.assign_to( + Place::from(lcl), + Rvalue::Use(Operand::Copy(place)), + source, + InsertPosition::Before, + ); + lcl + } + MinedExpr::Const(_, c) => { + let ty = c.const_.ty(); + let lcl = body.new_local(ty, span, Mutability::Not); + body.assign_to( + Place::from(lcl), + Rvalue::Use(Operand::Constant(c.clone())), + source, + InsertPosition::Before, + ); + lcl + } + MinedExpr::BinOp(op, a, b) => { + let la = build_mined_expr(body, source, value_local, a); + let lb = build_mined_expr(body, source, value_local, b); + let ty = expr.ty().unwrap(); + let lcl = body.new_local(ty, span, Mutability::Not); + body.assign_to( + Place::from(lcl), + Rvalue::BinaryOp( + *op, + Operand::Copy(Place::from(la)), + Operand::Copy(Place::from(lb)), + ), + source, + InsertPosition::Before, + ); + lcl + } + MinedExpr::UnOp(op, a) => { + let la = build_mined_expr(body, source, value_local, a); + let ty = expr.ty().unwrap(); + let lcl = body.new_local(ty, span, Mutability::Not); + body.assign_to( + Place::from(lcl), + Rvalue::UnaryOp(*op, Operand::Copy(Place::from(la))), + source, + InsertPosition::Before, + ); + lcl + } + } +} + +/// The enum variant a conjunct is guarded by, if any: mining produces conjuncts whose +/// downcast field reads all target the assert's match arm, so a single variant governs the +/// whole expression. +fn conjunct_guard_variant(expr: &MinedExpr) -> Option { + match expr { + MinedExpr::Field(_) | MinedExpr::Const(_, _) => None, + MinedExpr::DowncastField(v, _) => Some(*v), + MinedExpr::BinOp(_, a, b) => { + conjunct_guard_variant(a).or_else(|| conjunct_guard_variant(b)) + } + MinedExpr::UnOp(_, a) => conjunct_guard_variant(a), + } +} + +/// Build the final condition local for a conjunct over `value_local`: the raw expression +/// for struct conjuncts, or `discriminant(value) != variant || expr` for variant-guarded +/// (enum) conjuncts, making the claim vacuously true on other variants. +fn build_guarded_conjunct( + tcx: TyCtxt, + body: &mut MutableBody, + source: &mut SourceInstruction, + value_local: Local, + value_ty: Ty, + expr: &MinedExpr, +) -> Option { + let raw = build_mined_expr(body, source, value_local, expr); + let Some(variant) = conjunct_guard_variant(expr) else { return Some(raw) }; + let span = source.span(body.blocks()); + // discriminant(value) + let discr_ty = value_ty.kind().discriminant_ty()?; + let discr_lcl = body.new_local(discr_ty, span, Mutability::Not); + body.assign_to( + Place::from(discr_lcl), + Rvalue::Discriminant(Place::from(value_local)), + source, + InsertPosition::Before, + ); + // Transmute to a same-width uint for the comparison (as assume_scalar_niche does). + let niche_bits = crate::kani_middle::scalar_width_bits(tcx, discr_ty)?; + let uint_ty = match niche_bits { + 8 => UintTy::U8, + 16 => UintTy::U16, + 32 => UintTy::U32, + 64 => UintTy::U64, + 128 => UintTy::U128, + _ => return Some(raw), + }; + let raw_ty = Ty::from_rigid_kind(RigidTy::Uint(uint_ty)); + let discr_uint = body.new_local(raw_ty, span, Mutability::Not); + body.assign_to( + Place::from(discr_uint), + Rvalue::Cast(CastKind::Transmute, Operand::Copy(Place::from(discr_lcl)), raw_ty), + source, + InsertPosition::Before, + ); + let TyKind::RigidTy(RigidTy::Adt(adt_def, _)) = value_ty.kind() else { return Some(raw) }; + let discr_val = + adt_def.discriminant_for_variant(rustc_public::ty::VariantIdx::to_val(variant)).val; + let mask = if niche_bits == 128 { u128::MAX } else { (1u128 << niche_bits) - 1 }; + let variant_const = Operand::Constant(ConstOperand { + span, + user_ty: None, + const_: MirConst::try_from_uint(discr_val & mask, uint_ty).ok()?, + }); + let bool_ty = Ty::bool_ty(); + let ne_lcl = body.new_local(bool_ty, span, Mutability::Not); + body.assign_to( + Place::from(ne_lcl), + Rvalue::BinaryOp(BinOp::Ne, Operand::Copy(Place::from(discr_uint)), variant_const), + source, + InsertPosition::Before, + ); + let cond_lcl = body.new_local(bool_ty, span, Mutability::Not); + body.assign_to( + Place::from(cond_lcl), + Rvalue::BinaryOp( + BinOp::BitOr, + Operand::Move(Place::from(ne_lcl)), + Operand::Move(Place::from(raw)), + ), + source, + InsertPosition::Before, + ); + Some(cond_lcl) +} + +/// Emit `kani::assume()` for each mined conjunct of `ty` over the value in +/// `value_local`. Mined conjuncts are the type's own assertions (a necessary condition of +/// the values the crate's code accepts), so assuming them filters generated values the same +/// way constructor-assert mining does, at lower formula cost than constructor inlining. +fn assume_mined_invariants( + tcx: TyCtxt, + kani_assume: FnDef, + body: &mut MutableBody, + source: &mut SourceInstruction, + value_local: Local, + value_ty: Ty, + conjuncts: &[MinedConjunct], +) { + let assume_inst = Instance::resolve(kani_assume, &GenericArgs(vec![])).unwrap(); + for conjunct in conjuncts { + let Some(cond) = + build_guarded_conjunct(tcx, body, source, value_local, value_ty, &conjunct.expr) + else { + continue; + }; + let span = source.span(body.blocks()); + 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))], + Place::from(unit_lcl), + ); + } +} + +/// Emit `kani::assert(, msg)` for each mined conjunct of `ty` over the value in +/// `value_local` (`--check-invariants`): checks that a function's return value satisfies +/// the type's own assertions. Reported with a distinct message so users can recognize the +/// property class (the mined predicate is heuristic; a failure means the returned value +/// would trip the type's own assertions when used). +fn check_mined_invariants( + tcx: TyCtxt, + kani_assert: FnDef, + body: &mut MutableBody, + source: &mut SourceInstruction, + value_local: Local, + ty: Ty, + // For payloads peeled out of Option/Result returns: (wrapper local, ok variant idx, + // wrapper ty). Each check is guarded with `wrapper discriminant != ok || conjunct`, so + // None/Err returns pass vacuously (the payload read is a harmless byte-level read). + wrapper: Option<(Local, usize, Ty)>, + conjuncts: &[MinedConjunct], +) { + let assert_inst = Instance::resolve(kani_assert, &GenericArgs(vec![])).unwrap(); + // Compute the wrapper guard (discriminant != ok) once. + let wrapper_ne: Option = wrapper.and_then(|(wlcl, ok_idx, wty)| { + let span = source.span(body.blocks()); + let discr_ty = wty.kind().discriminant_ty()?; + let discr_lcl = body.new_local(discr_ty, span, Mutability::Not); + body.assign_to( + Place::from(discr_lcl), + Rvalue::Discriminant(Place::from(wlcl)), + source, + InsertPosition::Before, + ); + let bits = crate::kani_middle::scalar_width_bits(tcx, discr_ty)?; + let uint_ty = match bits { + 8 => UintTy::U8, + 16 => UintTy::U16, + 32 => UintTy::U32, + 64 => UintTy::U64, + 128 => UintTy::U128, + _ => return None, + }; + let raw_ty = Ty::from_rigid_kind(RigidTy::Uint(uint_ty)); + let discr_uint = body.new_local(raw_ty, span, Mutability::Not); + body.assign_to( + Place::from(discr_uint), + Rvalue::Cast(CastKind::Transmute, Operand::Copy(Place::from(discr_lcl)), raw_ty), + source, + InsertPosition::Before, + ); + let TyKind::RigidTy(RigidTy::Adt(adt_def, _)) = wty.kind() else { return None }; + let discr_val = + adt_def.discriminant_for_variant(rustc_public::ty::VariantIdx::to_val(ok_idx)).val; + let mask = if bits == 128 { u128::MAX } else { (1u128 << bits) - 1 }; + let c = Operand::Constant(ConstOperand { + span, + user_ty: None, + const_: MirConst::try_from_uint(discr_val & mask, uint_ty).ok()?, + }); + let ne = body.new_local(Ty::bool_ty(), span, Mutability::Not); + body.assign_to( + Place::from(ne), + Rvalue::BinaryOp(BinOp::Ne, Operand::Copy(Place::from(discr_uint)), c), + source, + InsertPosition::Before, + ); + Some(ne) + }); + for conjunct in conjuncts { + let Some(mut cond) = + build_guarded_conjunct(tcx, body, source, value_local, ty, &conjunct.expr) + else { + continue; + }; + if let Some(ne) = wrapper_ne { + let span = source.span(body.blocks()); + let ored = body.new_local(Ty::bool_ty(), span, Mutability::Not); + body.assign_to( + Place::from(ored), + Rvalue::BinaryOp( + BinOp::BitOr, + Operand::Copy(Place::from(ne)), + Operand::Move(Place::from(cond)), + ), + source, + InsertPosition::Before, + ); + cond = ored; + } + let span = source.span(body.blocks()); + let msg = format!( + "mined invariant of `{ty}` violated by return value (asserted in {})", + conjunct.asserted_in.join(", ") + ); + let msg_op = body.new_str_operand(&msg, span); + let unit_lcl = body.new_local(Ty::new_tuple(&[]), span, Mutability::Not); + body.insert_call( + &assert_inst, + source, + InsertPosition::Before, + vec![Operand::Move(Place::from(cond)), msg_op], + Place::from(unit_lcl), + ); + } +} + +/// 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), + ); +} + +/// The (optional, alloc-requiring) unbounded generation models, resolved per argument type. +#[derive(Debug, Clone, Default)] +pub struct UnboundedModels { + slice_ref: Option, + slice_mut: Option, + vec: Option, +} + +impl UnboundedModels { + pub fn from_kani_functions(kani_fns: &std::collections::HashMap) -> Self { + UnboundedModels { + slice_ref: kani_fns.get(&KaniModel::AnySliceRefUnbounded.into()).copied(), + slice_mut: kani_fns.get(&KaniModel::AnySliceMutUnbounded.into()).copied(), + vec: kani_fns.get(&KaniModel::AnyVecUnbounded.into()).copied(), + } + } + + /// The model instance generating `ty` unbounded, if `ty` qualifies. + fn instance_for(&self, tcx: TyCtxt, ty: Ty) -> Option { + let (def, elem) = match ty.kind() { + TyKind::RigidTy(RigidTy::Ref(_, inner, mutability)) => match inner.kind() { + TyKind::RigidTy(RigidTy::Slice(elem)) + if crate::kani_middle::slice_elem_unbounded_ok(tcx, elem) => + { + let def = + if mutability == Mutability::Not { self.slice_ref } else { self.slice_mut }; + (def?, elem) + } + _ => return None, + }, + _ => { + let elem = crate::kani_middle::vec_elem_ty(ty)?; + if !crate::kani_middle::slice_elem_unbounded_ok(tcx, elem) { + return None; + } + (self.vec?, elem) + } + }; + Instance::resolve(def, &GenericArgs(vec![GenericArgKind::Type(elem)])).ok() + } +} + fn call_kani_any_for_ty( + tcx: TyCtxt, kani_any: FnDef, + kani_assume: FnDef, + kani_assert: FnDef, + constructor_args: bool, + mined_cache: &mut FxHashMap>, + unbounded_models: &UnboundedModels, body: &mut MutableBody, ty: Ty, mutability: Mutability, source: &mut SourceInstruction, ) -> Local { + // Unbounded generation for slices (&[T]/&mut [T]) and Vec of primitive + // integer/float elements: fresh allocations of nondeterministic size, so results hold + // for all lengths (mirrors the eligibility decision in automatic_harness_partition). + if let Some(model_inst) = unbounded_models.instance_for(tcx, ty) { + let lcl = body.new_local(ty, source.span(body.blocks()), mutability); + body.insert_call(&model_inst, source, InsertPosition::Before, vec![], Place::from(lcl)); + return lcl; + } if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind() { - let inner_lcl = call_kani_any_for_ty(kani_any, body, inner_ty, inner_mutability, source); + let inner_lcl = call_kani_any_for_ty( + tcx, + kani_any, + kani_assume, + kani_assert, + constructor_args, + mined_cache, + unbounded_models, + 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 +1054,22 @@ 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); + + // Under --constructor-args (the heuristic-filter umbrella), assume the type's + // mined invariant conjuncts (its own methods' assertions) for the generated value. + if constructor_args { + if matches!(ty.kind(), TyKind::RigidTy(RigidTy::Adt(..))) { + let conjuncts = mined_cache + .entry(ty) + .or_insert_with(|| mine_self_assert_conjuncts(tcx, ty, kani_assert)); + if !conjuncts.is_empty() { + let conjuncts = conjuncts.clone(); + assume_mined_invariants(tcx, kani_assume, body, source, lcl, ty, &conjuncts); + } + } + } lcl } } @@ -170,6 +1084,8 @@ impl AutomaticArbitraryPass { /// This function will panic if a field type does not implement Arbitrary. fn call_kani_any_for_variant( &self, + tcx: TyCtxt, + mined_cache: &mut FxHashMap>, adt_def: AdtDef, adt_args: &GenericArgs, body: &mut MutableBody, @@ -181,7 +1097,19 @@ 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, + self.kani_assert, + self.constructor_args, + mined_cache, + &self.unbounded_models, + body, + ty, + Mutability::Not, + source, + ); field_locals.push(lcl); } @@ -202,6 +1130,238 @@ impl AutomaticArbitraryPass { source.bb() - (fields.len() + 1) } + /// Overwrite the default `kani::any()` implementation `body` for a struct with private + /// fields by inlining an assert-guarded representation constructor with nondeterministic + /// arguments and panic paths converted into assumptions + /// (c.f. [find_unchecked_constructor][crate::kani_middle::find_unchecked_constructor]). + /// Returns None if the constructor body contains constructs the inliner does not support. + fn generate_unchecked_ctor_body( + &self, + tcx: TyCtxt, + ctor: Instance, + ty: Ty, + body: Body, + ) -> Option { + let mut new_body = MutableBody::from(body); + new_body.clear_body(TerminatorKind::Unreachable); + let mut mined_cache: FxHashMap> = FxHashMap::default(); + let mut source = SourceInstruction::Terminator { bb: 0 }; + let ctor_sig = ctor.ty().kind().fn_sig().unwrap().skip_binder(); + let arg_locals: Vec = ctor_sig + .inputs() + .iter() + .map(|input_ty| { + call_kani_any_for_ty( + tcx, + self.kani_any, + self.kani_assume, + self.kani_assert, + self.constructor_args, + &mut mined_cache, + &self.unbounded_models, + &mut new_body, + *input_ty, + Mutability::Not, + &mut source, + ) + }) + .collect(); + let ret_lcl = inline_with_assumed_panics( + tcx, + self.kani_assume, + self.kani_assert, + &mut new_body, + &mut source, + ctor, + &arg_locals, + ty, + )?; + // RETURN_LOCAL = move ret; return + new_body.assign_to( + Place::from(0), + Rvalue::Use(Operand::Move(Place::from(ret_lcl))), + &mut source, + InsertPosition::Before, + ); + let span = source.span(new_body.blocks()); + new_body.insert_terminator( + &mut source, + InsertPosition::Before, + Terminator { kind: TerminatorKind::Return, span }, + ); + Some(new_body.into()) + } + + /// Overwrite the default `kani::any()` implementation `body` for a struct with private + /// fields by calling a public constructor with nondeterministic arguments + /// (`--constructor-args`). The returned body is equivalent to: + /// ```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 mined_cache: FxHashMap> = FxHashMap::default(); + 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, + self.kani_assert, + self.constructor_args, + &mut mined_cache, + &self.unbounded_models, + &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,17 +1373,24 @@ 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); let mut new_body = MutableBody::from(body); new_body.clear_body(TerminatorKind::Unreachable); + let mut mined_cache: FxHashMap> = FxHashMap::default(); let mut source = SourceInstruction::Terminator { bb: 0 }; // Generate a nondet u128 to switch on let discr_lcl = call_kani_any_for_ty( + tcx, self.kani_any, + self.kani_assume, + self.kani_assert, + self.constructor_args, + &mut mined_cache, + &self.unbounded_models, &mut new_body, Ty::from_rigid_kind(RigidTy::Uint(UintTy::U128)), Mutability::Not, @@ -241,8 +1408,15 @@ 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, + &mut mined_cache, + def, + &args, + &mut new_body, + &mut source, + variant, + ); branches.push((variant.idx.to_index() as u128, target_bb)); } @@ -268,15 +1442,30 @@ 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); new_body.clear_body(TerminatorKind::Unreachable); + let mut mined_cache: FxHashMap> = FxHashMap::default(); 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, + &mut mined_cache, + def, + &args, + &mut new_body, + &mut source, + variant, + ); new_body.into() } @@ -284,21 +1473,41 @@ 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 { + kani_assert: FnDef, + constructor_args: bool, + check_invariants: bool, + /// The FnDef of KaniHook::Assume (used for layout-niche assumptions). + kani_assume: FnDef, kani_any: FnDef, init_contracts_hook: Instance, kani_autoharness_intrinsic: FnDef, + unbounded_models: UnboundedModels, } 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 kani_assert = *kani_fns.get(&KaniHook::Assert.into()).unwrap(); + let constructor_args = query_db.args().autoharness_constructor_args; + let check_invariants = query_db.args().autoharness_check_invariants; + let unbounded_models = UnboundedModels::from_kani_functions(kani_fns); let init_contracts_hook = *kani_fns.get(&KaniHook::InitContracts.into()).unwrap(); let init_contracts_hook = Instance::resolve(init_contracts_hook, &GenericArgs(vec![])).unwrap(); - Self { kani_any, init_contracts_hook, kani_autoharness_intrinsic } + Self { + kani_assume, + kani_any, + kani_assert, + constructor_args, + check_invariants, + unbounded_models, + init_contracts_hook, + kani_autoharness_intrinsic, + } } } @@ -319,6 +1528,7 @@ impl TransformPass for AutomaticHarnessPass { fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { debug!(function=?instance.name(), "AutomaticHarnessPass::transform"); + let mut mined_cache: FxHashMap> = FxHashMap::default(); if instance.def.def_id() != self.kani_autoharness_intrinsic.def_id() { return (false, body); @@ -359,7 +1569,13 @@ impl TransformPass for AutomaticHarnessPass { .iter() .map(|local_decl| { call_kani_any_for_ty( + tcx, self.kani_any, + self.kani_assume, + self.kani_assert, + self.constructor_args, + &mut mined_cache, + &self.unbounded_models, &mut harness_body, local_decl.ty, local_decl.mutability, @@ -369,11 +1585,12 @@ impl TransformPass for AutomaticHarnessPass { .collect::>(); let func_to_verify_ret = fn_to_verify_body.ret_local(); - let ret_place = Place::from(harness_body.new_local( + let ret_lcl = harness_body.new_local( func_to_verify_ret.ty, source.span(harness_body.blocks()), func_to_verify_ret.mutability, - )); + ); + let ret_place = Place::from(ret_lcl); // Call `fn_to_verify` on the nondeterministic arguments generated above. harness_body.insert_call( @@ -384,6 +1601,96 @@ impl TransformPass for AutomaticHarnessPass { ret_place, ); + // Under --check-invariants, check the return value against the type's mined + // invariants. Direct T and &T returns are handled (Option/Result peeling is a + // logged follow-up). + if self.check_invariants { + let ret_ty = func_to_verify_ret.ty; + // Peel the return type down to a checkable ADT value: direct T, &T, and the + // payloads of Option/Result. For the latter two, the payload is read + // via a downcast (harmless byte-level read on the other variant) and every + // conjunct is guarded with `discriminant != Some/Ok || conjunct`, making the + // check vacuously true for None/Err returns. + let mut wrapper_guard: Option<(usize, Ty)> = None; // (ok variant idx, wrapper ty) + let (check_ty, check_lcl) = match ret_ty.kind() { + TyKind::RigidTy(RigidTy::Ref(_, inner, _)) + if matches!(inner.kind(), TyKind::RigidTy(RigidTy::Adt(..))) => + { + // Deref into a temp of the pointee type. + let span = source.span(harness_body.blocks()); + let tmp = harness_body.new_local(inner, span, Mutability::Not); + harness_body.assign_to( + Place::from(tmp), + Rvalue::Use(Operand::Copy(Place { + local: ret_lcl, + projection: vec![ProjectionElem::Deref], + })), + &mut source, + InsertPosition::Before, + ); + (inner, Some(tmp)) + } + TyKind::RigidTy(RigidTy::Adt(d, ref wargs)) + if matches!( + d.name().as_str(), + "std::option::Option" + | "core::option::Option" + | "std::result::Result" + | "core::result::Result" + ) => + { + let ok_idx = if d.name().contains("Option") { 1 } else { 0 }; + let payload = wargs.0.iter().find_map(|a| match a { + GenericArgKind::Type(t) => Some(*t), + _ => None, + }); + match payload { + Some(pt) if matches!(pt.kind(), TyKind::RigidTy(RigidTy::Adt(..))) => { + let span = source.span(harness_body.blocks()); + let tmp = harness_body.new_local(pt, span, Mutability::Not); + harness_body.assign_to( + Place::from(tmp), + Rvalue::Use(Operand::Copy(Place { + local: ret_lcl, + projection: vec![ + ProjectionElem::Downcast( + rustc_public::ty::VariantIdx::to_val(ok_idx), + ), + ProjectionElem::Field(0, pt), + ], + })), + &mut source, + InsertPosition::Before, + ); + wrapper_guard = Some((ok_idx, ret_ty)); + (pt, Some(tmp)) + } + _ => (ret_ty, None), + } + } + TyKind::RigidTy(RigidTy::Adt(..)) => (ret_ty, Some(ret_lcl)), + _ => (ret_ty, None), + }; + if let Some(lcl) = check_lcl { + let conjuncts = mined_cache + .entry(check_ty) + .or_insert_with(|| mine_self_assert_conjuncts(tcx, check_ty, self.kani_assert)) + .clone(); + if !conjuncts.is_empty() { + check_mined_invariants( + tcx, + self.kani_assert, + &mut harness_body, + &mut source, + lcl, + check_ty, + wrapper_guard.map(|(ok, wty)| (ret_lcl, ok, wty)), + &conjuncts, + ); + } + } + } + (true, harness_body.into()) } } diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 9d36caadcd73..360aa3829ef5 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -359,6 +359,28 @@ impl MutableBody { self.split_bb(source, position, terminator); } + /// Append a fully-formed basic block (whose targets the caller has already remapped into + /// this body's index space) and return its index. Building block for inlining callee + /// bodies, c.f. `automatic::inline_with_assumed_panics`. + pub fn push_raw_bb(&mut self, bb: BasicBlock) -> BasicBlockIdx { + self.blocks.push(bb); + self.blocks.len() - 1 + } + + /// Split the block at `source`, terminating the first half with `terminator` (whose + /// targets may still be placeholders), and return (index of the terminator's block, + /// index of the remainder block). Building block for inlining callee bodies. + pub fn split_with_terminator( + &mut self, + source: &mut SourceInstruction, + terminator: Terminator, + ) -> (BasicBlockIdx, BasicBlockIdx) { + let remainder_idx = self.blocks.len(); + let term_bb_idx = source.bb(); + self.split_bb(source, InsertPosition::Before, terminator); + (term_bb_idx, remainder_idx) + } + /// Insert statement before or after the source instruction and update the source as needed. If /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the diff --git a/kani-driver/src/args/autoharness_args.rs b/kani-driver/src/args/autoharness_args.rs index 93d9eb439127..2d59d2c47de1 100644 --- a/kani-driver/src/args/autoharness_args.rs +++ b/kani-driver/src/args/autoharness_args.rs @@ -23,6 +23,29 @@ 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, + + /// Check that values returned by verified functions satisfy their type's *mined* + /// invariants: assertions over the type's own fields that at least two of its methods + /// state. Failures are reported as a distinct property class; since the mined predicate + /// is heuristic, a failure means the returned value would trip the type's own + /// assertions when used, which may or may not be a bug in the returning function. + #[arg(long)] + pub check_invariants: 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..15575eaaf3f0 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,8 @@ 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, + common_autoharness_args.check_invariants, ); } @@ -161,7 +163,13 @@ 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, + check_invariants: bool, + ) { let mut args = vec![]; for pattern in included { args.push(format!("--autoharness-include-pattern {pattern}")); @@ -169,6 +177,12 @@ impl KaniSession { for pattern in excluded { args.push(format!("--autoharness-exclude-pattern {pattern}")); } + if constructor_args { + args.push("--autoharness-constructor-args".to_string()); + } + if check_invariants { + args.push("--autoharness-check-invariants".to_string()); + } self.autoharness_compiler_flags = Some(args); } @@ -207,20 +221,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 +254,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/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 0b3fb5084091..3916a4793d4d 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -41,3 +41,103 @@ impl Arbitrary for std::time::Duration { std::time::Duration::new(u64::any(), nanos) } } + +/// Generate a slice of *unbounded* nondeterministic length: a fresh allocation of +/// nondeterministic size whose contents are nondeterministic, with element validity +/// established by `slice_validity_assume` (a compiler hook that emits a quantified +/// assumption constraining each element's raw bits to the element type's layout niche; +/// a no-op for element types whose every bit pattern is valid, e.g. integers). +/// +/// This model is used by the compiler to generate nondeterministic `&[T]` arguments for +/// automatic harnesses (`kani autoharness`) when the element type qualifies; verification +/// results hold for ALL slice lengths (functions that iterate over the slice surface any +/// insufficient loop bound as an unwinding-assertion failure rather than passing silently). +/// +/// This model is *optional*: it requires `alloc` and thus has no `core::kani` counterpart, +/// c.f. `KaniModel::is_optional`. +#[kanitool::fn_marker = "AnySliceRefUnboundedModel"] +#[inline(never)] +#[doc(hidden)] +pub fn any_slice_ref_unbounded() -> &'static [T] { + let len: usize = crate::any(); + let elem = std::mem::size_of::(); + if elem == 0 { + // ZST slices: no storage needed, any length is fine. + return unsafe { std::slice::from_raw_parts(std::ptr::NonNull::dangling().as_ptr(), len) }; + } + crate::assume(len <= (isize::MAX as usize) / elem); + let layout = std::alloc::Layout::array::(len.max(1)).unwrap(); + let ptr = unsafe { std::alloc::alloc(layout) }; + crate::assume(!ptr.is_null()); + slice_validity_assume::(ptr, len); + unsafe { std::slice::from_raw_parts(ptr as *const T, len) } +} + +/// Generate a mutable slice of *unbounded* nondeterministic length: as +/// `any_slice_ref_unbounded`, but returning `&mut [T]`. Each call produces a fresh (leaked) +/// allocation, so the returned slice is exclusive by construction; writes through it are +/// unconstrained by other generated values. +/// +/// This model is *optional*: it requires `alloc`, c.f. `KaniModel::is_optional`. +#[kanitool::fn_marker = "AnySliceMutUnboundedModel"] +#[inline(never)] +#[doc(hidden)] +pub fn any_slice_mut_unbounded() -> &'static mut [T] { + let len: usize = crate::any(); + let elem = std::mem::size_of::(); + if elem == 0 { + return unsafe { + std::slice::from_raw_parts_mut(std::ptr::NonNull::dangling().as_ptr(), len) + }; + } + crate::assume(len <= (isize::MAX as usize) / elem); + let layout = std::alloc::Layout::array::(len.max(1)).unwrap(); + let ptr = unsafe { std::alloc::alloc(layout) }; + crate::assume(!ptr.is_null()); + slice_validity_assume::(ptr, len); + unsafe { std::slice::from_raw_parts_mut(ptr as *mut T, len) } +} + +/// Generate a `Vec` of *unbounded* nondeterministic length: a fresh allocation of +/// nondeterministic size whose contents are nondeterministic, with element validity +/// established by `slice_validity_assume` (c.f. `any_slice_ref_unbounded`), handed to +/// `Vec::from_raw_parts` with `capacity == len` (the allocation came from the global +/// allocator with exactly that layout, as `Vec`'s safety contract requires; `Vec` frees it +/// on drop). +/// +/// This model is used by the compiler to generate nondeterministic `Vec` arguments for +/// automatic harnesses (`kani autoharness`) when the element type qualifies; verification +/// results hold for ALL lengths. Optional: requires `alloc`. +#[kanitool::fn_marker = "AnyVecUnboundedModel"] +#[inline(never)] +#[doc(hidden)] +pub fn any_vec_unbounded() -> Vec { + let len: usize = crate::any(); + let elem = std::mem::size_of::(); + if elem == 0 { + // For ZSTs, Vec never allocates and uses a dangling pointer; constructing from a + // dangling pointer with any len is the documented pattern (and loop-free, which + // matters: generation code must not itself be bounded by unwinding). + return unsafe { + Vec::from_raw_parts(std::ptr::NonNull::dangling().as_ptr(), len, usize::MAX) + }; + } + crate::assume(len <= (isize::MAX as usize) / elem); + let layout = std::alloc::Layout::array::(len.max(1)).unwrap(); + let ptr = unsafe { std::alloc::alloc(layout) }; + crate::assume(!ptr.is_null()); + slice_validity_assume::(ptr, len); + unsafe { Vec::from_raw_parts(ptr as *mut T, len, len.max(1)) } +} + +/// Compiler hook (c.f. `KaniHook::SliceValidityAssume`): assume that every element of the +/// `len`-element `T`-array at `ptr` has raw bits within `T`'s layout niche. Lowered directly +/// to a quantified goto assumption; a no-op when `T` has no niche. The default body is +/// unreachable: calls are always intercepted during code generation. +#[kanitool::fn_marker = "SliceValidityAssumeHook"] +#[inline(never)] +#[doc(hidden)] +pub fn slice_validity_assume(_ptr: *const u8, _len: usize) { + #[cfg(not(kani))] + unreachable!("kani::slice_validity_assume is a verification-only hook"); +} diff --git a/tests/script-based-pre/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..6d34194a2e6c --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_constructor/constructor.expected @@ -0,0 +1,21 @@ +=== 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 | Ranged::new_unchecked | #[kani::proof] | Failure | +| cargo_autoharness_constructor | Wrapper::from_raw_unchecked | #[kani::proof] | Failure | +| cargo_autoharness_constructor | wrapped_ordinal0 | #[kani::proof] | Failure | +=== with flag === +Note: harnesses marked "(ctor)" generate some values through a type's public constructor (--constructor-args); +| cargo_autoharness_constructor | Celsius::from_milli | #[kani::proof] | Success | +| 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 | 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 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..b228bac1014a --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_constructor/src/lib.rs @@ -0,0 +1,83 @@ +// 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 + } +} + +// Assert-guarded representation constructors (unsafe/doc-hidden/_unchecked) are inlined +// with their validity assertions converted into filters — including one level of nesting +// (Wrapper's ctor calls Ranged's). +pub struct Ranged { + value: u16, // invariant 1..=366, stated by new_unchecked's debug_asserts +} + +impl Ranged { + #[doc(hidden)] + pub const fn new_unchecked(v: u16) -> Ranged { + debug_assert!(v >= 1); + debug_assert!(v <= 366); + Ranged { value: v } + } +} + +pub struct Wrapper { + inner: Ranged, +} + +impl Wrapper { + #[doc(hidden)] + pub const fn from_raw_unchecked(v: u16) -> Wrapper { + Wrapper { inner: Ranged::new_unchecked(v) } + } +} + +// TEST NOTE: should PASS with --constructor-args (the nested debug_asserts filter the +// generated values); FAILS without. +pub fn wrapped_ordinal0(w: Wrapper) -> u16 { + assert!(w.inner.value >= 1, "invariant violated"); + w.inner.value - 1 +} diff --git a/tests/script-based-pre/cargo_autoharness_mined_invariants/Cargo.toml b/tests/script-based-pre/cargo_autoharness_mined_invariants/Cargo.toml new file mode 100644 index 000000000000..0a9b12b2344f --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_mined_invariants/Cargo.toml @@ -0,0 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "cargo_autoharness_mined_invariants" +version = "0.1.0" +edition = "2021" diff --git a/tests/script-based-pre/cargo_autoharness_mined_invariants/config.yml b/tests/script-based-pre/cargo_autoharness_mined_invariants/config.yml new file mode 100644 index 000000000000..2017b54609a9 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_mined_invariants/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: mined.sh +expected: mined.expected +exit_code: 1 diff --git a/tests/script-based-pre/cargo_autoharness_mined_invariants/mined.expected b/tests/script-based-pre/cargo_autoharness_mined_invariants/mined.expected new file mode 100644 index 000000000000..352a2c2e4f98 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_mined_invariants/mined.expected @@ -0,0 +1,10 @@ + - Description: "mined invariant of `Day` violated by return value (asserted in cargo_autoharness_mined_invariants::Day::ordinal0, cargo_autoharness_mined_invariants::Day::ordinal)" +Failed Checks: mined invariant of `Day` violated by return value (asserted in cargo_autoharness_mined_invariants::Day::ordinal0, cargo_autoharness_mined_invariants::Day::ordinal) +| cargo_autoharness_mined_invariants | day_user | #[kani::proof] (ctor) | Success | +| cargo_autoharness_mined_invariants | good_make_day | #[kani::proof] | Success | +| cargo_autoharness_mined_invariants | good_try_make_day | #[kani::proof] | Success | +| cargo_autoharness_mined_invariants | length_user | #[kani::proof] (ctor) | Success | +| cargo_autoharness_mined_invariants | tank_user | #[kani::proof] (ctor) | Success | +| cargo_autoharness_mined_invariants | buggy_make_day | #[kani::proof] | Failure | +| cargo_autoharness_mined_invariants | buggy_try_make_day | #[kani::proof] | Failure | +| cargo_autoharness_mined_invariants | prec_user | #[kani::proof] | Failure | diff --git a/tests/script-based-pre/cargo_autoharness_mined_invariants/mined.sh b/tests/script-based-pre/cargo_autoharness_mined_invariants/mined.sh new file mode 100755 index 000000000000..5468a9f95922 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_mined_invariants/mined.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Mined type invariants (assertions over self fields stated by >= 2 methods): +# - assumed for generated values under --constructor-args (day_user passes; the +# single-method precondition on Gauge::drain is NOT mined, so prec_user still fails); +# - checked on return values under --check-invariants (buggy_make_day fails with the +# distinct property class; good_make_day passes). +cargo kani autoharness -Z autoharness --constructor-args --check-invariants --output-format=regular diff --git a/tests/script-based-pre/cargo_autoharness_mined_invariants/src/lib.rs b/tests/script-based-pre/cargo_autoharness_mined_invariants/src/lib.rs new file mode 100644 index 000000000000..2fe27c251b5c --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_mined_invariants/src/lib.rs @@ -0,0 +1,127 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// A type whose invariant (value in 1..=366) is stated by asserts in TWO methods: +// mined as an invariant (frequency filter passes) and assumed for generated values. +pub struct Day { + value: u16, +} + +impl Day { + pub fn ordinal0(&self) -> u16 { + assert!(self.value >= 1); + self.value - 1 + } + + pub fn ordinal(&self) -> u16 { + assert!(self.value >= 1); + self.value + } +} + +// TEST NOTE: previously a false alarm (raw field synthesis generates value == 0); +// with mined-invariant assumption, PASSES. +pub fn day_user(d: Day) -> u16 { + d.ordinal0() +} + +// A method-local precondition asserted in only ONE method: must NOT be mined +// (frequency filter), so the false alarm on prec_user remains — honest behavior. +pub struct Gauge { + level: u8, +} + +impl Gauge { + pub fn drain(&self) -> u8 { + assert!(self.level >= 10, "drain requires level >= 10"); + self.level - 10 + } +} + +// TEST NOTE: still FAILS (assert in drain is not mined as an invariant). +pub fn prec_user(g: Gauge) -> u8 { + g.drain() +} + +// TEST NOTE (--check-invariants): makes an INVALID Day (value == 0) — the mined-invariant +// output check must FAIL on this function. +pub fn buggy_make_day(seed: u16) -> Day { + Day { value: seed % 366 } // BUG: yields 0 when seed % 366 == 0; invariant needs 1..=366 +} + +// TEST NOTE (--check-invariants): correct producer — output check must PASS. +pub fn good_make_day(seed: u16) -> Day { + Day { value: (seed % 366) + 1 } +} + +// --- V2 cases --- + +// Getter-based invariant: the assert goes through self.level() (pure getter) — with +// one-level getter inlining, this mines like a direct field read (2 methods → invariant). +pub struct Tank { + level: u8, +} + +impl Tank { + pub fn level(&self) -> u8 { + self.level + } + pub fn a(&self) -> u8 { + assert!(self.level() <= 100); + self.level + } + pub fn b(&self) -> u8 { + assert!(self.level() <= 100); + 100 - self.level + } +} + +// TEST NOTE: previously a false alarm; with getter-inlined mining, PASSES. +pub fn tank_user(t: Tank) -> u8 { + t.b() +} + +// Result-returning producer: the mined Day invariant must be checked on the Ok payload; +// this buggy producer FAILS; Err returns pass vacuously. +pub fn buggy_try_make_day(seed: u16) -> Result { + if seed > 1000 { Err(()) } else { Ok(Day { value: seed % 366 }) } +} + +// TEST NOTE: correct Result producer — Ok payload valid, Err returns vacuously pass. +pub fn good_try_make_day(seed: u16) -> Result { + if seed > 1000 { Err(()) } else { Ok(Day { value: (seed % 366) + 1 }) } +} + +// Enum whose variant invariant (Cm value <= 100) is asserted in two methods via match: +// mined as a variant-guarded conjunct. +pub enum Length { + Cm(u8), + Inch(u8), +} + +impl Length { + pub fn cm_a(&self) -> u8 { + match self { + Length::Cm(v) => { + assert!(*v <= 100); + *v + } + Length::Inch(v) => *v, + } + } + pub fn cm_b(&self) -> u8 { + match self { + Length::Cm(v) => { + assert!(*v <= 100); + 100 - *v + } + Length::Inch(v) => *v, + } + } +} + +// TEST NOTE: previously a false alarm (generated Cm values above 100); with the +// variant-guarded mined conjunct assumed, PASSES. +pub fn length_user(l: Length) -> u8 { + l.cm_b() +} diff --git a/tests/script-based-pre/cargo_autoharness_vec_unbounded/Cargo.toml b/tests/script-based-pre/cargo_autoharness_vec_unbounded/Cargo.toml new file mode 100644 index 000000000000..94fdfd354943 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_vec_unbounded/Cargo.toml @@ -0,0 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "cargo_autoharness_vec_unbounded" +version = "0.1.0" +edition = "2021" diff --git a/tests/script-based-pre/cargo_autoharness_vec_unbounded/config.yml b/tests/script-based-pre/cargo_autoharness_vec_unbounded/config.yml new file mode 100644 index 000000000000..0f091d17fae0 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_vec_unbounded/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: vec.sh +expected: vec.expected +exit_code: 1 diff --git a/tests/script-based-pre/cargo_autoharness_vec_unbounded/src/lib.rs b/tests/script-based-pre/cargo_autoharness_vec_unbounded/src/lib.rs new file mode 100644 index 000000000000..66d4a8632e12 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_vec_unbounded/src/lib.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Vec arguments with qualifying element types (integers/floats) are generated +//! *unbounded*: results hold for all lengths, without --bounded-arguments and without the +//! "(bounded)" marker. Loops over the Vec surface insufficient unwinding bounds as +//! unwinding-assertion failures (c.f. `total`). Other element types keep needing +//! BoundedArbitrary support. + +// TEST NOTE: should PASS for ALL lengths (loop-free). +pub fn head(v: Vec) -> Option { + v.first().copied() +} + +// TEST NOTE: should PASS, and all cover checks must be SATISFIED (lengths beyond any +// bound and full content ranges are generated). +pub fn coverage(v: Vec) { + kani::cover!(v.len() > 100_000, "large lengths reachable"); + kani::cover!(!v.is_empty() && v[0] == i32::MIN, "extreme content reachable"); + kani::cover!(v.is_empty(), "empty vec reachable"); +} + +// TEST NOTE: should FAIL with an unwinding assertion: the Vec is unbounded, so the default +// loop bound cannot cover it — the incompleteness is signaled rather than silent. +pub fn total(v: Vec) -> u64 { + v.iter().map(|&b| b as u64).sum() +} + +// TEST NOTE: should PASS for ALL lengths: mutable slices are also unbounded (fresh +// exclusive allocations), and writes through them verify. +pub fn set_first(s: &mut [u8]) { + if !s.is_empty() { + s[0] = 42; + assert_eq!(s[0], 42); + } +} diff --git a/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.expected b/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.expected new file mode 100644 index 000000000000..78aff92666e3 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.expected @@ -0,0 +1,9 @@ +- Status: SATISFIED +- Status: SATISFIED +- Status: SATISFIED +Failed Checks: unwinding assertion loop 0 +| cargo_autoharness_vec_unbounded | coverage | #[kani::proof] | Success | +| cargo_autoharness_vec_unbounded | head | #[kani::proof] | Success | +| cargo_autoharness_vec_unbounded | set_first | #[kani::proof] | Success | +| cargo_autoharness_vec_unbounded | total | #[kani::proof] | Failure | +Complete - 3 successfully verified functions, 1 failures, 4 total. diff --git a/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.sh b/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.sh new file mode 100755 index 000000000000..16060e2fd373 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_vec_unbounded/vec.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoharness -Z autoharness --output-format=regular