Assume that push will not overflow

docs/security-considerations.rst

@@ -657,3 +657,14 @@ Notice that we do not clear knowledge about ``array`` and ``d`` because they
 are located in storage, even though they also have type ``uint[]``.  However,
 if ``d`` was assigned, we would need to clear knowledge about ``array`` and
 vice-versa.
+
+Real World Assumptions
+======================
+
+Some scenarios are expressive in Solidity and the EVM, but are expected to
+never occur in practice.
+One of such cases is the length of a dynamic storage array overflowing after a
+push: If the ``push`` operation is applied to such array 2^256 times, its
+length silently overflows.
+However, this is unlikely to happen in practice, since the Earth, the sun and
+the universe might not be around anymore at the end of the 2^256 operations.

libsolidity/formal/SMTEncoder.cpp

@@ -1085,6 +1085,11 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall)
 	auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
 	solAssert(symbArray, "");
 	auto oldLength = symbArray->length();
+	m_context.addAssertion(oldLength >= 0);
+	// Real world assumption: the array length is assumed to not overflow.
+	// This assertion guarantees that both the current and updated lengths have the above property.
+	m_context.addAssertion(oldLength + 1 < (smt::maxValue(*TypeProvider::uint256()) - 1));
+
 	auto const& arguments = _funCall.arguments();
 	smt::Expression element = arguments.empty() ?
 		smt::zeroValue(_funCall.annotation().type) :
@@ -1096,12 +1101,7 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall)
 	);
 	symbArray->increaseIndex();
 	m_context.addAssertion(symbArray->elements() == store);
-	auto newLength = smt::Expression::ite(
+	m_context.addAssertion(symbArray->length() == oldLength + 1);
-		oldLength == smt::maxValue(*TypeProvider::uint256()),
-		0,
-		oldLength + 1
-	);
-	m_context.addAssertion(symbArray->length() == newLength);
 
 	if (arguments.empty())
 		defineExpr(_funCall, element);

test/libsolidity/smtCheckerTests/array_members/push.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f(uint x) public {
+		require(a.length < 100000);
+		a.push(x);
+		assert(a[a.length - 1] == x);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/push_2d.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] a;
+	function f(uint[] memory x, uint y) public {
+		require(a.length < 100000);
+		a.push(x);
+		assert(a[a.length - 1][0] == x[0]);
+		require(a[0].length < 100000);
+		a[0].push(y);
+		assert(a[0][a[0].length - 1] == y);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint256[] x;
+	constructor() public { x.push(42); }
+	function f() public {
+		x.push(23);
+		assert(x[0] == 42 || x[0] == 23);
+	}
+}

test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint256[] x;
+	constructor() public { x.push(42); }
+	function f() public {
+		x.push(23);
+		assert(x[0] == 42);
+	}
+}
+// ----

test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe.sol

@@ -0,0 +1,12 @@
+contract C {
+	uint256[] x;
+	function f(uint256 l) public {
+		require(x.length == 0);
+		x.push(42);
+		x.push(84);
+		for(uint256 i = 0; i < l; ++i)
+			x.push(23);
+		assert(x[0] == 42 || x[0] == 23);
+	}
+}
+

test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint256[] x;
+	function f(uint256 l) public {
+		require(x.length == 0);
+		x.push(42);
+		x.push(84);
+		for(uint256 i = 0; i < l; ++i)
+			x.push(23);
+		assert(x[0] == 42);
+	}
+}
+
+// ----