SMTChecker: Loop conditions should be analyzed as in loop context in BMC

Value of loop condition can change between iterations of the loop.
Therefore, BMC should be in the "inside loop" state when analyzing loop
conditions.

Author: blishko

Changelog.md

@@ -8,6 +8,7 @@ Compiler Features:
 
 
 Bugfixes:
+* SMTChecker: Do not consider loop conditions as constant-condition verification target as this could cause incorrect reports and internal compiler errors.
 * SMTChecker: Fix incorrect analysis when only a subset of contracts is selected with `--model-checker-contracts`.
 * SMTChecker: Fix internal compiler error when string literal is used to initialize user-defined type based on fixed bytes.
 

libsolidity/formal/BMC.cpp

@@ -363,7 +363,9 @@ bool BMC::visit(WhileStatement const& _node)
 		{
 			//after loop iterations are done, we check the loop condition last final time
 			auto indices = copyVariableIndices();
+			m_loopCheckpoints.emplace();
 			_node.condition().accept(*this);
+			m_loopCheckpoints.pop();
 			loopCondition = expr(_node.condition());
 			// assert that the loop is complete
 			m_context.addAssertion(!loopCondition || broke || !loopConditionOnPreviousIterations);
@@ -391,13 +393,13 @@ bool BMC::visit(ForStatement const& _node)
 	for (unsigned int i = 0; i < bmcLoopIterations; ++i)
 	{
 		auto indicesBefore = copyVariableIndices();
+		m_loopCheckpoints.emplace();
 		if (_node.condition())
 		{
 			_node.condition()->accept(*this);
 			// values in loop condition might change during loop iteration
 			forCondition = expr(*_node.condition());
 		}
-		m_loopCheckpoints.emplace();
 		auto indicesAfterCondition = copyVariableIndices();
 
 		pushPathCondition(forCondition);
@@ -443,8 +445,10 @@ bool BMC::visit(ForStatement const& _node)
 		auto indices = copyVariableIndices();
 		if (_node.condition())
 		{
+			m_loopCheckpoints.emplace();
 			_node.condition()->accept(*this);
 			forCondition = expr(*_node.condition());
+			m_loopCheckpoints.pop();
 		}
 		// assert that the loop is complete
 		m_context.addAssertion(!forCondition || broke || !forConditionOnPreviousIterations);
@@ -932,9 +936,9 @@ void BMC::checkVerificationTarget(BMCVerificationTarget& _target)
 			checkAssert(_target);
 			break;
 		case VerificationTargetType::ConstantCondition:
-			solAssert(false, "Checks for constant condition are handled separately");
+			smtAssert(false, "Checks for constant condition are handled separately");
 		default:
-			solAssert(false, "");
+			smtAssert(false);
 	}
 }
 

test/libsolidity/smtCheckerTests/loops/for_loop_condition_constant_true_in_first_iteration_and_constant_false_in_second.sol

@@ -0,0 +1,10 @@
+contract Test {
+    function loop() public pure {
+        for (uint k = 0; (k == 0 ? true : false); k++) {
+        }
+    }
+}
+// ====
+// SMTEngine: bmc
+// SMTTargets: constantCondition
+// ----

test/libsolidity/smtCheckerTests/loops/while_loop_condition_constant_true_in_first_iteration_and_constant_false_in_second.sol

@@ -0,0 +1,12 @@
+contract Test {
+    function loop() public pure {
+        uint k = 0;
+        while (k == 0 ? true : false) {
+            ++k;
+        }
+    }
+}
+// ====
+// SMTEngine: bmc
+// SMTTargets: constantCondition
+// ----