Merge pull request #8848 from ethereum/smt_array_length_tuple

[SMTChecker] Support array length

Changelog.md

@@ -5,6 +5,7 @@ Language Features:
 
 Compiler Features:
  * Build system: Update the soljson.js build to emscripten 1.39.15 and boost 1.73.0 and include Z3 for integrated SMTChecker support without the callback mechanism.
+ * SMTChecker: Support array ``length``.
 
 
 Bugfixes:

libsolidity/formal/CVC4Interface.cpp

@@ -206,6 +206,15 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 			CVC4::Expr s = dt[0][index].getSelector();
 			return m_context.mkExpr(CVC4::kind::APPLY_SELECTOR, s, arguments[0]);
 		}
+		else if (n == "tuple_constructor")
+		{
+			shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.sort);
+			solAssert(tupleSort, "");
+			CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
+			CVC4::Datatype const& dt = tt.getDatatype();
+			CVC4::Expr c = dt[0].getConstructor();
+			return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments);
+		}
 
 		solAssert(false, "");
 	}

libsolidity/formal/SMTEncoder.cpp

@@ -890,6 +890,33 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 			return false;
 		}
 	}
+	else if (exprType->category() == Type::Category::Array)
+	{
+		_memberAccess.expression().accept(*this);
+		if (_memberAccess.memberName() == "length")
+		{
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_memberAccess.expression()));
+			solAssert(symbArray, "");
+			defineExpr(_memberAccess, symbArray->length());
+			m_uninterpretedTerms.insert(&_memberAccess);
+			setSymbolicUnknownValue(
+				expr(_memberAccess),
+				_memberAccess.annotation().type,
+				m_context
+			);
+		}
+		else
+		{
+			auto const& name = _memberAccess.memberName();
+			solAssert(name == "push" || name == "pop", "");
+			m_errorReporter.warning(
+				9098_error,
+				_memberAccess.location(),
+				"Assertion checker does not yet support array member \"" + name + "\"."
+			);
+		}
+		return false;
+	}
 	else
 		m_errorReporter.warning(
 			7650_error,
@@ -939,9 +966,10 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		return;
 	}
 
-	solAssert(array, "");
+	auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
+	solAssert(arrayVar, "");
 	defineExpr(_indexAccess, smt::Expression::select(
-		array->currentValue(),
+		arrayVar->elements(),
 		expr(*_indexAccess.indexExpression())
 	));
 	setSymbolicUnknownValue(
@@ -1013,16 +1041,20 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 					return false;
 				});
 
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.variable(*varDecl));
 			smt::Expression store = smt::Expression::store(
-				m_context.variable(*varDecl)->currentValue(),
+				symbArray->elements(),
 				expr(*indexAccess->indexExpression()),
 				toStore
 			);
-			m_context.addAssertion(m_context.newValue(*varDecl) == store);
+			auto oldLength = symbArray->length();
+			symbArray->increaseIndex();
+			m_context.addAssertion(symbArray->elements() == store);
+			m_context.addAssertion(symbArray->length() == oldLength);
 			// Update the SMT select value after the assignment,
 			// necessary for sound models.
 			defineExpr(*indexAccess, smt::Expression::select(
-				m_context.variable(*varDecl)->currentValue(),
+				symbArray->elements(),
 				expr(*indexAccess->indexExpression())
 			));
 
@@ -1030,7 +1062,12 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 		}
 		else if (auto base = dynamic_cast<IndexAccess const*>(&indexAccess->baseExpression()))
 		{
-			toStore = smt::Expression::store(expr(*base), expr(*indexAccess->indexExpression()), toStore);
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*base));
+			solAssert(symbArray, "");
+			toStore = smt::Expression::tuple_constructor(
+				smt::Expression(base->annotation().type),
+				{smt::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
+			);
 			indexAccess = base;
 		}
 		else
