diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 2f7aedf59663..bed0e2d50322 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -315,6 +315,15 @@ fn can_derive_arbitrary( if let TyKind::RigidTy(RigidTy::Adt(..)) = ty.kind() { fields_impl_arbitrary &= can_derive_arbitrary(ty, kani_any_def, ty_arbitrary_cache); + } else if let TyKind::RigidTy(RigidTy::Ref(..)) = ty.kind() { + // A reference *field* cannot be synthesized: the storage for the referent + // would live inside the synthesized `any()` body and dangle once it + // returns. (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..5ad09536cf02 100644 --- a/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs +++ b/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs @@ -70,6 +70,8 @@ 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) {} diff --git a/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected b/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected index 1352713e50dd..94b075966387 100644 --- a/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected +++ b/tests/script-based-pre/autoderive_arbitrary_structs/structs.expected @@ -1,4 +1,4 @@ -Kani generated automatic harnesses for 17 function(s): +Kani generated automatic harnesses for 15 function(s): +------------------------------+-------------------------------------------------------------------------------+ | Crate | Selected Function | +==============================================================================================================+ @@ -30,16 +30,16 @@ Kani generated automatic harnesses for 17 function(s): |------------------------------+-------------------------------------------------------------------------------| | 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::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 | |------------------------------+--------------------------------------------+------------------------------------------------------------------------------------------------------------------------| @@ -128,9 +128,7 @@ Autoharness Summary: |------------------------------+-------------------------------------------------------------------------------+-----------------------------+---------------------| | 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::unit_struct | #[kani::proof] | Success | |------------------------------+-------------------------------------------------------------------------------+-----------------------------+---------------------| diff --git a/tests/script-based-pre/cargo_autoharness_ref_field/Cargo.toml b/tests/script-based-pre/cargo_autoharness_ref_field/Cargo.toml new file mode 100644 index 000000000000..67558676829d --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_ref_field/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_ref_field" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_ref_field/config.yml b/tests/script-based-pre/cargo_autoharness_ref_field/config.yml new file mode 100644 index 000000000000..18d803a38ca3 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_ref_field/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: ref-field.sh +expected: ref-field.expected diff --git a/tests/script-based-pre/cargo_autoharness_ref_field/ref-field.expected b/tests/script-based-pre/cargo_autoharness_ref_field/ref-field.expected new file mode 100644 index 000000000000..75c4762aeb9e --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_ref_field/ref-field.expected @@ -0,0 +1,3 @@ +| cargo_autoharness_ref_field | read_direct | +| cargo_autoharness_ref_field | read_ref | Missing Arbitrary implementation for argument(s) h: HasStaticRef | +| | cargo_autoharness_ref_field | read_direct | diff --git a/tests/script-based-pre/cargo_autoharness_ref_field/ref-field.sh b/tests/script-based-pre/cargo_autoharness_ref_field/ref-field.sh new file mode 100755 index 000000000000..c240c9e72e2e --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_ref_field/ref-field.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 --list diff --git a/tests/script-based-pre/cargo_autoharness_ref_field/src/lib.rs b/tests/script-based-pre/cargo_autoharness_ref_field/src/lib.rs new file mode 100644 index 000000000000..6fe0ae507ef1 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_ref_field/src/lib.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that autoharness does not deem a struct with a (static) reference field derivable: +// the synthesized Arbitrary implementation would create the referent's storage inside the +// synthesized any() body, and the returned reference would dangle, producing spurious +// "dead object" verification failures. + +pub struct HasStaticRef { + pub r: &'static u32, +} + +pub fn read_ref(h: HasStaticRef) -> u32 { + *h.r +} + +// Top-level reference arguments (where the harness owns the storage) remain supported. +pub fn read_direct(r: &u32) -> u32 { + *r +}