Skip to content

Commit fe0714f

Browse files
anvacaruehildenb
anvacaru
and
ehildenb
authored
Support expectStaticCall cheat code (#1448)
* implement expectCall * save wip * include delegate call * fix foundry_success predicate * add expectRegularCall(address,uint256,bytes) * add expectCreate * documentation * fix expect calls * run make black * docs * fix typo * retry failing proof once * add unimplemented selectors * foundry.k.check.expected Co-authored-by: Everett Hildenbrandt <[email protected]>
1 parent d7ffe15 commit fe0714f

File tree

6 files changed

+1243
-29
lines changed

6 files changed

+1243
-29
lines changed

‎include/kframework/foundry.md

Lines changed: 205 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -136,10 +136,10 @@ Hence, checking if a `DSTest.assert*` has failed amounts to reading as a boolean
136136
module FOUNDRY-SUCCESS
137137
imports EVM
138138
139-
syntax Bool ::= "foundry_success" "(" StatusCode "," Int "," Bool ")" [function, klabel(foundry_success), symbol]
140-
// -----------------------------------------------------------------------------------------------------------------
141-
rule foundry_success(EVMC_SUCCESS, 0, false) => true
142-
rule foundry_success(_, _, _) => false [owise]
139+
syntax Bool ::= "foundry_success" "(" StatusCode "," Int "," Bool "," Bool ")" [function, klabel(foundry_success), symbol]
140+
// --------------------------------------------------------------------------------------------------------------------------
141+
rule foundry_success(EVMC_SUCCESS, 0, false, false) => true
142+
rule foundry_success(_, _, _, _) => false [owise]
143143
144144
endmodule
145145
```
@@ -158,6 +158,12 @@ The configuration of the Foundry Cheat Codes is defined as follwing:
158158
- `<expectedRevert>` flags if the next call is expected to revert or not.
159159
- `<expectedDepth>` records the depth at which the call is expected to revert.
160160
- `<expectedBytes>` keeps the expected revert message as a ByteArray.
161+
3. The `<expectOpcode>` subconfiguration stores values used for `expect*OPCODE*` cheat codes.
162+
- `<isOpcodeExpected>` flags if a call opcode is expected.
163+
- `<expectedAddress>` keeps the expected caller.
164+
- `<expectedValue>` keeps expected `msg.value`.
165+
- `<expectedData>` keeps expected `calldata`.
166+
- `<opcodeType>` keeps track of what `CALL*` Opcode is expected.
161167

162168
```k
163169
module FOUNDRY-CHEAT-CODES
@@ -181,6 +187,13 @@ module FOUNDRY-CHEAT-CODES
181187
<expectedBytes> .ByteArray </expectedBytes>
182188
<expectedDepth> 0 </expectedDepth>
183189
</expected>
190+
<expectedOpcode>
191+
<isOpcodeExpected> false </isOpcodeExpected>
192+
<expectedAddress> .Account </expectedAddress>
193+
<expectedValue> 0 </expectedValue>
194+
<expectedData> .ByteArray </expectedData>
195+
<opcodeType> .OpcodeType </opcodeType>
196+
</expectedOpcode>
184197
</cheatcodes>
185198
```
186199

@@ -539,6 +552,136 @@ If the `expectRevert()` selector is matched, call the `#setExpectRevert` product
539552
orBool SELECTOR ==Int selector ( "expectRevert(bytes)" )
540553
```
541554

555+
Expecting a specific CALL/CREATE opcode
556+
---------------------------------------
557+
558+
First we define a sort to identify expected opcodes.
559+
560+
```k
561+
syntax OpcodeType ::= ".OpcodeType" | "Call" | "Static" | "Delegate" | "Create" | "Create2"
562+
```
563+
564+
If the `expect*OPCODE*` selector is matched, the rule will load the account into the state and add the `#setExpectOpcode` production to the K cell to initialize the `<expectedOpcode/>` subconfiguration with the given parameters.
565+
566+
```{.k .bytes}
567+
rule [foundry.call.expectStaticCall]:
568+
<k> #call_foundry SELECTOR ARGS
569+
=> #loadAccount #asWord(#range(ARGS, 0, 32))
570+
~> #let CODE_START = 96 #in
571+
#let DATA_LENGTH = #asWord(#range(ARGS, 64, 32)) #in
572+
#setExpectOpcode #asWord(#range(ARGS, 0, 32)) #range(ARGS, CODE_START, DATA_LENGTH) 0 Static
573+
...
574+
</k>
575+
requires SELECTOR ==Int selector ( "expectStaticCall(address,bytes)" )
576+
577+
rule [foundry.call.expectDelegateCall]:
578+
<k> #call_foundry SELECTOR ARGS
579+
=> #loadAccount #asWord(#range(ARGS, 0, 32))
580+
~> #let DATA_START = 96 #in
581+
#let DATA_LENGTH = #asWord(#range(ARGS, 64, 32)) #in
582+
#setExpectOpcode #asWord(#range(ARGS, 0, 32)) #range(ARGS, DATA_START, DATA_LENGTH) 0 Delegate
583+
...
584+
</k>
585+
requires SELECTOR ==Int selector ( "expectDelegateCall(address,bytes)" )
586+
587+
rule [foundry.call.expectRegularCall]:
588+
<k> #call_foundry SELECTOR ARGS
589+
=> #loadAccount #asWord(#range(ARGS, 0, 32))
590+
~> #let DATA_START = 128 #in
591+
#let DATA_LENGTH = #asWord(#range(ARGS, 96, 32)) #in
592+
#setExpectOpcode #asWord(#range(ARGS, 0, 32)) #range(ARGS, DATA_START, DATA_LENGTH) #asWord(#range(ARGS, 32, 32)) Call
593+
...
594+
</k>
595+
requires SELECTOR ==Int selector ( "expectRegularCall(address,uint256,bytes)" )
596+
597+
rule [foundry.call.expectCreate]:
598+
<k> #call_foundry SELECTOR ARGS
599+
=> #loadAccount #asWord(#range(ARGS, 0, 32))
600+
~> #let DATA_START = 128 #in
601+
#let DATA_LENGTH = #asWord(#range(ARGS, 96, 32)) #in
602+
#setExpectOpcode #asWord(#range(ARGS, 0, 32)) #range(ARGS, DATA_START, DATA_LENGTH) #asWord(#range(ARGS, 32, 32)) Create
603+
...
604+
</k>
605+
requires SELECTOR ==Int selector ( "expectCreate(address,uint256,bytes)" )
606+
607+
rule [foundry.call.expectCreate2]:
608+
<k> #call_foundry SELECTOR ARGS
609+
=> #loadAccount #asWord(#range(ARGS, 0, 32))
610+
~> #let DATA_START = 128 #in
611+
#let DATA_LENGTH = #asWord(#range(ARGS, 96, 32)) #in
612+
#setExpectOpcode #asWord(#range(ARGS, 0, 32)) #range(ARGS, DATA_START, DATA_LENGTH) #asWord(#range(ARGS, 32, 32)) Create2
613+
...
614+
</k>
615+
requires SELECTOR ==Int selector ( "expectCreate2(address,uint256,bytes)" )
616+
```
617+
618+
Next, everytime one of the `STATICCALL`, `DELEGATECALL`, `CALL`, `CREATE` or `CREATE2` opcodes is executed, we check if the `sender` address, `msg.value` and `calldata` match the expected values.
619+
`calldata` needs to match only the first byte.
620+
621+
```{.k .bytes}
622+
rule <k> (. => #clearExpectOpcode) ~> STATICCALL _GCAP ACCTTO ARGSTART ARGWIDTH _RETSTART _RETWIDTH ... </k>
623+
<localMem> LM </localMem>
624+
<expectedOpcode>
625+
<isOpcodeExpected> true </isOpcodeExpected>
626+
<expectedAddress> ACCTTO </expectedAddress>
627+
<expectedData> DATA </expectedData>
628+
<opcodeType> Static </opcodeType>
629+
...
630+
</expectedOpcode>
631+
requires #range(LM, ARGSTART, ARGWIDTH) ==K #range(DATA, 0, ARGWIDTH)
632+
[priority(40)]
633+
634+
rule <k> (. => #clearExpectOpcode) ~> DELEGATECALL _GCAP ACCTTO ARGSTART ARGWIDTH _RETSTART _RETWIDTH ... </k>
635+
<localMem> LM </localMem>
636+
<expectedOpcode>
637+
<isOpcodeExpected> true </isOpcodeExpected>
638+
<expectedAddress> ACCTTO </expectedAddress>
639+
<expectedData> DATA </expectedData>
640+
<opcodeType> Delegate </opcodeType>
641+
...
642+
</expectedOpcode>
643+
requires #range(LM, ARGSTART, ARGWIDTH) ==K #range(DATA, 0, ARGWIDTH)
644+
[priority(40)]
645+
646+
rule <k> (. => #clearExpectOpcode) ~> CALL _GCAP ACCTTO VALUE ARGSTART ARGWIDTH _RETSTART _RETWIDTH ... </k>
647+
<localMem> LM </localMem>
648+
<expectedOpcode>
649+
<isOpcodeExpected> true </isOpcodeExpected>
650+
<expectedAddress> ACCTTO </expectedAddress>
651+
<expectedData> DATA </expectedData>
652+
<opcodeType> Call </opcodeType>
653+
<expectedValue> VALUE </expectedValue>
654+
</expectedOpcode>
655+
requires #range(LM, ARGSTART, ARGWIDTH) ==K #range(DATA, 0, ARGWIDTH)
656+
[priority(40)]
657+
658+
rule <k> (. => #clearExpectOpcode) ~> CREATE VALUE MEMSTART MEMWIDTH ... </k>
659+
<localMem> LM </localMem>
660+
<id> ACCT </id>
661+
<expectedOpcode>
662+
<isOpcodeExpected> true </isOpcodeExpected>
663+
<expectedAddress> ACCT </expectedAddress>
664+
<expectedData> DATA </expectedData>
665+
<opcodeType> Create </opcodeType>
666+
<expectedValue> VALUE </expectedValue>
667+
</expectedOpcode>
668+
requires #range(LM, MEMSTART, MEMWIDTH) ==K #range(DATA, 0, MEMWIDTH)
669+
[priority(40)]
670+
671+
rule <k> (. => #clearExpectOpcode) ~> CREATE2 VALUE MEMSTART MEMWIDTH _SALT ... </k>
672+
<localMem> LM </localMem>
673+
<id> ACCT </id>
674+
<expectedOpcode>
675+
<isOpcodeExpected> true </isOpcodeExpected>
676+
<expectedAddress> ACCT </expectedAddress>
677+
<expectedData> DATA </expectedData>
678+
<opcodeType> Create2 </opcodeType>
679+
<expectedValue> VALUE </expectedValue>
680+
</expectedOpcode>
681+
requires #range(LM, MEMSTART, MEMWIDTH) ==K #range(DATA, 0, MEMWIDTH)
682+
[priority(40)]
683+
```
684+
542685
Pranks
543686
------
544687

@@ -768,6 +911,37 @@ Utils
768911
</expected>
769912
```
770913

914+
- `#setExpectOpcode` initializes the `<expectedOpcode>` subconfiguration with an expected `Address`, and `ByteArray` to match the calldata.
915+
`CallType` is used to specify what `CALL*` opcode is expected.
916+
917+
```k
918+
syntax KItem ::= "#setExpectOpcode" Account ByteArray Int OpcodeType [klabel(foundry_setExpectOpcode)]
919+
// ------------------------------------------------------------------------------------------------------
920+
rule <k> #setExpectOpcode ACCT DATA VALUE OPTYPE => . ... </k>
921+
<expectedOpcode>
922+
<isOpcodeExpected> _ => true </isOpcodeExpected>
923+
<expectedAddress> _ => ACCT </expectedAddress>
924+
<expectedData> _ => DATA </expectedData>
925+
<expectedValue> _ => VALUE </expectedValue>
926+
<opcodeType> _ => OPTYPE </opcodeType>
927+
</expectedOpcode>
928+
```
929+
930+
- `#clearExpectOpcode` restore the `<expectedOpcode>` subconfiguration to its initial values.
931+
932+
```k
933+
syntax KItem ::= "#clearExpectOpcode" [klabel(foundry_clearExpectOpcode)]
934+
// -------------------------------------------------------------------------
935+
rule <k> #clearExpectOpcode => . ... </k>
936+
<expectedOpcode>
937+
<isOpcodeExpected> _ => false </isOpcodeExpected>
938+
<expectedAddress> _ => .Account </expectedAddress>
939+
<expectedData> _ => .ByteArray </expectedData>
940+
<opcodeType> _ => .OpcodeType </opcodeType>
941+
<expectedValue> _ => 0 </expectedValue>
942+
</expectedOpcode>
943+
```
944+
771945
- `#setPrank NEWCALLER NEWORIGIN SINGLEPRANK` will set the `<prank/>` subconfiguration for the given accounts.
772946

773947
```k
@@ -832,30 +1006,38 @@ If the production is matched when no prank is active, it will be ignored.
8321006
- selectors for cheat code functions.
8331007

8341008
```k
835-
rule ( selector ( "assume(bool)" ) => 1281615202 )
836-
rule ( selector ( "deal(address,uint256)" ) => 3364511341 )
837-
rule ( selector ( "etch(address,bytes)" ) => 3033974658 )
838-
rule ( selector ( "warp(uint256)" ) => 3856056066 )
839-
rule ( selector ( "roll(uint256)" ) => 528174896 )
840-
rule ( selector ( "fee(uint256)" ) => 968063664 )
841-
rule ( selector ( "chainId(uint256)" ) => 1078582738 )
842-
rule ( selector ( "coinbase(address)" ) => 4282924116 )
843-
rule ( selector ( "label(address,string)" ) => 3327641368 )
844-
rule ( selector ( "getNonce(address)" ) => 755185067 )
845-
rule ( selector ( "addr(uint256)" ) => 4288775753 )
846-
rule ( selector ( "load(address,bytes32)" ) => 1719639408 )
847-
rule ( selector ( "store(address,bytes32,bytes32)" ) => 1892290747 )
848-
rule ( selector ( "setNonce(address,uint64)" ) => 4175530839 )
849-
rule ( selector ( "expectRevert()" ) => 4102309908 )
850-
rule ( selector ( "expectRevert(bytes)" ) => 4069379763 )
851-
rule ( selector ( "startPrank(address)" ) => 105151830 )
852-
rule ( selector ( "startPrank(address,address)" ) => 1169514616 )
853-
rule ( selector ( "stopPrank()" ) => 2428830011 )
1009+
rule ( selector ( "assume(bool)" ) => 1281615202 )
1010+
rule ( selector ( "deal(address,uint256)" ) => 3364511341 )
1011+
rule ( selector ( "etch(address,bytes)" ) => 3033974658 )
1012+
rule ( selector ( "warp(uint256)" ) => 3856056066 )
1013+
rule ( selector ( "roll(uint256)" ) => 528174896 )
1014+
rule ( selector ( "fee(uint256)" ) => 968063664 )
1015+
rule ( selector ( "chainId(uint256)" ) => 1078582738 )
1016+
rule ( selector ( "coinbase(address)" ) => 4282924116 )
1017+
rule ( selector ( "label(address,string)" ) => 3327641368 )
1018+
rule ( selector ( "getNonce(address)" ) => 755185067 )
1019+
rule ( selector ( "addr(uint256)" ) => 4288775753 )
1020+
rule ( selector ( "load(address,bytes32)" ) => 1719639408 )
1021+
rule ( selector ( "store(address,bytes32,bytes32)" ) => 1892290747 )
1022+
rule ( selector ( "setNonce(address,uint64)" ) => 4175530839 )
1023+
rule ( selector ( "expectRevert()" ) => 4102309908 )
1024+
rule ( selector ( "expectRevert(bytes)" ) => 4069379763 )
1025+
rule ( selector ( "startPrank(address)" ) => 105151830 )
1026+
rule ( selector ( "startPrank(address,address)" ) => 1169514616 )
1027+
rule ( selector ( "stopPrank()" ) => 2428830011 )
1028+
rule ( selector ( "expectStaticCall(address,bytes)" ) => 2232945516 )
1029+
rule ( selector ( "expectDelegateCall(address,bytes)" ) => 1030406631 )
1030+
rule ( selector ( "expectRegularCall(address,uint256,bytes)" ) => 1973496647 )
1031+
rule ( selector ( "expectCreate(address,uint256,bytes)" ) => 658968394 )
1032+
rule ( selector ( "expectCreate2(address,uint256,bytes)" ) => 3854582462 )
8541033
```
8551034

8561035
- selectors for unimplemented cheat code functions.
8571036

8581037
```k
1038+
rule selector ( "expectRegularCall(address,bytes)" ) => 3178868520
1039+
rule selector ( "expectNoCall()" ) => 3861374088
1040+
rule selector ( "symbolicStorage(address)" ) => 769677742
8591041
rule selector ( "sign(uint256,bytes32)" ) => 3812747940
8601042
rule selector ( "ffi(string[])" ) => 2299921511
8611043
rule selector ( "setEnv(string,string)" ) => 1029252078

‎kevm-pyk/src/kevm_pyk/kevm.py

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -367,12 +367,12 @@ def _patch_symbol_table(symbol_table: Dict[str, Any]) -> None:
367367
KEVM._patch_symbol_table(symbol_table)
368368

369369
@staticmethod
370-
def success(s: KInner, dst: KInner, r: KInner) -> KApply:
371-
return KApply('foundry_success ', [s, dst, r])
370+
def success(s: KInner, dst: KInner, r: KInner, c: KInner) -> KApply:
371+
return KApply('foundry_success ', [s, dst, r, c])
372372

373373
@staticmethod
374-
def fail(s: KInner, dst: KInner, r: KInner) -> KApply:
375-
return notBool(Foundry.success(s, dst, r))
374+
def fail(s: KInner, dst: KInner, r: KInner, c: KInner) -> KApply:
375+
return notBool(Foundry.success(s, dst, r, c))
376376

377377
# address(uint160(uint256(keccak256("foundry default caller"))))
378378

‎kevm-pyk/src/kevm_pyk/solc_to_k.py

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -411,6 +411,11 @@ def _init_term(
411411
),
412412
'SINGLECALL_CELL': FALSE,
413413
'EXPECTEDREVERT_CELL': FALSE,
414+
'ISOPCODEEXPECTED_CELL': FALSE,
415+
'EXPECTEDADDRESS_CELL': KToken('.Account', 'K'),
416+
'EXPECTEDVALUE_CELL': intToken(0),
417+
'EXPECTEDDATA_CELL': KToken('.ByteArray', 'K'),
418+
'OPCODETYPE_CELL': KToken('.OpcodeType', 'K'),
414419
}
415420

