Skip to content

Commit e5c1bdb

Browse files
anvacaruehildenb
anvacaru
and
ehildenb
authored
Implement expectRevert cheat codes (#1436)
* Add expectRevert structure * save wip * check expectedBytes * tidy up * fix typo * Update foundry.md Co-authored-by: Everett Hildenbrandt <[email protected]> * uncomment tests * remove 'expectRevert(bytes4)' for now * formatting * update foundry.k.check.expected * initalize InterimState cell with .List * clean-ups Co-authored-by: Everett Hildenbrandt <[email protected]>
1 parent a0dc06d commit e5c1bdb

File tree

6 files changed

+381
-17
lines changed

6 files changed

+381
-17
lines changed

‎include/kframework/foundry.md

Lines changed: 91 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -136,24 +136,28 @@ 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 ")" [function, klabel(foundry_success), symbol]
140-
// --------------------------------------------------------------------------------------------------------
141-
rule foundry_success(EVMC_SUCCESS, 0) => true
142-
rule foundry_success(_, _) => false [owise]
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]
143143
144144
endmodule
145145
```
146146

147147
### Foundry Cheat Codes
148148

149149
The configuration of the Foundry Cheat Codes is defined as follwing:
150-
1. The `<prank>` subconfiguration stores values which are used during the execution of any kind of `prank` cheatcode:
150+
1. The `<prank>` subconfiguration stores values which are used during the execution of any kind of `prank` cheat code:
151151
- `<prevCaller>` keeps the current address of the contract that initiated the prank.
152152
- `<prevOrigin>` keeps the current address of the `tx.origin` value.
153153
- `<newCaller>` and `<newOrigin>` are addresses to be assigned after the prank call to `msg.sender` and `tx.origin`.
154154
- `<active>` signals if a prank is active or not.
155155
- `<depth>` records the current call depth at which the prank was invoked.
156156
- `<singleCall>` tells whether the prank stops by itself after the next call or when a `stopPrank` cheat code is invoked.
157+
2. The `<expected>` subconfiguration stores values used for the `expectRevert` cheat code.
158+
- `<expectedRevert>` flags if the next call is expected to revert or not.
159+
- `<expectedDepth>` records the depth at which the call is expected to revert.
160+
- `<expectedBytes>` keeps the expected revert message as a ByteArray.
157161

158162
```k
159163
module FOUNDRY-CHEAT-CODES
@@ -172,6 +176,11 @@ module FOUNDRY-CHEAT-CODES
172176
<depth> 0 </depth>
173177
<singleCall> false </singleCall>
174178
</prank>
179+
<expected>
180+
<expectedRevert> false </expectedRevert>
181+
<expectedBytes> .ByteArray </expectedBytes>
182+
<expectedDepth> 0 </expectedDepth>
183+
</expected>
175184
</cheatcodes>
176185
```
177186

@@ -469,6 +478,67 @@ This rule then takes from the function call data the account using `#asWord(#ran
469478
requires SELECTOR ==Int selector ( "store(address,bytes32,bytes32)" )
470479
```
471480

481+
#### expectRevert - expect the next call to revert.
482+
483+
```
484+
function expectRevert() external;
485+
function expectRevert(bytes4 msg) external;
486+
function expectRevert(bytes calldata msg) external;
487+
```
488+
489+
Ignore all cheat code calls which take place while `expectRevert` is active.
490+
491+
```{.k .bytes}
492+
rule [foundry.call.ignoreCalls]:
493+
<k> #call_foundry _ _ => . ... </k>
494+
<expected>
495+
<expectedRevert> true </expectedRevert>
496+
...
497+
</expected>
498+
[priority(35)]
499+
```
500+
501+
Catch reverts.
502+
If the current call depth is equal with the `expectedDepth` and the `expectedBytes` match the `<output>` cell, then replace the `EVMC_REVERT` status code with `EVMC_SUCCESS`.
503+
504+
```{.k .bytes}
505+
rule <statusCode> EVMC_REVERT => EVMC_SUCCESS </statusCode>
506+
<k> #halt ~> #return _RETSTART _RETWIDTH ... </k>
507+
<output> OUT </output>
508+
<callDepth> CD </callDepth>
509+
<expected>
510+
<expectedRevert> true => false </expectedRevert>
511+
<expectedDepth> CD </expectedDepth>
512+
<expectedBytes> EXPECTED </expectedBytes>
513+
</expected>
514+
requires (EXPECTED =/=K .ByteArray andBool EXPECTED ==K #range(OUT, 4, #sizeByteArray(OUT) -Int 4))
515+
orBool EXPECTED ==K .ByteArray
516+
[priority(40)]
517+
```
518+
519+
Change the status code from `EVMC_SUCCESS` to `EVMC_REVERT` if a revert is expected but the call succeded.
520+
521+
```{.k .bytes}
522+
rule <statusCode> EVMC_SUCCESS => EVMC_REVERT </statusCode>
523+
<k> #halt ~> #return _RETSTART _RETWIDTH ... </k>
524+
<callDepth> CD </callDepth>
525+
<expected>
526+
<expectedRevert> true => false </expectedRevert>
527+
<expectedDepth> CD </expectedDepth>
528+
...
529+
</expected>
530+
[priority(40)]
531+
```
532+
533+
If the `expectRevert()` selector is matched, call the `#setExpectRevert` production to initialize the `<expected>` subconfiguration.
534+
535+
```{.k .bytes}
536+
rule [foundry.call.expectRevert]:
537+
<k> #call_foundry SELECTOR ARGS => #setExpectRevert ARGS ... </k>
538+
requires SELECTOR ==Int selector ( "expectRevert()" )
539+
orBool SELECTOR ==Int selector ( "expectRevert(bytes)" )
540+
```
541+
472542
Pranks
473543
------
474544

@@ -652,6 +722,20 @@ Utils
652722
</account>
653723
```
654724

725+
- `#setExpectRevert` sets the `<expected>` subconfiguration with the current call depth and the expected message from `expectRevert`.
726+
727+
```k
728+
syntax KItem ::= "#setExpectRevert" ByteArray [klabel(foundry_setExpectedRevert)]
729+
// ---------------------------------------------------------------------------------
730+
rule <k> #setExpectRevert EXPECTED => . ... </k>
731+
<callDepth> CD </callDepth>
732+
<expected>
733+
<expectedRevert> false => true </expectedRevert>
734+
<expectedDepth> _ => CD +Int 1 </expectedDepth>
735+
<expectedBytes> _ => EXPECTED </expectedBytes>
736+
</expected>
737+
```
738+
655739
- `#setPrank NEWCALLER NEWORIGIN` will set the `<prank/>` subconfiguration for the given accounts.
656740

657741
```k
@@ -694,7 +778,6 @@ If the production is matched when no prank is active, it will be ignored.
694778
<prevOrigin> OG </prevOrigin>
695779
...
696780
</prank>
697-
698781
```
699782

700783
- `#clearPrank` will clear the prank subconfiguration.
@@ -731,6 +814,8 @@ If the production is matched when no prank is active, it will be ignored.
731814
rule ( selector ( "load(address,bytes32)" ) => 1719639408 )
732815
rule ( selector ( "store(address,bytes32,bytes32)" ) => 1892290747 )
733816
rule ( selector ( "setNonce(address,uint64)" ) => 4175530839 )
817+
rule ( selector ( "expectRevert()" ) => 4102309908 )
818+
rule ( selector ( "expectRevert(bytes)" ) => 4069379763 )
734819
rule ( selector ( "startPrank(address)" ) => 105151830 )
735820
rule ( selector ( "startPrank(address,address)" ) => 1169514616 )
736821
rule ( selector ( "stopPrank()" ) => 2428830011 )
@@ -757,13 +842,8 @@ If the production is matched when no prank is active, it will be ignored.
757842
rule selector ( "envString(string,string)" ) => 347089865
758843
rule selector ( "envBytes(string,string)" ) => 3720504603
759844
rule selector ( "prank(address)" ) => 3395723175
760-
rule selector ( "startPrank(address)" ) => 105151830
761845
rule selector ( "prank(address,address)" ) => 1206193358
762-
rule selector ( "startPrank(address,address)" ) => 1169514616
763-
rule selector ( "stopPrank()" ) => 2428830011
764-
rule selector ( "expectRevert(bytes)" ) => 4069379763
765846
rule selector ( "expectRevert(bytes4)" ) => 3273568480
766-
rule selector ( "expectRevert()" ) => 4102309908
767847
rule selector ( "record()" ) => 644673801
768848
rule selector ( "accesses(address)" ) => 1706857601
769849
rule selector ( "expectEmit(bool,bool,bool,bool)" ) => 1226622914

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

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

346346
@staticmethod
347-
def success(s: KInner, dst: KInner) -> KApply:
348-
return KApply('foundry_success ', [s, dst])
347+
def success(s: KInner, dst: KInner, r: KInner) -> KApply:
348+
return KApply('foundry_success ', [s, dst, r])
349349

350350
@staticmethod
351-
def fail(s: KInner, dst: KInner) -> KApply:
352-
return notBool(Foundry.success(s, dst))
351+
def fail(s: KInner, dst: KInner, r: KInner) -> KApply:
352+
return notBool(Foundry.success(s, dst, r))
353353

354354
# address(uint160(uint256(keccak256("foundry default caller"))))
355355

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

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -379,6 +379,7 @@ def _init_term(
379379
'CALLER_CELL': KVariable('CALLER_ID'),
380380
'ACCESSEDACCOUNTS_CELL': KApply('.Set'),
381381
'ACCESSEDSTORAGE_CELL': KApply('.Map'),
382+
'INTERIMSTATES_CELL': KApply('.List'),
382383
'ACTIVEACCOUNTS_CELL': build_assoc(
383384
KApply('.Set'),
384385
KLabel('_Set_'),
@@ -413,6 +414,7 @@ def _init_term(
413414
KVariable('ACCOUNTS_INIT'),
414415
]
415416
),
417+
'EXPECTEDREVERT_CELL': FALSE,
416418
}
417419

418420
if calldata is not None:
@@ -428,7 +430,7 @@ def _final_cterm(empty_config: KInner, contract_name: str, *, failing: bool, is_
428430
final_term = _final_term(empty_config, contract_name)
429431
key_dst = KEVM.loc(KToken('FoundryCheat . Failed', 'ContractAccess'))
430432
dst_failed_post = KEVM.lookup(KVariable('CHEATCODE_STORAGE_FINAL'), key_dst)
431-
foundry_success = Foundry.success(KVariable('STATUSCODE_FINAL'), dst_failed_post)
433+
foundry_success = Foundry.success(KVariable('STATUSCODE_FINAL'), dst_failed_post, KVariable('EXPECTEDREVERT_FINAL'))
432434
final_cterm = CTerm(final_term)
433435
if is_test:
434436
if not failing:
@@ -461,9 +463,11 @@ def _final_term(empty_config: KInner, contract_name: str) -> KInner:
461463
KVariable('ACCOUNTS_FINAL'),
462464
]
463465
),
466+
'EXPECTEDREVERT_CELL': KVariable('EXPECTEDREVERT_FINAL'),
464467
}
465468
return abstract_cell_vars(
466-
substitute(empty_config, final_subst), [KVariable('STATUSCODE_FINAL'), KVariable('ACCOUNTS_FINAL')]
469+
substitute(empty_config, final_subst),
470+
[KVariable('STATUSCODE_FINAL'), KVariable('ACCOUNTS_FINAL'), KVariable('EXPECTEDREVERT_FINAL')],
467471
)
468472

469473

‎tests/foundry/exclude

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,8 @@ EnvTest.testEnvStringArray
3636
EnvTest.testEnvUInt
3737
EnvTest.testEnvUIntArray
3838
EtchTest.testEtchSymbolic
39+
ExpectRevertTest.testFail_expectRevert_bytes4
40+
ExpectRevertTest.test_expectRevert_bytes4
3941
FfiTest.testffi
4042
FfiTest.testFFIFOO
4143
FfiTest.testFFIScript

0 commit comments

Comments
 (0)