Add support for `unaligned_volatile_load` and `unaligned_volatile_store` by ivmat · Pull Request #4673 · model-checking/kani

ivmat · 2026-07-26T16:38:40Z

Completes the volatile intrinsic family on the tracking issue #1163, on top of #4672
(volatile copy/set).

Depends on #4672 and includes its commit. GitHub cannot base a PR on a branch that
lives in a fork, so this is opened against main and its diff currently contains both
commits; the two are separate and separately titled in the commit list. Happy to rebase
and shrink this to its own commit as soon as #4672 lands, or to squash the two into a
single PR if you would rather review them together.

The dependency is real, not just presentational: the core_intrinsics.rs change below is
only correct once both volatile_set_memory and unaligned_volatile_store are
supported, and unstable_codegen! only becomes unused once all five arms are gone.

With these two, unstable_codegen! has no remaining uses anywhere in kani-compiler and
is removed — these five volatile/unaligned entries were the last gated intrinsics in the
codegen match.

Modelling

Neither intrinsic has an alignment requirement, so neither emits an alignment assertion —
tolerating a misaligned pointer is the entire purpose of the unaligned_* variants.
unaligned_volatile_load was already sketched behind the gate as a plain dereference;
unaligned_volatile_store had no codegen and no Intrinsic variant at all, and is added
mirroring volatile_store minus the alignment check. Dereferenceability is still checked
by --pointer-check, as for the aligned variants.

That leaves one question worth being explicit about: is a misaligned typed dereference
modelled byte-precisely, or does it quietly assume alignment? The tests answer it rather
than assume it. Each proof compares the accessed value against a byte-wise oracle at a
deliberately misaligned offset, so an implementation that touched the aligned word instead
would fail rather than silently pass:

Reading a u32 at byte offset 1 of a known pattern, the only correct little-endian
answer is 0x55443322; an alignment-assuming read from offset 0 would give 0x44332211.
The store proof checks the neighbouring bytes are untouched, so a wrongly-aligned write
shows up as a clobbered neighbour.
A third proof leaves the offset symbolic and compares against u32::from_le_bytes at
every offset, so the result cannot be reached by constant folding.

Tests

tests/kani/Intrinsics/Volatile/unaligned.rs — the three proofs above.
tests/kani/VolatileIntrinsics/core_intrinsics.rs — this was marked kani-verify-fail,
but that expectation existed only because unaligned_volatile_store (and
volatile_set_memory) were unsupported. With both implemented the proof verifies,
0 of 120 failed, so the header is removed and it becomes a passing test.

Note

tests/kani/VolatileIntrinsics/main_fixme.rs is left untouched (it is skipped as a fixme
test). Its test_copy_volatile names its arguments as though volatile_copy_memory were
(src, dst, count); the assertion it makes happens to hold under either argument order, so
it neither catches nor is broken by the ordering. Worth a separate look if that suite is
ever revived.

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

