[v3risec]

Summary

Kani incorrectly checks the destination of a volatile atomic store for prior initialization and fails to mark it as initialized after the write. As a result, a valid store to uninitialized allocated memory is rejected, and a subsequent read also fails its initialization check.

The code generator shared by atomic store and exchange also reads the previous destination value even for stores, although only exchange needs to return it.

Changes

• Generate a write-only atomic block for stores, while preserving exchange's old-value read and return behavior.
• Mark the destination as initialized after atomic stores.
• Skip the pre-store initialization check only when the intrinsic's VOLATILE argument is true. Preserve the existing check for non-volatile stores pending clarification of their from_ptr-based safety contract.
• Update the shared code generator's documentation to distinguish store and exchange behavior.

Regression tests

Added coverage for:

• Volatile integer stores initializing memory with Relaxed, Release, and SeqCst ordering.
• Volatile raw-pointer stores, including loading and dereferencing stored non-null pointers.
• Non-volatile stores updating already initialized integer and pointer storage.
• Atomic exchange returning the previous value.
• Rejection of uninitialized loads, compare-and-exchange, and exchange operations.
• Rejection of null atomic stores, including both volatile and non-volatile variants.
• Preservation of initialization checks for adjacent unwritten memory and the existing non-volatile store behavior on uninitialized memory.

Validation

Validated against upstream commit c5e65fdfc3e15ec32293f2a4c07509aebec033c9, using nightly-2026-10-23, CBMC 6.11.0, and x86_64 Linux.

Targeted validation:

• Unmodified baseline: Both volatile initialization harnesses fail, while the initialized non-volatile store and exchange harnesses pass.
• Revised compiler: All four positive harnesses pass, and all five negative harnesses produce the expected failures.
• Minimal volatile reproducer: Three failed checks on the baseline and none on the revised compiler.
• Miri: Corresponding concrete test programs pass with the experimental -Zmiri-recursive-validation flag. This is supplementary evidence, not a definitive resolution of Rust's reference-validity rules.
• Generated C: Atomic stores no longer read the previous destination value.

Broader regression results:

• Formatting checks and the unit tests run by scripts/kani-regression.sh passed.
• Expected suite: 535 passed, 13 ignored.
• UI suite: 153 passed.
• Kani suite: 627 passed, 24 ignored, with one timeout in Quantifiers/gcd_invariant.rs at 300 seconds. The same test also timed out on the unmodified baseline at 120 seconds. The focused atomic test passed separately.

The full regression script stopped at the Kani-suite timeout. Expected and UI were run independently; later suites were not run. These results do not constitute a fully passing regression run.

Scope and limitations

The volatile-store reproducer relies on Rust's raw-pointer store_volatile safety contract and uses ordinary allocated memory.

The initial reproducer used VOLATILE=false, but its validity under the from_ptr-based safety contract has not been established. This change preserves the existing non-volatile initialization check and does not resolve whether non-volatile atomic stores may initialize uninitialized storage.

This change does not implement complete volatile externally observable behavior, MMIO, or concurrency modeling.

Resolves #5114

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