Add support for `volatile_copy_memory`, `volatile_copy_nonoverlapping_memory` and `volatile_set_memory` by ivmat · Pull Request #4672 · model-checking/kani

ivmat · 2026-07-26T16:21:54Z

Implements three of the intrinsics still unchecked on the tracking issue #1163:
volatile_copy_memory, volatile_copy_nonoverlapping_memory and volatile_set_memory.

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 as ($($tt:tt)*) and never expands its tokens — it always emits a
codegen_unimplemented_expr. The bodies above 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 Rust intrinsics take the destination first:

pub unsafe fn volatile_copy_memory<T>(dst: *mut T, src: *const T, count: usize);
pub unsafe fn volatile_copy_nonoverlapping_memory<T>(dst: *mut T, src: *const T, count: usize);

whereas codegen_copy consumes source first (let src = fargs.remove(0); let dst = fargs.remove(0);)
and indexes farg_types[0] / farg_types[1] for the src and dst alignment checks respectively.
Both fargs and farg_types are therefore swapped before delegating. Without swapping both, the two
alignment assertions are silently applied to the wrong pointers — a discrepancy that a test using two
equally-aligned buffers would not detect.

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's codegen 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, which already delegate to their non-volatile counterparts.

Points-to analysis

Adding the VolatileSetMemory variant required one further line. points_to_analysis.rs matches
exhaustively over Intrinsic with a final unimplemented!() wildcard; WriteBytes is protected from it
by being listed in is_identity_aliasing_intrinsic. Before this change volatile_set_memory reached the
analysis as Intrinsic::Unimplemented { .. }, which is explicitly handled as a no-op. Introducing the new
variant would have routed it to the panicking wildcard instead, so it is listed alongside WriteBytes in
the same way.

The other two visitors that match on Intrinsic
(check_uninit/ptr_uninit/uninit_visitor.rs, check_uninit/delayed_ub/initial_target_visitor.rs) have
non-panicking fallbacks, so behaviour there is unchanged.

Tests

tests/kani/Intrinsics/Volatile/copy.rs — both copy intrinsics move the expected bytes, including an
overlapping case for volatile_copy_memory (memmove semantics) to distinguish 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
tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/ test for the non-volatile intrinsic.
tests/expected/intrinsics/volatile_copy/unaligned/ — a misaligned pointer fails the alignment check.

Test layout follows #1347, which added volatile_load support.

Towards #1163. The remaining unchecked volatile entries — unaligned_volatile_load and
unaligned_volatile_store — are deliberately left out of this PR: the gated body for
unaligned_volatile_load is a plain dereference, which does not model the unaligned access itself, so
those two need a separate decision about how unaligned accesses should be represented.

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.

…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.

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

Pushed two follow-up commits after a review pass, and corrected one claim in the description above.

The comment about volatility overclaimed. It said the UB conditions are exactly those of the non-volatile counterparts. That is not right as a generalisation: the volatile family's docs additionally permit pointers outside any Rust allocation (the MMIO carve-out documented on ptr::read_volatile), which copy/copy_nonoverlapping/write_bytes do not. The modelling is still sound, but for a narrower reason, and the comments now say so: these intrinsics document their safety requirements as consistent with copy_nonoverlapping / write_bytes, so reusing that codegen checks at least the documented UB conditions. It is conservative rather than exact — a legal MMIO access may be rejected by --pointer-check, but real UB is never missed.

volatile_set_memory was missing from the memory-initialization visitor. The compiler matches on Intrinsic in three places — codegen, points-to, and check_uninit's visitor — and only the first two had been updated, so under -Z uninit-checks the intrinsic produced a spurious "does not support reasoning about memory initialization" failure. It now shares the write_bytes arm: same (dst, val, count) shape, same initialization effect.

Also added 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 carries its safety checks across.

Full regression run locally on CBMC 6.10.0: no failures introduced (the only failures are three pre-existing Quantifiers tests that fail identically on unmodified main here, for want of z3).

Copilot

Pull request overview

Adds Kani support for three previously-unchecked Rust volatile memory intrinsics by reusing the existing (non-volatile) copy/set codegen paths, extending internal analyses to understand the new intrinsic variant, and adding regression/expected-output tests to validate semantics and safety checks.

