[SMTChecker] Refactor smt::Sort and its usage

libsolidity/formal/CVC4Interface.cpp

@@ -50,7 +50,7 @@ void CVC4Interface::pop()
 	m_solver.pop();
 }
 
-void CVC4Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
+void CVC4Interface::declareFunction(string _name, vector<SortPointer> const& _domain, Sort const& _codomain)
 {
 	if (!m_functions.count(_name))
 	{
@@ -186,13 +186,13 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 	return arguments[0];
 }
 
-CVC4::Type CVC4Interface::cvc4Sort(Sort _sort)
+CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
 {
-	switch (_sort)
+	switch (_sort.kind)
 	{
-	case Sort::Bool:
+	case Kind::Bool:
 		return m_context.booleanType();
-	case Sort::Int:
+	case Kind::Int:
 		return m_context.integerType();
 	default:
 		break;
@@ -202,10 +202,10 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort _sort)
 	return m_context.integerType();
 }
 
-vector<CVC4::Type> CVC4Interface::cvc4Sort(vector<Sort> const& _sorts)
+vector<CVC4::Type> CVC4Interface::cvc4Sort(vector<SortPointer> const& _sorts)
 {
 	vector<CVC4::Type> cvc4Sorts;
 	for (auto const& _sort: _sorts)
-		cvc4Sorts.push_back(cvc4Sort(_sort));
+		cvc4Sorts.push_back(cvc4Sort(*_sort));
 	return cvc4Sorts;
 }

libsolidity/formal/CVC4Interface.h

@@ -51,7 +51,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
+	void declareFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain) override;
 	void declareInteger(std::string _name) override;
 	void declareBool(std::string _name) override;
 
@@ -60,8 +60,8 @@ public:
 
 private:
 	CVC4::Expr toCVC4Expr(Expression const& _expr);
-	CVC4::Type cvc4Sort(smt::Sort _sort);
+	CVC4::Type cvc4Sort(smt::Sort const& _sort);
-	std::vector<CVC4::Type> cvc4Sort(std::vector<smt::Sort> const& _sort);
+	std::vector<CVC4::Type> cvc4Sort(std::vector<smt::SortPointer> const& _sorts);
 
 	CVC4::ExprManager m_context;
 	CVC4::SmtEngine m_solver;

libsolidity/formal/SMTChecker.cpp

@@ -416,7 +416,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
 {
 	string blockHash = "blockhash";
-	defineUninterpretedFunction(blockHash, {smt::Sort::Int}, smt::Sort::Int);
+	defineUninterpretedFunction(blockHash, {make_shared<smt::Sort>(smt::Kind::Int)}, smt::Kind::Int);
 	auto const& arguments = _funCall.arguments();
 	solAssert(arguments.size() == 1, "");
 	defineExpr(_funCall, m_uninterpretedFunctions.at(blockHash)({expr(*arguments[0])}));
@@ -605,7 +605,7 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e
 	defineExpr(_expr, m_specialVariables.at(_name)->currentValue());
 }
 
-void SMTChecker::defineUninterpretedFunction(string const& _name, vector<smt::Sort> const& _domain, smt::Sort _codomain)
+void SMTChecker::defineUninterpretedFunction(string const& _name, vector<smt::SortPointer> const& _domain, smt::Sort const& _codomain)
 {
 	if (!m_uninterpretedFunctions.count(_name))
 		m_uninterpretedFunctions.emplace(_name, m_interface->newFunction(_name, _domain, _codomain));

libsolidity/formal/SMTChecker.h

@@ -83,7 +83,7 @@ private:
 	void inlineFunctionCall(FunctionCall const&);
 
 	void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false);
-	void defineUninterpretedFunction(std::string const& _name, std::vector<smt::Sort> const& _domain, smt::Sort _codomain);
+	void defineUninterpretedFunction(std::string const& _name, std::vector<smt::SortPointer> const& _domain, smt::Sort const& _codomain);
 
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.

