From 82db35e5639cba0ec0693c6d4e383287598b1c1c Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Tue, 12 May 2020 00:39:00 +0200
Subject: [PATCH 1/5] [SMTChecker] Support array push/pop

---
 Changelog.md                      |  1 +
 libsolidity/formal/SMTEncoder.cpp | 81 +++++++++++++++++++++++++++----
 libsolidity/formal/SMTEncoder.h   |  4 ++
 3 files changed, 76 insertions(+), 10 deletions(-)

diff --git a/Changelog.md b/Changelog.md
index cfd281893..0409261c2 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -6,6 +6,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``.
+ * SMTChecker: Support array ``push`` and ``pop``.
 
 
 Bugfixes:
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 09c188435..c90dbde6d 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -646,6 +646,12 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 		m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value));
 		break;
 	}
+	case FunctionType::Kind::ArrayPush:
+		arrayPush(_funCall);
+		break;
+	case FunctionType::Kind::ArrayPop:
+		arrayPop(_funCall);
+		break;
 	default:
 		m_errorReporter.warning(
 			4588_error,
@@ -905,16 +911,6 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 				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
@@ -1082,6 +1078,71 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 	}
 }
 
+void SMTEncoder::arrayPush(FunctionCall const& _funCall)
+{
+	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 const& arguments = _funCall.arguments();
+	smt::Expression element = arguments.empty() ?
+		smt::zeroValue(_funCall.annotation().type) :
+		expr(*arguments.front());
+	smt::Expression store = smt::Expression::store(
+		symbArray->elements(),
+		oldLength,
+		element
+	);
+	symbArray->increaseIndex();
+	m_context.addAssertion(symbArray->elements() == store);
+	auto newLength = smt::Expression::ite(
+		oldLength == smt::maxValue(*TypeProvider::uint256()),
+		0,
+		oldLength + 1
+	);
+	m_context.addAssertion(symbArray->length() == newLength);
+
+	if (arguments.empty())
+		defineExpr(_funCall, element);
+
+	arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
+}
+
+void SMTEncoder::arrayPop(FunctionCall const& _funCall)
+{
+	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 oldElements = symbArray->elements();
+	auto oldLength = symbArray->length();
+	symbArray->increaseIndex();
+	m_context.addAssertion(symbArray->elements() == oldElements);
+	auto newLength = smt::Expression::ite(
+		oldLength == 0,
+		smt::maxValue(*TypeProvider::uint256()),
+		oldLength - 1
+	);
+	m_context.addAssertion(symbArray->length() == newLength);
+
+	arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
+}
+
+void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array)
+{
+	if (auto const* id = dynamic_cast<Identifier const*>(&_expr))
+	{
+		auto varDecl = identifierToVariable(*id);
+		solAssert(varDecl, "");
+		m_context.addAssertion(m_context.newValue(*varDecl) == _array);
+	}
+	else if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(&_expr))
+		arrayIndexAssignment(*indexAccess, _array);
+	else
+		solAssert(false, "");
+}
+
 void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex)
 {
 	if (!m_context.knownGlobalSymbol(_name))
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 21bf094c0..871a3d8b5 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -137,6 +137,10 @@ protected:
 	/// Handles assignment to SMT array index.
 	void arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide);
 
+	void arrayPush(FunctionCall const& _funCall);
+	void arrayPop(FunctionCall const& _funCall);
+	void arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array);
+
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
 	smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);

From d4d26c02e4fec88cde45fbda70e3997494a48729 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Sun, 17 May 2020 20:20:17 +0200
Subject: [PATCH 2/5] Assume that push will not overflow

---
 docs/security-considerations.rst                  | 11 +++++++++++
 libsolidity/formal/SMTEncoder.cpp                 | 12 ++++++------
 .../smtCheckerTests/array_members/push.sol        | 10 ++++++++++
 .../smtCheckerTests/array_members/push_2d.sol     | 13 +++++++++++++
 .../array_members/push_overflow_1_safe.sol        | 10 ++++++++++
 ...ush_overflow_1_safe_no_overflow_assumption.sol | 11 +++++++++++
 .../array_members/push_overflow_2_safe.sol        | 12 ++++++++++++
 ...ush_overflow_2_safe_no_overflow_assumption.sol | 15 +++++++++++++++
 8 files changed, 88 insertions(+), 6 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_2d.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol

diff --git a/docs/security-considerations.rst b/docs/security-considerations.rst
index f899736aa..4ea39671d 100644
--- a/docs/security-considerations.rst
+++ b/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.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index c90dbde6d..e109b625e 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/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(
-		oldLength == smt::maxValue(*TypeProvider::uint256()),
-		0,
-		oldLength + 1
-	);
-	m_context.addAssertion(symbArray->length() == newLength);
+	m_context.addAssertion(symbArray->length() == oldLength + 1);
 
 	if (arguments.empty())
 		defineExpr(_funCall, element);
diff --git a/test/libsolidity/smtCheckerTests/array_members/push.sol b/test/libsolidity/smtCheckerTests/array_members/push.sol
new file mode 100644
index 000000000..f6623d361
--- /dev/null
+++ b/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);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_2d.sol b/test/libsolidity/smtCheckerTests/array_members/push_2d.sol
new file mode 100644
index 000000000..d09e847b7
--- /dev/null
+++ b/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);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol
new file mode 100644
index 000000000..f563504f4
--- /dev/null
+++ b/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);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol
new file mode 100644
index 000000000..2a2b6b91a
--- /dev/null
+++ b/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);
+	}
+}
+// ----
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe.sol
new file mode 100644
index 000000000..340f670d0
--- /dev/null
+++ b/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);
+	}
+}
+
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
new file mode 100644
index 000000000..70fcb8709
--- /dev/null
+++ b/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);
+	}
+}
+
+// ----

From 2435ab938c9e1b34ba7ded71f3df2173955d04e8 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Sun, 17 May 2020 23:21:08 +0200
Subject: [PATCH 3/5] Add verification target for empty pop

---
 libsolidity/formal/CHC.cpp                    | 98 +++++++++++++++++--
 libsolidity/formal/CHC.h                      |  7 +-
 libsolidity/formal/SMTEncoder.cpp             |  7 +-
 libsolidity/formal/SMTEncoder.h               |  5 +-
 .../array_members/pop_1_safe.sol              |  9 ++
 .../array_members/pop_1_unsafe.sol            | 10 ++
 .../array_members/pop_2d_safe.sol             | 10 ++
 .../array_members/pop_2d_unsafe.sol           | 10 ++
 .../array_members/pop_constructor_safe.sol    |  9 ++
 .../array_members/pop_constructor_unsafe.sol  |  8 ++
 .../array_members/pop_loop_safe.sol           | 11 +++
 .../array_members/pop_loop_unsafe.sol         | 12 +++
 .../{push_2d.sol => push_2d_arg_1_safe.sol}   |  3 -
 .../array_members/push_2d_arg_1_unsafe.sol    | 11 +++
 .../{push.sol => push_arg_1.sol}              |  1 -
 ...overflow_1_safe_no_overflow_assumption.sol |  1 -
 ...overflow_2_safe_no_overflow_assumption.sol |  2 -
 .../array_members/push_zero_2d_safe.sol       | 10 ++
 .../array_members/push_zero_2d_unsafe.sol     | 10 ++
 .../array_members/push_zero_safe.sol          |  9 ++
 .../array_members/push_zero_unsafe.sol        |  9 ++
 21 files changed, 232 insertions(+), 20 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/pop_1_safe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/pop_2d_safe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/pop_constructor_safe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol
 rename test/libsolidity/smtCheckerTests/array_members/{push_2d.sol => push_2d_arg_1_safe.sol} (63%)
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
 rename test/libsolidity/smtCheckerTests/array_members/{push.sol => push_arg_1.sol} (81%)
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_zero_2d_safe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_zero_safe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol

diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 1453df34f..f30959972 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -98,17 +98,45 @@ void CHC::analyze(SourceUnit const& _source)
 
 	for (auto const& [scope, target]: m_verificationTargets)
 	{
-		auto assertions = transactionAssertions(scope);
-		for (auto const* assertion: assertions)
+		if (target.type == VerificationTarget::Type::Assert)
 		{
+			auto assertions = transactionAssertions(scope);
+			for (auto const* assertion: assertions)
+			{
+				createErrorBlock();
+				connectBlocks(target.value, error(), target.constraints && (target.errorId == assertion->id()));
+				auto [result, model] = query(error(), assertion->location());
+				// This should be fine but it's a bug in the old compiler
+				(void)model;
+				if (result == smt::CheckResult::UNSATISFIABLE)
+					m_safeAssertions.insert(assertion);
+			}
+		}
+		else if (target.type == VerificationTarget::Type::PopEmptyArray)
+		{
+			solAssert(dynamic_cast<FunctionCall const*>(scope), "");
 			createErrorBlock();
-			connectBlocks(target.value, error(), target.constraints && (target.errorId == assertion->id()));
-			auto [result, model] = query(error(), assertion->location());
+			connectBlocks(target.value, error(), target.constraints && (target.errorId == scope->id()));
+			auto [result, model] = query(error(), scope->location());
 			// This should be fine but it's a bug in the old compiler
 			(void)model;
-			if (result == smt::CheckResult::UNSATISFIABLE)
-				m_safeAssertions.insert(assertion);
+			if (result != smt::CheckResult::UNSATISFIABLE)
+			{
+				string msg = "Empty array \"pop\" ";
+				if (result == smt::CheckResult::SATISFIABLE)
+					msg += "detected here.";
+				else
+					msg += "might happen here.";
+				m_unsafeTargets.insert(scope);
+				m_outerErrorReporter.warning(
+					2529_error,
+					scope->location(),
+					msg
+				);
+			}
 		}
+		else
+			solAssert(false, "");
 	}
 }
 
