Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Log all errors caught in the frontend at debug level
Browse files Browse the repository at this point in the history
mbovel committed Dec 10, 2024
1 parent b8b76f4 commit 4f2e240
Showing 1 changed file with 17 additions and 2 deletions.
19 changes: 17 additions & 2 deletions core/src/main/scala/stainless/frontend/ThreadedFrontend.scala
Original file line number Diff line number Diff line change
@@ -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()
@@ -45,6 +59,8 @@ abstract class ThreadedFrontend(callback: CallBack, ctx: inox.Context) extends F
thread.setUncaughtExceptionHandler(new Thread.UncaughtExceptionHandler() {
override def uncaughtException(t: Thread, e: Throwable): Unit = {
ThreadedFrontend.this.synchronized(exceptions += e)
ctx.reporter.debug("The following exception has been caught in the frontend end:")
ctx.reporter.debug(e)
}
})

@@ -69,9 +85,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
}
}

0 comments on commit 4f2e240

Please sign in to comment.