[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);
@@ -202,17 +200,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;
 }
@@ -229,8 +227,8 @@ bool SMTChecker::visit(IfStatement const& _node)
 bool SMTChecker::visit(WhileStatement const& _node)
 {
 	auto indicesBeforeLoop = copyVariableIndices();
-	auto touchedVariables = m_variableUsage->touchedVariables(_node);
+	auto touchedVars = touchedVariables(_node);
-	resetVariables(touchedVariables);
+	resetVariables(touchedVars);
 	decltype(indicesBeforeLoop) indicesAfterLoop;
 	if (_node.isDoWhile())
 	{
@@ -257,7 +255,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;
@@ -272,17 +270,13 @@ bool SMTChecker::visit(ForStatement const& _node)
 	auto indicesBeforeLoop = copyVariableIndices();
 
 	// Do not reset the init expression part.
-	auto touchedVariables =
+	auto touchedVars = touchedVariables(_node.body());
-		m_variableUsage->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());
+		touchedVars += touchedVariables(*_node.loopExpression());
-	// Remove duplicates
-	std::sort(touchedVariables.begin(), touchedVariables.end());
-	touchedVariables.erase(std::unique(touchedVariables.begin(), touchedVariables.end()), touchedVariables.end());
 
-	resetVariables(touchedVariables);
+	resetVariables(touchedVars);
 
 	if (_node.condition())
 	{
@@ -307,7 +301,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;
@@ -1153,17 +1147,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()));
 		}
 	}
@@ -1498,7 +1492,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);
@@ -1520,12 +1514,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)
@@ -1755,3 +1743,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:
@@ -200,7 +199,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);
@@ -208,7 +207,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.
@@ -271,8 +269,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
+	Declaration const* declaration = _identifier.annotation().referencedDeclaration;
-	{
+	solAssert(declaration, "");
-		if (auto identifier = dynamic_cast<Identifier const*>(&n))
+	if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
-		{
+		if (_identifier.annotation().lValueRequested)
-			Declaration const* declaration = identifier->annotation().referencedDeclaration;
+			m_touchedVariables.insert(varDecl);
-			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);
 }
 