@@ -1326,7 +1363,14 @@ smt::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression const& _value)
 {
-	assignment(_variable, expr(_value, _variable.type()));
+	// In general, at this point, the SMT sorts of _variable and _value are the same,
+	// even if there is implicit conversion.
+	// This is a special case where the SMT sorts are different.
+	// For now we are unaware of other cases where this happens, but if they do appear
+	// we should extract this into an `implicitConversion` function.
+	if (_variable.type()->category() != Type::Category::Array || _value.annotation().type->category() != Type::Category::StringLiteral)
+		assignment(_variable, expr(_value, _variable.type()));
+	// TODO else { store each string literal byte into the array }
 }
 
 void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expression const& _value)
@@ -1616,7 +1660,7 @@ SMTEncoder::VariableIndices SMTEncoder::copyVariableIndices()
 void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
 {
 	for (auto const& var: _indices)
-		m_context.variable(*var.first)->index() = var.second;
+		m_context.variable(*var.first)->setIndex(var.second);
 }
 
 void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)

libsolidity/formal/SMTLib2Interface.cpp

@@ -153,7 +153,15 @@ string SMTLib2Interface::toSExpr(smt::Expression const& _expr)
 		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));
+		sexpr += "|" + tupleSort->members.at(index) + "| " + toSExpr(_expr.arguments.at(0));
+	}
+	else if (_expr.name == "tuple_constructor")
+	{
+		auto tupleSort = dynamic_pointer_cast<TupleSort>(_expr.sort);
+		solAssert(tupleSort, "");
+		sexpr += "|" + tupleSort->name + "|";
+		for (auto const& arg: _expr.arguments)
+			sexpr += " " + toSExpr(arg);
 	}
 	else
 	{
@@ -182,18 +190,19 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
 	case Kind::Tuple:
 	{
 		auto const& tupleSort = dynamic_cast<TupleSort const&>(_sort);
-		if (!m_userSorts.count(tupleSort.name))
+		string tupleName = "|" + tupleSort.name + "|";
+		if (!m_userSorts.count(tupleName))
 		{
-			m_userSorts.insert(tupleSort.name);
-			string decl("(declare-datatypes ((" + tupleSort.name + " 0)) (((" + tupleSort.name);
+			m_userSorts.insert(tupleName);
+			string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName);
 			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 += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")";
 			decl += "))))";
 			write(decl);
 		}
 
-		return tupleSort.name;
+		return tupleName;
 	}
 	default:
 		solAssert(false, "Invalid SMT sort");

libsolidity/formal/SSAVariable.cpp

@@ -29,5 +29,12 @@ SSAVariable::SSAVariable()
 void SSAVariable::resetIndex()
 {
 	m_currentIndex = 0;
-	m_nextFreeIndex = make_unique<unsigned>(1);
+	m_nextFreeIndex = 1;
+}
+
+void SSAVariable::setIndex(unsigned _index)
+{
+	m_currentIndex = _index;
+	if (m_nextFreeIndex <= _index)
+		m_nextFreeIndex = _index + 1;
 }

libsolidity/formal/SSAVariable.h

@@ -29,7 +29,10 @@ class SSAVariable
 {
 public:
 	SSAVariable();
+	/// Resets index to 0 and next index to 1.
 	void resetIndex();
+	/// Sets index to _index and only adjusts next if next <= _index.
+	void setIndex(unsigned _index);
 
 	/// This function returns the current index of this SSA variable.
 	unsigned index() const { return m_currentIndex; }
@@ -37,12 +40,12 @@ public:
 
 	unsigned operator++()
 	{
-		return m_currentIndex = (*m_nextFreeIndex)++;
+		return m_currentIndex = m_nextFreeIndex++;
 	}
 
 private:
 	unsigned m_currentIndex;
-	std::unique_ptr<unsigned> m_nextFreeIndex;
+	unsigned m_nextFreeIndex;
 };
 
 }

libsolidity/formal/SolverInterface.h

@@ -28,6 +28,7 @@
 #include <boost/noncopyable.hpp>
 #include <cstdio>
 #include <map>
