[SMTChecker] Refactoring types

libsolidity/formal/SMTChecker.cpp

@@ -22,6 +22,7 @@
 #include <libsolidity/formal/SSAVariable.h>
 #include <libsolidity/formal/SymbolicIntVariable.h>
 #include <libsolidity/formal/VariableUsage.h>
+#include <libsolidity/formal/SymbolicTypes.h>
 
 #include <libsolidity/interface/ErrorReporter.h>
 
@@ -116,9 +117,7 @@ bool SMTChecker::visit(IfStatement const& _node)
 		touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
 	}
 	else
-	{
+		countersEndFalse = copyVariableSequenceCounters();
-		countersEndFalse = m_variables;
-	}
 
 	mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse);
 
@@ -176,7 +175,6 @@ bool SMTChecker::visit(ForStatement const& _node)
 			checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE.");
 	}
 
-	VariableSequenceCounters sequenceCountersStart = m_variables;
 	m_interface->push();
 	if (_node.condition())
 		m_interface->addAssertion(expr(*_node.condition()));
@@ -187,7 +185,6 @@ bool SMTChecker::visit(ForStatement const& _node)
 	m_interface->pop();
 
 	m_loopExecutionHappened = true;
-	std::swap(sequenceCountersStart, m_variables);
 
 	resetVariables(touchedVariables);
 
@@ -220,7 +217,7 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 			_assignment.location(),
 			"Assertion checker does not yet implement compound assignment."
 		);
-	else if (!SSAVariable::isSupportedType(_assignment.annotation().type->category()))
+	else if (!isSupportedType(_assignment.annotation().type->category()))
 		m_errorReporter.warning(
 			_assignment.location(),
 			"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
@@ -281,7 +278,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 	{
 	case Token::Not: // !
 	{
-		solAssert(SSAVariable::isBool(_op.annotation().type->category()), "");
+		solAssert(isBool(_op.annotation().type->category()), "");
 		defineExpr(_op, !expr(_op.subExpression()));
 		break;
 	}
@@ -289,7 +286,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 	case Token::Dec: // -- (pre- or postfix)
 	{
 
-		solAssert(SSAVariable::isInteger(_op.annotation().type->category()), "");
+		solAssert(isInteger(_op.annotation().type->category()), "");
 		solAssert(_op.subExpression().annotation().lValueRequested, "");
 		if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
 		{
@@ -461,7 +458,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 	{
 		// Will be translated as part of the node that requested the lvalue.
 	}
-	else if (SSAVariable::isSupportedType(_identifier.annotation().type->category()))
+	else if (isSupportedType(_identifier.annotation().type->category()))
 	{
 		if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration))
 			defineExpr(_identifier, currentValue(*decl));
@@ -567,13 +564,13 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 void SMTChecker::compareOperation(BinaryOperation const& _op)
 {
 	solAssert(_op.annotation().commonType, "");
-	if (SSAVariable::isSupportedType(_op.annotation().commonType->category()))
+	if (isSupportedType(_op.annotation().commonType->category()))
 	{
 		smt::Expression left(expr(_op.leftExpression()));
 		smt::Expression right(expr(_op.rightExpression()));
 		Token::Value op = _op.getOperator();
 		shared_ptr<smt::Expression> value;
-		if (SSAVariable::isInteger(_op.annotation().commonType->category()))
+		if (isInteger(_op.annotation().commonType->category()))
 		{
 			value = make_shared<smt::Expression>(
 				op == Token::Equal ? (left == right) :
@@ -586,7 +583,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
 		}
 		else // Bool
 		{
-			solUnimplementedAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "Operation not yet supported");
+			solUnimplementedAssert(isBool(_op.annotation().commonType->category()), "Operation not yet supported");
 			value = make_shared<smt::Expression>(
 				op == Token::Equal ? (left == right) :
 				/*op == Token::NotEqual*/ (left != right)
@@ -656,17 +653,15 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s
 
 SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
 {
-	VariableSequenceCounters beforeVars = m_variables;
+	auto countersBeforeBranch = copyVariableSequenceCounters();
-
 	if (_condition)
 		pushPathCondition(*_condition);
 	_statement.accept(*this);
 	if (_condition)
 		popPathCondition();
-
+	auto countersAfterBranch = copyVariableSequenceCounters();
-	std::swap(m_variables, beforeVars);
+	resetVariableCounters(countersBeforeBranch);
-
+	return countersAfterBranch;
-	return beforeVars;
 }
 
 void SMTChecker::checkCondition(
@@ -905,8 +900,8 @@ void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _varia
 	for (auto const* decl: uniqueVars)
 	{
 		solAssert(_countersEndTrue.count(decl) && _countersEndFalse.count(decl), "");
-		int trueCounter = _countersEndTrue.at(decl).index();
+		int trueCounter = _countersEndTrue.at(decl);
-		int falseCounter = _countersEndFalse.at(decl).index();
+		int falseCounter = _countersEndFalse.at(decl);
 		solAssert(trueCounter != falseCounter, "");
 		m_interface->addAssertion(newValue(*decl) == smt::Expression::ite(
 			_condition,
@@ -921,10 +916,11 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 	// This might be the case for multiple calls to the same function.
 	if (hasVariable(_varDecl))
 		return true;
-	else if (SSAVariable::isSupportedType(_varDecl.type()->category()))
+	auto const& type = _varDecl.type();
+	if (isSupportedType(type->category()))
 	{
 		solAssert(m_variables.count(&_varDecl) == 0, "");
-		m_variables.emplace(&_varDecl, SSAVariable(*_varDecl.type(), _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface));
+		m_variables.emplace(&_varDecl, newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface));
 		return true;
 	}
 	else
@@ -950,32 +946,31 @@ bool SMTChecker::knownVariable(VariableDeclaration const& _decl)
 smt::Expression SMTChecker::currentValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	return m_variables.at(&_decl)();
+	return m_variables.at(&_decl)->current();
 }
 
 smt::Expression SMTChecker::valueAtSequence(VariableDeclaration const& _decl, int _sequence)
 {
 	solAssert(knownVariable(_decl), "");
-	return m_variables.at(&_decl)(_sequence);
+	return m_variables.at(&_decl)->valueAtSequence(_sequence);
 }
 
 smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	++m_variables.at(&_decl);
+	return m_variables.at(&_decl)->increase();
-	return m_variables.at(&_decl)();
 }
 
 void SMTChecker::setZeroValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	m_variables.at(&_decl).setZeroValue();
+	m_variables.at(&_decl)->setZeroValue();
 }
 
 void SMTChecker::setUnknownValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	m_variables.at(&_decl).setUnknownValue();
+	m_variables.at(&_decl)->setUnknownValue();
 }
 
 smt::Expression SMTChecker::expr(Expression const& _e)
@@ -1074,3 +1069,17 @@ bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef)
 {
 	return contains(m_functionPath, _funDef);
 }
+
+SMTChecker::VariableSequenceCounters SMTChecker::copyVariableSequenceCounters()
+{
+	VariableSequenceCounters counters;
+	for (auto var: m_variables)
+		counters.emplace(var.first, var.second->index());
+	return counters;
+}
+
+void SMTChecker::resetVariableCounters(VariableSequenceCounters const& _counters)
+{
+	for (auto var: _counters)
+		m_variables.at(var.first)->index() = var.second;
+}

libsolidity/formal/SMTChecker.h

@@ -19,14 +19,14 @@
 
 
 #include <libsolidity/formal/SolverInterface.h>
-
+#include <libsolidity/formal/SymbolicVariable.h>
-#include <libsolidity/formal/SSAVariable.h>
 
 #include <libsolidity/ast/ASTVisitor.h>
 
 #include <libsolidity/interface/ReadFile.h>
 
 #include <map>
+#include <unordered_map>
 #include <string>
 #include <vector>
 
@@ -86,7 +86,7 @@ private:
 	void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location);
 
 	/// Maps a variable to an SSA index.
-	using VariableSequenceCounters = std::map<VariableDeclaration const*, SSAVariable>;
+	using VariableSequenceCounters = std::unordered_map<VariableDeclaration const*, int>;
 
 	/// Visits the branch given by the statement, pushes and pops the current path conditions.
 	/// @param _condition if present, asserts that this condition is true within the branch.
@@ -176,13 +176,18 @@ private:
 	/// Checks if VariableDeclaration was seen.
 	bool hasVariable(VariableDeclaration const& _e) const;
 
+	/// Copy the SSA indices of m_variables.
+	VariableSequenceCounters copyVariableSequenceCounters();
+	/// Resets the variable counters.
+	void resetVariableCounters(VariableSequenceCounters const& _counters); 
+
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::shared_ptr<VariableUsage> m_variableUsage;
 	bool m_loopExecutionHappened = false;
 	/// An Expression may have multiple smt::Expression due to
 	/// repeated calls to the same function.
 	std::multimap<Expression const*, smt::Expression> m_expressions;
-	std::map<VariableDeclaration const*, SSAVariable> m_variables;
+	std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;
 

libsolidity/formal/SSAVariable.cpp

@@ -17,46 +17,12 @@
 
 #include <libsolidity/formal/SSAVariable.h>
 
-#include <libsolidity/formal/SymbolicBoolVariable.h>
-#include <libsolidity/formal/SymbolicIntVariable.h>
-
-#include <libsolidity/ast/AST.h>
-
 using namespace std;
-using namespace dev;
 using namespace dev::solidity;
 
-SSAVariable::SSAVariable(
+SSAVariable::SSAVariable()
-	Type const& _type,
-	string const& _uniqueName,
-	smt::SolverInterface& _interface
-)
 {
 	resetIndex();
-
-	if (isInteger(_type.category()))
-		m_symbolicVar = make_shared<SymbolicIntVariable>(_type, _uniqueName, _interface);
-	else if (isBool(_type.category()))
-		m_symbolicVar = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _interface);
-	else
-	{
-		solAssert(false, "");
-	}
-}
-
-bool SSAVariable::isSupportedType(Type::Category _category)
-{
-	return isInteger(_category) || isBool(_category);
-}
-
-bool SSAVariable::isInteger(Type::Category _category)
-{
-	return _category == Type::Category::Integer || _category == Type::Category::Address;
-}
-
-bool SSAVariable::isBool(Type::Category _category)
-{
-	return _category == Type::Category::Bool;
 }
 
 void SSAVariable::resetIndex()
@@ -65,23 +31,3 @@ void SSAVariable::resetIndex()
 	m_nextFreeSequenceCounter.reset (new int);
 	*m_nextFreeSequenceCounter = 1;
 }
-
-int SSAVariable::index() const
-{
-	return m_currentSequenceCounter;
-}
-
-int SSAVariable::next() const
-{
-	return *m_nextFreeSequenceCounter;
-}
-
-void SSAVariable::setZeroValue()
-{
-	m_symbolicVar->setZeroValue(index());
-}
-
-void SSAVariable::setUnknownValue()
-{
-	m_symbolicVar->setUnknownValue(index());
-}

libsolidity/formal/SSAVariable.h

@@ -17,8 +17,6 @@
 
 #pragma once
 
-#include <libsolidity/formal/SymbolicVariable.h>
-
 #include <memory>
 
 namespace dev
@@ -32,53 +30,19 @@ namespace solidity
 class SSAVariable
 {
 public:
-	/// @param _type Forwarded to the symbolic var.
+	SSAVariable();
-	/// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver.
-	SSAVariable(
-		Type const& _type,
-		std::string const& _uniqueName,
-		smt::SolverInterface& _interface
-	);
-
 	void resetIndex();
 
 	/// This function returns the current index of this SSA variable.
-	int index() const;
+	int index() const { return m_currentSequenceCounter; }
-	/// This function returns the next free index of this SSA variable.
+	int& index() { return m_currentSequenceCounter; }
-	int next() const;
 
 	int operator++()
 	{
 		return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++;
 	}
 
-	smt::Expression operator()() const
-	{
-		return valueAtSequence(index());
-	}
-
-	smt::Expression operator()(int _seq) const
-	{
-		return valueAtSequence(_seq);
-	}
-
-	/// These two functions forward the call to the symbolic var
-	/// which generates the constraints according to the type.
-	void setZeroValue();
-	void setUnknownValue();
-
-	/// So far Int and Bool are supported.
-	static bool isSupportedType(Type::Category _category);
-	static bool isInteger(Type::Category _category);
-	static bool isBool(Type::Category _category);
-
 private:
-	smt::Expression valueAtSequence(int _seq) const
-	{
-		return (*m_symbolicVar)(_seq);
-	}
-
-	std::shared_ptr<SymbolicVariable> m_symbolicVar = nullptr;
 	int m_currentSequenceCounter;
 	/// The next free sequence counter is a shared pointer because we want
 	/// the copy and the copied to share it.

libsolidity/formal/SymbolicBoolVariable.cpp

@@ -17,8 +17,6 @@
 
 #include <libsolidity/formal/SymbolicBoolVariable.h>
 
-#include <libsolidity/ast/AST.h>
-
 using namespace std;
 using namespace dev;
 using namespace dev::solidity;
@@ -38,11 +36,11 @@ smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const
 	return m_interface.newBool(uniqueSymbol(_seq));
 }
 
-void SymbolicBoolVariable::setZeroValue(int _seq)
+void SymbolicBoolVariable::setZeroValue()
 {
-	m_interface.addAssertion(valueAtSequence(_seq) == smt::Expression(false));
+	m_interface.addAssertion(current() == smt::Expression(false));
 }
 
-void SymbolicBoolVariable::setUnknownValue(int)
+void SymbolicBoolVariable::setUnknownValue()
 {
 }

libsolidity/formal/SymbolicBoolVariable.h

@@ -37,9 +37,9 @@ public:
 	);
 
 	/// Sets the var to false.
-	void setZeroValue(int _seq);
+	void setZeroValue();
-	/// Does nothing since the SMT solver already knows the valid values.
+	/// Does nothing since the SMT solver already knows the valid values for Bool.
-	void setUnknownValue(int _seq);
+	void setUnknownValue();
 
 protected:
 	smt::Expression valueAtSequence(int _seq) const;

libsolidity/formal/SymbolicIntVariable.cpp

@@ -40,26 +40,26 @@ smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const
 	return m_interface.newInteger(uniqueSymbol(_seq));
 }
 
-void SymbolicIntVariable::setZeroValue(int _seq)
+void SymbolicIntVariable::setZeroValue()
 {
-	m_interface.addAssertion(valueAtSequence(_seq) == 0);
+	m_interface.addAssertion(current() == 0);
 }
 
-void SymbolicIntVariable::setUnknownValue(int _seq)
+void SymbolicIntVariable::setUnknownValue()
 {
 	if (m_type.category() == Type::Category::Integer)
 	{
 		auto intType = dynamic_cast<IntegerType const*>(&m_type);
 		solAssert(intType, "");
-		m_interface.addAssertion(valueAtSequence(_seq) >= minValue(*intType));
+		m_interface.addAssertion(current() >= minValue(*intType));
-		m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(*intType));
+		m_interface.addAssertion(current() <= maxValue(*intType));
 	}
 	else
 	{
 		solAssert(m_type.category() == Type::Category::Address, "");
 		IntegerType addrType{160};
-		m_interface.addAssertion(valueAtSequence(_seq) >= minValue(addrType));
+		m_interface.addAssertion(current() >= minValue(addrType));
-		m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(addrType));
+		m_interface.addAssertion(current() <= maxValue(addrType));
 	}
 }
 

libsolidity/formal/SymbolicIntVariable.h

@@ -37,9 +37,9 @@ public:
 	);
 
 	/// Sets the var to 0.
-	void setZeroValue(int _seq);
+	void setZeroValue();
 	/// Sets the variable to the full valid value range.
-	void setUnknownValue(int _seq);
+	void setUnknownValue();
 
 	static smt::Expression minValue(IntegerType const& _t);
 	static smt::Expression maxValue(IntegerType const& _t);

libsolidity/formal/SymbolicTypes.cpp

@@ -0,0 +1,72 @@
+/*
+	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/SymbolicTypes.h>
+
+#include <libsolidity/formal/SymbolicBoolVariable.h>
+#include <libsolidity/formal/SymbolicIntVariable.h>
+
+#include <libsolidity/ast/Types.h>
+
+#include <memory>
+
+using namespace std;
+using namespace dev::solidity;
+
+bool dev::solidity::isSupportedType(Type::Category _category)
+{
+	return isInteger(_category) || isBool(_category);
+}
+
+bool dev::solidity::isSupportedType(Type const& _type)
+{
+	return isSupportedType(_type.category());
+}
+
+bool dev::solidity::isInteger(Type::Category _category)
+{
+	return _category == Type::Category::Integer || _category == Type::Category::Address;
+}
+
+bool dev::solidity::isInteger(Type const& _type)
+{
+	return isInteger(_type.category());
+}
+
+bool dev::solidity::isBool(Type::Category _category)
+{
+	return _category == Type::Category::Bool;
+}
+
+bool dev::solidity::isBool(Type const& _type)
+{
+	return isBool(_type.category());
+}
+
+shared_ptr<SymbolicVariable> dev::solidity::newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver)
+{
+	if (!isSupportedType(_type))
+		return nullptr;
+	if (isBool(_type.category()))
+		return make_shared<SymbolicBoolVariable>(_type, _uniqueName, _solver);
+	else if (isInteger(_type.category()))
+		return make_shared<SymbolicIntVariable>(_type, _uniqueName, _solver);
+	else
+		solAssert(false, "");
+}
+
+

libsolidity/formal/SymbolicTypes.h

@@ -0,0 +1,45 @@
+/*
+	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 <libsolidity/formal/SolverInterface.h>
+#include <libsolidity/formal/SymbolicVariable.h>
+
+#include <libsolidity/ast/AST.h>
+#include <libsolidity/ast/Types.h>
+
+namespace dev
+{
+namespace solidity
+{
+
+/// So far int, bool and address are supported.
+/// Returns true if type is supported.
+bool isSupportedType(Type::Category _category);
+bool isSupportedType(Type const& _type);
+
+bool isInteger(Type::Category _category);
+bool isInteger(Type const& _type);
+
+bool isBool(Type::Category _category);
+bool isBool(Type const& _type);
+
+std::shared_ptr<SymbolicVariable> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver);
+
+}
+}

libsolidity/formal/SymbolicVariable.cpp

@@ -30,7 +30,8 @@ SymbolicVariable::SymbolicVariable(
 ):
 	m_type(_type),
 	m_uniqueName(_uniqueName),
-	m_interface(_interface)
+	m_interface(_interface),
+	m_ssa(make_shared<SSAVariable>())
 {
 }
 

libsolidity/formal/SymbolicVariable.h

@@ -17,6 +17,8 @@
 
 #pragma once
 
+#include <libsolidity/formal/SSAVariable.h>
+
 #include <libsolidity/formal/SolverInterface.h>
 
 #include <libsolidity/ast/Types.h>
@@ -43,25 +45,35 @@ public:
 	);
 	virtual ~SymbolicVariable() = default;
 
-	smt::Expression operator()(int _seq) const
+	smt::Expression current() const
 	{
-		return valueAtSequence(_seq);
+		return valueAtSequence(m_ssa->index());
 	}
 
-	std::string uniqueSymbol(int _seq) const;
+	virtual smt::Expression valueAtSequence(int _seq) const = 0;
+
+	smt::Expression increase()
+	{
+		++(*m_ssa);
+		return current();
+	}
+
+	int index() const { return m_ssa->index(); }
+	int& index() { return m_ssa->index(); }
 
 	/// Sets the var to the default value of its type.
-	virtual void setZeroValue(int _seq) = 0;
+	virtual void setZeroValue() = 0;
 	/// The unknown value is the full range of valid values,
 	/// and that's sub-type dependent.
-	virtual void setUnknownValue(int _seq) = 0;
+	virtual void setUnknownValue() = 0;
 
 protected:
-	virtual smt::Expression valueAtSequence(int _seq) const = 0;
+	std::string uniqueSymbol(int _seq) const;
 
 	Type const& m_type;
 	std::string m_uniqueName;
 	smt::SolverInterface& m_interface;
+	std::shared_ptr<SSAVariable> m_ssa = nullptr;
 };
 
 }