Changes:

Implement volatile_copy_memory / volatile_copy_nonoverlapping_memory by delegating to codegen_copy with correct (dst, src) argument/type swapping.
Add a new Intrinsic::VolatileSetMemory variant and implement it via codegen_write_bytes, plus update points-to and uninitialized-memory analyses.
Add new kani + expected tests for happy paths and key failures (overlap, unaligned, out-of-bounds), and update the intrinsics support documentation.

Reviewed changes

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

Show a summary per file

File	Description
tests/kani/Intrinsics/Volatile/set.rs	New proof harnesses validating successful `volatile_set_memory` behavior.
tests/kani/Intrinsics/Volatile/copy.rs	New proof harnesses validating both volatile copy intrinsics, including an overlapping memmove case.
tests/expected/intrinsics/volatile_set/out-of-bounds/main.rs	Expected-failure test ensuring OOB volatile set is caught (mirrors `write_bytes`).
tests/expected/intrinsics/volatile_set/out-of-bounds/expected	Expected output for the volatile set OOB failure.
tests/expected/intrinsics/volatile_copy/unaligned/main.rs	Expected-failure test ensuring misaligned `dst` is caught and swap is correct.
tests/expected/intrinsics/volatile_copy/unaligned/expected	Expected output for the unaligned volatile copy failure.
tests/expected/intrinsics/volatile_copy/overlapping/main.rs	Expected-failure test ensuring nonoverlapping volatile copy rejects overlap.
tests/expected/intrinsics/volatile_copy/overlapping/expected	Expected output for the overlap failure.
kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs	Treat `VolatileSetMemory` like `WriteBytes` for initialization tracking.
kani-compiler/src/kani_middle/points_to/points_to_analysis.rs	Mark `VolatileSetMemory` as identity-aliasing to avoid panicking wildcard handling.
kani-compiler/src/intrinsics.rs	Add `VolatileSetMemory` variant and map `volatile_set_memory` name/signature to it.
kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs	Implement volatile copy intrinsics via `codegen_copy` (with swap) and volatile set via `codegen_write_bytes`.
docs/src/rust-feature-support/intrinsics.md	Update support status for the three intrinsics to “Partial”.

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

