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 <devops@runtimeverification.com> Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>
runtimeverification · Jul 17, 2024 · 3cc4186 · 3cc4186
1 parent f7ee4d2
commit 3cc4186
Show file tree

Hide file tree

Showing 8 changed files with 56 additions and 47 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.356
+0.1.357
diff --git 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. <contact@runtimeverification.com>",

diff --git 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
@@ -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)" )
 ```
 

diff --git 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
@@ -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
@@ -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
@@ -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