Add support for volatile_copy_memory, volatile_copy_nonoverlapping_memory and volatile_set_memory

[ivmat]

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.

Related

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.

[ivmat]

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