Current function cell (#32)

* Added cell that tracks current function Id. * Tests for the function name in new cell. * Updated ref outputs. * Removed contractInit. Removed KItem for Id update. * Updated reference outputs.
Pi-Squared-Inc · Sep 18, 2024 · cb5ae6b · cb5ae6b
1 parent 95f5df6
commit cb5ae6b
Show file tree

Hide file tree

Showing 26 changed files with 422 additions and 10 deletions.
diff --git a/src/expression.md b/src/expression.md
@@ -14,7 +14,8 @@ module SOLIDITY-EXPRESSION
        <this-type> TYPE => X </this-type>
        <env> E => .Map </env>
        <store> S => .Map </store>
-       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
+       <current-function> FUNC => constructor </current-function>
+       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE, FUNC)) </call-stack>
        <contract-id> X </contract-id>
        <contract-init> INIT </contract-init>
        <contract-fn-id> constructor </contract-fn-id>
@@ -39,7 +40,8 @@ module SOLIDITY-EXPRESSION
        <this-type> TYPE => X </this-type>
        <env> E => .Map </env>
        <store> S => .Map </store>
-       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
+       <current-function> FUNC => constructor </current-function>
+       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE, FUNC)) </call-stack>
        <contract-id> X </contract-id>
        <contract-init> INIT </contract-init>
        <live-contracts>
@@ -192,7 +194,8 @@ module SOLIDITY-EXPRESSION
        <this-type> TYPE => TYPE' </this-type>
        <env> E => .Map </env>
        <store> S => .Map </store>
-       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
+       <current-function> FUNC => F </current-function>
+       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE, FUNC)) </call-stack>
        <contract-id> TYPE' </contract-id>
        <contract-fn-id> F </contract-fn-id>
        <contract-fn-param-names> PARAMS </contract-fn-param-names>
@@ -217,7 +220,8 @@ module SOLIDITY-EXPRESSION
        <this-type> TYPE => TYPE' </this-type>
        <env> E => .Map </env>
        <store> S => .Map </store>
-       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
+       <current-function> FUNC => F </current-function>
+       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE, FUNC)) </call-stack>
        <contract-id> TYPE' </contract-id>
        <contract-fn-id> F </contract-fn-id>
        <contract-fn-payable> PAYABLE </contract-fn-payable>
@@ -234,7 +238,8 @@ module SOLIDITY-EXPRESSION
   rule <k> F:Id ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
        <env> E => .Map </env>
        <store> S </store>
-       <call-stack>... .List => ListItem(frame(K, E)) </call-stack>
+       <current-function> FUNC => F </current-function>
+       <call-stack>... .List => ListItem(frame(K, E, FUNC)) </call-stack>
        <this-type> TYPE </this-type>
        <contract-id> TYPE </contract-id>
        <contract-fn-id> F </contract-fn-id>

diff --git a/src/solidity.md b/src/solidity.md
@@ -70,6 +70,7 @@ module SOLIDITY-CONFIGURATION
         <this-type> Id </this-type>
         <env> .Map </env>
         <store> .Map </store>
+        <current-function> Id </current-function>
         <call-stack> .List </call-stack>
         <live-contracts>
           <live-contract multiplicity="*" type="Map">
@@ -164,9 +165,9 @@ module SOLIDITY-DATA
   rule isAggregateType(_) => false [owise]
 
   // external frame
-  syntax Frame ::= frame(continuation: K, env: Map, store: Map, from: MInt{160}, type: Id, value: MInt{256})
+  syntax Frame ::= frame(continuation: K, env: Map, store: Map, from: MInt{160}, type: Id, value: MInt{256}, func: Id)
   // internal frame
-                 | frame(continuation: K, env: Map)
+                 | frame(continuation: K, env: Map, func: Id)
   syntax Event ::= event(name: Id, args: TypedVals)
 
 endmodule

diff --git a/src/statement.md b/src/statement.md
@@ -19,7 +19,8 @@ module SOLIDITY-STATEMENT
        <this-type> _ => TYPE </this-type>
        <env> _ => E </env>
        <store> _ => S </store>
-       <call-stack>... ListItem(frame(K, E, S, FROM, TYPE, VALUE)) => .List </call-stack>
+       <current-function> _ => FUNC </current-function>
+       <call-stack>... ListItem(frame(K, E, S, FROM, TYPE, VALUE, FUNC)) => .List </call-stack>
 
   rule <k> return void ; ~> _ => void ~> K </k>
        <msg-sender> THIS => FROM </msg-sender>
