Merge pull request #8639 from ethereum/smt_tuple_sort

[SMTChecker] Add and use tuple sort

libsolidity/formal/CVC4Interface.cpp

@@ -196,6 +196,16 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 			solAssert(sortSort, "");
 			return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1]));
 		}
+		else if (n == "tuple_get")
+		{
+			shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.arguments[0].sort);
+			solAssert(tupleSort, "");
+			CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
+			CVC4::Datatype const& dt = tt.getDatatype();
+			size_t index = std::stoi(_expr.arguments[1].name);
+			CVC4::Expr s = dt[0][index].getSelector();
+			return m_context.mkExpr(CVC4::kind::APPLY_SELECTOR, s, arguments[0]);
+		}
 
 		solAssert(false, "");
 	}
@@ -229,6 +239,11 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
 		auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
 		return m_context.mkArrayType(cvc4Sort(*arraySort.domain), cvc4Sort(*arraySort.range));
 	}
+	case Kind::Tuple:
+	{
+		auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
+		return m_context.mkTupleType(cvc4Sort(tupleSort.components));
+	}
 	default:
 		break;
 	}

libsolidity/formal/SMTEncoder.cpp

@@ -296,16 +296,22 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
 		{
 			auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*init));
 			solAssert(symbTuple, "");
-			auto const& components = symbTuple->components();
+			auto const& symbComponents = symbTuple->components();
+
+			auto tupleType = dynamic_cast<TupleType const*>(init->annotation().type);
+			solAssert(tupleType, "");
+			solAssert(tupleType->components().size() == symbTuple->components().size(), "");
+			auto const& components = tupleType->components();
+
 			auto const& declarations = _varDecl.declarations();
-			solAssert(components.size() == declarations.size(), "");
+			solAssert(symbComponents.size() == declarations.size(), "");
 			for (unsigned i = 0; i < declarations.size(); ++i)
 				if (
 					components.at(i) &&
 					declarations.at(i) &&
 					m_context.knownVariable(*declarations.at(i))
 				)
-					assignment(*declarations.at(i), components.at(i)->currentValue(declarations.at(i)->type()));
+					assignment(*declarations.at(i), symbTuple->component(i, components.at(i), declarations.at(i)->type()));
 		}
 	}
 	else if (m_context.knownVariable(*_varDecl.declarations().front()))
@@ -354,7 +360,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 	{
 		auto const& type = _assignment.annotation().type;
 		vector<smt::Expression> rightArguments;
-		if (_assignment.rightHandSide().annotation().type->category() == Type::Category::Tuple)
+		if (auto const* tupleTypeRight = dynamic_cast<TupleType const*>(_assignment.rightHandSide().annotation().type))
 		{
 			auto symbTupleLeft = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_assignment.leftHandSide()));
 			solAssert(symbTupleLeft, "");
@@ -365,17 +371,16 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 			auto const& rightComponents = symbTupleRight->components();
 			solAssert(leftComponents.size() == rightComponents.size(), "");
 