416421
if calldata is not None:
@@ -426,7 +431,12 @@ def _final_cterm(empty_config: KInner, contract_name: str, *, failing: bool, is_
426431
final_term = _final_term(empty_config, contract_name)
427432
key_dst = KEVM.loc(KToken('FoundryCheat . Failed', 'ContractAccess'))
428433
dst_failed_post = KEVM.lookup(KVariable('CHEATCODE_STORAGE_FINAL'), key_dst)
429-
foundry_success = Foundry.success(KVariable('STATUSCODE_FINAL'), dst_failed_post, KVariable('EXPECTEDREVERT_FINAL'))
434+
foundry_success = Foundry.success(
435+
KVariable('STATUSCODE_FINAL'),
436+
dst_failed_post,
437+
KVariable('EXPECTEDREVERT_FINAL'),
438+
KVariable('ISOPCODEEXPECTED_FINAL'),
439+
)
430440
final_cterm = CTerm(final_term)
431441
if is_test:
432442
if not failing:
@@ -460,10 +470,16 @@ def _final_term(empty_config: KInner, contract_name: str) -> KInner:
460470
]
461471
),
462472
'EXPECTEDREVERT_CELL': KVariable('EXPECTEDREVERT_FINAL'),
473+
'ISOPCODEEXPECTED_CELL': KVariable('ISOPCODEEXPECTED_FINAL'),
463474
}
464475
return abstract_cell_vars(
465476
substitute(empty_config, final_subst),
466-
[KVariable('STATUSCODE_FINAL'), KVariable('ACCOUNTS_FINAL'), KVariable('EXPECTEDREVERT_FINAL')],
477+
[
478+
KVariable('STATUSCODE_FINAL'),
479+
KVariable('ACCOUNTS_FINAL'),
480+
KVariable('EXPECTEDREVERT_FINAL'),
481+
KVariable('ISOPCODEEXPECTED_FINAL'),
482+
],
467483
)
468484

469485

0 commit comments

Comments
 (0)