@@ -28,14 +29,16 @@ module SOLIDITY-STATEMENT
        <this-type> _ => TYPE </this-type>
        <env> _ => E </env>
        <store> _ => S </store>
-       <call-stack>... ListItem(frame(K, E, S, FROM, TYPE, VALUE)) => .List </call-stack>
+       <current-function> _ => FUNC </current-function>
+       <call-stack>... ListItem(frame(K, E, S, FROM, TYPE, VALUE, FUNC)) => .List </call-stack>
 
   rule <k> return lv(I:Int, .List, T) ; => return v(L, T) ; ...</k>
        <store>... I |-> L ...</store>
 
   rule <k> return V:TypedVal ; ~> _ => V ~> K </k>
        <env> _ => E </env>
-       <call-stack>... ListItem(frame(K, E)) => .List </call-stack> [owise]
+       <current-function> _ => FUNC </current-function>
+       <call-stack>... ListItem(frame(K, E, FUNC)) => .List </call-stack> [owise]
 
   // variable declaration
   rule <k> LT:TypeName X:Id = v(V, RT) ; => .K ...</k>

diff --git a/src/transaction.md b/src/transaction.md
@@ -16,6 +16,7 @@ module SOLIDITY-TRANSACTION
        <this-type> _ => CTOR </this-type>
        <env> _ => .Map </env>
        <store> _ => .Map </store>
+       <current-function> _ => constructor </current-function>
        <contract-id> CTOR </contract-id>
        <contract-init> INIT </contract-init>
        <contract-fn-id> constructor </contract-fn-id>
@@ -42,6 +43,7 @@ module SOLIDITY-TRANSACTION
        <this-type> _ => CTOR </this-type>
        <env> _ => .Map </env>
        <store> _ => .Map </store>
+       <current-function> _ => constructor </current-function>
        <contract-id> CTOR </contract-id>
        <contract-init> INIT </contract-init>
        <live-contracts>
@@ -67,6 +69,7 @@ module SOLIDITY-TRANSACTION
        <this-type> _ => TYPE </this-type>
        <env> _ => .Map </env>
        <store> _ => .Map </store>
+       <current-function> _ => FUNC </current-function>
        <live-contracts>
          <contract-address> TO </contract-address>
          <contract-type> TYPE </contract-type>

diff --git a/test/regression/addliquidity.ref b/test/regression/addliquidity.ref
@@ -2356,6 +2356,9 @@
       3 |-> 0p256
       4 |-> 0p256
     </store>
+    <current-function>
+      testRouterAddLiquidity
+    </current-function>
     <call-stack>
       .List
     </call-stack>

diff --git a/test/regression/arithmetic.ref b/test/regression/arithmetic.ref
@@ -96,6 +96,9 @@
       6 |-> 2p8
       7 |-> 4p8
     </store>
+    <current-function>
+      constructor
+    </current-function>
     <call-stack>
       .List
     </call-stack>

diff --git a/test/regression/arraystestcontract.ref b/test/regression/arraystestcontract.ref
@@ -108,6 +108,9 @@
     <store>
       .Map
     </store>
+    <current-function>
+      constructor
+    </current-function>
     <call-stack>
       .List
     </call-stack>

diff --git a/test/regression/block.ref b/test/regression/block.ref
@@ -83,6 +83,9 @@
       0 |-> false
       1 |-> true
     </store>
+    <current-function>
+      constructor
+    </current-function>
     <call-stack>
       .List
     </call-stack>

diff --git a/test/regression/boolean.ref b/test/regression/boolean.ref
@@ -107,6 +107,9 @@
     <store>
       0 |-> false
     </store>
+    <current-function>
+      constructor
+    </current-function>
     <call-stack>
       .List
     </call-stack>

diff --git a/test/regression/contract.ref b/test/regression/contract.ref
@@ -352,6 +352,9 @@
       1 |-> 3p160
       2 |-> 4p160
     </store>
+    <current-function>
+      constructor
+    </current-function>
     <call-stack>
       .List
     </call-stack>

diff --git a/test/regression/emit.ref b/test/regression/emit.ref
@@ -100,6 +100,9 @@
     <store>
       .Map
     </store>
+    <current-function>
+      constructor
+    </current-function>
     <call-stack>
       .List
     </call-stack>

