Merge pull request #6421 from ethereum/smt_fix_variable_usage

[SMTChecker] Refactor VariableUsage

libsolidity/formal/SMTChecker.cpp

@@ -18,7 +18,6 @@
 #include <libsolidity/formal/SMTChecker.h>
 
 #include <libsolidity/formal/SMTPortfolio.h>
-#include <libsolidity/formal/VariableUsage.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
 #include <libdevcore/StringUtils.h>
@@ -51,7 +50,6 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _
 
 void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner)
 {
-	m_variableUsage = make_shared<VariableUsage>(_source);
 	m_scanner = _scanner;
 	if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		_source.accept(*this);
@@ -211,17 +209,17 @@ bool SMTChecker::visit(IfStatement const& _node)
 		checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
 
 	auto indicesEndTrue = visitBranch(&_node.trueStatement(), expr(_node.condition()));
-	vector<VariableDeclaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
+	auto touchedVars = touchedVariables(_node.trueStatement());
 	decltype(indicesEndTrue) indicesEndFalse;
 	if (_node.falseStatement())
 	{
 		indicesEndFalse = visitBranch(_node.falseStatement(), !expr(_node.condition()));
-		touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
+		touchedVars += touchedVariables(*_node.falseStatement());
 	}
 	else
 		indicesEndFalse = copyVariableIndices();
 
-	mergeVariables(touchedVariables, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
+	mergeVariables(touchedVars, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
 
 	return false;
 }
@@ -238,8 +236,8 @@ bool SMTChecker::visit(IfStatement const& _node)
 bool SMTChecker::visit(WhileStatement const& _node)
 {
 	auto indicesBeforeLoop = copyVariableIndices();
-	auto touchedVariables = m_variableUsage->touchedVariables(_node);
-	resetVariables(touchedVariables);
+	auto touchedVars = touchedVariables(_node);
+	resetVariables(touchedVars);
 	decltype(indicesBeforeLoop) indicesAfterLoop;
 	if (_node.isDoWhile())
 	{
@@ -266,7 +264,7 @@ bool SMTChecker::visit(WhileStatement const& _node)
 	if (!_node.isDoWhile())
 		_node.condition().accept(*this);
 
-	mergeVariables(touchedVariables, expr(_node.condition()), indicesAfterLoop, copyVariableIndices());
+	mergeVariables(touchedVars, expr(_node.condition()), indicesAfterLoop, copyVariableIndices());
 
 	m_loopExecutionHappened = true;
 	return false;
@@ -281,17 +279,13 @@ bool SMTChecker::visit(ForStatement const& _node)
 	auto indicesBeforeLoop = copyVariableIndices();
 
 	// Do not reset the init expression part.
-	auto touchedVariables =
-		m_variableUsage->touchedVariables(_node.body());
+	auto touchedVars = touchedVariables(_node.body());
 	if (_node.condition())
-		touchedVariables += m_variableUsage->touchedVariables(*_node.condition());
+		touchedVars += touchedVariables(*_node.condition());
 	if (_node.loopExpression())
-		touchedVariables += m_variableUsage->touchedVariables(*_node.loopExpression());
-	// Remove duplicates
-	std::sort(touchedVariables.begin(), touchedVariables.end());
-	touchedVariables.erase(std::unique(touchedVariables.begin(), touchedVariables.end()), touchedVariables.end());
+		touchedVars += touchedVariables(*_node.loopExpression());
 
-	resetVariables(touchedVariables);
+	resetVariables(touchedVars);
 
 	if (_node.condition())
 	{
@@ -316,7 +310,7 @@ bool SMTChecker::visit(ForStatement const& _node)
 		_node.condition()->accept(*this);
 
 	auto forCondition = _node.condition() ? expr(*_node.condition()) : smt::Expression(true);
-	mergeVariables(touchedVariables, forCondition, indicesAfterLoop, copyVariableIndices());
+	mergeVariables(touchedVars, forCondition, indicesAfterLoop, copyVariableIndices());
 
 	m_loopExecutionHappened = true;
 	return false;
@@ -1162,17 +1156,17 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
 	{
 		// @TODO check that both of them are not constant
 		_op.leftExpression().accept(*this);
-		auto touchedVariables = m_variableUsage->touchedVariables(_op.leftExpression());
+		auto touchedVars = touchedVariables(_op.leftExpression());
 		if (_op.getOperator() == Token::And)
 		{
 			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression()));
-			mergeVariables(touchedVariables, !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
+			mergeVariables(touchedVars, !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
 		}
 		else
 		{
 			auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression()));
-			mergeVariables(touchedVariables, expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
+			mergeVariables(touchedVars, expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
 			defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
 		}
 	}
@@ -1507,7 +1501,7 @@ void SMTChecker::resetStorageReferences()
 	resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); });
 }
 
-void SMTChecker::resetVariables(vector<VariableDeclaration const*> _variables)
+void SMTChecker::resetVariables(set<VariableDeclaration const*> const& _variables)
 {
 	for (auto const* decl: _variables)
 		resetVariable(*decl);
@@ -1529,12 +1523,6 @@ TypePointer SMTChecker::typeWithoutPointer(TypePointer const& _type)
 	return _type;
 }
 
-void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
-{
-	set<VariableDeclaration const*> uniqueVars(_variables.begin(), _variables.end());
-	mergeVariables(uniqueVars, _condition, _indicesEndTrue, _indicesEndFalse);
-}
-
 void SMTChecker::mergeVariables(set<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
 {
 	for (auto const* decl: _variables)
@@ -1764,3 +1752,9 @@ FunctionDefinition const* SMTChecker::inlinedFunctionCallToDefinition(FunctionCa
 
 	return nullptr;
 }
+
+set<VariableDeclaration const*> SMTChecker::touchedVariables(ASTNode const& _node)
+{
+	solAssert(!m_functionPath.empty(), "");
+	return m_variableUsage.touchedVariables(_node, m_functionPath);
+}

libsolidity/formal/SMTChecker.h

@@ -20,6 +20,7 @@
 
 #include <libsolidity/formal/SolverInterface.h>
 #include <libsolidity/formal/SymbolicVariables.h>
+#include <libsolidity/formal/VariableUsage.h>
 
 #include <libsolidity/ast/ASTVisitor.h>
 #include <libsolidity/interface/ReadFile.h>
@@ -41,8 +42,6 @@ namespace dev
 namespace solidity
 {
 
-class VariableUsage;
-
 class SMTChecker: private ASTConstVisitor
 {
 public:
@@ -201,7 +200,7 @@ private:
 	void resetVariable(VariableDeclaration const& _variable);
 	void resetStateVariables();
 	void resetStorageReferences();
-	void resetVariables(std::vector<VariableDeclaration const*> _variables);
+	void resetVariables(std::set<VariableDeclaration const*> const& _variables);
 	void resetVariables(std::function<bool(VariableDeclaration const&)> const& _filter);
 	/// @returns the type without storage pointer information if it has it.
 	TypePointer typeWithoutPointer(TypePointer const& _type);
@@ -209,7 +208,6 @@ private:
 	/// Given two different branches and the touched variables,
 	/// merge the touched variables into after-branch ite variables
 	/// using the branch condition as guard.
-	void mergeVariables(std::vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);
 	void mergeVariables(std::set<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);
 	/// Tries to create an uninitialized variable and returns true on success.
 	/// This fails if the type is not supported.
@@ -272,8 +270,11 @@ private:
 	/// Resets the variable indices.
 	void resetVariableIndices(VariableIndices const& _indices);
 
+	/// @returns variables that are touched in _node's subtree.
+	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node);
+
 	std::shared_ptr<smt::SolverInterface> m_interface;
-	std::shared_ptr<VariableUsage> m_variableUsage;
+	VariableUsage m_variableUsage;
 	bool m_loopExecutionHappened = false;
 	bool m_arrayAssignmentHappened = false;
 	// True if the "No SMT solver available" warning was already created.

libsolidity/formal/VariableUsage.cpp

@@ -19,72 +19,61 @@
 
 #include <libsolidity/formal/SMTChecker.h>
 
-#include <libsolidity/ast/ASTVisitor.h>
+#include <algorithm>
 
 using namespace std;
 using namespace dev;
 using namespace dev::solidity;
 
-VariableUsage::VariableUsage(ASTNode const& _node)
+void VariableUsage::endVisit(Identifier const& _identifier)
 {
-	auto nodeFun = [&](ASTNode const& n) -> bool
-	{
-		if (auto identifier = dynamic_cast<Identifier const*>(&n))
-		{
-			Declaration const* declaration = identifier->annotation().referencedDeclaration;
-			solAssert(declaration, "");
-			if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
-				if (identifier->annotation().lValueRequested)
-					m_touchedVariable[&n] = varDecl;
-		}
-		else if (auto funCall = dynamic_cast<FunctionCall const*>(&n))
-		{
-			if (FunctionDefinition const* funDef = SMTChecker::inlinedFunctionCallToDefinition(*funCall))
-				m_children[&n].push_back(funDef);
-		}
-		return true;
-	};
-	auto edgeFun = [&](ASTNode const& _parent, ASTNode const& _child)
-	{
-		if (m_touchedVariable.count(&_child) || m_children.count(&_child))
-			m_children[&_parent].push_back(&_child);
-	};
-
-	ASTReduce reducer(nodeFun, edgeFun);
-	_node.accept(reducer);
+	Declaration const* declaration = _identifier.annotation().referencedDeclaration;
+	solAssert(declaration, "");
+	if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
+		if (_identifier.annotation().lValueRequested)
+			m_touchedVariables.insert(varDecl);
 }
 
-vector<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node) const
+void VariableUsage::endVisit(FunctionCall const& _funCall)
 {
-	if (!m_children.count(&_node) && !m_touchedVariable.count(&_node))
-		return {};
+	if (auto const& funDef = SMTChecker::inlinedFunctionCallToDefinition(_funCall))
+		if (find(m_functionPath.begin(), m_functionPath.end(), funDef) == m_functionPath.end())
+			funDef->accept(*this);
+}
 
-	set<VariableDeclaration const*> touched;
-	set<ASTNode const*> visitedFunctions;
-	vector<ASTNode const*> toVisit;
-	toVisit.push_back(&_node);
+bool VariableUsage::visit(FunctionDefinition const& _function)
+{
+	m_functionPath.push_back(&_function);
+	return true;
+}
 
-	while (!toVisit.empty())
-	{
-		ASTNode const* n = toVisit.back();
-		toVisit.pop_back();
+void VariableUsage::endVisit(FunctionDefinition const&)
+{
+	solAssert(!m_functionPath.empty(), "");
+	m_functionPath.pop_back();
+}
 
-		if (auto funDef = dynamic_cast<FunctionDefinition const*>(n))
-			visitedFunctions.insert(funDef);
+void VariableUsage::endVisit(ModifierInvocation const& _modifierInv)
+{
+	auto const& modifierDef = dynamic_cast<ModifierDefinition const*>(_modifierInv.name()->annotation().referencedDeclaration);
+	if (modifierDef)
+		modifierDef->accept(*this);
+}
 
-		if (m_children.count(n))
-		{
-			solAssert(!m_touchedVariable.count(n), "");
-			for (auto const& child: m_children.at(n))
-				if (!visitedFunctions.count(child))
-					toVisit.push_back(child);
-		}
-		else
-		{
-			solAssert(m_touchedVariable.count(n), "");
-			touched.insert(m_touchedVariable.at(n));
-		}
-	}
+void VariableUsage::endVisit(PlaceholderStatement const&)
+{
+	solAssert(!m_functionPath.empty(), "");
+	FunctionDefinition const* function = m_functionPath.back();
+	solAssert(function, "");
+	if (function->isImplemented())
+		function->body().accept(*this);
+}
 
-	return {touched.begin(), touched.end()};
+set<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node, vector<FunctionDefinition const*> const& _outerCallstack)
+{
+	m_touchedVariables.clear();
+	m_functionPath.clear();
+	m_functionPath += _outerCallstack;
+	_node.accept(*this);
+	return m_touchedVariables;
 }

libsolidity/formal/VariableUsage.h

@@ -17,33 +17,35 @@
 
 #pragma once
 
-#include <map>
-#include <set>
+#include <libsolidity/ast/ASTVisitor.h>
+
 #include <vector>
+#include <set>
 
 namespace dev
 {
 namespace solidity
 {
 
-class ASTNode;
-class VariableDeclaration;
-
 /**
- * This class collects information about which local variables of value type
- * are modified in which parts of the AST.
+ * This class computes information about which variables are modified in a certain subtree.
  */
-class VariableUsage
+class VariableUsage: private ASTConstVisitor
 {
 public:
-	explicit VariableUsage(ASTNode const& _node);
-
-	std::vector<VariableDeclaration const*> touchedVariables(ASTNode const& _node) const;
+	/// @param _outerCallstack the current callstack in the callers context.
+	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node, std::vector<FunctionDefinition const*> const& _outerCallstack);
 
 private:
-	// Variable touched by a specific AST node.
-	std::map<ASTNode const*, VariableDeclaration const*> m_touchedVariable;
-	std::map<ASTNode const*, std::vector<ASTNode const*>> m_children;
+	void endVisit(Identifier const& _node) override;
+	void endVisit(FunctionCall const& _node) override;
+	bool visit(FunctionDefinition const& _node) override;
+	void endVisit(FunctionDefinition const& _node) override;
+	void endVisit(ModifierInvocation const& _node) override;
+	void endVisit(PlaceholderStatement const& _node) override;
+
+	std::set<VariableDeclaration const*> m_touchedVariables;
+	std::vector<FunctionDefinition const*> m_functionPath;
 };
 
 }