Merge pull request #15862 from ethereum/smt-fix-loops-in-bmc

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

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

@@ -247,14 +247,8 @@ bool BMC::visit(IfStatement const& _node)
 	m_context.pushSolver();
 	_node.condition().accept(*this);
 
-	// We ignore called functions here because they have
-	// specific input values.
-	if (isRootFunction() && !isInsideLoop())
-		addVerificationTarget(
-			VerificationTargetType::ConstantCondition,
-			expr(_node.condition()),
-			&_node.condition()
-		);
+	checkIfConditionIsConstant(_node.condition());
+
 	m_context.popSolver();
 	resetVariableIndices(std::move(indicesBeforePush));
 
@@ -283,13 +277,7 @@ bool BMC::visit(Conditional const& _op)
 	auto indicesBeforePush = copyVariableIndices();
 	m_context.pushSolver();
 	_op.condition().accept(*this);
-
-	if (isRootFunction() && !isInsideLoop())
-		addVerificationTarget(
-			VerificationTargetType::ConstantCondition,
-			expr(_op.condition()),
-			&_op.condition()
-		);
+	checkIfConditionIsConstant(_op.condition());
 	m_context.popSolver();
 	resetVariableIndices(std::move(indicesBeforePush));
 
@@ -375,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);
@@ -403,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);
@@ -455,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);
@@ -690,12 +682,7 @@ void BMC::visitRequire(FunctionCall const& _funCall)
 	auto const& args = _funCall.arguments();
 	solAssert(args.size() >= 1, "");
 	solAssert(args.front()->annotation().type->category() == Type::Category::Bool, "");
-	if (isRootFunction() && !isInsideLoop())
-		addVerificationTarget(
-			VerificationTargetType::ConstantCondition,
-			expr(*args.front()),
-			args.front().get()
-		);
+	checkIfConditionIsConstant(*args.front());
 }
 
 void BMC::visitAddMulMod(FunctionCall const& _funCall)
@@ -933,9 +920,6 @@ void BMC::checkVerificationTarget(BMCVerificationTarget& _target)
 
 	switch (_target.type)
 	{
-		case VerificationTargetType::ConstantCondition:
-			checkConstantCondition(_target);
-			break;
 		case VerificationTargetType::Underflow:
 			checkUnderflow(_target);
 			break;
@@ -951,19 +935,70 @@ void BMC::checkVerificationTarget(BMCVerificationTarget& _target)
 		case VerificationTargetType::Assert:
 			checkAssert(_target);
 			break;
+		case VerificationTargetType::ConstantCondition:
+			smtAssert(false, "Checks for constant condition are handled separately");
 		default:
-			solAssert(false, "");
+			smtAssert(false);
 	}
 }
 
-void BMC::checkConstantCondition(BMCVerificationTarget& _target)
+void BMC::checkIfConditionIsConstant(Expression const& _condition)
 {
-	checkBooleanNotConstant(
-		*_target.expression,
-		_target.constraints,
-		_target.value,
-		_target.callStack
-	);
+	if (
+		!m_settings.targets.has(VerificationTargetType::ConstantCondition) ||
+		(m_currentContract && !shouldEncode(*m_currentContract))
+	)
+		return;
+
+	// We ignore called functions here because they have specific input values.
+	// Also, expressions inside loop can have different values in different iterations.
+	if (!isRootFunction() || isInsideLoop())
+		return;
+
+	// Do not check for const-ness if this is a literal.
+	if (dynamic_cast<Literal const*>(&_condition))
+		return;
+
+	auto [canBeTrue, canBeFalse] = checkBooleanNotConstant(currentPathConditions() && m_context.assertions(), expr(_condition));
+
+	// Report based on the result of the checks
+	if (canBeTrue == CheckResult::ERROR || canBeFalse == CheckResult::ERROR)
+		m_errorReporter.warning(8592_error, _condition.location(), "BMC: Error trying to invoke SMT solver.");
+	else if (canBeTrue == CheckResult::CONFLICTING || canBeFalse == CheckResult::CONFLICTING)
+		m_errorReporter.warning(3356_error, _condition.location(), "BMC: At least two SMT solvers provided conflicting answers. Results might not be sound.");
+	else if (canBeTrue == CheckResult::UNKNOWN || canBeFalse == CheckResult::UNKNOWN)
+	{
+		// Not enough information to make definite claims.
+	}
+	else if (canBeTrue == CheckResult::SATISFIABLE && canBeFalse == CheckResult::SATISFIABLE)
+	{
+		// Condition can be both true and false for some program runs.
+	}
+
+	else if (canBeTrue == CheckResult::UNSATISFIABLE && canBeFalse == CheckResult::UNSATISFIABLE)
+		m_errorReporter.warning(2512_error, _condition.location(), "BMC: Condition unreachable.", SMTEncoder::callStackMessage(m_callStack));
+	else
+	{
+		std::string description;
+		if (canBeFalse == smtutil::CheckResult::UNSATISFIABLE)
+		{
+			smtAssert(canBeTrue == smtutil::CheckResult::SATISFIABLE);
+			description = "BMC: Condition is always true.";
+		}
+		else
+		{
+			smtAssert(canBeTrue == smtutil::CheckResult::UNSATISFIABLE);
+			smtAssert(canBeFalse == smtutil::CheckResult::SATISFIABLE);
+			description = "BMC: Condition is always false.";
+		}
+		m_errorReporter.warning(
+			6838_error,
+			_condition.location(),
+			description,
+			SMTEncoder::callStackMessage(m_callStack)
+		);
+	}
+
 }
 
 void BMC::checkUnderflow(BMCVerificationTarget& _target)
