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

Diff for: Changelog.md

@@ -18,6 +18,7 @@ Bugfixes:
  * General: Fix internal compiler error when requesting IR AST outputs for interfaces and abstract contracts.
  * SMTChecker: Fix internal compiler error when analyzing overflowing expressions or bitwise negation of unsigned types involving constants.
  * SMTChecker: Fix reporting on targets that are safe in the context of one contract but unsafe in the context of another contract.
+ * SMTChecker: Fix SMT logic error in BMC when loop condition is always true in one iteration and always false in the next one.
  * SMTChecker: Fix SMT logic error when analyzing cross-contract getter call with BMC.
  * SMTChecker: Fix SMT logic error when contract deployment involves string literal to fixed bytes conversion.
  * SMTChecker: Fix SMT logic error when external call has extra effectless parentheses.

Diff for: 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);
 	}
 }
 

Diff for: libsolidity/formal/BMC.h

@@ -171,9 +171,12 @@ class BMC: public SMTEncoder
 		smtutil::Expression const& _value,
 		Expression const* _expression
 	);
+	/// Special handling of ConstantCondition verification target.
+	/// The target is checked immediately, unlike the other targets that are queued for checking at the end of analysis.
+	void checkIfConditionIsConstant(Expression const& _condition);
 	//@}
 
-	void checkIfConditionIsConstant(Expression const& _condition);
+
 
 	/// Solver related.
 	//@{
@@ -223,20 +226,23 @@ class BMC: public SMTEncoder
 	/// Number of verification conditions that could not be proved.
 	size_t m_unprovedAmt = 0;
 
+	/// Loop analysis
+	//@{
 	enum class LoopControlKind
 	{
 		Continue,
 		Break
 	};
 
-	// Current path conditions and SSA indices for break or continue statement
+	/// Current path conditions and SSA indices for break or continue statement
 	struct LoopControl {
 		LoopControlKind kind;
 		smtutil::Expression pathConditions;
 		VariableIndices variableIndices;
 	};
 
-	// Loop control statements for every loop
+	/// Loop control statements for every loop
 	std::stack<std::vector<LoopControl>> m_loopCheckpoints;
+	//@}
 };
 }

Diff for: test/libsolidity/smtCheckerTests/loops/for_loop_ternary_operator_in_condition.sol

@@ -0,0 +1,10 @@
+contract Test {
+    function loop() public pure {
+        for (uint k = 0; (k == 0 ? true : false); k++) {
+        }
+    }
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.