From 3708257a5fb973122d1f12b3574c8797d7809410 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sat, 24 Jan 2026 16:26:07 +1000 Subject: [PATCH 1/3] Added `volatile_store` intrinsic test programs --- .../show/volatile_store-fail.main.expected | 16 ++++++++++++++++ .../show/write_volatile-fail.main.expected | 14 ++++++++++++++ .../data/prove-rs/volatile_store-fail.rs | 11 +++++++++++ .../data/prove-rs/write_volatile-fail.rs | 10 ++++++++++ kmir/src/tests/integration/test_integration.py | 2 ++ 5 files changed, 53 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/volatile_store-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/write_volatile-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/volatile_store-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/write_volatile-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_store-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_store-fail.main.expected new file mode 100644 index 000000000..16a1ee516 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/volatile_store-fail.main.expected @@ -0,0 +1,16 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (30 steps) +└─ 3 (stuck, leaf) + #execIntrinsic ( IntrinsicFunction ( symbol ( "volatile_store" ) ) , operandCopy + function: main + span: 51 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/write_volatile-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/write_volatile-fail.main.expected new file mode 100644 index 000000000..75bff6515 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/write_volatile-fail.main.expected @@ -0,0 +1,14 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (67 steps) +└─ 3 (stuck, leaf) + #execIntrinsic ( IntrinsicFunction ( symbol ( "volatile_store" ) ) , operandMove + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_store-fail.rs b/kmir/src/tests/integration/data/prove-rs/volatile_store-fail.rs new file mode 100644 index 000000000..cc187e418 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/volatile_store-fail.rs @@ -0,0 +1,11 @@ +#![feature(core_intrinsics)] +fn main() { + let mut a: i32 = 5555; + let a_ptr = &mut a as *mut _; + + unsafe { + std::intrinsics::volatile_store(a_ptr, 7777); + } + + assert!(a == 7777); +} diff --git a/kmir/src/tests/integration/data/prove-rs/write_volatile-fail.rs b/kmir/src/tests/integration/data/prove-rs/write_volatile-fail.rs new file mode 100644 index 000000000..d708d8823 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/write_volatile-fail.rs @@ -0,0 +1,10 @@ +fn main() { + let mut a: i32 = 5555; + let a_ptr = &mut a as *mut _; + + unsafe { + std::ptr::write_volatile(a_ptr, 7777); + } + + assert!(a == 7777); +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index f3e172edd..e0abde970 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -61,6 +61,8 @@ 'transmute-maybe-uninit-fail', 'iter_next_2-fail', 'test_offset_from-fail', + 'volatile_store-fail', + 'write_volatile-fail', ] From 4d9043429d4b315a3edbb8633caab92e6330d271 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sat, 24 Jan 2026 16:41:32 +1000 Subject: [PATCH 2/3] Added `volatile_store` intrinsic to semantics --- .../src/kmir/kdist/mir-semantics/intrinsics.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md index 7b3d37533..c8294c694 100644 --- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md +++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md @@ -125,6 +125,24 @@ Execution gets stuck (no matching rule) when operands have different types or un rule #extractOperandType(_, _) => TyUnknown [owise] ``` +#### Volatile Store (`std::intrinsics::volatile_store`, `std::ptr::write_volatile`) + +The `volatile_store` intrinsic writes a value to a memory location through a pointer, ensuring the write is not +optimized away by the compiler. Unlike normal stores, volatile stores are guaranteed to occur exactly once and +in order with respect to other volatile operations. In the semantics, this is equivalent to a regular store +through a dereferenced pointer. We extract the place from the pointer operand, add a deref projection, and +write the value to that location. + +```k + rule #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandCopy(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST) + => #setLocalValue(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)), ARG2) + ... + + rule #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandMove(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST) + => #setLocalValue(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)), ARG2) + ... +``` + #### Ptr Offset Computations (`std::intrinsics::ptr_offset_from`, `std::intrinsics::ptr_offset_from_unsigned`) The `ptr_offset_from[_unsigned]` calculates the distance between two pointers within the same allocation, From 6f2330a35e8eb14534fe85b56be0879db9c7d6ce Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sat, 24 Jan 2026 16:45:56 +1000 Subject: [PATCH 3/3] Changed failing tests to passing --- .../show/volatile_store-fail.main.expected | 16 ---------------- .../show/write_volatile-fail.main.expected | 14 -------------- ...{volatile_store-fail.rs => volatile_store.rs} | 0 ...{write_volatile-fail.rs => write_volatile.rs} | 0 kmir/src/tests/integration/test_integration.py | 2 -- 5 files changed, 32 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/volatile_store-fail.main.expected delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/write_volatile-fail.main.expected rename kmir/src/tests/integration/data/prove-rs/{volatile_store-fail.rs => volatile_store.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{write_volatile-fail.rs => write_volatile.rs} (100%) diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_store-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_store-fail.main.expected deleted file mode 100644 index 16a1ee516..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/volatile_store-fail.main.expected +++ /dev/null @@ -1,16 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (30 steps) -└─ 3 (stuck, leaf) - #execIntrinsic ( IntrinsicFunction ( symbol ( "volatile_store" ) ) , operandCopy - function: main - span: 51 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/write_volatile-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/write_volatile-fail.main.expected deleted file mode 100644 index 75bff6515..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/write_volatile-fail.main.expected +++ /dev/null @@ -1,14 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (67 steps) -└─ 3 (stuck, leaf) - #execIntrinsic ( IntrinsicFunction ( symbol ( "volatile_store" ) ) , operandMove - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_store-fail.rs b/kmir/src/tests/integration/data/prove-rs/volatile_store.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/volatile_store-fail.rs rename to kmir/src/tests/integration/data/prove-rs/volatile_store.rs diff --git a/kmir/src/tests/integration/data/prove-rs/write_volatile-fail.rs b/kmir/src/tests/integration/data/prove-rs/write_volatile.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/write_volatile-fail.rs rename to kmir/src/tests/integration/data/prove-rs/write_volatile.rs diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index e0abde970..f3e172edd 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -61,8 +61,6 @@ 'transmute-maybe-uninit-fail', 'iter_next_2-fail', 'test_offset_from-fail', - 'volatile_store-fail', - 'write_volatile-fail', ]