Skip to content

Commit 11d13ed

Browse files
StevengreStevengre
committed
feat: pass borrow
1 parent 61b6c6b commit 11d13ed

File tree

1 file changed

+105
-77
lines changed

1 file changed

+105
-77
lines changed

‎kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md‎

Lines changed: 105 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ module KMIR-SPL-TOKEN
3737
Aggregate(variantIdx(0),
3838
ListItem(Range(?SplAccountKey:List)) // pub key: &'a Pubkey
3939
ListItem(SPLRc(SPLRefCell(Integer(?SplLamports:Int, 64, false)))) // lamports: Rc<RefCell<&'a mut u64>>
40-
ListItem(Aggregate(variantIdx(0), ListItem( Aggregate(variantIdx(0), ListItem( // data: Rc<RefCell<&'a mut [u8]>>
40+
ListItem( // data: Rc<RefCell<&'a mut [u8]>>
4141
SPLRc(SPLRefCell(SPLDataBuffer( // data: Rc<RefCell<&'a mut [u8]>>, Aggregate is for &account.data
4242
Aggregate(variantIdx(0),
4343
ListItem(Range(?SplMintKey:List)) // Account.mint: Pubkey
@@ -49,7 +49,7 @@ module KMIR-SPL-TOKEN
4949
ListItem(Integer(?SplDelegatedAmount:Int, 64, false)) // Account.delegated_amount: u64
5050
ListItem(?SplCloseAuthCOpt:Value) // Account.close_authority: COption<Pubkey>
5151
)
52-
))))))))
52+
))))
5353
ListItem(Range(?SplOwnerKey)) // owner: &'a Pubkey
5454
ListItem(Integer(?SplRentEpoch:Int, 64, false)) // rent_epoch: u64
5555
ListItem(BoolVal(?_SplIsSigner:Bool)) // is_signer: bool
@@ -97,45 +97,33 @@ module KMIR-SPL-TOKEN
9797

9898
## Accessing `Rc<RefCell<_>>`
9999

100-
101-
```k
102-
rule <k> #cast(SPLRc(VALUE), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
103-
=> SPLRc(VALUE) ...
104-
</k>
105-
requires #typesCompatible(lookupTy(TY_SOURCE), lookupTy(TY_TARGET))
106-
[preserves-definedness] // valid map lookups checked
107-
```
108-
109100
We shortcut the MIR field access that `<Rc<_> as Deref>::deref` performs and
110101
expose the wrapped payload directly.
111102