libsolidity/formal/SMTLib2Interface.cpp

@@ -64,12 +64,12 @@ void SMTLib2Interface::pop()
 	m_accumulatedOutput.pop_back();
 }
 
-void SMTLib2Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
+void SMTLib2Interface::declareFunction(string _name, vector<SortPointer> const& _domain, Sort const& _codomain)
 {
 	// TODO Use domain and codomain as key as well
 	string domain("");
 	for (auto const& sort: _domain)
-		domain += toSmtLibSort(sort) + ' ';
+		domain += toSmtLibSort(*sort) + ' ';
 	if (!m_functions.count(_name))
 	{
 		m_functions.insert(_name);
@@ -79,7 +79,7 @@ void SMTLib2Interface::declareFunction(string _name, vector<Sort> const& _domain
 			"| (" +
 			domain +
 			") " +
-			(_codomain == Sort::Int ? "Int" : "Bool") +
+			(_codomain.kind == Kind::Int ? "Int" : "Bool") +
 			")"
 		);
 	}
@@ -143,13 +143,13 @@ string SMTLib2Interface::toSExpr(Expression const& _expr)
 	return sexpr;
 }
 
-string SMTLib2Interface::toSmtLibSort(Sort _sort)
+string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 {
-	switch (_sort)
+	switch (_sort.kind)
 	{
-	case Sort::Int:
+	case Kind::Int:
 		return "Int";
-	case Sort::Bool:
+	case Kind::Bool:
 		return "Bool";
 	default:
 		solAssert(false, "Invalid SMT sort");
@@ -173,8 +173,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
 		for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
 		{
 			auto const& e = _expressionsToEvaluate.at(i);
-			solAssert(e.sort == Sort::Int || e.sort == Sort::Bool, "Invalid sort for expression to evaluate.");
+			solAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate.");
-			command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + ")\n";
+			command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n";
 			command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
 		}
 		command += "(check-sat)\n";

libsolidity/formal/SMTLib2Interface.h

@@ -49,7 +49,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
+	void declareFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain) override;
 	void declareInteger(std::string _name) override;
 	void declareBool(std::string _name) override;
 
@@ -58,7 +58,7 @@ public:
 
 private:
 	std::string toSExpr(Expression const& _expr);
-	std::string toSmtLibSort(Sort _sort);
+	std::string toSmtLibSort(Sort const& _sort);
 
 	void write(std::string _data);
 

libsolidity/formal/SMTPortfolio.cpp

@@ -64,7 +64,7 @@ void SMTPortfolio::pop()
 		s->pop();
 }
 
-void SMTPortfolio::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
+void SMTPortfolio::declareFunction(string _name, vector<SortPointer> const& _domain, Sort const& _codomain)
 {
 	for (auto s : m_solvers)
 		s->declareFunction(_name, _domain, _codomain);

libsolidity/formal/SMTPortfolio.h

@@ -49,7 +49,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
+	void declareFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain) override;
 	void declareInteger(std::string _name) override;
 	void declareBool(std::string _name) override;
 

libsolidity/formal/SolverInterface.h

@@ -42,21 +42,32 @@ enum class CheckResult
 	SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR
 };
 
-enum class Sort
+enum class Kind
 {
 	Int,
 	Bool
 };
 
