From 16bc15acac60fc433dddea6d189c477ad8915722 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Fri, 27 Aug 2021 18:53:15 +0200
Subject: [PATCH] Fix false negative on storage array references returned by
 internal functions

---
 Changelog.md                                  |  1 +
 libsolidity/formal/SMTEncoder.cpp             | 42 +++++++++++--------
 .../push_function_return_value.sol            | 20 +++++++++
 .../array_members/storage_pointer_push_1.sol  |  1 +
 4 files changed, 46 insertions(+), 18 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/array_members/push_function_return_value.sol

diff --git a/Changelog.md b/Changelog.md
index 8e5da286d..1482e4034 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -13,6 +13,7 @@ Compiler Features:
 Bugfixes:
  * SMTChecker: Fix false positive in external calls from constructors.
  * SMTChecker: Fix internal error on some multi-source uses of ``abi.*``, cryptographic functions and constants.
+ * SMTChecker: Fix false negative caused by ``push`` on storage array references returned by internal functions.
 
 
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index ef2316bd0..6ecb57a7f 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1977,26 +1977,32 @@ void SMTEncoder::assignment(
 		indexOrMemberAssignment(*left, _right);
 	else if (auto const* funCall = dynamic_cast<FunctionCall const*>(left))
 	{
-		if (
-			auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type);
-			funType && funType->kind() == FunctionType::Kind::ArrayPush
-		)
+		if (auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type))
 		{
-			auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
-			solAssert(memberAccess, "");
-			auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(memberAccess->expression()));
-			solAssert(symbArray, "");
+			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,
-				_right
-			);
-			symbArray->increaseIndex();
-			m_context.addAssertion(symbArray->elements() == store);
-			m_context.addAssertion(symbArray->length() == oldLength);
-			assignment(memberAccess->expression(), symbArray->currentValue());
+				auto oldLength = symbArray->length();
+				auto store = smtutil::Expression::store(
+					symbArray->elements(),
+					symbArray->length() - 1,
+					_right
+				);
+				symbArray->increaseIndex();
+				m_context.addAssertion(symbArray->elements() == store);
+				m_context.addAssertion(symbArray->length() == oldLength);
+				assignment(memberAccess->expression(), symbArray->currentValue());
+			}
+			else if (funType->kind() == FunctionType::Kind::Internal)
+			{
+				for (auto type: funType->returnParameterTypes())
+					if (type->category() == Type::Category::Mapping || dynamic_cast<ReferenceType const*>(type))
+						resetReferences(type);
+			}
 		}
 	}
 	else
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_function_return_value.sol b/test/libsolidity/smtCheckerTests/array_members/push_function_return_value.sol
new file mode 100644
index 000000000..ae897ce13
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/array_members/push_function_return_value.sol
@@ -0,0 +1,20 @@
+contract C {
+	bytes x;
+
+	function getX() internal view returns (bytes storage) {
+		return x;
+	}
+
+	function s() public {
+		require(x.length == 0);
+		getX().push("a");
+		assert(x.length == 1); // should hold but knowledge is erased due to pushing a reference
+		assert(x.length == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (168-189): CHC: Assertion violation happens here.
+// Warning 6328: (259-280): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol b/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol
index 55a03254d..bbbc3a68f 100644
--- a/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1.sol
@@ -17,4 +17,5 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 6368: (159-169): CHC: Out of bounds access happens here.
 // Warning 6328: (152-181): CHC: Assertion violation happens here.