diff --git a/src/expression.md b/src/expression.md
index e4ba232..949bba9 100644
--- 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
index 9bb5312..29c888f 100644
--- 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
index 3b8f4f5..9949f23 100644
--- a/src/statement.md
+++ b/src/statement.md
@@ -31,4 +31,18 @@ module SOLIDITY-STATEMENT
... .List => ListItem(event(X, ARGS))
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 { S } => S ~> restoreEnv(E) ...
+ E
+
+ syntax KItem ::= restoreEnv(Map)
+ rule restoreEnv(E) => .K ...
+ _ => E
+
endmodule
diff --git a/test/regression/block.ref b/test/regression/block.ref
new file mode 100644
index 0000000..263cf13
--- /dev/null
+++ b/test/regression/block.ref
@@ -0,0 +1,98 @@
+
+
+ .K
+
+
+ BlockTest
+
+
+ .IfaceCellMap
+
+
+
+
+ BlockTest
+
+
+ .Map
+
+
+ .List
+
+
+
+
+ constructor
+
+
+ public
+
+
+ .List
+
+
+ .List
+
+
+ .List
+
+
+ .List
+
+
+ bool x = false ; { bool x = true ; require ( x , "" , .TypedVals ) ; .Statements } if ( x ) { require ( false , "" , .TypedVals ) ; .Statements } .Statements
+
+
+
+
+ .ContractEventCellMap
+
+
+
+
+
+ 1p160
+
+
+ 0p256
+
+
+ 1p160
+
+
+ 2p160
+
+
+ BlockTest
+
+
+ x |-> var ( 0 , bool )
+
+
+ 0 |-> false
+ 1 |-> true
+
+
+ .List
+
+
+
+
+ 2p160
+
+
+ BlockTest
+
+
+ .Map
+
+
+
+
+ .List
+
+
+ 3p160
+
+
+
diff --git a/test/regression/block.sol b/test/regression/block.sol
new file mode 100644
index 0000000..c3a9706
--- /dev/null
+++ 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
new file mode 100644
index 0000000..9571da7
--- /dev/null
+++ b/test/regression/block.txn
@@ -0,0 +1 @@
+create(1, 0, BlockTest, )
diff --git a/test/regression/boolean.ref b/test/regression/boolean.ref
new file mode 100644
index 0000000..1fdbda5
--- /dev/null
+++ b/test/regression/boolean.ref
@@ -0,0 +1,119 @@
+
+
+ .K
+
+
+ BoolTest
+
+
+ .IfaceCellMap
+
+
+
+
+ BoolTest
+
+
+ .Map
+
+
+ .List
+
+
+
+
+ constructor
+
+
+ public
+
+
+ .List
+
+
+ .List
+
+
+ .List
+
+
+ .List
+
+
+ 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
+
+
+
+ fail
+
+
+ private
+
+
+ .List
+
+
+ .List
+
+
+ .List
+
+
+ .List
+
+
+ require ( false , "" , .TypedVals ) ; .Statements
+
+
+
+
+ .ContractEventCellMap
+
+
+
+
+
+ 1p160
+
+
+ 0p256
+
+
+ 1p160
+
+
+ 2p160
+
+
+ BoolTest
+
+
+ x |-> var ( 0 , bool )
+
+
+ 0 |-> false
+
+
+ .List
+
+
+
+
+ 2p160
+
+
+ BoolTest
+
+
+ .Map
+
+
+
+
+ .List
+
+
+ 3p160
+
+
+
diff --git a/test/regression/boolean.sol b/test/regression/boolean.sol
new file mode 100644
index 0000000..bdf3984
--- /dev/null
+++ 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
new file mode 100644
index 0000000..561f2f3
--- /dev/null
+++ b/test/regression/boolean.txn
@@ -0,0 +1 @@
+create(1, 0, BoolTest, )
diff --git a/test/regression/if.ref b/test/regression/if.ref
new file mode 100644
index 0000000..f0e0f02
--- /dev/null
+++ b/test/regression/if.ref
@@ -0,0 +1,99 @@
+
+
+ .K
+
+
+ IfTest
+
+
+ .IfaceCellMap
+
+
+
+
+ IfTest
+
+
+ .Map
+
+
+ .List
+
+
+
+
+ constructor
+
+
+ public
+
+
+ .List
+
+
+ .List
+
+
+ .List
+
+
+ .List
+
+
+ bool x = true ; bool y = false ; if ( x ) { y = true ; .Statements } else { require ( false , "" , .TypedVals ) ; .Statements } require ( y , "" , .TypedVals ) ; y = false ; x = false ; if ( x ) { require ( false , "" , .TypedVals ) ; .Statements } else { y = true ; .Statements } require ( y , "" , .TypedVals ) ; if ( x ) { require ( false , "" , .TypedVals ) ; .Statements } .Statements
+
+
+
+
+ .ContractEventCellMap
+
+
+
+
+
+ 1p160
+
+
+ 0p256
+
+
+ 1p160
+
+
+ 2p160
+
+
+ IfTest
+
+
+ x |-> var ( 0 , bool )
+ y |-> var ( 1 , bool )
+
+
+ 0 |-> false
+ 1 |-> true
+
+
+ .List
+
+
+
+
+ 2p160
+
+
+ IfTest
+
+
+ .Map
+
+
+
+
+ .List
+
+
+ 3p160
+
+
+
diff --git a/test/regression/if.sol b/test/regression/if.sol
new file mode 100644
index 0000000..540a641
--- /dev/null
+++ b/test/regression/if.sol
@@ -0,0 +1,26 @@
+pragma solidity ^0.8.24;
+
+contract IfTest {
+
+ constructor() {
+ bool x = true;
+ bool y = false;
+ if (x) {
+ y = true;
+ } else {
+ require(false, "");
+ }
+ require(y, "");
+ y = false;
+ x = false;
+ if (x) {
+ require(false, "");
+ } else {
+ y = true;
+ }
+ require(y, "");
+ if (x) {
+ require(false, "");
+ }
+ }
+}
diff --git a/test/regression/if.txn b/test/regression/if.txn
new file mode 100644
index 0000000..904ffed
--- /dev/null
+++ b/test/regression/if.txn
@@ -0,0 +1 @@
+create(1, 0, IfTest, )