From 3cc41861eff021107c1f4d931644cf5fae4e6946 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20V=C4=83caru?= <16517508+anvacaru@users.noreply.github.com> Date: Wed, 17 Jul 2024 15:42:13 +0300 Subject: [PATCH] Load correct account in allowChangesToStorage (#704) * load correct acct in allowChangesToStorage * Set Version: 0.1.356 * Set Version: 0.1.357 * contracts.k: update expected output --------- Co-authored-by: devops Co-authored-by: Palina Tolmach --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- src/kontrol/kdist/cheatcodes.md | 2 +- .../integration/test-data/foundry-prove-all | 1 + .../test-data/foundry-prove-skip-legacy | 1 + .../foundry/test/AllowChangesTest.t.sol | 49 +++++++++---------- .../test-data/show/contracts.k.expected | 44 ++++++++++------- 8 files changed, 56 insertions(+), 47 deletions(-) diff --git a/package/version b/package/version index bde4d3b9e..c1d7880d1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.356 +0.1.357 diff --git a/pyproject.toml b/pyproject.toml index 135e3c4b0..7cabdb093 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -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. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index ff5a5d4db..443ec4ab6 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.356' +VERSION: Final = '0.1.357' diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md index efc3f8be9..24d322bc6 100644 --- a/src/kontrol/kdist/cheatcodes.md +++ b/src/kontrol/kdist/cheatcodes.md @@ -875,7 +875,7 @@ function allowChangesToStorage(address,uint256) external; ```k rule [foundry.allowStorageSlotToAddress]: - #cheatcode_call SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #addStorageSlotToWhitelist { #asWord(#range(ARGS, 0, 32)) | #asWord(#range(ARGS, 32, 32)) } ... + #cheatcode_call SELECTOR ARGS => #loadAccount #asWord(#range(ARGS, 0, 32)) ~> #addStorageSlotToWhitelist { #asWord(#range(ARGS, 0, 32)) | #asWord(#range(ARGS, 32, 32)) } ... requires SELECTOR ==Int selector ( "allowChangesToStorage(address,uint256)" ) ``` diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all index 5c3fbc5e3..682d1ce25 100644 --- a/src/tests/integration/test-data/foundry-prove-all +++ b/src/tests/integration/test-data/foundry-prove-all @@ -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() diff --git a/src/tests/integration/test-data/foundry-prove-skip-legacy b/src/tests/integration/test-data/foundry-prove-skip-legacy index f4f594cb9..f43564508 100644 --- a/src/tests/integration/test-data/foundry-prove-skip-legacy +++ b/src/tests/integration/test-data/foundry-prove-skip-legacy @@ -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() diff --git a/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol b/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol index e8f8d66dc..918e5c68d 100644 --- a/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol +++ b/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol @@ -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); } } diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected index 20902939f..8aa84421d 100644 --- a/src/tests/integration/test-data/show/contracts.k.expected +++ b/src/tests/integration/test-data/show/contracts.k.expected @@ -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_")] @@ -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_")] @@ -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 ) ) @@ -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 ) ) @@ -501,6 +506,9 @@ module S2KtestZModAllowChangesTest-CONTRACT rule ( selector ( "kevm()" ) => 3601001590 ) + rule ( selector ( "setUp()" ) => 177362148 ) + + rule ( selector ( "targetArtifactSelectors()" ) => 1725540768 ) @@ -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 ) @@ -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