Merge pull request #6512 from ethereum/smt_refactor_symbvars

[SMTChecker] Allow SymbolicVariable from smt::Sort

libsolidity/formal/SolverInterface.h

@@ -297,6 +297,7 @@ public:
 	Expression newVariable(std::string _name, SortPointer _sort)
 	{
 		// Subclasses should do something here
+		solAssert(_sort, "");
 		declareVariable(_name, *_sort);
 		return Expression(std::move(_name), {}, std::move(_sort));
 	}

libsolidity/formal/SymbolicTypes.cpp

@@ -236,6 +236,7 @@ void dev::solidity::smt::setSymbolicZeroValue(SymbolicVariable const& _variable,
 
 void dev::solidity::smt::setSymbolicZeroValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface)
 {
+	solAssert(_type, "");
 	if (isInteger(_type->category()))
 		_interface.addAssertion(_expr == 0);
 	else if (isBool(_type->category()))
@@ -249,6 +250,7 @@ void dev::solidity::smt::setSymbolicUnknownValue(SymbolicVariable const& _variab
 
 void dev::solidity::smt::setSymbolicUnknownValue(smt::Expression _expr, TypePointer const& _type, smt::SolverInterface& _interface)
 {
+	solAssert(_type, "");
 	if (isEnum(_type->category()))
 	{
 		auto enumType = dynamic_cast<EnumType const*>(_type.get());

libsolidity/formal/SymbolicVariables.cpp

@@ -26,14 +26,30 @@ using namespace dev::solidity;
 
 SymbolicVariable::SymbolicVariable(
 	TypePointer _type,
-	string const& _uniqueName,
+	string _uniqueName,
 	smt::SolverInterface& _interface
 ):
 	m_type(move(_type)),
-	m_uniqueName(_uniqueName),
+	m_uniqueName(move(_uniqueName)),
 	m_interface(_interface),
 	m_ssa(make_shared<SSAVariable>())
 {
+	solAssert(m_type, "");
+	m_sort = smtSort(*m_type);
+	solAssert(m_sort, "");
+}
+
+SymbolicVariable::SymbolicVariable(
+	smt::SortPointer _sort,
+	string _uniqueName,
+	smt::SolverInterface& _interface
+):
+	m_sort(move(_sort)),
+	m_uniqueName(move(_uniqueName)),
+	m_interface(_interface),
+	m_ssa(make_shared<SSAVariable>())
+{
+	solAssert(m_sort, "");
 }
 
 smt::Expression SymbolicVariable::currentValue() const
@@ -48,7 +64,7 @@ string SymbolicVariable::currentName() const
 
 smt::Expression SymbolicVariable::valueAtIndex(int _index) const
 {
-	return m_interface.newVariable(uniqueSymbol(_index), smtSort(*m_type));
+	return m_interface.newVariable(uniqueSymbol(_index), m_sort);
 }
 
 string SymbolicVariable::uniqueSymbol(unsigned _index) const
@@ -64,55 +80,55 @@ smt::Expression SymbolicVariable::increaseIndex()
 
 SymbolicBoolVariable::SymbolicBoolVariable(
 	TypePointer _type,
-	string const& _uniqueName,
+	string _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	SymbolicVariable(move(_type), _uniqueName, _interface)
+	SymbolicVariable(move(_type), move(_uniqueName), _interface)
 {
 	solAssert(m_type->category() == Type::Category::Bool, "");
 }
 
 SymbolicIntVariable::SymbolicIntVariable(
 	TypePointer _type,
-	string const& _uniqueName,
+	string _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	SymbolicVariable(move(_type), _uniqueName, _interface)
+	SymbolicVariable(move(_type), move(_uniqueName), _interface)
 {
 	solAssert(isNumber(m_type->category()), "");
 }
 
 SymbolicAddressVariable::SymbolicAddressVariable(
-	string const& _uniqueName,
+	string _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	SymbolicIntVariable(make_shared<IntegerType>(160), _uniqueName, _interface)
+	SymbolicIntVariable(make_shared<IntegerType>(160), move(_uniqueName), _interface)
 {
 }
 
 SymbolicFixedBytesVariable::SymbolicFixedBytesVariable(
 	unsigned _numBytes,
-	string const& _uniqueName,
+	string _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	SymbolicIntVariable(make_shared<IntegerType>(_numBytes * 8), _uniqueName, _interface)
+	SymbolicIntVariable(make_shared<IntegerType>(_numBytes * 8), move(_uniqueName), _interface)
 {
 }
 
 SymbolicFunctionVariable::SymbolicFunctionVariable(
 	TypePointer _type,
-	string const& _uniqueName,
+	string _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	SymbolicVariable(move(_type), _uniqueName, _interface),
+	SymbolicVariable(move(_type), move(_uniqueName), _interface),
-	m_declaration(m_interface.newVariable(currentName(), smtSort(*m_type)))
+	m_declaration(m_interface.newVariable(currentName(), m_sort))
 {
 	solAssert(m_type->category() == Type::Category::Function, "");
 }
 
 void SymbolicFunctionVariable::resetDeclaration()
 {
-	m_declaration = m_interface.newVariable(currentName(), smtSort(*m_type));
+	m_declaration = m_interface.newVariable(currentName(), m_sort);
 }
 
 smt::Expression SymbolicFunctionVariable::increaseIndex()
@@ -129,30 +145,30 @@ smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _ar
 
 SymbolicMappingVariable::SymbolicMappingVariable(
 	TypePointer _type,
-	string const& _uniqueName,
+	string _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	SymbolicVariable(move(_type), _uniqueName, _interface)
+	SymbolicVariable(move(_type), move(_uniqueName), _interface)
 {
 	solAssert(isMapping(m_type->category()), "");
 }
 
 SymbolicArrayVariable::SymbolicArrayVariable(
 	TypePointer _type,
-	string const& _uniqueName,
+	string _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	SymbolicVariable(move(_type), _uniqueName, _interface)
+	SymbolicVariable(move(_type), move(_uniqueName), _interface)
 {
 	solAssert(isArray(m_type->category()), "");
 }
 
 SymbolicEnumVariable::SymbolicEnumVariable(
 	TypePointer _type,
-	string const& _uniqueName,
+	string _uniqueName,
 	smt::SolverInterface& _interface
 ):
-	SymbolicVariable(move(_type), _uniqueName, _interface)
+	SymbolicVariable(move(_type), move(_uniqueName), _interface)
 {
 	solAssert(isEnum(m_type->category()), "");
 }

libsolidity/formal/SymbolicVariables.h

@@ -37,7 +37,12 @@ class SymbolicVariable
 public:
 	SymbolicVariable(
 		TypePointer _type,
-		std::string const& _uniqueName,
+		std::string _uniqueName,
+		smt::SolverInterface& _interface
+	);
+	SymbolicVariable(
+		smt::SortPointer _sort,
+		std::string _uniqueName,
 		smt::SolverInterface& _interface
 	);
 
@@ -60,6 +65,9 @@ public:
 protected:
 	std::string uniqueSymbol(unsigned _index) const;
 
+	/// SMT sort.
+	smt::SortPointer m_sort;
+	/// Solidity type, used for size and range in number types.
 	TypePointer m_type;
 	std::string m_uniqueName;
 	smt::SolverInterface& m_interface;
@@ -74,7 +82,7 @@ class SymbolicBoolVariable: public SymbolicVariable
 public:
 	SymbolicBoolVariable(
 		TypePointer _type,
-		std::string const& _uniqueName,
+		std::string _uniqueName,
 		smt::SolverInterface& _interface
 	);
 };
@@ -87,7 +95,7 @@ class SymbolicIntVariable: public SymbolicVariable
 public:
 	SymbolicIntVariable(
 		TypePointer _type,
-		std::string const& _uniqueName,
+		std::string _uniqueName,
 		smt::SolverInterface& _interface
 	);
 };
@@ -99,7 +107,7 @@ class SymbolicAddressVariable: public SymbolicIntVariable
 {
 public:
 	SymbolicAddressVariable(
-		std::string const& _uniqueName,
+		std::string _uniqueName,
 		smt::SolverInterface& _interface
 	);
 };
@@ -112,7 +120,7 @@ class SymbolicFixedBytesVariable: public SymbolicIntVariable
 public:
 	SymbolicFixedBytesVariable(
 		unsigned _numBytes,
-		std::string const& _uniqueName,
+		std::string _uniqueName,
 		smt::SolverInterface& _interface
 	);
 };
@@ -125,7 +133,7 @@ class SymbolicFunctionVariable: public SymbolicVariable
 public:
 	SymbolicFunctionVariable(
 		TypePointer _type,
-		std::string const& _uniqueName,
+		std::string _uniqueName,
 		smt::SolverInterface& _interface
 	);
 
@@ -148,7 +156,7 @@ class SymbolicMappingVariable: public SymbolicVariable
 public:
 	SymbolicMappingVariable(
 		TypePointer _type,
-		std::string const& _uniqueName,
+		std::string _uniqueName,
 		smt::SolverInterface& _interface
 	);
 };
@@ -161,7 +169,7 @@ class SymbolicArrayVariable: public SymbolicVariable
 public:
 	SymbolicArrayVariable(
 		TypePointer _type,
-		std::string const& _uniqueName,
+		std::string _uniqueName,
 		smt::SolverInterface& _interface
 	);
 };
@@ -174,7 +182,7 @@ class SymbolicEnumVariable: public SymbolicVariable
 public:
 	SymbolicEnumVariable(
 		TypePointer _type,
-		std::string const& _uniqueName,
+		std::string _uniqueName,
 		smt::SolverInterface& _interface
 	);
 };