Check for conditions being constant.

4 files changed, 102 insertions, 27 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 1cf5dc95..3ad9db92 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -28,6 +28,7 @@
 #include <libsolidity/interface/ErrorReporter.h>
 
 #include <boost/range/adaptor/map.hpp>
+#include <boost/algorithm/string/replace.hpp>
 
 using namespace std;
 using namespace dev;
@@ -87,7 +88,7 @@ bool SMTChecker::visit(IfStatement const& _node)
 {
 	_node.condition().accept(*this);
 
-	// TODO Check if condition is always true
+	checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
 
 	visitBranch(_node.trueStatement(), expr(_node.condition()));
 	vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
@@ -104,8 +105,6 @@ bool SMTChecker::visit(IfStatement const& _node)
 
 bool SMTChecker::visit(WhileStatement const& _node)
 {
-	// TODO Check if condition is always true
-
 	auto touchedVariables = m_variableUsage->touchedVariables(_node);
 	resetVariables(touchedVariables);
 	if (_node.isDoWhile())
@@ -113,10 +112,13 @@ bool SMTChecker::visit(WhileStatement const& _node)
 		visitBranch(_node.body());
 		// TODO the assertions generated in the body should still be active in the condition
 		_node.condition().accept(*this);
+		checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE.");
 	}
 	else
 	{
 		_node.condition().accept(*this);
+		checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE.");
+
 		visitBranch(_node.body(), expr(_node.condition()));
 	}
 	resetVariables(touchedVariables);
@@ -264,6 +266,8 @@ void SMTChecker::endVisit(Literal const& _literal)
 
 		m_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal)));
 	}
+	else if (type.category() == Type::Category::Bool)
+		m_interface->addAssertion(expr(_literal) == smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
 	else
 		m_errorReporter.warning(
 			_literal.location(),
@@ -426,18 +430,7 @@ void SMTChecker::checkCondition(
 	}
 	smt::CheckResult result;
 	vector<string> values;
-	try
-	{
-		tie(result, values) = m_interface->check(expressionsToEvaluate);
-	}
-	catch (smt::SolverError const& _e)
-	{
-		string description("Error querying SMT solver");
-		if (_e.comment())
-			description += ": " + *_e.comment();
-		m_errorReporter.warning(_location, description);
-		return;
-	}
+	tie(result, values) = checkSatisifableAndGenerateModel(expressionsToEvaluate);
 
 	string conditionalComment;
 	if (m_conditionalExecutionHappened)
@@ -455,17 +448,7 @@ void SMTChecker::checkCondition(
 			message << " for:\n";
 			solAssert(values.size() == expressionNames.size(), "");
 			for (size_t i = 0; i < values.size(); ++i)
-			{
-				string formattedValue = values.at(i);
-				try
-				{
-					// Parse and re-format nicely
-					formattedValue = formatNumber(bigint(formattedValue));
-				}
-				catch (...) { }
-
-				message << "  " << expressionNames.at(i) << " = " << formattedValue << "\n";
-			}
+				message << "  " << expressionNames.at(i) << " = " << values.at(i) << "\n";
 		}
 		else
 			message << ".";
@@ -486,6 +469,84 @@ void SMTChecker::checkCondition(
 	m_interface->pop();
 }
 
+void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string const& _description)
+{
+	// Do not check for const-ness if this is a constant.
+	if (dynamic_cast<Literal const*>(&_condition))
+		return;
+
+	m_interface->push();
+	m_interface->addAssertion(expr(_condition));
+	auto positiveResult = checkSatisifable();
+	m_interface->pop();
+
+	m_interface->push();
+	m_interface->addAssertion(!expr(_condition));
+	auto negatedResult = checkSatisifable();
+	m_interface->pop();
+
+	if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
+		m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver.");
+	else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE)
+	{
+		// everything fine.
+	}
+	else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
+		m_errorReporter.warning(_condition.location(), "Condition unreachable.");
+	else
+	{
+		string value;
+		if (positiveResult == smt::CheckResult::SATISFIABLE)
+		{
+			solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, "");
+			value = "true";
+		}
+		else
+		{
+			solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, "");
+			solAssert(negatedResult == smt::CheckResult::SATISFIABLE, "");
+			value = "false";
+		}
+		m_errorReporter.warning(_condition.location(), boost::algorithm::replace_all_copy(_description, "$VALUE", value));
+	}
+}
+
+pair<smt::CheckResult, vector<string>>
+SMTChecker::checkSatisifableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
+{
+	smt::CheckResult result;
+	vector<string> values;
+	try
+	{
+		tie(result, values) = m_interface->check(_expressionsToEvaluate);
+	}
+	catch (smt::SolverError const& _e)
+	{
+		string description("Error querying SMT solver");
+		if (_e.comment())
+			description += ": " + *_e.comment();
+		m_errorReporter.warning(description);
+		result = smt::CheckResult::ERROR;
+	}
+
+	for (string& value: values)
+	{
+		try
+		{
+			// Parse and re-format nicely
+			value = formatNumber(bigint(value));
+		}
+		catch (...) { }
+	}
+
+	return make_pair(result, values);
+}
+
+smt::CheckResult SMTChecker::checkSatisifable()
+{
+	return checkSatisifableAndGenerateModel({}).first;
+}
+
 void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
 {
 	for (auto const& variable: _function.localVariables())
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index b2726a42..85a37f2c 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -72,6 +72,7 @@ private:
 	void visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
 	void visitBranch(Statement const& _statement, smt::Expression _condition);
 
+	/// Check that a condition can be satisfied.
 	void checkCondition(
 		smt::Expression _condition,
 		SourceLocation const& _location,
@@ -79,6 +80,18 @@ private:
 		std::string const& _additionalValueName = "",
 		smt::Expression* _additionalValue = nullptr
 	);
+	/// Checks that a boolean condition is not constant. Do not warn if the expression
+	/// is a literal constant.
+	/// @param _description the warning string, $VALUE will be replaced by the constant value.
+	void checkBooleanNotConstant(
+		Expression const& _condition,
+		std::string const& _description
+	);
+
+	std::pair<smt::CheckResult, std::vector<std::string>>
+	checkSatisifableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
+
+	smt::CheckResult checkSatisifable();
 
 	void initializeLocalVariables(FunctionDefinition const& _function);
 	void resetVariables(std::vector<Declaration const*> _variables);
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 70dc1585..a69d19d5 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -52,6 +52,7 @@ class Expression
 {
 	friend class SolverInterface;
 public:
+	explicit Expression(bool _v): name(_v ? "true" : "false") {}
 	Expression(size_t _number): name(std::to_string(_number)) {}
 	Expression(u256 const& _number): name(_number.str()) {}
 	Expression(bigint const& _number): name(_number.str()) {}
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 6111b2c8..0c083abc 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -91,7 +91,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
 			solAssert(false, "");
 		}
 
-		if (result != CheckResult::UNSATISFIABLE)
+		if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty())
 		{
 			z3::model m = m_solver.get_model();
 			for (Expression const& e: _expressionsToEvaluate)