+struct Sort
+{
+	Sort(Kind _kind):
+		kind(_kind) {}
+	virtual ~Sort() = default;
+	Kind const kind;
+	bool operator==(Sort const& _other) const { return kind == _other.kind; }
+};
+using SortPointer = std::shared_ptr<Sort>;
+
+
 /// C++ representation of an SMTLIB2 expression.
 class Expression
 {
 	friend class SolverInterface;
 public:
-	explicit Expression(bool _v): name(_v ? "true" : "false"), sort(Sort::Bool) {}
+	explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
-	Expression(size_t _number): name(std::to_string(_number)), sort(Sort::Int) {}
+	Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
-	Expression(u256 const& _number): name(_number.str()), sort(Sort::Int) {}
+	Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
-	Expression(bigint const& _number): name(_number.str()), sort(Sort::Int) {}
+	Expression(bigint const& _number): Expression(_number.str(), Kind::Int) {}
 
 	Expression(Expression const&) = default;
 	Expression(Expression&&) = default;
@@ -85,7 +96,7 @@ public:
 
 	static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
 	{
-		solAssert(_trueValue.sort == _falseValue.sort, "");
+		solAssert(*_trueValue.sort == *_falseValue.sort, "");
 		return Expression("ite", std::vector<Expression>{
 			std::move(_condition), std::move(_trueValue), std::move(_falseValue)
 		}, _trueValue.sort);
@@ -98,19 +109,19 @@ public:
 
 	friend Expression operator!(Expression _a)
 	{
-		return Expression("not", std::move(_a), Sort::Bool);
+		return Expression("not", std::move(_a), Kind::Bool);
 	}
 	friend Expression operator&&(Expression _a, Expression _b)
 	{
-		return Expression("and", std::move(_a), std::move(_b), Sort::Bool);
+		return Expression("and", std::move(_a), std::move(_b), Kind::Bool);
 	}
 	friend Expression operator||(Expression _a, Expression _b)
 	{
-		return Expression("or", std::move(_a), std::move(_b), Sort::Bool);
+		return Expression("or", std::move(_a), std::move(_b), Kind::Bool);
 	}
 	friend Expression operator==(Expression _a, Expression _b)
 	{
-		return Expression("=", std::move(_a), std::move(_b), Sort::Bool);
+		return Expression("=", std::move(_a), std::move(_b), Kind::Bool);
 	}
 	friend Expression operator!=(Expression _a, Expression _b)
 	{
@@ -118,35 +129,35 @@ public:
 	}
 	friend Expression operator<(Expression _a, Expression _b)
 	{
-		return Expression("<", std::move(_a), std::move(_b), Sort::Bool);
+		return Expression("<", std::move(_a), std::move(_b), Kind::Bool);
 	}
 	friend Expression operator<=(Expression _a, Expression _b)
 	{
-		return Expression("<=", std::move(_a), std::move(_b), Sort::Bool);
+		return Expression("<=", std::move(_a), std::move(_b), Kind::Bool);
 	}
 	friend Expression operator>(Expression _a, Expression _b)
 	{
-		return Expression(">", std::move(_a), std::move(_b), Sort::Bool);
+		return Expression(">", std::move(_a), std::move(_b), Kind::Bool);
 	}
 	friend Expression operator>=(Expression _a, Expression _b)
 	{
-		return Expression(">=", std::move(_a), std::move(_b), Sort::Bool);
+		return Expression(">=", std::move(_a), std::move(_b), Kind::Bool);
 	}
 	friend Expression operator+(Expression _a, Expression _b)
 	{
-		return Expression("+", std::move(_a), std::move(_b), Sort::Int);
+		return Expression("+", std::move(_a), std::move(_b), Kind::Int);
 	}
 	friend Expression operator-(Expression _a, Expression _b)
 	{
-		return Expression("-", std::move(_a), std::move(_b), Sort::Int);
+		return Expression("-", std::move(_a), std::move(_b), Kind::Int);
 	}
 	friend Expression operator*(Expression _a, Expression _b)
 	{
-		return Expression("*", std::move(_a), std::move(_b), Sort::Int);
+		return Expression("*", std::move(_a), std::move(_b), Kind::Int);
 	}
 	friend Expression operator/(Expression _a, Expression _b)
 	{
-		return Expression("/", std::move(_a), std::move(_b), Sort::Int);
+		return Expression("/", std::move(_a), std::move(_b), Kind::Int);
 	}
 	Expression operator()(std::vector<Expression> _arguments) const
 	{
@@ -154,36 +165,26 @@ public:
 			arguments.empty(),
 			"Attempted function application to non-function."
 		);
-		switch (sort)
+		return Expression(name, std::move(_arguments), sort);
-		{
-		case Sort::Int:
-			return Expression(name, std::move(_arguments), Sort::Int);
-		case Sort::Bool:
-			return Expression(name, std::move(_arguments), Sort::Bool);
-		default:
-			solAssert(
-				false,
-				"Attempted function application to invalid type."
-			);
-			break;
-		}
 	}
 
 	std::string name;
 	std::vector<Expression> arguments;
-	Sort sort;
+	SortPointer sort;
 
 private:
-	/// Manual constructor, should only be used by SolverInterface and this class itself.
+	/// Manual constructors, should only be used by SolverInterface and this class itself.
-	Expression(std::string _name, std::vector<Expression> _arguments, Sort _sort):
+	Expression(std::string _name, std::vector<Expression> _arguments, SortPointer _sort):
-		name(std::move(_name)), arguments(std::move(_arguments)), sort(_sort) {}
+		name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {}
+	Expression(std::string _name, std::vector<Expression> _arguments, Kind _kind):
+		Expression(std::move(_name), std::move(_arguments), std::make_shared<Sort>(_kind)) {}
 
-	explicit Expression(std::string _name, Sort _sort):
+	explicit Expression(std::string _name, Kind _kind):
-		Expression(std::move(_name), std::vector<Expression>{}, _sort) {}
+		Expression(std::move(_name), std::vector<Expression>{}, _kind) {}
-	Expression(std::string _name, Expression _arg, Sort _sort):
+	Expression(std::string _name, Expression _arg, Kind _kind):
-		Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}, _sort) {}
+		Expression(std::move(_name), std::vector<Expression>{std::move(_arg)}, _kind) {}
-	Expression(std::string _name, Expression _arg1, Expression _arg2, Sort _sort):
+	Expression(std::string _name, Expression _arg1, Expression _arg2, Kind _kind):
-		Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}, _sort) {}
+		Expression(std::move(_name), std::vector<Expression>{std::move(_arg1), std::move(_arg2)}, _kind) {}
 };
 
 DEV_SIMPLE_EXCEPTION(SolverError);
