Add support for volatile_copy_memory, volatile_copy_nonoverlapping_memory and volatile_set_memory

docs/src/rust-feature-support/intrinsics.md

@@ -232,10 +232,10 @@ unchecked_sub | Yes | |
 unlikely | Yes | |
 unreachable | Yes | |
 variant_count | Yes | |
-volatile_copy_memory | No | See [Notes - Concurrency](#concurrency) |
-volatile_copy_nonoverlapping_memory | No | See [Notes - Concurrency](#concurrency) |
+volatile_copy_memory | Partial | See [Notes - Concurrency](#concurrency) |
+volatile_copy_nonoverlapping_memory | Partial | See [Notes - Concurrency](#concurrency) |
 volatile_load | Partial | See [Notes - Concurrency](#concurrency) |
-volatile_set_memory | No | See [Notes - Concurrency](#concurrency) |
+volatile_set_memory | Partial | See [Notes - Concurrency](#concurrency) |
 volatile_store | Partial | See [Notes - Concurrency](#concurrency) |
 wrapping_add | Yes | |
 wrapping_mul | Yes | |

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -576,11 +576,50 @@ impl GotocCtx<'_, '_> {
             Intrinsic::UncheckedDiv => codegen_op_with_div_overflow_check!(div),
             Intrinsic::UncheckedRem => codegen_op_with_div_overflow_check!(rem),
             Intrinsic::Unlikely => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc),
-            Intrinsic::VolatileCopyMemory => unstable_codegen!(codegen_intrinsic_copy!(Memmove)),
+            // These two document their safety requirements as "consistent
+            // with `copy`" / "consistent with `copy_nonoverlapping`", so
+            // reusing `codegen_copy` checks the conditions their own docs
+            // state. Volatility itself constrains the optimizer (the access
+            // must not be elided or reordered), which Kani has no need to
+            // model since it performs no such optimization.
+            //
+            // One direction is worth being explicit about: the volatile
+            // family's docs additionally permit pointers *outside* any Rust
+            // allocation (the MMIO carve-out on `ptr::read_volatile`), which
+            // the non-volatile counterparts do not. Reusing `codegen_copy`
+            // therefore checks *at least* the documented UB conditions and is
+            // conservative rather than exact -- a legal MMIO access may be
+            // rejected by `--pointer-check`. That is incompleteness, never a
+            // missed UB, which is the safe direction for a verifier.
+            //
+            // Both intrinsics are declared as `(dst, src, count)`, but
+            // `codegen_copy` expects `fargs`/`farg_types` ordered as
+            // `[src, dst, ..]` (it does `fargs.remove(0)` for `src` followed
+            // by `fargs.remove(0)` for `dst`). So we swap the first two
+            // entries of `fargs`, and build a `farg_types` slice with the
+            // first two entries swapped as well, before delegating.
+            Intrinsic::VolatileCopyMemory => {
+                fargs.swap(0, 1);
+                let swapped_types = [farg_types[1], farg_types[0]];
+                self.codegen_copy(intrinsic_str, false, fargs, &swapped_types, Some(place), loc)
+            }
             Intrinsic::VolatileCopyNonOverlappingMemory => {
-                unstable_codegen!(codegen_intrinsic_copy!(Memcpy))
+                fargs.swap(0, 1);
+                let swapped_types = [farg_types[1], farg_types[0]];
+                self.codegen_copy(intrinsic_str, true, fargs, &swapped_types, Some(place), loc)
             }
             Intrinsic::VolatileLoad => self.codegen_volatile_load(fargs, farg_types, place, loc),
+            // `volatile_set_memory(dst, val, count)` has the same argument
+            // order as `write_bytes(dst, val, count)` (no `dst`/`src` swap is
+            // needed, unlike the two copy intrinsics above), and its docs
+            // state its safety requirements as "consistent with
+            // `write_bytes`", so `codegen_write_bytes` checks the conditions
+            // its own docs state. The same conservative-direction caveat as
+            // the copy intrinsics above applies to the MMIO carve-out.
+            Intrinsic::VolatileSetMemory => {
+                assert!(self.place_ty_stable(place).kind().is_unit());
+                self.codegen_write_bytes(fargs, farg_types, loc)
+            }
             Intrinsic::VolatileStore => {
                 assert!(self.place_ty_stable(place).kind().is_unit());
                 self.codegen_volatile_store(fargs, farg_types, loc)

kani-compiler/src/intrinsics.rs

@@ -144,6 +144,7 @@ pub enum Intrinsic {
     VolatileCopyMemory,
     VolatileCopyNonOverlappingMemory,
     VolatileLoad,
+    VolatileSetMemory,
     VolatileStore,
     VtableSize,
     VtableAlign,
@@ -424,6 +425,10 @@ impl Intrinsic {
                 assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _);
                 Self::VolatileLoad
             }
+            "volatile_set_memory" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::Uint(UintTy::U8), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_));
+                Self::VolatileSetMemory
+            }
             "volatile_store" => {
                 assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_));
                 Self::VolatileStore

kani-compiler/src/kani_middle/points_to/points_to_analysis.rs

@@ -698,6 +698,9 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
         | Intrinsic::UncheckedDiv
         | Intrinsic::UncheckedRem
         | Intrinsic::Unlikely
+        // Same argument shape/semantics as `WriteBytes` below (volatility is not
+        // an aliasing concern), so it is likewise identity-aliasing.
+        | Intrinsic::VolatileSetMemory
         | Intrinsic::VtableSize
         | Intrinsic::VtableAlign
         | Intrinsic::WrappingAdd

kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs

@@ -336,14 +336,16 @@ impl MirVisitor for CheckUninitVisitor {
                                     position: InsertPosition::After,
                                 });
                             }
-                            Intrinsic::WriteBytes => {
-                                self.push_target(MemoryInitOp::SetSliceChunk {
+                            // `volatile_set_memory(dst, val, count)` has the same shape and the
+                            // same memory-initialization effect as `write_bytes(dst, val, count)`;
+                            // volatility does not change which bytes become initialized.
+                            Intrinsic::WriteBytes | Intrinsic::VolatileSetMemory => self
+                                .push_target(MemoryInitOp::SetSliceChunk {
                                     operand: args[0].clone(),
                                     count: args[2].clone(),
                                     value: true,
                                     position: InsertPosition::After,
-                                })
-                            }
+                                }),
                             intrinsic => {
                                 self.push_target(MemoryInitOp::Unsupported {
                                     reason: format!("Kani does not support reasoning about memory initialization of intrinsic `{intrinsic:?}`."),

tests/expected/intrinsics/volatile_copy/overlapping/expected

@@ -0,0 +1 @@
+memcpy src/dst overlap

tests/expected/intrinsics/volatile_copy/overlapping/main.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `volatile_copy_nonoverlapping_memory` fails if the `dst`/`src`
+// regions overlap.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn test_volatile_copy_nonoverlapping_memory_with_overlap() {
+    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);
+    }
+}

tests/expected/intrinsics/volatile_copy/unaligned/expected

@@ -0,0 +1,2 @@
+FAILURE\
+`dst` must be properly aligned

tests/expected/intrinsics/volatile_copy/unaligned/main.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `volatile_copy_memory` fails when `dst` is not aligned.
+//
+// This specifically misaligns `dst` (and not `src`) because
+// `volatile_copy_memory` is declared as `(dst, src, count)`, the reverse of
+// the `(src, dst, ..)` order that `codegen_copy` expects internally, so
+// codegen must swap `fargs`/`farg_types` before delegating to it. Misaligning
+// `dst` while keeping `src` aligned distinguishes a correct swap (which
+// reports "`dst` must be properly aligned") from a missing/backwards swap
+// (which would instead misreport "`src` must be properly aligned").
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn test_volatile_copy_memory_unaligned_dst() {
+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // Obtain an unaligned pointer by casting into `*const i8`, adding an
+        // offset of 1 and casting back into `*mut i32`.
+        let dst_i8: *const i8 = src as *const i8;
+        let dst_unaligned = dst_i8.add(1) as *mut i32;
+        core::intrinsics::volatile_copy_memory(dst_unaligned, src, 1);
+    }
+}

tests/expected/intrinsics/volatile_set/out-of-bounds/expected

@@ -0,0 +1,2 @@
+FAILURE\
+memset destination region writeable

tests/expected/intrinsics/volatile_set/out-of-bounds/main.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `volatile_set_memory` fails if an out-of-bounds write is made.
+// Mirrors the equivalent `write_bytes` test, since the two share codegen: this
+// pins that reusing `codegen_write_bytes` really does carry its safety checks
+// over to the volatile variant, rather than only its happy path.
+#![feature(core_intrinsics)]
+use std::intrinsics::volatile_set_memory;
+
+#[kani::proof]
+fn main() {
+    let mut vec = vec![0u32; 4];
+    unsafe {
+        let vec_ptr = vec.as_mut_ptr().add(4);
+        volatile_set_memory(vec_ptr, 0xfe, 1);
+    }
+    assert_eq!(vec, [0, 0, 0, 0]);
+}

tests/kani/Intrinsics/Volatile/copy.rs

@@ -0,0 +1,57 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `volatile_copy_memory` and `volatile_copy_nonoverlapping_memory`
+// copy `count` elements from `src` to `dst`.
+//
+// `volatile_copy_memory` further allows the `src`/`dst` regions to overlap
+// (memmove semantics), while `volatile_copy_nonoverlapping_memory` requires
+// disjoint regions (memcpy semantics; the failing overlapping case is
+// checked separately under
+// `tests/expected/intrinsics/volatile_copy/overlapping`). Exercising the
+// overlapping case here for `volatile_copy_memory` also distinguishes the
+// two variants from one another: if they were accidentally coded up
+// identically (e.g. both using `memcpy`), this proof would fail.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn test_volatile_copy_memory_simple() {
+    let mut expected_val = 42;
+    let src: *mut i32 = &mut expected_val as *mut i32;
+    let mut old_val = 99;
+    let dst: *mut i32 = &mut old_val;
+    unsafe {
+        core::intrinsics::volatile_copy_memory(dst, src, 1);
+        assert!(*dst == expected_val);
+    }
+}
+
+#[kani::proof]
+fn test_volatile_copy_memory_with_overlap() {
+    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);
+        // The first value does not change
+        assert!(arr[0] == 0);
+        // The next values are copied from `arr[0..=1]`
+        assert!(arr[1] == 0);
+        assert!(arr[2] == 1);
+    }
+}
+
+#[kani::proof]
+fn test_volatile_copy_nonoverlapping_memory_simple() {
+    let mut expected_val = 42;
+    let src: *mut i32 = &mut expected_val as *mut i32;
+    let mut old_val = 99;
+    let dst: *mut i32 = &mut old_val;
+    unsafe {
+        core::intrinsics::volatile_copy_nonoverlapping_memory(dst, src, 1);
+        assert!(*dst == expected_val);
+    }
+}

tests/kani/Intrinsics/Volatile/set.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `volatile_set_memory` fills `count` elements starting at `dst`
+// with the byte value `val`.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn test_volatile_set_memory_simple() {
+    let mut arr: [u8; 4] = [0, 0, 0, 0];
+    let dst: *mut u8 = arr.as_mut_ptr();
+    unsafe {
+        core::intrinsics::volatile_set_memory(dst, 0xAB, 4);
+    }
+    assert!(arr == [0xAB, 0xAB, 0xAB, 0xAB]);
+}
+
+#[kani::proof]
+fn test_volatile_set_memory_partial() {
+    let mut arr: [u8; 4] = [1, 2, 3, 4];
+    unsafe {
+        // Only fill the first two elements.
+        let dst: *mut u8 = arr.as_mut_ptr();
+        core::intrinsics::volatile_set_memory(dst, 0, 2);
+    }
+    assert!(arr == [0, 0, 3, 4]);
+}