Skip to content

Commit c17566d

Browse files
dkcummingdkcumming
committed
Updated Solana cheatcodes with Span in Call Terminator 
1 parent 0b0c0e9 commit c17566d

2 files changed

Lines changed: 21 additions & 21 deletions

File tree

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

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -484,25 +484,25 @@ An `AccountInfo` reference is passed to the function.
484484
```k
485485
// special rule to intercept the cheat code function calls and replace them by #mkPToken<thing>
486486
rule [cheatcode-is-account]:
487-
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
487+
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
488488
=> #mkPTokenAccount(PLACE) ~> #continueAt(TARGET)
489489
</k>
490490
requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::cheatcode_is_account"
491491
[priority(30), preserves-definedness]
492492
rule [cheatcode-is-mint]:
493-
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
493+
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
494494
=> #mkPTokenMint(PLACE) ~> #continueAt(TARGET)
495495
</k>
496496
requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::cheatcode_is_mint"
497497
[priority(30), preserves-definedness]
498498
rule [cheatcode-is-multisig]:
499-
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
499+
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
500500
=> #mkPTokenMultisig(PLACE) ~> #continueAt(TARGET)
501501
</k>
502502
requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::cheatcode_is_multisig"
503503
[priority(30), preserves-definedness]
504504
rule [cheatcode-is-rent]:
505-
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
505+
<k> #execTerminatorCall(_, FUNC, operandCopy(PLACE) .Operands, _DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
506506
=> #mkPTokenRent(PLACE) ~> #continueAt(TARGET)
507507
</k>
508508
requires #functionName(FUNC) ==String "pinocchio_token_program::entrypoint::cheatcode_is_rent"
@@ -771,7 +771,7 @@ The `PAccByteRef` carries a stack offset, so it must be adjusted on reads.
771771
```k
772772
// intercept calls to `borrow_data_unchecked` and write `PAccountRef` to destination
773773
rule [cheatcode-borrow-data]:
774-
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, TARGET, _UNWIND) ~> _CONT
774+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
775775
=> #mkPAccByteRef(DEST, operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) .ProjectionElems))), mutabilityNot)
776776
~> #continueAt(TARGET)
777777
</k>
@@ -780,7 +780,7 @@ The `PAccByteRef` carries a stack offset, so it must be adjusted on reads.
780780
781781
// intercept calls to `borrow_mut_data_unchecked` and write `PAccountRef` to destination
782782
rule [cheatcode-borrow-mut-data]:
783-
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, TARGET, _UNWIND) ~> _CONT
783+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
784784
=> #mkPAccByteRef(DEST, operandCopy(place(LOCAL, appendP(PROJS, projectionElemDeref projectionElemField(fieldIdx(0), #hack()) .ProjectionElems))), mutabilityMut)
785785
~> #continueAt(TARGET)
786786
</k>
@@ -848,7 +848,7 @@ NB Both `load_unchecked` and `load_mut_unchecked` are intercepted in the same wa
848848
```k
849849
// intercept calls to `load_unchecked` and `load_mut_unchecked`
850850
rule [cheatcode-mk-iface-account-ref]:
851-
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND) ~> _CONT
851+
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
852852
=> #mkPAccountRef(DEST, OPERAND, PAccountIAcc, true)
853853
~> #continueAt(TARGET)
854854
</k>
@@ -860,7 +860,7 @@ NB Both `load_unchecked` and `load_mut_unchecked` are intercepted in the same wa
860860
[priority(30), preserves-definedness]
861861
862862
rule [cheatcode-mk-imint-ref]:
863-
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND) ~> _CONT
863+
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
864864
=> #mkPAccountRef(DEST, OPERAND, PAccountIMint, true)
865865
~> #continueAt(TARGET)
866866
</k>
@@ -872,7 +872,7 @@ NB Both `load_unchecked` and `load_mut_unchecked` are intercepted in the same wa
872872
[priority(30), preserves-definedness]
873873
874874
rule [cheatcode-mk-imulti-ref]:
875-
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND) ~> _CONT
875+
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
876876
=> #mkPAccountRef(DEST, OPERAND, PAccountIMulti, true)
877877
~> #continueAt(TARGET)
878878
</k>
@@ -884,7 +884,7 @@ NB Both `load_unchecked` and `load_mut_unchecked` are intercepted in the same wa
884884
[priority(30), preserves-definedness]
885885
886886
rule [cheatcode-mk-prent-ref]:
887-
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND) ~> _CONT
887+
<k> #execTerminatorCall(_, FUNC, OPERAND .Operands, DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
888888
=> #mkPAccountRef(DEST, OPERAND, PAccountPRent, false)
889889
~> #continueAt(TARGET)
890890
</k>
@@ -930,7 +930,7 @@ Therefore, the value gets created in a dedicated place on first access.
930930

931931
```k
932932
rule [cheatcode-get-sys-prent]:
933-
<k> #execTerminatorCall(_, FUNC, .Operands, DEST, TARGET, _UNWIND) ~> _CONT
933+
<k> #execTerminatorCall(_, FUNC, .Operands, DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
934934
=> #writeSysRent(DEST)
935935
~> #continueAt(TARGET)
936936
</k>

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

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -330,7 +330,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
330330
.ProjectionElems
331331
332332
rule [cheatcode-is-spl-account]:
333-
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
333+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
334334
=> #forceSetPlaceValue(
335335
place(LOCAL, appendP(PROJS, DATA_BUFFER_PROJS)), // navigate to [u8] data buffer
336336
SPLDataBuffer(
@@ -378,7 +378,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
378378
</k>
379379
380380
rule [cheatcode-is-spl-mint]:
381-
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
381+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
382382
=> #forceSetPlaceValue(
383383
place(LOCAL, appendP(PROJS, DATA_BUFFER_PROJS)), // navigate to [u8] data buffer
384384
SPLDataBuffer(
@@ -414,7 +414,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
414414
[priority(30), preserves-definedness]
415415
416416
rule [cheatcode-is-spl-rent]:
417-
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
417+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
418418
=> #forceSetPlaceValue(
419419
place(LOCAL, appendP(PROJS, DATA_BUFFER_PROJS)), // navigate to [u8] data buffer
420420
SPLDataBuffer(
@@ -438,7 +438,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
438438
[priority(30), preserves-definedness]
439439
440440
rule [cheatcode-is-spl-multisig]:
441-
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
441+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, _DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
442442
=> #forceSetPlaceValue(
443443
place(LOCAL, appendP(PROJS, DATA_BUFFER_PROJS)), // navigate to [u8] data buffer
444444
SPLDataBuffer(
@@ -491,7 +491,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
491491
```k
492492
// RefCell::<&mut [u8]>::borrow / borrow_mut - returns Ref/RefMut wrapper with pointer to data
493493
rule [spl-borrow-data]:
494-
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, TARGET, _UNWIND) ~> _CONT
494+
<k> #execTerminatorCall(_, FUNC, operandCopy(place(LOCAL, PROJS)) .Operands, DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
495495
=> #setSPLBorrowData(DEST, operandCopy(place(LOCAL, PROJS)))
496496
~> #continueAt(TARGET)
497497
</k>
@@ -511,7 +511,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
511511
```k
512512
// Account/Mint::unpack_from_slice, bincode::deserialize (for Rent) - extracts struct from SPLDataBuffer
513513
rule [spl-account-unpack]:
514-
<k> #execTerminatorCall(_, FUNC, OP:Operand .Operands, DEST, TARGET, _UNWIND) ~> _CONT
514+
<k> #execTerminatorCall(_, FUNC, OP:Operand .Operands, DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
515515
=> #splUnpack(DEST, #withDeref(OP))
516516
~> #continueAt(TARGET)
517517
</k>
@@ -525,7 +525,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
525525
526526
// Account/Mint::pack_into_slice - writes struct into SPLDataBuffer
527527
rule [spl-account-pack]:
528-
<k> #execTerminatorCall(_, FUNC, SRC:Operand DST:Operand .Operands, _DEST, TARGET, _UNWIND) ~> _CONT
528+
<k> #execTerminatorCall(_, FUNC, SRC:Operand DST:Operand .Operands, _DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
529529
=> #splPack(#withDeref(SRC), #withDeref(DST)) ~> #continueAt(TARGET)
530530
</k>
531531
requires #isSPLPackFunc(#functionName(FUNC))
@@ -541,7 +541,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
541541
```{.k .symbolic}
542542
// Rent::get - returns stable value, cached in outermost frame
543543
rule [spl-rent-get]:
544-
<k> #execTerminatorCall(_, FUNC, .Operands, DEST, TARGET, _UNWIND) ~> _CONT
544+
<k> #execTerminatorCall(_, FUNC, .Operands, DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
545545
=> #writeSPLSysRent(DEST)
546546
~> #continueAt(TARGET)
547547
</k>
@@ -594,7 +594,7 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
594594
## Pubkey comparison shortcut
595595
```k
596596
rule [spl-cmp-pubkeys]:
597-
<k> #execTerminatorCall(_, FUNC, ARG1:Operand ARG2:Operand .Operands, DEST, TARGET, _UNWIND) ~> _CONT
597+
<k> #execTerminatorCall(_, FUNC, ARG1:Operand ARG2:Operand .Operands, DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
598598
=> #execSPLCmpPubkeys( DEST, #withDeref(ARG1), #withDeref(ARG2))
599599
~> #continueAt(TARGET)
600600
</k>
@@ -647,7 +647,7 @@ be called prior to capturing initial state and prior to executing the implementa
647647
<k> #execTerminatorCall(_, FUNC,
648648
operandCopy(place(LOCAL1, PROJS1))
649649
operandCopy(place(LOCAL2, PROJS2))
650-
.Operands, _DEST, TARGET, _UNWIND) ~> _CONT
650+
.Operands, _DEST, TARGET, _UNWIND, _SPAN) ~> _CONT
651651
=> #maybeLinkAccounts(
652652
operandCopy(place(LOCAL1, appendP(PROJS1, KEY_PROJS))),
653653
operandCopy(place(LOCAL2, appendP(PROJS2, KEY_PROJS))),

0 commit comments

Comments
 (0)