Skip to content

Commit eafe909

Browse files
Stevengredkcummingclaude
authored
fix(types): make #pointeeProjection confluent with source-first unwrapping strategy (#988)
## Summary - Fixes stuck execution caused by incorrect projection chains from `#pointeeProjection` - Root cause: non-deterministic overlap between struct and array rules — when source is a struct and target is an array (or vice versa), both rules match and the LLVM backend's choice determines correctness - Commit history shows why `[priority(45)]` alone doesn't work (it fixes one case but regresses the other) - Fix: always unwrap the source type first; target-side unwrapping deferred to `#pointeeProjectionTarget` - Reproducer from @dkcumming's review comment (minimal `Wrapper([u8; 2])` cast) ## Test plan - [x] `ptr-cast-wrapper-to-array` passes (new reproducer) - [x] `iter_next_2` still passes (regression test for opposite overlap: `[Thing;3] → Thing`) - [x] Full integration test suite passes --------- Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 92056cd commit eafe909

11 files changed

Lines changed: 223 additions & 21 deletions

‎kmir/src/kmir/kdist/mir-semantics/rt/types.md‎

Lines changed: 49 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -76,29 +76,18 @@ It also implements cancellation of inverse projections (such as casting from one
7676

7777
The `#pointeeProjection` function computes, for compatible pointee types, how to project from one pointee to the other.
7878

79+
It uses a **source-first strategy**: always unwrap the source type (struct wrapper or array) before
80+
attempting to unwrap the target type. This eliminates non-deterministic overlap between source-side
81+
and target-side rules, because a type cannot be both a struct and an array simultaneously.
82+
When the source cannot be unwrapped further, target-side unwrapping is handled by `#pointeeProjectionTarget`.
83+
7984
```k
8085
syntax MaybeProjectionElems ::= #pointeeProjection ( TypeInfo , TypeInfo ) [function, total]
8186
```
8287

8388
A short-cut rule for identical types takes preference.
84-
As a default, no projection elements are returned for incompatible types.
8589
```k
8690
rule #pointeeProjection(T , T) => .ProjectionElems [priority(40)]
87-
rule #pointeeProjection(_ , _) => NoProjectionElems [owise]
88-
```
89-
90-
Pointers to arrays/slices are compatible with pointers to the element type
91-
```k
92-
rule #pointeeProjection(typeInfoArrayType(TY1, _), TY2)
93-
=> maybeConcatProj(
94-
projectionElemConstantIndex(0, 0, false),
95-
#pointeeProjection(lookupTy(TY1), TY2)
96-
)
97-
rule #pointeeProjection(TY1, typeInfoArrayType(TY2, _))
98-
=> maybeConcatProj(
99-
projectionElemSingletonArray,
100-
#pointeeProjection(TY1, lookupTy(TY2))
101-
)
10291
```
10392

10493
Pointers to zero-sized types can be converted from and to. No recursion beyond the ZST.
@@ -112,22 +101,33 @@ Pointers to zero-sized types can be converted from and to. No recursion beyond t
112101
[priority(45)]
113102
```
114103

115-
Pointers to structs with a single zero-offset field are compatible with pointers to that field's type
116-
```k
104+
Source-side: unwrap structs and arrays from the source type first.
117105

106+
When source is an array and target is a transparent wrapper whose inner type equals the source,
107+
the source should be wrapped rather than unwrapped (e.g., `*const [u8;2] → *const Wrapper([u8;2])`).
108+
```k
118109
rule #pointeeProjection(typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER)
119110
=> maybeConcatProj(
120111
projectionElemField(fieldIdx(0), FIELD),
121112
#pointeeProjection(lookupTy(FIELD), OTHER)
122113
)
123114
requires #zeroFieldOffset(LAYOUT)
124115
125-
rule #pointeeProjection(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
116+
rule #pointeeProjection(SRC:TypeInfo, typeInfoStructType(_NAME, _ADTDEF, FIELD .Tys, LAYOUT))
126117
=> maybeConcatProj(
127118
projectionElemWrapStruct,
128-
#pointeeProjection(OTHER, lookupTy(FIELD))
119+
#pointeeProjection(SRC, lookupTy(FIELD))
120+
)
121+
requires #isArrayType(SRC)
122+
andBool #zeroFieldOffset(LAYOUT)
123+
andBool lookupTy(FIELD) ==K SRC
124+
[priority(42)]
125+
126+
rule #pointeeProjection(typeInfoArrayType(TY1, _), TY2)
127+
=> maybeConcatProj(
128+
projectionElemConstantIndex(0, 0, false),
129+
#pointeeProjection(lookupTy(TY1), TY2)
129130
)
130-
requires #zeroFieldOffset(LAYOUT)
131131
```
132132

133133
Pointers to `MaybeUninit<X>` can be cast to pointers to `X`.
@@ -148,6 +148,34 @@ which is a singleton struct (see above).
148148
andBool #lookupMaybeTy(getFieldTy(#lookupMaybeTy(getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)) ==K ELEM_TYINFO
149149
```
150150

151+
Fallback: source is not unwrappable, delegate to target-side.
152+
```k
153+
rule #pointeeProjection(SRC, TGT) => #pointeeProjectionTarget(SRC, TGT) [owise]
154+
```
155+
156+
Target-side fallback: only reached when source cannot be unwrapped further.
157+
After one step of target unwrapping, recurse back to `#pointeeProjection` to maintain
158+
the source-first strategy.
159+
160+
```k
161+
syntax MaybeProjectionElems ::= #pointeeProjectionTarget ( TypeInfo , TypeInfo ) [function, total]
162+
163+
rule #pointeeProjectionTarget(TY1, typeInfoArrayType(TY2, _))
164+
=> maybeConcatProj(
165+
projectionElemSingletonArray,
166+
#pointeeProjection(TY1, lookupTy(TY2))
167+
)
168+
169+
rule #pointeeProjectionTarget(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
170+
=> maybeConcatProj(
171+
projectionElemWrapStruct,
172+
#pointeeProjection(OTHER, lookupTy(FIELD))
173+
)
174+
requires #zeroFieldOffset(LAYOUT)
175+
176+
rule #pointeeProjectionTarget(_, _) => NoProjectionElems [owise]
177+
```
178+
151179
```k
152180
syntax Bool ::= #zeroFieldOffset ( MaybeLayoutShape ) [function, total]
153181
// --------------------------------------------------------------------

‎kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-fail.rs‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// [T; N] -> W2(W1([T; N])) - nested struct wrapping on target
2+
#[derive(Clone, Copy, PartialEq, Debug)]
3+
struct Inner([u8; 2]);
4+
5+
#[derive(Clone, Copy, PartialEq, Debug)]
6+
struct Outer(Inner);
7+
8+
fn main() {
9+
let arr: [u8; 2] = [11, 22];
10+
let o: Outer = unsafe { *((&arr) as *const [u8; 2] as *const Outer) };
11+
assert_eq!(o.0 .0, [11, 22]);
12+
}

‎kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-fail.rs‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// [T; N] -> W([[T; N]; 1]) - singleton-array wrapping array (in-wrapper) on target
2+
#[derive(Clone, Copy, PartialEq, Debug)]
3+
struct Wrapper([[u8; 2]; 1]);
4+
5+
fn main() {
6+
let arr: [u8; 2] = [11, 22];
7+
let w: Wrapper = unsafe { *((&arr) as *const [u8; 2] as *const Wrapper) };
8+
assert_eq!(w.0, [[11, 22]]);
9+
}

‎kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-fail.rs‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
#[derive(Clone, Copy, PartialEq, Debug)]
2+
struct Wrapper([u8; 2]);
3+
4+
fn main() {
5+
let arr: [u8; 2] = [11, 22];
6+
let w: Wrapper = unsafe { *((&arr) as *const [u8; 2] as *const Wrapper) };
7+
assert_eq!(w.0, [11, 22]);
8+
}

‎kmir/src/tests/integration/data/prove-rs/ptr-cast-nested-wrapper-to-array.rs‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// W2(W1([T; N])) -> [T; N] - nested struct wrapping on source
2+
struct Inner([u8; 2]);
3+
struct Outer(Inner);
4+
5+
fn main() {
6+
let o = Outer(Inner([11, 22]));
7+
let arr: [u8; 2] = unsafe { *((&o) as *const Outer as *const [u8; 2]) };
8+
assert_eq!(arr, [11, 22]);
9+
}

‎kmir/src/tests/integration/data/prove-rs/ptr-cast-singleton-wrapped-array-to-array.rs‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
// W([[T; N]; 1]) -> [T; N] - singleton-array wrapping array (in-wrapper) on source
2+
struct Wrapper([[u8; 2]; 1]);
3+
4+
fn main() {
5+
let w = Wrapper([[11, 22]]);
6+
let arr: [u8; 2] = unsafe { *((&w) as *const Wrapper as *const [u8; 2]) };
7+
assert_eq!(arr, [11, 22]);
8+
}

‎kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array.rs‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
struct Wrapper([u8; 2]);
2+
3+
fn main() {
4+
let w = Wrapper([11, 22]);
5+
let arr: [u8; 2] = unsafe { *((&w) as *const Wrapper as *const [u8; 2]) };
6+
assert_eq!(arr, [11, 22]);
7+
}

‎kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-fail.main.expected‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (128 steps)
7+
├─ 3
8+
│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
9+
│ function: main
10+
┃
11+
┃ (1 step)
12+
┣━━┓
13+
┃ │
14+
┃ ├─ 4
15+
┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
16+
┃ │ function: main
17+
┃ │
18+
┃ │ (1 step)
19+
┃ └─ 6 (stuck, leaf)
20+
┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
21+
┃ function: main
22+
┃
23+
┗━━┓
24+
│
25+
├─ 5
26+
│ #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
27+
│ function: main
28+
│
29+
│ (11 steps)
30+
└─ 7 (stuck, leaf)
31+
#traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
32+
function: main
33+
span: 282
34+
35+
36+
┌─ 2 (root, leaf, target, terminal)
37+
│ #EndProgram ~> .K
38+
39+

‎kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-fail.main.expected‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (128 steps)
7+
├─ 3
8+
│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
9+
│ function: main
10+
┃
11+
┃ (1 step)
12+
┣━━┓
13+
┃ │
14+
┃ ├─ 4
15+
┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
16+
┃ │ function: main
17+
┃ │
18+
┃ │ (1 step)
19+
┃ └─ 6 (stuck, leaf)
20+
┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
21+
┃ function: main
22+
┃
23+
┗━━┓
24+
│
25+
├─ 5
26+
│ #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
27+
│ function: main
28+
│
29+
│ (10 steps)
30+
└─ 7 (stuck, leaf)
31+
#traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
32+
function: main
33+
span: 282
34+
35+
36+
┌─ 2 (root, leaf, target, terminal)
37+
│ #EndProgram ~> .K
38+
39+

‎kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: 0
5+
│
6+
│ (128 steps)
7+
├─ 3
8+
│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
9+
│ function: main
10+
┃
11+
┃ (1 step)
12+
┣━━┓
13+
┃ │
14+
┃ ├─ 4
15+
┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
16+
┃ │ function: main
17+
┃ │
18+
┃ │ (1 step)
19+
┃ └─ 6 (stuck, leaf)
20+
┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
21+
┃ function: main
22+
┃
23+
┗━━┓
24+
│
25+
├─ 5
26+
│ #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
27+
│ function: main
28+
│
29+
│ (154 steps)
30+
├─ 7 (terminal)
31+
│ #EndProgram ~> .K
32+
│ function: main
33+
│
34+
┊ constraint: true
35+
┊ subst: ...
36+
└─ 2 (leaf, target, terminal)
37+
#EndProgram ~> .K
38+
39+
40+

0 commit comments

Comments
 (0)