Merge branch 'main' into swap-summary-cont

Pi-Squared-Inc · Oct 10, 2024 · f1ace85 · f1ace85
2 parents 8387d33 + 5beaa76
commit f1ace85
Show file tree

Hide file tree

Showing 9 changed files with 327 additions and 15 deletions.
diff --git a/src/expression.md b/src/expression.md
@@ -386,6 +386,9 @@ module SOLIDITY-EXPRESSION
   rule <k> bind(STORE, ListItem(X:Id) PARAMS, ListItem(LT:TypeName) TYPES, v(V:Value, RT:TypeName), ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2) ...</k>
        <env> E => E [ X <- var(size(S), LT) ] </env>
        <store> S => S ListItem(convert(V, RT, LT)) </store>
+  rule <k> bind(STORE, ListItem(X:Id) PARAMS, ListItem(LT:TypeName) TYPES, N:Int, ARGS, L1:List, L2:List) => bind(STORE, PARAMS, TYPES, ARGS, L1, L2) ...</k>
+       <env> E => E [ X <- var(size(S), LT) ] </env>
+       <store> S => S ListItem(convert(N, LT)) </store>
   rule <k> bind(STORE, .List, .List, .CallArgumentList, ListItem(LT:TypeName) TYPES, ListItem(X:Id) NAMES) => bind(STORE, .List, .List, .CallArgumentList, TYPES, NAMES) ...</k>
        <env> E => E [ X <- var(size(S), LT) ] </env>
        <store> S => S ListItem(default(LT)) </store>

diff --git a/src/statement.md b/src/statement.md
@@ -82,8 +82,9 @@ module SOLIDITY-STATEMENT
        <env> E </env>
 
   syntax KItem ::= restoreEnv(Map)
+  rule <k> restoreEnv( _:Map ) ~> .Statements ~> restoreEnv( E:Map ) => restoreEnv(E) ...</k>
   rule <k> restoreEnv(E) => .K ...</k>
-       <env> _ => E </env>
+       <env> _ => E </env> [owise]
 
   // while statement
   rule while (Cond) Body => if (Cond) {Body while(Cond) Body} else {.Statements}

diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
@@ -2743,13 +2743,6 @@ module SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY
        </store>
        <current-function> uniswapV2LibraryGetAmountsOut </current-function> [priority(40)]
 
-  // Skip environment updates when not needed.
-  // These occur due to the multiple block statements, introduced by the if
-  // statement that the while rewrites to.
-  rule <k> restoreEnv( _:Map ) ~> .Statements ~> restoreEnv( E:Map ) => restoreEnv(E) ...</k>
-       <summarize> true </summarize>
-       <current-function> uniswapV2LibraryGetAmountsOut </current-function> [priority(40)]
-
   // End of function: final environment restoration until return from getAmountsOut to caller
   rule <k> restoreEnv ( _:Map (amounts |-> var(Ia, uint256 [])) ) ~> .Statements ~> return amounts ; ~> .K => v ( Va , uint256 [] ) ~> K </k>
        <summarize> true </summarize>
@@ -3595,13 +3588,6 @@ module SOLIDITY-MATHSQRT-SUMMARY
        </store>
        <current-function> mathSqrt </current-function> [priority(40)]
 
-  // Skip environment updates when not needed.
-  // These occur due to the multiple block statements, introduced by the if
-  // statement that the while rewrites to.
-  rule <k> restoreEnv( _:Map ) ~> .Statements ~> restoreEnv( E:Map ) => restoreEnv(E) ...</k>
-       <summarize> true </summarize>
-       <current-function> mathSqrt </current-function> [priority(40)]
-
   // End of function: final environment restoration to return to caller
   rule <k> restoreEnv ( _:Map (z |-> var(Iz, uint256)) ) ~> .Statements ~> return z ; ~> .K => v (Vz, uint256) ~> K </k>
        <summarize> true </summarize>