…mory and volatile_set_memory Implements three of the intrinsics still unchecked on tracking issue model-checking#1163. Why the existing placeholders could not simply be un-gated ---------------------------------------------------------- The two copy intrinsics already had arms, but behind `unstable_codegen!`: Intrinsic::VolatileCopyMemory => unstable_codegen!(codegen_intrinsic_copy!(Memmove)), Intrinsic::VolatileCopyNonOverlappingMemory => { unstable_codegen!(codegen_intrinsic_copy!(Memcpy)) } `unstable_codegen!` is declared `($($tt:tt)*)` and never expands its tokens -- it unconditionally emits a codegen_unimplemented_expr. Those bodies were therefore never type-checked, and they have since rotted: codegen_intrinsic_copy! no longer exists anywhere in kani-compiler. Removing the gate alone does not compile, so both arms are rewritten rather than un-gated. `volatile_set_memory` had no Intrinsic variant at all and fell through to the unsupported catch-all. Argument order -------------- The intrinsics take the destination first: volatile_copy_memory<T>(dst: *mut T, src: *const T, count: usize) volatile_copy_nonoverlapping_memory<T>(dst: *mut T, src: *const T, count: usize) whereas codegen_copy consumes source first (two successive fargs.remove(0), src then dst) and indexes farg_types[0]/farg_types[1] for the src and dst alignment assertions. Both fargs and farg_types are therefore swapped before delegating. Swapping only one silently applies each alignment check to the wrong pointer -- a defect no test using two equally-aligned buffers would catch. volatile_set_memory(dst, val, count) matches write_bytes(dst, val, count), so no swap is needed there. Soundness of reusing the non-volatile codegen --------------------------------------------- Volatility constrains what the optimizer may do -- it must not elide, duplicate or reorder the access. It is not a memory-safety property: the UB conditions for these three intrinsics are exactly those of copy, copy_nonoverlapping and write_bytes. Kani performs no optimization that volatility is meant to suppress, so there is nothing additional to model. This mirrors the existing treatment of volatile_load/volatile_store. Points-to analysis ------------------ points_to_analysis.rs matches exhaustively over Intrinsic with a terminal unimplemented!() wildcard; write_bytes is protected from it via is_identity_aliasing_intrinsic. Before this change volatile_set_memory reached that pass as Intrinsic::Unimplemented, which is explicitly handled as a no-op. Introducing the new variant would have routed it to the panicking wildcard, so it is listed alongside write_bytes in the same way. The two check_uninit visitors have non-panicking fallbacks and are unchanged. Tests ----- Layout follows model-checking#1347, which added volatile_load support. tests/kani/Intrinsics/Volatile/copy.rs both copy intrinsics move the expected bytes, including an overlapping case for volatile_copy_memory (memmove semantics) that distinguishes it from the non-overlapping variant tests/kani/Intrinsics/Volatile/set.rs volatile_set_memory fills the destination, full and partial tests/expected/intrinsics/volatile_copy/overlapping/ volatile_copy_nonoverlapping_memory on overlapping ranges fails, matching the existing copy-nonoverlapping test for the non-volatile intrinsic tests/expected/intrinsics/volatile_copy/unaligned/ a misaligned pointer fails the alignment check The unaligned pair is deliberately left out: unaligned_volatile_load's gated body is a plain dereference, which does not model the unaligned access itself, and unaligned_volatile_store has no codegen at all. Those need a separate decision about how unaligned accesses should be represented.

`docs/src/rust-feature-support/intrinsics.md` listed all three as `No`. They are now supported, so the table has to move. `Partial` rather than `Yes`, matching the neighbouring `volatile_load` and `volatile_store` rows and keeping the same Concurrency note. The memory-safety semantics are modelled exactly (they are those of the non-volatile counterparts), but the volatile guarantees themselves -- that the access is not elided or reordered, and really does touch memory -- are not, since Kani assumes sequential execution. Claiming `Yes` would overstate that and would disagree with how the two already-supported volatile intrinsics are documented.

ivmat · 2026-07-26T20:28:52Z

Marking this as a draft until #4672 is reviewed and lands. Nothing has changed in the content — this is just to make the ordering explicit, since GitHub cannot base a cross-fork PR on a fork branch and this diff therefore currently shows #4672's commits as well. Once #4672 merges I will rebase this down to its own two commits and mark it ready.

…s comment Two review findings on the previous commit. 1. The compiler matches on `Intrinsic` in three places -- codegen, the points-to analysis, and the memory-initialization visitor -- and only the first two were updated. `volatile_set_memory` therefore fell to the visitor's catch-all and produced a spurious "Kani does not support reasoning about memory initialization" failure under -Z uninit-checks, while the codegen comment claimed it behaves exactly like `write_bytes`. It now shares that arm: same argument shape (dst, val, count), same initialization effect. 2. The comment overclaimed. "The UB conditions are exactly those of the non-volatile counterpart" is false as a generalisation: the volatile family's docs additionally permit pointers outside any Rust allocation (the MMIO carve-out on ptr::read_volatile), which the non-volatile ops do not. The modelling is still sound, but for a different reason than the comment gave -- reusing codegen_copy/codegen_write_bytes checks AT LEAST the documented UB conditions, so it is conservative rather than exact: a legal MMIO access can be rejected by --pointer-check, but real UB is never missed. The comments now say that, and anchor on what these intrinsics' own docs state ("consistent with copy_nonoverlapping" / "consistent with write_bytes") rather than on a blanket claim about volatility. Also adds tests/expected/intrinsics/volatile_set/out-of-bounds, mirroring the existing write_bytes test. The happy-path test alone did not pin that reusing codegen_write_bytes actually carries its safety checks across.