@@ -161,7 +189,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	auto stateExprs = vector<smt::Expression>{m_error.currentValue()} + currentStateVariables();
 	setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs);
 
-	addVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue());
+	addAssertVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue());
 	connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0);
 
 	SMTEncoder::endVisit(_contract);
@@ -256,7 +284,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
 
 			if (_function.isPublic())
 			{
-				addVerificationTarget(&_function, m_currentBlock, sum, assertionError);
+				addAssertVerificationTarget(&_function, m_currentBlock, sum, assertionError);
 				connectBlocks(m_currentBlock, iface, sum && (assertionError == 0));
 			}
 		}
@@ -556,10 +584,34 @@ void CHC::unknownFunctionCall(FunctionCall const&)
 	m_unknownFunctionCallSeen = true;
 }
 
+void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop)
+{
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_arrayPop.expression().annotation().type);
+	solAssert(funType.kind() == FunctionType::Kind::ArrayPop, "");
+
+	auto memberAccess = dynamic_cast<MemberAccess const*>(&_arrayPop.expression());
+	solAssert(memberAccess, "");
+	auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
+	solAssert(symbArray, "");
+
+	auto previousError = m_error.currentValue();
+	m_error.increaseIndex();
+
+	addArrayPopVerificationTarget(&_arrayPop, m_error.currentValue());
+	connectBlocks(
+		m_currentBlock,
+		m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction),
+		currentPathConditions() && symbArray->length() <= 0 && m_error.currentValue() == _arrayPop.id()
+	);
+
+	m_context.addAssertion(m_error.currentValue() == previousError);
+}
+
 void CHC::resetSourceAnalysis()
 {
 	m_verificationTargets.clear();
 	m_safeAssertions.clear();
+	m_unsafeTargets.clear();
 	m_functionAssertions.clear();
 	m_callGraph.clear();
 	m_summaries.clear();
@@ -974,9 +1026,35 @@ pair<smt::CheckResult, vector<string>> CHC::query(smt::Expression const& _query,
 	return {result, values};
 }
 
-void CHC::addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId)
+void CHC::addVerificationTarget(
+	ASTNode const* _scope,
+	VerificationTarget::Type _type,
+	smt::Expression _from,
+	smt::Expression _constraints,
+	smt::Expression _errorId
+)
 {
-	m_verificationTargets.emplace(_scope, CHCVerificationTarget{{VerificationTarget::Type::Assert, _from, _constraints}, _errorId});
+	m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
+}
+
+void CHC::addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId)
+{
+	addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId);
+}
+
+void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId)
+{
+	solAssert(m_currentContract, "");
+	solAssert(m_currentFunction, "");
+
+	if (m_currentFunction->isConstructor())
+		addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, summary(*m_currentContract), smt::Expression(true), _errorId);
+	else
+	{
+		auto iface = (*m_interfaces.at(m_currentContract))(initialStateVariables());
+		auto sum = summary(*m_currentFunction);
+		addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, iface, sum, _errorId);
+	}
 }
 
 string CHC::uniquePrefix()
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
index 7fc752451..87f902732 100644
--- a/libsolidity/formal/CHC.h
+++ b/libsolidity/formal/CHC.h
@@ -78,6 +78,7 @@ private:
 	void visitAssert(FunctionCall const& _funCall);
 	void internalFunctionCall(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);
+	void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
 	//@}
 
 	struct IdCompare
@@ -182,7 +183,9 @@ private:
 	/// @returns <false, model> otherwise.
 	std::pair<smt::CheckResult, std::vector<std::string>> query(smt::Expression const& _query, langutil::SourceLocation const& _location);
 
-	void addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
+	void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
+	void addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
+	void addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId);
 	//@}
 
 	/// Misc.