+#include <memory>
 #include <string>
 #include <vector>
 
@@ -63,7 +64,8 @@ class Expression
 	friend class SolverInterface;
 public:
 	explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
-	explicit Expression(frontend::TypePointer _type): Expression(_type->toString(), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
+	explicit Expression(frontend::TypePointer _type): Expression(_type->toString(true), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
+	explicit Expression(std::shared_ptr<SortSort> _sort): Expression("", {}, _sort) {}
 	Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
 	Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
 	Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {}
@@ -76,6 +78,13 @@ public:
 
 	bool hasCorrectArity() const
 	{
+		if (name == "tuple_constructor")
+		{
+			auto tupleSort = std::dynamic_pointer_cast<TupleSort>(sort);
+			solAssert(tupleSort, "");
+			return arguments.size() == tupleSort->components.size();
+		}
+
 		static std::map<std::string, unsigned> const operatorsArity{
 			{"ite", 3},
 			{"not", 1},
@@ -138,8 +147,7 @@ public:
 	/// The function is pure and returns the modified array.
 	static Expression store(Expression _array, Expression _index, Expression _element)
 	{
-		solAssert(_array.sort->kind == Kind::Array, "");
-		std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
+		auto arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
 		solAssert(arraySort, "");
 		solAssert(_index.sort, "");
 		solAssert(_element.sort, "");
@@ -180,6 +188,20 @@ public:
 		);
 	}
 
+	static Expression tuple_constructor(Expression _tuple, std::vector<Expression> _arguments)
+	{
+		solAssert(_tuple.sort->kind == Kind::Sort, "");
+		auto sortSort = std::dynamic_pointer_cast<SortSort>(_tuple.sort);
+		auto tupleSort = std::dynamic_pointer_cast<TupleSort>(sortSort->inner);
+		solAssert(tupleSort, "");
+		solAssert(_arguments.size() == tupleSort->components.size(), "");
+		return Expression(
+			"tuple_constructor",
+			std::move(_arguments),
+			tupleSort
+		);
+	}
+
 	friend Expression operator!(Expression _a)
 	{
 		return Expression("not", std::move(_a), Kind::Bool);

libsolidity/formal/SymbolicState.cpp

@@ -47,7 +47,7 @@ Expression SymbolicState::balance()
 
 Expression SymbolicState::balance(Expression _address)
 {
-	return Expression::select(m_balances.currentValue(), move(_address));
+	return Expression::select(m_balances.elements(), move(_address));
 }
 
 void SymbolicState::transfer(Expression _from, Expression _to, Expression _value)
@@ -72,11 +72,13 @@ void SymbolicState::transfer(Expression _from, Expression _to, Expression _value
 void SymbolicState::addBalance(Expression _address, Expression _value)
 {
 	auto newBalances = Expression::store(
-		m_balances.currentValue(),
+		m_balances.elements(),
 		_address,
 		balance(_address) + move(_value)
 	);
+	auto oldLength = m_balances.length();
 	m_balances.increaseIndex();
-	m_context.addAssertion(newBalances == m_balances.currentValue());
+	m_context.addAssertion(m_balances.elements() == newBalances);
+	m_context.addAssertion(m_balances.length() == oldLength);
 }
 

libsolidity/formal/SymbolicTypes.cpp

@@ -21,6 +21,7 @@
 #include <libsolidity/ast/Types.h>
 #include <libsolutil/CommonData.h>
 #include <memory>
+#include <vector>
 
 using namespace std;
 
@@ -55,17 +56,18 @@ SortPointer smtSort(frontend::Type const& _type)
 	}
 	case Kind::Array:
 	{
+		shared_ptr<ArraySort> array;
 		if (isMapping(_type.category()))
 		{
 			auto mapType = dynamic_cast<frontend::MappingType const*>(&_type);
 			solAssert(mapType, "");
-			return make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
+			array = make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
 		}
 		else if (isStringLiteral(_type.category()))
 		{
 			auto stringLitType = dynamic_cast<frontend::StringLiteralType const*>(&_type);
 			solAssert(stringLitType, "");
-			return make_shared<ArraySort>(SortProvider::intSort, SortProvider::intSort);
+			array = make_shared<ArraySort>(SortProvider::intSort, SortProvider::intSort);
 		}
 		else
 		{
@@ -78,8 +80,25 @@ SortPointer smtSort(frontend::Type const& _type)
 				solAssert(false, "");
 
 			solAssert(arrayType, "");
-			return make_shared<ArraySort>(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType()));
+			array = make_shared<ArraySort>(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType()));
 		}
+
+		string tupleName;
+		if (
+			auto arrayType = dynamic_cast<ArrayType const*>(&_type);
+			(arrayType && arrayType->isString()) ||
+			_type.category() == frontend::Type::Category::ArraySlice ||
+			_type.category() == frontend::Type::Category::StringLiteral
+		)
+			tupleName = "bytes_tuple";
+		else
+			tupleName = _type.toString(true) + "_tuple";
+
+		return make_shared<TupleSort>(
+			tupleName,
+			vector<string>{tupleName + "_accessor_array", tupleName + "_accessor_length"},
+			vector<SortPointer>{array, SortProvider::intSort}
+		);
 	}
 	case Kind::Tuple:
 	{
@@ -219,9 +238,7 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
 		else
 			var = make_shared<SymbolicIntVariable>(type, type, _uniqueName, _context);
 	}
-	else if (isMapping(_type.category()))
-		var = make_shared<SymbolicMappingVariable>(type, _uniqueName, _context);
-	else if (isArray(_type.category()))
+	else if (isMapping(_type.category()) || isArray(_type.category()))
 		var = make_shared<SymbolicArrayVariable>(type, type, _uniqueName, _context);
 	else if (isTuple(_type.category()))
 		var = make_shared<SymbolicTupleVariable>(type, _uniqueName, _context);
@@ -349,11 +366,26 @@ Expression zeroValue(frontend::TypePointer const& _type)
 			return Expression(false);
 		if (isArray(_type->category()) || isMapping(_type->category()))
 		{
+			auto tupleSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
+			solAssert(tupleSort, "");
+			auto sortSort = make_shared<SortSort>(tupleSort->components.front());
+
+			std::optional<Expression> zeroArray;
+			auto length = bigint(0);
 			if (auto arrayType = dynamic_cast<ArrayType const*>(_type))
-				return Expression::const_array(Expression(arrayType), zeroValue(arrayType->baseType()));
-			auto mappingType = dynamic_cast<MappingType const*>(_type);
-			solAssert(mappingType, "");
-			return Expression::const_array(Expression(mappingType), zeroValue(mappingType->valueType()));
+			{
+				zeroArray = Expression::const_array(Expression(sortSort), zeroValue(arrayType->baseType()));
+				if (!arrayType->isDynamicallySized())
+					length = bigint(arrayType->length());
+			}
+			else if (auto mappingType = dynamic_cast<MappingType const*>(_type))
+				zeroArray = Expression::const_array(Expression(sortSort), zeroValue(mappingType->valueType()));
+			else
+				solAssert(false, "");
+
+			solAssert(zeroArray, "");
+			return Expression::tuple_constructor(Expression(_type), vector<Expression>{*zeroArray, length});
+
 		}
 		solAssert(false, "");
 	}

libsolidity/formal/SymbolicVariables.cpp

@@ -86,6 +86,12 @@ smt::Expression SymbolicVariable::resetIndex()
 	return currentValue();
 }
 
