Merge pull request #9977 from ethereum/smtArrayLiterals

[SMTChecker] Supporting inline arrays.

Changelog.md

@@ -5,7 +5,7 @@ Language Features:
 
 
 Compiler Features:
-
+ * SMTChecker: Support inline arrays.
 
 Bugfixes:
  * Code generator: Fix internal compiler error when referencing members via module name but not using the reference.

libsolidity/formal/SMTEncoder.cpp

@@ -391,11 +391,13 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 	createExpr(_tuple);
 
 	if (_tuple.isInlineArray())
-		m_errorReporter.warning(
+	{
-			2177_error,
+		// Add constraints for the length and values as it is known.
-			_tuple.location(),
+		auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(_tuple));
-			"Assertion checker does not yet implement inline arrays."
+		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();
+		addArrayLiteralAssertions(
-		m_context.addAssertion(symbArray->length() == value.length());
+			*symbArray,
-		for (size_t i = 0; i < value.length(); i++)
+			applyMap(_literal.value(), [&](auto const& c) { return smtutil::Expression{size_t(c)}; })
-			m_context.addAssertion(
+		);
-				smtutil::Expression::select(symbArray->elements(), i) == size_t(value[i])
-			);
 	}
 	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);

test/libsolidity/smtCheckerTests/types/array_literal_1.sol

@@ -4,8 +4,9 @@ contract C
 {
 	function f() public pure {
 		uint[3] memory array = [uint(1), 2, 3];
+		assert(array[0] == 1);
+		assert(array[1] == 2);
+		assert(array[2] == 3);
 	}
 }
 // ----
-// Warning 2072: (76-96): Unused local variable.
-// Warning 2177: (99-114): Assertion checker does not yet implement inline arrays.

test/libsolidity/smtCheckerTests/types/array_literal_2.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint[3] memory a = [uint(1), 2, 3];
+		uint[3] memory b = [uint(1), 2, 4];
+		assert(a[0] == b[0]);
+		assert(a[1] == b[1]);
+		assert(a[2] == b[2]); // fails
+	}
+}
+// ----
+// Warning 6328: (200-220): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/array_literal_3.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		(uint[3] memory a, uint[3] memory b) = ([uint(1), 2, 3], [uint(1), 2, 4]);
+		assert(a[0] == b[0]);
+		assert(a[1] == b[1]);
+		assert(a[2] == b[2]); // fails
+	}
+}
+// ----
+// Warning 6328: (201-221): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/array_literal_4.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool c) public pure {
+		uint[3] memory a = c ? [uint(1), 2, 3] : [uint(1), 2, 4];
+		uint[3] memory b = [uint(1), 2, c ? 3 : 4];
+		assert(a[0] == b[0]);
+		assert(a[1] == b[1]);
+		assert(a[2] == b[2]);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/types/array_literal_5.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] s;
+	function f() public {
+		uint[3] memory a = [uint(1), 2, 3];
+		s = a;
+		assert(s.length == a.length);
+		assert(s[0] == a[0]);
+		assert(s[1] == a[1]);
+		assert(s[2] != a[2]); // fails
+	}
+}
+// ----
+// Warning 6328: (209-229): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/array_literal_6.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public pure {
+		uint[3] memory a = [uint(1), 2, 3];
+		uint[4] memory b = [uint(1), 2, 4, 3];
+		uint[4] memory c = b;
+		assert(a.length == c.length); // fails
+		assert(a[0] == c[0]);
+		assert(a[1] == c[1]);
+		assert(a[2] == c[2]); // fails
+		assert(a[2] == c[3]);
+	}
+}
+// ----
+// Warning 6328: (179-207): CHC: Assertion violation happens here.
+// Warning 6328: (268-288): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/types/array_literal_7.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] s;
+	function f() public {
+		uint[3] memory a = [uint(1), 2, 3];
+		uint[4] memory b = [uint(1), 2, 4, 3];
+		uint[4] memory c = b;
+		assert(c.length == b.length);
+		s = a;
+		assert(s.length == a.length);
+
+		assert(s.length == c.length); // fails
+		assert(s[0] == c[0]);
+		assert(s[1] == c[1]);
+		assert(s[2] == c[2]); // fails
+		assert(s[2] == c[3]);
+	}
+}
+// ----
+// Warning 6328: (259-287): CHC: Assertion violation happens here.
+// Warning 6328: (348-368): CHC: Assertion violation happens here.