Repository navigation
Autoharness: do not synthesize Arbitrary for structs with reference fields - #4694
Merged
feliperodri merged 5 commits intoAug 23, 2026
Merged
Conversation
…ields
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 <kiro-agent@users.noreply.github.com>
github-actions
Bot
added
Z-EndToEndBenchCI
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 <kiro-agent@users.noreply.github.com>
# Conflicts: # tests/script-based-pre/autoderive_arbitrary_structs/structs.expected
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.
feliperodri
approved these changes
Aug 23, 2026
feliperodri
enabled auto-merge
August 23, 2026 16:43
… 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::<Field>(). 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 model-checking#4694.
feliperodri
added
the
[C] Feature / Enhancement
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
can_derive_arbitraryrecursed into reference field types, so a struct with a&'staticreference field (reference fields with lifetime parameters were already rejected via the ADT's generic arguments) was deemed derivable. The compiler-synthesizedany()then created the referent's storage inside its own body and returned a dangling reference, so the generated harness failed spuriously with "dereference failure: dead object" — a false alarm the user can do nothing about.Reject reference fields in the derivability check; such functions are now skipped with the usual "Missing Arbitrary implementation" reason. Top-level reference arguments are unaffected: for those the generated harness itself owns the referent's storage, which outlives the call.
Found while implementing #4691 (the storage-lifetime asymmetry between argument position and field position is exactly what that PR documents for slices).
Testing
New script-based test
cargo_autoharness_ref_field: asserts the struct-with-reference-field function is skipped (previously: spurious dead-object failure) while a plain&u32argument remains supported. Formatting and the compiler unit tests pass.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.