From 95b076eeab37888bafc5a4085f8d7deae2285e2a Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sun, 15 Mar 2026 22:28:22 +1000 Subject: [PATCH 1/3] Added `volatile_load` intrinsic test programs --- .../data/prove-rs/read_volatile-fail.rs | 11 +++++++++++ .../show/read_volatile-fail.main.expected | 15 +++++++++++++++ .../show/volatile_load-fail.main.expected | 16 ++++++++++++++++ .../data/prove-rs/volatile_load-fail.rs | 12 ++++++++++++ kmir/src/tests/integration/test_integration.py | 2 ++ 5 files changed, 56 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/read_volatile-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/show/read_volatile-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/volatile_load-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/volatile_load-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/read_volatile-fail.rs b/kmir/src/tests/integration/data/prove-rs/read_volatile-fail.rs new file mode 100644 index 000000000..1d8f96587 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/read_volatile-fail.rs @@ -0,0 +1,11 @@ +fn main() { + let a: i32 = 5555; + let a_ptr = &a as *const _; + + let b: i32; + unsafe { + b = std::ptr::read_volatile(a_ptr); + } + + assert!(b == 5555); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/read_volatile-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/read_volatile-fail.main.expected new file mode 100644 index 000000000..ff656efd9 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/read_volatile-fail.main.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (60 steps) +└─ 3 (stuck, leaf) + #execIntrinsic ( IntrinsicFunction ( symbol ( "volatile_load" ) ) , operandMove + span: 55 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_load-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_load-fail.main.expected new file mode 100644 index 000000000..1f73a2727 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/volatile_load-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_load" ) ) , operandCopy + function: main + span: 51 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_load-fail.rs b/kmir/src/tests/integration/data/prove-rs/volatile_load-fail.rs new file mode 100644 index 000000000..313adec3f --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/volatile_load-fail.rs @@ -0,0 +1,12 @@ +#![feature(core_intrinsics)] +fn main() { + let a: i32 = 5555; + let a_ptr = &a as *const _; + + let b: i32; + unsafe { + b = std::intrinsics::volatile_load(a_ptr); + } + + assert!(b == 5555); +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 8c59cce9b..381bfdbc2 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -65,6 +65,8 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', + 'volatile_load-fail', + 'read_volatile-fail', ] From 02c65cc8c2ccefa423789068a4534e10e04a57ee Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sun, 15 Mar 2026 22:38:41 +1000 Subject: [PATCH 2/3] Added `volatile_load` intrinsic to semantics --- .../kmir/kdist/mir-semantics/intrinsics.md | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md index 5da5a85f2..8788d9861 100644 --- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md +++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md @@ -143,6 +143,26 @@ write the value to that location. ... ``` +#### Volatile Load (`std::intrinsics::volatile_load`, `std::ptr::read_volatile`) + +The `volatile_load` intrinsic reads a value from a memory location through a pointer, ensuring the read is not +optimised away by the compiler. Unlike normal loads, volatile loads are guaranteed to occur exactly once and +in order with respect to other volatile operations. In the semantics, this is equivalent to a regular load +through a dereferenced pointer. We extract the place from the pointer operand, add a deref projection, and +read the value from that location into the destination. Since `#setLocalValue` is strict in its second argument, +the dereferenced operand is evaluated (i.e., the value is read from memory) before being written to `DEST`. + +```k + rule #execIntrinsic(IntrinsicFunction(symbol("volatile_load")), operandCopy(place(LOCAL, PROJ)) .Operands, DEST, _SPAN) + => #setLocalValue(DEST, operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)))) + ... + + // for `operandMove` the pointer is moved, but the pointed-to value is copied (read, not consumed) + rule #execIntrinsic(IntrinsicFunction(symbol("volatile_load")), operandMove(place(LOCAL, PROJ)) .Operands, DEST, _SPAN) + => #setLocalValue(DEST, operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)))) + ... +``` + #### 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 95b74725237bcce6df3a71bf61e572d39cfe77d1 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sun, 15 Mar 2026 22:42:22 +1000 Subject: [PATCH 3/3] Changed failing tests to passing --- .../{read_volatile-fail.rs => read_volatile.rs} | 0 .../show/read_volatile-fail.main.expected | 15 --------------- .../show/volatile_load-fail.main.expected | 16 ---------------- .../{volatile_load-fail.rs => volatile_load.rs} | 0 kmir/src/tests/integration/test_integration.py | 2 -- 5 files changed, 33 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{read_volatile-fail.rs => read_volatile.rs} (100%) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/read_volatile-fail.main.expected delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/volatile_load-fail.main.expected rename kmir/src/tests/integration/data/prove-rs/{volatile_load-fail.rs => volatile_load.rs} (100%) diff --git a/kmir/src/tests/integration/data/prove-rs/read_volatile-fail.rs b/kmir/src/tests/integration/data/prove-rs/read_volatile.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/read_volatile-fail.rs rename to kmir/src/tests/integration/data/prove-rs/read_volatile.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/read_volatile-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/read_volatile-fail.main.expected deleted file mode 100644 index ff656efd9..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/read_volatile-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (60 steps) -└─ 3 (stuck, leaf) - #execIntrinsic ( IntrinsicFunction ( symbol ( "volatile_load" ) ) , operandMove - span: 55 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_load-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_load-fail.main.expected deleted file mode 100644 index 1f73a2727..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/volatile_load-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_load" ) ) , operandCopy - function: main - span: 51 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_load-fail.rs b/kmir/src/tests/integration/data/prove-rs/volatile_load.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/volatile_load-fail.rs rename to kmir/src/tests/integration/data/prove-rs/volatile_load.rs diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 381bfdbc2..8c59cce9b 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -65,8 +65,6 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', - 'volatile_load-fail', - 'read_volatile-fail', ]