Merge pull request #5209 from ethereum/smt_ssa_refactor

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

1 files changed, 19 insertions, 11 deletions

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)