From 2add79ed53e2f1261cd3b90c6f777655db929d42 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 29 Jul 2026 09:43:03 +0000 Subject: [PATCH 1/2] Autoharness: do not synthesize Arbitrary for structs with reference fields can_derive_arbitrary recursed into reference field types (reachable for 'static references; reference fields with a lifetime parameter were already rejected via the ADT's generic arguments), so a struct like struct HasStaticRef { r: &'static u32 } was deemed derivable. The synthesized any() then created the referent's storage inside its own body and returned a dangling reference, producing spurious 'dereference failure: dead object' verification failures in the generated harness. Reject reference fields in the derivability check. Note the asymmetry with top-level argument references, which remain supported: for those, the generated harness itself owns the referent's storage, which therefore outlives the call. Co-authored-by: Kiro --- kani-compiler/src/kani_middle/mod.rs | 9 +++++++++ .../cargo_autoharness_ref_field/Cargo.toml | 10 ++++++++++ .../cargo_autoharness_ref_field/config.yml | 4 ++++ .../ref-field.expected | 3 +++ .../cargo_autoharness_ref_field/ref-field.sh | 5 +++++ .../cargo_autoharness_ref_field/src/lib.rs | 20 +++++++++++++++++++ 6 files changed, 51 insertions(+) create mode 100644 tests/script-based-pre/cargo_autoharness_ref_field/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoharness_ref_field/config.yml create mode 100644 tests/script-based-pre/cargo_autoharness_ref_field/ref-field.expected create mode 100755 tests/script-based-pre/cargo_autoharness_ref_field/ref-field.sh create mode 100644 tests/script-based-pre/cargo_autoharness_ref_field/src/lib.rs 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/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 +} From 6380645aeae63eb859c246bbb141a6193e9120a1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 5 Aug 2026 09:44:38 +0000 Subject: [PATCH 2/2] Update autoderive_arbitrary_structs expectations for ref-field rejection The test's RefStruct/RefRefStruct cases move from derived (17 harnesses) to skipped (Missing Arbitrary implementation), matching this PR's behavior change; document the rationale in the test source. Co-authored-by: Kiro --- .../autoderive_arbitrary_structs/src/lib.rs | 2 ++ .../autoderive_arbitrary_structs/structs.expected | 10 ++++------ 2 files changed, 6 insertions(+), 6 deletions(-) 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 | |------------------------------+-------------------------------------------------------------------------------+-----------------------------+---------------------|