Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Load correct account in allowChangesToStorage #704

Merged
merged 5 commits into from
Jul 17, 2024
Merged

Load correct account in allowChangesToStorage #704

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
52dc96b
load correct acct in allowChangesToStorage
anvacaru Jul 17, 2024
d98cbbf
Set Version: 0.1.356
Jul 17, 2024
9f57828
Merge branch 'master' into whitelist_storage_fix
palinatolmach Jul 17, 2024
08fbefe
Set Version: 0.1.357
Jul 17, 2024
5082c37
contracts.k: update expected output
anvacaru Jul 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package/version
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.356
0.1.357
2 changes: 1 addition & 1 deletion pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kontrol"
version = "0.1.356"
version = "0.1.357"
description = "Foundry integration for KEVM"
authors = [
"Runtime Verification, Inc. <contact@runtimeverification.com>",
Expand Down
2 changes: 1 addition & 1 deletion src/kontrol/__init__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@
if TYPE_CHECKING:
from typing import Final

VERSION: Final = '0.1.356'
VERSION: Final = '0.1.357'
2 changes: 1 addition & 1 deletion src/kontrol/kdist/cheatcodes.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -875,7 +875,7 @@ function allowChangesToStorage(address,uint256) external;

```k
rule [foundry.allowStorageSlotToAddress]:
<k> #cheatcode_call SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #addStorageSlotToWhitelist { #asWord(#range(ARGS, 0, 32)) | #asWord(#range(ARGS, 32, 32)) } ... </k>
<k> #cheatcode_call SELECTOR ARGS => #loadAccount #asWord(#range(ARGS, 0, 32)) ~> #addStorageSlotToWhitelist { #asWord(#range(ARGS, 0, 32)) | #asWord(#range(ARGS, 32, 32)) } ... </k>
requires SELECTOR ==Int selector ( "allowChangesToStorage(address,uint256)" )
```

Expand Down
1 change: 1 addition & 0 deletions src/tests/integration/test-data/foundry-prove-all
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ AddrTest.test_notBuiltinAddress_concrete()
AddrTest.test_notBuiltinAddress_symbolic(address)
AllowChangesTest.test()
AllowChangesTest.testAllow()
AllowChangesTest.testAllowSymbolic()
AllowChangesTest.testAllow_fail()
AllowChangesTest.testFailAllowCallsToAddress()
AllowChangesTest.testFailAllowChangesToStorage()
Expand Down
1 change: 1 addition & 0 deletions src/tests/integration/test-data/foundry-prove-skip-legacy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ AddrTest.testFail_addr_true()
AddrTest.test_notBuiltinAddress_symbolic(address)
AllowChangesTest.test()
AllowChangesTest.testAllow()
AllowChangesTest.testAllowSymbolic()
AllowChangesTest.testAllow_fail()
AllowChangesTest.testFailAllowCallsToAddress()
AllowChangesTest.testFailAllowChangesToStorage()
Expand Down
49 changes: 24 additions & 25 deletions src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,60 +5,59 @@ import "forge-std/Test.sol";
import "kontrol-cheatcodes/KontrolCheats.sol";

contract ValueStore {
uint256 public value1;
uint256 public value2;
uint256 public slot0;
uint256 public slot1;

function changeValue1(uint256 newValue) public {
value1 = newValue;
function changeSlot0(uint256 newValue) public {
slot0 = newValue;
}

function changeValue2(uint256 newValue) public {
value2 = newValue;
function changeSlot1(uint256 newValue) public {
slot1 = newValue;
}
}

contract AllowChangesTest is Test, KontrolCheats {
function test() public {
assertTrue(true);
}
ValueStore canChange;
ValueStore cannotChange;

function testAllow() public {
ValueStore canChange = new ValueStore();
ValueStore cannotChange = new ValueStore();
function setUp() public {
canChange = new ValueStore();
cannotChange = new ValueStore();
}

function testAllow() public {
kevm.allowCallsToAddress(address(canChange));
kevm.allowChangesToStorage(address(canChange), 0);

canChange.changeValue1(85);
canChange.changeSlot0(85);
}

function testFailAllowCallsToAddress() public {
ValueStore canChange = new ValueStore();
ValueStore cannotChange = new ValueStore();
function testAllowSymbolic() public {
kevm.symbolicStorage(address(canChange));

kevm.allowCallsToAddress(address(canChange));
kevm.allowChangesToStorage(address(canChange), 0);
canChange.changeSlot0(85);
}
function testFailAllowCallsToAddress() public {
kevm.allowCallsToAddress(address(canChange));
kevm.allowChangesToStorage(address(canChange), 0);

cannotChange.changeValue1(10245);
cannotChange.changeSlot0(10245);
}

function testFailAllowChangesToStorage() public {
ValueStore canChange = new ValueStore();
ValueStore cannotChange = new ValueStore();

kevm.allowCallsToAddress(address(canChange));
kevm.allowChangesToStorage(address(canChange), 0);

canChange.changeValue2(23452);
canChange.changeSlot1(23452);
}

function testAllow_fail() public {
ValueStore canChange = new ValueStore();
ValueStore cannotChange = new ValueStore();

kevm.allowCallsToAddress(address(canChange));
kevm.allowChangesToStorage(address(canChange), 0);

canChange.changeValue2(234521);
canChange.changeSlot1(234521);
}
}
44 changes: 26 additions & 18 deletions src/tests/integration/test-data/show/contracts.k.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -415,6 +415,8 @@ module S2KtestZModAllowChangesTest-CONTRACT

syntax S2KtestZModAllowChangesTestMethod ::= "S2Kkevm" "(" ")" [symbol("method_test%AllowChangesTest_S2Kkevm_")]

syntax S2KtestZModAllowChangesTestMethod ::= "S2KsetUp" "(" ")" [symbol("method_test%AllowChangesTest_S2KsetUp_")]

syntax S2KtestZModAllowChangesTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol("method_test%AllowChangesTest_S2KtargetArtifactSelectors_")]

syntax S2KtestZModAllowChangesTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol("method_test%AllowChangesTest_S2KtargetArtifacts_")]
Expand All @@ -425,10 +427,10 @@ module S2KtestZModAllowChangesTest-CONTRACT

syntax S2KtestZModAllowChangesTestMethod ::= "S2KtargetSenders" "(" ")" [symbol("method_test%AllowChangesTest_S2KtargetSenders_")]

syntax S2KtestZModAllowChangesTestMethod ::= "S2Ktest" "(" ")" [symbol("method_test%AllowChangesTest_S2Ktest_")]

syntax S2KtestZModAllowChangesTestMethod ::= "S2KtestAllow" "(" ")" [symbol("method_test%AllowChangesTest_S2KtestAllow_")]

syntax S2KtestZModAllowChangesTestMethod ::= "S2KtestAllowSymbolic" "(" ")" [symbol("method_test%AllowChangesTest_S2KtestAllowSymbolic_")]

syntax S2KtestZModAllowChangesTestMethod ::= "S2KtestAllowZUndfail" "(" ")" [symbol("method_test%AllowChangesTest_S2KtestAllowZUndfail_")]

syntax S2KtestZModAllowChangesTestMethod ::= "S2KtestFailAllowCallsToAddress" "(" ")" [symbol("method_test%AllowChangesTest_S2KtestFailAllowCallsToAddress_")]
Expand All @@ -453,6 +455,9 @@ module S2KtestZModAllowChangesTest-CONTRACT
rule ( S2KtestZModAllowChangesTest . S2Kkevm ( ) => #abiCallData ( "kevm" , .TypedArgs ) )


rule ( S2KtestZModAllowChangesTest . S2KsetUp ( ) => #abiCallData ( "setUp" , .TypedArgs ) )


rule ( S2KtestZModAllowChangesTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) )


Expand All @@ -468,10 +473,10 @@ module S2KtestZModAllowChangesTest-CONTRACT
rule ( S2KtestZModAllowChangesTest . S2KtargetSenders ( ) => #abiCallData ( "targetSenders" , .TypedArgs ) )


rule ( S2KtestZModAllowChangesTest . S2Ktest ( ) => #abiCallData ( "test" , .TypedArgs ) )
rule ( S2KtestZModAllowChangesTest . S2KtestAllow ( ) => #abiCallData ( "testAllow" , .TypedArgs ) )


rule ( S2KtestZModAllowChangesTest . S2KtestAllow ( ) => #abiCallData ( "testAllow" , .TypedArgs ) )
rule ( S2KtestZModAllowChangesTest . S2KtestAllowSymbolic ( ) => #abiCallData ( "testAllowSymbolic" , .TypedArgs ) )


rule ( S2KtestZModAllowChangesTest . S2KtestAllowZUndfail ( ) => #abiCallData ( "testAllow_fail" , .TypedArgs ) )
Expand Down Expand Up @@ -501,6 +506,9 @@ module S2KtestZModAllowChangesTest-CONTRACT
rule ( selector ( "kevm()" ) => 3601001590 )


rule ( selector ( "setUp()" ) => 177362148 )


rule ( selector ( "targetArtifactSelectors()" ) => 1725540768 )


Expand All @@ -516,10 +524,10 @@ module S2KtestZModAllowChangesTest-CONTRACT
rule ( selector ( "targetSenders()" ) => 1046363171 )


rule ( selector ( "test()" ) => 4171824493 )
rule ( selector ( "testAllow()" ) => 3693132891 )


rule ( selector ( "testAllow()" ) => 3693132891 )
rule ( selector ( "testAllowSymbolic()" ) => 4094715175 )


rule ( selector ( "testAllow_fail()" ) => 4129570225 )
Expand All @@ -542,38 +550,38 @@ module S2KtestZModValueStore-CONTRACT

syntax Bytes ::= S2KtestZModValueStoreContract "." S2KtestZModValueStoreMethod [function, symbol("method_test%ValueStore")]

syntax S2KtestZModValueStoreMethod ::= "S2KchangeValue1" "(" Int ":" "uint256" ")" [symbol("method_test%ValueStore_S2KchangeValue1_uint256")]
syntax S2KtestZModValueStoreMethod ::= "S2KchangeSlot0" "(" Int ":" "uint256" ")" [symbol("method_test%ValueStore_S2KchangeSlot0_uint256")]

syntax S2KtestZModValueStoreMethod ::= "S2KchangeValue2" "(" Int ":" "uint256" ")" [symbol("method_test%ValueStore_S2KchangeValue2_uint256")]
syntax S2KtestZModValueStoreMethod ::= "S2KchangeSlot1" "(" Int ":" "uint256" ")" [symbol("method_test%ValueStore_S2KchangeSlot1_uint256")]

syntax S2KtestZModValueStoreMethod ::= "S2Kvalue1" "(" ")" [symbol("method_test%ValueStore_S2Kvalue1_")]
syntax S2KtestZModValueStoreMethod ::= "S2Kslot0" "(" ")" [symbol("method_test%ValueStore_S2Kslot0_")]

syntax S2KtestZModValueStoreMethod ::= "S2Kvalue2" "(" ")" [symbol("method_test%ValueStore_S2Kvalue2_")]
syntax S2KtestZModValueStoreMethod ::= "S2Kslot1" "(" ")" [symbol("method_test%ValueStore_S2Kslot1_")]

rule ( S2KtestZModValueStore . S2KchangeValue1 ( V0_newValue : uint256 ) => #abiCallData ( "changeValue1" , ( #uint256 ( V0_newValue ) , .TypedArgs ) ) )
rule ( S2KtestZModValueStore . S2KchangeSlot0 ( V0_newValue : uint256 ) => #abiCallData ( "changeSlot0" , ( #uint256 ( V0_newValue ) , .TypedArgs ) ) )
ensures #rangeUInt ( 256 , V0_newValue )


rule ( S2KtestZModValueStore . S2KchangeValue2 ( V0_newValue : uint256 ) => #abiCallData ( "changeValue2" , ( #uint256 ( V0_newValue ) , .TypedArgs ) ) )
rule ( S2KtestZModValueStore . S2KchangeSlot1 ( V0_newValue : uint256 ) => #abiCallData ( "changeSlot1" , ( #uint256 ( V0_newValue ) , .TypedArgs ) ) )
ensures #rangeUInt ( 256 , V0_newValue )


rule ( S2KtestZModValueStore . S2Kvalue1 ( ) => #abiCallData ( "value1" , .TypedArgs ) )
rule ( S2KtestZModValueStore . S2Kslot0 ( ) => #abiCallData ( "slot0" , .TypedArgs ) )


rule ( S2KtestZModValueStore . S2Kvalue2 ( ) => #abiCallData ( "value2" , .TypedArgs ) )
rule ( S2KtestZModValueStore . S2Kslot1 ( ) => #abiCallData ( "slot1" , .TypedArgs ) )


rule ( selector ( "changeValue1(uint256)" ) => 1634438405 )
rule ( selector ( "changeSlot0(uint256)" ) => 1508657921 )


rule ( selector ( "changeValue2(uint256)" ) => 367426214 )
rule ( selector ( "changeSlot1(uint256)" ) => 3545667351 )


rule ( selector ( "value1()" ) => 808665403 )
rule ( selector ( "slot0()" ) => 944818109 )


rule ( selector ( "value2()" ) => 1563665023 )
rule ( selector ( "slot1()" ) => 524647605 )


endmodule
Expand Down
Loading