Skip to content

Commit 4da0440

Browse files
authored
Special fix-up rule to apply field projection on array head elements (#876)
When using pointer offsets followed by dereferencing, the returned result is an array (subslice of the original). In some cases, the value is used as a single element, for instance by projecting out a field. This PR adds a special rule for the field projection case to proceed using the head element in those cases. Related: #771
1 parent f8f55a5 commit 4da0440

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)