[SMTChecker] Fix soundness of array pop

Changelog.md

@@ -20,6 +20,7 @@ Bugfixes:
  * SMTChecker: Fix internal error in BMC function inlining.
  * SMTChecker: Fix internal error on array implicit conversion.
  * SMTChecker: Fix internal error on fixed bytes index access.
+ * SMTChecker: Fix soundness of array ``pop``.
  * References Resolver: Fix internal bug when using constructor for library.
  * Yul Optimizer: Make function inlining order more resilient to whether or not unrelated source files are present.
  * Type Checker: Disallow signed literals as exponent in exponentiation operator.

libsolidity/formal/SMTEncoder.cpp

@@ -1111,11 +1111,11 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
 	symbArray->increaseIndex();
 	m_context.addAssertion(symbArray->elements() == oldElements);
 	auto newLength = smtutil::Expression::ite(
-		oldLength == 0,
-		smt::maxValue(*TypeProvider::uint256()),
-		oldLength - 1
+		oldLength > 0,
+		oldLength - 1,
+		0
 	);
-	m_context.addAssertion(symbArray->length() == oldLength - 1);
+	m_context.addAssertion(symbArray->length() == newLength);
 
 	arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
 }

test/libsolidity/smtCheckerTests/array_members/array_pop_length_1.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f() public {
+		a.pop();
+		a.push();
+	}
+}
+// ----
+// Warning 2529: (82-89): Empty array "pop" detected here

test/libsolidity/smtCheckerTests/array_members/array_pop_length_2.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f() public {
+		a.pop();
+		a.length;
+	}
+}
+// ----
+// Warning 2529: (82-89): Empty array "pop" detected here

test/libsolidity/smtCheckerTests/array_members/array_pop_length_3.sol

@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f() public {
+		a.pop();
+		a.pop();
+	}
+}
+// ----
+// Warning 2529: (82-89): Empty array "pop" detected here
+// Warning 2529: (93-100): Empty array "pop" detected here

test/libsolidity/smtCheckerTests/array_members/array_pop_length_4.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f() public {
+		a.length;
+		a.pop();
+	}
+}
+// ----
+// Warning 2529: (94-101): Empty array "pop" detected here

test/libsolidity/smtCheckerTests/array_members/array_pop_length_5.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function g() internal {
+		a.push();
+	}
+	function f() public {
+		a.pop();
+		g();
+	}
+}
+// ----
+// Warning 2529: (122-129): Empty array "pop" detected here

test/libsolidity/smtCheckerTests/array_members/array_pop_length_6.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function g() internal view {
+		a.length;
+	}
+	function f() public {
+		a.pop();
+		g();
+	}
+}
+// ----
+// Warning 2529: (127-134): Empty array "pop" detected here

test/libsolidity/smtCheckerTests/array_members/array_pop_length_7.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f() public {
+		a.push();
+		a.pop();
+	}
+}

test/libsolidity/smtCheckerTests/array_members/array_pop_length_8.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] a;
+	function f() public {
+		a.pop();
+		a.push();
+		a.push();
+		a.push();
+		a.pop();
+		a.pop();
+		a.pop();
+	}
+}
+// ----
+// Warning 2529: (82-89): Empty array "pop" detected here

test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol

@@ -9,4 +9,4 @@ contract C {
 	}
 }
 // ----
-// Warning 2529: (111-121): Empty array "pop" detected here.
+// Warning 2529: (111-121): Empty array "pop" detected here