Merge pull request #5209 from ethereum/smt_ssa_refactor

[SMTChecker] Refactor SSAVariable such that it only uses Type and not Declaration

9 files changed, 48 insertions, 37 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 1e27dc33..0cb75530 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -924,7 +924,7 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl)
 	else 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
diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp
index 4fc2dd45..ceeea49a 100644
--- a/libsolidity/formal/SSAVariable.cpp
+++ b/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()))
-		m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface);
-	else if (isBool(_decl.type()->category()))
-		m_symbolicVar = make_shared<SymbolicBoolVariable>(_decl, _interface);
+	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, "");
diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h
index bf5dae3b..f4a4e93e 100644
--- a/libsolidity/formal/SSAVariable.h
+++ b/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
 	);
 
diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp
index 5cf22d7d..5e5aec8f 100644
--- a/libsolidity/formal/SymbolicBoolVariable.cpp
+++ b/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
diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h
index 678f97d9..33ac9061 100644
--- a/libsolidity/formal/SymbolicBoolVariable.h
+++ b/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
 	);
 
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
index 4f65b1fd..0adb9d09 100644
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ b/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 ||
-		m_declaration.type()->category() == Type::Category::Address,
+		_type.category() == Type::Category::Integer ||
+		_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 (!intType)
-		intType = make_shared<IntegerType>(160);
-	m_interface.addAssertion(valueAtSequence(_seq) >= minValue(*intType));
-	m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(*intType));
+	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)
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
index d591e8db..92eeb13d 100644
--- a/libsolidity/formal/SymbolicIntVariable.h
+++ b/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
 	);
 
diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp
index caefa3a3..afbc01ba 100644
--- a/libsolidity/formal/SymbolicVariable.cpp
+++ b/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);
 }
 
 
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
index e29ded26..977515f8 100644
--- a/libsolidity/formal/SymbolicVariable.h
+++ b/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;
 };