Merge pull request #3947 from ethereum/smt_storage

[SMTChecker] Support to integer and Bool storage vars

5 files changed, 121 insertions, 5 deletions

diff --git a/Changelog.md b/Changelog.md
index ce0adfd7..ddd33df7 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -10,6 +10,7 @@ Features:
  * Optimizer: Remove unnecessary masking of the result of known short instructions (``ADDRESS``, ``CALLER``, ``ORIGIN`` and ``COINBASE``).
  * Parser: Display nicer error messages by showing the actual tokens and not internal names.
  * Parser: Use the entire location of the token instead of only its starting position as source location for parser errors.
+ * SMT Checker: Support state variables of integer and bool type.
  * Type Checker: Deprecate the ``years`` unit denomination and raise a warning for it (or an error as experimental 0.5.0 feature).
  * Type Checker: Make literals (without explicit type casting) an error for tight packing as experimental 0.5.0 feature.
  * Type Checker: Warn about wildcard tuple assignments (this will turn into an error with version 0.5.0).
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index c4dee22d..425c5c1e 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -58,6 +58,19 @@ void SMTChecker::analyze(SourceUnit const& _source)
 		_source.accept(*this);
 }
 
+bool SMTChecker::visit(ContractDefinition const& _contract)
+{
+	for (auto _var : _contract.stateVariables())
+		if (_var->type()->isValueType())
+			createVariable(*_var);
+	return true;
+}
+
+void SMTChecker::endVisit(ContractDefinition const&)
+{
+	m_stateVariables.clear();
+}
+
 void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
 {
 	if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
@@ -72,13 +85,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 +599,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 +626,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 +742,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 +781,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
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index fd54fb5c..50d40ab9 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -50,6 +50,8 @@ private:
 	// because the order of expression evaluation is undefined
 	// TODO: or just force a certain order, but people might have a different idea about that.
 
+	virtual bool visit(ContractDefinition const& _node) override;
+	virtual void endVisit(ContractDefinition const& _node) override;
 	virtual void endVisit(VariableDeclaration const& _node) override;
 	virtual bool visit(FunctionDefinition const& _node) override;
 	virtual void endVisit(FunctionDefinition const& _node) override;
@@ -111,6 +113,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 +166,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;
 
diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp
index 4e96059d..c2dea844 100644
--- a/libsolidity/formal/VariableUsage.cpp
+++ b/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()
 				)
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index beb933a4..71fdb906 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -467,6 +467,82 @@ 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
+		{
+			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);
+			}
+			address a;
+			bool b;
+			uint c;
+		}
+	)";
+	CHECK_SUCCESS_NO_WARNINGS(text);
+	text = R"(
+		contract C
+		{
+			function f() public view {
+				assert(c > 0);
+			}
+			uint c;
+		}
+	)";
+	CHECK_WARNING(text, "Assertion violation happens here");
+
+}
+
 BOOST_AUTO_TEST_CASE(while_loop_simple)
 {
 	// Check that variables are cleared