Log all errors caught in the frontend at debug level

[mbovel]

While trying to debug my modifications to the frontend, I found that some exceptions are swallowed. This makes it very hard to debug the frontend.

I found that this is due to the way errors are handled in ThreadedFrontend.

cc @mario-bucev and @samuelchassot: this is the problem I had this afternoon.

Background

• b0338b2 made sure that catching an error in the frontend would call Callback.failed.
• bf38bae removed the intermediate catch that caught the errors thrown during the frontend onRun method.
• Callback.failed is now a no-op.

Current semantic and questions

• Frontend.onEnd runs even if exceptions are thrown during Frontend.onRun. Is that excepted? I guess this might be to allow Frontend.onEnd to recover from some errors?

• If an exception is thrown in Frontend.onEnd, it swallows any exception thrown in Frontend.onRun. Here is a minimal reproduction:

  @main def main(): Nothing =
    try
      throw new Exception("Forever lost in the void")
    finally
      throw new Exception("Thrown from finally")

  Is this expected? I think the first exception should at least be logged in debug mode. Should it also be rethrown?

• The first exception which is not UnsupportedCodeException thrown during Frontend.onEnd, or during Frontend.onRun is rethrown without being reported as an error, it is only logged at the debug level. Why are UnsupportedCodeExceptions handled differently?

• UnsupportedCodeException which are thrown before the first non-UnsupportedCodeException exception are reported as errors. The others are ignored. This seems weird. See def rethrow.

Proposed changes

This PR enables logging all exceptions thrown in the frontend, at debug level.

It doesn't make any other changes. In particular, the semantic described above is preserved.

Depending on the answers to my questions above, further changes might be needed.

[mario-bucev]

All the exceptions are caught in the exception handler added before the thread is started:

stainless/core/src/main/scala/stainless/frontend/ThreadedFrontend.scala

Lines 45 to 49 in 88e4de5

	thread.setUncaughtExceptionHandler(new Thread.UncaughtExceptionHandler() {
	override def uncaughtException(t: Thread, e: Throwable): Unit = {
	ThreadedFrontend.this.synchronized(exceptions += e)
	}
	})

These are then handled in a helper method rethrow, called in onStop and onJoin:

stainless/core/src/main/scala/stainless/frontend/ThreadedFrontend.scala

Lines 68 to 75 in 88e4de5

	private def rethrow(): Unit = for (ex <- exceptions) ex match {
	case UnsupportedCodeException(pos, msg) =>
	ctx.reporter.error(pos, msg)
	case _ =>
	ctx.reporter.debug(s"Rethrowing exception emitted from within the compiler: ${ex.getMessage}")
	exceptions.clear()
	throw ex
	}

If there is an exception other than UnsupportedCodeException (which is usually thrown for features Stainless does not support), all the remaining exceptions are swallowed (due to the exceptions.clear()), and that exception is rethrown.
I think we should do something similar to the UnsupportedCodeException (with ctx.reporter.error). That said, the other kind of exceptions are usually due to a bug e.g. ClassCastException.

[mario-bucev]

Regarding ThreadedFrontend.onEnd, this method in a no-op in the only concrete implementation of ThreadedFrontend (an anonymous class in DottyCompiler).

stainless/frontends/dotty/src/main/scala/stainless/frontends/dotc/DottyCompiler.scala

Lines 142 to 143 in 4f2e240

	override def apply(ctx: inox.Context, compilerArgs: Seq[String], callback: CallBack): Frontend =
	new ThreadedFrontend(callback, ctx) {

stainless/frontends/dotty/src/main/scala/stainless/frontends/dotc/DottyCompiler.scala

Line 175 in 4f2e240

override def onEnd(): Unit = ()

[vkuncak]

@mbovel can you rebase?