Add support for unaligned_volatile_load and unaligned_volatile_store

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

@@ -220,8 +220,8 @@ try | No | [#267](https://github.com/model-checking/kani/issues/267) |
 type_id | Yes | |
 type_name | Yes | |
 typed_swap_nonoverlapping | Yes | |
-unaligned_volatile_load | No | See [Notes - Concurrency](#concurrency) |
-unaligned_volatile_store | No | See [Notes - Concurrency](#concurrency) |
+unaligned_volatile_load | Partial | See [Notes - Concurrency](#concurrency) |
+unaligned_volatile_store | Partial | See [Notes - Concurrency](#concurrency) |
 unchecked_add | Yes | |
 unchecked_div | Yes | |
 unchecked_mul | Yes | |

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

@@ -254,18 +254,6 @@ impl GotocCtx<'_, '_> {
             }};
         }
 
-        macro_rules! unstable_codegen {
-            ($($tt:tt)*) => {{
-                let expr = self.codegen_unimplemented_expr(
-                    &format!("'{}' intrinsic", intrinsic_str),
-                    cbmc_ret_ty,
-                    loc,
-                    "https://github.com/model-checking/kani/issues/new/choose",
-                );
-                self.codegen_expr_to_place_stable(place, expr, loc)
-            }};
-        }
-
         let intrinsic = Intrinsic::from_instance(&instance);
 
         match intrinsic {
@@ -566,12 +554,31 @@ impl GotocCtx<'_, '_> {
             Intrinsic::TruncF32 => codegen_simple_intrinsic!(Truncf),
             Intrinsic::TruncF64 => codegen_simple_intrinsic!(Trunc),
             Intrinsic::TypedSwap => self.codegen_swap(fargs, farg_types, loc),
+            // No alignment assertion for these two, by design: tolerating a
+            // misaligned pointer is the entire purpose of the `unaligned_*`
+            // 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_ne_bytes` at every
+            // offset -- native order, so the oracle stays byte-precise without
+            // assuming an endianness. Dereferenceability itself is still checked
+            // by `--pointer-check`, as for the aligned variants.
             Intrinsic::UnalignedVolatileLoad => {
-                unstable_codegen!(self.codegen_expr_to_place_stable(
-                    place,
-                    fargs.remove(0).dereference(),
-                    loc
-                ))
+                self.codegen_expr_to_place_stable(place, fargs.remove(0).dereference(), loc)
+            }
+            Intrinsic::UnalignedVolatileStore => {
+                assert!(self.place_ty_stable(place).kind().is_unit());
+                let dst = fargs.remove(0);
+                let src = fargs.remove(0);
+                let dst_typ = farg_types[0];
+                if self.is_zst_stable(pointee_type_stable(dst_typ).unwrap()) {
+                    // Do not dereference (and assign) a ZST -- same guard as
+                    // `codegen_volatile_store`. A ZST pointer may legally be
+                    // dangling-but-aligned, so this path is reachable.
+                    Stmt::skip(loc)
+                } else {
+                    dst.dereference().assign(src, loc)
+                }
             }
             Intrinsic::UncheckedDiv => codegen_op_with_div_overflow_check!(div),
             Intrinsic::UncheckedRem => codegen_op_with_div_overflow_check!(rem),

kani-compiler/src/intrinsics.rs

@@ -138,6 +138,7 @@ pub enum Intrinsic {
     TruncF64,
     TypedSwap,
     UnalignedVolatileLoad,
+    UnalignedVolatileStore,
     UncheckedDiv,
     UncheckedRem,
     Unlikely,
@@ -391,6 +392,10 @@ impl Intrinsic {
                 assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _);
                 Self::UnalignedVolatileLoad
             }
+            "unaligned_volatile_store" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_));
+                Self::UnalignedVolatileStore
+            }
             "unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr"
             | "unchecked_sub" => {
                 unreachable!("Expected intrinsic `{intrinsic_str}` to be lowered before codegen")

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

@@ -290,7 +290,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> {
                             state.extend(&lvalue_set, &state.successors(&rvalue_set));
                         }
                         // Semantically equivalent *a = b.
-                        Intrinsic::VolatileStore => {
+                        Intrinsic::VolatileStore | Intrinsic::UnalignedVolatileStore => {
                             let lvalue_set = self.successors_for_deref(state, args[0].node.clone());
                             let rvalue_set =
                                 self.successors_for_operand(state, args[1].node.clone());

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

@@ -329,7 +329,7 @@ impl MirVisitor for CheckUninitVisitor {
                             Intrinsic::VolatileLoad | Intrinsic::UnalignedVolatileLoad => {
                                 self.push_target(MemoryInitOp::Check { operand: args[0].clone() });
                             }
-                            Intrinsic::VolatileStore => {
+                            Intrinsic::VolatileStore | Intrinsic::UnalignedVolatileStore => {
                                 self.push_target(MemoryInitOp::Set {
                                     operand: args[0].clone(),
                                     value: true,

tests/expected/intrinsics/unaligned_volatile/out_of_bounds/expected

@@ -0,0 +1,14 @@
+Checking harness check_unaligned_volatile_load_out_of_bounds...
+
+check_unaligned_volatile_load_out_of_bounds.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"
+
+Checking harness check_unaligned_volatile_store_out_of_bounds...
+
+check_unaligned_volatile_store_out_of_bounds.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"
+
+Verification failed for - check_unaligned_volatile_load_out_of_bounds
+Verification failed for - check_unaligned_volatile_store_out_of_bounds

tests/expected/intrinsics/unaligned_volatile/out_of_bounds/main.rs

@@ -0,0 +1,35 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that an out-of-bounds access through `unaligned_volatile_load` and
+// `unaligned_volatile_store` is still caught.
+//
+// The `unaligned_*` variants deliberately emit no alignment assertion, and they
+// codegen the access as a bare dereference rather than going through place
+// codegen, which is where Kani normally attaches validity assertions. That makes
+// it worth pinning down that dereferenceability is nevertheless checked, by
+// CBMC's `--pointer-check`. Every other test for these intrinsics uses a valid,
+// in-bounds pointer, so none of them would notice if that check were absent.
+//
+// The pointer arithmetic here is in bounds -- `add(1)` on a four-byte array is
+// well defined -- so it is the *access* that overruns the object: reading or
+// writing a `u32` at byte offset 1 touches bytes 1..5 of a 4-byte allocation.
+// That keeps the failure attributable to the dereference rather than to the
+// offset computation.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn check_unaligned_volatile_load_out_of_bounds() {
+    let buf: [u8; 4] = [0x11, 0x22, 0x33, 0x44];
+    let p = unsafe { buf.as_ptr().add(1) } as *const u32;
+    let v = unsafe { std::intrinsics::unaligned_volatile_load(p) };
+    assert_eq!(v, v);
+}
+
+#[kani::proof]
+fn check_unaligned_volatile_store_out_of_bounds() {
+    let mut buf: [u8; 4] = [0u8; 4];
+    let p = unsafe { buf.as_mut_ptr().add(1) } as *mut u32;
+    unsafe { std::intrinsics::unaligned_volatile_store(p, 0x55443322u32) };
+    assert_eq!(buf[0], 0x00);
+}

tests/kani/Intrinsics/Volatile/unaligned.rs

@@ -0,0 +1,107 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `unaligned_volatile_load` and `unaligned_volatile_store` access
+// memory byte-precisely through a deliberately misaligned pointer.
+//
+// These intrinsics carry no alignment requirement, so the codegen emits no
+// alignment assertion for them. That makes the modelling itself the thing worth
+// testing: each proof compares against a byte-wise oracle, so an implementation
+// that quietly read or wrote the *aligned* word instead would be caught rather
+// 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, 2, 3 and 4, whereas
+// an alignment-assuming read from offset 0 would give the interpretation of
+// bytes 0, 1, 2 and 3 -- different under either endianness.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn check_unaligned_volatile_load_is_byte_precise() {
+    let buf: [u8; 8] = [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88];
+    let p = unsafe { buf.as_ptr().add(1) } as *const u32;
+    let v = unsafe { std::intrinsics::unaligned_volatile_load(p) };
+    let expect = u32::from_ne_bytes([buf[1], buf[2], buf[3], buf[4]]);
+    assert_eq!(v, expect, "unaligned load must read bytes 1, 2, 3 and 4, byte-precisely");
+}
+
+// The store direction: write a `u32` at byte offset 1 and check the neighbouring
+// bytes too, so a wrongly-aligned write shows up as a clobbered neighbour rather
+// than passing silently.
+#[kani::proof]
+fn check_unaligned_volatile_store_is_byte_precise() {
+    let mut buf: [u8; 8] = [0u8; 8];
+    let p = unsafe { buf.as_mut_ptr().add(1) } as *mut u32;
+    let val: u32 = 0x55443322;
+    let bytes = val.to_ne_bytes();
+    unsafe { std::intrinsics::unaligned_volatile_store(p, val) };
+    assert_eq!(buf[0], 0x00, "byte before the store must be untouched");
+    assert_eq!(buf[1], bytes[0]);
+    assert_eq!(buf[2], bytes[1]);
+    assert_eq!(buf[3], bytes[2]);
+    assert_eq!(buf[4], bytes[3]);
+    assert_eq!(buf[5], 0x00, "byte after the store must be untouched");
+}
+
+// Symbolic offset: the offset is not a constant, so the result cannot be reached
+// by constant folding. This is the case that would expose an alignment
+// assumption hidden behind constant propagation.
+#[kani::proof]
+fn check_unaligned_volatile_load_symbolic_offset() {
+    let buf: [u8; 8] = [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88];
+    let off: usize = kani::any();
+    kani::assume(off <= 4);
+    let p = unsafe { buf.as_ptr().add(off) } as *const u32;
+    let v = unsafe { std::intrinsics::unaligned_volatile_load(p) };
+    let expect = u32::from_ne_bytes([buf[off], buf[off + 1], buf[off + 2], buf[off + 3]]);
+    assert_eq!(v, expect, "unaligned load must agree with a byte-wise oracle at every offset");
+}
+
+// The store direction with a symbolic offset, mirroring the load above. Without
+// this, byte-precision on the store side rests on a constant offset alone, which
+// a correct simplifier could satisfy while the general path stayed wrong.
+#[kani::proof]
+fn check_unaligned_volatile_store_symbolic_offset() {
+    let mut buf: [u8; 8] = [0u8; 8];
+    let off: usize = kani::any();
+    kani::assume(off <= 4);
+    let p = unsafe { buf.as_mut_ptr().add(off) } as *mut u32;
+    let val: u32 = 0x55443322;
+    let bytes = val.to_ne_bytes();
+    unsafe { std::intrinsics::unaligned_volatile_store(p, val) };
+    // The four written bytes must land at `off`, not at the aligned word.
+    assert_eq!(buf[off], bytes[0], "store must begin at the requested byte offset");
+    assert_eq!(buf[off + 1], bytes[1]);
+    assert_eq!(buf[off + 2], bytes[2]);
+    assert_eq!(buf[off + 3], bytes[3]);
+    // Everything outside that range must be untouched, so a wrongly-aligned
+    // write shows up as a clobbered neighbour at every offset, not just one.
+    let mut i = 0;
+    while i < 8 {
+        if i < off || i >= off + 4 {
+            assert_eq!(buf[i], 0, "bytes outside the stored range must be untouched");
+        }
+        i += 1;
+    }
+}
+
+// A ZST store: `unaligned_volatile_store::<()>` must not attempt a dereference.
+// A ZST pointer may legally be dangling-but-aligned, which is why
+// `codegen_volatile_store` carries the same guard.
+#[kani::proof]
+fn check_zst_unaligned_volatile_store() {
+    let mut zst = ();
+    let p = &mut zst as *mut ();
+    unsafe { std::intrinsics::unaligned_volatile_store(p, ()) };
+}
+
+// The case the ZST guard actually exists for: a *dangling* pointer. A ZST
+// reference is allowed to be any non-null, suitably aligned address, so this is
+// a pointer safe Rust can hand to the intrinsic. Nothing is dereferenced, so
+// this must verify. The harness above passes a pointer to a real local, which a
+// dereference would happily succeed on -- so it does not exercise the guard,
+// and only this one does.
+#[kani::proof]
+fn check_dangling_zst_unaligned_volatile_store() {
+    let p = core::ptr::without_provenance_mut::<()>(core::mem::align_of::<()>());
+    unsafe { std::intrinsics::unaligned_volatile_store(p, ()) };
+}

tests/kani/VolatileIntrinsics/core_intrinsics.rs

@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
 
 #![feature(core_intrinsics)]