diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 407b89ea8033..3713e0a3f5dc 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -275,7 +275,11 @@ fn implements_arbitrary( if let TyKind::RigidTy(RigidTy::Ref(_, inner_ty, _)) = ty.kind() { if let TyKind::RigidTy(RigidTy::Adt(..)) = inner_ty.kind() { - return can_derive_arbitrary(inner_ty, kani_any_def, ty_arbitrary_cache); + // The harness owns the referent's storage, so a top-level reference argument is + // supported whenever its pointee is: prefer the pointee's own `Arbitrary` impl (which + // may exist even for a type containing references), falling back to synthesizing one. + return implements_arbitrary(inner_ty, kani_any_def, ty_arbitrary_cache) + || can_derive_arbitrary(inner_ty, kani_any_def, ty_arbitrary_cache); } else { return implements_arbitrary(inner_ty, kani_any_def, ty_arbitrary_cache); } @@ -409,8 +413,23 @@ fn can_derive_arbitrary( let mut fields_impl_arbitrary = true; for ty in fields.iter().map(|field| field.ty_with_args(&args)) { if let TyKind::RigidTy(RigidTy::Adt(..)) = ty.kind() { + // Prefer the field type's own `Arbitrary` implementation: a hand-written + // impl can exist even for a type that itself contains references (and so is + // not compiler-derivable), and the synthesized `any()` would call it via + // `kani::any::()`. Only fall back to synthesizing one if it has none. fields_impl_arbitrary &= - can_derive_arbitrary(ty, kani_any_def, ty_arbitrary_cache); + implements_arbitrary(ty, kani_any_def, ty_arbitrary_cache) + || can_derive_arbitrary(ty, kani_any_def, ty_arbitrary_cache); + } else if let TyKind::RigidTy(RigidTy::Ref(..)) = ty.kind() { + // A bare reference *field* cannot be synthesized: the storage for the referent + // would live inside the synthesized `any()` body and dangle once it returns, + // and (unlike an ADT field) a reference type cannot carry a hand-written + // `Arbitrary` impl (orphan rule). (Only `&'static` fields reach this point: + // reference fields with a lifetime parameter make the ADT's generic arguments + // contain a lifetime, which is rejected below.) + // Note that this differs from *top-level argument* references, for which + // the harness itself owns the storage. + fields_impl_arbitrary = false; } else { fields_impl_arbitrary &= implements_arbitrary(ty, kani_any_def, ty_arbitrary_cache); 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 33fdda60a3a8..2f8a6a0c0ae9 100644 --- a/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs +++ b/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs @@ -70,12 +70,40 @@ mod should_derive { foo.data.unwrap_or(Some((0, 0))).unwrap_or((0, 0)).1 as usize + 100 } + // Structs with reference fields are skipped: synthesizing an Arbitrary implementation + // for them would need to materialize referents with arbitrary lifetimes. struct RefStruct(&'static i32); fn ref_struct(foo: RefStruct) {} struct RefRefStruct(&'static &'static i32); fn ref_ref_struct(foo: RefRefStruct) {} + // A struct with a reference field but a *hand-written* Arbitrary implementation that safely + // materializes the referent (a shared reference to a `static`). Because the field type itself + // implements Arbitrary, a struct nesting it -- and a top-level `&ManualRefStruct` argument -- + // are supported: the synthesized `any()` calls this hand-written impl via + // `kani::any::()` rather than trying to synthesize the reference itself. + // Regression test: the derivability check must consult a field/pointee type's own Arbitrary + // impl before recursing into it (and rejecting its reference field). + pub struct ManualRefStruct(&'static u8); + + impl kani::Arbitrary for ManualRefStruct { + fn any() -> Self { + static BYTE: u8 = 0; + ManualRefStruct(&BYTE) + } + } + + struct NestsManualRef { + inner: ManualRefStruct, + } + + fn nests_manual_ref(foo: NestsManualRef) { + let _ = foo.inner; + } + + fn ref_to_manual(foo: &ManualRefStruct) {} + #[derive(Eq, PartialEq)] pub struct AlignmentStruct(usize); diff --git a/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected b/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected index 55788182de79..557db797d23f 100644 --- a/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected +++ b/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected @@ -26,21 +26,25 @@ Kani generated automatic harnesses for 17 function(s): |------------------------------+------------------------------------------------------------------------| | autoderive_arbitrary_structs | should_derive::named_struct | |------------------------------+------------------------------------------------------------------------| +| autoderive_arbitrary_structs | should_derive::nests_manual_ref | +|------------------------------+------------------------------------------------------------------------| | autoderive_arbitrary_structs | should_derive::partially_used_generics_test | |------------------------------+------------------------------------------------------------------------| | autoderive_arbitrary_structs | should_derive::recursively_eligible | |------------------------------+------------------------------------------------------------------------| -| autoderive_arbitrary_structs | should_derive::ref_ref_struct | -|------------------------------+------------------------------------------------------------------------| -| autoderive_arbitrary_structs | should_derive::ref_struct | +| autoderive_arbitrary_structs | should_derive::ref_to_manual | |------------------------------+------------------------------------------------------------------------| | autoderive_arbitrary_structs | should_derive::unit_struct | +------------------------------+------------------------------------------------------------------------+ -Kani did not generate automatic harnesses for 3 function(s). +Kani did not generate automatic harnesses for 5 function(s). +------------------------------+--------------------------------------------+------------------------------------------------------------------------------------------------------------------------+ | Crate | Skipped Function | Reason for Skipping | +====================================================================================================================================================================================================+ +| autoderive_arbitrary_structs | should_derive::ref_ref_struct | Missing Arbitrary implementation for argument(s) foo: should_derive::RefRefStruct | +|------------------------------+--------------------------------------------+------------------------------------------------------------------------------------------------------------------------| +| autoderive_arbitrary_structs | should_derive::ref_struct | Missing Arbitrary implementation for argument(s) foo: should_derive::RefStruct | +|------------------------------+--------------------------------------------+------------------------------------------------------------------------------------------------------------------------| | 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 | @@ -124,13 +128,13 @@ Autoharness Summary: |------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| | autoderive_arbitrary_structs | should_derive::generic_recursively_eligible | #[kani::proof] | Success | |------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| +| autoderive_arbitrary_structs | should_derive::nests_manual_ref | #[kani::proof] | Success | +|------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| | autoderive_arbitrary_structs | should_derive::partially_used_generics_test | #[kani::proof] | Success | |------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| | autoderive_arbitrary_structs | should_derive::recursively_eligible | #[kani::proof] | Success | |------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| -| autoderive_arbitrary_structs | should_derive::ref_ref_struct | #[kani::proof] | Success | -|------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| -| autoderive_arbitrary_structs | should_derive::ref_struct | #[kani::proof] | Success | +| autoderive_arbitrary_structs | should_derive::ref_to_manual | #[kani::proof] | Success | |------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| | autoderive_arbitrary_structs | should_derive::unit_struct | #[kani::proof] | Success | |------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------|