Autoharness: do not synthesize Arbitrary for structs with reference fields

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);

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) {}
 

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<char>         |
 |------------------------------+--------------------------------------------+------------------------------------------------------------------------------------------------------------------------|
@@ -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             |
 |------------------------------+-------------------------------------------------------------------------------+-----------------------------+---------------------|

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)'] }

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

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 |

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

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
+}