@@ -197,39 +198,26 @@ public:
 	virtual void push() = 0;
 	virtual void pop() = 0;
 
-	virtual void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) = 0;
+	virtual void declareFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain) = 0;
-	void declareFunction(std::string _name, Sort _domain, Sort _codomain)
+	Expression newFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain)
-	{
-		declareFunction(std::move(_name), std::vector<Sort>{std::move(_domain)}, std::move(_codomain));
-	}
-	Expression newFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain)
 	{
 		declareFunction(_name, _domain, _codomain);
 		// Subclasses should do something here
-		switch (_codomain)
+		return Expression(std::move(_name), {}, _codomain.kind);
-		{
-		case Sort::Int:
-			return Expression(std::move(_name), {}, Sort::Int);
-		case Sort::Bool:
-			return Expression(std::move(_name), {}, Sort::Bool);
-		default:
-			solAssert(false, "Function sort not supported.");
-			break;
-		}
 	}
 	virtual void declareInteger(std::string _name) = 0;
 	Expression newInteger(std::string _name)
 	{
 		// Subclasses should do something here
 		declareInteger(_name);
-		return Expression(std::move(_name), {}, Sort::Int);
+		return Expression(std::move(_name), {}, Kind::Int);
 	}
 	virtual void declareBool(std::string _name) = 0;
 	Expression newBool(std::string _name)
 	{
 		// Subclasses should do something here
 		declareBool(_name);
-		return Expression(std::move(_name), {}, Sort::Bool);
+		return Expression(std::move(_name), {}, Kind::Bool);
 	}
 
 	virtual void addAssertion(Expression const& _expr) = 0;

