diff --git a/Cargo.lock b/Cargo.lock index 2a695d57a3d4..206de7609e5b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1084,6 +1084,7 @@ dependencies = [ "charon", "clap", "cprover_bindings", + "fxhash", "itertools 0.14.0", "kani_metadata", "lazy_static", diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index 95cebc9c7738..1a4a7c32b8f5 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -103,10 +103,10 @@ please add them to [this GitHub issue](https://github.com/model-checking/kani/is ## Limitations ### Arguments Implementing Arbitrary -Kani will only generate an automatic harness for a function if it can determine that all of the function's arguments implement Arbitrary. -It does not attempt to derive/implement Arbitrary for any types, even if those types could implement Arbitrary. -For example, imagine a user defines `struct MyStruct { x: u8, y: u8}`, but does not derive or implement Arbitrary for `MyStruct`. -Kani does not attempt to add such derivations itself, so it will not generate a harness for a function that takes `MyStruct` as input. +Kani will only generate an automatic harness for a function if it can represent each of its arguments nondeterministically, without bounds. +In technical terms, each of the arguments needs to implement the `Arbitrary` trait or be capable of 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. ### Generic Functions The current implementation does not generate harnesses for generic functions. diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 3650276d39a5..2772b346d921 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -12,6 +12,7 @@ publish = false cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true } charon = { path = "../charon/charon", optional = true, default-features = false } clap = { version = "4.4.11", features = ["derive", "cargo"] } +fxhash = "0.2.1" itertools = "0.14" kani_metadata = { path = "../kani_metadata" } lazy_static = "1.5.0" diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 9715d9976b61..4b786adee31c 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -16,7 +16,9 @@ use crate::kani_middle::metadata::{ use crate::kani_middle::reachability::filter_crate_items; use crate::kani_middle::resolve::expect_resolve_fn; use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; +use crate::kani_middle::{can_derive_arbitrary, implements_arbitrary}; use crate::kani_queries::QueryDb; +use fxhash::FxHashMap; use kani_metadata::{ ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessKind, HarnessMetadata, KaniMetadata, @@ -26,8 +28,8 @@ use rustc_hir::def_id::DefId; use rustc_middle::ty::TyCtxt; use rustc_session::config::OutputType; use rustc_smir::rustc_internal; -use stable_mir::mir::{TerminatorKind, mono::Instance}; -use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, IndexedVal, RigidTy, TyKind}; +use stable_mir::mir::mono::Instance; +use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, IndexedVal, RigidTy, Ty, TyKind}; use stable_mir::{CrateDef, CrateItem}; use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; use std::fs::File; @@ -394,10 +396,13 @@ fn automatic_harness_partition( let included_set = make_regex_set(args.autoharness_included_patterns.clone()); let excluded_set = make_regex_set(args.autoharness_excluded_patterns.clone()); + // Cache whether a type implements or can derive Arbitrary + let mut ty_arbitrary_cache: FxHashMap = FxHashMap::default(); + // If `func` is not eligible for an automatic harness, return the reason why; if it is eligible, return None. // Note that we only return one reason for ineligiblity, when there could be multiple; // we can revisit this implementation choice in the future if users request more verbose output. - let skip_reason = |fn_item: CrateItem| -> Option { + let mut skip_reason = |fn_item: CrateItem| -> Option { if KaniAttributes::for_def_id(tcx, fn_item.def_id()).is_kani_instrumentation() { return Some(AutoHarnessSkipReason::KaniImpl); } @@ -432,25 +437,12 @@ 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() { - let kani_any_body = - Instance::resolve(kani_any_def, &GenericArgs(vec![GenericArgKind::Type(arg.ty)])) - .unwrap() - .body() - .unwrap(); - - let implements_arbitrary = if let TerminatorKind::Call { func, .. } = - &kani_any_body.blocks[0].terminator.kind - { - if let Some((def, args)) = func.ty(body.arg_locals()).unwrap().kind().fn_def() { - Instance::resolve(def, args).is_ok() - } else { - false - } - } else { - false - }; - - if !implements_arbitrary { + let implements_arbitrary = ty_arbitrary_cache.entry(arg.ty).or_insert_with(|| { + implements_arbitrary(arg.ty, kani_any_def) + || can_derive_arbitrary(arg.ty, kani_any_def) + }); + + if !(*implements_arbitrary) { // Find the name of the argument by referencing var_debug_info. // Note that enumerate() starts at 0, while StableMIR argument_index starts at 1, hence the idx+1. let arg_name = body diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index e6839487c046..c3d78a741619 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -9,8 +9,11 @@ use crate::kani_queries::QueryDb; use rustc_hir::{def::DefKind, def_id::DefId as InternalDefId, def_id::LOCAL_CRATE}; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; -use stable_mir::mir::mono::MonoItem; -use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind}; +use stable_mir::mir::TerminatorKind; +use stable_mir::mir::mono::{Instance, MonoItem}; +use stable_mir::ty::{ + AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Span as SpanStable, Ty, TyKind, +}; use stable_mir::visitor::{Visitable, Visitor as TyVisitor}; use stable_mir::{CrateDef, DefId}; use std::ops::ControlFlow; @@ -165,3 +168,65 @@ pub fn stable_fn_def(tcx: TyCtxt, def_id: InternalDefId) -> Option { None } } + +/// Inspect a `kani::any()` call to determine if `T: Arbitrary` +/// `kani_any_def` refers to a function that looks like: +/// ```rust +/// fn any() -> T { +/// T::any() +/// } +/// ``` +/// So we select the terminator that calls T::kani::Arbitrary::any(), then try to resolve it to an Instance. +/// `T` implements Arbitrary iff we successfully resolve the Instance. +fn implements_arbitrary(ty: Ty, kani_any_def: FnDef) -> bool { + let kani_any_body = + Instance::resolve(kani_any_def, &GenericArgs(vec![GenericArgKind::Type(ty)])) + .unwrap() + .body() + .unwrap(); + + 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 +} + +/// Is `ty` a struct or enum whose fields/variants implement Arbitrary? +fn can_derive_arbitrary(ty: Ty, kani_any_def: FnDef) -> bool { + let variants_can_derive = |def: AdtDef| { + for variant in def.variants_iter() { + let fields = variant.fields(); + let mut fields_impl_arbitrary = true; + for ty in fields.iter().map(|field| field.ty()) { + fields_impl_arbitrary &= implements_arbitrary(ty, kani_any_def); + } + if !fields_impl_arbitrary { + return false; + } + } + true + }; + + if let TyKind::RigidTy(RigidTy::Adt(def, _)) = ty.kind() { + match def.kind() { + AdtKind::Enum => { + // Enums with no variants cannot be instantiated + if def.num_variants() == 0 { + return false; + } + variants_can_derive(def) + } + AdtKind::Struct => variants_can_derive(def), + AdtKind::Union => false, + } + } else { + false + } +} diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 2eaf82078287..cbc026d63fd7 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -1,14 +1,15 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module transforms the body of an automatic harness to verify a function. -//! Upon entry to this module, a harness has the dummy body of the automatic_harness Kani intrinsic. -//! We obtain the function its meant to verify by inspecting its generic arguments, -//! then transform its body to be a harness for that function. +//! This module contains two passes: +//! 1. `AutomaticHarnessPass`, which transforms the body of an automatic harness to verify a function. +//! 2. `AutomaticArbitraryPass`, which creates `T::any()` implementations for `T`s that do not implement Arbitrary in source code, +//! but we have determined can derive it. 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}; @@ -16,10 +17,249 @@ use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use stable_mir::CrateDef; use stable_mir::mir::mono::Instance; -use stable_mir::mir::{Body, Mutability, Operand, Place, TerminatorKind}; -use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, RigidTy, Ty}; +use stable_mir::mir::{ + AggregateKind, BasicBlockIdx, Body, Local, Mutability, Operand, Place, Rvalue, SwitchTargets, + Terminator, TerminatorKind, +}; +use stable_mir::ty::{ + AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, IndexedVal, RigidTy, Ty, TyKind, UintTy, + VariantDef, +}; use tracing::debug; +/// Generate `T::any()` implementations for `T`s that do not implement Arbitrary in source code. +/// Currently limited to structs and enums. +#[derive(Debug)] +pub struct AutomaticArbitraryPass { + /// The FnDef of KaniModel::Any + kani_any: FnDef, +} + +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 } + } +} + +impl TransformPass for AutomaticArbitraryPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Stubbing + } + + fn is_enabled(&self, query_db: &QueryDb) -> bool + where + Self: Sized, + { + matches!(query_db.args().reachability_analysis, ReachabilityType::AllFns) + } + + /// Transform the body of a kani::any::() call if `T` does not implement `Arbitrary`. + /// This occurs if an automatic harness calls kani::any() for a type that `automatic_harness_partition` determined can derive Arbitrary. + /// The default implementation for `kani::any()` (c.f. kani_core::kani_intrinsics) is: + /// ```ignore + /// pub fn any() -> T { + /// T::any() + /// } + /// ``` + /// We need to overwrite this implementation because `T` doesn't implement `Arbitrary`, so trying to call `T::any()` will fail. + /// Instead, we inline the body of what `T::any()` would be if it existed. + /// For example: + /// ```ignore + /// enum Foo { + /// Variant1, + /// Variant2, + /// } + /// ``` + /// we replace the body: + /// ```ignore + /// pub fn any() -> Foo { + /// Foo::any() // doesn't exist, must replace + /// } + /// ``` + /// so that instead, we have: + /// ```ignore + /// pub fn any() -> Foo { + /// match kani::any() { + /// 0 => Foo::Variant1, + /// _ => Foo::Variant2, + /// } + /// } + /// ``` + /// 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) { + debug!(function=?instance.name(), "AutomaticArbitraryPass::transform"); + + let unexpected_ty = |ty: &Ty| { + panic!( + "AutomaticArbitraryPass: should only find compiler-inserted kani::any() calls for structs or enums, found {ty}" + ) + }; + + if instance.def.def_id() != self.kani_any.def_id() { + return (false, body); + } + + // Get the `ty` we're calling `kani::any()` on + let binding = instance.args(); + let ty = binding.0[0].expect_ty(); + + if implements_arbitrary(*ty, self.kani_any) { + return (false, body); + } + + if let TyKind::RigidTy(RigidTy::Adt(def, ..)) = ty.kind() { + match def.kind() { + AdtKind::Enum => (true, self.generate_enum_body(def, body)), + AdtKind::Struct => (true, self.generate_struct_body(def, body)), + AdtKind::Union => unexpected_ty(ty), + } + } else { + unexpected_ty(ty) + } + } +} + +impl AutomaticArbitraryPass { + /// Insert a call to kani::any::() in `body`; return the local storing the result. + /// Panics if `ty` does not implement Arbitrary. + fn call_kani_any_for_ty( + &self, + body: &mut MutableBody, + ty: Ty, + source: &mut SourceInstruction, + ) -> Local { + let kani_any_inst = + Instance::resolve(self.kani_any, &GenericArgs(vec![GenericArgKind::Type(ty)])) + .unwrap_or_else(|_| panic!("expected a ty that implements Arbitrary, got {ty}")); + let lcl = body.new_local(ty, source.span(body.blocks()), Mutability::Not); + body.insert_call(&kani_any_inst, source, InsertPosition::Before, vec![], Place::from(lcl)); + lcl + } + + /// Insert the basic blocks for generating an arbitrary variant into `body`. + /// Return the index of the first inserted basic block. + /// We generate an arbitrary variant by: + /// 1. Calling kani::any() for each of the variant's field types, then + /// 2. Constructing the variant from the results of 1) and assigning it to the return local. + /// + /// This function will panic if a field type does not implement Arbitrary. + fn call_kani_any_for_variant( + &self, + def: AdtDef, + body: &mut MutableBody, + source: &mut SourceInstruction, + variant: VariantDef, + ) -> BasicBlockIdx { + let fields = variant.fields(); + let mut field_locals = vec![]; + + // Construct nondeterministic values for each of the variant's fields + for ty in fields.iter().map(|field| field.ty()) { + let lcl = self.call_kani_any_for_ty(body, ty, source); + field_locals.push(lcl); + } + + // Insert a basic block that constructs the variant from each of the nondet fields, then returns it + body.insert_terminator( + source, + InsertPosition::Before, + Terminator { kind: TerminatorKind::Return, span: source.span(body.blocks()) }, + ); + let mut assign_instr = SourceInstruction::Terminator { bb: source.bb() - 1 }; + let rvalue = Rvalue::Aggregate( + AggregateKind::Adt(def, variant.idx, GenericArgs(vec![]), None, None), + field_locals.into_iter().map(|lcl| Operand::Move(lcl.into())).collect(), + ); + body.assign_to(Place::from(0), rvalue, &mut assign_instr, InsertPosition::Before); + + // The index of the first block we inserted is (last bb index - number of bbs we inserted above it) + source.bb() - (fields.len() + 1) + } + + /// Overwrite the default kani::any() implementation `body` for the enum described by `def`. + /// The returned body is equivalent to: + /// ```ignore + /// let discriminant = kani::any(); + /// match discriminant { + /// 0 => Enum::Variant1(field1, field2), + /// 1 => Enum::Variant2(..), + /// ... (cont.) + /// _ => Enum::LastVariant + /// } + /// ``` + fn generate_enum_body(&self, def: AdtDef, 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 source = SourceInstruction::Terminator { bb: 0 }; + + // Generate a nondet u128 to switch on + let discr_lcl = self.call_kani_any_for_ty( + &mut new_body, + Ty::from_rigid_kind(RigidTy::Uint(UintTy::U128)), + &mut source, + ); + + // Insert a 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_int_instr = SourceInstruction::Terminator { bb: source.bb() - 1 }; + + let mut branches: Vec<(u128, BasicBlockIdx)> = vec![]; + for variant in def.variants_iter() { + let target_bb = + self.call_kani_any_for_variant(def, &mut new_body, &mut source, variant); + branches.push((variant.idx.to_index() as u128, target_bb)); + } + + let otherwise = branches.pop().unwrap().1; + let match_term = Terminator { + kind: TerminatorKind::SwitchInt { + discr: Operand::Copy(Place::from(discr_lcl)), + targets: SwitchTargets::new(branches, otherwise), + }, + span: source.span(new_body.blocks()), + }; + new_body.replace_terminator(&switch_int_instr, match_term); + + new_body.into() + } + + /// Overwrite the default kani::any() implementation `body` for the struct described by `def`. + /// The returned body is equivalent to: + /// ```ignore + /// struct Struct { + /// field1: kani::any(), + /// field2: kani::any(), + /// ... + /// } + /// ``` + fn generate_struct_body(&self, def: AdtDef, body: Body) -> Body { + assert_eq!(def.num_variants(), 1); + + let mut new_body = MutableBody::from(body); + new_body.clear_body(TerminatorKind::Unreachable); + let mut source = SourceInstruction::Terminator { bb: 0 }; + + let variant = def.variants()[0]; + self.call_kani_any_for_variant(def, &mut new_body, &mut source, variant); + + new_body.into() + } +} +/// Transform the dummy body of an automatic_harness Kani intrinsic to be a proof harness for a given function. #[derive(Debug)] pub struct AutomaticHarnessPass { /// The FnDef of KaniModel::Any diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 60b99e5cf13d..367bb6ee32f2 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -13,6 +13,7 @@ use stable_mir::ty::{GenericArgs, MirConst, Span, Ty, UintTy}; use std::fmt::Debug; use std::mem; +#[derive(Debug)] /// This structure mimics a Body that can actually be modified. pub struct MutableBody { blocks: Vec, diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 164730499efb..7b7b2f054893 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -26,7 +26,7 @@ use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_middle::transform::loop_contracts::LoopContractPass; use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; -use automatic::AutomaticHarnessPass; +use automatic::{AutomaticArbitraryPass, AutomaticHarnessPass}; use dump_mir_pass::DumpMirPass; use rustc_middle::ty::TyCtxt; use stable_mir::mir::Body; @@ -76,6 +76,7 @@ impl BodyTransformation { let unsupported_check_type = CheckType::new_unsupported_check_assert_assume_false(queries); // This has to come first, since creating harnesses affects later stubbing and contract passes. transformer.add_pass(queries, AutomaticHarnessPass::new(unit, queries)); + transformer.add_pass(queries, AutomaticArbitraryPass::new(unit, queries)); transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); transformer.add_pass(queries, FunctionWithContractPass::new(tcx, queries, unit)); diff --git a/tests/script-based-pre/autoderive_arbitrary_enums/Cargo.toml b/tests/script-based-pre/autoderive_arbitrary_enums/Cargo.toml new file mode 100644 index 000000000000..7be8b70b9cd4 --- /dev/null +++ b/tests/script-based-pre/autoderive_arbitrary_enums/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "autoderive_arbitrary_enums" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/autoderive_arbitrary_enums/config.yml b/tests/script-based-pre/autoderive_arbitrary_enums/config.yml new file mode 100644 index 000000000000..6038fd632cb7 --- /dev/null +++ b/tests/script-based-pre/autoderive_arbitrary_enums/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: enums.sh +expected: enums.expected +exit_code: 1 \ No newline at end of file diff --git a/tests/script-based-pre/autoderive_arbitrary_enums/enums.expected b/tests/script-based-pre/autoderive_arbitrary_enums/enums.expected new file mode 100644 index 000000000000..ef97df46db3a --- /dev/null +++ b/tests/script-based-pre/autoderive_arbitrary_enums/enums.expected @@ -0,0 +1,86 @@ +Kani generated automatic harnesses for 8 function(s): ++----------------------------+------------------------------------------------+ +| Crate | Selected Function | ++=============================================================================+ +| autoderive_arbitrary_enums | should_derive::Foo::AnonMultipleVariant | +|----------------------------+------------------------------------------------| +| autoderive_arbitrary_enums | should_derive::Foo::AnonVariant | +|----------------------------+------------------------------------------------| +| autoderive_arbitrary_enums | should_derive::alignment_fail | +|----------------------------+------------------------------------------------| +| autoderive_arbitrary_enums | should_derive::alignment_pass | +|----------------------------+------------------------------------------------| +| autoderive_arbitrary_enums | should_derive::foo | +|----------------------------+------------------------------------------------| +| autoderive_arbitrary_enums | should_not_derive::NotAllVariantsEligible::Num | +|----------------------------+------------------------------------------------| +| autoderive_arbitrary_enums | should_not_derive::NotAllVariantsEligible::Pin | +|----------------------------+------------------------------------------------| +| autoderive_arbitrary_enums | should_not_derive::RecursivelyEligible::Foo | ++----------------------------+------------------------------------------------+ + +Kani did not generate automatic harnesses for 10 function(s). ++----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------+ +| Crate | Skipped Function | Reason for Skipping | ++=======================================================================================================================================================================================================================================+ +| autoderive_arbitrary_enums | ::assert_receiver_is_total_eq | Missing Arbitrary implementation for argument(s) self: &should_derive::AlignmentEnum | +|----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_enums | ::eq | Missing Arbitrary implementation for argument(s) self: &should_derive::AlignmentEnum, other: &should_derive::AlignmentEnum | +|----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_enums | should_not_derive::NoVariantsEligible::Ptr | Missing Arbitrary implementation for argument(s) _: *const i8 | +|----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_enums | should_not_derive::NoVariantsEligible::Str | Missing Arbitrary implementation for argument(s) _: &str | +|----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_enums | should_not_derive::NotAllVariantsEligible::Ref | Missing Arbitrary implementation for argument(s) _: &mut i32 | +|----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_enums | should_not_derive::never | Missing Arbitrary implementation for argument(s) n: should_not_derive::Never | +|----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_enums | should_not_derive::no_variants_eligible | Missing Arbitrary implementation for argument(s) val: should_not_derive::NoVariantsEligible | +|----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_enums | should_not_derive::not_all_variants_eligible | Missing Arbitrary implementation for argument(s) val: should_not_derive::NotAllVariantsEligible | +|----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_enums | should_not_derive::recursively_eligible | Missing Arbitrary implementation for argument(s) val: should_not_derive::RecursivelyEligible | +|----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_enums | should_not_derive::some_arguments_support | Missing Arbitrary implementation for argument(s) val: should_not_derive::NotAllVariantsEligible | ++----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------+ + +should_derive::alignment_pass\ + - Status: SUCCESS\ + - Description: "assertion failed: std::mem::align_of_val(&int) % (align as usize) == 0" + +should_derive::alignment_fail.assertion\ + - Status: FAILURE\ + - Description: "assertion failed: std::mem::align_of_val(&int) % (align as usize) == 0" + +should_derive::foo.assertion\ + - Status: FAILURE\ + - Description: "attempt to calculate the remainder with a divisor of zero" + +should_derive::foo.assertion\ + - Status: FAILURE\ + - Description: "attempt to calculate the remainder with overflow" + +should_derive::foo.assertion\ + - Status: FAILURE\ + - Description: "foo held an i28, but it didn't divide evenly" + +Autoharness Summary: ++----------------------------+------------------------------------------------+-----------------------------+---------------------+ +| Crate | Selected Function | Kind of Automatic Harness | Verification Result | ++=================================================================================================================================+ +| autoderive_arbitrary_enums | should_derive::Foo::AnonMultipleVariant | #[kani::proof] | Success | +|----------------------------+------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::Foo::AnonVariant | #[kani::proof] | Success | +|----------------------------+------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::alignment_pass | #[kani::proof_for_contract] | Success | +|----------------------------+------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_not_derive::NotAllVariantsEligible::Num | #[kani::proof] | Success | +|----------------------------+------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_not_derive::NotAllVariantsEligible::Pin | #[kani::proof] | Success | +|----------------------------+------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_not_derive::RecursivelyEligible::Foo | #[kani::proof] | Success | +|----------------------------+------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::alignment_fail | #[kani::proof] | Failure | +|----------------------------+------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::foo | #[kani::proof] | Failure | ++----------------------------+------------------------------------------------+-----------------------------+---------------------+ diff --git a/tests/script-based-pre/autoderive_arbitrary_enums/enums.sh b/tests/script-based-pre/autoderive_arbitrary_enums/enums.sh new file mode 100755 index 000000000000..db4a99f8be09 --- /dev/null +++ b/tests/script-based-pre/autoderive_arbitrary_enums/enums.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/autoderive_arbitrary_enums/src/lib.rs b/tests/script-based-pre/autoderive_arbitrary_enums/src/lib.rs new file mode 100644 index 000000000000..04df090264b0 --- /dev/null +++ b/tests/script-based-pre/autoderive_arbitrary_enums/src/lib.rs @@ -0,0 +1,91 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Test deriving Arbitrary for enums inside the compiler + +#![allow(dead_code)] +#![allow(unused_variables)] + +mod should_derive { + pub enum Foo { + UnitVariant, + AnonVariant(u8), + AnonMultipleVariant(u32, char), + NamedVariant { val: u32 }, + NamedMultipleVariant { num: i128, char: char }, + } + + fn foo(foo: Foo, divisor: i128) { + match foo { + Foo::UnitVariant + | Foo::AnonVariant(_) + | Foo::AnonMultipleVariant(..) + | Foo::NamedVariant { .. } => {} + Foo::NamedMultipleVariant { num, char } if num % divisor == 0 => {} + _ => panic!("foo held an i28, but it didn't divide evenly"), + } + } + + #[derive(Eq, PartialEq)] + pub enum AlignmentEnum { + _Align1Shl0 = 1 << 0, + _Align1Shl1 = 1 << 1, + _Align1Shl2 = 1 << 2, + _Align1Shl3 = 1 << 3, + _Align1Shl4 = 1 << 4, + _Align1Shl5 = 1 << 5, + _Align1Shl6 = 1 << 6, + _Align1Shl7 = 1 << 7, + _Align1Shl8 = 1 << 8, + _Align1Shl9 = 1 << 9, + _Align1Shl10 = 1 << 10, + _Align1Shl11 = 1 << 11, + _Align1Shl12 = 1 << 12, + _Align1Shl13 = 1 << 13, + _Align1Shl14 = 1 << 14, + _Align1Shl15 = 1 << 15, + } + + fn alignment_fail(align: AlignmentEnum) { + let int = 7; + assert_eq!(std::mem::align_of_val(&int) % (align as usize), 0); + } + + #[kani::requires(align == AlignmentEnum::_Align1Shl0 || align == AlignmentEnum::_Align1Shl1 || align == AlignmentEnum::_Align1Shl2)] + fn alignment_pass(align: AlignmentEnum) { + let int = 7; + assert_eq!(std::mem::align_of_val(&int) % (align as usize), 0); + } +} + +mod should_not_derive { + use super::should_derive::Foo; + use std::marker::PhantomPinned; + + // Zero-variant enum + enum Never {} + + // None of the variants impl Arbitrary + enum NoVariantsEligible { + Str(&'static str), + Ptr(*const i8), + } + + // At least one of the variants doesn't impl Arbitrary + enum NotAllVariantsEligible { + Pin(PhantomPinned), + Ref(&'static mut i32), + Num(u32), + } + + // The enum can impl Arbitrary recursively, but we don't support that + enum RecursivelyEligible { + Foo(Foo), + } + + fn never(n: Never) {} + fn no_variants_eligible(val: NoVariantsEligible) {} + fn not_all_variants_eligible(val: NotAllVariantsEligible) {} + fn recursively_eligible(val: RecursivelyEligible) {} + fn some_arguments_support(foo: Foo, val: NotAllVariantsEligible) {} +} diff --git a/tests/script-based-pre/autoderive_arbitrary_structs/Cargo.toml b/tests/script-based-pre/autoderive_arbitrary_structs/Cargo.toml new file mode 100644 index 000000000000..822f77b48d86 --- /dev/null +++ b/tests/script-based-pre/autoderive_arbitrary_structs/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "autoderive_arbitrary_structs" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/autoderive_arbitrary_structs/config.yml b/tests/script-based-pre/autoderive_arbitrary_structs/config.yml new file mode 100644 index 000000000000..23fc0ba4cde9 --- /dev/null +++ b/tests/script-based-pre/autoderive_arbitrary_structs/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: structs.sh +expected: structs.expected +exit_code: 1 \ No newline at end of file diff --git a/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs b/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs new file mode 100644 index 000000000000..a4d90d7ebd63 --- /dev/null +++ b/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs @@ -0,0 +1,96 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Test deriving Arbitrary for structs inside the compiler + +#![allow(dead_code)] +#![allow(unused_variables)] + +mod should_derive { + #[derive(Eq, PartialEq)] + pub struct UnitStruct; + pub struct AnonStruct(u8); + pub struct AnonMultipleStruct(u32, char); + pub struct NamedStruct { + val: u32, + } + pub struct NamedMultipleStruct { + num: i128, + char: char, + } + + fn unit_struct(foo: UnitStruct, bar: UnitStruct) -> UnitStruct { + assert_eq!(foo, bar); + foo + } + + fn anon_struct(foo: AnonStruct, divisor: u8) { + if foo.0 % divisor != 0 { + panic!("foo held an u32, but it didn't divide evenly"); + } + } + + fn anon_multiple_struct(foo: AnonMultipleStruct, divisor: u32) { + if foo.0 % divisor != 0 { + panic!("foo held an u32, but it didn't divide evenly"); + } + } + + fn named_struct(foo: NamedStruct, divisor: u32) { + if foo.val % divisor != 0 { + panic!("foo held an u32, but it didn't divide evenly"); + } + } + + fn named_multiple(foo: NamedMultipleStruct, divisor: i128) { + if foo.num % divisor != 0 { + panic!("foo held an i28, but it didn't divide evenly"); + } + } + + #[derive(Eq, PartialEq)] + pub struct AlignmentStruct(usize); + + impl AlignmentStruct { + const _ALIGN1SHL0: AlignmentStruct = AlignmentStruct(1 << 0); + const _ALIGN1SHL1: AlignmentStruct = AlignmentStruct(1 << 1); + const _ALIGN1SHL2: AlignmentStruct = AlignmentStruct(1 << 2); + const _ALIGN1SHL3: AlignmentStruct = AlignmentStruct(1 << 3); + const _ALIGN1SHL4: AlignmentStruct = AlignmentStruct(1 << 4); + const _ALIGN1SHL5: AlignmentStruct = AlignmentStruct(1 << 5); + const _ALIGN1SHL6: AlignmentStruct = AlignmentStruct(1 << 6); + const _ALIGN1SHL7: AlignmentStruct = AlignmentStruct(1 << 7); + const _ALIGN1SHL8: AlignmentStruct = AlignmentStruct(1 << 8); + const _ALIGN1SHL9: AlignmentStruct = AlignmentStruct(1 << 9); + const _ALIGN1SHL10: AlignmentStruct = AlignmentStruct(1 << 10); + const _ALIGN1SHL11: AlignmentStruct = AlignmentStruct(1 << 11); + const _ALIGN1SHL12: AlignmentStruct = AlignmentStruct(1 << 12); + const _ALIGN1SHL13: AlignmentStruct = AlignmentStruct(1 << 13); + const _ALIGN1SHL14: AlignmentStruct = AlignmentStruct(1 << 14); + const _ALIGN1SHL15: AlignmentStruct = AlignmentStruct(1 << 15); + } + + fn alignment_fail(align: AlignmentStruct) { + let int = 7; + assert_eq!(std::mem::align_of_val(&int) % align.0, 0); + } + + #[kani::requires(align == AlignmentStruct::_ALIGN1SHL0 || align == AlignmentStruct::_ALIGN1SHL1 || align == AlignmentStruct::_ALIGN1SHL2)] + fn alignment_pass(align: AlignmentStruct) { + let int = 7; + assert_eq!(std::mem::align_of_val(&int) % align.0, 0); + } +} + +mod should_not_derive { + use super::should_derive::*; + + struct StrStruct(&'static str); + struct PtrStruct(*const i8); + struct RefStruct(&'static mut i32); + struct RecursiveFoo(NamedMultipleStruct); + + fn no_structs_eligible(val: StrStruct, val2: PtrStruct) {} + fn recursively_eligible(val: RecursiveFoo) {} + fn some_arguments_support(supported: NamedMultipleStruct, unsupported: RefStruct) {} +} diff --git a/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected b/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected new file mode 100644 index 000000000000..6a07985199de --- /dev/null +++ b/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected @@ -0,0 +1,130 @@ +Kani generated automatic harnesses for 11 function(s): ++------------------------------+-------------------------------------+ +| Crate | Selected Function | ++====================================================================+ +| autoderive_arbitrary_structs | should_derive::AlignmentStruct | +|------------------------------+-------------------------------------| +| autoderive_arbitrary_structs | should_derive::AnonMultipleStruct | +|------------------------------+-------------------------------------| +| autoderive_arbitrary_structs | should_derive::AnonStruct | +|------------------------------+-------------------------------------| +| autoderive_arbitrary_structs | should_derive::alignment_fail | +|------------------------------+-------------------------------------| +| autoderive_arbitrary_structs | should_derive::alignment_pass | +|------------------------------+-------------------------------------| +| autoderive_arbitrary_structs | should_derive::anon_multiple_struct | +|------------------------------+-------------------------------------| +| autoderive_arbitrary_structs | should_derive::anon_struct | +|------------------------------+-------------------------------------| +| autoderive_arbitrary_structs | should_derive::named_multiple | +|------------------------------+-------------------------------------| +| autoderive_arbitrary_structs | should_derive::named_struct | +|------------------------------+-------------------------------------| +| autoderive_arbitrary_structs | should_derive::unit_struct | +|------------------------------+-------------------------------------| +| autoderive_arbitrary_structs | should_not_derive::RecursiveFoo | ++------------------------------+-------------------------------------+ + +Kani did not generate automatic harnesses for 10 function(s). ++------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------+ +| Crate | Skipped Function | Reason for Skipping | ++===============================================================================================================================================================================================================================================+ +| autoderive_arbitrary_structs | ::assert_receiver_is_total_eq | Missing Arbitrary implementation for argument(s) self: &should_derive::AlignmentStruct | +|------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_structs | ::eq | Missing Arbitrary implementation for argument(s) self: &should_derive::AlignmentStruct, other: &should_derive::AlignmentStruct | +|------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_structs | ::assert_receiver_is_total_eq | Missing Arbitrary implementation for argument(s) self: &should_derive::UnitStruct | +|------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_structs | ::eq | Missing Arbitrary implementation for argument(s) self: &should_derive::UnitStruct, other: &should_derive::UnitStruct | +|------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_structs | should_not_derive::PtrStruct | Missing Arbitrary implementation for argument(s) _: *const i8 | +|------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_structs | should_not_derive::RefStruct | Missing Arbitrary implementation for argument(s) _: &mut i32 | +|------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_structs | should_not_derive::StrStruct | Missing Arbitrary implementation for argument(s) _: &str | +|------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_structs | should_not_derive::no_structs_eligible | Missing Arbitrary implementation for argument(s) val: should_not_derive::StrStruct, val2: should_not_derive::PtrStruct | +|------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_structs | should_not_derive::recursively_eligible | Missing Arbitrary implementation for argument(s) val: should_not_derive::RecursiveFoo | +|------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_structs | should_not_derive::some_arguments_support | Missing Arbitrary implementation for argument(s) unsupported: should_not_derive::RefStruct | ++------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------+ + +should_derive::alignment_pass\ + - Status: SUCCESS\ + - Description: "assertion failed: std::mem::align_of_val(&int) % align.0 == 0" + +should_derive::alignment_fail.assertion\ + - Status: FAILURE\ + - Description: "assertion failed: std::mem::align_of_val(&int) % align.0 == 0" + +should_derive::alignment_fail.assertion\ + - Status: FAILURE\ + - Description: "attempt to calculate the remainder with a divisor of zero" + +should_derive::named_multiple.assertion\ + - Status: FAILURE\ + - Description: "attempt to calculate the remainder with a divisor of zero" + +should_derive::named_multiple.assertion\ + - Status: FAILURE\ + - Description: "attempt to calculate the remainder with overflow" + +should_derive::named_multiple.assertion\ + - Status: FAILURE\ + - Description: "foo held an i28, but it didn't divide evenly" + +should_derive::named_struct.assertion\ + - Status: FAILURE\ + - Description: "attempt to calculate the remainder with a divisor of zero" + +should_derive::named_struct.assertion\ + - Status: FAILURE\ + - Description: "foo held an u32, but it didn't divide evenly" + +should_derive::anon_multiple_struct.assertion\ + - Status: FAILURE\ + - Description: "attempt to calculate the remainder with a divisor of zero" + +should_derive::anon_multiple_struct.assertion\ + - Status: FAILURE\ + - Description: "foo held an u32, but it didn't divide evenly" + +should_derive::anon_struct.assertion\ + - Status: FAILURE\ + - Description: "attempt to calculate the remainder with a divisor of zero" + +should_derive::anon_struct.assertion\ + - Status: FAILURE\ + - Description: "foo held an u32, but it didn't divide evenly" + +should_derive::unit_struct.assertion\ + - Status: SUCCESS\ + - Description: "assertion failed: foo == bar" + +Autoharness Summary: ++------------------------------+-------------------------------------+-----------------------------+---------------------+ +| Crate | Selected Function | Kind of Automatic Harness | Verification Result | ++========================================================================================================================+ +| autoderive_arbitrary_structs | should_derive::AlignmentStruct | #[kani::proof] | Success | +|------------------------------+-------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::AnonMultipleStruct | #[kani::proof] | Success | +|------------------------------+-------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::AnonStruct | #[kani::proof] | Success | +|------------------------------+-------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::alignment_pass | #[kani::proof_for_contract] | Success | +|------------------------------+-------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::unit_struct | #[kani::proof] | Success | +|------------------------------+-------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_not_derive::RecursiveFoo | #[kani::proof] | Success | +|------------------------------+-------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::alignment_fail | #[kani::proof] | Failure | +|------------------------------+-------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::anon_multiple_struct | #[kani::proof] | Failure | +|------------------------------+-------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::anon_struct | #[kani::proof] | Failure | +|------------------------------+-------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::named_multiple | #[kani::proof] | Failure | +|------------------------------+-------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::named_struct | #[kani::proof] | Failure | ++------------------------------+-------------------------------------+-----------------------------+---------------------+ diff --git a/tests/script-based-pre/autoderive_arbitrary_structs/structs.sh b/tests/script-based-pre/autoderive_arbitrary_structs/structs.sh new file mode 100755 index 000000000000..db4a99f8be09 --- /dev/null +++ b/tests/script-based-pre/autoderive_arbitrary_structs/structs.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_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected index f00cd9c79404..06a6d3186d03 100644 --- a/tests/script-based-pre/cargo_autoharness_filter/filter.expected +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected @@ -1,4 +1,4 @@ -Kani generated automatic harnesses for 42 function(s): +Kani generated automatic harnesses for 43 function(s): +--------------------------+----------------------------------------------+ | Crate | Selected Function | +=========================================================================+ @@ -10,6 +10,8 @@ Kani generated automatic harnesses for 42 function(s): |--------------------------+----------------------------------------------| | cargo_autoharness_filter | yes_harness::f_char | |--------------------------+----------------------------------------------| +| cargo_autoharness_filter | yes_harness::f_compiler_derives_arbitrary | +|--------------------------+----------------------------------------------| | cargo_autoharness_filter | yes_harness::f_derives_arbitrary | |--------------------------+----------------------------------------------| | cargo_autoharness_filter | yes_harness::f_f128 | @@ -89,25 +91,25 @@ Kani generated automatic harnesses for 42 function(s): Kani did not generate automatic harnesses for 8 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_const_pointer | Missing Arbitrary implementation for argument(s) _y: *const i32 | -|--------------------------+----------------------------------------+------------------------------------------------------------------------------| -| cargo_autoharness_filter | no_harness::unsupported_generic | Generic Function | -|--------------------------+----------------------------------------+------------------------------------------------------------------------------| -| cargo_autoharness_filter | no_harness::unsupported_mut_pointer | Missing Arbitrary implementation for argument(s) _y: *mut i32 | -|--------------------------+----------------------------------------+------------------------------------------------------------------------------| -| cargo_autoharness_filter | no_harness::unsupported_no_arg_name | Missing Arbitrary implementation for argument(s) _: &() | -|--------------------------+----------------------------------------+------------------------------------------------------------------------------| -| cargo_autoharness_filter | no_harness::unsupported_ref | Missing Arbitrary implementation for argument(s) _y: &i32 | -|--------------------------+----------------------------------------+------------------------------------------------------------------------------| -| cargo_autoharness_filter | no_harness::unsupported_slice | Missing Arbitrary implementation for argument(s) _y: &[u8] | -|--------------------------+----------------------------------------+------------------------------------------------------------------------------| -| cargo_autoharness_filter | no_harness::unsupported_vec | Missing Arbitrary implementation for argument(s) _y: std::vec::Vec | -+--------------------------+----------------------------------------+------------------------------------------------------------------------------+ ++--------------------------+----------------------------------------+----------------------------------------------------------------------------------+ +| 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_const_pointer | Missing Arbitrary implementation for argument(s) _y: *const i32 | +|--------------------------+----------------------------------------+----------------------------------------------------------------------------------| +| cargo_autoharness_filter | no_harness::unsupported_generic | Generic Function | +|--------------------------+----------------------------------------+----------------------------------------------------------------------------------| +| cargo_autoharness_filter | no_harness::unsupported_mut_pointer | Missing Arbitrary implementation for argument(s) _y: *mut i32 | +|--------------------------+----------------------------------------+----------------------------------------------------------------------------------| +| cargo_autoharness_filter | no_harness::unsupported_no_arg_name | Missing Arbitrary implementation for argument(s) _: &() | +|--------------------------+----------------------------------------+----------------------------------------------------------------------------------| +| cargo_autoharness_filter | no_harness::unsupported_ref | Missing Arbitrary implementation for argument(s) _y: &i32 | +|--------------------------+----------------------------------------+----------------------------------------------------------------------------------| +| cargo_autoharness_filter | no_harness::unsupported_slice | Missing Arbitrary implementation for argument(s) _y: &[u8] | +|--------------------------+----------------------------------------+----------------------------------------------------------------------------------| +| cargo_autoharness_filter | no_harness::unsupported_vec | Missing Arbitrary implementation for argument(s) _y: std::vec::Vec | ++--------------------------+----------------------------------------+----------------------------------------------------------------------------------+ Autoharness: Checking function yes_harness::f_tuple against all possible inputs... Autoharness: Checking function yes_harness::f_maybe_uninit against all possible inputs... @@ -130,6 +132,7 @@ Autoharness: Checking function yes_harness::f_f128 against all possible inputs.. Autoharness: Checking function yes_harness::f_f16 against all possible inputs... Autoharness: Checking function yes_harness::f_f64 against all possible inputs... Autoharness: Checking function yes_harness::f_f32 against all possible inputs... +Autoharness: Checking function yes_harness::f_compiler_derives_arbitrary against all possible inputs... Autoharness: Checking function yes_harness::f_char against all possible inputs... Autoharness: Checking function yes_harness::f_bool against all possible inputs... Autoharness: Checking function yes_harness::f_isize against all possible inputs... @@ -167,6 +170,8 @@ Autoharness Summary: |--------------------------+----------------------------------------------+---------------------------+---------------------| | cargo_autoharness_filter | yes_harness::f_char | #[kani::proof] | Success | |--------------------------+----------------------------------------------+---------------------------+---------------------| +| cargo_autoharness_filter | yes_harness::f_compiler_derives_arbitrary | #[kani::proof] | Success | +|--------------------------+----------------------------------------------+---------------------------+---------------------| | cargo_autoharness_filter | yes_harness::f_derives_arbitrary | #[kani::proof] | Success | |--------------------------+----------------------------------------------+---------------------------+---------------------| | cargo_autoharness_filter | yes_harness::f_f128 | #[kani::proof] | Success | @@ -243,4 +248,4 @@ Autoharness Summary: |--------------------------+----------------------------------------------+---------------------------+---------------------| | cargo_autoharness_filter | yes_harness::f_usize | #[kani::proof] | Success | +--------------------------+----------------------------------------------+---------------------------+---------------------+ -Complete - 42 successfully verified functions, 0 failures, 42 total. +Complete - 43 successfully verified functions, 0 failures, 43 total. diff --git a/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs index 0237606e2931..fd6e58978a49 100644 --- a/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs @@ -4,13 +4,15 @@ // Test that the automatic harness generation feature filters functions correctly, // i.e., that it generates harnesses for a function iff: // - It is not itself a harness -// - All of its arguments implement Arbitrary, either trivially or through a user-provided implementation +// - All of its arguments implement Arbitrary, either trivially, +// through a user-provided implementation, or compiler-derived implementation. // The bodies of these functions are purposefully left as simple as possible; // the point is not to test the generated harnesses themselves, // but only that we generate the harnesses in the first place. #![feature(f16)] #![feature(f128)] +#![allow(dead_code)] extern crate kani; use kani::Arbitrary; @@ -31,14 +33,16 @@ impl Arbitrary for ManuallyImplementsArbitrary { Self { x: kani::any(), y: kani::any() } } } - -struct DoesntImplementArbitrary { +struct CompilerDerivesArbitrary { x: u8, y: u32, } - +struct DoesntImplementArbitrary<'a> { + x: &'a u8, + y: u32, +} mod yes_harness { - use crate::{DerivesArbitrary, ManuallyImplementsArbitrary}; + use crate::{CompilerDerivesArbitrary, DerivesArbitrary, ManuallyImplementsArbitrary}; use std::marker::{PhantomData, PhantomPinned}; use std::mem::MaybeUninit; use std::num::NonZero; @@ -164,6 +168,11 @@ mod yes_harness { fn f_derives_arbitrary(x: DerivesArbitrary) -> DerivesArbitrary { x } + + fn f_compiler_derives_arbitrary(x: CompilerDerivesArbitrary) -> CompilerDerivesArbitrary { + x + } + fn f_manually_implements_arbitrary( x: ManuallyImplementsArbitrary, ) -> ManuallyImplementsArbitrary {