Merge pull request #11854 from ethereum/smt_fix_push_lvalue

[SMTChecker] Fix false negative after `push` on storage references

Author: Leonardo

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.
 
 
 

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, "");
-
-			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());
+			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());
+			}
+			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

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.

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.