libsolidity/formal/SymbolicTypes.cpp

@@ -24,12 +24,24 @@
 using namespace std;
 using namespace dev::solidity;
 
-smt::Sort dev::solidity::smtSort(Type::Category _category)
+smt::SortPointer dev::solidity::smtSort(Type const& _type)
+{
+	switch (smtKind(_type.category()))
+	{
+	case smt::Kind::Int:
+		return make_shared<smt::Sort>(smt::Kind::Int);
+	case smt::Kind::Bool:
+		return make_shared<smt::Sort>(smt::Kind::Bool);
+	}
+	solAssert(false, "Invalid type");
+}
+
+smt::Kind dev::solidity::smtKind(Type::Category _category)
 {
 	if (isNumber(_category))
-		return smt::Sort::Int;
+		return smt::Kind::Int;
 	else if (isBool(_category))
-		return smt::Sort::Bool;
+		return smt::Kind::Bool;
 	solAssert(false, "Invalid type");
 }
 

libsolidity/formal/SymbolicTypes.h

@@ -29,7 +29,9 @@ namespace solidity
 {
 
 /// Returns the SMT sort that models the Solidity type _type.
-smt::Sort smtSort(Type::Category _type);
+smt::SortPointer smtSort(Type const& _type);
+/// Returns the SMT kind that models the Solidity type type category _category.
+smt::Kind smtKind(Type::Category _category);
 
 /// So far int, bool and address are supported.
 /// Returns true if type is supported.

libsolidity/formal/Z3Interface.cpp

@@ -51,7 +51,7 @@ void Z3Interface::pop()
 	m_solver.pop();
 }
 
-void Z3Interface::declareFunction(string _name, vector<Sort> const& _domain, Sort _codomain)
+void Z3Interface::declareFunction(string _name, vector<SortPointer> const& _domain, Sort const& _codomain)
 {
 	if (!m_functions.count(_name))
 		m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))});
@@ -168,13 +168,13 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 	return arguments[0];
 }
 
-z3::sort Z3Interface::z3Sort(Sort _sort)
+z3::sort Z3Interface::z3Sort(Sort const& _sort)
 {
-	switch (_sort)
+	switch (_sort.kind)
 	{
-	case Sort::Bool:
+	case Kind::Bool:
 		return m_context.bool_sort();
-	case Sort::Int:
+	case Kind::Int:
 		return m_context.int_sort();
 	default:
 		break;
@@ -184,10 +184,10 @@ z3::sort Z3Interface::z3Sort(Sort _sort)
 	return m_context.int_sort();
 }
 
-z3::sort_vector Z3Interface::z3Sort(vector<Sort> const& _sorts)
+z3::sort_vector Z3Interface::z3Sort(vector<SortPointer> const& _sorts)
 {
 	z3::sort_vector z3Sorts(m_context);
 	for (auto const& _sort: _sorts)
-		z3Sorts.push_back(z3Sort(_sort));
+		z3Sorts.push_back(z3Sort(*_sort));
 	return z3Sorts;
 }

libsolidity/formal/Z3Interface.h

@@ -40,7 +40,7 @@ public:
 	void push() override;
 	void pop() override;
 
-	void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
+	void declareFunction(std::string _name, std::vector<SortPointer> const& _domain, Sort const& _codomain) override;
 	void declareInteger(std::string _name) override;
 	void declareBool(std::string _name) override;
 
@@ -49,8 +49,8 @@ public:
 
 private:
 	z3::expr toZ3Expr(Expression const& _expr);
-	z3::sort z3Sort(smt::Sort _sort);
+	z3::sort z3Sort(smt::Sort const& _sort);
-	z3::sort_vector z3Sort(std::vector<smt::Sort> const& _sort);
+	z3::sort_vector z3Sort(std::vector<smt::SortPointer> const& _sorts);
 
 	z3::context m_context;
 	z3::solver m_solver;