If statements and boolean operators (#16)

* boolean and/or * if statements * blocks * add test * update tests * update test to have better coverage
Pi-Squared-Inc · Aug 26, 2024 · 5585171 · 5585171
1 parent d0de1dc
commit 5585171
Show file tree

Hide file tree

Showing 12 changed files with 410 additions and 2 deletions.
diff --git a/src/expression.md b/src/expression.md
@@ -150,6 +150,12 @@ module SOLIDITY-EXPRESSION
   rule v(true, bool) ? X : _ => X
   rule v(false, bool) ? _ : X => X
 
+  // boolean and/or
+  rule v(true, bool) && E => E
+  rule v(false, bool) && _ => v(false, bool)
+  rule v(true, bool) || _ => v(true, bool)
+  rule v(false, bool) || E => E
+
   // helpers
   syntax Int ::= Number2Int(NumberLiteral) [function]
   rule Number2Int(X:HexNumber) => HexNumberString2Int(HexNumber2String(X))

diff --git a/src/solidity-syntax.md b/src/solidity-syntax.md
@@ -183,8 +183,8 @@ Following is a list of supported statements.
                                             | VariableDeclaration "=" Expression ";" [strict(2)]
                                             | "(" VariableDeclaration "," ")" "=" Expression ";" [strict(2)]
 
-    syntax IfStatement ::= "if" "(" Expression ")" Statement
-                         | "if" "(" Expression ")" Statement "else" Statement
+    syntax IfStatement ::= "if" "(" Expression ")" Statement [strict(1)]
+                         | "if" "(" Expression ")" Statement "else" Statement [avoid, strict(1)]
 
     syntax ForStatement ::= "for" "(" InitStatement ConditionStatement PostLoopStatement ")" Statement
     syntax InitStatement ::= VariableDeclarationStatement | ExpressionStatement | ";"

diff --git a/src/statement.md b/src/statement.md
@@ -31,4 +31,18 @@ module SOLIDITY-STATEMENT
        <events>... .List => ListItem(event(X, ARGS)) </events>
     requires isKResult(ARGS)
 
+  // if statement
+  rule if ( v(true, bool ) ) S => S
+  rule if ( v(false, bool ) ) _ => .K
+  rule if ( v(true, bool ) ) S else _ => S
+  rule if ( v(false, bool ) ) _ else S => S
+
+  // blocks
+  rule <k> { S } => S ~> restoreEnv(E) ...</k>
+       <env> E </env>
+
+  syntax KItem ::= restoreEnv(Map)
+  rule <k> restoreEnv(E) => .K ...</k>
+       <env> _ => E </env>
+
 endmodule
diff --git a/test/regression/block.ref b/test/regression/block.ref
@@ -0,0 +1,98 @@
+<solidity>
+  <k>
+    .K
+  </k>
+  <current-body>
+    BlockTest
+  </current-body>
+  <ifaces>
+    .IfaceCellMap
+  </ifaces>
+  <contracts>
+    <contract>
+      <contract-id>
+        BlockTest
+      </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>
+            bool x = false ;  { bool x = true ;  require ( x , "" , .TypedVals ) ;  .Statements }  if ( x ) { require ( false , "" , .TypedVals ) ;  .Statements }  .Statements
+          </contract-fn-body>
+        </contract-fn>
+      </contract-fns>
+      <contract-events>
+        .ContractEventCellMap
+      </contract-events>
+    </contract>
+  </contracts>
+  <exec>
+    <msg-sender>
+      1p160
+    </msg-sender>
+    <msg-value>
+      0p256
+    </msg-value>
+    <tx-origin>
+      1p160
+    </tx-origin>
+    <this>
+      2p160
+    </this>
+    <this-type>
+      BlockTest
+    </this-type>
+    <env>
+      x |-> var ( 0 , bool )
+    </env>
+    <store>
+      0 |-> false
+      1 |-> true
+    </store>
+    <call-stack>
+      .List
+    </call-stack>
+    <live-contracts>
+      <live-contract>
+        <contract-address>
+          2p160
+        </contract-address>
+        <contract-type>
+          BlockTest
+        </contract-type>
+        <contract-storage>
+          .Map
+        </contract-storage>
+      </live-contract>
+    </live-contracts>
+    <events>
+      .List
+    </events>
+    <next-address>
+      3p160
+    </next-address>
+  </exec>
+</solidity>
diff --git a/test/regression/block.sol b/test/regression/block.sol
@@ -0,0 +1,15 @@
+pragma solidity ^0.8.24;
+
+contract BlockTest {
+
+    constructor() {
+      bool x = false;
+      {
+        bool x = true;
+	require(x, "");
+      }
+      if (x) {
+        require(false, "");
+      }
+    }
+}
diff --git a/test/regression/block.txn b/test/regression/block.txn
@@ -0,0 +1 @@
+create(1, 0, BlockTest, )
diff --git a/test/regression/boolean.ref b/test/regression/boolean.ref
@@ -0,0 +1,119 @@
+<solidity>
+  <k>
+    .K
+  </k>
+  <current-body>
+    BoolTest
+  </current-body>
+  <ifaces>
+    .IfaceCellMap
+  </ifaces>
+  <contracts>
+    <contract>
+      <contract-id>
+        BoolTest
+      </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>
+            bool x = true ;  if ( x || fail ( .TypedVals ) ) { .Statements } else { require ( false , "" , .TypedVals ) ;  .Statements }  if ( x && true ) { .Statements } else { require ( false , "" , .TypedVals ) ;  .Statements }  x = false ;  if ( x && fail ( .TypedVals ) ) { require ( false , "" , .TypedVals ) ;  .Statements }  if ( x || true ) { .Statements } else { require ( false , "" , .TypedVals ) ;  .Statements }  .Statements
+          </contract-fn-body>
+        </contract-fn> <contract-fn>
+          <contract-fn-id>
+            fail
+          </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>
+            .List
+          </contract-fn-return-types>
+          <contract-fn-return-names>
+            .List
+          </contract-fn-return-names>
+          <contract-fn-body>
+            require ( false , "" , .TypedVals ) ;  .Statements
+          </contract-fn-body>
+        </contract-fn>
+      </contract-fns>
+      <contract-events>
+        .ContractEventCellMap
+      </contract-events>
+    </contract>
+  </contracts>
+  <exec>
+    <msg-sender>
+      1p160
+    </msg-sender>
+    <msg-value>
+      0p256
+    </msg-value>
+    <tx-origin>
+      1p160
+    </tx-origin>
+    <this>
+      2p160
+    </this>
+    <this-type>
+      BoolTest
+    </this-type>
+    <env>
+      x |-> var ( 0 , bool )
+    </env>
+    <store>
+      0 |-> false
+    </store>
+    <call-stack>
+      .List
+    </call-stack>
+    <live-contracts>
+      <live-contract>
+        <contract-address>
+          2p160
+        </contract-address>
+        <contract-type>
+          BoolTest
+        </contract-type>
+        <contract-storage>
+          .Map
+        </contract-storage>
+      </live-contract>
+    </live-contracts>
+    <events>
+      .List
+    </events>
+    <next-address>
+      3p160
+    </next-address>
+  </exec>
+</solidity>
diff --git a/test/regression/boolean.sol b/test/regression/boolean.sol
@@ -0,0 +1,28 @@
+pragma solidity ^0.8.24;
+
+contract BoolTest {
+
+    function fail() private {
+      require(false, "");
+    }
+
+    constructor() {
+      bool x = true;
+      if (x || fail()) {
+      } else {
+        require(false, "");
+      }
+      if (x && true) {
+      } else {
+        require(false, "");
+      }
+      x = false;
+      if (x && fail()) {
+        require(false, "");
+      }
+      if (x || true) {
+      } else {
+        require(false, "");
+      }
+    }
+}
diff --git a/test/regression/boolean.txn b/test/regression/boolean.txn
@@ -0,0 +1 @@
+create(1, 0, BoolTest, )