@@ -245,6 +248,8 @@ private:
 
 	/// Assertions proven safe.
 	std::set<Expression const*> m_safeAssertions;
+	/// Targets proven unsafe.
+	std::set<ASTNode const*> m_unsafeTargets;
 	//@}
 
 	/// Control-flow.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index e109b625e..44bec4d85 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1115,8 +1115,13 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
 	solAssert(memberAccess, "");
 	auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
 	solAssert(symbArray, "");
+
+	makeArrayPopVerificationTarget(_funCall);
+
 	auto oldElements = symbArray->elements();
 	auto oldLength = symbArray->length();
+	m_context.addAssertion(oldLength > 0);
+
 	symbArray->increaseIndex();
 	m_context.addAssertion(symbArray->elements() == oldElements);
 	auto newLength = smt::Expression::ite(
@@ -1124,7 +1129,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
 		smt::maxValue(*TypeProvider::uint256()),
 		oldLength - 1
 	);
-	m_context.addAssertion(symbArray->length() == newLength);
+	m_context.addAssertion(symbArray->length() == oldLength - 1);
 
 	arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
 }
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 871a3d8b5..f62f18558 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -140,6 +140,9 @@ protected:
 	void arrayPush(FunctionCall const& _funCall);
 	void arrayPop(FunctionCall const& _funCall);
 	void arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array);
+	/// Allows BMC and CHC to create verification targets for popping
+	/// an empty array.
+	virtual void makeArrayPopVerificationTarget(FunctionCall const&) {}
 
 	/// Division expression in the given type. Requires special treatment because
 	/// of rounding for signed division.
@@ -244,7 +247,7 @@ protected:
 
 	struct VerificationTarget
 	{
-		enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type;
+		enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray } type;
 		smt::Expression value;
 		smt::Expression constraints;
 	};
diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_1_safe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_1_safe.sol
new file mode 100644
index 000000000..34663d931
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_1_safe.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f() public {
+		a.push();
+		a.pop();
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol
new file mode 100644
index 000000000..e6f2273f8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f() public {
+		a.pop();
+	}
+}
+// ----
+// Warning: (82-89): Empty array "pop" detected here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_2d_safe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_2d_safe.sol
new file mode 100644
index 000000000..c67e91959
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_2d_safe.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] a;
+	function f() public {
+		a.push();
+		a[0].push();
+		a[0].pop();
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
new file mode 100644
index 000000000..1b7713089
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] a;
+	function f() public {
+		a.push();
+		a[0].push();
+		a[1].pop();
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_constructor_safe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_safe.sol
new file mode 100644
index 000000000..4842ee56f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_safe.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	constructor() public {
+		a.push();
+		a.pop();
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
new file mode 100644
index 000000000..f94bdcd68
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	constructor() public {
+		a.pop();
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol
new file mode 100644
index 000000000..25986da7b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f(uint l) public {
+		for (uint i = 0; i < l; ++i) {
+			a.push();
+			a.pop();
+		}
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol
new file mode 100644
index 000000000..2218c6665
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f(uint l) public {
+		for (uint i = 0; i < l; ++i) {
+			a.push();
+			a.pop();
+		}
+		a.pop();
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_2d.sol b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_safe.sol
similarity index 63%
rename from test/libsolidity/smtCheckerTests/array_members/push_2d.sol
rename to test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_safe.sol
index d09e847b7..34a1ae680 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_2d.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_safe.sol
@@ -3,10 +3,7 @@ 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);
 	}
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
new file mode 100644
index 000000000..23b8f6f00
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] a;
+	function f(uint[] memory x, uint y) public {
+		a.push(x);
+		a[0].push(y);
+		a[0].pop();
+		assert(a[0][a[0].length - 1] == y);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/push.sol b/test/libsolidity/smtCheckerTests/array_members/push_arg_1.sol
similarity index 81%
rename from test/libsolidity/smtCheckerTests/array_members/push.sol
rename to test/libsolidity/smtCheckerTests/array_members/push_arg_1.sol
index f6623d361..e36895554 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_arg_1.sol
@@ -3,7 +3,6 @@ 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);
 	}
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol
index 2a2b6b91a..7ed99a69e 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol
@@ -8,4 +8,3 @@ contract C {
 		assert(x[0] == 42);
 	}
 }
-// ----
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
index 70fcb8709..1f468f592 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
@@ -11,5 +11,3 @@ contract C {
 		assert(x[0] == 42);
 	}
 }
