From 5daa97f41711fef9d3886f40284c446e2e60fb93 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Sun, 3 Apr 2022 17:23:05 +0200
Subject: [PATCH] fixup external low calls

---
 libsolidity/formal/CHC.cpp | 34 +++++++++++++++++++++++-----------
 1 file changed, 23 insertions(+), 11 deletions(-)

diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 3b226d4f7..d6b318520 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -896,17 +896,8 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	/// so we just add the nondet_interface predicate.
 
 	solAssert(m_currentContract, "");
+
 	auto [callExpr, callOptions] = functionCallExpression(_funCall);
-
-	if (
-		encodeExternalCallsAsTrusted() ||
-		isExternalCallToThis(callExpr)
-	)
-	{
-		externalFunctionCallToTrustedCode(_funCall);
-		return;
-	}
-
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
 
 	auto kind = funType.kind();
@@ -917,12 +908,33 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 		""
 	);
 
-	solAssert(m_currentContract, "");
+
+	// Only consider high level external calls in trusted mode.
+	if (
+		kind == FunctionType::Kind::External &&
+		(encodeExternalCallsAsTrusted() || isExternalCallToThis(callExpr))
+	)
+	{
+		externalFunctionCallToTrustedCode(_funCall);
+		return;
+	}
+
+	// Low level calls are still encoded nondeterministically.
+
 	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
 	if (function)
 		for (auto var: function->returnParameters())
 			m_context.variable(*var)->increaseIndex();
 
+	// If we see a low level call in trusted mode,
+	// we need to havoc the global state.
+	if (
+		kind == FunctionType::Kind::BareCall &&
+		encodeExternalCallsAsTrusted()
+	)
+		state().newStorage();
+
+	// No reentrancy from constructor calls.
 	if (!m_currentFunction || m_currentFunction->isConstructor())
 		return;