From f02709afd3d52dab33b93a3f013ffaeeeb4fff06 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 16 Mar 2026 22:00:22 +1000 Subject: [PATCH 1/5] Added failing tests for `volatile_{load,store}` with statics --- .../show/volatile_load_static-fail.main.expected | 16 ++++++++++++++++ .../volatile_store_static-fail.main.expected | 16 ++++++++++++++++ .../data/prove-rs/volatile_load_static-fail.rs | 11 +++++++++++ .../data/prove-rs/volatile_store_static-fail.rs | 12 ++++++++++++ kmir/src/tests/integration/test_integration.py | 2 ++ 5 files changed, 57 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/volatile_load_static-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/volatile_store_static-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-fail.main.expected new file mode 100644 index 000000000..f792b03d2 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-fail.main.expected @@ -0,0 +1,16 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (17 steps) +└─ 3 (stuck, leaf) + #traverseProjection ( toLocal ( 3 ) , thunk ( #decodeConstant ( constantKindAllo + function: main + span: 53 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-fail.main.expected new file mode 100644 index 000000000..0c9649cc5 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-fail.main.expected @@ -0,0 +1,16 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (17 steps) +└─ 3 (stuck, leaf) + #traverseProjection ( toLocal ( 4 ) , thunk ( #decodeConstant ( constantKindAllo + function: main + span: 57 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_load_static-fail.rs b/kmir/src/tests/integration/data/prove-rs/volatile_load_static-fail.rs new file mode 100644 index 000000000..7704d6ae2 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/volatile_load_static-fail.rs @@ -0,0 +1,11 @@ +#![feature(core_intrinsics)] +static A: i32 = 5555; + +fn main() { + let val: i32; + unsafe { + val = std::intrinsics::volatile_load(&A as *const i32); + } + + assert!(val == 5555); +} diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_store_static-fail.rs b/kmir/src/tests/integration/data/prove-rs/volatile_store_static-fail.rs new file mode 100644 index 000000000..852d0a602 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/volatile_store_static-fail.rs @@ -0,0 +1,12 @@ +#![feature(core_intrinsics)] +static mut A: i32 = 5555; + +fn main() { + unsafe { + std::intrinsics::volatile_store(&mut A as *mut i32, 7777); + } + + unsafe { + assert!(A == 7777); + } +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 8c59cce9b..ae5e49dad 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_store_static-fail', + 'volatile_load_static-fail', ] From ca057a1bd621b5f2093c16c8a6c5b867d7bec6a1 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 16 Mar 2026 22:20:07 +1000 Subject: [PATCH 2/5] Added failing test for box heap allocation --- .../data/prove-rs/box_heap_alloc-fail.rs | 4 ++++ .../show/box_heap_alloc-fail.main.expected | 15 +++++++++++++++ kmir/src/tests/integration/test_integration.py | 1 + 3 files changed, 20 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/box_heap_alloc-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-fail.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/box_heap_alloc-fail.rs b/kmir/src/tests/integration/data/prove-rs/box_heap_alloc-fail.rs new file mode 100644 index 000000000..10988cbe7 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/box_heap_alloc-fail.rs @@ -0,0 +1,4 @@ +fn main() { + let a = Box::new(42i32); + assert!(*a == 42); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-fail.main.expected new file mode 100644 index 000000000..6b316872b --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-fail.main.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (199 steps) +└─ 3 (stuck, leaf) + #execIntrinsic ( IntrinsicFunction ( symbol ( "volatile_load" ) ) , operandConst + span: 32 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index ae5e49dad..c67f6275f 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -67,6 +67,7 @@ 'ref-ptr-cast-elem-offset-fail', 'volatile_store_static-fail', 'volatile_load_static-fail', + 'box_heap_alloc-fail', ] From a3b70606ab3a7b25077aea09924224aca251931a Mon Sep 17 00:00:00 2001 From: dkcumming Date: Mon, 16 Mar 2026 23:06:38 +1000 Subject: [PATCH 3/5] Added failing tests for up- and down-cast of transparent wrappers --- ...ransparent_wrapper_down-fail.main.expected | 46 +++++++++++++++++++ ..._transparent_wrapper_up-fail.main.expected | 16 +++++++ ...transmute_transparent_wrapper_down-fail.rs | 7 +++ .../transmute_transparent_wrapper_up-fail.rs | 7 +++ .../src/tests/integration/test_integration.py | 2 + 5 files changed, 78 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_down-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_up-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_down-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_up-fail.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_down-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_down-fail.main.expected new file mode 100644 index 000000000..7c76d590f --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_down-fail.main.expected @@ -0,0 +1,46 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (37 steps) +├─ 3 +│ #selectBlock ( switchTargets ( ... branches: branch ( 42 , basicBlockIdx ( 1 ) ) +│ function: main +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ #execBlockIdx ( basicBlockIdx ( 1 ) ) ~> .K +┃ │ function: main +┃ │ +┃ │ (4 steps) +┃ ├─ 7 (terminal) +┃ │ #EndProgram ~> .K +┃ │ function: main +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┣━━┓ +┃ │ +┃ ├─ 5 +┃ │ #selectBlock ( switchTargets ( ... branches: .Branches , otherwise: basicBlockId +┃ │ function: main +┃ │ +┃ │ (6 steps) +┃ └─ 8 (stuck, leaf) +┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h +┃ span: 32 +┃ +┗━━┓ + │ + └─ 6 (stuck, leaf) + #selectBlock ( switchTargets ( ... branches: branch ( 42 , basicBlockIdx ( 1 ) ) + function: main + + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_up-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_up-fail.main.expected new file mode 100644 index 000000000..f84177f7f --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_up-fail.main.expected @@ -0,0 +1,16 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (31 steps) +└─ 3 (stuck, leaf) + #traverseProjection ( toLocal ( 1 ) , thunk ( #cast ( Integer ( 42 , 64 , false + function: main + span: 50 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_down-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_down-fail.rs new file mode 100644 index 000000000..7d48657eb --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_down-fail.rs @@ -0,0 +1,7 @@ +struct Wrapper(u64); + +fn main() { + let wrapped = Wrapper(42); + let val: u64 = unsafe { core::mem::transmute::(wrapped) }; + assert!(val == 42); +} diff --git a/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_up-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_up-fail.rs new file mode 100644 index 000000000..043193722 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_up-fail.rs @@ -0,0 +1,7 @@ +struct Wrapper(u64); + +fn main() { + let val: u64 = 42; + let wrapped: Wrapper = unsafe { core::mem::transmute::(val) }; + assert!(wrapped.0 == 42); +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index c67f6275f..6aa989fdb 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -68,6 +68,8 @@ 'volatile_store_static-fail', 'volatile_load_static-fail', 'box_heap_alloc-fail', + 'transmute_transparent_wrapper_down-fail', + 'transmute_transparent_wrapper_up-fail', ] From 96f410ed7ca2ff36551728809b28b88eed41fb5b Mon Sep 17 00:00:00 2001 From: dkcumming Date: Tue, 17 Mar 2026 01:28:49 +1000 Subject: [PATCH 4/5] Added rules for transparent wrapper transmute casts --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 24 ++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index f76620160..c50f5783d 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1606,6 +1606,30 @@ The first cast is reified as a `thunk`, the second one resolves it and eliminate andBool lookupTy(TY_DEST_INNER) ==K lookupTy(TY_SRC_OUTER) // and is well-formed (invariant) ``` +Transmuting a value `T` into a single-field wrapper struct `G` (or vice versa) is sound when the struct +has its field at zero offset and `transmute` compiled (guaranteeing equal sizes). +These are essentially `#[repr(transparent)]` but are `#[repr(rust)]` by default without the annotation and +thus there are no compiler optimisations to remove the transmute (there would be otherwise for downcast). +The layout is the same for the wrapped type and so the cast in either direction is sound. + +```k + // Up: T -> Wrapper(T) + rule #cast(VAL:Value, castKindTransmute, TY_SOURCE, TY_TARGET) + => + Aggregate(variantIdx(0), ListItem(VAL)) + ... + + requires #transparentFieldTy(lookupTy(TY_TARGET)) ==K TY_SOURCE + + // Down: Wrapper(T) -> T + rule #cast(Aggregate(variantIdx(0), ListItem(VAL)), castKindTransmute, TY_SOURCE, TY_TARGET) + => + VAL + ... + + requires {#transparentFieldTy(lookupTy(TY_SOURCE))}:>Ty ==K TY_TARGET +``` + Casting a byte array/slice to an integer reinterprets the bytes in little-endian order. ```k From 2c1ec684e8a127e63451e8a934bcb7f80bdac6df Mon Sep 17 00:00:00 2001 From: dkcumming Date: Tue, 17 Mar 2026 01:33:31 +1000 Subject: [PATCH 5/5] Changed failing transmute transparent wrapper tests to passing --- ...ransparent_wrapper_down-fail.main.expected | 46 ------------------- ..._transparent_wrapper_up-fail.main.expected | 16 ------- ... => transmute_transparent_wrapper_down.rs} | 0 ...rs => transmute_transparent_wrapper_up.rs} | 0 .../src/tests/integration/test_integration.py | 2 - 5 files changed, 64 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_down-fail.main.expected delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_up-fail.main.expected rename kmir/src/tests/integration/data/prove-rs/{transmute_transparent_wrapper_down-fail.rs => transmute_transparent_wrapper_down.rs} (100%) rename kmir/src/tests/integration/data/prove-rs/{transmute_transparent_wrapper_up-fail.rs => transmute_transparent_wrapper_up.rs} (100%) diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_down-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_down-fail.main.expected deleted file mode 100644 index 7c76d590f..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_down-fail.main.expected +++ /dev/null @@ -1,46 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (37 steps) -├─ 3 -│ #selectBlock ( switchTargets ( ... branches: branch ( 42 , basicBlockIdx ( 1 ) ) -│ function: main -┃ -┃ (1 step) -┣━━┓ -┃ │ -┃ ├─ 4 -┃ │ #execBlockIdx ( basicBlockIdx ( 1 ) ) ~> .K -┃ │ function: main -┃ │ -┃ │ (4 steps) -┃ ├─ 7 (terminal) -┃ │ #EndProgram ~> .K -┃ │ function: main -┃ │ -┃ ┊ constraint: true -┃ ┊ subst: ... -┃ └─ 2 (leaf, target, terminal) -┃ #EndProgram ~> .K -┃ -┣━━┓ -┃ │ -┃ ├─ 5 -┃ │ #selectBlock ( switchTargets ( ... branches: .Branches , otherwise: basicBlockId -┃ │ function: main -┃ │ -┃ │ (6 steps) -┃ └─ 8 (stuck, leaf) -┃ #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h -┃ span: 32 -┃ -┗━━┓ - │ - └─ 6 (stuck, leaf) - #selectBlock ( switchTargets ( ... branches: branch ( 42 , basicBlockIdx ( 1 ) ) - function: main - - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_up-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_up-fail.main.expected deleted file mode 100644 index f84177f7f..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/transmute_transparent_wrapper_up-fail.main.expected +++ /dev/null @@ -1,16 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (31 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 1 ) , thunk ( #cast ( Integer ( 42 , 64 , false - function: main - span: 50 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_down-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_down.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_down-fail.rs rename to kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_down.rs diff --git a/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_up-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_up.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_up-fail.rs rename to kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_up.rs diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 6aa989fdb..c67f6275f 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -68,8 +68,6 @@ 'volatile_store_static-fail', 'volatile_load_static-fail', 'box_heap_alloc-fail', - 'transmute_transparent_wrapper_down-fail', - 'transmute_transparent_wrapper_up-fail', ]