Completes the volatile intrinsic family on tracking issue model-checking#1163, on top of the volatile copy/set support. With these two, `unstable_codegen!` has no remaining uses and is removed: these were the last gated intrinsics in the codegen match. Modelling --------- Neither intrinsic has an alignment requirement, so neither emits an alignment assertion -- tolerating a misaligned pointer is the whole point of the `unaligned_*` variants. `unaligned_volatile_load` was already sketched (behind the gate) as a plain dereference; `unaligned_volatile_store` had no codegen and no Intrinsic variant at all, and is added mirroring `volatile_store` minus the alignment check. Dereferenceability is still checked by --pointer-check, as for the aligned variants. The question this leaves is whether a misaligned typed dereference is modelled byte-precisely rather than silently assuming alignment. The tests answer it directly rather than assuming: each proof compares the accessed value against a byte-wise oracle at a deliberately misaligned offset, so an implementation that quietly touched the *aligned* word would fail rather than pass. Reading a u32 at byte offset 1 of a known pattern, the only correct little-endian answer is 0x55443322; an alignment-assuming read from offset 0 would give 0x44332211. A third proof leaves the offset symbolic and compares against u32::from_le_bytes at every offset, so the result cannot be reached by constant folding. Tests ----- tests/kani/Intrinsics/Volatile/unaligned.rs byte-precise load at a misaligned offset; byte-precise store checking the neighbouring bytes are untouched; symbolic-offset load against a byte-wise oracle. tests/kani/VolatileIntrinsics/core_intrinsics.rs was marked kani-verify-fail; that expectation existed only because unaligned_volatile_store (and volatile_set_memory) were unsupported. With both implemented the proof verifies -- 0 of 120 failed -- so the kani-verify-fail header is removed and it becomes a passing test. Note: tests/kani/VolatileIntrinsics/main_fixme.rs is left untouched (it is skipped as a fixme test). Its test_copy_volatile names its arguments as though volatile_copy_memory were (src, dst, count); the assertion it makes happens to hold under either argument order, so it neither catches nor is broken by the ordering. Worth a separate look if that suite is ever revived.

…ort table Same reasoning as for the copy/set trio: the table listed both as `No`, and `Partial` matches the neighbouring volatile rows. The memory-safety semantics are modelled -- including the byte-precise misaligned access these two exist for -- but the volatile guarantees are not, since Kani assumes sequential execution.

…rop endianness assumption Review findings on the previous commit. The first is a regression the commit introduced and is the reason for this one. 1. ICE. Adding the `UnalignedVolatileStore` variant without teaching the points-to analysis about it routed it into that pass's terminal `unimplemented!()`. Before this feature the intrinsic resolved to `Intrinsic::Unimplemented`, which the pass handles gracefully -- so the feature turned a clean "unsupported" into a compiler panic for anyone running -Z uninit-checks over code calling it. It now shares the `VolatileStore` arm; the aliasing semantics (`*a = b`) are identical. The asymmetry was visible in the diff: the *load* was handled, the store was not. 2. Same omission in the memory-initialization visitor: `unaligned_volatile_store` fell to the catch-all and reported "unsupported" rather than marking its destination initialized. It now shares the `VolatileStore` arm there too. Both were the same root cause -- the compiler matches on `Intrinsic` in three places (codegen, points-to, uninit visitor) and they must be updated as a set. 3. ZST. `unaligned_volatile_store` dereferenced unconditionally, while `codegen_volatile_store` guards exactly that case ("do not attempt to dereference (and assign) a ZST"). A ZST pointer may legally be dangling-but-aligned, so the path is reachable. Guard replicated and a regression test added. 4. Tests no longer assume little-endian. The oracles now use `u32::from_ne_bytes` / `to_ne_bytes`, which is equally byte-precise and discriminates the same way -- an alignment-assuming read of bytes 0..4 differs from the correct 1..5 under either endianness -- without pinning the suite to one target. Verified: -Z uninit-checks over code calling both `unaligned_volatile_store` and `volatile_set_memory` now verifies successfully, with no panic and no spurious memory-initialization failure.