diff --git a/test/regression/eventtestcontract.ref b/test/regression/eventtestcontract.ref
@@ -228,6 +228,9 @@
     <store>
       .Map
     </store>
+    <current-function>
+      constructor
+    </current-function>
     <call-stack>
       .List
     </call-stack>

diff --git a/test/regression/for.ref b/test/regression/for.ref
@@ -85,6 +85,9 @@
       1 |-> 20p256
       2 |-> 10p256
     </store>
+    <current-function>
+      constructor
+    </current-function>
     <call-stack>
       .List
     </call-stack>

diff --git a/test/regression/funcnamefail.ref b/test/regression/funcnamefail.ref
@@ -0,0 +1,159 @@
+<solidity>
+  <k>
+    require ( v ( false , bool ) , "" , .TypedVals ) ~> #freezer_;_SOLIDITY-SYNTAX_ExpressionStatement_Expression0_ ( ) ~> return 2 ;  .Statements ~> return void ; ~> .K
+  </k>
+  <summarize>
+    false
+  </summarize>
+  <compile>
+    <current-body>
+      FuncNameFailTest
+    </current-body>
+    <ifaces>
+      .IfaceCellMap
+    </ifaces>
+    <contracts>
+      <contract>
+        <contract-id>
+          FuncNameFailTest
+        </contract-id>
+        <contract-state>
+          .Map
+        </contract-state>
+        <contract-init>
+          .List
+        </contract-init>
+        <contract-fns>
+          <contract-fn>
+            <contract-fn-id>
+              chaincall1
+            </contract-fn-id>
+            <contract-fn-visibility>
+              private
+            </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 ( uint256 )
+            </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 chaincall2 ( .TypedVals ) ;  .Statements
+            </contract-fn-body>
+          </contract-fn> <contract-fn>
+            <contract-fn-id>
+              chaincall2
+            </contract-fn-id>
+            <contract-fn-visibility>
+              private
+            </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 ( uint256 )
+            </contract-fn-return-types>
+            <contract-fn-return-names>
+              ListItem ( noId )
+            </contract-fn-return-names>
+            <contract-fn-payable>
+              false
+            </contract-fn-payable>
+            <contract-fn-body>
+              require ( false , "" , .TypedVals ) ;  return 2 ;  .Statements
+            </contract-fn-body>
+          </contract-fn> <contract-fn>
+            <contract-fn-id>
+              constructor
+            </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>
+              uint256 x = chaincall1 ( .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>
+      0p256
+    </block-timestamp>
+    <this>
+      2p160
+    </this>
+    <this-type>
+      FuncNameFailTest
+    </this-type>
+    <env>
+      .Map
+    </env>
+    <store>
+      .Map
+    </store>
+    <current-function>
+      chaincall2
+    </current-function>
+    <call-stack>
+      ListItem ( frame (... continuation: #freezer_=_;_SOLIDITY-SYNTAX_VariableDeclarationStatement_VariableDeclaration_Expression1_ ( uint256 x ~> .K ) ~> .Statements ~> .Transactions ~> .K , env: .Map , func: constructor ) )
+      ListItem ( frame (... continuation: #freezerreturn_;_SOLIDITY-SYNTAX_ReturnStatement_Expression0_ ( ) ~> .Statements ~> return void ; ~> .K , env: .Map , func: chaincall1 ) )
+    </call-stack>
+    <live-contracts>
+      <live-contract>
+        <contract-address>
+          2p160
+        </contract-address>
+        <contract-type>
+          FuncNameFailTest
+        </contract-type>
+        <contract-storage>
+          .Map
+        </contract-storage>
+      </live-contract>
+    </live-contracts>
+    <next-address>
+      3p160
+    </next-address>
+  </exec>
+</solidity>
diff --git a/test/regression/funcnamefail.sol b/test/regression/funcnamefail.sol
@@ -0,0 +1,17 @@
+pragma solidity ^0.8.24;
+
+contract FuncNameFailTest {
+
+    function chaincall2() private returns (uint) {
+        require(false, "");
+        return 2;
+    }
+
+    function chaincall1() private returns (uint) {
+       return chaincall2();
+    }
+
+    constructor() {
+      uint x = chaincall1();
+    }
+}
diff --git a/test/regression/funcnamefail.txn b/test/regression/funcnamefail.txn
@@ -0,0 +1 @@
+create(1, 0, 0, FuncNameFailTest, )