diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index a1376d8fdd2..0bfbcc1ad43 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -165,17 +165,26 @@ smaller bound reflects the cost of reasoning about UTF-8 for symbolic execution. chosen to stay below the default loop-unwinding bound of 20, so that loops over the slice can be fully unwound by default. +Additionally (also requiring `--bounded-arguments`), for arguments whose type implements +[`BoundedArbitrary`](../bounded_arbitrary.md) +(e.g. `Vec`, `String`, or user types deriving it), the harness generates a bounded +nondeterministic value with **bound 4** (via `kani::bounded_any`). The same caveat applies: +verification results only hold up to the bound. The smaller bound reflects that these values are +heap allocated and, for `String`, involve UTF-8 reasoning, both of which are costly for symbolic +execution. + Nested slice references (e.g. `&&[u8]`) and slices inside user-defined types remain unsupported. ## Limitations ### Arguments Implementing Arbitrary Kani will only generate an automatic harness for a function if it can represent each of its arguments nondeterministically. -By default, it must be able to do so *without bounds*; the `--bounded-arguments` option (see above) relaxes this to -additionally allow argument types that can only be represented up to a bound, such as slice (`&[T]`/`&mut [T]`) and -string (`&str`) references. -In technical terms, each of the arguments needs to implement the `Arbitrary` +By default, it must be able to do so *without bounds*: each argument needs to implement the `Arbitrary` trait or be capable of deriving it, or be a reference (mutable or immutable) where any of the prior requirements is fulfilled by the referenced type. +The `--bounded-arguments` option (see above) relaxes this to +additionally allow argument types that can only be represented up to a bound: slice (`&[T]`/`&mut [T]`) and +string (`&str`) references, and types implementing [`BoundedArbitrary`](../bounded_arbitrary.md) +(e.g. `Vec`, `String`, or user types deriving it). Kani will detect if a struct or enum could implement `Arbitrary` and derive it automatically. Note that this automatic derivation feature is only available for autoharness. diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index bd20dbc30a2..39ac29f260f 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -108,6 +108,7 @@ impl CodegenUnits { args, &crate_info.name, *kani_fns.get(&KaniModel::Any.into()).unwrap(), + *kani_fns.get(&KaniModel::BoundedAny.into()).unwrap(), ); AUTOHARNESS_MD .set(AutoHarnessMetadata { @@ -524,6 +525,7 @@ fn automatic_harness_partition( args: &Arguments, crate_name: &str, kani_any_def: FnDef, + kani_bounded_any_def: FnDef, ) -> (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 @@ -563,6 +565,7 @@ fn automatic_harness_partition( if is_proof_harness(tcx, instance) || name.contains("kani::Arbitrary") + || name.contains("kani::BoundedArbitrary") || name.contains("kani::Invariant") { return Err(AutoHarnessSkipReason::KaniImpl); @@ -574,8 +577,8 @@ fn automatic_harness_partition( // Each argument of `instance` must be supported by automatic harness generation, i.e., // implement Arbitrary (or be capable of deriving it), be a raw pointer, or -- if the user - // opted in via --bounded-arguments -- be a supported slice/string reference, - // c.f. `autoharness_supported_arg_ty`. + // opted in via --bounded-arguments -- be a supported slice/string reference or a + // BoundedArbitrary container type, c.f. `autoharness_supported_arg_ty`. // Note that generic functions have been instantiated with concrete types at this point, // so we know that each of these arguments has a concrete type. let mut problematic_args = vec![]; @@ -584,12 +587,17 @@ fn automatic_harness_partition( // 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 - // pointers, and slice/string references whose backing storage the harness owns): - // caching the argument-position verdict under the same key would poison the cache for - // the ADT-field checks. `implements_arbitrary` memoizes its own recursion internally, - // so repeated argument types stay cheap. - let support = - autoharness_supported_arg_ty(arg.ty, kani_any_def, &mut ty_arbitrary_cache); + // pointers, slice/string references whose backing storage the harness owns, and + // BoundedArbitrary container types): caching the argument-position verdict under the + // same key would poison the cache for the ADT-field checks. `implements_arbitrary` + // memoizes its own recursion internally, so repeated argument types stay cheap. + let support = autoharness_supported_arg_ty( + tcx, + arg.ty, + kani_any_def, + kani_bounded_any_def, + &mut ty_arbitrary_cache, + ); if support == ArgSupport::Arbitrary { continue; diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index b4ea258288a..6b7cc8da30d 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -75,6 +75,8 @@ pub enum KaniModel { AnyStrRef, #[strum(serialize = "AssumeSafeModel")] AssumeSafe, + #[strum(serialize = "BoundedAnyModel")] + BoundedAny, #[strum(serialize = "CopyInitStateModel")] CopyInitState, #[strum(serialize = "CopyInitStateSingleModel")] diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 62e301ee9b0..407b89ea803 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -13,7 +13,8 @@ use rustc_public::mir::mono::{Instance, MonoItem}; use rustc_public::mir::{Mutability, TerminatorKind}; use rustc_public::rustc_internal; use rustc_public::ty::{ - AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Span as SpanStable, Ty, TyKind, + AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Span as SpanStable, Ty, TyConst, + TyKind, }; use rustc_public::visitor::{Visitable, Visitor as TyVisitor}; use rustc_public::{CrateDef, DefId, local_crate}; @@ -348,6 +349,53 @@ fn implements_invariant( res } +/// Whether `ty` is statically sized. Nondeterministic-value generation (and the resolution +/// checks probing for it) must not instantiate generic models with unsized types: apart from +/// being ungeneratable, this can crash constant evaluation during body retrieval. +fn ty_is_sized(tcx: TyCtxt, ty: Ty) -> bool { + rustc_internal::internal(tcx, ty) + .is_sized(*tcx.at(rustc_span::DUMMY_SP), rustc_middle::ty::TypingEnv::fully_monomorphized()) +} + +/// Inspect a `kani::bounded_any::()` (c.f. `KaniModel::BoundedAny`) instantiation to +/// determine if `T: BoundedArbitrary`. The model looks like: +/// ```rust +/// fn bounded_any() -> T { +/// T::bounded_any::() +/// } +/// ``` +/// So we select the terminator that calls `T::bounded_any::()`, then try to resolve it to an +/// Instance; `T` implements `BoundedArbitrary` iff we successfully resolve the Instance +/// (mirroring `implements_arbitrary`). +fn implements_bounded_arbitrary(tcx: TyCtxt, ty: Ty, kani_bounded_any_def: FnDef) -> bool { + if ty.kind().rigid().is_none() || !ty_is_sized(tcx, ty) { + return false; + } + + let args = GenericArgs(vec![ + GenericArgKind::Type(ty), + GenericArgKind::Const(TyConst::try_from_target_usize(1).unwrap()), + ]); + let Ok(instance) = Instance::resolve(kani_bounded_any_def, &args) else { + return false; + }; + let Some(body) = instance.body() else { + return false; + }; + + for bb in body.blocks.iter() { + let TerminatorKind::Call { func, .. } = &bb.terminator.kind else { + continue; + }; + if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = + func.ty(body.arg_locals()).unwrap().kind() + { + return Instance::resolve(def, &args).is_ok(); + } + } + false +} + /// Is `ty` a struct or enum whose fields/variants implement Arbitrary, or a reference to such a /// type? fn can_derive_arbitrary( @@ -422,15 +470,20 @@ pub enum ArgSupport { /// - slice references (`&[T]`/`&mut [T]`, provided `T` implements or can derive `Arbitrary`) and /// string slices (`&str`): for those, the harness generates a slice of *bounded* nondeterministic /// length backed by harness-local storage, c.f. `KaniModel::AnySliceRef` and -/// `KaniModel::AnyStrRef`. +/// `KaniModel::AnyStrRef` (reported as [ArgSupport::Bounded]); +/// - types that implement `BoundedArbitrary` (e.g. `Vec`, `String`, or user types deriving +/// it): the harness generates a bounded nondeterministic value via `KaniModel::BoundedAny` +/// (reported as [ArgSupport::Bounded]). /// /// Note that raw pointers and slice/string references are only supported as immediate harness /// arguments (raw pointers also through other raw pointers): such a type behind a reference or /// inside an ADT remains unsupported, since the pointee/backing storage that the generated harness /// allocates would not outlive the generated value. fn autoharness_supported_arg_ty( + tcx: TyCtxt, ty: Ty, kani_any_def: FnDef, + kani_bounded_any_def: FnDef, ty_arbitrary_cache: &mut FxHashMap, ) -> ArgSupport { let arbitrary_or_derive = |ty: Ty, cache: &mut FxHashMap| { @@ -446,7 +499,13 @@ fn autoharness_supported_arg_ty( if let TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _)) = ty.kind() { // A raw pointer is supported as long as its pointee is: propagate the pointee's verdict, // so a pointer to a bounded pointee (e.g. `*mut &[T]`) is itself reported as bounded. - autoharness_supported_arg_ty(inner_ty, kani_any_def, ty_arbitrary_cache) + autoharness_supported_arg_ty( + tcx, + inner_ty, + kani_any_def, + kani_bounded_any_def, + ty_arbitrary_cache, + ) } else if let TyKind::RigidTy(RigidTy::Ref(_, inner_ty, inner_mutability)) = ty.kind() { match inner_ty.kind() { TyKind::RigidTy(RigidTy::Slice(elem_ty)) => { @@ -468,6 +527,12 @@ fn autoharness_supported_arg_ty( _ => arbitrary_or_derive(ty, ty_arbitrary_cache), } } else { - arbitrary_or_derive(ty, ty_arbitrary_cache) + if arbitrary_or_derive(ty, ty_arbitrary_cache) == ArgSupport::Arbitrary { + ArgSupport::Arbitrary + } else if implements_bounded_arbitrary(tcx, ty, kani_bounded_any_def) { + ArgSupport::Bounded + } else { + ArgSupport::Unsupported + } } } diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index cabf24ebe37..6417b485326 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -12,7 +12,7 @@ use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::kani_functions::{KaniHook, KaniIntrinsic, KaniModel}; use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use crate::kani_middle::transform::{TransformPass, TransformationType}; -use crate::kani_middle::{implements_arbitrary, implements_invariant}; +use crate::kani_middle::{can_derive_arbitrary, implements_arbitrary, implements_invariant}; use crate::kani_queries::QueryDb; use rustc_data_structures::fx::FxHashMap; use rustc_middle::ty::TyCtxt; @@ -44,6 +44,8 @@ struct AnyModels { kani_any_str_ref: FnDef, /// The FnDef of KaniModel::AssumeSafe kani_assume_safe: FnDef, + /// The FnDef of KaniModel::BoundedAny + kani_bounded_any: FnDef, } impl AnyModels { @@ -55,6 +57,7 @@ impl AnyModels { kani_any_slice_ref: *kani_fns.get(&KaniModel::AnySliceRef.into()).unwrap(), kani_any_str_ref: *kani_fns.get(&KaniModel::AnyStrRef.into()).unwrap(), kani_assume_safe: *kani_fns.get(&KaniModel::AssumeSafe.into()).unwrap(), + kani_bounded_any: *kani_fns.get(&KaniModel::BoundedAny.into()).unwrap(), } } } @@ -122,7 +125,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| { @@ -145,8 +148,8 @@ impl TransformPass for AutomaticArbitraryPass { if let TyKind::RigidTy(RigidTy::Adt(def, args)) = ty.kind() { 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 { @@ -172,6 +175,14 @@ const AUTOHARNESS_SLICE_BOUND: u64 = 16; /// not time out should raise `--harness-timeout`). const AUTOHARNESS_STR_BOUND: u64 = 4; +/// The bound for nondeterministic values of types that implement `BoundedArbitrary` (rather +/// than `Arbitrary`) that automatic harnesses generate, e.g. `Vec` or `String`. +/// Verification results for functions with such arguments are only valid up to this bound. +/// This is smaller than the slice/str bounds since `BoundedArbitrary` values are heap +/// allocated, and for `String` additionally involve UTF-8 reasoning; a bound of 8 already +/// makes simple `String` harnesses exceed Kani's default 60s harness timeout. +const AUTOHARNESS_BOUNDED_ANY_BOUND: u64 = 4; + /// For raw pointer types, insert a call to the `KaniModel::AnyPtr` model instead, which generates /// a pointer in a nondeterministic allocation state (null, out of bounds, or valid); /// in the valid case, the pointer points to a nondeterministic value stored in a dedicated local @@ -180,13 +191,17 @@ const AUTOHARNESS_STR_BOUND: u64 = 4; /// models instead, which return a slice of nondeterministic length (bounded by /// [AUTOHARNESS_SLICE_BOUND]) backed by a nondeterministic array stored in a dedicated local, /// which stays alive for the entire harness. +/// If `ty` does not implement `Arbitrary` (and cannot derive it) but implements `BoundedArbitrary` +/// (e.g. `Vec` or `String`), insert a call to the `KaniModel::BoundedAny` model, which returns +/// a *bounded* nondeterministic value (bounded by [AUTOHARNESS_BOUNDED_ANY_BOUND]). /// If `ty` is an ADT that implements `Invariant`, additionally insert a call to the /// `KaniModel::AssumeSafe` model (`kani_assume_safe`), which assumes that the nondeterministic /// value respects the type's safety invariant, c.f. /// . -/// Panics if `ty` does not implement Arbitrary (and is not a reference or raw pointer to such a -/// type, or a reference to a slice or str of such a type). +/// Panics if `ty` does not implement Arbitrary or BoundedArbitrary (and is not a reference or raw +/// pointer to such a type, or a reference to a slice or str of such a type). fn call_kani_any_for_ty( + tcx: TyCtxt, models: AnyModels, body: &mut MutableBody, ty: Ty, @@ -234,6 +249,7 @@ fn call_kani_any_for_ty( let elem_lcls = (0..bound) .map(|_| { call_kani_any_for_ty( + tcx, models, body, elem_ty, @@ -301,8 +317,15 @@ fn call_kani_any_for_ty( slice_lcl } } else if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind() { - let inner_lcl = - call_kani_any_for_ty(models, body, inner_ty, inner_mutability, source, invariant_cache); + let inner_lcl = call_kani_any_for_ty( + tcx, + models, + body, + inner_ty, + inner_mutability, + source, + invariant_cache, + ); let ref_lcl = body.new_local(ty, source.span(body.blocks()), mutability); let borrow_kind = if inner_mutability == Mutability::Not { BorrowKind::Shared @@ -320,8 +343,15 @@ fn call_kani_any_for_ty( // Generate the storage for the valid-pointer case: a local with a nondeterministic value // of the pointee type. Since it is a local of the body being transformed, it stays alive // for as long as that body executes. - let storage_lcl = - call_kani_any_for_ty(models, body, inner_ty, Mutability::Mut, source, invariant_cache); + let storage_lcl = call_kani_any_for_ty( + tcx, + models, + body, + inner_ty, + Mutability::Mut, + source, + invariant_cache, + ); // Pass a mutable reference to the storage to the AnyPtr model, which returns a `*mut T` // that is either null, out of bounds (one past the end), or pointing to the storage. @@ -367,16 +397,44 @@ fn call_kani_any_for_ty( ptr_lcl } } else { - let kani_any_inst = - Instance::resolve(models.kani_any, &GenericArgs(vec![GenericArgKind::Type(ty)])) - .unwrap_or_else(|_| panic!("expected a ty that implements Arbitrary, got {ty}")); + // Prefer an unbounded nondeterministic value via (implemented or compiler-derived) + // Arbitrary; fall back to BoundedArbitrary for container types like Vec or String. + // Note: use a fresh cache for the Arbitrary check -- `invariant_cache` memoizes a + // different predicate (Invariant), so the two must not share a map. + let mut arbitrary_cache = FxHashMap::default(); + let use_arbitrary = implements_arbitrary(ty, models.kani_any, &mut arbitrary_cache) + || can_derive_arbitrary(ty, models.kani_any, &mut arbitrary_cache); + let (model, generic_args) = if use_arbitrary { + (models.kani_any, GenericArgs(vec![GenericArgKind::Type(ty)])) + } else { + // `Instance::resolve` does not check trait bounds, so ensure the type actually + // implements BoundedArbitrary before emitting the call: an unresolvable + // `T::bounded_any` would otherwise only surface as an ICE during reachability. + assert!( + crate::kani_middle::implements_bounded_arbitrary(tcx, ty, models.kani_bounded_any), + "expected a ty that implements Arbitrary or BoundedArbitrary, got {ty}" + ); + ( + models.kani_bounded_any, + GenericArgs(vec![ + GenericArgKind::Type(ty), + GenericArgKind::Const( + TyConst::try_from_target_usize(AUTOHARNESS_BOUNDED_ANY_BOUND).unwrap(), + ), + ]), + ) + }; + let any_inst = Instance::resolve(model, &generic_args).unwrap_or_else(|_| { + panic!("expected a ty that implements Arbitrary or BoundedArbitrary, 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)); + body.insert_call(&any_inst, source, InsertPosition::Before, vec![], Place::from(lcl)); // If the type has a safety invariant, assume that it holds for the nondeterministic value. // We only check ADTs since those are the only types for which users can implement // `Invariant` in a way that constrains the values (the library's implementations for - // primitive types are trivially `true`). + // primitive types are trivially `true`). This applies regardless of whether the value was + // generated via Arbitrary or BoundedArbitrary. if matches!(ty.kind(), TyKind::RigidTy(RigidTy::Adt(..))) && implements_invariant(ty, models.kani_assume_safe, invariant_cache) { @@ -413,6 +471,7 @@ impl AutomaticArbitraryPass { #[allow(clippy::too_many_arguments)] fn call_kani_any_for_variant( &self, + tcx: TyCtxt, adt_def: AdtDef, adt_args: &GenericArgs, body: &mut MutableBody, @@ -427,6 +486,7 @@ 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( + tcx, self.models, body, ty, @@ -465,7 +525,7 @@ impl AutomaticArbitraryPass { /// _ => Enum::LastVariant /// } /// ``` - fn generate_enum_body(&self, def: AdtDef, args: GenericArgs, body: Body) -> Body { + fn generate_enum_body(&self, tcx: TyCtxt, def: AdtDef, args: GenericArgs, body: Body) -> Body { // Autoharness only deems a function with an enum eligible if it has at least one variant, c.f. `can_derive_arbitrary` assert!(def.num_variants() > 0); @@ -476,6 +536,7 @@ impl AutomaticArbitraryPass { // Generate a nondet u128 to switch on let discr_lcl = call_kani_any_for_ty( + tcx, self.models, &mut new_body, Ty::from_rigid_kind(RigidTy::Uint(UintTy::U128)), @@ -500,6 +561,7 @@ impl AutomaticArbitraryPass { for (idx, variant) in def.variants_iter().enumerate() { let variant_idx = VariantIdx::to_val(idx); let target_bb = self.call_kani_any_for_variant( + tcx, def, &args, &mut new_body, @@ -533,7 +595,13 @@ impl AutomaticArbitraryPass { /// ... /// } /// ``` - fn generate_struct_body(&self, def: AdtDef, args: GenericArgs, body: Body) -> Body { + fn generate_struct_body( + &self, + tcx: TyCtxt, + def: AdtDef, + args: GenericArgs, + body: Body, + ) -> Body { assert_eq!(def.num_variants(), 1); let mut new_body = MutableBody::from(body); @@ -544,6 +612,7 @@ impl AutomaticArbitraryPass { let variant = def.variants()[0]; // A struct has a single variant at index 0. self.call_kani_any_for_variant( + tcx, def, &args, &mut new_body, @@ -671,6 +740,7 @@ impl TransformPass for AutomaticHarnessPass { .iter() .map(|local_decl| { call_kani_any_for_ty( + tcx, self.models, &mut harness_body, local_decl.ty, diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 181eb9008eb..5dbfda083ae 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -302,6 +302,7 @@ macro_rules! kani_intrinsics { /// implementing BoundedArbitrary decides exactly what size means for them. /// /// *Note*: Any proof using a bounded symbolic value is only valid up to that bound. + #[kanitool::fn_marker = "BoundedAnyModel"] #[inline(always)] pub fn bounded_any() -> T { T::bounded_any::() diff --git a/tests/script-based-pre/cargo_autoharness_bounded/Cargo.toml b/tests/script-based-pre/cargo_autoharness_bounded/Cargo.toml new file mode 100644 index 00000000000..ca66247aca8 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_bounded/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_bounded" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected b/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected new file mode 100644 index 00000000000..6f6a94b3311 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_bounded/bounded.expected @@ -0,0 +1,14 @@ +[without --bounded-arguments] +Requires --bounded-arguments for argument(s) p: Packet +[with --bounded-arguments] +Missing Arbitrary implementation for argument(s) xs: std::vec::Vec> +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 | string_first_byte | #[kani::proof] (bounded) | Failure | +| cargo_autoharness_bounded | vec_first | #[kani::proof] (bounded) | Failure | +Note: harnesses marked "(bounded)" use bounded nondeterministic values for some arguments (--bounded-arguments); +Complete - 4 successfully verified functions, 2 failures, 6 total. diff --git a/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh b/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh new file mode 100755 index 00000000000..581b26d5f7d --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_bounded/bounded.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +echo "[without --bounded-arguments]" +# Capture the command status explicitly: piping straight into `grep` would mask a +# failure of `cargo kani ... --list` (the pipeline would report grep's status). +list_output=$(cargo kani autoharness -Z autoharness --list 2>&1) +echo "$list_output" | grep -m1 'Requires --bounded-arguments' + +echo "[with --bounded-arguments]" +# `string_head`/`string_first_byte` reason about UTF-8 over a bounded nondeterministic +# `String`, which is expensive; on slower CI runners it can exceed the autoharness default +# 60s harness timeout, so raise it here to keep these harnesses from spuriously timing out. +# This run reports failures (`vec_first`/`string_first_byte`), so it exits non-zero (see config.yml). +cargo kani autoharness -Z autoharness -Z unstable-options --bounded-arguments --harness-timeout 5m diff --git a/tests/script-based-pre/cargo_autoharness_bounded/config.yml b/tests/script-based-pre/cargo_autoharness_bounded/config.yml new file mode 100644 index 00000000000..830a5e4ae57 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_bounded/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: bounded.sh +expected: bounded.expected +exit_code: 1 diff --git a/tests/script-based-pre/cargo_autoharness_bounded/src/lib.rs b/tests/script-based-pre/cargo_autoharness_bounded/src/lib.rs new file mode 100644 index 00000000000..8db3f493e0a --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_bounded/src/lib.rs @@ -0,0 +1,53 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that the autoharness subcommand supports arguments whose types implement +// `BoundedArbitrary` (rather than `Arbitrary`), e.g. `Vec`, `String`, or user types +// deriving it. The generated harness produces a bounded nondeterministic value via +// `kani::bounded_any` with bound AUTOHARNESS_BOUNDED_ANY_BOUND (4); verification results +// only hold up to that bound. The "TEST NOTE" comments explain the expected result per +// function. + +// TEST NOTE: should PASS: summing at most 4 u8s cannot overflow u64. +pub fn vec_sum(xs: Vec) -> u64 { + xs.iter().map(|&x| x as u64).sum() +} + +// TEST NOTE: should FAIL: the vector may be empty, so the index may be out of bounds. +pub fn vec_first(xs: Vec) -> u8 { + xs[0] +} + +// TEST NOTE: should PASS: strings generated via String's BoundedArbitrary implementation. +pub fn string_head(s: String) -> Option { + s.chars().next() +} + +// TEST NOTE: should FAIL: the string may be empty, so the index may be out of bounds. +pub fn string_first_byte(s: String) -> u8 { + s.as_bytes()[0] +} + +// TEST NOTE: should PASS: user-defined types deriving BoundedArbitrary are supported too. +#[derive(kani::BoundedArbitrary)] +pub struct Packet { + #[bounded] + payload: Vec, + flag: bool, +} + +pub fn packet_check(p: Packet) -> usize { + if p.flag { p.payload.len() } else { 0 } +} + +// TEST NOTE: should PASS, and the cover check must be SATISFIED: maximum-length vectors +// with specific nondeterministic contents are generated. +pub fn vec_cover(xs: Vec) { + kani::cover!(xs.len() == 4 && xs[0] == 42, "max-length vec with specific contents"); +} + +// TEST NOTE: skipped: Vec> is unsupported, since Vec's BoundedArbitrary +// implementation requires the element type to implement Arbitrary. +pub fn nested_vec(xs: Vec>) -> usize { + xs.len() +} diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected index 2e619294cc1..b7cbf3029a9 100644 --- a/tests/script-based-pre/cargo_autoharness_filter/filter.expected +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected @@ -104,11 +104,11 @@ If you believe that the provided reason is incorrect and Kani should have genera +======================================================================================================================================================+ | 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 | Missing Arbitrary implementation for argument(s) _: std::vec::Vec | +| 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 | Missing Arbitrary implementation for argument(s) _y: std::vec::Vec | +| cargo_autoharness_filter | no_harness::unsupported_vec | Requires --bounded-arguments for argument(s) _y: std::vec::Vec | +--------------------------+----------------------------------------+----------------------------------------------------------------------------------+ Autoharness: Checking function yes_harness::f_mut_pointer against all possible inputs... Autoharness: Checking function yes_harness::f_const_pointer against all possible inputs...