+smt::Expression SymbolicVariable::setIndex(unsigned _index)
+{
+	m_ssa->setIndex(_index);
+	return currentValue();
+}
+
 smt::Expression SymbolicVariable::increaseIndex()
 {
 	++(*m_ssa);
@@ -179,6 +185,12 @@ smt::Expression SymbolicFunctionVariable::resetIndex()
 	return m_abstract.resetIndex();
 }
 
+smt::Expression SymbolicFunctionVariable::setIndex(unsigned _index)
+{
+	SymbolicVariable::setIndex(_index);
+	return m_abstract.setIndex(_index);
+}
+
 smt::Expression SymbolicFunctionVariable::increaseIndex()
 {
 	++(*m_ssa);
@@ -197,46 +209,6 @@ void SymbolicFunctionVariable::resetDeclaration()
 	m_declaration = m_context.newVariable(currentName(), m_sort);
 }
 
-SymbolicMappingVariable::SymbolicMappingVariable(
-	frontend::TypePointer _type,
-	string _uniqueName,
-	EncodingContext& _context
-):
-	SymbolicVariable(_type, _type, move(_uniqueName), _context)
-{
-	solAssert(isMapping(m_type->category()), "");
-}
-
-SymbolicArrayVariable::SymbolicArrayVariable(
-	frontend::TypePointer _type,
-	frontend::TypePointer _originalType,
-	string _uniqueName,
-	EncodingContext& _context
-):
-	SymbolicVariable(_type, _originalType, move(_uniqueName), _context)
-{
-	solAssert(isArray(m_type->category()), "");
-}
-
-SymbolicArrayVariable::SymbolicArrayVariable(
-	SortPointer _sort,
-	string _uniqueName,
-	EncodingContext& _context
-):
-	SymbolicVariable(move(_sort), move(_uniqueName), _context)
-{
-	solAssert(m_sort->kind == Kind::Array, "");
-}
-
-smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
-{
-	optional<smt::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
-	if (conversion)
-		return *conversion;
-
-	return SymbolicVariable::currentValue(_targetType);
-}
-
 SymbolicEnumVariable::SymbolicEnumVariable(
 	frontend::TypePointer _type,
 	string _uniqueName,
@@ -286,3 +258,62 @@ smt::Expression SymbolicTupleVariable::component(
 
 	return smt::Expression::tuple_get(currentValue(), _index);
 }
+
+SymbolicArrayVariable::SymbolicArrayVariable(
+	frontend::TypePointer _type,
+	frontend::TypePointer _originalType,
+	string _uniqueName,
+	EncodingContext& _context
+):
+	SymbolicVariable(_type, _originalType, move(_uniqueName), _context),
+	m_pair(
+		smtSort(*_type),
+		m_uniqueName + "_length_pair",
+		m_context
+	)
+{
+	solAssert(isArray(m_type->category()) || isMapping(m_type->category()), "");
+}
+
+SymbolicArrayVariable::SymbolicArrayVariable(
+	SortPointer _sort,
+	string _uniqueName,
+	EncodingContext& _context
+):
+	SymbolicVariable(move(_sort), move(_uniqueName), _context),
+	m_pair(
+		std::make_shared<TupleSort>(
+			"array_length_pair",
+			std::vector<std::string>{"array", "length"},
+			std::vector<SortPointer>{m_sort, SortProvider::intSort}
+		),
+		m_uniqueName + "_array_length_pair",
+		m_context
+	)
+{
+	solAssert(m_sort->kind == Kind::Array, "");
+}
+
+smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
+{
+	optional<smt::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
+	if (conversion)
+		return *conversion;
+
+	return m_pair.currentValue();
+}
+
+smt::Expression SymbolicArrayVariable::valueAtIndex(int _index) const
+{
+	return m_pair.valueAtIndex(_index);
+}
+
+smt::Expression SymbolicArrayVariable::elements()
+{
+	return m_pair.component(0);
+}
+
+smt::Expression SymbolicArrayVariable::length()
+{
+	return m_pair.component(1);
+}

libsolidity/formal/SymbolicVariables.h

@@ -56,6 +56,7 @@ public:
 	virtual Expression valueAtIndex(int _index) const;
 	virtual std::string nameAtIndex(int _index) const;
 	virtual Expression resetIndex();
+	virtual Expression setIndex(unsigned _index);
 	virtual Expression increaseIndex();
 	virtual Expression operator()(std::vector<Expression> /*_arguments*/) const
 	{
@@ -169,6 +170,7 @@ public:
 	Expression functionValueAtIndex(int _index) const;
 
 	Expression resetIndex() override;
+	Expression setIndex(unsigned _index) override;
 	Expression increaseIndex() override;
 
 	Expression operator()(std::vector<Expression> _arguments) const override;
@@ -189,42 +191,6 @@ private:
 	};
 };
 