@@ -1068,6 +1103,7 @@ void BMC::addVerificationTarget(
 	Expression const* _expression
 )
 {
+	smtAssert(_type != VerificationTargetType::ConstantCondition, "Checks for constant condition are handled separately");
 	if (!m_settings.targets.has(_type) || (m_currentContract && !shouldAnalyzeVerificationTargetsFor(*m_currentContract)))
 		return;
 
@@ -1081,10 +1117,7 @@ void BMC::addVerificationTarget(
 		m_callStack,
 		modelExpressions()
 	};
-	if (_type == VerificationTargetType::ConstantCondition)
-		checkVerificationTarget(target);
-	else
-		m_verificationTargets.emplace_back(std::move(target));
+	m_verificationTargets.emplace_back(std::move(target));
 }
 
 /// Solving.
@@ -1188,62 +1221,22 @@ void BMC::checkCondition(
 	m_interface->pop();
 }
 
-void BMC::checkBooleanNotConstant(
-	Expression const& _condition,
+BMC::ConstantExpressionCheckResult BMC::checkBooleanNotConstant(
 	smtutil::Expression const& _constraints,
-	smtutil::Expression const& _value,
-	std::vector<SMTEncoder::CallStackEntry> const& _callStack
+	smtutil::Expression const& _condition
 )
 {
-	// Do not check for const-ness if this is a constant.
-	if (dynamic_cast<Literal const*>(&_condition))
-		return;
-
 	m_interface->push();
-	m_interface->addAssertion(_constraints && _value);
+	m_interface->addAssertion(_constraints && _condition);
 	auto positiveResult = checkSatisfiable();
 	m_interface->pop();
 
 	m_interface->push();
-	m_interface->addAssertion(_constraints && !_value);
+	m_interface->addAssertion(_constraints && !_condition);
 	auto negatedResult = checkSatisfiable();
 	m_interface->pop();
 
-	if (positiveResult == smtutil::CheckResult::ERROR || negatedResult == smtutil::CheckResult::ERROR)
-		m_errorReporter.warning(8592_error, _condition.location(), "BMC: Error trying to invoke SMT solver.");
-	else if (positiveResult == smtutil::CheckResult::CONFLICTING || negatedResult == smtutil::CheckResult::CONFLICTING)
-		m_errorReporter.warning(3356_error, _condition.location(), "BMC: At least two SMT solvers provided conflicting answers. Results might not be sound.");
-	else if (positiveResult == smtutil::CheckResult::SATISFIABLE && negatedResult == smtutil::CheckResult::SATISFIABLE)
-	{
-		// everything fine.
-	}
-	else if (positiveResult == smtutil::CheckResult::UNKNOWN || negatedResult == smtutil::CheckResult::UNKNOWN)
-	{
-		// can't do anything.
-	}
-	else if (positiveResult == smtutil::CheckResult::UNSATISFIABLE && negatedResult == smtutil::CheckResult::UNSATISFIABLE)
-		m_errorReporter.warning(2512_error, _condition.location(), "BMC: Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
-	else
-	{
-		std::string description;
-		if (positiveResult == smtutil::CheckResult::SATISFIABLE)
-		{
-			solAssert(negatedResult == smtutil::CheckResult::UNSATISFIABLE, "");
-			description = "BMC: Condition is always true.";
-		}
-		else
-		{
-			solAssert(positiveResult == smtutil::CheckResult::UNSATISFIABLE, "");
-			solAssert(negatedResult == smtutil::CheckResult::SATISFIABLE, "");
-			description = "BMC: Condition is always false.";
-		}
-		m_errorReporter.warning(
-			6838_error,
-			_condition.location(),
-			description,
-			SMTEncoder::callStackMessage(_callStack)
-		);
-	}
+	return {.canBeTrue = positiveResult, .canBeFalse = negatedResult};
 }
 
 std::pair<smtutil::CheckResult, std::vector<std::string>>

libsolidity/formal/BMC.h

@@ -161,7 +161,6 @@ class BMC: public SMTEncoder
 
 	void checkVerificationTargets();
 	void checkVerificationTarget(BMCVerificationTarget& _target);
-	void checkConstantCondition(BMCVerificationTarget& _target);
 	void checkUnderflow(BMCVerificationTarget& _target);
 	void checkOverflow(BMCVerificationTarget& _target);
 	void checkDivByZero(BMCVerificationTarget& _target);
@@ -172,8 +171,13 @@ 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);
 	//@}
 
+
+
 	/// Solver related.
 	//@{
 	/// Check that a condition can be satisfied.
@@ -188,13 +192,18 @@ class BMC: public SMTEncoder
 		std::string const& _additionalValueName = "",
 		smtutil::Expression const* _additionalValue = nullptr
 	);
-	/// Checks that a boolean condition is not constant. Do not warn if the expression
-	/// is a literal constant.
-	void checkBooleanNotConstant(
-		Expression const& _condition,
+
+	struct ConstantExpressionCheckResult
+	{
+		smtutil::CheckResult canBeTrue;
+		smtutil::CheckResult canBeFalse;
+	};
+
+	/// Checks whether the given boolean condition is either true or always false under given constraints.
+	/// Returns the results from the solver for these two checks.
+	ConstantExpressionCheckResult checkBooleanNotConstant(
 		smtutil::Expression const& _constraints,
-		smtutil::Expression const& _value,
-		std::vector<CallStackEntry> const& _callStack
+		smtutil::Expression const& _condition
 	);
 	std::pair<smtutil::CheckResult, std::vector<std::string>>
 	checkSatisfiableAndGenerateModel(std::vector<smtutil::Expression> const& _expressionsToEvaluate);
@@ -222,20 +231,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;
+	//@}
 };
 }

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
+// ----