ivmat · 2026-07-26T20:52:26Z

Pushed a follow-up commit after a review pass. One item was a regression this PR itself introduced, so flagging it explicitly rather than folding it in quietly.

ICE. Adding the UnalignedVolatileStore variant without teaching the points-to analysis about it routed the intrinsic into that pass's terminal unimplemented!(). Before this feature it resolved to Intrinsic::Unimplemented, which that pass handles gracefully — so the change turned a clean "unsupported" into a compiler panic for anyone running -Z uninit-checks over code calling it. It now shares the VolatileStore arm; the aliasing semantics (*a = b) are identical. The asymmetry was visible in the diff: the load was handled and the store was not.

The same omission existed in check_uninit's visitor. Root cause for both: the compiler matches on Intrinsic in three places — codegen, points-to, and the memory-initialization visitor — and they need updating as a set.

ZST guard. unaligned_volatile_store dereferenced unconditionally, while codegen_volatile_store guards exactly that case. A ZST pointer may legally be dangling-but-aligned, so the path is reachable. Guard replicated, regression test added.

Endianness. The oracle tests no longer assume little-endian — they use u32::from_ne_bytes/to_ne_bytes, which discriminates identically (an alignment-assuming read of bytes 0..4 differs from the correct 1..5 under either endianness) without pinning the suite to one target.

Verified: -Z uninit-checks over code calling both unaligned_volatile_store and volatile_set_memory now verifies cleanly, with no panic and no spurious memory-initialization failure. Full regression on CBMC 6.10.0 introduces no failures.

The soundness comment was also reworded — see the note on #4672; the same conservative-direction correction applies here.

Copilot

Pull request overview

This PR completes support for Rust’s remaining volatile intrinsics tracked in #1163 by implementing unaligned_volatile_load / unaligned_volatile_store and (via the included dependency commit) volatile_copy_memory, volatile_copy_nonoverlapping_memory, and volatile_set_memory. It removes the last unstable_codegen!-gated volatile intrinsics from kani-compiler codegen and adds regression tests to validate both correct behavior and expected failure modes.

Changes:

Implement codegen support for unaligned_volatile_store (new Intrinsic variant) and un-gate unaligned_volatile_load by lowering it to a dereference without alignment assertions.
Implement codegen for volatile_copy_memory, volatile_copy_nonoverlapping_memory, and volatile_set_memory, including proper argument reordering for the copy intrinsics and plumbing through analyses.
Add passing and expected-failure tests for the new intrinsics and update the intrinsics support documentation to reflect partial support.

Reviewed changes

