Refactor SSAVariable such that it only uses Type and not Declaration

libsolidity/formal/SMTChecker.cpp

@@ -782,7 +782,7 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 	if (SSAVariable::isSupportedType(_varDecl.type()->category()))
 	{
 		solAssert(m_variables.count(&_varDecl) == 0, "");
-		m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface));
+		m_variables.emplace(&_varDecl, SSAVariable(*_varDecl.type(), _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface));
 		return true;
 	}
 	else

libsolidity/formal/SSAVariable.cpp

@@ -27,16 +27,17 @@ using namespace dev;
 using namespace dev::solidity;
 
 SSAVariable::SSAVariable(
-	Declaration const& _decl,
+	Type const& _type,
+	string const& _uniqueName,
 	smt::SolverInterface& _interface
 )
 {
 	resetIndex();
 
-	if (isInteger(_decl.type()->category()))
+	if (isInteger(_type.category()))
-		m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
+		m_symbolicVar = make_shared<SymbolicIntVariable>(_type, _uniqueName, _interface);
-	else if (isBool(_decl.type()->category()))
+	else if (isBool(_type.category()))
-		m_symbolicVar = make_shared<SymbolicBoolVariable>(_decl, _interface);
+		m_symbolicVar = make_shared<SymbolicBoolVariable>(_type, _uniqueName, _interface);
 	else
 	{
 		solAssert(false, "");

libsolidity/formal/SSAVariable.h

@@ -26,18 +26,17 @@ namespace dev
 namespace solidity
 {
 
-class Declaration;
-
 /**
  * This class represents the SSA representation of a program variable.
  */
 class SSAVariable
 {
 public:
-	/// @param _decl Used to determine the type and forwarded to the symbolic var.
+	/// @param _type Forwarded to the symbolic var.
 	/// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver.
 	SSAVariable(
-		Declaration const& _decl,
+		Type const& _type,
+		std::string const& _uniqueName,
 		smt::SolverInterface& _interface
 	);
 

libsolidity/formal/SymbolicBoolVariable.cpp

@@ -24,12 +24,13 @@ using namespace dev;
 using namespace dev::solidity;
 
 SymbolicBoolVariable::SymbolicBoolVariable(
-	Declaration const& _decl,
+	Type const& _type,
+	string const& _uniqueName,
 	smt::SolverInterface&_interface
 ):
-	SymbolicVariable(_decl, _interface)
+	SymbolicVariable(_type, _uniqueName, _interface)
 {
-	solAssert(m_declaration.type()->category() == Type::Category::Bool, "");
+	solAssert(_type.category() == Type::Category::Bool, "");
 }
 
 smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const

libsolidity/formal/SymbolicBoolVariable.h

@@ -19,8 +19,6 @@
 
 #include <libsolidity/formal/SymbolicVariable.h>
 
-#include <libsolidity/ast/Types.h>
-
 namespace dev
 {
 namespace solidity
@@ -33,7 +31,8 @@ class SymbolicBoolVariable: public SymbolicVariable
 {
 public:
 	SymbolicBoolVariable(
-		Declaration const& _decl,
+		Type const& _type,
+		std::string const& _uniqueName,
 		smt::SolverInterface& _interface
 	);
 

libsolidity/formal/SymbolicIntVariable.cpp

@@ -17,21 +17,20 @@
 
 #include <libsolidity/formal/SymbolicIntVariable.h>
 
-#include <libsolidity/ast/AST.h>
-
 using namespace std;
 using namespace dev;
 using namespace dev::solidity;
 
 SymbolicIntVariable::SymbolicIntVariable(
-	Declaration const& _decl,
+	Type const& _type,
+	string const& _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	SymbolicVariable(_decl, _interface)
+	SymbolicVariable(_type, _uniqueName, _interface)
 {
 	solAssert(
-		m_declaration.type()->category() == Type::Category::Integer ||
+		_type.category() == Type::Category::Integer ||
-		m_declaration.type()->category() == Type::Category::Address,
+		_type.category() == Type::Category::Address,
 		""
 	);
 }
@@ -48,11 +47,20 @@ void SymbolicIntVariable::setZeroValue(int _seq)
 
 void SymbolicIntVariable::setUnknownValue(int _seq)
 {
-	auto intType = dynamic_pointer_cast<IntegerType const>(m_declaration.type());
+	if (m_type.category() == Type::Category::Integer)
-	if (!intType)
+	{
-		intType = make_shared<IntegerType>(160);
+		auto intType = dynamic_cast<IntegerType const*>(&m_type);
-	m_interface.addAssertion(valueAtSequence(_seq) >= minValue(*intType));
+		solAssert(intType, "");
-	m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(*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)

libsolidity/formal/SymbolicIntVariable.h

@@ -19,8 +19,6 @@
 
 #include <libsolidity/formal/SymbolicVariable.h>
 
-#include <libsolidity/ast/Types.h>
-
 namespace dev
 {
 namespace solidity
@@ -33,7 +31,8 @@ class SymbolicIntVariable: public SymbolicVariable
 {
 public:
 	SymbolicIntVariable(
-		Declaration const& _decl,
+		Type const& _type,
+		std::string const& _uniqueName,
 		smt::SolverInterface& _interface
 	);
 

libsolidity/formal/SymbolicVariable.cpp

@@ -24,17 +24,19 @@ using namespace dev;
 using namespace dev::solidity;
 
 SymbolicVariable::SymbolicVariable(
-	Declaration const& _decl,
+	Type const& _type,
+	string const& _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	m_declaration(_decl),
+	m_type(_type),
+	m_uniqueName(_uniqueName),
 	m_interface(_interface)
 {
 }
 
 string SymbolicVariable::uniqueSymbol(int _seq) const
 {
-	return m_declaration.name() + "_" + to_string(m_declaration.id()) + "_" + to_string(_seq);
+	return m_uniqueName + "_" + to_string(_seq);
 }
 
 

libsolidity/formal/SymbolicVariable.h

@@ -19,7 +19,7 @@
 
 #include <libsolidity/formal/SolverInterface.h>
 
-#include <libsolidity/ast/AST.h>
+#include <libsolidity/ast/Types.h>
 
 #include <memory>
 
@@ -28,7 +28,7 @@ namespace dev
 namespace solidity
 {
 
-class Declaration;
+class Type;
 
 /**
  * This class represents the symbolic version of a program variable.
@@ -37,7 +37,8 @@ class SymbolicVariable
 {
 public:
 	SymbolicVariable(
-		Declaration const& _decl,
+		Type const& _type,
+		std::string const& _uniqueName,
 		smt::SolverInterface& _interface
 	);
 	virtual ~SymbolicVariable() = default;
@@ -58,7 +59,8 @@ public:
 protected:
 	virtual smt::Expression valueAtSequence(int _seq) const = 0;
 
-	Declaration const& m_declaration;
+	Type const& m_type;
+	std::string m_uniqueName;
 	smt::SolverInterface& m_interface;
 };