Skip to content

Commit 4b49f34

Browse files
anvacaruanvacaru
authored
Revert for unimplemented cheat codes. (#1426)
* add rules to revert for undefined cheats * add unparseSelector production * fix typos * add test * fix test * review * fix typo * Fix Simple.t.sol * update foundry.k.check.expected
1 parent aab0445 commit 4b49f34

File tree

4 files changed

+157
-5
lines changed

4 files changed

+157
-5
lines changed

‎foundry.md

Lines changed: 86 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -216,10 +216,10 @@ We define two productions named `#return_foundry` and `#call_foundry`, which wil
216216
The rule `foundry.return` will rewrite the `#return_foundry` production into other productions that will place the output of the execution into the local memory, refund the gas value of the call and push the value `1` on the call stack.
217217

218218
```{.k .bytes}
219-
syntax KItem ::= "#error_foundry" [klabel(foundry_error)]
220-
| "#return_foundry" Int Int [klabel(foundry_return)]
219+
syntax KItem ::= "#return_foundry" Int Int [klabel(foundry_return)]
221220
| "#call_foundry" Int ByteArray [klabel(foundry_call)]
222-
// ---------------------------------------------------------------------
221+
| "#error_foundry" Int ByteArray [klabel(foundry_error)]
222+
// -----------------------------------------------------------------------
223223
rule [foundry.return]:
224224
<k> #return_foundry RETSTART RETWIDTH
225225
=> #setLocalMem RETSTART RETWIDTH OUT
@@ -230,6 +230,13 @@ The rule `foundry.return` will rewrite the `#return_foundry` production into oth
230230
<callGas> GCALL </callGas>
231231
```
232232

233+
We define a new status code named `FOUNDRY_UNIMPLEMENTED`, which signals that the execution ran into an unimplemented cheat code.
234+
235+
```{.k .bytes}
236+
syntax ExceptionalStatusCode ::= "FOUNDRY_UNIMPLEMENTED"
237+
// --------------------------------------------------------
238+
```
239+
233240
Below, we define rules for the `#call_foundry` production, handling the cheat codes.
234241

235242
#### `assume` - Insert a condition
@@ -541,7 +548,9 @@ Otherwise, throw an error for any other call to the Foundry contract.
541548

542549
```{.k .bytes}
543550
rule [foundry.call.owise]:
544-
<k> #call_foundry _ _ => #error_foundry ... </k> [owise]
551+
<k> #call_foundry SELECTOR ARGS => #error_foundry SELECTOR ARGS ... </k>
552+
<statusCode> _ => FOUNDRY_UNIMPLEMENTED </statusCode>
553+
[owise]
545554
```
546555

547556
Utils
@@ -724,6 +733,79 @@ If the production is matched when no prank is active, it will be ignored.
724733
rule ( selector ( "startPrank(address,address)" ) => 1169514616 )
725734
rule ( selector ( "stopPrank()" ) => 2428830011 )
726735
```
736+
737+
- selectors for unimplemented cheat code functions.
738+
739+
```k
740+
rule selector ( "sign(uint256,bytes32)" ) => 3812747940
741+
rule selector ( "ffi(string[])" ) => 2299921511
742+
rule selector ( "setEnv(string,string)" ) => 1029252078
743+
rule selector ( "envBool(string)" ) => 2127686781
744+
rule selector ( "envUint(string)" ) => 3247934751
745+
rule selector ( "envInt(string)" ) => 2301234273
746+
rule selector ( "envAddress(string)" ) => 890066623
747+
rule selector ( "envBytes32(string)" ) => 2543095874
748+
rule selector ( "envString(string)" ) => 4168600345
749+
rule selector ( "envBytes(string)" ) => 1299951366
750+
rule selector ( "envBool(string,string)" ) => 2863521455
751+
rule selector ( "envUint(string,string)" ) => 4091461785
752+
rule selector ( "envInt(string,string)" ) => 1108873552
753+
rule selector ( "envAddress(string,string)" ) => 2905717242
754+
rule selector ( "envBytes32(string,string)" ) => 1525821889
755+
rule selector ( "envString(string,string)" ) => 347089865
756+
rule selector ( "envBytes(string,string)" ) => 3720504603
757+
rule selector ( "prank(address)" ) => 3395723175
758+
rule selector ( "startPrank(address)" ) => 105151830
759+
rule selector ( "prank(address,address)" ) => 1206193358
760+
rule selector ( "startPrank(address,address)" ) => 1169514616
761+
rule selector ( "stopPrank()" ) => 2428830011
762+
rule selector ( "expectRevert(bytes)" ) => 4069379763
763+
rule selector ( "expectRevert(bytes4)" ) => 3273568480
764+
rule selector ( "expectRevert()" ) => 4102309908
765+
rule selector ( "record()" ) => 644673801
766+
rule selector ( "accesses(address)" ) => 1706857601
767+
rule selector ( "expectEmit(bool,bool,bool,bool)" ) => 1226622914
768+
rule selector ( "expectEmit(bool,bool,bool,bool,address)" ) => 2176505587
769+
rule selector ( "mockCall(address,bytes calldata,bytes)" ) => 378193464
770+
rule selector ( "mockCall(address,uint256,bytes,bytes)" ) => 2168494993
771+
rule selector ( "clearMockedCalls()" ) => 1071599125
772+
rule selector ( "expectCall(address,bytes)" ) => 3177903156
773+
rule selector ( "expectCall(address,uint256,bytes)" ) => 4077681571
774+
rule selector ( "getCode(string)" ) => 2367473957
775+
rule selector ( "broadcast()" ) => 2949218368
776+
rule selector ( "broadcast(address)" ) => 3868601563
777+
rule selector ( "startBroadcast()" ) => 2142579071
778+
rule selector ( "startBroadcast(address)" ) => 2146183821
779+
rule selector ( "stopBroadcast()" ) => 1995103542
780+
rule selector ( "readFile(string)" ) => 1626979089
781+
rule selector ( "readLine(string)" ) => 1895126824
782+
rule selector ( "writeFile(string,string)" ) => 2306738839
783+
rule selector ( "writeLine(string,string)" ) => 1637714303
784+
rule selector ( "closeFile(string)" ) => 1220748319
785+
rule selector ( "removeFile(string)" ) => 4054835277
786+
rule selector ( "toString(address)" ) => 1456103998
787+
rule selector ( "toString(bytes)" ) => 1907020045
788+
rule selector ( "toString(bytes32)" ) => 2971277800
789+
rule selector ( "toString(bool)" ) => 1910302682
790+
rule selector ( "toString(uint256)" ) => 1761649582
791+
rule selector ( "toString(int256)" ) => 2736964622
792+
rule selector ( "recordLogs()" ) => 1101999954
793+
rule selector ( "getRecordedLogs()" ) => 420828068
794+
rule selector ( "snapshot()" ) => 2534502746
795+
rule selector ( "revertTo(uint256)" ) => 1155002532
796+
rule selector ( "createFork(string,uint256)" ) => 1805892139
797+
rule selector ( "createFork(string)" ) => 834286744
798+
rule selector ( "createSelectFork(string,uint256)" ) => 1911440973
799+
rule selector ( "createSelectFork(string)" ) => 2556952628
800+
rule selector ( "selectFork(uint256)" ) => 2663344167
801+
rule selector ( "activeFork()" ) => 789593890
802+
rule selector ( "rollFork(uint256)" ) => 3652973473
803+
rule selector ( "rollFork(uint256,uint256)" ) => 3612115876
804+
rule selector ( "rpcUrl(string)" ) => 2539285737
805+
rule selector ( "rpcUrls()" ) => 2824504344
806+
rule selector ( "deriveKey(string,uint32)" ) => 1646872971
807+
```
808+
727809
```k
728810
endmodule
729811
```

‎tests/foundry/exclude

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ AddrTest.testFail_addr_true
44
AssertTest.test_assert_false
55
AssertTest.testFail_assert_false
66
AssertTest.testFail_assert_true
7+
AssertTest.testFail_expect_revert
78
AssumeTest.test_assume_false
89
AssumeTest.testFail_assume_false
910
AssumeTest.testFail_assume_true

‎tests/foundry/foundry.k.check.expected

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3169,18 +3169,59 @@ module ASSERTTEST-BIN-RUNTIME
31693169

31703170

31713171

3172+
syntax Field ::= AssertTestField
3173+
3174+
syntax AssertTestField ::= "IS_TEST" [symbol(), klabel(field_AssertTest_IS_TEST)]
3175+
3176+
syntax AssertTestField ::= "_failed" [symbol(), klabel(field_AssertTest__failed)]
3177+
3178+
syntax AssertTestField ::= "IS_SCRIPT" [symbol(), klabel(field_AssertTest_IS_SCRIPT)]
3179+
3180+
syntax AssertTestField ::= "stdstore" [symbol(), klabel(field_AssertTest_stdstore)]
3181+
3182+
rule ( #loc ( AssertTest . IS_TEST ) => 0 )
3183+
3184+
3185+
rule ( #loc ( AssertTest . _failed ) => 0 )
3186+
3187+
3188+
rule ( #loc ( AssertTest . IS_SCRIPT ) => 0 )
3189+
3190+
3191+
rule ( #loc ( AssertTest . stdstore ) => 1 )
3192+
3193+
31723194
syntax ByteArray ::= AssertTestContract "." AssertTestMethod [function(), symbol(), klabel(method_AssertTest)]
31733195

3196+
syntax AssertTestMethod ::= "IS_SCRIPT" "(" ")" [symbol(), klabel(method_AssertTest_IS_SCRIPT)]
3197+
3198+
syntax AssertTestMethod ::= "IS_TEST" "(" ")" [symbol(), klabel(method_AssertTest_IS_TEST)]
3199+
3200+
syntax AssertTestMethod ::= "failed" "(" ")" [symbol(), klabel(method_AssertTest_failed)]
3201+
31743202
syntax AssertTestMethod ::= "setUp" "(" ")" [symbol(), klabel(method_AssertTest_setUp)]
31753203

31763204
syntax AssertTestMethod ::= "testFail_assert_false" "(" ")" [symbol(), klabel(method_AssertTest_testFail_assert_false)]
31773205

31783206
syntax AssertTestMethod ::= "testFail_assert_true" "(" ")" [symbol(), klabel(method_AssertTest_testFail_assert_true)]
31793207

3208+
syntax AssertTestMethod ::= "testFail_expect_revert" "(" ")" [symbol(), klabel(method_AssertTest_testFail_expect_revert)]
3209+
31803210
syntax AssertTestMethod ::= "test_assert_false" "(" ")" [symbol(), klabel(method_AssertTest_test_assert_false)]
31813211

31823212
syntax AssertTestMethod ::= "test_assert_true" "(" ")" [symbol(), klabel(method_AssertTest_test_assert_true)]
31833213

3214+
syntax AssertTestMethod ::= "vm" "(" ")" [symbol(), klabel(method_AssertTest_vm)]
3215+
3216+
rule ( AssertTest . IS_SCRIPT ( ) => #abiCallData ( "IS_SCRIPT" , .TypedArgs ) )
3217+
3218+
3219+
rule ( AssertTest . IS_TEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) )
3220+
3221+
3222+
rule ( AssertTest . failed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
3223+
3224+
31843225
rule ( AssertTest . setUp ( ) => #abiCallData ( "setUp" , .TypedArgs ) )
31853226

31863227

@@ -3190,12 +3231,27 @@ module ASSERTTEST-BIN-RUNTIME
31903231
rule ( AssertTest . testFail_assert_true ( ) => #abiCallData ( "testFail_assert_true" , .TypedArgs ) )
31913232

31923233

3234+
rule ( AssertTest . testFail_expect_revert ( ) => #abiCallData ( "testFail_expect_revert" , .TypedArgs ) )
3235+
3236+
31933237
rule ( AssertTest . test_assert_false ( ) => #abiCallData ( "test_assert_false" , .TypedArgs ) )
31943238

31953239

31963240
rule ( AssertTest . test_assert_true ( ) => #abiCallData ( "test_assert_true" , .TypedArgs ) )
31973241

31983242

3243+
rule ( AssertTest . vm ( ) => #abiCallData ( "vm" , .TypedArgs ) )
3244+
3245+
3246+
rule ( selector ( "IS_SCRIPT" ) => 4174167879 )
3247+
3248+
3249+
rule ( selector ( "IS_TEST" ) => 4202047188 )
3250+
3251+
3252+
rule ( selector ( "failed" ) => 3124842406 )
3253+
3254+
31993255
rule ( selector ( "setUp" ) => 177362148 )
32003256

32013257

@@ -3205,11 +3261,17 @@ module ASSERTTEST-BIN-RUNTIME
32053261
rule ( selector ( "testFail_assert_true" ) => 409427266 )
32063262

32073263

3264+
rule ( selector ( "testFail_expect_revert" ) => 709747105 )
3265+
3266+
32083267
rule ( selector ( "test_assert_false" ) => 1574882301 )
32093268

32103269

32113270
rule ( selector ( "test_assert_true" ) => 906863826 )
32123271

3272+
3273+
rule ( selector ( "vm" ) => 980845667 )
3274+
32133275

32143276
endmodule
32153277

‎tests/foundry/test/Simple.t.sol

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
// SPDX-License-Identifier: UNLICENSED
22
pragma solidity =0.8.13;
33

4-
contract AssertTest {
4+
import "forge-std/Test.sol";
5+
6+
contract AssertTest is Test {
57
function setUp() public {}
68

79
function test_assert_true() public pure {
@@ -17,6 +19,11 @@ contract AssertTest {
1719
}
1820

1921
function testFail_assert_false() public pure {
22+
assert(false);
23+
}
24+
25+
function testFail_expect_revert() public{
26+
vm.expectRevert();
2027
assert(false);
2128
}
2229
}

0 commit comments

Comments
 (0)