-/**
- * Specialization of SymbolicVariable for Mapping
- */
-class SymbolicMappingVariable: public SymbolicVariable
-{
-public:
-	SymbolicMappingVariable(
-		frontend::TypePointer _type,
-		std::string _uniqueName,
-		EncodingContext& _context
-	);
-};
-
-/**
- * Specialization of SymbolicVariable for Array
- */
-class SymbolicArrayVariable: public SymbolicVariable
-{
-public:
-	SymbolicArrayVariable(
-		frontend::TypePointer _type,
-		frontend::TypePointer _originalTtype,
-		std::string _uniqueName,
-		EncodingContext& _context
-	);
-	SymbolicArrayVariable(
-		SortPointer _sort,
-		std::string _uniqueName,
-		EncodingContext& _context
-	);
-
-	SymbolicArrayVariable(SymbolicArrayVariable&&) = default;
-
-	Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
-};
-
 /**
  * Specialization of SymbolicVariable for Enum
  */
@@ -263,4 +229,38 @@ public:
 	);
 };
 
+/**
+ * Specialization of SymbolicVariable for Array
+ */
+class SymbolicArrayVariable: public SymbolicVariable
+{
+public:
+	SymbolicArrayVariable(
+		frontend::TypePointer _type,
+		frontend::TypePointer _originalTtype,
+		std::string _uniqueName,
+		EncodingContext& _context
+	);
+	SymbolicArrayVariable(
+		SortPointer _sort,
+		std::string _uniqueName,
+		EncodingContext& _context
+	);
+
+	SymbolicArrayVariable(SymbolicArrayVariable&&) = default;
+
+	Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
+	Expression valueAtIndex(int _index) const override;
+	Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); }
+	Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); }
+	Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); }
+	Expression elements();
+	Expression length();
+
+	SortPointer tupleSort() { return m_pair.sort(); }
+
+private:
+	SymbolicTupleVariable m_pair;
+};
+
 }