-vector<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node) const
+void VariableUsage::endVisit(FunctionCall const& _funCall)
 {
-	if (!m_children.count(&_node) && !m_touchedVariable.count(&_node))
+	if (auto const& funDef = SMTChecker::inlinedFunctionCallToDefinition(_funCall))
-		return {};
+		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;
+bool VariableUsage::visit(FunctionDefinition const& _function)
-	toVisit.push_back(&_node);
+{
-
+	m_functionPath.push_back(&_function);
-	while (!toVisit.empty())
+	return true;
-	{
+}
-		ASTNode const* n = toVisit.back();
+
-		toVisit.pop_back();
+void VariableUsage::endVisit(FunctionDefinition const&)
-
+{
-		if (auto funDef = dynamic_cast<FunctionDefinition const*>(n))
+	solAssert(!m_functionPath.empty(), "");
-			visitedFunctions.insert(funDef);
+	m_functionPath.pop_back();
-
+}
-		if (m_children.count(n))
+
-		{
+void VariableUsage::endVisit(ModifierInvocation const& _modifierInv)
-			solAssert(!m_touchedVariable.count(n), "");
+{
-			for (auto const& child: m_children.at(n))
+	auto const& modifierDef = dynamic_cast<ModifierDefinition const*>(_modifierInv.name()->annotation().referencedDeclaration);
-				if (!visitedFunctions.count(child))
+	if (modifierDef)
-					toVisit.push_back(child);
+		modifierDef->accept(*this);
-		}
+}
-		else
+
-		{
+void VariableUsage::endVisit(PlaceholderStatement const&)
-			solAssert(m_touchedVariable.count(n), "");
+{
-			touched.insert(m_touchedVariable.at(n));
+	solAssert(!m_functionPath.empty(), "");
-		}
+	FunctionDefinition const* function = m_functionPath.back();
-	}
+	solAssert(function, "");
-
+	if (function->isImplemented())
-	return {touched.begin(), touched.end()};
+		function->body().accept(*this);
+}
+
+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 <libsolidity/ast/ASTVisitor.h>
-#include <set>
+
 #include <vector>
+#include <set>
 
 namespace dev
 {
 namespace solidity
 {
 
-class ASTNode;
-class VariableDeclaration;
-
 /**
- * This class collects information about which local variables of value type
+ * This class computes information about which variables are modified in a certain subtree.
- * are modified in which parts of the AST.
  */
-class VariableUsage
+class VariableUsage: private ASTConstVisitor
 {
 public:
-	explicit VariableUsage(ASTNode const& _node);
+	/// @param _outerCallstack the current callstack in the callers context.
-
+	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node, std::vector<FunctionDefinition const*> const& _outerCallstack);
-	std::vector<VariableDeclaration const*> touchedVariables(ASTNode const& _node) const;
 
 private:
-	// Variable touched by a specific AST node.
+	void endVisit(Identifier const& _node) override;
-	std::map<ASTNode const*, VariableDeclaration const*> m_touchedVariable;
+	void endVisit(FunctionCall const& _node) override;
-	std::map<ASTNode const*, std::vector<ASTNode const*>> m_children;
+	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;
 };
 
 }

test/libsolidity/smtCheckerTests/functions/function_inline_chain.sol

@@ -0,0 +1,41 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint x;
+	uint y;
+	uint z;
+
+	function f() public {
+		if (x == 1)
+			x = 2;
+		else
+			x = 1;
+		g();
+		assert(y == 1);
+	}
+
+	function g() public {
+		y = 1;
+		h();
+		assert(z == 1);
+	}
+
+	function h() public {
+		z = 1;
+		x = 1;
+		f();
+		// This fails for the following calls to the contract:
+		// h()
+		// g() h()
+		// It does not fail for f() g() h() because in that case
+		// h() will not inline f() since it already is in the callstack.
+		assert(x == 1);
+	}
+}
+// ----
+// Warning: (271-274): Assertion checker does not support recursive function calls.
+// Warning: (140-143): Assertion checker does not support recursive function calls.
+// Warning: (483-497): Assertion violation happens here
+// Warning: (201-204): Assertion checker does not support recursive function calls.
+// Warning: (483-497): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_assignment_outside_branch.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+    uint x;
+    address owner;
+
+	modifier onlyOwner {
+        if (msg.sender == owner) _;
+    }
+
+    function f() public onlyOwner {
+    }
+
+    function g(uint y) public {
+        y = 1;
+        if (y > x) f();
+    }
+}

test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+    address owner;
+    modifier onlyOwner {
+        if (msg.sender == owner) _;
+    }
+    function g() public onlyOwner {
+    }
+    function f(uint x) public {
+        if (x > 0) g();
+    }
+}

test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x;
+	address owner;
+
+	modifier onlyOwner {
+		if (msg.sender == owner) _;
+	}
+
+	function f() public onlyOwner {
+		x = 0;
+	}
+	function g(uint y) public {
+		x = 1;
+		if (y > 0)
+			f();
+		// Fails for {y = >0, msg.sender == owner, x = 0}.
+		assert(x > 0);
+	}
+}
+// ----
+// Warning: (287-300): Assertion violation happens here

test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_branch.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x;
+	address owner;
+
+	modifier onlyOwner {
+		if (msg.sender == owner) {
+			require(x > 0);
+			_;
+		}
+	}
+
+	function f() public onlyOwner {
+		// Condition is always true due to `require(x > 0)` in the modifier.
+		if (x > 0)
+			x -= 1;
+	}
+	function g(uint y) public {
+		x = 2;
+		if (y > 0)
+			f();
+		assert(x > 0);
+	}
+}
+// ----
+// Warning: (266-271): Condition is always true.

test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment_multi_branches.sol

@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint x;
+	address owner;
+
+	modifier onlyOwner {
+		if (msg.sender == owner) {
+			require(x > 0);
+			_;
+		}
+	}
+
+	function f() public onlyOwner {
+		x -= 1;
+		h();
+	}
+	function h() public onlyOwner {
+		require(x < 10000);
+		x += 2;
+	}
+	function g(uint y) public {
+		require(y > 0 && y < 10000);
+		require(msg.sender == owner);
+		x = y;
+		if (y > 1) {
+			f();
+			assert(x == y + 1);
+		}
+		// Fails for {y = 0, x = 0}.
+		assert(x == 0);
+	}
+}
+// ----
+// Warning: (461-475): Assertion violation happens here