diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 9395399cfe3..6e8b39d8706 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -925,6 +925,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; @@ -1365,6 +1453,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 7ee2df565ea..c2637cc5e2e 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -113,6 +113,19 @@ impl CodegenUnits { *kani_fns.get(&KaniModel::Any.into()).unwrap(), *kani_fns.get(&KaniModel::BoundedAny.into()).unwrap(), SmartPointerModels::from_kani_functions(kani_fns), + // Require *all three* unbounded models: eligibility admits `&[T]`, `&mut [T]` + // and `Vec`, but generation resolves each model independently, so gating on + // only one could report a `&mut [T]`/`Vec` arg as unbounded-verified while + // generation silently fell back to a bounded (or unsupported) path. They are + // defined together (all present with `alloc`, all absent in `no_core`), so this + // is all-or-nothing in practice; the conjunction just makes that explicit. + [ + KaniModel::AnySliceRefUnbounded, + KaniModel::AnySliceMutUnbounded, + KaniModel::AnyVecUnbounded, + ] + .iter() + .all(|m| kani_fns.contains_key(&(*m).into())), ); AUTOHARNESS_MD .set(AutoHarnessMetadata { @@ -685,6 +698,7 @@ fn automatic_harness_partition( kani_any_def: FnDef, kani_bounded_any_def: FnDef, smart_pointer_models: SmartPointerModels, + unbounded_slice_available: bool, ) -> (Vec<(Instance, AutoHarnessCaveats)>, BTreeMap) { let crate_fn_defs = rustc_public::local_crate().fn_defs().into_iter().collect::>(); // Filter out CrateItems that are functions, but not functions defined in the crate itself, i.e., rustc-inserted functions @@ -766,6 +780,26 @@ fn automatic_harness_partition( let mut problematic_args = vec![]; let mut bounded_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 -- unbounded, so no bound caveat), when the + // optional alloc-requiring models are present. This takes precedence over the + // bounded slice/string support classified by `autoharness_supported_arg_ty`. + 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; + } + } // Note: we deliberately do not insert the verdict into `ty_arbitrary_cache` here. // The cache stores whether a type implements (or can derive) Arbitrary, which is the // wrong semantics for types that are supported in argument position only (raw diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 03377297321..8d81089774e 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 = "AnyArcModel")] @@ -157,6 +163,8 @@ pub enum KaniHook { AnyRaw, #[strum(serialize = "AssertHook")] Assert, + #[strum(serialize = "SliceValidityAssumeHook")] + SliceValidityAssume, #[strum(serialize = "AssumeHook")] Assume, #[strum(serialize = "CheckHook")] @@ -191,11 +199,19 @@ pub enum KaniHook { } impl KaniModel { - /// Whether this model may legitimately be absent. The smart-pointer 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. + /// 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::AnyArc | KaniModel::AnyBox | KaniModel::AnyRc) + matches!( + self, + KaniModel::AnyArc + | KaniModel::AnyBox + | KaniModel::AnyRc + | KaniModel::AnySliceMutUnbounded + | KaniModel::AnySliceRefUnbounded + | KaniModel::AnyVecUnbounded + ) } } diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index ed05689f924..e08db06636f 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -630,6 +630,61 @@ fn to_fn_def(tcx: TyCtxt, def_id: rustc_span::def_id::DefId) -> Option { } } +/// If `ty` is `Vec` with the default allocator, return `T`. +pub fn vec_elem_ty(ty: Ty) -> Option { + let TyKind::RigidTy(RigidTy::Adt(def, ref args)) = ty.kind() else { return None }; + let name = def.name(); + if name != "std::vec::Vec" && name != "alloc::vec::Vec" { + return None; + } + // Vec: only the default allocator is supported (the model allocates via + // the global allocator). The allocator parameter is defaulted, so a crate naming a + // custom allocator produces a second type argument != Global. + let mut ty_args = args.0.iter().filter_map(|a| match a { + GenericArgKind::Type(t) => Some(*t), + _ => None, + }); + let elem = ty_args.next()?; + // Only the default `Global` allocator is supported. Match the allocator type exactly rather + // than by substring, so a custom allocator whose name merely contains "Global" (e.g. + // `MyGlobalAlloc`) is not misclassified as the default. + if let Some(alloc_ty) = ty_args.next() { + let is_global = matches!( + alloc_ty.kind(), + TyKind::RigidTy(RigidTy::Adt(def, _)) + if matches!(def.name().as_str(), "std::alloc::Global" | "alloc::alloc::Global") + ); + if !is_global { + return None; + } + } + Some(elem) +} + +/// Whether `&[T]` arguments with this element type qualify for *unbounded* generation +/// (`KaniModel::AnySliceRefUnbounded`): raw nondeterministic memory must be a sound AND +/// complete model of the element's values *without any validity assumption*, i.e. every bit +/// pattern must be a valid element. This holds exactly for the primitive integer and float +/// types. +/// +/// Types with validity constraints (bool, char, NonZero, ranged newtypes) are excluded even +/// though the `SliceValidityAssume` hook can express byte-width niche constraints: CBMC's +/// default (SAT) backend only instantiates quantifiers with *constant* bounds, and silently +/// degrades symbolic-bound quantifiers to unconstrained free variables +/// (`boolbvt::finish_eager_conversion_quantifiers` -> `conversion_failed`), which would make +/// the validity assumption vacuous. SMT backends (e.g. `--solver z3`) handle the quantified +/// assumption, including multi-byte elements; routing niched element types here can be +/// revisited when CBMC's SAT backend learns symbolic-bound instantiation or Kani selects +/// backends per harness. +pub fn slice_elem_unbounded_ok(_tcx: TyCtxt, ty: Ty) -> bool { + matches!( + ty.kind(), + TyKind::RigidTy(RigidTy::Int(_)) + | TyKind::RigidTy(RigidTy::Uint(_)) + | TyKind::RigidTy(RigidTy::Float(_)) + ) +} + /// The niche constraint of a scalar-ABI type: the width of the scalar in bits, and the /// (possibly wrapping) inclusive range of valid bit patterns. /// Returns None for non-scalar ABIs, pointer/float scalars, and scalars whose valid range diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index e37361a6736..1dafd08897c 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -9,7 +9,7 @@ use crate::args::ReachabilityType; use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; -use crate::kani_middle::kani_functions::{KaniHook, KaniIntrinsic, KaniModel}; +use crate::kani_middle::kani_functions::{KaniFunction, KaniHook, KaniIntrinsic, KaniModel}; use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_middle::{ @@ -60,6 +60,8 @@ struct AnyModels { kani_bounded_any: FnDef, /// The (optional) smart-pointer generation models (`Box`/`Rc`/`Arc`). smart_pointer_models: SmartPointerModels, + /// The (optional, alloc-requiring) unbounded slice/`Vec` generation models. + unbounded_models: UnboundedModels, } impl AnyModels { @@ -75,6 +77,7 @@ impl AnyModels { kani_assume_safe: *kani_fns.get(&KaniModel::AssumeSafe.into()).unwrap(), kani_bounded_any: *kani_fns.get(&KaniModel::BoundedAny.into()).unwrap(), smart_pointer_models: SmartPointerModels::from_kani_functions(kani_fns), + unbounded_models: UnboundedModels::from_kani_functions(kani_fns), } } } @@ -753,6 +756,55 @@ fn assume_scalar_niche( ); } +/// The (optional, alloc-requiring) unbounded generation models, resolved per argument type. +#[derive(Debug, Clone, Copy, 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) + } + }; + let instance = + Instance::resolve(def, &GenericArgs(vec![GenericArgKind::Type(elem)])).ok()?; + // Only use the model if its return type matches `ty` exactly (mirrors + // `smart_pointer_model_instance`): guards against generating an ill-typed value if the + // model's signature ever skews from the argument type (e.g. a `Vec` with a + // non-`Global` allocator that slipped past `vec_elem_ty`). + let ret_ty = instance.ty().kind().fn_sig()?.skip_binder().output(); + (ret_ty == ty).then_some(instance) + } +} + fn call_kani_any_for_ty( tcx: TyCtxt, models: AnyModels, @@ -762,6 +814,14 @@ fn call_kani_any_for_ty( source: &mut SourceInstruction, invariant_cache: &mut FxHashMap, ) -> 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) = models.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() && matches!( inner_ty.kind(), diff --git a/library/kani/build.rs b/library/kani/build.rs index c094cc0254c..8c61c2b020d 100644 --- a/library/kani/build.rs +++ b/library/kani/build.rs @@ -4,4 +4,8 @@ fn main() { // Make sure `kani_sysroot` is a recognized config println!("cargo::rustc-check-cfg=cfg(kani_sysroot)"); + // `kani` is set by the Kani compiler when verifying user code; recognize it here so that + // verification-only hook bodies can gate on `cfg(not(kani))` without tripping the + // `unexpected_cfgs` lint during the library's own build. + println!("cargo::rustc-check-cfg=cfg(kani)"); } diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 7666325cdaf..a109fc76f04 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -70,3 +70,105 @@ 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` equal to the allocated element count (`len.max(1)` +/// for non-ZSTs, since the allocation uses `Layout::array::(len.max(1))` to avoid a +/// zero-sized allocation; `usize::MAX` for ZSTs). The allocation thus came from the global +/// allocator with exactly the layout `Vec`'s safety contract requires for `capacity`, so `Vec` +/// frees it correctly on drop. +/// +/// This model is used by the compiler to generate nondeterministic `Vec` arguments for +/// automatic harnesses (`kani autoharness`) when the element type qualifies; verification +/// results hold for ALL lengths. Optional: requires `alloc`. +#[kanitool::fn_marker = "AnyVecUnboundedModel"] +#[inline(never)] +#[doc(hidden)] +pub fn any_vec_unbounded() -> Vec { + let len: usize = crate::any(); + let elem = std::mem::size_of::(); + if elem == 0 { + // For ZSTs, Vec never allocates and uses a dangling pointer; constructing from a + // dangling pointer with any len is the documented pattern (and loop-free, which + // matters: generation code must not itself be bounded by unwinding). + return unsafe { + Vec::from_raw_parts(std::ptr::NonNull::dangling().as_ptr(), len, usize::MAX) + }; + } + crate::assume(len <= (isize::MAX as usize) / elem); + let layout = std::alloc::Layout::array::(len.max(1)).unwrap(); + let ptr = unsafe { std::alloc::alloc(layout) }; + crate::assume(!ptr.is_null()); + slice_validity_assume::(ptr, len); + unsafe { Vec::from_raw_parts(ptr as *mut T, len, len.max(1)) } +} + +/// Compiler hook (c.f. `KaniHook::SliceValidityAssume`): assume that every element of the +/// `len`-element `T`-array at `ptr` has raw bits within `T`'s layout niche. Lowered directly +/// to a quantified goto assumption; a no-op when `T` has no niche. The default body is +/// unreachable: calls are always intercepted during code generation. +#[kanitool::fn_marker = "SliceValidityAssumeHook"] +#[inline(never)] +#[doc(hidden)] +pub fn slice_validity_assume(_ptr: *const u8, _len: usize) { + #[cfg(not(kani))] + unreachable!("kani::slice_validity_assume is a verification-only hook"); +} diff --git a/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected b/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected index 6f6a94b3311..a19b87660d9 100644 --- a/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected +++ b/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected @@ -6,9 +6,9 @@ Status: SATISFIED\ Description: "max-length vec with specific contents" | cargo_autoharness_bounded | packet_check | #[kani::proof] (bounded) | Success | | cargo_autoharness_bounded | string_head | #[kani::proof] (bounded) | Success | -| cargo_autoharness_bounded | vec_cover | #[kani::proof] (bounded) | Success | -| cargo_autoharness_bounded | vec_sum | #[kani::proof] (bounded) | Success | +| cargo_autoharness_bounded | vec_cover | #[kani::proof] | Success | | cargo_autoharness_bounded | string_first_byte | #[kani::proof] (bounded) | Failure | -| cargo_autoharness_bounded | vec_first | #[kani::proof] (bounded) | Failure | +| cargo_autoharness_bounded | vec_first | #[kani::proof] | Failure | +| cargo_autoharness_bounded | vec_sum | #[kani::proof] | Failure | Note: harnesses marked "(bounded)" use bounded nondeterministic values for some arguments (--bounded-arguments); -Complete - 4 successfully verified functions, 2 failures, 6 total. +Complete - 3 successfully verified functions, 3 failures, 6 total. diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected index b7cbf3029a9..09b71fcd488 100644 --- a/tests/script-based-pre/cargo_autoharness_filter/filter.expected +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected @@ -1,7 +1,13 @@ -Kani generated automatic harnesses for 47 function(s): +Kani generated automatic harnesses for 50 function(s): +--------------------------+----------------------------------------------+ | Crate | Selected Function | +=========================================================================+ +| cargo_autoharness_filter | no_harness::unsupported_no_arg_name | +|--------------------------+----------------------------------------------| +| cargo_autoharness_filter | no_harness::unsupported_slice | +|--------------------------+----------------------------------------------| +| cargo_autoharness_filter | no_harness::unsupported_vec | +|--------------------------+----------------------------------------------| | cargo_autoharness_filter | yes_harness::empty_body | |--------------------------+----------------------------------------------| | cargo_autoharness_filter | yes_harness::f_array | @@ -97,22 +103,19 @@ Kani generated automatic harnesses for 47 function(s): | cargo_autoharness_filter | yes_harness::f_usize | +--------------------------+----------------------------------------------+ -Kani did not generate automatic harnesses for 4 function(s). +Kani did not generate automatic harnesses for 1 function(s). If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832 +--------------------------+----------------------------------------+----------------------------------------------------------------------------------+ | Crate | Skipped Function | Reason for Skipping | +======================================================================================================================================================+ | cargo_autoharness_filter | no_harness::doesnt_implement_arbitrary | Missing Arbitrary implementation for argument(s) x: DoesntImplementArbitrary<'_> | -|--------------------------+----------------------------------------+----------------------------------------------------------------------------------| -| cargo_autoharness_filter | no_harness::unsupported_no_arg_name | Requires --bounded-arguments for argument(s) _: std::vec::Vec | -|--------------------------+----------------------------------------+----------------------------------------------------------------------------------| -| cargo_autoharness_filter | no_harness::unsupported_slice | Requires --bounded-arguments for argument(s) _y: &[u8] | -|--------------------------+----------------------------------------+----------------------------------------------------------------------------------| -| cargo_autoharness_filter | no_harness::unsupported_vec | Requires --bounded-arguments for argument(s) _y: std::vec::Vec | +--------------------------+----------------------------------------+----------------------------------------------------------------------------------+ +Autoharness: Checking function no_harness::unsupported_no_arg_name against all possible inputs... +Autoharness: Checking function no_harness::unsupported_slice against all possible inputs... +Autoharness: Checking function no_harness::unsupported_vec against all possible inputs... +Autoharness: Checking function yes_harness::f_generic:: against all possible inputs... Autoharness: Checking function yes_harness::f_mut_pointer against all possible inputs... Autoharness: Checking function yes_harness::f_const_pointer against all possible inputs... -Autoharness: Checking function yes_harness::f_generic:: against all possible inputs... Autoharness: Checking function yes_harness::f_ref against all possible inputs... Autoharness: Checking function yes_harness::empty_body against all possible inputs... Autoharness: Checking function yes_harness::f_phantom_pinned against all possible inputs... @@ -165,6 +168,12 @@ Autoharness Summary: +--------------------------+----------------------------------------------+---------------------------+---------------------+ | Crate | Selected Function | Kind of Automatic Harness | Verification Result | +===========================================================================================================================+ +| cargo_autoharness_filter | no_harness::unsupported_no_arg_name | #[kani::proof] | Success | +|--------------------------+----------------------------------------------+---------------------------+---------------------| +| cargo_autoharness_filter | no_harness::unsupported_slice | #[kani::proof] | Success | +|--------------------------+----------------------------------------------+---------------------------+---------------------| +| cargo_autoharness_filter | no_harness::unsupported_vec | #[kani::proof] | Success | +|--------------------------+----------------------------------------------+---------------------------+---------------------| | cargo_autoharness_filter | yes_harness::empty_body | #[kani::proof] | Success | |--------------------------+----------------------------------------------+---------------------------+---------------------| | cargo_autoharness_filter | yes_harness::f_array | #[kani::proof] | Success | @@ -259,4 +268,4 @@ Autoharness Summary: |--------------------------+----------------------------------------------+---------------------------+---------------------| | cargo_autoharness_filter | yes_harness::f_usize | #[kani::proof] | Success | +--------------------------+----------------------------------------------+---------------------------+---------------------+ -Complete - 47 successfully verified functions, 0 failures, 47 total. +Complete - 50 successfully verified functions, 0 failures, 50 total. diff --git a/tests/script-based-pre/cargo_autoharness_slices/slices.expected b/tests/script-based-pre/cargo_autoharness_slices/slices.expected index 130f479befc..249a4ca7f87 100644 --- a/tests/script-based-pre/cargo_autoharness_slices/slices.expected +++ b/tests/script-based-pre/cargo_autoharness_slices/slices.expected @@ -12,12 +12,12 @@ Description: "3-byte string starting with 'a'" Status: SATISFIED\ Description: "string starting with a non-ASCII char" | cargo_autoharness_slices | count_a | #[kani::proof] (bounded) | Success | -| cargo_autoharness_slices | slice_cover | #[kani::proof] (bounded) | Success | +| cargo_autoharness_slices | slice_cover | #[kani::proof] | Success | | cargo_autoharness_slices | str_cover | #[kani::proof] (bounded) | Success | -| cargo_autoharness_slices | sum | #[kani::proof] (bounded) | Success | +| cargo_autoharness_slices | sum | #[kani::proof] | Success | | cargo_autoharness_slices | sum_derivable | #[kani::proof] (bounded) | Success | -| cargo_autoharness_slices | zero_all | #[kani::proof] (bounded) | Success | -| cargo_autoharness_slices | first | #[kani::proof] (bounded) | Failure | +| cargo_autoharness_slices | zero_all | #[kani::proof] | Success | +| cargo_autoharness_slices | first | #[kani::proof] | Failure | | cargo_autoharness_slices | first_byte | #[kani::proof] (bounded) | Failure | Note: harnesses marked "(bounded)" use bounded nondeterministic values for some arguments (--bounded-arguments); Complete - 6 successfully verified functions, 2 failures, 8 total. 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 00000000000..94fdfd35494 --- /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 00000000000..0f091d17fae --- /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 00000000000..66d4a8632e1 --- /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 00000000000..78aff92666e --- /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 00000000000..16060e2fd37 --- /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