Merge pull request #9451 from ethereum/smt_fix_push_push

[SMTChecker] Fix push().push()

Changelog.md

@@ -13,6 +13,7 @@ Bugfixes:
  * SMTChecker: Fix internal error when using bitwise operators on fixed bytes type.
  * SMTChecker: Fix internal error when using compound bitwise operator assignments on array indices inside branches.
  * SMTChecker: Fix error in events with indices of type static array.
+ * SMTChecker: Fix internal error in sequential storage array pushes (``push().push()`).
  * Type Checker: Fix overload resolution in combination with ``{value: ...}``.
  * Type Checker: Fix internal compiler error related to oversized types.
  * Code Generator: Avoid double cleanup when copying to memory.

libsolidity/formal/SMTEncoder.cpp

@@ -1077,7 +1077,7 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall)
 	m_context.addAssertion(symbArray->length() == oldLength + 1);
 
 	if (arguments.empty())
-		defineExpr(_funCall, element);
+		defineExpr(_funCall, smtutil::Expression::select(symbArray->elements(), oldLength));
 
 	arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
 }
@@ -1119,6 +1119,28 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
 	}
 	else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(&_expr))
 		arrayIndexAssignment(*indexAccess, _array);
+	else if (auto const* funCall = dynamic_cast<FunctionCall const*>(&_expr))
+	{
+		FunctionType const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
+		if (funType.kind() == FunctionType::Kind::ArrayPush)
+		{
+			auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
+			solAssert(memberAccess, "");
+			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
+			solAssert(symbArray, "");
+
+			auto oldLength = symbArray->length();
+			auto store = smtutil::Expression::store(
+				symbArray->elements(),
+				symbArray->length() - 1,
+				_array
+			);
+			symbArray->increaseIndex();
+			m_context.addAssertion(symbArray->elements() == store);
+			m_context.addAssertion(symbArray->length() == oldLength);
+			arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
+		}
+	}
 	else if (dynamic_cast<MemberAccess const*>(&_expr))
 		m_errorReporter.warning(
 			9599_error,

test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract C {
+	int[][] array2d;
+	function l() public {
+		array2d.push().push();
+		assert(array2d.length > 0);
+		assert(array2d[array2d.length - 1].length > 0);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1_fail.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+	int[][] array2d;
+	function l() public {
+		array2d.push().push();
+		assert(array2d.length > 2);
+		assert(array2d[array2d.length - 1].length > 3);
+	}
+}
+// ----
+// Warning 4661: (113-139): Assertion violation happens here
+// Warning 4661: (143-189): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract C {
+	int[][][] array2d;
+	function l() public {
+		array2d.push().push().push();
+		assert(array2d.length > 0);
+		uint last = array2d[array2d.length - 1].length;
+		assert(last > 0);
+		assert(array2d[array2d.length - 1][last - 1].length > 0);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C {
+	int[][][] array2d;
+	function l() public {
+		array2d.push().push().push();
+		assert(array2d.length > 2);
+		uint last = array2d[array2d.length - 1].length;
+		assert(last > 3);
+		assert(array2d[array2d.length - 1][last - 1].length > 4);
+	}
+}
+// ----
+// Warning 4661: (122-148): Assertion violation happens here
+// Warning 4661: (202-218): Assertion violation happens here
+// Warning 4661: (222-278): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+contract C {
+	int[][] array2d;
+	function l() public {
+		s().push();
+		// False positive.
+		// Knowledge is erased because `s()` is a storage pointer.
+		assert(array2d[2].length > 0);
+	}
+	function s() internal returns (int[] storage) {
+		array2d.push();
+		array2d.push();
+		array2d.push();
+		return array2d[2];
+	}
+}
+// ----
+// Warning 4661: (184-213): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1_safe.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C {
+	int[][] array2d;
+	function l() public {
+		s();
+		array2d[2].push();
+		assert(array2d[2].length > 0);
+	}
+	function s() internal returns (int[] storage) {
+		array2d.push();
+		array2d.push();
+		array2d.push();
+		return array2d[2];
+	}
+}