diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 4b786adee31c..9f860bf80156 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -18,7 +18,7 @@ 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 fxhash::{FxHashMap, FxHashSet}; use kani_metadata::{ ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessKind, HarnessMetadata, KaniMetadata, @@ -390,8 +390,16 @@ fn automatic_harness_partition( crate_name: &str, kani_any_def: FnDef, ) -> (Vec, BTreeMap) { - let crate_fns = - stable_mir::all_local_items().into_iter().filter(|item| item.ty().kind().is_fn()); + let crate_fn_defs = stable_mir::local_crate().fn_defs().into_iter().collect::>(); + // Filter out CrateItems that are functions, but not functions defined in the crate itself, i.e., rustc-inserted functions + // (c.f. https://github.com/model-checking/kani/issues/4189) + let crate_fns = stable_mir::all_local_items().into_iter().filter(|item| { + if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = item.ty().kind() { + crate_fn_defs.contains(&def) + } else { + false + } + }); let included_set = make_regex_set(args.autoharness_included_patterns.clone()); let excluded_set = make_regex_set(args.autoharness_excluded_patterns.clone()); @@ -437,12 +445,15 @@ 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 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 !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(); - if !(*implements_arbitrary) { + if !impls_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 c3d78a741619..9f32820b2f75 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -6,6 +6,7 @@ use std::collections::HashSet; use crate::kani_queries::QueryDb; +use fxhash::FxHashMap; use rustc_hir::{def::DefKind, def_id::DefId as InternalDefId, def_id::LOCAL_CRATE}; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; @@ -178,7 +179,19 @@ pub fn stable_fn_def(tcx: TyCtxt, def_id: InternalDefId) -> Option { /// ``` /// 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 { +fn implements_arbitrary( + ty: Ty, + kani_any_def: FnDef, + ty_arbitrary_cache: &mut FxHashMap, +) -> bool { + if let Some(v) = ty_arbitrary_cache.get(&ty) { + return *v; + } + + if ty.kind().rigid().is_none() { + return false; + } + let kani_any_body = Instance::resolve(kani_any_def, &GenericArgs(vec![GenericArgKind::Type(ty)])) .unwrap() @@ -192,20 +205,32 @@ fn implements_arbitrary(ty: Ty, kani_any_def: FnDef) -> bool { if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = func.ty(kani_any_body.arg_locals()).unwrap().kind() { - return Instance::resolve(def, &args).is_ok(); + let res = Instance::resolve(def, &args).is_ok(); + ty_arbitrary_cache.insert(ty, res); + return res; } } 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| { +fn can_derive_arbitrary( + ty: Ty, + kani_any_def: FnDef, + ty_arbitrary_cache: &mut FxHashMap, +) -> bool { + let mut variants_can_derive = |def: AdtDef, args: GenericArgs| { 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); + for ty in fields.iter().map(|field| field.ty_with_args(&args)) { + if let TyKind::RigidTy(RigidTy::Adt(..)) = ty.kind() { + fields_impl_arbitrary &= + can_derive_arbitrary(ty, kani_any_def, ty_arbitrary_cache); + } else { + fields_impl_arbitrary &= + implements_arbitrary(ty, kani_any_def, ty_arbitrary_cache); + } } if !fields_impl_arbitrary { return false; @@ -214,16 +239,22 @@ fn can_derive_arbitrary(ty: Ty, kani_any_def: FnDef) -> bool { true }; - if let TyKind::RigidTy(RigidTy::Adt(def, _)) = ty.kind() { + if let TyKind::RigidTy(RigidTy::Adt(def, args)) = ty.kind() { + for arg in &args.0 { + if let GenericArgKind::Lifetime(..) = arg { + return false; + } + } + match def.kind() { AdtKind::Enum => { // Enums with no variants cannot be instantiated if def.num_variants() == 0 { return false; } - variants_can_derive(def) + variants_can_derive(def, args) } - AdtKind::Struct => variants_can_derive(def), + AdtKind::Struct => variants_can_derive(def, args), AdtKind::Union => false, } } else { diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index cbc026d63fd7..a0be5477bd0d 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -14,6 +14,7 @@ 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_queries::QueryDb; +use fxhash::FxHashMap; use rustc_middle::ty::TyCtxt; use stable_mir::CrateDef; use stable_mir::mir::mono::Instance; @@ -109,14 +110,14 @@ impl TransformPass for AutomaticArbitraryPass { let binding = instance.args(); let ty = binding.0[0].expect_ty(); - if implements_arbitrary(*ty, self.kani_any) { + if implements_arbitrary(*ty, self.kani_any, &mut FxHashMap::default()) { return (false, body); } - if let TyKind::RigidTy(RigidTy::Adt(def, ..)) = ty.kind() { + if let TyKind::RigidTy(RigidTy::Adt(def, args)) = ty.kind() { match def.kind() { - AdtKind::Enum => (true, self.generate_enum_body(def, body)), - AdtKind::Struct => (true, self.generate_struct_body(def, body)), + AdtKind::Enum => (true, self.generate_enum_body(def, args, body)), + AdtKind::Struct => (true, self.generate_struct_body(def, args, body)), AdtKind::Union => unexpected_ty(ty), } } else { @@ -151,7 +152,8 @@ impl AutomaticArbitraryPass { /// This function will panic if a field type does not implement Arbitrary. fn call_kani_any_for_variant( &self, - def: AdtDef, + adt_def: AdtDef, + adt_args: &GenericArgs, body: &mut MutableBody, source: &mut SourceInstruction, variant: VariantDef, @@ -160,7 +162,7 @@ impl AutomaticArbitraryPass { let mut field_locals = vec![]; // Construct nondeterministic values for each of the variant's fields - for ty in fields.iter().map(|field| field.ty()) { + for ty in fields.iter().map(|field| field.ty_with_args(adt_args)) { let lcl = self.call_kani_any_for_ty(body, ty, source); field_locals.push(lcl); } @@ -173,7 +175,7 @@ impl AutomaticArbitraryPass { ); let mut assign_instr = SourceInstruction::Terminator { bb: source.bb() - 1 }; let rvalue = Rvalue::Aggregate( - AggregateKind::Adt(def, variant.idx, GenericArgs(vec![]), None, None), + AggregateKind::Adt(adt_def, variant.idx, adt_args.clone(), 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); @@ -193,7 +195,7 @@ impl AutomaticArbitraryPass { /// _ => Enum::LastVariant /// } /// ``` - fn generate_enum_body(&self, def: AdtDef, body: Body) -> Body { + fn generate_enum_body(&self, 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); @@ -220,7 +222,7 @@ 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, &mut new_body, &mut source, variant); + self.call_kani_any_for_variant(def, &args, &mut new_body, &mut source, variant); branches.push((variant.idx.to_index() as u128, target_bb)); } @@ -246,7 +248,7 @@ impl AutomaticArbitraryPass { /// ... /// } /// ``` - fn generate_struct_body(&self, def: AdtDef, body: Body) -> Body { + fn generate_struct_body(&self, def: AdtDef, args: GenericArgs, body: Body) -> Body { assert_eq!(def.num_variants(), 1); let mut new_body = MutableBody::from(body); @@ -254,7 +256,7 @@ impl AutomaticArbitraryPass { 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); + self.call_kani_any_for_variant(def, &args, &mut new_body, &mut source, variant); new_body.into() } @@ -262,37 +264,21 @@ impl AutomaticArbitraryPass { /// 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 kani_any: FnDef, init_contracts_hook: Instance, - /// All of the automatic harness Instances that we generated in the CodegenUnits constructor - automatic_harnesses: Vec, + kani_autoharness_intrinsic: FnDef, } impl AutomaticHarnessPass { - // FIXME: this is a bit clunky. - // Historically, in codegen_crate, we reset the BodyTransformation cache on a per-unit basis, - // so the BodyTransformation constructor only accepts a CodegenUnit and thus this constructor can only accept a unit. - // Later, we changed codegen to reset the cache on a per-harness basis (for uninitialized memory instrumentation). - // So BodyTransformation should really be changed to reflect that, so that this constructor can just save the one automatic harness it should transform - // and not all of the possibilities. - pub fn new(unit: &CodegenUnit, query_db: &QueryDb) -> Self { + pub fn new(query_db: &QueryDb) -> Self { let kani_fns = query_db.kani_functions(); - let harness_intrinsic = *kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); + let kani_autoharness_intrinsic = + *kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap(); let init_contracts_hook = *kani_fns.get(&KaniHook::InitContracts.into()).unwrap(); let init_contracts_hook = Instance::resolve(init_contracts_hook, &GenericArgs(vec![])).unwrap(); - let automatic_harnesses = unit - .harnesses - .iter() - .cloned() - .filter(|harness| { - let (def, _) = harness.ty().kind().fn_def().unwrap(); - def == harness_intrinsic - }) - .collect::>(); - Self { kani_any, init_contracts_hook, automatic_harnesses } + Self { kani_any, init_contracts_hook, kani_autoharness_intrinsic } } } @@ -314,7 +300,7 @@ impl TransformPass for AutomaticHarnessPass { fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { debug!(function=?instance.name(), "AutomaticHarnessPass::transform"); - if !self.automatic_harnesses.contains(&instance) { + if instance.def.def_id() != self.kani_autoharness_intrinsic.def_id() { return (false, body); } diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 9b6cc6e403f0..e52526644aed 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -75,7 +75,7 @@ impl BodyTransformation { let safety_check_type = CheckType::new_safety_check_assert_assume(queries); 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, AutomaticHarnessPass::new(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)); diff --git a/tests/script-based-pre/autoderive_arbitrary_enums/enums.expected b/tests/script-based-pre/autoderive_arbitrary_enums/enums.expected index ef97df46db3a..d5dee821e111 100644 --- a/tests/script-based-pre/autoderive_arbitrary_enums/enums.expected +++ b/tests/script-based-pre/autoderive_arbitrary_enums/enums.expected @@ -1,25 +1,23 @@ -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 generated automatic harnesses for 7 function(s): ++----------------------------+---------------------------------------------+ +| Crate | Selected Function | ++==========================================================================+ +| autoderive_arbitrary_enums | should_derive::alignment_fail | +|----------------------------+---------------------------------------------| +| autoderive_arbitrary_enums | should_derive::alignment_pass | +|----------------------------+---------------------------------------------| +| autoderive_arbitrary_enums | should_derive::foo | +|----------------------------+---------------------------------------------| +| autoderive_arbitrary_enums | should_derive::generic_recursively_eligible | +|----------------------------+---------------------------------------------| +| autoderive_arbitrary_enums | should_derive::multiple_generics_test | +|----------------------------+---------------------------------------------| +| autoderive_arbitrary_enums | should_derive::partially_used_generics_test | +|----------------------------+---------------------------------------------| +| autoderive_arbitrary_enums | should_derive::recursively_eligible | ++----------------------------+---------------------------------------------+ -Kani did not generate automatic harnesses for 10 function(s). +Kani did not generate automatic harnesses for 7 function(s). +----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------+ | Crate | Skipped Function | Reason for Skipping | +=======================================================================================================================================================================================================================================+ @@ -27,11 +25,7 @@ Kani did not generate automatic harnesses for 10 function(s). |----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| | 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::generic_unsupported_arg | Missing Arbitrary implementation for argument(s) unsupported: should_not_derive::UnsupportedGenericField | |----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| | autoderive_arbitrary_enums | should_not_derive::never | Missing Arbitrary implementation for argument(s) n: should_not_derive::Never | |----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| @@ -39,9 +33,7 @@ Kani did not generate automatic harnesses for 10 function(s). |----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------| | 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 | +| autoderive_arbitrary_enums | should_not_derive::some_arguments_support | Missing Arbitrary implementation for argument(s) unsupported_2: should_not_derive::NotAllVariantsEligible | +----------------------------+-----------------------------------------------------------------------------+----------------------------------------------------------------------------------------------------------------------------+ should_derive::alignment_pass\ @@ -64,23 +56,29 @@ should_derive::foo.assertion\ - Status: FAILURE\ - Description: "foo held an i28, but it didn't divide evenly" +should_derive::partially_used_generics_test.assertion\ + - Status: SUCCESS\ + - Description: "attempt to add with overflow" + +multiple_generics_test.assertion\ + - Status: FAILURE\ + - Description: "assertion failed: n % 2 > 0" + 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 | -+----------------------------+------------------------------------------------+-----------------------------+---------------------+ ++----------------------------+---------------------------------------------+-----------------------------+---------------------+ +| Crate | Selected Function | Kind of Automatic Harness | Verification Result | ++==============================================================================================================================+ +| autoderive_arbitrary_enums | should_derive::alignment_pass | #[kani::proof_for_contract] | Success | +|----------------------------+---------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::generic_recursively_eligible | #[kani::proof] | Success | +|----------------------------+---------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::partially_used_generics_test | #[kani::proof] | Success | +|----------------------------+---------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::recursively_eligible | #[kani::proof] | Success | +|----------------------------+---------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::alignment_fail | #[kani::proof] | Failure | +|----------------------------+---------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::foo | #[kani::proof] | Failure | +|----------------------------+---------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_enums | should_derive::multiple_generics_test | #[kani::proof] | Failure | ++----------------------------+---------------------------------------------+-----------------------------+---------------------+ diff --git a/tests/script-based-pre/autoderive_arbitrary_enums/src/lib.rs b/tests/script-based-pre/autoderive_arbitrary_enums/src/lib.rs index 04df090264b0..a9f777361561 100644 --- a/tests/script-based-pre/autoderive_arbitrary_enums/src/lib.rs +++ b/tests/script-based-pre/autoderive_arbitrary_enums/src/lib.rs @@ -15,6 +15,19 @@ mod should_derive { NamedMultipleVariant { num: i128, char: char }, } + pub enum MultipleGenerics { + First(T), + Second { val: U }, + Both(T, U), + Neither, + } + + pub enum PartiallyUsedGenerics { + Data(T), + Count(usize), + Optional(Option), + } + fn foo(foo: Foo, divisor: i128) { match foo { Foo::UnitVariant @@ -26,6 +39,27 @@ mod should_derive { } } + fn multiple_generics_test(foo: MultipleGenerics) -> usize { + match foo { + MultipleGenerics::First(n) => { + assert!(n % 2 > 0); + n % 2 + } + _ => 0, + } + } + + fn partially_used_generics_test( + foo: PartiallyUsedGenerics>, bool>, + ) -> usize { + match foo { + PartiallyUsedGenerics::Data(opt) => { + opt.unwrap_or(Some((0, 0))).unwrap_or((0, 0)).1 as usize + 100 + } + _ => 0, + } + } + #[derive(Eq, PartialEq)] pub enum AlignmentEnum { _Align1Shl0 = 1 << 0, @@ -56,10 +90,23 @@ mod should_derive { let int = 7; assert_eq!(std::mem::align_of_val(&int) % (align as usize), 0); } + + enum RecursivelyEligible { + Foo(Foo), + } + + enum ComplexGenerics { + First(Result), + Second(MultipleGenerics), + Third((T, U)), + } + + fn recursively_eligible(val: RecursivelyEligible) {} + fn generic_recursively_eligible(val: ComplexGenerics) {} } mod should_not_derive { - use super::should_derive::Foo; + use super::should_derive::*; use std::marker::PhantomPinned; // Zero-variant enum @@ -78,14 +125,20 @@ mod should_not_derive { Num(u32), } - // The enum can impl Arbitrary recursively, but we don't support that - enum RecursivelyEligible { - Foo(Foo), + // Generic enum with unsupported field type + enum UnsupportedGenericField { + First(Vec), + Second(T), } 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) {} + fn some_arguments_support( + unsupported: Foo, + supported: MultipleGenerics, + unsupported_2: NotAllVariantsEligible, + ) { + } + fn generic_unsupported_arg(unsupported: UnsupportedGenericField) {} } diff --git a/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs b/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs index a4d90d7ebd63..a2072df0a2a3 100644 --- a/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs +++ b/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs @@ -19,6 +19,17 @@ mod should_derive { char: char, } + pub struct MultipleGenerics { + first: T, + second: U, + } + + pub struct PartiallyUsedGenerics { + data: T, + count: usize, + optional: Option, + } + fn unit_struct(foo: UnitStruct, bar: UnitStruct) -> UnitStruct { assert_eq!(foo, bar); foo @@ -48,6 +59,17 @@ mod should_derive { } } + fn multiple_generics_test(foo: MultipleGenerics) -> usize { + assert!(foo.first % 2 > 0); + foo.first % 2 + } + + fn partially_used_generics_test( + foo: PartiallyUsedGenerics>, bool>, + ) -> usize { + foo.data.unwrap_or(Some((0, 0))).unwrap_or((0, 0)).1 as usize + 100 + } + #[derive(Eq, PartialEq)] pub struct AlignmentStruct(usize); @@ -80,6 +102,16 @@ mod should_derive { let int = 7; assert_eq!(std::mem::align_of_val(&int) % align.0, 0); } + + struct RecursiveFoo(NamedMultipleStruct); + pub struct ComplexGenerics { + data: Result, + mapping: MultipleGenerics, + pair: (T, U), + } + + fn recursively_eligible(val: RecursiveFoo) {} + fn generic_recursively_eligible(val: ComplexGenerics) {} } mod should_not_derive { @@ -88,9 +120,18 @@ mod should_not_derive { struct StrStruct(&'static str); struct PtrStruct(*const i8); struct RefStruct(&'static mut i32); - struct RecursiveFoo(NamedMultipleStruct); + + pub struct UnsupportedGenericField { + outer: T, + inner: Vec, + } fn no_structs_eligible(val: StrStruct, val2: PtrStruct) {} - fn recursively_eligible(val: RecursiveFoo) {} - fn some_arguments_support(supported: NamedMultipleStruct, unsupported: RefStruct) {} + fn some_arguments_support( + supported: NamedMultipleStruct, + supported_2: MultipleGenerics, + unsupported: RefStruct, + ) { + } + fn generic_unsupported_arg(unsupported: UnsupportedGenericField) {} } diff --git a/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected b/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected index 6a07985199de..cacc7e798db6 100644 --- a/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected +++ b/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected @@ -1,31 +1,31 @@ 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 | Selected Function | ++============================================================================+ +| 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::multiple_generics_test | +|------------------------------+---------------------------------------------| +| autoderive_arbitrary_structs | should_derive::named_multiple | +|------------------------------+---------------------------------------------| +| autoderive_arbitrary_structs | should_derive::named_struct | +|------------------------------+---------------------------------------------| +| autoderive_arbitrary_structs | should_derive::partially_used_generics_test | +|------------------------------+---------------------------------------------| +| autoderive_arbitrary_structs | should_derive::unit_struct | +|------------------------------+---------------------------------------------| +| autoderive_arbitrary_structs | should_derive::recursively_eligible | +|------------------------------+---------------------------------------------| +| autoderive_arbitrary_structs | should_derive::generic_recursively_eligible | +|------------------------------+---------------------------------------------| + +Kani did not generate automatic harnesses for 7 function(s). +------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------+ | Crate | Skipped Function | Reason for Skipping | +===============================================================================================================================================================================================================================================+ @@ -37,16 +37,10 @@ Kani did not generate automatic harnesses for 10 function(s). |------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------| | 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::generic_unsupported_arg | Missing Arbitrary implementation for argument(s) unsupported: should_not_derive::UnsupportedGenericField | |------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------| | 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 | +------------------------------+-------------------------------------------------------------------------------+--------------------------------------------------------------------------------------------------------------------------------+ @@ -102,29 +96,37 @@ should_derive::unit_struct.assertion\ - Status: SUCCESS\ - Description: "assertion failed: foo == bar" +should_derive::partially_used_generics_test.assertion\ + - Status: SUCCESS\ + - Description: "attempt to add with overflow" + +multiple_generics_test.assertion\ + - Status: FAILURE\ + - Description: "assertion failed: foo.first % 2 > 0" + 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 | -+------------------------------+-------------------------------------+-----------------------------+---------------------+ ++------------------------------+---------------------------------------------+-----------------------------+---------------------+ +| Crate | Selected Function | Kind of Automatic Harness | Verification Result | ++================================================================================================================================+ +| autoderive_arbitrary_structs | should_derive::alignment_pass | #[kani::proof_for_contract] | Success | +|------------------------------+---------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::partially_used_generics_test | #[kani::proof] | Success | +|------------------------------+---------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::unit_struct | #[kani::proof] | Success | +|------------------------------+---------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::recursively_eligible | #[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::multiple_generics_test | #[kani::proof] | Failure | +|------------------------------+---------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::named_multiple | #[kani::proof] | Failure | +|------------------------------+---------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::named_struct | #[kani::proof] | Failure | ++------------------------------+---------------------------------------------+-----------------------------+---------------------+ +| autoderive_arbitrary_structs | should_derive::generic_recursively_eligible | #[kani::proof] | Success | +|------------------------------+---------------------------------------------+-----------------------------+---------------------| diff --git a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected index 2afedc9e0b0a..b963f7d6a912 100644 --- a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected +++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected @@ -1,11 +1,9 @@ -Kani generated automatic harnesses for 7 function(s): +Kani generated automatic harnesses for 6 function(s): +-----------------------------+---------------------------------------------+ | Crate | Selected Function | +===========================================================================+ | cargo_autoharness_contracts | should_fail::max | |-----------------------------+---------------------------------------------| -| cargo_autoharness_contracts | should_pass::alignment::Alignment | -|-----------------------------+---------------------------------------------| | cargo_autoharness_contracts | should_pass::alignment::Alignment::as_usize | |-----------------------------+---------------------------------------------| | cargo_autoharness_contracts | should_pass::div | @@ -57,8 +55,6 @@ Autoharness Summary: +-----------------------------+---------------------------------------------+-----------------------------+---------------------+ | Crate | Selected Function | Kind of Automatic Harness | Verification Result | +===============================================================================================================================+ -| cargo_autoharness_contracts | should_pass::alignment::Alignment | #[kani::proof] | Success | -|-----------------------------+---------------------------------------------+-----------------------------+---------------------| | cargo_autoharness_contracts | should_pass::alignment::Alignment::as_usize | #[kani::proof_for_contract] | Success | |-----------------------------+---------------------------------------------+-----------------------------+---------------------| | cargo_autoharness_contracts | should_pass::div | #[kani::proof_for_contract] | Success | @@ -73,4 +69,4 @@ Autoharness Summary: +-----------------------------+---------------------------------------------+-----------------------------+---------------------+ Note that `kani autoharness` sets default --harness-timeout of 60s and --default-unwind of 20. If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract). -Complete - 6 successfully verified functions, 1 failures, 7 total. +Complete - 5 successfully verified functions, 1 failures, 6 total. diff --git a/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.expected b/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.expected index cc8e9b32ca14..53a6c9a42ccb 100644 --- a/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.expected +++ b/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.expected @@ -1,4 +1,4 @@ -Kani generated automatic harnesses for 7 function(s): +Kani generated automatic harnesses for 6 function(s): +----------------------------------+----------------------------+ | Crate | Selected Function | +===============================================================+ @@ -10,8 +10,6 @@ Kani generated automatic harnesses for 7 function(s): |----------------------------------+----------------------------| | cargo_autoharness_type_invariant | Duration::new | |----------------------------------+----------------------------| -| cargo_autoharness_type_invariant | Nanoseconds | -|----------------------------------+----------------------------| | cargo_autoharness_type_invariant | Nanoseconds::as_inner | |----------------------------------+----------------------------| | cargo_autoharness_type_invariant | Nanoseconds::new_unchecked | @@ -97,8 +95,6 @@ Autoharness Summary: |----------------------------------+----------------------------+-----------------------------+---------------------| | cargo_autoharness_type_invariant | Duration::checked_sub | #[kani::proof_for_contract] | Success | |----------------------------------+----------------------------+-----------------------------+---------------------| -| cargo_autoharness_type_invariant | Nanoseconds | #[kani::proof] | Success | -|----------------------------------+----------------------------+-----------------------------+---------------------| | cargo_autoharness_type_invariant | Nanoseconds::as_inner | #[kani::proof] | Success | |----------------------------------+----------------------------+-----------------------------+---------------------| | cargo_autoharness_type_invariant | Nanoseconds::new_unchecked | #[kani::proof_for_contract] | Success | @@ -107,4 +103,4 @@ Autoharness Summary: +----------------------------------+----------------------------+-----------------------------+---------------------+ Note that `kani autoharness` sets default --harness-timeout of 60s and --default-unwind of 20. If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract). -Complete - 6 successfully verified functions, 1 failures, 7 total. +Complete - 5 successfully verified functions, 1 failures, 6 total.