Add support for unaligned_volatile_load and unaligned_volatile_store

[ivmat]

Completes the volatile intrinsic family on the tracking issue #1163, following #4672
(volatile copy/set), which has since landed. This branch is rebased onto main and now
contains only its own work.

With #4672 merged and these two arms implemented, unstable_codegen! has no remaining uses
anywhere in kani-compiler and is removed — these 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, including the same zero-sized-type
guard.

That leaves two questions worth being explicit about, and the tests answer both rather than
assume them.

Is a misaligned typed dereference modelled byte-precisely, or does it quietly assume
alignment? 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. The oracle uses u32::from_ne_bytes, which keeps it
byte-precise without baking in an endianness: reading a u32 at byte offset 1 must equal the
native-order interpretation of bytes 1..5, whereas an alignment-assuming read from offset 0
would give the interpretation of bytes 0..4 — different under either endianness. Both
directions also have a symbolic-offset proof, so neither can be satisfied by constant
folding, and the store proofs check that bytes outside the written range are untouched.

Is dereferenceability still checked, given this path builds the dereference directly rather
than going through place codegen? It is, by --pointer-check, and there is now a test that
pins that down instead of asserting it in a comment.

Tests

• tests/kani/Intrinsics/Volatile/unaligned.rs — six proofs: byte-precise load and store,
  each at a constant and at a symbolic offset, plus two ZST stores — one through a valid
  pointer and one through a dangling but aligned pointer,
  without_provenance_mut(align_of::<()>()), which is the case the ZST guard actually
  exists for.
• tests/expected/intrinsics/unaligned_volatile/out_of_bounds/ — an expected-fail test for
  an out-of-bounds unaligned load and store. It accesses a u32 at byte offset 1 of a
  4-byte array, so the pointer arithmetic stays in bounds and it is the access that
  overruns the object; the failure is therefore attributable to the dereference rather than
  to the offset computation. The expected file pins that split for each harness
  separately — the offset safety check must report SUCCESS while pointer_dereference
  reports dereference failure: pointer outside object bounds.
• 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, so the
  header is removed and it becomes a passing test.

The two review-driven tests were fault-injected before being committed, in both directions.
Deleting the ZST guard turns the dangling-ZST harness from 0 VCCs into 6, of which 5 fail
with pointer dereference errors; restoring it returns the file to green. Running the
out-of-bounds test with --no-memory-safety-checks, which drops CBMC's --pointer-check,
turns both of its harnesses green and removes every pointer_dereference property —
confirming that check is what catches them.

One asymmetry worth pre-empting

The ZST guard exists on the store paths only. codegen_volatile_load and this PR's
unaligned_volatile_load both dereference unconditionally, so a zero-sized read through a
dangling-but-aligned pointer — which is legal Rust — currently produces a spurious
verification failure. I measured this: it fails identically on the already-merged
volatile_load, with the guarded store passing on the same input, so it is pre-existing
behaviour that the unaligned variant inherits rather than introduces. I have deliberately
left it alone here rather than widen this PR into codegen_volatile_load, but I am happy to
fix both in a follow-up, or here if you would prefer it.

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.

[ivmat]

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.

[ivmat]

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.

[ivmat]

One documentation fix, and a note on where the other review findings went.

The oracle comment named the wrong constructor, and that was self-inflicted. The codegen comment for
the unaligned_* intrinsics said the byte-wise oracle tests compare against u32::from_le_bytes. They
compare against u32::from_ne_bytes — deliberately, so the oracle stays byte-precise without assuming
an endianness. The endianness assumption was dropped from the tests in this branch's own earlier
follow-up commit and the comment documenting the oracle was not updated with it: a correct change that
left its own documentation lying. The comment now names from_ne_bytes and states why native order is
the right choice.

The other two findings were about #4672's files, not this PR's. This PR currently contains #4672's
commits because a cross-fork PR cannot be based on a fork branch, so the automated review attributed
them here. Both — plus a third instance of the same class that the review did not flag — are fixed on
#4672's branch, and this branch has been rebased onto the corrected version. Details are in the reply
on #4672.

On a question that may come up: the // kani-verify-fail removal from
tests/kani/VolatileIntrinsics/core_intrinsics.rs belongs to this PR rather than #4672. That file
exercises both volatile_set_memory and unaligned_volatile_store, so it still fails with only #4672
applied and begins verifying only once this half lands.

Regression re-run locally on CBMC 6.10.0 against a baseline build of de332bbb9, the commit these
two branches are based on: no failures introduced — identical failing set on baseline and branch.
kani suite 594 passed / 3 failed here vs 591 / 3 on the baseline; expected 461 / 2 vs 458 / 2. All
five failures carry #[kani::solver(z3)] and fail for want of z3 on this machine.

[Copilot]

Pull request overview

Copilot reviewed 9 out of 9 changed files in this pull request and generated no new comments.

Suppressed comments (3)

tests/kani/Intrinsics/Volatile/unaligned.rs:24

• This assertion message says "bytes 1..5" but the expected value is built from buf[1]..buf[4] (i.e., bytes [1..5) end-exclusive). Updating the message avoids ambiguity when diagnosing failures.

    assert_eq!(v, expect, "unaligned load must read bytes 1..5, byte-precisely");

tests/kani/Intrinsics/Volatile/unaligned.rs:15

• The header comment uses ranges like "bytes 1..5" / "0..4" which can be read as inclusive; since the test is indexing [1,2,3,4], it’s clearer to spell these as end-exclusive ranges to avoid confusion when reading failures.

This issue also appears on line 24 of the same file.

// than silently pass. The oracle is built with `u32::from_ne_bytes` so the test
// is byte-precise without assuming an endianness: reading a `u32` at byte offset
// 1 must equal the native-order interpretation of bytes 1..5, whereas an
// alignment-assuming read from offset 0 would give the interpretation of bytes
// 0..4 -- different under either endianness.

tests/expected/intrinsics/unaligned_volatile/out_of_bounds/expected:18

• The expected output here is much more verbose and relies on specific property IDs/status formatting (e.g., *.pointer_dereference, kani::rustc_intrinsics::offset::<...>). In the tests/expected/intrinsics/**/main.rs suites, expected files are typically the concise FAILURE\\ + message form (see tests/expected/intrinsics/simd-div-rem-overflow/expected). Consider switching to that stable format to avoid brittleness across CBMC/Kani output changes.

check_unaligned_volatile_load_out_of_bounds.pointer_dereference\
Status: FAILURE\
Description: "dereference failure: pointer outside object bounds"

check_unaligned_volatile_store_out_of_bounds.pointer_dereference\

[feliperodri]

@ivmat could you address all Copilot comments?

[ivmat]

@feliperodri on it

[Copilot]

Pull request overview

Copilot reviewed 9 out of 9 changed files in this pull request and generated no new comments.