From b8913b1e9f8c8eca6851905f173188e789fc0354 Mon Sep 17 00:00:00 2001
From: Matt Bovel <matthieu@bovel.net>
Date: Tue, 10 Dec 2024 20:46:20 +0000
Subject: [PATCH] Log all errors caught in the frontend at debug level

---
 .../stainless/frontend/ThreadedFrontend.scala | 28 +++++++++++++++----
 1 file changed, 22 insertions(+), 6 deletions(-)

diff --git a/core/src/main/scala/stainless/frontend/ThreadedFrontend.scala b/core/src/main/scala/stainless/frontend/ThreadedFrontend.scala
index 9332affb7..875a9e8cd 100644
--- a/core/src/main/scala/stainless/frontend/ThreadedFrontend.scala
+++ b/core/src/main/scala/stainless/frontend/ThreadedFrontend.scala
@@ -32,6 +32,20 @@ abstract class ThreadedFrontend(callback: CallBack, ctx: inox.Context) extends F
           initRun()
           callback.beginExtractions()
           onRun()
+        } catch {
+          case e: Throwable => {
+            // `BatchedCallBack.endExtractions` and
+            // `SplitCallBack.endExtractions` only run if there are no errors
+            // reported. Not reporting errors here allow them to potentially
+            // recover from some errors.
+            //
+            // Matt: Do we really want that? From which errors can they actually
+            // recover? There might be non-recoverable exceptions benefiting
+            // from being reported here already or in handler below, either as
+            // errors or as warnings. See #1618 for more context.
+            ctx.reporter.debug("The following exception has been caught in the frontend init or run:")
+            ctx.reporter.debug(e)
+          }
         } finally {
           callback.endExtractions()
           onEnd()
@@ -43,10 +57,13 @@ abstract class ThreadedFrontend(callback: CallBack, ctx: inox.Context) extends F
 
     thread = new Thread(runnable, "stainless frontend")
     thread.setUncaughtExceptionHandler(new Thread.UncaughtExceptionHandler() {
-      override def uncaughtException(t: Thread, e: Throwable): Unit = {
-        ThreadedFrontend.this.synchronized(exceptions += e)
-      }
-    })
+      override def uncaughtException(t: Thread, e: Throwable): Unit =
+        this.synchronized {
+          exceptions += e
+        }
+        ctx.reporter.debug("The following exception has been caught in the frontend end:")
+        ctx.reporter.debug(e)
+  })
 
     thread.start()
   }
@@ -69,9 +86,8 @@ abstract class ThreadedFrontend(callback: CallBack, ctx: inox.Context) extends F
     case UnsupportedCodeException(pos, msg) =>
       ctx.reporter.error(pos, msg)
     case _ =>
-      ctx.reporter.debug(s"Rethrowing exception emitted from within the compiler: ${ex.getMessage}")
+      ctx.reporter.debug(s"Rethrowing the first exception caught in the frontend end: ${ex.getMessage}.")
       exceptions.clear()
       throw ex
   }
 }
-