Skip to content

Commit 60b5e5a

Browse files
committed
Remove consP HACK rule and removeIndexTail from RawPtr aggregate
The consP rule that merged ConstantIndex with PointerOffset was a workaround for a deeper issue: removeIndexTail in #mkAggregate(aggregateKindRawPtr) strips the element-extraction CI(0) when constructing fat pointers from thin pointers, but #typeProjection later adds per-element navigation projections (Field for MaybeUninit→ManuallyDrop→T) that assume the element has already been extracted. Removing removeIndexTail preserves the CI(0) through the fat pointer construction, allowing the subsequent #typeProjection projections to correctly navigate into individual array elements. The consP HACK rule is also removed as it is no longer needed and was conceptually unsound (merging projections from different semantic levels). The iterator-simple test now reaches a different stuck state: PointerOffset(1,0) applied to a scalar Integer after successful element navigation, which is closer to the real remaining issue (projection ordering between CI and PointerOffset). See #1011.
1 parent 79bd202 commit 60b5e5a

2 files changed

Lines changed: 3 additions & 6 deletions

File tree

kmir/src/kmir/kdist/mir-semantics/rt/data.md

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -384,9 +384,6 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
384384
rule consP(projectionElemWrapStruct, projectionElemField(fieldIdx(0), _) PS:ProjectionElems) => PS [priority(40)]
385385
// this rule is not valid if the original pointee has more than one field
386386
// rule consP(projectionElemField(fieldIdx(0), _), projectionElemWrapStruct PS:ProjectionElems) => PS [priority(40)]
387-
// HACK: special rule which munges together constant-indexing and offset projections
388-
rule consP( projectionElemConstantIndex(I, 0, false), PointerOffset(OFF, _SIZE) PS) => projectionElemConstantIndex(I +Int OFF, 0, false) PS [priority(40)]
389-
// requires I +Int OFF < _SIZE // _SIZE is metadataSize, needs a < operation for this to work
390387
rule consP(projectionElemToZST, projectionElemFromZST PS:ProjectionElems) => PS [priority(40)]
391388
rule consP(projectionElemFromZST, projectionElemToZST PS:ProjectionElems) => PS [priority(40)]
392389
@@ -1113,7 +1110,7 @@ and an array of the indeicated size gets reconstructed if the provided metadata
11131110
rule <k> ListItem(PtrLocal(OFFSET, place(LOCAL, PROJS), _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE)))
11141111
ListItem(Integer(LENGTH, 64, false))
11151112
~> #mkAggregate(aggregateKindRawPtr(_TY, MUT))
1116-
=> PtrLocal(OFFSET, place(LOCAL, removeIndexTail(PROJS)), MUT, metadata(dynamicSize(LENGTH), PTR_OFFSET, ORIGIN_SIZE))
1113+
=> PtrLocal(OFFSET, place(LOCAL, PROJS), MUT, metadata(dynamicSize(LENGTH), PTR_OFFSET, ORIGIN_SIZE))
11171114
...
11181115
</k>
11191116
// requires LENGTH +Int PTR_OFFSET <=Int ORIGIN_SIZE // refuse to create an invalid fat pointer

kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
44
│ span: 0
55
6-
│ (1066 steps)
6+
│ (1069 steps)
77
└─ 3 (stuck, leaf)
8-
#traverseProjection ( toStack ( 3 , local ( 3 ) ) , Range ( ListItem ( Union ( f
8+
#traverseProjection ( toStack ( 3 , local ( 3 ) ) , Integer ( 1 , 32 , true ) ,
99
span: 106
1010

1111

0 commit comments

Comments
 (0)