[SMTChecker] Supporting inline arrays.

libsolidity/formal/SMTEncoder.cpp

@@ -391,11 +391,13 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 	createExpr(_tuple);
 
 	if (_tuple.isInlineArray())
-		m_errorReporter.warning(
-			2177_error,
-			_tuple.location(),
-			"Assertion checker does not yet implement inline arrays."
-		);
+	{
+		// Add constraints for the length and values as it is known.
+		auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_tuple));
+		solAssert(symbArray, "");
+
+		addArrayLiteralAssertions(*symbArray, applyMap(_tuple.components(), [&](auto const& c) { return expr(*c); }));
+	}
 	else if (_tuple.components().size() == 1)
 		defineExpr(_tuple, expr(*_tuple.components().front()));
 	else
@@ -965,12 +967,10 @@ void SMTEncoder::endVisit(Literal const& _literal)
 		auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_literal));
 		solAssert(symbArray, "");
 
-		auto value = _literal.value();
-		m_context.addAssertion(symbArray->length() == value.length());
-		for (size_t i = 0; i < value.length(); i++)
-			m_context.addAssertion(
-				smtutil::Expression::select(symbArray->elements(), i) == size_t(value[i])
-			);
+		addArrayLiteralAssertions(
+			*symbArray,
+			applyMap(_literal.value(), [&](auto const& c) { return smtutil::Expression{size_t(c)}; })
+		);
 	}
 	else
 	{
@@ -984,6 +984,16 @@ void SMTEncoder::endVisit(Literal const& _literal)
 	}
 }
 
+void SMTEncoder::addArrayLiteralAssertions(
+	smt::SymbolicArrayVariable& _symArray,
+	vector<smtutil::Expression> const& _elementValues
+)
+{
+	m_context.addAssertion(_symArray.length() == _elementValues.size());
+	for (size_t i = 0; i < _elementValues.size(); i++)
+		m_context.addAssertion(smtutil::Expression::select(_symArray.elements(), i) == _elementValues[i]);
+}
+
 void SMTEncoder::endVisit(Return const& _return)
 {
 	if (_return.expression() && m_context.knownExpression(*_return.expression()))

libsolidity/formal/SMTEncoder.h

@@ -169,6 +169,11 @@ protected:
 	/// an empty array.
 	virtual void makeArrayPopVerificationTarget(FunctionCall const&) {}
 
+	void addArrayLiteralAssertions(
+		smt::SymbolicArrayVariable& _symArray,
+		std::vector<smtutil::Expression> const& _elementValues
+	);
+
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
 	smtutil::Expression division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type);