Track usage of variables.

libsolidity/formal/SMTChecker.cpp

@@ -23,6 +23,8 @@
 #include <libsolidity/formal/SMTLib2Interface.h>
 #endif
 
+#include <libsolidity/formal/VariableUsage.h>
+
 #include <libsolidity/interface/ErrorReporter.h>
 
 #include <boost/range/adaptor/map.hpp>
@@ -44,23 +46,15 @@ SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback con
 
 void SMTChecker::analyze(SourceUnit const& _source)
 {
+	m_variableUsage = make_shared<VariableUsage>(_source);
 	if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		_source.accept(*this);
 }
 
 void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
 {
-	if (_varDecl.value())
+	if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
-	{
+		assignment(_varDecl, *_varDecl.value());
-		m_errorReporter.warning(
-			_varDecl.location(),
-			"Assertion checker does not yet support this."
-		);
-	}
-	else if (_varDecl.isLocalOrReturn())
-		createVariable(_varDecl, true);
-	else if (_varDecl.isCallableParameter())
-		createVariable(_varDecl, false);
 }
 
 bool SMTChecker::visit(FunctionDefinition const& _function)
@@ -77,6 +71,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 	m_currentSequenceCounter.clear();
 	m_nextFreeSequenceCounter.clear();
 	m_conditionalExecutionHappened = false;
+	initializeLocalVariables(_function);
 	return true;
 }
 
@@ -94,9 +89,13 @@ bool SMTChecker::visit(IfStatement const& _node)
 
 	// TODO Check if condition is always true
 
-	auto touchedVariables = visitBranch(_node.trueStatement(), expr(_node.condition()));
+	visitBranch(_node.trueStatement(), expr(_node.condition()));
+	vector<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
 	if (_node.falseStatement())
-		touchedVariables += visitBranch(*_node.falseStatement(), !expr(_node.condition()));
+	{
+		visitBranch(*_node.falseStatement(), !expr(_node.condition()));
+		touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
+	}
 
 	resetVariables(touchedVariables);
 
@@ -111,20 +110,21 @@ bool SMTChecker::visit(WhileStatement const& _node)
 	// uint x = 1;
 	// while (x ++ > 0) { assert(x == 2); }
 	// solution: clear variables first, then execute and assert condition, then executed body.
+
+	auto touchedVariables = m_variableUsage->touchedVariables(_node);
+	resetVariables(touchedVariables);
 	if (_node.isDoWhile())
 	{
-		auto touchedVariables = visitBranch(_node.body());
+		visitBranch(_node.body());
-		// TODO what about the side-effects of this?
+		// TODO the assertions generated in the body should still be active in the condition
-		// If we have a "break", this might never be executed.
 		_node.condition().accept(*this);
-		resetVariables(touchedVariables);
 	}
 	else
 	{
 		_node.condition().accept(*this);
-		auto touchedVariables = visitBranch(_node.body(), expr(_node.condition()));
+		visitBranch(_node.body(), expr(_node.condition()));
-		resetVariables(touchedVariables);
 	}
+	resetVariables(touchedVariables);
 
 	return false;
 }
