Refactor SymbolicAddressVariable and SymbolicVariable allocation

8 files changed, 159 insertions, 51 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 8787d25a..671c2049 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -257,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>",
@@ -570,7 +570,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
 		smt::Expression right(expr(_op.rightExpression()));
 		Token::Value op = _op.getOperator();
 		shared_ptr<smt::Expression> value;
-		if (isInteger(_op.annotation().commonType->category()))
+		if (isNumber(_op.annotation().commonType->category()))
 		{
 			value = make_shared<smt::Expression>(
 				op == Token::Equal ? (left == right) :
diff --git a/libsolidity/formal/SymbolicAddressVariable.cpp b/libsolidity/formal/SymbolicAddressVariable.cpp
new file mode 100644
index 00000000..68b95080
--- /dev/null
+++ b/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));
+}
diff --git a/libsolidity/formal/SymbolicAddressVariable.h b/libsolidity/formal/SymbolicAddressVariable.h
new file mode 100644
index 00000000..4a0f2361
--- /dev/null
+++ b/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();
+};
+
+}
+}
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
index d75275c6..cf1a7486 100644
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ b/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,11 +30,7 @@ SymbolicIntVariable::SymbolicIntVariable(
 ):
 	SymbolicVariable(_type, _uniqueName, _interface)
 {
-	solAssert(
-		_type.category() == Type::Category::Integer ||
-		_type.category() == Type::Category::Address,
-		""
-	);
+	solAssert(isNumber(_type.category()), "");
 }
 
 smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
@@ -47,28 +45,8 @@ void SymbolicIntVariable::setZeroValue()
 
 void SymbolicIntVariable::setUnknownValue()
 {
-	if (m_type.category() == Type::Category::Integer)
-	{
-		auto intType = dynamic_cast<IntegerType const*>(&m_type);
-		solAssert(intType, "");
-		m_interface.addAssertion(currentValue() >= minValue(*intType));
-		m_interface.addAssertion(currentValue() <= maxValue(*intType));
-	}
-	else
-	{
-		solAssert(m_type.category() == Type::Category::Address, "");
-		IntegerType addrType{160};
-		m_interface.addAssertion(currentValue() >= minValue(addrType));
-		m_interface.addAssertion(currentValue() <= 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));
 }
diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h
index d0ac3888..110ebb09 100644
--- a/libsolidity/formal/SymbolicIntVariable.h
+++ b/libsolidity/formal/SymbolicIntVariable.h
@@ -39,10 +39,7 @@ public:
 	/// Sets the var to 0.
 	void setZeroValue();
 	/// Sets the variable to the full valid value range.
-	void setUnknownValue();
-
-	static smt::Expression minValue(IntegerType const& _t);
-	static smt::Expression maxValue(IntegerType const& _t);
+	virtual void setUnknownValue();
 
 protected:
 	smt::Expression valueAtIndex(int _index) const;
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index deb52ac1..2d993865 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -19,6 +19,7 @@
 
 #include <libsolidity/formal/SymbolicBoolVariable.h>
 #include <libsolidity/formal/SymbolicIntVariable.h>
+#include <libsolidity/formal/SymbolicAddressVariable.h>
 
 #include <libsolidity/ast/Types.h>
 
@@ -29,7 +30,27 @@ using namespace dev::solidity;
 
 bool dev::solidity::isSupportedType(Type::Category _category)
 {
-	return isInteger(_category) || isBool(_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)
@@ -39,7 +60,7 @@ bool dev::solidity::isSupportedType(Type const& _type)
 
 bool dev::solidity::isInteger(Type::Category _category)
 {
-	return _category == Type::Category::Integer || _category == Type::Category::Address;
+	return _category == Type::Category::Integer;
 }
 
 bool dev::solidity::isInteger(Type const& _type)
@@ -47,6 +68,27 @@ 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;
@@ -57,16 +99,12 @@ bool dev::solidity::isBool(Type const& _type)
 	return isBool(_type.category());
 }
 
-shared_ptr<SymbolicVariable> dev::solidity::newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver)
+smt::Expression dev::solidity::minValue(IntegerType const& _type)
 {
-	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
-		solAssert(false, "");
+	return smt::Expression(_type.minValue());
 }
 
-
+smt::Expression dev::solidity::maxValue(IntegerType const& _type)
+{
+	return smt::Expression(_type.maxValue());
+}
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index f9df6853..77822fed 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -36,10 +36,19 @@ 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);
+
 }
 }
diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h
index 215c9ac1..417e1f92 100644
--- a/libsolidity/formal/SymbolicVariable.h
+++ b/libsolidity/formal/SymbolicVariable.h
@@ -62,10 +62,11 @@ public:
 	int& index() { return m_ssa->index(); }
 
 	/// Sets the var to the default value of its type.
+	/// Inherited types must implement.
 	virtual void setZeroValue() = 0;
-	/// The unknown value is the full range of valid values,
-	/// and that's sub-type dependent.
-	virtual void setUnknownValue() = 0;
+	/// The unknown value is the full range of valid values.
+	/// It is sub-type dependent, but not mandatory.
+	virtual void setUnknownValue() {}
 
 protected:
 	std::string uniqueSymbol(int _index) const;