-			for (unsigned i = 0; i < leftComponents.size(); ++i)
-			{
-				auto const& left = leftComponents.at(i);
-				auto const& right = rightComponents.at(i);
-				/// Right hand side tuple component cannot be empty.
-				solAssert(right, "");
-				if (left)
-					rightArguments.push_back(right->currentValue(left->originalType()));
-				else
-					rightArguments.push_back(right->currentValue());
-			}
+			auto tupleTypeLeft = dynamic_cast<TupleType const*>(_assignment.leftHandSide().annotation().type);
+			solAssert(tupleTypeLeft, "");
+			solAssert(tupleTypeLeft->components().size() == leftComponents.size(), "");
+			auto const& typesLeft = tupleTypeLeft->components();
+
+			solAssert(tupleTypeRight->components().size() == rightComponents.size(), "");
+			auto const& typesRight = tupleTypeRight->components();
+
+			for (unsigned i = 0; i < rightComponents.size(); ++i)
+				rightArguments.push_back(symbTupleRight->component(i, typesRight.at(i), typesLeft.at(i)));
 		}
 		else
 		{
@@ -418,17 +423,16 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 		solAssert(symbComponents.size() == tupleComponents->size(), "");
 		for (unsigned i = 0; i < symbComponents.size(); ++i)
 		{
-			auto sComponent = symbComponents.at(i);
 			auto tComponent = tupleComponents->at(i);
-			if (sComponent && tComponent)
+			if (tComponent)
 			{
 				if (auto varDecl = identifierToVariable(*tComponent))
-					m_context.addAssertion(sComponent->currentValue() == currentValue(*varDecl));
+					m_context.addAssertion(symbTuple->component(i) == currentValue(*varDecl));
 				else
 				{
 					if (!m_context.knownExpression(*tComponent))
 						createExpr(*tComponent);
-					m_context.addAssertion(sComponent->currentValue() == expr(*tComponent));
+					m_context.addAssertion(symbTuple->component(i) == expr(*tComponent));
 				}
 			}
 		}
@@ -807,13 +811,15 @@ void SMTEncoder::endVisit(Return const& _return)
 		{
 			auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(*_return.expression()));
 			solAssert(symbTuple, "");
-			auto const& components = symbTuple->components();
-			solAssert(components.size() == returnParams.size(), "");
+			solAssert(symbTuple->components().size() == returnParams.size(), "");
+
+			auto const* tupleType = dynamic_cast<TupleType const*>(_return.expression()->annotation().type);
+			solAssert(tupleType, "");
+			auto const& types = tupleType->components();
+			solAssert(types.size() == returnParams.size(), "");
+
 			for (unsigned i = 0; i < returnParams.size(); ++i)
-			{
-				solAssert(components.at(i), "");
-				m_context.addAssertion(components.at(i)->currentValue(returnParams.at(i)->type()) == m_context.newValue(*returnParams.at(i)));
-			}
+				m_context.addAssertion(symbTuple->component(i, types.at(i), returnParams.at(i)->type()) == m_context.newValue(*returnParams.at(i)));
 		}
 		else if (returnParams.size() == 1)
 			m_context.addAssertion(expr(*_return.expression(), returnParams.front()->type()) == m_context.newValue(*returnParams.front()));
@@ -1676,14 +1682,10 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
 		solAssert(symbComponents.size() == returnParams.size(), "");
 		for (unsigned i = 0; i < symbComponents.size(); ++i)
 		{
-			auto sComponent = symbComponents.at(i);
 			auto param = returnParams.at(i);
 			solAssert(param, "");
-			if (sComponent)
-			{
-				solAssert(m_context.knownVariable(*param), "");
-				m_context.addAssertion(sComponent->currentValue() == currentValue(*param));
-			}
+			solAssert(m_context.knownVariable(*param), "");
+			m_context.addAssertion(symbTuple->component(i) == currentValue(*param));
 		}
 	}
 	else if (returnParams.size() == 1)

libsolidity/formal/SMTLib2Interface.cpp

@@ -28,6 +28,7 @@
 #include <iostream>
 #include <memory>
 #include <stdexcept>
+#include <string>
 
 using namespace std;
 using namespace solidity;
@@ -50,6 +51,7 @@ void SMTLib2Interface::reset()
 	m_accumulatedOutput.clear();
 	m_accumulatedOutput.emplace_back();
 	m_variables.clear();
+	m_userSorts.clear();
 	write("(set-option :produce-models true)");
 	write("(set-logic ALL)");
 }
@@ -145,6 +147,14 @@ string SMTLib2Interface::toSExpr(smt::Expression const& _expr)
 		sexpr += "(as const " + toSmtLibSort(*arraySort) + ") ";
 		sexpr += toSExpr(_expr.arguments.at(1));
 	}
