@@ -299,18 +299,18 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
299299 | toStack ( Int , Local )
300300
301301 // retains information about the value that was deconstructed by a projection
302- syntax Context ::= CtxField( VariantIdx, List, Int )
302+ syntax Context ::= CtxField( VariantIdx, List, Int , Ty )
303303 | CtxIndex( List , Int ) // array index constant or has been read before
304304 | CtxSubslice( List , Int , Int ) // start and end always counted from beginning
305305
306306 syntax Contexts ::= List{Context, ""}
307307
308308 syntax Value ::= #buildUpdate ( Value , Contexts ) [function]
309-
309+ // ----------------------------------------------------------
310310 rule #buildUpdate(VAL, .Contexts) => VAL
311311 [preserves-definedness]
312312
313- rule #buildUpdate(VAL, CtxField(IDX, ARGS, I) CTXS)
313+ rule #buildUpdate(VAL, CtxField(IDX, ARGS, I, _ ) CTXS)
314314 => #buildUpdate(Aggregate(IDX, ARGS[I <- VAL]), CTXS)
315315 [preserves-definedness] // valid list indexing checked upon context construction
316316
@@ -387,14 +387,14 @@ This is done without consideration of the validity of the Downcast[^downcast].
387387 rule <k> #traverseProjection(
388388 DEST,
389389 Aggregate(IDX, ARGS),
390- projectionElemField(fieldIdx(I), _ ) PROJS,
390+ projectionElemField(fieldIdx(I), TY ) PROJS,
391391 CTXTS
392392 )
393393 => #traverseProjection(
394394 DEST,
395395 getValue(ARGS, I),
396396 PROJS,
397- CtxField(IDX, ARGS, I) CTXTS
397+ CtxField(IDX, ARGS, I, TY ) CTXTS
398398 )
399399 ...
400400 </k>
@@ -877,9 +877,23 @@ For slices (represented as `Value::Range`), the metadata is the length (as a dyn
877877For ` struct ` s (represented as ` Value::Aggregate ` ), the metadata is that of the _ last_ field (for dynamically-sized data).
878878Other ` Value ` s are not expected to have pointer ` Metadata ` as per their types.
879879
880+ As references are sometimes created by dereferencing other references or pointers, the referenced value is first evaluated (using ` #traverseProjection ` ).
881+ This eliminates any ` Deref ` projections from the place, and also resolves ` Index ` projections to ` ConstantIndex ` ones.
882+
880883``` k
881- rule <k> rvalueRef(_REGION, KIND, place(local(I), PROJS) #as PLACE)
882- => #mkRef(PLACE, #mutabilityOf(KIND), #metadata(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS, TYPEMAP), LOCALS)
884+ // reconstructs projections stored as context (used for Rvalues Ref and AddressOf )
885+ syntax ProjectionElems ::= #projectionsFor( Contexts ) [function, total]
886+ | #projectionsFor( Contexts , ProjectionElems ) [function, total]
887+ // ----------------------------------------------------------------------------------------
888+ rule #projectionsFor(CTXS) => #projectionsFor(CTXS, .ProjectionElems)
889+ rule #projectionsFor( .Contexts , PROJS) => PROJS
890+ rule #projectionsFor(CtxField(_, _, I, TY) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemField(fieldIdx(I), TY) PROJS)
891+ rule #projectionsFor( CtxIndex(_, I) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemConstantIndex(I, 0, false) PROJS)
892+ rule #projectionsFor( CtxSubslice(_, I, J) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemSubslice(I, J, false) PROJS)
893+
894+ rule <k> rvalueRef(_REGION, KIND, place(local(I), PROJS))
895+ => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts)
896+ ~> #forRef(#mutabilityOf(KIND), #metadata(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS, TYPEMAP))
883897 ...
884898 </k>
885899 <locals> LOCALS </locals>
@@ -888,37 +902,30 @@ Other `Value`s are not expected to have pointer `Metadata` as per their types.
888902 andBool isTypedValue(LOCALS[I])
889903 [preserves-definedness] // valid list indexing checked, #metadata should only use static information
890904
891- syntax Evaluation ::= #mkRef ( Place , Mutability, Metadata, List)
892- | #mkDynSizeRef ( Place , Mutability , List , Evaluation ) [strict(4)]
905+ syntax KItem ::= #forRef( Mutability , Metadata )
893906
894- rule <k> #mkRef( PLACE , MUT, dynamicSize(_), LOCALS) => #mkDynSizeRef(PLACE, MUT, LOCALS, operandCopy(PLACE)) ... </k>
895- rule <k> #mkRef(place(LOCAL, PROJS), MUT, META , LOCALS) => Reference(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, META) ... </k> [priority(60)]
907+ // once traversal is finished, reconstruct the last projections and the reference offset/local, and possibly read the size
908+ rule <k> #traverseProjection(DEST, VAL:Value, .ProjectionElems, CTXTS) ~> #forRef(MUT, META)
909+ => #mkRef(DEST, #projectionsFor(CTXTS), MUT, #maybeDynamicSize(META, VAL))
910+ ...
911+ </k>
896912
897- // with dynamic metadata (reading the value)
898- rule <k> #mkDynSizeRef(place(LOCAL, PROJS), MUT, LOCALS, VAL:Value) => Reference(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, metadataFor(VAL)) ... </k>
913+ syntax Evaluation ::= #mkRef( WriteTo , ProjectionElems , Mutability , Metadata ) // [function, total]
914+ // -----------------------------------------------------------------------------------------------
915+ rule <k> #mkRef( toLocal(I) , PROJS, MUT, META) => Reference( 0 , place(local(I), PROJS), MUT, META) ... </k>
916+ rule <k> #mkRef(toStack(OFFSET, LOCAL), PROJS, MUT, META) => Reference(OFFSET, place( LOCAL , PROJS), MUT, META) ... </k>
899917
900- syntax Metadata ::= metadataFor ( Value ) [function, total]
901- // --------------------------------------------------------
902- rule metadataFor( Range(LIST) ) => dynamicSize(size(LIST))
903- rule metadataFor( _OTHER ) => noMetadata [owise]
918+ syntax Metadata ::= #maybeDynamicSize ( Metadata , Value ) [function, total]
919+ // -------------------------------------------------------------------------
920+ rule #maybeDynamicSize(dynamicSize(_), Range(LIST)) => dynamicSize(size(LIST))
921+ rule #maybeDynamicSize(dynamicSize(_), _OTHER ) => noMetadata [priority(100)]
922+ rule #maybeDynamicSize( OTHER_META , _ ) => OTHER_META [owise]
904923
905924 syntax Mutability ::= #mutabilityOf ( BorrowKind ) [function, total]
906925 // -----------------------------------------------------------------
907926 rule #mutabilityOf(borrowKindShared) => mutabilityNot
908927 rule #mutabilityOf(borrowKindFake(_)) => mutabilityNot // Shallow fake borrow disallowed in late stages
909928 rule #mutabilityOf(borrowKindMut(_)) => mutabilityMut // all mutable kinds behave equally for us
910-
911- // turns Index(LOCAL) projections into ConstantIndex(Int)
912- syntax ProjectionElems ::= #resolveProjs ( ProjectionElems , List ) [function, total]
913- // ----------------------------------------------------------------------------------
914- rule #resolveProjs( .ProjectionElems , _LOCALS) => .ProjectionElems
915- rule #resolveProjs( projectionElemIndex(local(I)) REST, LOCALS ) => projectionElemConstantIndex(#expectUsize(getValue(LOCALS,I)), 0, false) #resolveProjs(REST, LOCALS)
916- requires 0 <=Int I
917- andBool I <Int size(LOCALS)
918- andBool isTypedValue(LOCALS[I])
919- andBool isInt(#expectUsize(getValue(LOCALS,I)))
920- [preserves-definedness]
921- rule #resolveProjs( OTHER:ProjectionElem REST, LOCALS ) => OTHER #resolveProjs(REST, LOCALS) [owise]
922929```
923930
924931A ` CopyForDeref ` ` RValue ` has the semantics of a simple ` Use(operandCopy(...)) ` ,
@@ -935,9 +942,12 @@ to casts and pointer arithmetic using `BinOp::Offset`.
935942The operation typically creates a pointer with empty metadata.
936943
937944``` k
938- rule <k> rvalueAddressOf(MUT, place(local(I), PROJS) #as PLACE)
945+ syntax KItem ::= #forPtr ( Mutability, Metadata )
946+
947+ rule <k> rvalueAddressOf(MUT, place(local(I), PROJS))
939948 =>
940- #mkPtr(PLACE, MUT, #metadata(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS, TYPEMAP), LOCALS)
949+ #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts)
950+ ~> #forPtr(MUT, #metadata(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS, TYPEMAP))
941951 // we should use #alignOf to emulate the address
942952 ...
943953 </k>
@@ -947,23 +957,16 @@ The operation typically creates a pointer with empty metadata.
947957 andBool isTypedValue(LOCALS[I])
948958 [preserves-definedness] // valid list indexing checked, #metadata should only use static information
949959
950- syntax Evaluation ::= #mkPtr ( Place , Mutability , Metadata , List )
951- | #mkDynLengthPtr ( Place , Mutability , List , Evaluation ) [strict(4)]
952-
953- rule <k> #mkPtr( PLACE , MUT, dynamicSize(_), LOCALS)
954- => #mkDynLengthPtr(PLACE, MUT, LOCALS, operandCopy(PLACE))
960+ // once traversal is finished, reconstruct the last projections and the reference offset/local, and possibly read the size
961+ rule <k> #traverseProjection(DEST, VAL:Value, .ProjectionElems, CTXTS) ~> #forPtr(MUT, META)
962+ => #mkPtr(DEST, #projectionsFor(CTXTS), MUT, #maybeDynamicSize(META, VAL))
955963 ...
956- </k>
964+ </k>
957965
958- rule <k> #mkPtr(place(LOCAL, PROJS), MUT, META , LOCALS)
959- => PtrLocal(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, ptrEmulation(META))
960- ...
961- </k> [priority(60)]
962-
963- rule <k> #mkDynLengthPtr(place(LOCAL, PROJS), MUT, LOCALS, Range(ELEMS))
964- => PtrLocal(0, place(LOCAL, #resolveProjs(PROJS, LOCALS)), MUT, ptrEmulation(dynamicSize(size(ELEMS))))
965- ...
966- </k>
966+ syntax Evaluation ::= #mkPtr ( WriteTo, ProjectionElems, Mutability , Metadata ) // [function, total]
967+ // ------------------------------------------------------------------------------------------
968+ rule <k> #mkPtr( toLocal(I) , PROJS, MUT, META) => PtrLocal( 0 , place(local(I), PROJS), MUT, ptrEmulation(META)) ... </k>
969+ rule <k> #mkPtr(toStack(OFFSET, LOCAL), PROJS, MUT, META) => PtrLocal(OFFSET, place( LOCAL , PROJS), MUT, ptrEmulation(META)) ... </k>
967970```
968971
969972In practice, the ` AddressOf ` can often be found applied to references that get dereferenced first,
0 commit comments