112103
```k
113-
rule <k> #traverseProjection(
114-
DEST,
115-
SPLRc(VALUE),
116-
projectionElemDeref PROJS,
117-
CTXTS
118-
)
119-
=> #traverseProjection(
120-
DEST,
121-
VALUE,
122-
PROJS,
123-
CtxSPLRc CTXTS
124-
)
125-
...
126-
</k>
127-
[priority(30)]
104+
// rule <k> #traverseProjection(
105+
// DEST,
106+
// SPLRc(VALUE),
107+
// projectionElemDeref PROJS,
108+
// CTXTS
109+
// )
110+
// => #traverseProjection(
111+
// DEST,
112+
// VALUE,
113+
// PROJS,
114+
// CtxSPLRc CTXTS
115+
// )
116+
// ...
117+
// </k>
118+
// [priority(30)]
128119
129-
syntax Context ::= "CtxSPLRc"
120+
// syntax Context ::= "CtxSPLRc"
130121
131-
rule #buildUpdate(VAL, CtxSPLRc CTXS) => #buildUpdate(SPLRc(VAL), CTXS)
132-
rule #projectionsFor(CtxSPLRc CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS)
122+
// rule #buildUpdate(VAL, CtxSPLRc CTXS) => #buildUpdate(SPLRc(VAL), CTXS)
123+
// rule #projectionsFor(CtxSPLRc CTXS, PROJS) => #projectionsFor(CTXS, projectionElemDeref PROJS)
133124
134125
rule [spl-rc-deref]:
135-
<k> #execTerminator(
136-
terminator(
137-
terminatorKindCall(FUNC, OP:Operand OPS:Operands, DEST, TARGET, UNWIND),
138-
_SPAN))
126+
<k> #execTerminator(terminator(terminatorKindCall(FUNC, OP:Operand OPS:Operands, DEST, TARGET, UNWIND), _SPAN))
139127
=> #finishSPLRcDeref(OP, DEST, TARGET, FUNC, OP OPS, UNWIND)
140128
...
141129
</k>
@@ -144,51 +132,91 @@ expose the wrapped payload directly.
144132
[priority(30), preserves-definedness]
145133
146134
syntax KItem ::= #finishSPLRcDeref ( Evaluation , Place , MaybeBasicBlockIdx , Operand , Operands , UnwindAction ) [seqstrict(1)]
135+
| #resolveSPLRcRef ( Value , Place , MaybeBasicBlockIdx , Operand , Operands , UnwindAction )
136+
| #finishResolvedSPLRc ( Place , MaybeBasicBlockIdx , Operand , Operands , UnwindAction )
147137
148-
// rule <k> #finishSPLRcDeref(SPLRc(VALUE), DEST, TARGET, _FUNC, _ARGS, _UNWIND)
149-
// => #setLocalValue(DEST, VALUE) ~> #continueAt(TARGET)
150-
// ...
151-
// </k>
152-
153-
// rule [spl-rc-deref-fallback]:
154-
// <k> #finishSPLRcDeref(_VAL:Value, DEST, TARGET, FUNC, ARGS, UNWIND)
155-
// => #setUpCalleeData(lookupFunction(#tyOfCall(FUNC)), ARGS)
156-
// ...
157-
// </k>
158-
// <currentFunc> CALLER => #tyOfCall(FUNC) </currentFunc>
159-
// <currentFrame>
160-
// <currentBody> _ </currentBody>
161-
// <caller> OLDCALLER => CALLER </caller>
162-
// <dest> OLDDEST => DEST </dest>
163-
// <target> OLDTARGET => TARGET </target>
164-
// <unwind> OLDUNWIND => UNWIND </unwind>
165-
// <locals> LOCALS </locals>
166-
// </currentFrame>
167-
// <stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
168-
// [owise]
169-
```
138+
rule <k> #finishSPLRcDeref(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET, FUNC, ARGS, UNWIND)
139+
=> #resolveSPLRcRef(Reference(OFFSET, PLACE, MUT, META), DEST, TARGET, FUNC, ARGS, UNWIND)
140+
...
141+
</k>
170142
171-
```k
172-
rule <k> #traverseProjection(
173-
DEST,
174-
SPLRefCell(VALUE),
175-
projectionElemField(fieldIdx(2), TY) PROJS,
176-
CTXTS
143+
rule <k> #resolveSPLRcRef(Reference(0, place(local(I), PROJS), _, _), DEST, TARGET, FUNC, ARGS, UNWIND)
144+
=> #traverseProjection(
145+
toLocal(I),
146+
getValue(LOCALS, I),
147+
PROJS,
148+
.Contexts
177149
)
150+
~> #readProjection(false)
151+
~> #finishResolvedSPLRc(DEST, TARGET, FUNC, ARGS, UNWIND)
152+
...
153+
</k>
154+
<locals> LOCALS </locals>
155+
requires 0 <=Int I
156+
andBool I <Int size(LOCALS)
157+
andBool isTypedValue(LOCALS[I])
158+
159+
rule <k> #resolveSPLRcRef(Reference(OFFSET, place(local(I), PROJS), _, _), DEST, TARGET, FUNC, ARGS, UNWIND)
178160
=> #traverseProjection(
179-
DEST,
180-
VALUE,
161+
toStack(OFFSET, local(I)),
162+
#localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(I), OFFSET),
181163
PROJS,
182-
CtxSPLRefCell(TY) CTXTS
164+
.Contexts
183165
)
166+
~> #readProjection(false)
167+
~> #finishResolvedSPLRc(DEST, TARGET, FUNC, ARGS, UNWIND)
168+
...
169+
</k>
170+
<stack> STACK </stack>
171+
requires 0 <Int OFFSET
172+
andBool OFFSET <=Int size(STACK)
173+
andBool isStackFrame(STACK[OFFSET -Int 1])
174+
andBool 0 <=Int I
175+
176+
rule <k> SPLRc(PAYLOAD) ~> #finishResolvedSPLRc(DEST, TARGET, _FUNC, _ARGS, _UNWIND)
177+
=> #setLocalValue(DEST, PAYLOAD) ~> #continueAt(TARGET)
178+
...
179+
</k>
180+
181+
rule [spl-rc-deref-fallback]:
182+
<k> #finishSPLRcDeref(_VAL:Value, DEST, TARGET, FUNC, ARGS, UNWIND)
183+
=> #setUpCalleeData(lookupFunction(#tyOfCall(FUNC)), ARGS)
184184
...
185-
</k>
186-
[priority(30)]
185+
</k>
186+
<currentFunc> CALLER => #tyOfCall(FUNC) </currentFunc>
187+
<currentFrame>
188+
<currentBody> _ </currentBody>
189+
<caller> OLDCALLER => CALLER </caller>
190+
<dest> OLDDEST => DEST </dest>
191+
<target> OLDTARGET => TARGET </target>
192+
<unwind> OLDUNWIND => UNWIND </unwind>
193+
<locals> LOCALS </locals>
194+
</currentFrame>
195+
<stack> STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK </stack>
196+
[owise]
197+
```
187198

