Emit statements (#15)

* emit statement * add test * update tests
Pi-Squared-Inc · Aug 26, 2024 · d0de1dc · d0de1dc
1 parent 1ef0eea
commit d0de1dc
Show file tree

Hide file tree

Showing 11 changed files with 149 additions and 1 deletion.
diff --git a/src/solidity-syntax.md b/src/solidity-syntax.md
@@ -191,7 +191,7 @@ Following is a list of supported statements.
     syntax ConditionStatement ::= ExpressionStatement | ";"
     syntax PostLoopStatement ::= Expression | ""
 
-    syntax EmitStatement ::= "emit" Expression "(" CallArgumentList ")" ";"
+    syntax EmitStatement ::= "emit" Expression "(" CallArgumentList ")" ";" [strict(2)]
 
     syntax ReturnStatement ::= "return" ";"
                             | "return" Expression ";" [strict]

diff --git a/src/solidity.md b/src/solidity.md
@@ -72,6 +72,7 @@ module SOLIDITY-CONFIGURATION
             <contract-storage> .Map </contract-storage>
           </live-contract>
         </live-contracts>
+        <events> .List </events>
         <next-address> 2p160 </next-address>
       </exec>
     </solidity>
@@ -152,6 +153,7 @@ module SOLIDITY-DATA
   rule getIndexed(_, Ep:EventParameters, N:Int) => getIndexed(Ep, N +Int 1) [owise]
 
   syntax Frame ::= frame(continuation: K, env: Map, store: Map, from: MInt{160}, type: Id)
+  syntax Event ::= event(name: Id, args: TypedVals)
 
 endmodule
 ```

diff --git a/src/statement.md b/src/statement.md
@@ -26,4 +26,9 @@ module SOLIDITY-STATEMENT
        <env> E => E [ X <- var(!I:Int, LT) ] </env>
        <store> S => S [ !I <- convert(Number2Int(N), LT) ] </store>
 
+  // emit statement
+  rule <k> emit X:Id ( ARGS ) ; => .K ...</k>
+       <events>... .List => ListItem(event(X, ARGS)) </events>
+    requires isKResult(ARGS)
+
 endmodule
diff --git a/test/regression/arraystestcontract.ref b/test/regression/arraystestcontract.ref
@@ -110,6 +110,9 @@
         </contract-storage>
       </live-contract>
     </live-contracts>
+    <events>
+      .List
+    </events>
     <next-address>
       3p160
     </next-address>

diff --git a/test/regression/contract.ref b/test/regression/contract.ref
@@ -333,6 +333,9 @@
         </contract-storage>
       </live-contract>
     </live-contracts>
+    <events>
+      .List
+    </events>
     <next-address>
       3p160
     </next-address>

diff --git a/test/regression/emit.ref b/test/regression/emit.ref
@@ -0,0 +1,115 @@
+<solidity>
+  <k>
+    .K
+  </k>
+  <current-body>
+    EmitTest
+  </current-body>
+  <ifaces>
+    .IfaceCellMap
+  </ifaces>
+  <contracts>
+    <contract>
+      <contract-id>
+        EmitTest
+      </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>
+            .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-body>
+            emit Approval ( address ( 1 , .TypedVals ) , address ( 0 , .TypedVals ) , address ( 2 , .TypedVals ) , .TypedVals ) ;  .Statements
+          </contract-fn-body>
+        </contract-fn>
+      </contract-fns>
+      <contract-events>
+        <contract-event>
+          <contract-event-id>
+            Approval
+          </contract-event-id>
+          <contract-event-arg-types>
+            ListItem ( address )
+            ListItem ( address )
+            ListItem ( uint256 )
+          </contract-event-arg-types>
+          <contract-event-param-names>
+            ListItem ( owner )
+            ListItem ( spender )
+            ListItem ( value )
+          </contract-event-param-names>
+          <contract-event-indexed-pos>
+            SetItem ( 0 )
+            SetItem ( 1 )
+          </contract-event-indexed-pos>
+        </contract-event>
+      </contract-events>
+    </contract>
+  </contracts>
+  <exec>
+    <msg-sender>
+      1p160
+    </msg-sender>
+    <msg-value>
+      10p256
+    </msg-value>
+    <tx-origin>
+      1p160
+    </tx-origin>
+    <this>
+      2p160
+    </this>
+    <this-type>
+      EmitTest
+    </this-type>
+    <env>
+      .Map
+    </env>
+    <store>
+      .Map
+    </store>
+    <call-stack>
+      .List
+    </call-stack>
+    <live-contracts>
+      <live-contract>
+        <contract-address>
+          2p160
+        </contract-address>
+        <contract-type>
+          EmitTest
+        </contract-type>
+        <contract-storage>
+          .Map
+        </contract-storage>
+      </live-contract>
+    </live-contracts>
+    <events>
+      ListItem ( event (... name: Approval , args: v ( 1p160 , address ) , v ( 0p160 , address ) , v ( 2p160 , address ) , .TypedVals ) )
+    </events>
+    <next-address>
+      3p160
+    </next-address>
+  </exec>
+</solidity>
diff --git a/test/regression/emit.sol b/test/regression/emit.sol
@@ -0,0 +1,10 @@
+pragma solidity ^0.8.24;
+
+contract EmitTest {
+
+  event Approval(address indexed owner, address indexed spender, uint256 value);
+
+  constructor() {
+    emit Approval(address(1), address(0), address(2));
+  }	
+}
diff --git a/test/regression/emit.txn b/test/regression/emit.txn
@@ -0,0 +1 @@
+create(1, 10, EmitTest, )
diff --git a/test/regression/eventtestcontract.ref b/test/regression/eventtestcontract.ref
@@ -233,6 +233,9 @@
         </contract-storage>
       </live-contract>
     </live-contracts>
+    <events>
+      .List
+    </events>
     <next-address>
       3p160
     </next-address>

diff --git a/test/regression/function.ref b/test/regression/function.ref
@@ -1963,6 +1963,9 @@
         </contract-storage>
       </live-contract>
     </live-contracts>
+    <events>
+      .List
+    </events>
     <next-address>
       11p160
     </next-address>

diff --git a/test/regression/mapstestcontract.ref b/test/regression/mapstestcontract.ref
@@ -133,6 +133,9 @@
         </contract-storage>
       </live-contract>
     </live-contracts>
+    <events>
+      .List
+    </events>
     <next-address>
       3p160
     </next-address>