+	else if (_expr.name == "tuple_get")
+	{
+		solAssert(_expr.arguments.size() == 2, "");
+		auto tupleSort = dynamic_pointer_cast<TupleSort>(_expr.arguments.at(0).sort);
+		unsigned index = std::stoi(_expr.arguments.at(1).name);
+		solAssert(index < tupleSort->members.size(), "");
+		sexpr += tupleSort->members.at(index) + " " + toSExpr(_expr.arguments.at(0));
+	}
 	else
 	{
 		sexpr += _expr.name;
@@ -169,6 +179,22 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 		solAssert(arraySort.domain && arraySort.range, "");
 		return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')';
 	}
+	case Kind::Tuple:
+	{
+		auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
+		if (!m_userSorts.count(tupleSort.name))
+		{
+			m_userSorts.insert(tupleSort.name);
+			string decl("(declare-datatypes ((" + tupleSort.name + " 0)) (((" + tupleSort.name);
+			solAssert(tupleSort.members.size() == tupleSort.components.size(), "");
+			for (unsigned i = 0; i < tupleSort.members.size(); ++i)
+				decl += " (" + tupleSort.members.at(i) + " " + toSmtLibSort(*tupleSort.components.at(i)) + ")";
+			decl += "))))";
+			write(decl);
+		}
+
+		return tupleSort.name;
+	}
 	default:
 		solAssert(false, "Invalid SMT sort");
 	}

libsolidity/formal/SMTLib2Interface.h

@@ -74,6 +74,7 @@ private:
 
 	std::vector<std::string> m_accumulatedOutput;
 	std::map<std::string, SortPointer> m_variables;
+	std::set<std::string> m_userSorts;
 
 	std::map<util::h256, std::string> const& m_queryResponses;
 	std::vector<std::string> m_unhandledQueries;

libsolidity/formal/SolverInterface.h

@@ -94,7 +94,8 @@ public:
 			{"mod", 2},
 			{"select", 2},
 			{"store", 3},
-			{"const_array", 2}
+			{"const_array", 2},
+			{"tuple_get", 2}
 		};
 		return operatorsArity.count(name) && operatorsArity.at(name) == arguments.size();
 	}
@@ -166,6 +167,19 @@ public:
 		);
 	}
 
+	static Expression tuple_get(Expression _tuple, size_t _index)
+	{
+		solAssert(_tuple.sort->kind == Kind::Tuple, "");
+		std::shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_tuple.sort);
+		solAssert(tupleSort, "");
+		solAssert(_index < tupleSort->components.size(), "");
+		return Expression(
+			"tuple_get",
+			std::vector<Expression>{std::move(_tuple), Expression(_index)},
+			tupleSort->components.at(_index)
+		);
+	}
+
 	friend Expression operator!(Expression _a)
 	{
 		return Expression("not", std::move(_a), Kind::Bool);

libsolidity/formal/Sorts.h

@@ -33,7 +33,8 @@ enum class Kind
 	Bool,
 	Function,
 	Array,
-	Sort
+	Sort,
+	Tuple
 };
 
 struct Sort
@@ -115,6 +116,46 @@ struct SortSort: public Sort
 	SortPointer inner;
 };
 
+struct TupleSort: public Sort
+{
+	TupleSort(
+		std::string _name,
+		std::vector<std::string> _members,
+		std::vector<SortPointer> _components
+	):
+		Sort(Kind::Tuple),
+		name(std::move(_name)),
+		members(std::move(_members)),
+		components(std::move(_components))
+	{}
+
+	bool operator==(Sort const& _other) const override
+	{
+		if (!Sort::operator==(_other))
+			return false;
+		auto _otherTuple = dynamic_cast<TupleSort const*>(&_other);
+		solAssert(_otherTuple, "");
+		if (name != _otherTuple->name)
+			return false;
+		if (members != _otherTuple->members)
+			return false;
+		if (components.size() != _otherTuple->components.size())
+			return false;
+		if (!std::equal(
+			components.begin(),
+			components.end(),
+			_otherTuple->components.begin(),
+			[&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
+		))
+			return false;
+		return true;
+	}
+
+	std::string const name;
+	std::vector<std::string> const members;
+	std::vector<SortPointer> const components;
+};
+
 /** Frequently used sorts.*/
 struct SortProvider
 {

libsolidity/formal/SymbolicTypes.cpp

@@ -75,6 +75,21 @@ SortPointer smtSort(frontend::Type const& _type)
 			return make_shared<ArraySort>(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType()));
 		}
 	}
