fix(spl): adjustRef for SPL Token domain data #870
Conversation
Stevengre
force-pushed
the
jh/spl/fix-traverse
branch
from
b2185e1 to
e7fba82
Compare
| | #finishResolvedSPLRc ( Place , MaybeBasicBlockIdx ) | ||
| | #resolveSPLRcRef ( Value , Place , MaybeBasicBlockIdx ) | ||
| | #finishResolvedSPLRc ( Place , MaybeBasicBlockIdx ) | ||
| | #writeThroughRef ( Value , Value ) [seqstrict(2)] |
There was a problem hiding this comment.
For the seqstrict to make sense, the 2nd argument has to be an Evaluation not a Value (the Value is already a KResult so there is nothing to evaluate further).
There was a problem hiding this comment.
Deleted the seqstrict. It's always Value when used.
| // Cross-frame write helper for SPL ref cells | ||
| rule <k> #writeThroughRef(Reference(0, place(local(I), PROJS), _, _), VAL) | ||
| => #forceSetPlaceValue(place(local(I), PROJS), VAL) | ||
| ... | ||
| </k> | ||
| <locals> LOCALS </locals> | ||
| requires 0 <=Int I andBool I <Int size(LOCALS) | ||
| andBool isTypedLocal(LOCALS[I]) | ||
| rule <k> #writeThroughRef(Reference(OFFSET, place(local(I), PROJS), _, _), VAL) | ||
| => #traverseProjection( | ||
| toStack(OFFSET, local(I)), | ||
| #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(I), OFFSET), | ||
| PROJS, | ||
| .Contexts | ||
| ) | ||
| ~> #writeProjection(VAL) | ||
| ... | ||
| </k> | ||
| <stack> STACK </stack> | ||
| requires 0 <Int OFFSET | ||
| andBool OFFSET <=Int size(STACK) | ||
| andBool isStackFrame(STACK[OFFSET -Int 1]) | ||
| andBool 0 <=Int I |
There was a problem hiding this comment.
The #writeThroughRef only operates on Reference values. It seems the WriteTo helper sort from data.md could be used instead of the first Value argument.
Many symbol arguments have changed sort from Place to Value, was this the reason?
There was a problem hiding this comment.
I want to support borrow mut in a callee function with different height.
| // Adjust references when moving across stack frames | ||
| rule #adjustRef(SPLRefCell(PLACE, VAL), OFFSET) => SPLRefCell(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) | ||
| rule #adjustRef(SPLDataBorrow(PLACE, VAL), OFFSET) => SPLDataBorrow(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) | ||
| rule #adjustRef(SPLDataBorrowMut(PLACE, VAL), OFFSET) => SPLDataBorrowMut(#adjustRef(PLACE, OFFSET), #adjustRef(VAL, OFFSET)) | ||
| rule #adjustRef(SPLDataBuffer(VAL), OFFSET) => SPLDataBuffer(#adjustRef(VAL, OFFSET)) | ||
| rule #adjustRef(SPLPubkeyRef(VAL), OFFSET) => SPLPubkeyRef(#adjustRef(VAL, OFFSET)) |
There was a problem hiding this comment.
The PLACE variables have changed sort to Value so they should probably not be called PLACE any more.
Could we implement #adjustRef for SPL* values directly instead of recurring to a Value? The Place will probably always have a known shape, but I don't know if double references (Deref in the projection) can be excluded. Maybe the Place should become a WrteTo?
There was a problem hiding this comment.
Could we implement #adjustRef for SPL* values directly instead of recurring to a Value?
Done!
Maybe the Place should become a WrteTo?
WriteTo cannot hold the projections.
The Place will probably always have a known shape, but I don't know if double references (Deref in the projection) can be excluded.
I don't quite understand this.
Stevengre
force-pushed
the
jh/spl/fix-traverse
branch
from
0a522e7 to
51eb312
Compare
#traverseProjectionwith#adjustRefsolana-token#115