Skip to content

Commit d6c0b7f

Browse files
committed
feat: support reverse transparent struct cast
1 parent fd09e81 commit d6c0b7f

File tree

1 file changed

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

1 file changed

+33
-0
lines changed

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

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1268,6 +1268,7 @@ which have the same representation `Value::Range`.
12681268
[preserves-definedness] // valid map lookups checked
12691269
12701270
syntax Place ::= #alignTransparentPlace ( Place , TypeInfo , TypeInfo ) [function, total]
1271+
syntax ProjectionElems ::= #popTransparentTailTo ( ProjectionElems , TypeInfo ) [function, total]
12711272
12721273
rule #alignTransparentPlace(place(LOCAL, PROJS), typeInfoStructType(_, _, FIELD_TY .Tys, LAYOUT) #as SOURCE, TARGET)
12731274
=> #alignTransparentPlace(
@@ -1281,8 +1282,38 @@ which have the same representation `Value::Range`.
12811282
requires #transparentDepth(SOURCE) >Int #transparentDepth(TARGET)
12821283
andBool #zeroFieldOffset(LAYOUT)
12831284
1285+
rule #alignTransparentPlace(
1286+
place(LOCAL, PROJS),
1287+
SOURCE,
1288+
typeInfoStructType(_, _, FIELD_TY .Tys, LAYOUT) #as TARGET
1289+
)
1290+
=> #alignTransparentPlace(
1291+
place(LOCAL, #popTransparentTailTo(PROJS, lookupTy(FIELD_TY))),
1292+
SOURCE,
1293+
lookupTy(FIELD_TY)
1294+
)
1295+
requires #transparentDepth(SOURCE) <Int #transparentDepth(TARGET)
1296+
andBool #zeroFieldOffset(LAYOUT)
1297+
andBool PROJS =/=K #popTransparentTailTo(PROJS, lookupTy(FIELD_TY))
1298+
12841299
rule #alignTransparentPlace(PLACE, _, _) => PLACE [owise]
12851300
1301+
rule #popTransparentTailTo(
1302+
projectionElemField(fieldIdx(0), FIELD_TY) .ProjectionElems,
1303+
TARGET
1304+
)
1305+
=> .ProjectionElems
1306+
requires lookupTy(FIELD_TY) ==K TARGET
1307+
1308+
rule #popTransparentTailTo(
1309+
X:ProjectionElem REST:ProjectionElems,
1310+
TARGET
1311+
)
1312+
=> X #popTransparentTailTo(REST, TARGET)
1313+
requires REST =/=K .ProjectionElems
1314+
1315+
rule #popTransparentTailTo(PROJS, _) => PROJS [owise]
1316+
12861317
syntax Metadata ::= #convertMetadata ( Metadata , TypeInfo ) [function, total]
12871318
// -------------------------------------------------------------------------------------
12881319
```
@@ -1401,6 +1432,8 @@ What can be supported without additional layout consideration is trivial casts b
14011432
rule <k> #cast(PtrLocal(_, _, _, _) #as PTR, castKindTransmute, TY_SOURCE, TY_TARGET) => PTR ... </k>
14021433
requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET)
14031434
1435+
// Transmuting a pointer to an integer discards provenance and
1436+
// reinterprets the pointer’s offset as a value of the target integer type.
14041437
rule <k> #cast(
14051438
PtrLocal(_, _, _, metadata(_, PTR_OFFSET, _)),
14061439
castKindTransmute,

0 commit comments

Comments
 (0)