diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 4b9236c5d45c..59a8397aa79a 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -15,7 +15,7 @@ use crate::kani_middle::metadata::{ }; use crate::kani_middle::reachability::filter_crate_items; use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; -use crate::kani_middle::{can_derive_arbitrary, implements_arbitrary}; +use crate::kani_middle::{SmartPointerModels, autoharness_supported_arg_ty}; use crate::kani_queries::QueryDb; use kani_metadata::{ ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessMetadata, @@ -103,6 +103,7 @@ impl CodegenUnits { args, &crate_info.name, *kani_fns.get(&KaniModel::Any.into()).unwrap(), + SmartPointerModels::from_kani_functions(kani_fns), ); AUTOHARNESS_MD .set(AutoHarnessMetadata { @@ -417,6 +418,7 @@ fn automatic_harness_partition( args: &Arguments, crate_name: &str, kani_any_def: FnDef, + smart_pointer_models: SmartPointerModels, ) -> (Vec, 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 @@ -474,17 +476,24 @@ fn automatic_harness_partition( return Some(AutoHarnessSkipReason::UserFilter); } - // Each argument of `instance` must implement Arbitrary. + // Each argument of `instance` must be supported by automatic harness generation, i.e., + // implement Arbitrary (or be capable of deriving it), or be a supported smart pointer, + // c.f. `autoharness_supported_arg_ty`. // Note that we've already filtered out generic functions, so we know that each of these arguments has a concrete type. + // 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 (smart pointers of + // derivable pointees); `implements_arbitrary` memoizes its own recursion internally, + // so repeated argument types stay cheap. let mut problematic_args = vec![]; for (idx, arg) in body.arg_locals().iter().enumerate() { - if !ty_arbitrary_cache.contains_key(&arg.ty) { - let impls_arbitrary = - implements_arbitrary(arg.ty, kani_any_def, &mut ty_arbitrary_cache) - || can_derive_arbitrary(arg.ty, kani_any_def, &mut ty_arbitrary_cache); - ty_arbitrary_cache.insert(arg.ty, impls_arbitrary); - } - let impls_arbitrary = ty_arbitrary_cache.get(&arg.ty).unwrap(); + let impls_arbitrary = &autoharness_supported_arg_ty( + tcx, + arg.ty, + kani_any_def, + &smart_pointer_models, + &mut ty_arbitrary_cache, + ); if !impls_arbitrary { // Find the name of the argument by referencing var_debug_info. diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index d5b97aa5406c..211a5a7010c3 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -67,6 +67,12 @@ pub enum KaniModel { AlignOfVal, #[strum(serialize = "AnyModel")] Any, + #[strum(serialize = "AnyArcModel")] + AnyArc, + #[strum(serialize = "AnyBoxModel")] + AnyBox, + #[strum(serialize = "AnyRcModel")] + AnyRc, #[strum(serialize = "CopyInitStateModel")] CopyInitState, #[strum(serialize = "CopyInitStateSingleModel")] @@ -162,6 +168,15 @@ pub enum KaniHook { UntrackedDeref, } +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. + pub fn is_optional(&self) -> bool { + matches!(self, KaniModel::AnyArc | KaniModel::AnyBox | KaniModel::AnyRc) + } +} + impl From for KaniFunction { fn from(value: KaniIntrinsic) -> Self { KaniFunction::Intrinsic(value) @@ -271,7 +286,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/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 2f7aedf59663..14945c4c18e2 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -300,6 +300,123 @@ fn implements_arbitrary( false } +/// The smart-pointer types for which automatic harnesses can generate nondeterministic values +/// via dedicated (optional) models, c.f. `KaniModel::is_optional`. +#[derive(Copy, Clone, Debug, Eq, PartialEq)] +pub enum SmartPointerKind { + Arc, + Box, + Rc, +} + +/// If `ty` is `Box`, `Rc`, or `Arc`, return the pointer kind and the pointee type `T`. +/// Note that `Box`/`Rc`/`Arc` with a non-default allocator are not +/// recognized, and unsized pointees (e.g. `Box<[T]>`) are rejected by the caller's +/// Arbitrary check on the pointee. +fn smart_pointer_pointee(tcx: TyCtxt, ty: Ty) -> Option<(SmartPointerKind, Ty)> { + let TyKind::RigidTy(RigidTy::Adt(def, args)) = ty.kind() else { + return None; + }; + + let kind = if def.is_box() { + SmartPointerKind::Box + } else { + let def_id = rustc_internal::internal(tcx, def.def_id()); + if tcx.get_diagnostic_item(rustc_span::sym::Rc) == Some(def_id) { + SmartPointerKind::Rc + } else if tcx.get_diagnostic_item(rustc_span::sym::Arc) == Some(def_id) { + SmartPointerKind::Arc + } else { + return None; + } + }; + + // The first generic argument is the pointee. (The remaining argument is the allocator, + // which is validated by the model return-type check in `smart_pointer_model_instance`.) + let pointee = args.0.iter().find_map(|arg| match arg { + GenericArgKind::Type(ty) => Some(*ty), + _ => None, + })?; + Some((kind, pointee)) +} + +/// If `ty` is a supported smart-pointer type whose generation model is available, resolve the +/// model for the pointee and return it together with the pointee type. Returns `None` if the +/// model's return type does not match `ty` exactly (e.g. for a non-default allocator). +fn smart_pointer_model_instance( + tcx: TyCtxt, + ty: Ty, + smart_pointer_models: &SmartPointerModels, +) -> Option<(Instance, Ty)> { + let (kind, pointee) = smart_pointer_pointee(tcx, ty)?; + let model = smart_pointer_models.for_kind(kind)?; + let instance = + Instance::resolve(model, &GenericArgs(vec![GenericArgKind::Type(pointee)])).ok()?; + let TyKind::RigidTy(RigidTy::FnDef(..)) = instance.ty().kind() else { + return None; + }; + let ret_ty = instance.ty().kind().fn_sig()?.skip_binder().output(); + (ret_ty == ty).then_some((instance, pointee)) +} + +/// The (optional) smart-pointer generation models, c.f. `smart_pointer_pointee`. +/// `None` entries mean the model is unavailable (e.g. in the `no_core` flow, which has no +/// `alloc`), in which case the corresponding smart-pointer types are not supported. +#[derive(Copy, Clone, Debug)] +pub struct SmartPointerModels { + pub any_arc: Option, + pub any_box: Option, + pub any_rc: Option, +} + +impl SmartPointerModels { + pub fn from_kani_functions( + kani_fns: &std::collections::HashMap< + crate::kani_middle::kani_functions::KaniFunction, + FnDef, + >, + ) -> Self { + use crate::kani_middle::kani_functions::KaniModel; + SmartPointerModels { + any_arc: kani_fns.get(&KaniModel::AnyArc.into()).copied(), + any_box: kani_fns.get(&KaniModel::AnyBox.into()).copied(), + any_rc: kani_fns.get(&KaniModel::AnyRc.into()).copied(), + } + } + + pub fn for_kind(&self, kind: SmartPointerKind) -> Option { + match kind { + SmartPointerKind::Arc => self.any_arc, + SmartPointerKind::Box => self.any_box, + SmartPointerKind::Rc => self.any_rc, + } + } +} + +/// Can an automatic harness generate a nondeterministic value of type `ty` for a harness +/// argument? In addition to the types that implement or can derive `Arbitrary`, automatic +/// harnesses support `Box`/`Rc`/`Arc` where `T` itself implements or can derive +/// `Arbitrary`, provided the corresponding generation model is available, +/// c.f. `smart_pointer_pointee`. +fn autoharness_supported_arg_ty( + tcx: TyCtxt, + ty: Ty, + kani_any_def: FnDef, + smart_pointer_models: &SmartPointerModels, + ty_arbitrary_cache: &mut FxHashMap, +) -> bool { + if implements_arbitrary(ty, kani_any_def, ty_arbitrary_cache) + || can_derive_arbitrary(ty, kani_any_def, ty_arbitrary_cache) + { + return true; + } + if let Some((_, pointee)) = smart_pointer_model_instance(tcx, ty, smart_pointer_models) { + return implements_arbitrary(pointee, kani_any_def, ty_arbitrary_cache) + || can_derive_arbitrary(pointee, kani_any_def, ty_arbitrary_cache); + } + false +} + /// 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..d4f04bf71d73 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -9,10 +9,12 @@ 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::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use crate::kani_middle::transform::{TransformPass, TransformationType}; +use crate::kani_middle::{ + SmartPointerModels, can_derive_arbitrary, implements_arbitrary, smart_pointer_model_instance, +}; use crate::kani_queries::QueryDb; use rustc_data_structures::fx::FxHashMap; use rustc_middle::ty::TyCtxt; @@ -34,13 +36,16 @@ use tracing::debug; pub struct AutomaticArbitraryPass { /// The FnDef of KaniModel::Any kani_any: FnDef, + /// The (optional) smart-pointer generation models. + smart_pointer_models: SmartPointerModels, } 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 smart_pointer_models = SmartPointerModels::from_kani_functions(kani_fns); + Self { kani_any, smart_pointer_models } } } @@ -93,7 +98,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| { @@ -116,8 +121,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 { @@ -127,16 +132,29 @@ 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. +/// For `Box`/`Rc`/`Arc` whose pointee only *can derive* Arbitrary, insert a call to +/// the corresponding smart-pointer model instead (the model's internal `kani::any::()` call +/// is replaced with the compiler-synthesized implementation by `AutomaticArbitraryPass`). +/// Panics if `ty` does not implement Arbitrary and is not a supported smart pointer. fn call_kani_any_for_ty( + tcx: TyCtxt, kani_any: FnDef, + smart_pointer_models: &SmartPointerModels, body: &mut MutableBody, ty: Ty, mutability: Mutability, source: &mut SourceInstruction, ) -> Local { 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, + smart_pointer_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 @@ -151,11 +169,25 @@ fn call_kani_any_for_ty( ); ref_lcl } else { - let kani_any_inst = + // Prefer a plain kani::any() call, which resolves to the type's (implemented or + // compiler-derived) Arbitrary; use the smart-pointer models only for pointees that + // lack an Arbitrary implementation (in which case resolving e.g. + // ` as Arbitrary>::any` would fail). + let mut cache = FxHashMap::default(); + let use_any = implements_arbitrary(ty, kani_any, &mut cache) + || can_derive_arbitrary(ty, kani_any, &mut cache); + let inst = if use_any { Instance::resolve(kani_any, &GenericArgs(vec![GenericArgKind::Type(ty)])) - .unwrap_or_else(|_| panic!("expected a ty that implements Arbitrary, got {ty}")); + .unwrap_or_else(|_| panic!("expected a ty that implements Arbitrary, got {ty}")) + } else { + let (inst, _) = smart_pointer_model_instance(tcx, ty, smart_pointer_models) + .unwrap_or_else(|| { + panic!("expected a ty that implements Arbitrary or a smart pointer, got {ty}") + }); + inst + }; 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(&inst, source, InsertPosition::Before, vec![], Place::from(lcl)); lcl } } @@ -170,6 +202,7 @@ impl AutomaticArbitraryPass { /// This function will panic if a field type does not implement Arbitrary. fn call_kani_any_for_variant( &self, + tcx: TyCtxt, adt_def: AdtDef, adt_args: &GenericArgs, body: &mut MutableBody, @@ -181,7 +214,15 @@ 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.smart_pointer_models, + body, + ty, + Mutability::Not, + source, + ); field_locals.push(lcl); } @@ -213,7 +254,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); @@ -223,7 +264,9 @@ impl AutomaticArbitraryPass { // Generate a nondet u128 to switch on let discr_lcl = call_kani_any_for_ty( + tcx, self.kani_any, + &self.smart_pointer_models, &mut new_body, Ty::from_rigid_kind(RigidTy::Uint(UintTy::U128)), Mutability::Not, @@ -241,8 +284,14 @@ 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, + def, + &args, + &mut new_body, + &mut source, + variant, + ); branches.push((variant.idx.to_index() as u128, target_bb)); } @@ -268,7 +317,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); @@ -276,7 +331,7 @@ impl AutomaticArbitraryPass { 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, def, &args, &mut new_body, &mut source, variant); new_body.into() } @@ -285,6 +340,7 @@ impl AutomaticArbitraryPass { #[derive(Debug, Clone)] pub struct AutomaticHarnessPass { kani_any: FnDef, + smart_pointer_models: SmartPointerModels, init_contracts_hook: Instance, kani_autoharness_intrinsic: FnDef, } @@ -295,10 +351,11 @@ impl AutomaticHarnessPass { let kani_autoharness_intrinsic = *kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap(); + let smart_pointer_models = SmartPointerModels::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_any, smart_pointer_models, init_contracts_hook, kani_autoharness_intrinsic } } } @@ -359,7 +416,9 @@ impl TransformPass for AutomaticHarnessPass { .iter() .map(|local_decl| { call_kani_any_for_ty( + tcx, self.kani_any, + &self.smart_pointer_models, &mut harness_body, local_decl.ty, local_decl.mutability, diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index f16f06165d29..7666325cdaff 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -15,6 +15,53 @@ where } } +impl Arbitrary for std::rc::Rc +where + T: Arbitrary, +{ + fn any() -> Self { + std::rc::Rc::new(T::any()) + } +} + +impl Arbitrary for std::sync::Arc +where + T: Arbitrary, +{ + fn any() -> Self { + std::sync::Arc::new(T::any()) + } +} + +/// The models below are used by the compiler to generate nondeterministic +/// `Box`/`Rc`/`Arc` values for automatic harnesses when `T` does not implement +/// `Arbitrary` in source code but the compiler can derive it: the `kani::any::()` calls in +/// their bodies are then replaced with the compiler-synthesized implementation. (For `T`s that +/// do implement `Arbitrary`, the `Arbitrary` implementations above are resolved directly +/// instead.) +/// These models are *optional*: they require `alloc` and thus have no `core::kani` +/// counterpart, c.f. `KaniModel::is_optional`. +#[kanitool::fn_marker = "AnyBoxModel"] +#[inline(never)] +#[doc(hidden)] +pub fn any_box() -> Box { + Box::new(crate::any()) +} + +#[kanitool::fn_marker = "AnyRcModel"] +#[inline(never)] +#[doc(hidden)] +pub fn any_rc() -> std::rc::Rc { + std::rc::Rc::new(crate::any()) +} + +#[kanitool::fn_marker = "AnyArcModel"] +#[inline(never)] +#[doc(hidden)] +pub fn any_arc() -> std::sync::Arc { + std::sync::Arc::new(crate::any()) +} + impl Arbitrary for std::time::Duration { fn any() -> Self { const NANOS_PER_SEC: u32 = 1_000_000_000; diff --git a/tests/kani/Arbitrary/rc_arc.rs b/tests/kani/Arbitrary/rc_arc.rs new file mode 100644 index 000000000000..8dee0066ee52 --- /dev/null +++ b/tests/kani/Arbitrary/rc_arc.rs @@ -0,0 +1,33 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that Rc and Arc implement Arbitrary (like Box), producing an +// unconstrained value of the pointee type behind shared-ownership indirection. + +use std::rc::Rc; +use std::sync::Arc; + +#[derive(kani::Arbitrary)] +struct Point { + x: u8, + y: u8, +} + +#[kani::proof] +fn check_rc() { + let p: Rc = kani::any(); + kani::cover!(p.x == 255 && p.y == 0, "extreme values are generated"); +} + +#[kani::proof] +fn check_arc() { + let v: Arc = kani::any(); + kani::cover!(*v == i32::MIN, "extreme values are generated"); + kani::cover!(*v == 42, "specific values are generated"); +} + +#[kani::proof] +fn check_nested() { + let v: Rc> = kani::any(); + kani::cover!(**v == 7, "nested smart pointers are generated"); +} diff --git a/tests/script-based-pre/cargo_autoharness_smart_pointers/Cargo.toml b/tests/script-based-pre/cargo_autoharness_smart_pointers/Cargo.toml new file mode 100644 index 000000000000..711326307404 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_smart_pointers/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_smart_pointers" +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_smart_pointers/config.yml b/tests/script-based-pre/cargo_autoharness_smart_pointers/config.yml new file mode 100644 index 000000000000..38045535b203 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_smart_pointers/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: smart-pointers.sh +expected: smart-pointers.expected +exit_code: 1 diff --git a/tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.expected b/tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.expected new file mode 100644 index 000000000000..b9b3b848a6ee --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.expected @@ -0,0 +1,8 @@ +| cargo_autoharness_smart_pointers | box_not_derivable | Missing Arbitrary implementation for argument(s) b: std::boxed::Box | +- Status: SATISFIED +| cargo_autoharness_smart_pointers | arc_derivable | #[kani::proof] | Success | +| cargo_autoharness_smart_pointers | box_derivable | #[kani::proof] | Success | +| cargo_autoharness_smart_pointers | box_derived | #[kani::proof] | Success | +| cargo_autoharness_smart_pointers | rc_derivable | #[kani::proof] | Success | +| cargo_autoharness_smart_pointers | arc_assert | #[kani::proof] | Failure | +Complete - 4 successfully verified functions, 1 failures, 5 total. diff --git a/tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.sh b/tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.sh new file mode 100755 index 000000000000..db4a99f8be09 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_smart_pointers/smart-pointers.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 diff --git a/tests/script-based-pre/cargo_autoharness_smart_pointers/src/lib.rs b/tests/script-based-pre/cargo_autoharness_smart_pointers/src/lib.rs new file mode 100644 index 000000000000..02c020a3540c --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_smart_pointers/src/lib.rs @@ -0,0 +1,58 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that the autoharness subcommand supports Box, Rc, and Arc arguments, both for +// pointee types that implement Arbitrary and for pointees whose Arbitrary implementation the +// compiler derives (via the AnyBox/AnyRc/AnyArc models). These values are *unbounded*: a smart +// pointer to T covers exactly the values of T, so no --bounded-arguments is needed. +// The "TEST NOTE" comments explain the expected result per function. + +use std::rc::Rc; +use std::sync::Arc; + +#[derive(kani::Arbitrary)] +pub struct Derived { + pub x: u8, +} + +// No Arbitrary implementation; the compiler derives one. +pub struct OnlyDerivable { + pub x: u8, +} + +// TEST NOTE: should PASS. +pub fn box_derived(b: Box) -> u8 { + b.x +} + +// TEST NOTE: should PASS: the pointee's Arbitrary implementation is compiler-derived. +pub fn box_derivable(b: Box) -> u8 { + b.x +} + +// TEST NOTE: should PASS. +pub fn rc_derivable(r: Rc) -> u8 { + r.x +} + +// TEST NOTE: should PASS. +pub fn arc_derivable(a: Arc) -> u8 { + a.x +} + +// TEST NOTE: should FAIL, and the cover check must be SATISFIED: all pointee values are +// generated (full coverage; smart pointers are not bounded). +pub fn arc_assert(a: Arc) { + kani::cover!(a.x == 255, "extreme pointee values are generated"); + assert!(a.x < 255); +} + +// TEST NOTE: skipped: pointees that can neither implement nor derive Arbitrary remain +// unsupported. +pub struct NotDerivable { + pub p: *const u8, +} + +pub fn box_not_derivable(b: Box) -> usize { + b.p as usize +}