diff --git a/test/regression/createwint1.ref b/test/regression/createwint1.ref
@@ -0,0 +1,108 @@
+<solidity>
+  <k>
+    .K
+  </k>
+  <summarize>
+    false
+  </summarize>
+  <compile>
+    <current-body>
+      SomeToken
+    </current-body>
+    <ifaces>
+      .IfaceCellMap
+    </ifaces>
+    <contracts>
+      <contract>
+        <contract-id>
+          SomeToken
+        </contract-id>
+        <contract-state>
+          .Map
+        </contract-state>
+        <contract-init>
+          .List
+        </contract-init>
+        <contract-fns>
+          <contract-fn>
+            <contract-fn-id>
+              constructor
+            </contract-fn-id>
+            <contract-fn-visibility>
+              public
+            </contract-fn-visibility>
+            <contract-fn-arg-types>
+              ListItem ( uint256 )
+            </contract-fn-arg-types>
+            <contract-fn-param-names>
+              ListItem ( init_supply )
+            </contract-fn-param-names>
+            <contract-fn-return-types>
+              .List
+            </contract-fn-return-types>
+            <contract-fn-return-names>
+              .List
+            </contract-fn-return-names>
+            <contract-fn-payable>
+              false
+            </contract-fn-payable>
+            <contract-fn-body>
+              .Statements
+            </contract-fn-body>
+          </contract-fn>
+        </contract-fns>
+        <contract-events>
+          .ContractEventCellMap
+        </contract-events>
+      </contract>
+    </contracts>
+  </compile>
+  <exec>
+    <msg-sender>
+      1p160
+    </msg-sender>
+    <msg-value>
+      0p256
+    </msg-value>
+    <tx-origin>
+      1p160
+    </tx-origin>
+    <block-timestamp>
+      1724300000p256
+    </block-timestamp>
+    <this>
+      2p160
+    </this>
+    <this-type>
+      SomeToken
+    </this-type>
+    <env>
+      init_supply |-> var ( 0 , uint256 )
+    </env>
+    <store>
+      ListItem ( 1000000000000000000p256 )
+    </store>
+    <current-function>
+      constructor
+    </current-function>
+    <call-stack>
+      .List
+    </call-stack>
+    <live-contracts>
+      <live-contract>
+        <contract-address>
+          2p160
+        </contract-address>
+        <contract-type>
+          SomeToken
+        </contract-type>
+        <contract-storage>
+          .Map
+        </contract-storage>
+      </live-contract>
+    </live-contracts>
+    <next-address>
+      3p160
+    </next-address>
+  </exec>
+</solidity>
diff --git a/test/regression/createwint1.sol b/test/regression/createwint1.sol
@@ -0,0 +1,8 @@
+pragma solidity ^0.8.24;
+
+contract SomeToken {
+
+    constructor(uint256 init_supply) {
+    }
+
+}
diff --git a/test/regression/createwint1.txn b/test/regression/createwint1.txn
@@ -0,0 +1 @@
+create(1, 0, 1724300000, SomeToken, 1e18)
diff --git a/test/regression/createwint2.ref b/test/regression/createwint2.ref
@@ -0,0 +1,184 @@
+<solidity>
+  <k>
+    .K
+  </k>
+  <summarize>
+    false
+  </summarize>
+  <compile>
+    <current-body>
+      SomeTokenCreate
+    </current-body>
+    <ifaces>
+      .IfaceCellMap
+    </ifaces>
+    <contracts>
+      <contract>
+        <contract-id>
+          SomeToken
+        </contract-id>
+        <contract-state>
+          .Map
+        </contract-state>
+        <contract-init>
+          .List
+        </contract-init>
+        <contract-fns>
+          <contract-fn>
+            <contract-fn-id>
+              constructor
+            </contract-fn-id>
+            <contract-fn-visibility>
+              public
+            </contract-fn-visibility>
+            <contract-fn-arg-types>
+              ListItem ( uint256 )
+            </contract-fn-arg-types>
+            <contract-fn-param-names>
+              ListItem ( init_supply )
+            </contract-fn-param-names>
+            <contract-fn-return-types>
+              .List
+            </contract-fn-return-types>
+            <contract-fn-return-names>
+              .List
+            </contract-fn-return-names>
+            <contract-fn-payable>
+              false
+            </contract-fn-payable>
+            <contract-fn-body>
+              .Statements
+            </contract-fn-body>
+          </contract-fn>
+        </contract-fns>
+        <contract-events>
+          .ContractEventCellMap
+        </contract-events>
+      </contract> <contract>
+        <contract-id>
+          SomeTokenCreate
+        </contract-id>
+        <contract-state>
+          _someToken |-> SomeToken
+        </contract-state>
+        <contract-init>
+          .List
+        </contract-init>
+        <contract-fns>
+          <contract-fn>
+            <contract-fn-id>
+              _someToken
+            </contract-fn-id>
+            <contract-fn-visibility>
+              public
+            </contract-fn-visibility>
+            <contract-fn-arg-types>
+              .List
+            </contract-fn-arg-types>
+            <contract-fn-param-names>
+              .List
+            </contract-fn-param-names>
+            <contract-fn-return-types>
+              ListItem ( SomeToken )
+            </contract-fn-return-types>
+            <contract-fn-return-names>
+              ListItem ( noId )
+            </contract-fn-return-names>
+            <contract-fn-payable>
+              false
+            </contract-fn-payable>
+            <contract-fn-body>
+              return _someToken ;  .Statements
+            </contract-fn-body>
+          </contract-fn> <contract-fn>
+            <contract-fn-id>
+              testSomeTokenCreate
+            </contract-fn-id>
+            <contract-fn-visibility>
+              public
+            </contract-fn-visibility>
+            <contract-fn-arg-types>
+              .List
+            </contract-fn-arg-types>
+            <contract-fn-param-names>
+              .List
+            </contract-fn-param-names>
+            <contract-fn-return-types>
+              .List
+            </contract-fn-return-types>
+            <contract-fn-return-names>
+              .List
+            </contract-fn-return-names>
+            <contract-fn-payable>
+              false
+            </contract-fn-payable>
+            <contract-fn-body>
+              _someToken = new SomeToken ( 1e18 , .TypedVals ) ;  .Statements
+            </contract-fn-body>
+          </contract-fn>
+        </contract-fns>
+        <contract-events>
+          .ContractEventCellMap
+        </contract-events>
+      </contract>
+    </contracts>
+  </compile>
+  <exec>
+    <msg-sender>
+      1p160
+    </msg-sender>
+    <msg-value>
+      0p256
+    </msg-value>
+    <tx-origin>
+      1p160
+    </tx-origin>
+    <block-timestamp>
+      1724300000p256
+    </block-timestamp>
+    <this>
+      2p160
+    </this>
+    <this-type>
+      SomeTokenCreate
+    </this-type>
+    <env>
+      .Map
+    </env>
+    <store>
+      .List
+    </store>
+    <current-function>
+      testSomeTokenCreate
+    </current-function>
+    <call-stack>
+      .List
+    </call-stack>
+    <live-contracts>
+      <live-contract>
+        <contract-address>
+          2p160
+        </contract-address>
+        <contract-type>
+          SomeTokenCreate
+        </contract-type>
+        <contract-storage>
+          _someToken |-> 3p160
+        </contract-storage>
+      </live-contract> <live-contract>
+        <contract-address>
+          3p160
+        </contract-address>
+        <contract-type>
+          SomeToken
+        </contract-type>
+        <contract-storage>
+          .Map
+        </contract-storage>
+      </live-contract>
+    </live-contracts>
+    <next-address>
+      4p160
+    </next-address>
+  </exec>
+</solidity>
diff --git a/test/regression/createwint2.sol b/test/regression/createwint2.sol
@@ -0,0 +1,19 @@
+pragma solidity ^0.8.24;
+
+contract SomeToken {
+
+    constructor(uint256 init_supply) {
+    }
+
+}
+
+contract SomeTokenCreate {
+
+    SomeToken public _someToken;
+
+    function testSomeTokenCreate() public {
+        // Create SomeToken
+        _someToken = new SomeToken(1e18);
+    }
+
+}
diff --git a/test/regression/createwint2.txn b/test/regression/createwint2.txn
@@ -0,0 +1,2 @@
+create(1, 0, 1724300000, SomeTokenCreate, ),
+txn(1, 2, 0, 1724300000, testSomeTokenCreate, )