libsolidity/formal/Z3Interface.cpp

@@ -198,6 +198,15 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 			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]);
 		}
+		else if (n == "tuple_constructor")
+		{
+			auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, z3Sort(*_expr.sort)));
+			solAssert(constructor.arity() == arguments.size(), "");
+			z3::expr_vector args(m_context);
+			for (auto const& arg: arguments)
+				args.push_back(arg);
+			return constructor(args);
+		}
 
 		solAssert(false, "");
 	}

test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_memory_to_memory.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	function f(uint[][] memory arr) public pure {
+		uint[][] memory arr2 = arr;
+		assert(arr2[0].length == arr[0].length);
+		assert(arr.length == arr2.length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	uint[][] arr;
+	uint[][] arr2;
+	function f() public view {
+		assert(arr2[0].length == arr[0].length);
+		assert(arr2.length == arr.length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_memory_to_storage.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	uint[][] arr;
+	function f(uint[][] memory arr2) public {
+		arr = arr2;
+		assert(arr2[0].length == arr[0].length);
+		assert(arr2.length == arr.length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	uint[][] arr;
+	function f() public view {
+		uint[][] memory arr2 = arr;
+		assert(arr2[0].length == arr[0].length);
+		assert(arr2.length == arr.length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol

@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint[]) map;
+	function f() public view {
+		assert(map[0].length == map[1].length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint[]) map;
+	function f(uint x, uint y) public view {
+		require(x == y);
+		assert(map[x].length == map[y].length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2d_1.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint[][]) map;
+	function f(uint x, uint y) public view {
+		require(x == y);
+		assert(map[x][0].length == map[y][0].length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint[] arr;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.arr.length == s2.arr.length);
+	}
+}
+// ----
+// Warning: (76-80): Assertion checker does not yet support the type of this variable.
+// Warning: (83-87): Assertion checker does not yet support the type of this variable.
+// Warning: (126-132): Assertion checker does not yet support this expression.
+// Warning: (126-128): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (143-149): Assertion checker does not yet support this expression.
+// Warning: (143-145): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (119-157): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint[][] arr;
+	}
+	S s1;
+	S s2;
+	function f() public view {
+		assert(s1.arr[0].length == s2.arr[0].length);
+	}
+}
+// ----
+// Warning: (78-82): Assertion checker does not yet support the type of this variable.
+// Warning: (85-89): Assertion checker does not yet support the type of this variable.
+// Warning: (128-134): Assertion checker does not yet support this expression.
+// Warning: (128-130): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (128-137): Assertion checker does not yet implement this expression.
+// Warning: (148-154): Assertion checker does not yet support this expression.
+// Warning: (148-150): Assertion checker does not yet implement type struct C.S storage ref
+// Warning: (148-157): Assertion checker does not yet implement this expression.
+// Warning: (121-165): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_assignment_2d_memory_to_memory.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+pragma experimental ABIEncoderV2;
+
+contract C {
+	function f(uint[][] memory arr) public pure {
+		uint[][] memory arr2 = arr;
+		assert(arr2.length == arr.length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_assignment_memory_to_memory.sol

@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(uint[] memory arr) public pure {
+		uint[] memory arr2 = arr;
+		assert(arr2.length == arr.length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_assignment_storage_to_storage.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] arr;
+	uint[] arr2;
+	function f() public {
+		arr2 = arr;
+		assert(arr2.length == arr.length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_basic.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] arr;
+	function f() public view {
+		uint x = arr.length;
+		uint y = x;
+		assert(arr.length == y);
+		assert(arr.length != y);
+	}
+}
+// ----
+// Warning: (153-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_copy_memory_to_storage.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] arr;
+	function f(uint[] memory marr) public {
+		arr = marr;
+		assert(marr.length == arr.length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_copy_storage_to_memory.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] arr;
+	function f() public view {
+		uint[] memory marr = arr;
+		assert(marr.length == arr.length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_function_call.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] arr;
+	function f() public view {
+		assert(arr.length == g().length);
+	}
+	function g() internal pure returns (uint[] memory) {
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] arr;
+	function f() public view {
+		uint[] memory arr2 = arr;
+		arr2[2] = 3;
+		assert(arr.length == arr2.length);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] arr;
+	uint[][] arr2;
+	function f() public {
+		uint x = arr[2].length;
+		uint y = arr[3].length;
+		uint z = arr.length;
+		arr[2][333] = 444;
+		assert(arr[2].length == x);
+		assert(arr[3].length == y);
+		assert(arr.length == z);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] arr;
+	uint[][] arr2;
+	function f() public {
+		uint x = arr[2].length;
+		uint y = arr[3].length;
+		uint z = arr.length;
+		arr[2][333] = 444;
+		assert(arr[2].length != x);
+		assert(arr[3].length != y);
+		assert(arr.length != z);
+	}
+}
+// ----
+// Warning: (198-224): Assertion violation happens here
+// Warning: (228-254): Assertion violation happens here
+// Warning: (258-281): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] arr;
+	uint[][] arr2;
+	function f() public {
+		uint x = arr[2].length;
+		uint y = arr[3].length;
+		uint z = arr.length;
+		uint t = arr[5].length;
+		arr[5] = arr[8];
+		assert(arr[2].length == x);
+		assert(arr[3].length == y);
+		assert(arr.length == z);
+		assert(arr[5].length == t);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] arr;
+	uint[][] arr2;
+	function f() public {
+		uint x = arr[2].length;
+		uint y = arr[3].length;
+		uint z = arr.length;
+		uint t = arr[5].length;
+		arr[5] = arr[8];
+		assert(arr[2].length != x);
+		assert(arr[3].length != y);
+		assert(arr.length != z);
+		assert(arr[5].length != t);
+	}
+}
+// ----
+// Warning: (222-248): Assertion violation happens here
+// Warning: (252-278): Assertion violation happens here
+// Warning: (282-305): Assertion violation happens here
+// Warning: (309-335): Assertion violation happens here

test/libsolidity/smtCheckerTests/complex/MerkleProof.sol

@@ -34,9 +34,7 @@ library MerkleProof {
 }
 
 // ----
-// Warning: (755-767): Assertion checker does not yet support this expression.
 // Warning: (988-991): Assertion checker does not yet implement type abi
 // Warning: (988-1032): Assertion checker does not yet implement this type of function call.
 // Warning: (1175-1178): Assertion checker does not yet implement type abi
 // Warning: (1175-1219): Assertion checker does not yet implement this type of function call.
-// Warning: (755-767): Assertion checker does not yet support this expression.

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol

@@ -19,5 +19,7 @@ contract LoopFor2 {
 	}
 }
 // ----
+// Warning: (317-337): Error trying to invoke SMT solver.
+// Warning: (317-337): Assertion violation happens here
 // Warning: (341-360): Assertion violation happens here
 // Warning: (364-383): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol

@@ -4,6 +4,7 @@ contract C
 {
 	uint[][] a;
 	function f(bool b) public {
+		a[1][1] = 512;
 		a[2][3] = 4;
 		if (b)
 			delete a;
@@ -16,3 +17,4 @@ contract C
 // ====
 // SMTSolvers: z3
 // ----
+// Warning: (191-211): Assertion violation happens here

test/libsolidity/smtCheckerTests/special/msg_data.sol

@@ -7,5 +7,4 @@ contract C
 	}
 }
 // ----
-// Warning: (86-101): Assertion checker does not yet support this expression.
 // Warning: (79-106): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/string_1.sol

@@ -7,6 +7,4 @@ contract C
 	}
 }
 // ----
-// Warning: (117-133): Assertion checker does not yet support this expression.
-// Warning: (137-153): Assertion checker does not yet support this expression.
 // Warning: (110-154): Assertion violation happens here

test/libsolidity/smtCheckerTestsJSON/multi.json

@@ -3,8 +3,8 @@
 	{
 		"smtlib2responses":
 		{
-			"0x9c50514d749eabf3c13d97ad7d787e682dd99a114bad652b10a01b8c6ad6c1fb": "sat\n((|EVALEXPR_0| 1))\n",
-			"0xb524e7c577188e2e36f0e67fead51269fa0f8b8fb41bff2d973dcf584d38cd1e": "sat\n((|EVALEXPR_0| 0))\n"
+			"0x45598870c7c0bc4c4f61acad7e0dd9399fb28aa3df198379dd36a95d70814ef8": "sat\n((|EVALEXPR_0| 1))\n",
+			"0xee335f8104fdb81b6e5fb418725923b81f7d78ffbd6bf95fb82e5593a1ac366a": "sat\n((|EVALEXPR_0| 0))\n"
 		}
 	}
 }

test/libsolidity/smtCheckerTestsJSON/simple.json

@@ -3,7 +3,7 @@
 	{
 		"smtlib2responses":
 		{
-			"0x45c37a9829e623d7838d82b547d297cd446d6b5faff36c53a56862fcee50fb41": "sat\n((|EVALEXPR_0| 0))\n"
+			"0x535c76d6b87d14bd4b4bf1014d14b8e91b648f073a68f9f267c4fe1df570bc14": "sat\n((|EVALEXPR_0| 0))\n"
 		}
 	}
 }