From 98446782e205499e3ebe9a90df80691fd92afdb1 Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@usi.ch>
Date: Tue, 23 Mar 2021 19:34:46 +0100
Subject: [PATCH] [SMTChecker] Fix compound assignment to push

---
 Changelog.md                                  |  1 +
 libsolidity/formal/SMTEncoder.cpp             | 35 ++++---------------
 .../push_as_lhs_compound_assignment.sol       | 15 ++++++++
 3 files changed, 22 insertions(+), 29 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_as_lhs_compound_assignment.sol

diff --git a/Changelog.md b/Changelog.md
index 4d13d673d..0a3747d98 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -8,6 +8,7 @@ Compiler Features:
 
 Bugfixes:
  * AST Output: Fix ``kind`` field of ``ModifierInvocation`` for base constructor calls.
+ * SMTChecker: Fix false positive and false negative on ``push`` as LHS of a compound assignment.
  * SMTChecker: Fix internal error on public getter returning dynamic data on older EVM versions where these are not available.
 
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 9f4a21497..cdfbad3ce 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -373,32 +373,10 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
 
 bool SMTEncoder::visit(Assignment const& _assignment)
 {
-	auto const& left = _assignment.leftHandSide();
-	auto const& right = _assignment.rightHandSide();
-
-	if (auto const* memberAccess = isEmptyPush(left))
-	{
-		right.accept(*this);
-		left.accept(*this);
-
-		auto const& memberExpr = memberAccess->expression();
-		auto& symbArray = dynamic_cast<smt::SymbolicArrayVariable&>(*m_context.expression(memberExpr));
-		smtutil::Expression oldElements = symbArray.elements();
-		smtutil::Expression length = symbArray.length();
-		symbArray.increaseIndex();
-		m_context.addAssertion(symbArray.elements() == smtutil::Expression::store(
-			oldElements,
-			length - 1,
-			expr(right)
-		));
-		m_context.addAssertion(symbArray.length() == length);
-
-		arrayPushPopAssign(memberExpr, symbArray.currentValue());
-		defineExpr(_assignment, expr(left));
-		return false;
-	}
-
-	return true;
+	// RHS must be visited before LHS; as opposed to what Assignment::accept does
+	_assignment.rightHandSide().accept(*this);
+	_assignment.leftHandSide().accept(*this);
+	return false;
 }
 
 void SMTEncoder::endVisit(Assignment const& _assignment)
@@ -408,9 +386,6 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
 	Token op = _assignment.assignmentOperator();
 	solAssert(TokenTraits::isAssignmentOp(op), "");
 
-	if (isEmptyPush(_assignment.leftHandSide()))
-		return;
-
 	if (!smt::isSupportedType(*_assignment.annotation().type))
 	{
 		// Give it a new index anyway to keep the SSA scheme sound.
@@ -2022,6 +1997,8 @@ void SMTEncoder::assignment(
 		dynamic_cast<MemberAccess const*>(left)
 	)
 		indexOrMemberAssignment(*left, _right);
+	else if (isEmptyPush(*left))
+		arrayPushPopAssign(*left, _right);
 	else
 		solAssert(false, "");
 }
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_compound_assignment.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_compound_assignment.sol
new file mode 100644
index 000000000..031bee0a5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_compound_assignment.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	int[] u;
+
+	function t() public {
+		require(u.length == 0);
+		u.push() -= 1;
+		assert(u[0] < 0); // should hold
+		assert(u[0] >= 0); // should fail
+	}
+}
+// ----
+// Warning 6328: (161-178): CHC: Assertion violation happens here.\nCounterexample:\nu = [(- 1)]\n\nTransaction trace:\nC.constructor()\nState: u = []\nC.t()