All three `volatile_copy` tests formed their `dst` by casting a pointer derived from `arr.as_ptr()` (a shared borrow) to `*mut i32` and then wrote through it, which is undefined behavior in its own right. For the two `tests/expected` harnesses this weakened what they prove: each is meant to fail for exactly one reason -- the overlap precondition and the alignment precondition respectively -- and a second, unintended source of UB means the harness may fail for a reason nobody named. Both pointers are now derived from `arr.as_mut_ptr()`, leaving the intended precondition as the only thing violated. Checked with Miri on the non-volatile counterparts (`ptr::copy` / `ptr::copy_nonoverlapping`, whose aliasing and alignment requirements are the ones these intrinsics' docs defer to): before, the overlapping harness reported a SharedReadOnly write violation instead of the overlap it is named for; after, it reports `copy_nonoverlapping called on overlapping ranges`, the unaligned harness reports only the alignment violation, and the `tests/kani` overlap proof runs clean with its assertions intact.

ivmat · 2026-07-30T17:08:30Z

Three test fixes from a review pass, all the same defect class.

The dst pointers in the copy tests were derived from a shared borrow. All three harnesses formed
dst by casting a pointer derived from arr.as_ptr() to *mut i32 and then wrote through it, which is
undefined behavior under Rust's aliasing rules regardless of what the intrinsic does with it. Both
pointers are now derived from arr.as_mut_ptr().

For the two tests/expected harnesses this was not just a technicality, and it is the sharper reason to
care: each is meant to fail for exactly one stated reason — the overlap precondition in
volatile_copy/overlapping, the alignment precondition in volatile_copy/unaligned — and a second,
unintended source of UB means the harness can pass its expected file while proving less than it
claims. Checked under Miri on the non-volatile counterparts (ptr::copy /
ptr::copy_nonoverlapping, whose aliasing requirements are the ones these intrinsics' docs defer to):
before, volatile_copy/overlapping reported a SharedReadOnly write violation rather than the overlap
it is named for; after, it reports copy_nonoverlapping called on overlapping ranges, the unaligned
harness reports only the misalignment, and the tests/kani overlap proof runs clean with its three
assertions intact.

One of the three was not reported. The automated review found the instances in
tests/kani/Intrinsics/Volatile/copy.rs and tests/expected/intrinsics/volatile_copy/overlapping; the
one in tests/expected/intrinsics/volatile_copy/unaligned came out of grepping the diff for the whole
pattern afterwards. Worth stating plainly, since it was the same mistake made three times in one PR.

Also re-verified, since missing it caused two earlier defects here: all three places that match on
Intrinsic — codegen, points-to, and check_uninit's visitor — cover all three intrinsics, and the two
pre-existing copy arms in points-to and the uninit visitor already handle the reversed
(dst, src, count) order correctly.

Regression re-run locally on CBMC 6.10.0 (the version this tree's kani-dependencies declares),
against a baseline build of de332bbb9, the commit this branch is based on: no failures introduced
— the failing set is identical on the baseline and on this branch, test for test. kani suite 593
passed / 3 failed here vs 591 / 3 on the baseline; expected suite 461 / 2 vs 458 / 2. All five
failures carry #[kani::solver(z3)] and fail because z3 is not installed on this machine, not because
of anything in this PR.

One correction to my earlier comment while I am here: it said "the only failures are three pre-existing
Quantifiers tests ... for want of z3". The cause was right but the set was incomplete — there are
five such tests, the two others being
expected/function-contract/as-assertions/assert-postconditions.rs and
expected/loop-contract/loop_assigns_for_vec.rs. Same cause, wider than stated.

ivmat · 2026-07-30T20:21:17Z

One practical note for whoever reviews or lands this, from exercising the new codegen end-to-end.

I ran the five now-supported intrinsics against real harnesses — the ones in verify-rust-std's challenge-2 set, which have sat #[cfg(not(kani))]-gated precisely because Kani refused them. Four verify in about a second each. The fifth, the self-overlapping volatile_copy_memory case, ran 40 minutes and 12.3 GB without converging.

That wall is the harness, not this PR's codegen. The harness was written as:

let shift: usize = kani::any();
kani::assume(shift >= 1 && shift < N);
...
unsafe { volatile_copy_memory(dst_ptr, src_ptr, N - shift) };
for i in 0..(N - shift) {
    assert_eq!(buf[i + shift], original[i]);
}

A symbolic shift combined with for i in 0..(N - shift) puts a symbolic trip count in the formula. That is the same self-overlap wall plain copy hits, and verify-rust-std already contains the resolution — its check_copy_overlapping_shift_no_ub uses a fixed representative SHIFT plus a symbolic index the solver may choose freely, which is equivalent in coverage without the symbolic-bound loop:

const SHIFT: usize = 3;
...
let i: usize = kani::any();
kani::assume(i < N - SHIFT);
assert_eq!(buf[i + SHIFT], original[i]);

Same harness, same property, same build: no result in 40 minutes → 0.133 s.

Worth flagging because the failure mode is misleading. This defect was invisible for months — Kani's "not currently supported" verdict fires before codegen, so the harness could never run far enough to blow up. Anyone who lands this PR and un-gates the obvious volatile_copy_memory harness will hit a 40-minute hang and could reasonably conclude the new codegen is at fault. It isn't.

How this was measured, and its limits: on a build of d4df833c8 — the Kani commit verify-rust-std currently pins — with this PR's commits and #4673's cherry-picked on top, CBMC 6.8.0. I used a graft rather than this branch directly because this branch is on nightly-2026-02-06 while verify-rust-std and its pinned Kani are on nightly-2025-11-25, so the branch as-is cannot verify that tree. So this is evidence about the composed pipeline (new codegen ⊕ CBMC) on a patched, non-official Kani — not a claim about official Kani, and not a claim that the fixed-shift harness is as strong as the symbolic one. It proves the property for a representative shift distance, not universally over distances.

ivmat · 2026-07-31T10:18:27Z

The perf-benchcomp failure here looks like gate noise rather than a regression from this PR. Sharing the evidence in case it's useful.

The emitted program is unchanged. benchcomp reports number_vccs and number_program_steps alongside the wall-clock metrics, and both are deterministic functions of the compiled program. They are identical between kani_old and kani_new for all 130 benchmarks, in all three runs on this branch. For the benchmark that tripped the gate (slice::tests::vectored_copy_fuzz_test) they are (3085, 93093) on both sides every time. In the same run its symex_runtime went 22.6156 → 22.2413 s (1.7% faster) while solver_runtime rose 55%.

That matches the diff: the compiler-side changes are five hunks, each inside a match arm keyed on VolatileCopyMemory / VolatileCopyNonOverlappingMemory / VolatileSetMemory. codegen_copy and codegen_write_bytes are called, not modified, and scripts/ is untouched, so CBMC and its flags are identical on both sides.

The same gate fires on unrelated PRs whose emitted programs are also unchanged. In the same week:

Autoharness: support generic functions #4679 (autoharness-generics) — vectored_copy_fuzz_test 100.486 → 260.364 s (2.591×), with 0 of 130 benchmarks showing any change in vccs/steps
Autoharness: support raw pointer arguments #4678 (autoharness-raw-pointers) — u32_u16_differential 14.008 → 23.847 s (1.702×), likewise 0 of 130

Both ratios are larger than the 1.5517× here.

On this branch specifically, the job also failed on 2026-07-29, on a different benchmark (u32_u16_differential, 1.918×), on a head that differs from the current one only in files under tests/ — and that same head passed this job on 2026-07-26.

The one thing that would settle it is a re-run: the failing ratio is max(new)/min(old) across six measurements of identical work, and paired with either of the other two base draws it would have been 1.145 or 1.195.

I'm not proposing a code change, since I can't find a path from this diff to that benchmark — happy to be corrected if I've missed one. Whether the threshold itself is worth revisiting is entirely your call.

feliperodri · 2026-08-01T21:19:33Z

Thanks for the contribution @ivmat!

ivmat · 2026-08-02T18:41:00Z

thank you @feliperodri for checking the PR !

…re` (model-checking#4673) Completes the volatile intrinsic family on the tracking issue model-checking#1163, following model-checking#4672 (volatile copy/set), which has since landed. This branch is rebased onto `main` and now contains only its own work. With model-checking#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 requested a review from a team as a code owner July 26, 2026 16:21

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 mentioned this pull request Jul 26, 2026

Add support for unaligned_volatile_load and unaligned_volatile_store #4673

Merged

ivmat added 2 commits July 26, 2026 18:54

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

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

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

Copilot AI reviewed Jul 29, 2026

View reviewed changes

ivmat mentioned this pull request Jul 30, 2026

Challenge 2 (partial): safety contracts + verification for 15 of 20 raw-pointer core::intrinsics model-checking/verify-rust-std#618

Open

feliperodri approved these changes Aug 1, 2026

View reviewed changes

feliperodri added this pull request to the merge queue Aug 1, 2026

Merged via the queue into model-checking:main with commit 23ff373 Aug 1, 2026
33 of 34 checks passed

Navigation Menu

Uh oh!

Add support for `volatile_copy_memory`, `volatile_copy_nonoverlapping_memory` and `volatile_set_memory` - #4672

Add support for `volatile_copy_memory`, `volatile_copy_nonoverlapping_memory` and `volatile_set_memory`#4672
feliperodri merged 4 commits into
model-checking:mainfrom
ivmat:volatile-intrinsics-support

ivmat commented Jul 26, 2026

Uh oh!

ivmat commented Jul 26, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

ivmat commented Jul 30, 2026

Uh oh!

ivmat commented Jul 30, 2026

Uh oh!

ivmat commented Jul 31, 2026

Uh oh!

feliperodri commented Aug 1, 2026

Uh oh!

Uh oh!

ivmat commented Aug 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

ivmat commented Jul 26, 2026

Why the existing placeholders could not simply be un-gated

Argument order

Soundness of reusing the non-volatile codegen

Points-to analysis

Tests

Related

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!

ivmat commented Jul 30, 2026

Uh oh!

ivmat commented Jul 30, 2026

Uh oh!

ivmat commented Jul 31, 2026

Uh oh!

feliperodri commented Aug 1, 2026

Uh oh!

Uh oh!

ivmat commented Aug 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants