Handling of Int in bind (#54)

* Added rule to handle Int in bind. * Added tests.
Pi-Squared-Inc · Oct 10, 2024 · d145b4b · d145b4b
1 parent 572158b
commit d145b4b
Show file tree

Hide file tree

Showing 7 changed files with 325 additions and 0 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/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, )
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		create(1, 0, 1724300000, SomeTokenCreate, ),
		txn(1, 2, 0, 1724300000, testSomeTokenCreate, )