-
-// ----
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_safe.sol
new file mode 100644
index 000000000..45a56e677
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_safe.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] a;
+	function f() public {
+		a.push();
+		a[0].push();
+		assert(a[a.length - 1][0] == 0);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol
new file mode 100644
index 000000000..91fcd90b1
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] a;
+	function f() public {
+		a.push();
+		a[0].push();
+		assert(a[a.length - 1][0] == 100);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_safe.sol
new file mode 100644
index 000000000..e8054e361
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_safe.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f() public {
+		a.push();
+		assert(a[a.length - 1] == 0);
+	}
+}
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol
new file mode 100644
index 000000000..b99f42fa4
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol
@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f() public {
+		a.push();
+		assert(a[a.length - 1] == 100);
+	}
+}

From 1ab6ad79d8302557f83764ffca2e4d22990eb036 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 18 May 2020 16:33:27 +0200
Subject: [PATCH 4/5] Update test expectation

---
 .../array_members/pop_2d_unsafe.sol              |  2 ++
 .../array_members/pop_constructor_unsafe.sol     |  2 ++
 .../array_members/pop_loop_unsafe.sol            |  2 ++
 .../array_members/push_2d_arg_1_unsafe.sol       |  3 +++
 .../push_storage_ref_safe_aliasing.sol           | 16 ++++++++++++++++
 .../push_storage_ref_unsafe_aliasing.sol         | 15 +++++++++++++++
 .../array_members/push_zero_2d_unsafe.sol        |  2 ++
 .../array_members/push_zero_unsafe.sol           |  2 ++
 8 files changed, 44 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol

diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
index 1b7713089..1161ab92e 100644
--- a/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
@@ -8,3 +8,5 @@ contract C {
 		a[1].pop();
 	}
 }
+// ----
+// Warning: (111-121): Empty array "pop" detected here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
index f94bdcd68..a86d1a3f3 100644
--- a/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
@@ -6,3 +6,5 @@ contract C {
 		a.pop();
 	}
 }
+// ----
+// Warning: (83-90): Empty array "pop" detected here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol
index 2218c6665..5d4241984 100644
--- a/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol
@@ -10,3 +10,5 @@ contract C {
 		a.pop();
 	}
 }
+// ----
+// Warning: (150-157): Empty array "pop" detected here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
index 23b8f6f00..d5bd19bb1 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
@@ -9,3 +9,6 @@ contract C {
 		assert(a[0][a[0].length - 1] == y);
 	}
 }
+// ----
+// Warning: (162-177): Underflow (resulting value less than 0) happens here
+// Warning: (150-184): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol
new file mode 100644
index 000000000..8ad5cdcad
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol
@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] a;
+	function f() public {
+		a.push();
+		uint[] storage b = a[0];
+		b.push(8);
+		assert(b[b.length - 1] == 8);
+		// Safe but fails due to aliasing.
+		assert(a[0][a[0].length - 1] == 8);
+	}
+}
+// ----
+// Warning: (217-232): Underflow (resulting value less than 0) happens here
+// Warning: (205-239): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
new file mode 100644
index 000000000..f54fc8d83
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] a;
+	function f() public {
+		a.push();
+		a[0].push();
+		a[0][0] = 16;
+		uint[] storage b = a[0];
+		b[0] = 32;
+		assert(a[0][0] == 16);
+	}
+}
+// ----
+// Warning: (167-188): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol
index 91fcd90b1..9b9516ccd 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol
@@ -8,3 +8,5 @@ contract C {
 		assert(a[a.length - 1][0] == 100);
 	}
 }
+// ----
+// Warning: (111-144): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol
index b99f42fa4..966b4e1bd 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol
@@ -7,3 +7,5 @@ contract C {
 		assert(a[a.length - 1] == 100);
 	}
 }
+// ----
+// Warning: (94-124): Assertion violation happens here

From 5d6dd6876601003017dcba497d0202b2486d1eda Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 18 May 2020 17:09:46 +0200
Subject: [PATCH 5/5] Update docs

---
 docs/security-considerations.rst | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/docs/security-considerations.rst b/docs/security-considerations.rst
index 4ea39671d..772fa7c1d 100644
--- a/docs/security-considerations.rst
+++ b/docs/security-considerations.rst
@@ -661,10 +661,10 @@ vice-versa.
 Real World Assumptions
 ======================
 
-Some scenarios are expressive in Solidity and the EVM, but are expected to
+Some scenarios can be expressed 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
+One of such cases is the length of a dynamic storage array overflowing during a
+push: If the ``push`` operation is applied to an array of length 2^256 - 1, 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.
+However, this is unlikely to happen in practice, since the operations required
+to grow the array to that point would take billions of years to execute.