+	case Kind::Tuple:
+	{
+		auto tupleType = dynamic_cast<frontend::TupleType const*>(&_type);
+		solAssert(tupleType, "");
+		vector<string> members;
+		auto const& tupleName = _type.identifier();
+		auto const& components = tupleType->components();
+		for (unsigned i = 0; i < components.size(); ++i)
+			members.emplace_back(tupleName + "_accessor_" + to_string(i));
+		return make_shared<TupleSort>(
+			tupleName,
+			members,
+			smtSortAbstractFunction(tupleType->components())
+		);
+	}
 	default:
 		// Abstract case.
 		return SortProvider::intSort;
@@ -96,6 +111,17 @@ SortPointer smtSortAbstractFunction(frontend::Type const& _type)
 	return smtSort(_type);
 }
 
+vector<SortPointer> smtSortAbstractFunction(vector<frontend::TypePointer> const& _types)
+{
+	vector<SortPointer> sorts;
+	for (auto const& type: _types)
+		if (type)
+			sorts.push_back(smtSortAbstractFunction(*type));
+		else
+			sorts.push_back(SortProvider::intSort);
+	return sorts;
+}
+
 Kind smtKind(frontend::Type::Category _category)
 {
 	if (isNumber(_category))
@@ -106,6 +132,8 @@ Kind smtKind(frontend::Type::Category _category)
 		return Kind::Function;
 	else if (isMapping(_category) || isArray(_category))
 		return Kind::Array;
+	else if (isTuple(_category))
+		return Kind::Tuple;
 	// Abstract case.
 	return Kind::Int;
 }
@@ -350,4 +378,17 @@ void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _typ
 	}
 }
 
+optional<Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to)
+{
+	if (_to && _from)
+		// StringLiterals are encoded as SMT arrays in the generic case,
+		// but they can also be compared/assigned to fixed bytes, in which
+		// case they'd need to be encoded as numbers.
+		if (auto strType = dynamic_cast<StringLiteralType const*>(_from))
+			if (_to->category() == frontend::Type::Category::FixedBytes)
+				return smt::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
+
+	return std::nullopt;
+}
+
 }

libsolidity/formal/SymbolicTypes.h

@@ -31,6 +31,7 @@ std::vector<SortPointer> smtSort(std::vector<frontend::TypePointer> const& _type
 /// If _type has type Function, abstract it to Integer.
 /// Otherwise return smtSort(_type).
 SortPointer smtSortAbstractFunction(frontend::Type const& _type);
+std::vector<SortPointer> smtSortAbstractFunction(std::vector<frontend::TypePointer> const& _types);
 /// Returns the SMT kind that models the Solidity type type category _category.
 Kind smtKind(frontend::Type::Category _category);
 
@@ -69,4 +70,5 @@ void setSymbolicZeroValue(Expression _expr, frontend::TypePointer const& _type,
 void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context);
 void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
 
+std::optional<Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to);
 }

libsolidity/formal/SymbolicVariables.cpp

