Merge pull request #14216 from ethereum/fix_bmc_side_effects_in_statement

Fix encoding of side-effects inside if and ternary in BMC

Changelog.md

@@ -8,6 +8,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix encoding of side-effects inside ``if`` and ``ternary conditional``statements in the BMC engine.
 
 
 ### 0.8.20 (2023-05-10)

libsolidity/formal/BMC.cpp

@@ -237,6 +237,7 @@ void BMC::endVisit(FunctionDefinition const& _function)
 
 bool BMC::visit(IfStatement const& _node)
 {
+	auto indicesBeforePush = copyVariableIndices();
 	// This check needs to be done in its own context otherwise
 	// constraints from the If body might influence it.
 	m_context.pushSolver();
@@ -251,6 +252,7 @@ bool BMC::visit(IfStatement const& _node)
 			&_node.condition()
 		);
 	m_context.popSolver();
+	resetVariableIndices(std::move(indicesBeforePush));
 
 	_node.condition().accept(*this);
 	auto conditionExpr = expr(_node.condition());
@@ -274,6 +276,7 @@ bool BMC::visit(IfStatement const& _node)
 
 bool BMC::visit(Conditional const& _op)
 {
+	auto indicesBeforePush = copyVariableIndices();
 	m_context.pushSolver();
 	_op.condition().accept(*this);
 
@@ -284,6 +287,7 @@ bool BMC::visit(Conditional const& _op)
 			&_op.condition()
 		);
 	m_context.popSolver();
+	resetVariableIndices(std::move(indicesBeforePush));
 
 	SMTEncoder::visit(_op);
 

test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_1.sol

@@ -0,0 +1,15 @@
+contract C {
+    function f() public pure {
+        uint x;
+        if (++x < 3) {}
+
+        assert(x == 1); // should hold
+        assert(x != 1); // should fail
+    }
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 6838: (72-79): BMC: Condition is always true.
+// Warning 4661: (132-146): BMC: Assertion violation happens here.
+// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_2.sol

@@ -0,0 +1,26 @@
+contract C {
+    uint x;
+
+    function inc() internal returns (uint) {
+        // BMC inlines function calls and also looks at functions in isolation,
+        // therefore it says once that this is safe, when called by `f`,
+        // but also that it is unsafe just looking at this function (false positive).
+        ++x;
+        return x;
+    }
+
+    function f() public {
+        require(x < 1000);
+        uint y = x;
+        if (inc() < 3) {}
+
+        assert(x == y + 1); // should hold
+        assert(x != y + 1); // should fail
+    }
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 2661: (318-321): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4661: (499-517): BMC: Assertion violation happens here.
+// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_3.sol

@@ -0,0 +1,30 @@
+contract C {
+    uint x;
+
+    function inc() internal returns (uint) {
+        // BMC inlines function calls and also looks at functions in isolation,
+        // therefore it says once that this is safe, when called by `f`,
+        // but also that it is unsafe just looking at this function (false positive).
+        ++x;
+        return x;
+    }
+
+    function inc2() internal returns (uint) {
+        return inc();
+    }
+
+    function f() public {
+        require(x < 1000);
+        uint y = x;
+        if (inc2() < 3) {}
+
+        assert(x == y + 1); // should hold
+        assert(x != y + 1); // should fail
+    }
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 2661: (318-321): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4661: (575-593): BMC: Assertion violation happens here.
+// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_if_4.sol

@@ -0,0 +1,15 @@
+contract C {
+    function f() public pure {
+        uint x = 2;
+        if (--x < 3) {}
+
+        assert(x == 1); // should hold
+        assert(x != 1); // should fail
+    }
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 6838: (76-83): BMC: Condition is always true.
+// Warning 4661: (136-150): BMC: Assertion violation happens here.
+// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_1.sol

@@ -0,0 +1,16 @@
+contract C {
+    function f() public pure {
+        uint x;
+        uint y = (++x < 3) ? ++x : --x;
+
+        assert(y == x); // should hold;
+        assert(x == 2); // should hold
+        assert(x != 2); // should fail
+    }
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 6838: (77-86): BMC: Condition is always true.
+// Warning 4661: (188-202): BMC: Assertion violation happens here.
+// Info 6002: BMC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_2.sol

@@ -0,0 +1,27 @@
+contract C {
+    uint x;
+
+    function inc() internal returns (uint) {
+        // BMC inlines function calls and also looks at functions in isolation,
+        // therefore it says once that this is safe, when called by `f`,
+        // but also that it is unsafe just looking at this function (false positive).
+        ++x;
+        return x;
+    }
+
+    function f() public {
+        require(x < 1000);
+        uint z = x;
+        uint y = (inc() < 3) ? inc() : inc();
+
+        assert(y == x);
+        assert(x == z + 2); // should hold
+        assert(x != z + 2); // should fail
+    }
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 2661: (318-321): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4661: (543-561): BMC: Assertion violation happens here.
+// Info 6002: BMC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_3.sol

@@ -0,0 +1,31 @@
+contract C {
+    uint x;
+
+    function inc() internal returns (uint) {
+        // BMC inlines function calls and also looks at functions in isolation,
+        // therefore it says once that this is safe, when called by `f`,
+        // but also that it is unsafe just looking at this function (false positive).
+        ++x;
+        return x;
+    }
+
+    function inc2() internal returns (uint) {
+        return inc();
+    }
+
+    function f() public {
+        require(x < 1000);
+        uint z = x;
+        uint y = (inc2() < 3) ? inc2() : inc2();
+
+        assert(y == x); // should hold
+        assert(x == z + 2); // should hold
+        assert(x != z + 2); // should fail
+    }
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 2661: (318-321): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4661: (636-654): BMC: Assertion violation happens here.
+// Info 6002: BMC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/control_flow/side_effects_inside_ternary_4.sol

@@ -0,0 +1,16 @@
+contract C {
+    function f() public pure {
+        uint x = 2;
+        uint y = (--x < 3) ? --x : 0;
+
+        assert(y == x); // should hold
+        assert(x == 0); // should hold
+        assert(x != 0); // should fail
+    }
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 6838: (81-90): BMC: Condition is always true.
+// Warning 4661: (189-203): BMC: Assertion violation happens here.
+// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.