[v3risec]

Summary

Fix false positives in -Z valid-value-checks when initializing storage, forming raw pointers to fields, or accessing initialized fields of partially initialized structures.

Previously, the checker validated an entire raw-pointer pointee whenever it encountered a ProjectionElem::Deref, even when the operation did not consume the old value.

This caused valid operations such as Box::new initialization and &raw mut (*inner).strong to fail with spurious invalid-value checks.

Changes

• Classify MIR Place accesses by their operation semantics: read, store, raw address, shared/mutable borrow, and drop.
• Avoid checking unconsumed destination values during stores and raw address formation.
• Check the final projected field rather than the entire enclosing structure for supported struct/tuple projections.
• Preserve validity checks for actual reads, reference creation, intermediate pointer/reference loads, and drops.
• Support precise access to pattern-type fields while avoiding unsupported stable type-kind conversions.
• Retain conservative checking for unsupported projection forms.

Tests

Added 7 regression test files (.rs and .expected pairs), containing 25 proof harnesses:

• 16 positive harnesses covering initialization, field access, nested projections, packed fields, pattern types, and call destinations.
• 9 negative harnesses covering invalid values, reference construction, intermediate reference loads, and drops.

The tests were consolidated from independently tested regression cases.

Limitations

This change does not address existing unsupported checks for mutable casts, copy_nonoverlapping, trait objects, or the separate limitations of -Z uninit-checks.

An earlier full regression attempt encountered a Z3 timeout in Quantifiers/gcd_invariant.rs; the same test also timed out on the unmodified baseline.

Resolves #5056

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[v3risec]

The branch is up to date with current main. CI on the latest head is waiting for workflow approval.

This fixes false positives in -Z valid-value-checks during initialization stores, raw field-address formation, and access to initialized fields of partially initialized structures (#5056).

Would appreciate workflow approval when convenient. Happy to rebase again if needed. Thanks!

[Copilot]

🔵 Needs a closer look

Soundness-critical MIR validity instrumentation relies on runtime-MIR access classification and projection guarantees that require compiler-expert validation and regression execution with the pinned Rust/CBMC toolchain before approval.

No open issues 🎉

What changed in this PR

This PR addresses #5056 by making Kani’s experimental value-validity checks distinguish operations that consume existing values from stores and raw-address formation, reducing false positives during initialization and partial-structure access.

Changes:

• Classifies place accesses by operation while preserving checks for reads, borrows, intermediate loads, and drops.
• Checks final projected fields for supported projections, including pattern-type fields, while retaining conservative handling elsewhere.
• Adds 25 regression harnesses across seven test pairs covering valid operations and invalid-value detection.

File	Description
tests/​expected/​valid-value-checks/​place_access_valid.rs	Tests initialization and access to initialized fields.
tests/​expected/​valid-value-checks/​place_access_valid.expected	Requires successful verification of 12 harnesses.
tests/​expected/​valid-value-checks/​place_access_pattern.rs	Tests raw addresses and invalid reads of pattern-type fields.
tests/​expected/​valid-value-checks/​place_access_pattern.expected	Records expected pattern-field successes and failure.
tests/​expected/​valid-value-checks/​place_access_packed.rs	Tests packed-field reads and raw addresses.
tests/​expected/​valid-value-checks/​place_access_packed.expected	Requires successful packed-field verification.
tests/​expected/​valid-value-checks/​place_access_invalid.rs	Tests invalid boolean reads and borrows.
tests/​expected/​valid-value-checks/​place_access_invalid.expected	Requires validity failures for five harnesses.
tests/​expected/​valid-value-checks/​place_access_intermediate.rs	Tests invalid intermediate reference loads.
tests/​expected/​valid-value-checks/​place_access_intermediate.expected	Requires failures for both intermediate-reference cases.
tests/​expected/​valid-value-checks/​place_access_drop.rs	Tests dropping an invalid value before replacement.
tests/​expected/​valid-value-checks/​place_access_drop.expected	Requires detection of the invalid dropped value.
tests/​expected/​valid-value-checks/​place_access_call_destination.rs	Tests initialization through a projected MIR call destination.
tests/​expected/​valid-value-checks/​place_access_call_destination.expected	Requires successful call-destination verification.
kani-compiler/​src/​kani_middle/​transform/​check_values.rs	Adds operation-aware validity checks and precise field handling.

_{Review effort: Balanced}