From 2add79ed53e2f1261cd3b90c6f777655db929d42 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 29 Jul 2026 09:43:03 +0000 Subject: [PATCH 1/4] 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/4] 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 | |------------------------------+-------------------------------------------------------------------------------+-----------------------------+---------------------| From 3a7b1813d46459097e5cb842393ef696d63d80fb Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 23 Aug 2026 15:43:48 +0000 Subject: [PATCH 3/4] Remove redundant cargo_autoharness_ref_field test The behavior change (structs with reference fields are not derived) is already covered by autoderive_arbitrary_structs (RefStruct/RefRefStruct now skipped as 'Missing Arbitrary implementation'). The preserved support for top-level reference arguments is already covered by autoharness-refs_immutable and autoharness-refs_mutable (takes_ref/takes_mut_ref etc.). The dedicated test added no unique coverage. --- .../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 ------------------- 5 files changed, 42 deletions(-) delete mode 100644 tests/script-based-pre/cargo_autoharness_ref_field/Cargo.toml delete mode 100644 tests/script-based-pre/cargo_autoharness_ref_field/config.yml delete mode 100644 tests/script-based-pre/cargo_autoharness_ref_field/ref-field.expected delete mode 100755 tests/script-based-pre/cargo_autoharness_ref_field/ref-field.sh delete mode 100644 tests/script-based-pre/cargo_autoharness_ref_field/src/lib.rs diff --git a/tests/script-based-pre/cargo_autoharness_ref_field/Cargo.toml b/tests/script-based-pre/cargo_autoharness_ref_field/Cargo.toml deleted file mode 100644 index 67558676829d..000000000000 --- a/tests/script-based-pre/cargo_autoharness_ref_field/Cargo.toml +++ /dev/null @@ -1,10 +0,0 @@ -# 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 deleted file mode 100644 index 18d803a38ca3..000000000000 --- a/tests/script-based-pre/cargo_autoharness_ref_field/config.yml +++ /dev/null @@ -1,4 +0,0 @@ -# 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 deleted file mode 100644 index 75c4762aeb9e..000000000000 --- a/tests/script-based-pre/cargo_autoharness_ref_field/ref-field.expected +++ /dev/null @@ -1,3 +0,0 @@ -| 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 deleted file mode 100755 index c240c9e72e2e..000000000000 --- a/tests/script-based-pre/cargo_autoharness_ref_field/ref-field.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/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 deleted file mode 100644 index 6fe0ae507ef1..000000000000 --- a/tests/script-based-pre/cargo_autoharness_ref_field/src/lib.rs +++ /dev/null @@ -1,20 +0,0 @@ -// 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 9da60917722383f1d6ba4ad286e8c12d40756465 Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 23 Aug 2026 17:29:04 +0000 Subject: [PATCH 4/4] Autoharness: consult a type's own Arbitrary impl before recursing for derivability can_derive_arbitrary recursed into an ADT field (and implements_arbitrary into a top-level &ADT pointee) without first checking whether that type already implements Arbitrary. A type with a hand-written Arbitrary impl that contains a reference field is not compiler-derivable, so nesting it in another struct -- or passing it behind a top-level reference -- was wrongly skipped, even though the synthesized any() would just call the hand-written impl via kani::any::(). Check implements_arbitrary before falling back to can_derive_arbitrary on both paths. A *bare* reference field is still rejected outright: it cannot carry a hand-written impl (orphan rule) and synthesizing it would dangle. Addresses review feedback on #4694. --- kani-compiler/src/kani_middle/mod.rs | 24 ++++++++++++----- .../autoderive_arbitrary_structs/src/lib.rs | 26 +++++++++++++++++++ .../structs.expected | 10 ++++++- 3 files changed, 52 insertions(+), 8 deletions(-) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 7645ff82d575..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,14 +413,20 @@ 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 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.) + // 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; 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 5ad09536cf02..2f8a6a0c0ae9 100644 --- a/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs +++ b/tests/script-based-pre/autoderive_arbitrary_structs/src/lib.rs @@ -78,6 +78,32 @@ mod should_derive { 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 93208fa8ab41..557db797d23f 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 15 function(s): +Kani generated automatic harnesses for 17 function(s): +------------------------------+------------------------------------------------------------------------+ | Crate | Selected Function | +=======================================================================================================+ @@ -26,10 +26,14 @@ Kani generated automatic harnesses for 15 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_to_manual | +|------------------------------+------------------------------------------------------------------------| | autoderive_arbitrary_structs | should_derive::unit_struct | +------------------------------+------------------------------------------------------------------------+ @@ -124,10 +128,14 @@ 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_to_manual | #[kani::proof] | Success | +|------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| | autoderive_arbitrary_structs | should_derive::unit_struct | #[kani::proof] | Success | |------------------------------+------------------------------------------------------------------------+-----------------------------+---------------------| | autoderive_arbitrary_structs | should_derive::alignment_fail | #[kani::proof] | Failure |