[SMTChecker] Support to integer and Bool storage vars

Changelog.md

@@ -25,6 +25,7 @@ Features:
  * Build system: Support Ubuntu Bionic.
  * SMTChecker: Integration with CVC4 SMT solver
  * Syntax Checker: Warn about functions named "constructor".
+ * SMTChecker: Support to integer and Bool state variables
 
 Bugfixes:
  * Type Checker: Improve error message for failed function overload resolution.

libsolidity/formal/SMTChecker.cpp

@@ -62,6 +62,8 @@ void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
 {
 	if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
 		assignment(_varDecl, *_varDecl.value(), _varDecl.location());
+	else if (_varDecl.isStateVariable() && _varDecl.type()->isValueType())
+		createVariable(_varDecl);
 }
 
 bool SMTChecker::visit(FunctionDefinition const& _function)
@@ -72,13 +74,13 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 			"Assertion checker does not yet support constructors and functions with modifiers."
 		);
 	m_currentFunction = &_function;
-	// We only handle local variables, so we clear at the beginning of the function.
-	// If we add storage variables, those should be cleared differently.
 	m_interface->reset();
 	m_variables.clear();
+	m_variables.insert(m_stateVariables.begin(), m_stateVariables.end());
 	m_pathConditions.clear();
 	m_loopExecutionHappened = false;
 	initializeLocalVariables(_function);
+	resetStateVariables();
 	return true;
 }
 
@@ -586,6 +588,12 @@ void SMTChecker::checkCondition(
 				expressionsToEvaluate.emplace_back(currentValue(*var));
 				expressionNames.push_back(var->name());
 			}
+		for (auto const& var: m_stateVariables)
+			if (knownVariable(*var.first))
+			{
+				expressionsToEvaluate.emplace_back(currentValue(*var.first));
+				expressionNames.push_back(var.first->name());
+			}
 	}
 	smt::CheckResult result;
 	vector<string> values;
@@ -607,7 +615,8 @@ void SMTChecker::checkCondition(
 			message << " for:\n";
 			solAssert(values.size() == expressionNames.size(), "");
 			for (size_t i = 0; i < values.size(); ++i)
-				message << "  " << expressionNames.at(i) << " = " << values.at(i) << "\n";
+				if (expressionsToEvaluate.at(i).name != values.at(i))
+					message << "  " << expressionNames.at(i) << " = " << values.at(i) << "\n";
 		}
 		else
 			message << ".";
@@ -722,6 +731,15 @@ void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
 				setZeroValue(*retParam);
 }
 
+void SMTChecker::resetStateVariables()
+{
+	for (auto const& variable: m_stateVariables)
+	{
+		newValue(*variable.first);
+		setUnknownValue(*variable.first);
+	}
+}
+
 void SMTChecker::resetVariables(vector<Declaration const*> _variables)
 {
 	for (auto const* decl: _variables)
@@ -752,7 +770,14 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 	if (SSAVariable::isSupportedType(_varDecl.type()->category()))
 	{
 		solAssert(m_variables.count(&_varDecl) == 0, "");
-		m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
+		solAssert(m_stateVariables.count(&_varDecl) == 0, "");
+		if (_varDecl.isLocalVariable())
+			m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
+		else
+		{
+			solAssert(_varDecl.isStateVariable(), "");
+			m_stateVariables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
+		}
 		return true;
 	}
 	else

libsolidity/formal/SMTChecker.h

@@ -111,6 +111,7 @@ private:
 	smt::CheckResult checkSatisfiable();
 
 	void initializeLocalVariables(FunctionDefinition const& _function);
+	void resetStateVariables();
 	void resetVariables(std::vector<Declaration const*> _variables);
 	/// Given two different branches and the touched variables,
 	/// merge the touched variables into after-branch ite variables
@@ -163,6 +164,7 @@ private:
 	bool m_loopExecutionHappened = false;
 	std::map<Expression const*, smt::Expression> m_expressions;
 	std::map<Declaration const*, SSAVariable> m_variables;
+	std::map<Declaration const*, SSAVariable> m_stateVariables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;
 

libsolidity/formal/VariableUsage.cpp

@@ -33,7 +33,6 @@ VariableUsage::VariableUsage(ASTNode const& _node)
 			solAssert(declaration, "");
 			if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
 				if (
-					varDecl->isLocalVariable() &&
 					identifier->annotation().lValueRequested &&
 					varDecl->annotation().type->isValueType()
 				)

test/libsolidity/SMTChecker.cpp

@@ -467,6 +467,72 @@ BOOST_AUTO_TEST_CASE(bool_int_mixed)
 	CHECK_SUCCESS_NO_WARNINGS(text);
 }
 
+BOOST_AUTO_TEST_CASE(storage_value_vars)
+{
+	string text = R"(
+		contract C
+		{
+			address a;
+			bool b;
+			uint c;
+			function f(uint x) public {
+				if (x == 0)
+				{
+					a = 100;
+					b = true;
+				}
+				else
+				{
+					a = 200;
+					b = false;
+				}
+				assert(a > 0 && b);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	text = R"(
+		contract C
+		{
+			address a;
+			bool b;
+			uint c;
+			function f() public view {
+				assert(c > 0);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+	text = R"(
+		contract C
+		{
+			address a;
+			bool b;
+			uint c;
+			function f(uint x) public {
+				if (x == 0)
+				{
+					a = 100;
+					b = true;
+				}
+				else
+				{
+					a = 200;
+					b = false;
+				}
+				assert(b == (a < 200));
+			}
+
+			function g() public view {
+				require(a < 100);
+				assert(c >= 0);
+			}
+
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+}
+
 BOOST_AUTO_TEST_CASE(while_loop_simple)
 {
 	// Check that variables are cleared