@@ -140,8 +140,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
 	{
 		if (_varDecl.initialValue())
 			// TODO more checks?
-			// TODO add restrictions about type (might be assignment from smaller type)
+			assignment(*_varDecl.declarations()[0], *_varDecl.initialValue());
-			m_interface->addAssertion(newValue(*_varDecl.declarations()[0]) == expr(*_varDecl.initialValue()));
 	}
 	else
 		m_errorReporter.warning(
@@ -170,9 +169,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 	{
 		Declaration const* decl = identifier->annotation().referencedDeclaration;
 		if (knownVariable(*decl))
-			// TODO more checks?
+			assignment(*decl, _assignment.rightHandSide());
-			// TODO add restrictions about type (might be assignment from smaller type)
-			m_interface->addAssertion(newValue(*decl) == expr(_assignment.rightHandSide()));
 		else
 			m_errorReporter.warning(
 				_assignment.location(),
@@ -249,23 +246,17 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 {
 	Declaration const* decl = _identifier.annotation().referencedDeclaration;
 	solAssert(decl, "");
-	if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+	if (_identifier.annotation().lValueRequested)
 	{
-		m_interface->addAssertion(expr(_identifier) == currentValue(*decl));
+		// Will be translated as part of the node that requested the lvalue.
-		return;
 	}
+	else if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
+		m_interface->addAssertion(expr(_identifier) == currentValue(*decl));
 	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
 	{
 		if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
 			return;
-		// TODO for others, clear our knowledge about storage and memory
 	}
-	m_errorReporter.warning(
-		_identifier.location(),
-		"Assertion checker does not yet support the type of this expression (" +
-		_identifier.annotation().type->toString() +
-		")."
-	);
 }
 
 void SMTChecker::endVisit(Literal const& _literal)
@@ -281,7 +272,7 @@ void SMTChecker::endVisit(Literal const& _literal)
 	else
 		m_errorReporter.warning(
 			_literal.location(),
-			"Assertion checker does not yet support the type of this expression (" +
+			"Assertion checker does not yet support the type of this literal (" +
 			_literal.annotation().type->toString() +
 			")."
 		);
@@ -379,12 +370,19 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
 					);
 }
 
-set<Declaration const*> SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
+void SMTChecker::assignment(Declaration const& _variable, Expression const& _value)
 {
-	return visitBranch(_statement, &_condition);
+	// TODO more checks?
+	// TODO add restrictions about type (might be assignment from smaller type)
+	m_interface->addAssertion(newValue(_variable) == expr(_value));
 }
 
-set<Declaration const*> SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
+void SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
+{
+	visitBranch(_statement, &_condition);
+}
+
+void SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
 {
 	VariableSequenceCounters sequenceCountersStart = m_currentSequenceCounter;
 
@@ -395,18 +393,7 @@ set<Declaration const*> SMTChecker::visitBranch(Statement const& _statement, smt
 	m_interface->pop();
 
 	m_conditionalExecutionHappened = true;
-
-	set<Declaration const*> touched;
-	for (auto const& seq: m_currentSequenceCounter)
-	{
-		if (!sequenceCountersStart.count(seq.first))
-			touched.insert(seq.first);
-		else if (sequenceCountersStart[seq.first] != seq.second)
-			touched.insert(seq.first);
-	}
 	m_currentSequenceCounter = sequenceCountersStart;
-
-	return touched;
 }
 
 void SMTChecker::checkCondition(
@@ -504,16 +491,36 @@ void SMTChecker::checkCondition(
 	m_interface->pop();
 }
 
-void SMTChecker::resetVariables(set<Declaration const*> _variables)
+void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function)
+{
+	for (auto const& variable: _function.localVariables())
+	{
+		createVariable(*variable);
+		setZeroValue(*variable);
+	}
+	for (auto const& param: _function.parameters())
+	{
+		createVariable(*param);
+		setUnknownValue(*param);
+	}
+	if (_function.returnParameterList())
+		for (auto const& retParam: _function.returnParameters())
+		{
+			createVariable(*retParam);
+			setZeroValue(*retParam);
+		}
+}
+
+void SMTChecker::resetVariables(vector<Declaration const*> _variables)
 {
 	for (auto const* decl: _variables)
 	{
 		newValue(*decl);
-		setValue(*decl, false);
+		setUnknownValue(*decl);
 	}
 }
 
-void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setToZero)
+void SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 {
 	if (dynamic_cast<IntegerType const*>(_varDecl.type().get()))
 	{
@@ -523,7 +530,6 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
 		m_currentSequenceCounter[&_varDecl] = 0;
 		m_nextFreeSequenceCounter[&_varDecl] = 1;
 		m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
-		setValue(_varDecl, _setToZero);
 	}
 	else
 		m_errorReporter.warning(
@@ -565,17 +571,17 @@ smt::Expression SMTChecker::newValue(Declaration const& _decl)
 	return currentValue(_decl);
 }
 
-void SMTChecker::setValue(Declaration const& _decl, bool _setToZero)
+void SMTChecker::setZeroValue(Declaration const& _decl)
+{
+	solAssert(_decl.type()->category() == Type::Category::Integer, "");
+	m_interface->addAssertion(currentValue(_decl) == 0);
+}
+
+void SMTChecker::setUnknownValue(Declaration const& _decl)
 {
 	auto const& intType = dynamic_cast<IntegerType const&>(*_decl.type());
-
+	m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
-	if (_setToZero)
+	m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
-		m_interface->addAssertion(currentValue(_decl) == 0);
-	else
-	{
-		m_interface->addAssertion(currentValue(_decl) >= minValue(intType));
-		m_interface->addAssertion(currentValue(_decl) <= maxValue(intType));
-	}
 }
 
 smt::Expression SMTChecker::minValue(IntegerType const& _t)

libsolidity/formal/SMTChecker.h

@@ -17,8 +17,11 @@
 
 #pragma once
 
-#include <libsolidity/ast/ASTVisitor.h>
+
 #include <libsolidity/formal/SolverInterface.h>
+
+#include <libsolidity/ast/ASTVisitor.h>
+
 #include <libsolidity/interface/ReadFile.h>
 
 #include <map>
@@ -29,6 +32,7 @@ namespace dev
 namespace solidity
 {
 
+class VariableUsage;
 class ErrorReporter;
 
 class SMTChecker: private ASTConstVisitor
@@ -61,11 +65,12 @@ private:
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);
 
+	void assignment(Declaration const& _variable, Expression const& _value);
+
 	// Visits the branch given by the statement, pushes and pops the SMT checker.
-	// @returns the set of touched declarations
 	// @param _condition if present, asserts that this condition is true within the branch.
-	std::set<Declaration const*> visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
+	void visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
-	std::set<Declaration const*> visitBranch(Statement const& _statement, smt::Expression _condition);
+	void visitBranch(Statement const& _statement, smt::Expression _condition);
 
 	void checkCondition(
 		smt::Expression _condition,
@@ -75,8 +80,9 @@ private:
 		smt::Expression* _additionalValue = nullptr
 	);
 
-	void resetVariables(std::set<Declaration const*> _variables);
+	void initializeLocalVariables(FunctionDefinition const& _function);
-	void createVariable(VariableDeclaration const& _varDecl, bool _setToZero);
+	void resetVariables(std::vector<Declaration const*> _variables);
+	void createVariable(VariableDeclaration const& _varDecl);
 
 	static std::string uniqueSymbol(Declaration const& _decl);
 	static std::string uniqueSymbol(Expression const& _expr);
@@ -94,8 +100,10 @@ private:
 	/// sequence number to this value and returns the expression.
 	smt::Expression newValue(Declaration const& _decl);
 
-	/// Sets the value of the declaration either to zero or to its intrinsic range.
+	/// Sets the value of the declaration to zero.
-	void setValue(Declaration const& _decl, bool _setToZero);
+	void setZeroValue(Declaration const& _decl);
+	/// Resets the variable to an unknown value (in its range).
+	void setUnknownValue(Declaration const& decl);
 
 	static smt::Expression minValue(IntegerType const& _t);
 	static smt::Expression maxValue(IntegerType const& _t);
@@ -110,6 +118,7 @@ private:
 	smt::Expression var(Declaration const& _decl);
 
 	std::shared_ptr<smt::SolverInterface> m_interface;
+	std::shared_ptr<VariableUsage> m_variableUsage;
 	bool m_conditionalExecutionHappened = false;
 	std::map<Declaration const*, int> m_currentSequenceCounter;
 	std::map<Declaration const*, int> m_nextFreeSequenceCounter;

libsolidity/formal/VariableUsage.cpp

@@ -0,0 +1,80 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/VariableUsage.h>
+
+#include <libsolidity/ast/ASTVisitor.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+VariableUsage::VariableUsage(ASTNode const& _node)
+{
+	auto nodeFun = [&](ASTNode const& n) -> bool
+	{
+		if (Identifier const* identifier = dynamic_cast<decltype(identifier)>(&n))
+		{
+			Declaration const* declaration = identifier->annotation().referencedDeclaration;
+			solAssert(declaration, "");
+			if (VariableDeclaration const* varDecl = dynamic_cast<VariableDeclaration const*>(declaration))
+				if (
+					varDecl->isLocalVariable() &&
+					identifier->annotation().lValueRequested &&
+					varDecl->annotation().type->isValueType()
+				)
+					m_touchedVariable[&n] = varDecl;
+		}
+		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<Declaration const*> VariableUsage::touchedVariables(ASTNode const& _node) const
+{
+	if (!m_children.count(&_node) && !m_touchedVariable.count(&_node))
+		return {};
+
+	set<Declaration const*> touched;
+	vector<ASTNode const*> toVisit;
+	toVisit.push_back(&_node);
+
+	while (!toVisit.empty())
+	{
+		ASTNode const* n = toVisit.back();
+		toVisit.pop_back();
+		if (m_children.count(n))
+		{
+			solAssert(!m_touchedVariable.count(n), "");
+			toVisit += m_children.at(n);
+		}
+		else
+		{
+			solAssert(m_touchedVariable.count(n), "");
+			touched.insert(m_touchedVariable.at(n));
+		}
+	}
+
+	return {touched.begin(), touched.end()};
+}

libsolidity/formal/VariableUsage.h

@@ -0,0 +1,50 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <map>
+#include <set>
+#include <vector>
+
+namespace dev
+{
+namespace solidity
+{
+
+class ASTNode;
+class Declaration;
+
+/**
+ * This class collects information about which local variables of value type
+ * are modified in which parts of the AST.
+ */
+class VariableUsage
+{
+public:
+	explicit VariableUsage(ASTNode const& _node);
+
+	std::vector<Declaration const*> touchedVariables(ASTNode const& _node) const;
+
+private:
+	// Variable touched by a specific AST node.
+	std::map<ASTNode const*, Declaration const*> m_touchedVariable;
+	std::map<ASTNode const*, std::vector<ASTNode const*>> m_children;
+};
+
+}
+}