188-
syntax Context ::= CtxSPLRefCell ( Ty )
199+
```k
200+
// rule <k> #traverseProjection(
201+
// DEST,
202+
// SPLRefCell(VALUE),
203+
// projectionElemField(fieldIdx(2), TY) PROJS,
204+
// CTXTS
205+
// )
206+
// => #traverseProjection(
207+
// DEST,
208+
// VALUE,
209+
// PROJS,
210+
// CtxSPLRefCell(TY) CTXTS
211+
// )
212+
// ...
213+
// </k>
214+
// [priority(30)]
215+
216+
// syntax Context ::= CtxSPLRefCell ( Ty )
189217
190-
rule #buildUpdate(VAL, CtxSPLRefCell(_) CTXS) => #buildUpdate(SPLRefCell(VAL), CTXS)
191-
rule #projectionsFor(CtxSPLRefCell(TY) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemField(fieldIdx(2), TY) PROJS)
218+
// rule #buildUpdate(VAL, CtxSPLRefCell(_) CTXS) => #buildUpdate(SPLRefCell(VAL), CTXS)
219+
// rule #projectionsFor(CtxSPLRefCell(TY) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemField(fieldIdx(2), TY) PROJS)
192220
```
193221

194222
## RefCell::<&mut [u8]> helpers
@@ -214,15 +242,15 @@ expose the wrapped payload directly.
214242
215243
syntax KItem ::= #mkSPLBorrowData ( Place , Evaluation , Place , Bool ) [seqstrict(2)]
216244
217-
// rule <k> #mkSPLBorrowData(DEST, SPLRefCellData(BUF), SRC, false)
218-
// => #setLocalValue(DEST, SPLDataBorrow(SRC, BUF))
219-
// ...
220-
// </k>
245+
rule <k> #mkSPLBorrowData(DEST, SPLRefCell(BUF), SRC, false)
246+
=> #setLocalValue(DEST, SPLDataBorrow(SRC, BUF))
247+
...
248+
</k>
221249
222-
// rule <k> #mkSPLBorrowData(DEST, SPLRefCellData(BUF), SRC, true)
223-
// => #setLocalValue(DEST, SPLDataBorrowMut(SRC, BUF))
224-
// ...
225-
// </k>
250+
rule <k> #mkSPLBorrowData(DEST, SPLRefCell(BUF), SRC, true)
251+
=> #setLocalValue(DEST, SPLDataBorrowMut(SRC, BUF))
252+
...
253+
</k>
226254
```
227255

228256
```k

0 commit comments

Comments
 (0)