Skip to content

Commit 297ef2c

Browse files
committed
add fix-up rule to apply field projection on array head element when array found
1 parent f8f55a5 commit 297ef2c

File tree

1 file changed

+15
-0
lines changed
  • kmir/src/kmir/kdist/mir-semantics/rt

1 file changed

+15
-0
lines changed

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -469,6 +469,21 @@ The context is populated with the correct field access data, so that write-backs
469469
[preserves-definedness, priority(100)]
470470
```
471471

472+
A somewhat dual case to this rule can occur when a pointer into an array of data elements has been offset and is then dereferenced.
473+
The dereferenced pointer may either point to a subslice or to a single element (depending on context).
474+
Therefore, a field projection may be found which has to be applied to the head element of an array.
475+
The following rule resolves this situation by using the head element.
476+
477+
```k
478+
rule <k> #traverseProjection(
479+
DEST,
480+
Range(ListItem(Aggregate(_, _) #as VALUE) _REST:List),
481+
projectionElemField(IDX, TY) PROJS,
482+
CTXTS
483+
)
484+
=> #traverseProjection(DEST, VALUE, projectionElemField(IDX, TY) PROJS, CTXTS) ... </k> // TODO mark context?
485+
[preserves-definedness, priority(100)]
486+
```
472487

473488
#### Unions
474489
```k

0 commit comments

Comments
 (0)