@@ -230,16 +230,9 @@ SymbolicArrayVariable::SymbolicArrayVariable(
 
 smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
 {
-	if (_targetType)
-	{
-		solAssert(m_originalType, "");
-		// StringLiterals are encoded as SMT arrays in the generic case,
-		// but they can also be compared/assigned to fixed bytes, in which
-		// case they'd need to be encoded as numbers.
-		if (auto strType = dynamic_cast<StringLiteralType const*>(m_originalType))
-			if (_targetType->category() == frontend::Type::Category::FixedBytes)
-				return smt::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
-	}
+	optional<smt::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
+	if (conversion)
+		return *conversion;
 
 	return SymbolicVariable::currentValue(_targetType);
 }
@@ -262,16 +255,34 @@ SymbolicTupleVariable::SymbolicTupleVariable(
 	SymbolicVariable(_type, _type, move(_uniqueName), _context)
 {
 	solAssert(isTuple(m_type->category()), "");
-	auto const& tupleType = dynamic_cast<TupleType const&>(*m_type);
-	auto const& componentsTypes = tupleType.components();
-	for (unsigned i = 0; i < componentsTypes.size(); ++i)
-		if (componentsTypes.at(i))
-		{
-			string componentName = m_uniqueName + "_component_" + to_string(i);
-			auto result = smt::newSymbolicVariable(*componentsTypes.at(i), componentName, m_context);
-			solAssert(result.second, "");
-			m_components.emplace_back(move(result.second));
-		}
-		else
-			m_components.emplace_back(nullptr);
+}
+
+SymbolicTupleVariable::SymbolicTupleVariable(
+	SortPointer _sort,
+	string _uniqueName,
+	EncodingContext& _context
+):
+	SymbolicVariable(move(_sort), move(_uniqueName), _context)
+{
+	solAssert(m_sort->kind == Kind::Tuple, "");
+}
+
+vector<SortPointer> const& SymbolicTupleVariable::components()
+{
+	auto tupleSort = dynamic_pointer_cast<TupleSort>(m_sort);
+	solAssert(tupleSort, "");
+	return tupleSort->components;
+}
+
+smt::Expression SymbolicTupleVariable::component(
+	size_t _index,
+	TypePointer _fromType,
+	TypePointer _toType
+)
+{
+	optional<smt::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
+	if (conversion)
+		return *conversion;
+
+	return smt::Expression::tuple_get(currentValue(), _index);
 }

libsolidity/formal/SymbolicVariables.h

@@ -249,14 +249,18 @@ public:
 		std::string _uniqueName,
 		EncodingContext& _context
 	);
+	SymbolicTupleVariable(
+		SortPointer _sort,
+		std::string _uniqueName,
+		EncodingContext& _context
+	);
 
-	std::vector<std::shared_ptr<SymbolicVariable>> const& components()
-	{
-		return m_components;
-	}
-
-private:
-	std::vector<std::shared_ptr<SymbolicVariable>> m_components;
+	std::vector<SortPointer> const& components();
+	Expression component(
+		size_t _index,
+		TypePointer _fromType = nullptr,
+		TypePointer _toType = nullptr
+	);
 };
 
 }

libsolidity/formal/Z3Interface.cpp

@@ -193,6 +193,11 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 			solAssert(arraySort && arraySort->domain, "");
 			return z3::const_array(z3Sort(*arraySort->domain), arguments[1]);
 		}
+		else if (n == "tuple_get")
+		{
+			size_t index = std::stoi(_expr.arguments[1].name);
+			return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), index))(arguments[0]);
+		}
 
 		solAssert(false, "");
 	}
@@ -217,6 +222,28 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
 		auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
 		return m_context.array_sort(z3Sort(*arraySort.domain), z3Sort(*arraySort.range));
 	}
+	case Kind::Tuple:
+	{
+		auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
+		vector<char const*> cMembers;
+		for (auto const& member: tupleSort.members)
+			cMembers.emplace_back(member.c_str());
+		/// Using this instead of the function below because with that one
+		/// we can't use `&sorts[0]` here.
+		vector<z3::sort> sorts;
+		for (auto const& sort: tupleSort.components)
+			sorts.push_back(z3Sort(*sort));
+		z3::func_decl_vector projs(m_context);
+		z3::func_decl tupleConstructor = m_context.tuple_sort(
+			tupleSort.name.c_str(),
+			tupleSort.members.size(),
+			&cMembers[0],
+			&sorts[0],
+			projs
+		);
+		return tupleConstructor.range();
+	}
+
 	default:
 		break;
 	}