Copilot reviewed 15 out of 15 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
tests/kani/VolatileIntrinsics/core_intrinsics.rs	Removes `kani-verify-fail` header now that the intrinsic set used by the test is supported.
tests/kani/Intrinsics/Volatile/unaligned.rs	Adds byte-precise oracle proofs for unaligned volatile load/store (including symbolic offset + ZST store).
tests/kani/Intrinsics/Volatile/set.rs	Adds passing proofs for `volatile_set_memory` behavior.
tests/kani/Intrinsics/Volatile/copy.rs	Adds passing proofs for volatile copy intrinsics, including an overlap case for memmove semantics.
tests/expected/intrinsics/volatile_set/out-of-bounds/main.rs	Adds an expected-failure test for out-of-bounds `volatile_set_memory`.
tests/expected/intrinsics/volatile_set/out-of-bounds/expected	Expected output for the volatile set out-of-bounds failure.
tests/expected/intrinsics/volatile_copy/unaligned/main.rs	Adds an expected-failure test for unaligned `volatile_copy_memory` destination.
tests/expected/intrinsics/volatile_copy/unaligned/expected	Expected output for the unaligned volatile copy failure.
tests/expected/intrinsics/volatile_copy/overlapping/main.rs	Adds an expected-failure test for overlapping `volatile_copy_nonoverlapping_memory`.
tests/expected/intrinsics/volatile_copy/overlapping/expected	Expected output for the overlapping volatile copy failure.
kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs	Extends memory-init tracking for `UnalignedVolatileStore` and models `VolatileSetMemory` like `WriteBytes`.
kani-compiler/src/kani_middle/points_to/points_to_analysis.rs	Updates aliasing and store modeling for `UnalignedVolatileStore` and marks `VolatileSetMemory` identity-aliasing.
kani-compiler/src/intrinsics.rs	Adds `UnalignedVolatileStore` and `VolatileSetMemory` to the intrinsic enum and instance decoding.
kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs	Implements new intrinsic codegen arms, swaps args for volatile copy, reuses `codegen_write_bytes` for volatile set, and removes `unstable_codegen!`.
docs/src/rust-feature-support/intrinsics.md	Updates support status for the affected volatile intrinsics from No → Partial.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // `dst` overlaps `src` in `arr[1]`. `volatile_copy_memory` must
+        // still succeed here (unlike `volatile_copy_nonoverlapping_memory`).
+        let dst = src.add(1) as *mut i32;
+        core::intrinsics::volatile_copy_memory(dst, src, 2);


+            // variants. CBMC models the misaligned typed access byte-precisely,
+            // so the plain dereference is faithful -- see the byte-wise oracle
+            // tests in `tests/kani/Intrinsics/Volatile/unaligned.rs`, which
+            // compare the loaded value against `u32::from_le_bytes` at every
+            // offset. Dereferenceability itself is still checked by


+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // The call to `volatile_copy_nonoverlapping_memory` is expected to
+        // fail because the `src` region and the `dst` region overlap in
+        // `arr[1]`
+        let dst = src.add(1) as *mut i32;
+        core::intrinsics::volatile_copy_nonoverlapping_memory(dst, src, 2);
+    }


ivmat requested a review from a team as a code owner July 26, 2026 16:38

github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Jul 26, 2026

ivmat force-pushed the unaligned-volatile-intrinsics branch from 89ad219 to 68437b9 Compare July 26, 2026 16:54

ivmat marked this pull request as draft July 26, 2026 20:28

ivmat added 4 commits July 26, 2026 22:47

ivmat force-pushed the unaligned-volatile-intrinsics branch from 68437b9 to ebfdfb8 Compare July 26, 2026 20:51

feliperodri added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Jul 29, 2026

feliperodri requested a review from Copilot July 29, 2026 11:08

Copilot started reviewing on behalf of feliperodri July 29, 2026 11:09 View session

feliperodri assigned ivmat Jul 29, 2026

Copilot AI reviewed Jul 29, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add support for `unaligned_volatile_load` and `unaligned_volatile_store` - #4673

Add support for `unaligned_volatile_load` and `unaligned_volatile_store`#4673
ivmat wants to merge 6 commits into
model-checking:mainfrom
ivmat:unaligned-volatile-intrinsics

ivmat commented Jul 26, 2026

Uh oh!

ivmat commented Jul 26, 2026

Uh oh!

ivmat commented Jul 26, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

ivmat commented Jul 26, 2026

Modelling

Tests

Note

Uh oh!

ivmat commented Jul 26, 2026

Uh oh!

ivmat commented Jul 26, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants