Merge pull request #5235 from ethereum/smt_refactor_types

[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>
 
@@ -107,20 +108,18 @@ bool SMTChecker::visit(IfStatement const& _node)
 	if (isRootFunction())
 		checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE.");
 
-	auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
+	auto indicesEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition()));
 	vector<VariableDeclaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement());
-	decltype(countersEndTrue) countersEndFalse;
+	decltype(indicesEndTrue) indicesEndFalse;
 	if (_node.falseStatement())
 	{
-		countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
+		indicesEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition()));
 		touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement());
 	}
 	else
-	{
-		countersEndFalse = m_variables;
-	}
+		indicesEndFalse = copyVariableIndices();
 
-	mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse);
+	mergeVariables(touchedVariables, expr(_node.condition()), indicesEndTrue, indicesEndFalse);
 
 	return false;
 }
@@ -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()
@@ -260,14 +257,14 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
 void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location)
 {
 	checkCondition(
-		_value < SymbolicIntVariable::minValue(_type),
+		_value < minValue(_type),
 		_location,
 		"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
 		"<result>",
 		&_value
 	);
 	checkCondition(
-		_value > SymbolicIntVariable::maxValue(_type),
+		_value > maxValue(_type),
 		_location,
 		"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
 		"<result>",
@@ -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 (isNumber(_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)
@@ -649,24 +646,22 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio
 	m_interface->addAssertion(newValue(_variable) == _value);
 }
 
-SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
+SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
 {
 	return visitBranch(_statement, &_condition);
 }
 
-SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
+SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition)
 {
-	VariableSequenceCounters beforeVars = m_variables;
-
+	auto indicesBeforeBranch = copyVariableIndices();
 	if (_condition)
 		pushPathCondition(*_condition);
 	_statement.accept(*this);
 	if (_condition)
 		popPathCondition();
-
-	std::swap(m_variables, beforeVars);
-
-	return beforeVars;
+	auto indicesAfterBranch = copyVariableIndices();
+	resetVariableIndices(indicesBeforeBranch);
+	return indicesAfterBranch;
 }
 
 void SMTChecker::checkCondition(
@@ -899,19 +894,19 @@ void SMTChecker::resetVariables(vector<VariableDeclaration const*> _variables)
 	}
 }
 
-void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse)
+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());
 	for (auto const* decl: uniqueVars)
 	{
-		solAssert(_countersEndTrue.count(decl) && _countersEndFalse.count(decl), "");
-		int trueCounter = _countersEndTrue.at(decl).index();
-		int falseCounter = _countersEndFalse.at(decl).index();
-		solAssert(trueCounter != falseCounter, "");
+		solAssert(_indicesEndTrue.count(decl) && _indicesEndFalse.count(decl), "");
+		int trueIndex = _indicesEndTrue.at(decl);
+		int falseIndex = _indicesEndFalse.at(decl);
+		solAssert(trueIndex != falseIndex, "");
 		m_interface->addAssertion(newValue(*decl) == smt::Expression::ite(
 			_condition,
-			valueAtSequence(*decl, trueCounter),
-			valueAtSequence(*decl, falseCounter))
+			valueAtIndex(*decl, trueIndex),
+			valueAtIndex(*decl, falseIndex))
 		);
 	}
 }
@@ -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)->currentValue();
 }
 
-smt::Expression SMTChecker::valueAtSequence(VariableDeclaration const& _decl, int _sequence)
+smt::Expression SMTChecker::valueAtIndex(VariableDeclaration const& _decl, int _index)
 {
 	solAssert(knownVariable(_decl), "");
-	return m_variables.at(&_decl)(_sequence);
+	return m_variables.at(&_decl)->valueAtIndex(_index);
 }
 
 smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl)
 {
 	solAssert(knownVariable(_decl), "");
-	++m_variables.at(&_decl);
-	return m_variables.at(&_decl)();
+	return m_variables.at(&_decl)->increaseIndex();
 }
 
 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::VariableIndices SMTChecker::copyVariableIndices()
+{
+	VariableIndices indices;
+	for (auto const& var: m_variables)
+		indices.emplace(var.first, var.second->index());
+	return indices;
+}
+
+void SMTChecker::resetVariableIndices(VariableIndices const& _indices)
+{
+	for (auto const& var: _indices)
+		m_variables.at(var.first)->index() = var.second;
+}

libsolidity/formal/SMTChecker.h

@@ -19,14 +19,14 @@
 
 
 #include <libsolidity/formal/SolverInterface.h>
-
-#include <libsolidity/formal/SSAVariable.h>
+#include <libsolidity/formal/SymbolicVariable.h>
 
 #include <libsolidity/ast/ASTVisitor.h>
 
 #include <libsolidity/interface/ReadFile.h>
 
 #include <map>
+#include <unordered_map>
 #include <string>
 #include <vector>
 
@@ -86,13 +86,13 @@ 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 VariableIndices = 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.
-	/// @returns the variable sequence counter after visiting the branch.
-	VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
-	VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression _condition);
+	/// @returns the variable indices after visiting the branch.
+	VariableIndices visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr);
+	VariableIndices visitBranch(Statement const& _statement, smt::Expression _condition);
 
 	/// Check that a condition can be satisfied.
 	void checkCondition(
@@ -125,7 +125,7 @@ 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, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse);
+	void mergeVariables(std::vector<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.
 	bool createVariable(VariableDeclaration const& _varDecl);
@@ -133,16 +133,16 @@ private:
 	static std::string uniqueSymbol(Expression const& _expr);
 
 	/// @returns true if _delc is a variable that is known at the current point, i.e.
-	/// has a valid sequence number
+	/// has a valid index
 	bool knownVariable(VariableDeclaration const& _decl);
 	/// @returns an expression denoting the value of the variable declared in @a _decl
 	/// at the current point.
 	smt::Expression currentValue(VariableDeclaration const& _decl);
 	/// @returns an expression denoting the value of the variable declared in @a _decl
-	/// at the given sequence point. Does not ensure that this sequence point exists.
-	smt::Expression valueAtSequence(VariableDeclaration const& _decl, int _sequence);
-	/// Allocates a new sequence number for the declaration, updates the current
-	/// sequence number to this value and returns the expression.
+	/// at the given index. Does not ensure that this index exists.
+	smt::Expression valueAtIndex(VariableDeclaration const& _decl, int _index);
+	/// Allocates a new index for the declaration, updates the current
+	/// index to this value and returns the expression.
 	smt::Expression newValue(VariableDeclaration const& _decl);
 
 	/// Sets the value of the declaration to zero.
@@ -176,13 +176,18 @@ private:
 	/// Checks if VariableDeclaration was seen.
 	bool hasVariable(VariableDeclaration const& _e) const;
 
+	/// Copy the SSA indices of m_variables.
+	VariableIndices copyVariableIndices();
+	/// Resets the variable indices.
+	void resetVariableIndices(VariableIndices const& _indices);
+
 	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,71 +17,17 @@
 
 #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(
-	Type const& _type,
-	string const& _uniqueName,
-	smt::SolverInterface& _interface
-)
+SSAVariable::SSAVariable()
 {
 	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()
 {
-	m_currentSequenceCounter = 0;
-	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());
+	m_currentIndex = 0;
+	m_nextFreeIndex.reset (new int);
+	*m_nextFreeIndex = 1;
 }

libsolidity/formal/SSAVariable.h

@@ -17,8 +17,6 @@
 
 #pragma once
 
-#include <libsolidity/formal/SymbolicVariable.h>
-
 #include <memory>
 
 namespace dev
@@ -32,57 +30,23 @@ namespace solidity
 class SSAVariable
 {
 public:
-	/// @param _type Forwarded to the symbolic var.
-	/// @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
-	);
-
+	SSAVariable();
 	void resetIndex();
 
 	/// This function returns the current index of this SSA variable.
-	int index() const;
-	/// This function returns the next free index of this SSA variable.
-	int next() const;
+	int index() const { return m_currentIndex; }
+	int& index() { return m_currentIndex; }
 
 	int operator++()
 	{
-		return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++;
+		return m_currentIndex = (*m_nextFreeIndex)++;
 	}
 
-	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
+	int m_currentIndex;
+	/// The next free index is a shared pointer because we want
 	/// the copy and the copied to share it.
-	std::shared_ptr<int> m_nextFreeSequenceCounter;
+	std::shared_ptr<int> m_nextFreeIndex;
 };
 
 }

libsolidity/formal/SymbolicAddressVariable.cpp

@@ -0,0 +1,41 @@
+/*
+	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/SymbolicAddressVariable.h>
+
+#include <libsolidity/formal/SymbolicTypes.h>
+
+using namespace std;
+using namespace dev;
+using namespace dev::solidity;
+
+SymbolicAddressVariable::SymbolicAddressVariable(
+	Type const& _type,
+	string const& _uniqueName,
+	smt::SolverInterface& _interface
+):
+	SymbolicIntVariable(_type, _uniqueName, _interface)
+{
+	solAssert(isAddress(_type.category()), "");
+}
+
+void SymbolicAddressVariable::setUnknownValue()
+{
+	IntegerType intType{160};
+	m_interface.addAssertion(currentValue() >= minValue(intType));
+	m_interface.addAssertion(currentValue() <= maxValue(intType));
+}

libsolidity/formal/SymbolicAddressVariable.h

@@ -0,0 +1,44 @@
+/*
+	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/SymbolicIntVariable.h>
+
+namespace dev
+{
+namespace solidity
+{
+
+/**
+ * Specialization of SymbolicVariable for Address
+ */
+class SymbolicAddressVariable: public SymbolicIntVariable
+{
+public:
+	SymbolicAddressVariable(
+		Type const& _type,
+		std::string const& _uniqueName,
+		smt::SolverInterface& _interface
+	);
+
+	/// Sets the variable to the full valid value range.
+	void setUnknownValue();
+};
+
+}
+}

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;
@@ -33,16 +31,16 @@ SymbolicBoolVariable::SymbolicBoolVariable(
 	solAssert(_type.category() == Type::Category::Bool, "");
 }
 
-smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const
+smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const
 {
-	return m_interface.newBool(uniqueSymbol(_seq));
+	return m_interface.newBool(uniqueSymbol(_index));
 }
 
-void SymbolicBoolVariable::setZeroValue(int _seq)
+void SymbolicBoolVariable::setZeroValue()
 {
-	m_interface.addAssertion(valueAtSequence(_seq) == smt::Expression(false));
+	m_interface.addAssertion(currentValue() == smt::Expression(false));
 }
 
-void SymbolicBoolVariable::setUnknownValue(int)
+void SymbolicBoolVariable::setUnknownValue()
 {
 }

libsolidity/formal/SymbolicBoolVariable.h

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

libsolidity/formal/SymbolicIntVariable.cpp

@@ -17,6 +17,8 @@
 
 #include <libsolidity/formal/SymbolicIntVariable.h>
 
+#include <libsolidity/formal/SymbolicTypes.h>
+
 using namespace std;
 using namespace dev;
 using namespace dev::solidity;
@@ -28,47 +30,23 @@ SymbolicIntVariable::SymbolicIntVariable(
 ):
 	SymbolicVariable(_type, _uniqueName, _interface)
 {
-	solAssert(
-		_type.category() == Type::Category::Integer ||
-		_type.category() == Type::Category::Address,
-		""
-	);
+	solAssert(isNumber(_type.category()), "");
 }
 
-smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const
+smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
 {
-	return m_interface.newInteger(uniqueSymbol(_seq));
+	return m_interface.newInteger(uniqueSymbol(_index));
 }
 
-void SymbolicIntVariable::setZeroValue(int _seq)
+void SymbolicIntVariable::setZeroValue()
 {
-	m_interface.addAssertion(valueAtSequence(_seq) == 0);
+	m_interface.addAssertion(currentValue() == 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(valueAtSequence(_seq) <= maxValue(*intType));
-	}
-	else
-	{
-		solAssert(m_type.category() == Type::Category::Address, "");
-		IntegerType addrType{160};
-		m_interface.addAssertion(valueAtSequence(_seq) >= minValue(addrType));
-		m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(addrType));
-	}
-}
-
-smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t)
-{
-	return smt::Expression(_t.minValue());
-}
-
-smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t)
-{
-	return smt::Expression(_t.maxValue());
+	auto intType = dynamic_cast<IntegerType const*>(&m_type);
+	solAssert(intType, "");
+	m_interface.addAssertion(currentValue() >= minValue(*intType));
+	m_interface.addAssertion(currentValue() <= maxValue(*intType));
 }

libsolidity/formal/SymbolicIntVariable.h

@@ -37,15 +37,12 @@ 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);
-
-	static smt::Expression minValue(IntegerType const& _t);
-	static smt::Expression maxValue(IntegerType const& _t);
+	virtual void setUnknownValue();
 
 protected:
-	smt::Expression valueAtSequence(int _seq) const;
+	smt::Expression valueAtIndex(int _index) const;
 };
 
 }

libsolidity/formal/SymbolicTypes.cpp

@@ -0,0 +1,110 @@
+/*
+	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/formal/SymbolicAddressVariable.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) ||
+		isAddress(_category) ||
+		isBool(_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 if (isAddress(_type.category()))
+		return make_shared<SymbolicAddressVariable>(_type, _uniqueName, _solver);
+	else
+		solAssert(false, "");
+}
+
+bool dev::solidity::isSupportedType(Type const& _type)
+{
+	return isSupportedType(_type.category());
+}
+
+bool dev::solidity::isInteger(Type::Category _category)
+{
+	return _category == Type::Category::Integer;
+}
+
+bool dev::solidity::isInteger(Type const& _type)
+{
+	return isInteger(_type.category());
+}
+
+bool dev::solidity::isAddress(Type::Category _category)
+{
+	return _category == Type::Category::Address;
+}
+
+bool dev::solidity::isAddress(Type const& _type)
+{
+	return isAddress(_type.category());
+}
+
+bool dev::solidity::isNumber(Type::Category _category)
+{
+	return isInteger(_category) ||
+		isAddress(_category);
+}
+
+bool dev::solidity::isNumber(Type const& _type)
+{
+	return isNumber(_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());
+}
+
+smt::Expression dev::solidity::minValue(IntegerType const& _type)
+{
+	return smt::Expression(_type.minValue());
+}
+
+smt::Expression dev::solidity::maxValue(IntegerType const& _type)
+{
+	return smt::Expression(_type.maxValue());
+}

libsolidity/formal/SymbolicTypes.h

@@ -0,0 +1,54 @@
+/*
+	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 isAddress(Type::Category _category);
+bool isAddress(Type const& _type);
+
+bool isNumber(Type::Category _category);
+bool isNumber(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);
+
+smt::Expression minValue(IntegerType const& _type);
+smt::Expression maxValue(IntegerType const& _type);
+
+}
+}

libsolidity/formal/SymbolicVariable.cpp

@@ -30,13 +30,14 @@ SymbolicVariable::SymbolicVariable(
 ):
 	m_type(_type),
 	m_uniqueName(_uniqueName),
-	m_interface(_interface)
+	m_interface(_interface),
+	m_ssa(make_shared<SSAVariable>())
 {
 }
 
-string SymbolicVariable::uniqueSymbol(int _seq) const
+string SymbolicVariable::uniqueSymbol(int _index) const
 {
-	return m_uniqueName + "_" + to_string(_seq);
+	return m_uniqueName + "_" + to_string(_index);
 }
 
 

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,36 @@ public:
 	);
 	virtual ~SymbolicVariable() = default;
 
-	smt::Expression operator()(int _seq) const
+	smt::Expression currentValue() const
 	{
-		return valueAtSequence(_seq);
+		return valueAtIndex(m_ssa->index());
 	}
 
-	std::string uniqueSymbol(int _seq) const;
+	virtual smt::Expression valueAtIndex(int _index) const = 0;
+
+	smt::Expression increaseIndex()
+	{
+		++(*m_ssa);
+		return currentValue();
+	}
+
+	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;
-	/// The unknown value is the full range of valid values,
-	/// and that's sub-type dependent.
-	virtual void setUnknownValue(int _seq) = 0;
+	/// Inherited types must implement.
+	virtual void setZeroValue() = 0;
+	/// The unknown value is the full range of valid values.
+	/// It is sub-type dependent, but not mandatory.
+	virtual void setUnknownValue() {}
 
 protected:
-	virtual smt::Expression valueAtSequence(int _seq) const = 0;
+	std::string uniqueSymbol(int _index) const;
 
 	Type const& m_type;
 	std::string m_uniqueName;
 	smt::SolverInterface& m_interface;
+	std::shared_ptr<SSAVariable> m_ssa = nullptr;
 };
 
 }