Make sure callbacks are sound wrt extraction failures

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

@@ -11,6 +11,7 @@ import extraction.xlang.{ trees => xt }
  * Frontends are required to follow this workflow (== one cycle):
  *  - when starting extracting compilation unit, [[beginExtractions]] should be called once;
  *  - the [[CallBack.apply]] method after extracting each compilation unit (i.e. a Scala file);
+ *  - the [[CallBack.failed]] method if the compilation unit extraction failed (or it contained errors);
  *  - finally, the frontend calls [[endExtractions]] to let the CallBack know all the data
  *    should be available by now.
  *
@@ -27,6 +28,7 @@ import extraction.xlang.{ trees => xt }
 trait CallBack {
   def beginExtractions(): Unit
   def apply(file: String, unit: xt.UnitDef, classes: Seq[xt.ClassDef], functions: Seq[xt.FunDef]): Unit
+  def failed(): Unit
   def endExtractions(): Unit
 
   def stop(): Unit // Blocking "stop".

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

@@ -44,6 +44,8 @@ trait CallBackWithRegistry extends CallBack with CheckFilter { self =>
     processSymbols(symss)
   }
 
+  final override def failed(): Unit = registry.failed()
+
   final override def endExtractions(): Unit = {
     val symss = registry.checkpoint()
     processSymbols(symss)

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

@@ -20,6 +20,10 @@ final class MasterCallBack(val callbacks: Seq[CallBack]) {
     callbacks foreach { c => c(file, unit, classes, functions) }
   }
 
+  def failed(): Unit = {
+    callbacks foreach { c => c.failed() }
+  }
+
   def endExtractions(): Unit = callbacks foreach { _.endExtractions() }
 
   def stop(): Unit = callbacks foreach { _.stop() }

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

@@ -14,7 +14,7 @@ abstract class ThreadedFrontend(callback: MasterCallBack, ctx: inox.Context) ext
   private implicit val debugSection = DebugSectionFrontend
 
   private var thread: Thread = _
-  private var exception: Throwable = _
+  private val exceptions = new scala.collection.mutable.ListBuffer[Throwable]
 
   protected def initRun(): Unit // Called when initializing the thread (before callback initialisation).
   protected def onRun(): Unit // Called when the thread is running (after callback initialisation).
@@ -31,7 +31,8 @@ abstract class ThreadedFrontend(callback: MasterCallBack, ctx: inox.Context) ext
         onRun()
       } catch {
         case e: Throwable =>
-          ctx.reporter.error(s"Exception thrown during compilation: ${e.getMessage}")
+          ctx.reporter.debug(s"Exception thrown during compilation: ${e.getMessage}")
+          callback.failed()
           throw e
       } finally {
         callback.endExtractions()
@@ -41,7 +42,9 @@ abstract class ThreadedFrontend(callback: MasterCallBack, ctx: inox.Context) ext
 
     thread = new Thread(runnable, "stainless frontend")
     thread.setUncaughtExceptionHandler(new Thread.UncaughtExceptionHandler() {
-      override def uncaughtException(t: Thread, e: Throwable): Unit = exception = e
+      override def uncaughtException(t: Thread, e: Throwable): Unit = {
+        ThreadedFrontend.this.synchronized(exceptions += e)
+      }
     })
 
     thread.start()
@@ -61,11 +64,13 @@ abstract class ThreadedFrontend(callback: MasterCallBack, ctx: inox.Context) ext
     rethrow()
   }
 
-  private def rethrow(): Unit = if (exception != null) {
-    val e = exception
-    exception = null
-    ctx.reporter.debug(s"Rethrowing exception emitted from within the compiler: ${e.getMessage}")
-    throw e
+  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
   }
 }
 

core/src/main/scala/stainless/utils/Registry.scala

@@ -81,11 +81,32 @@ trait Registry {
     } else updateImpl(classes, functions)
   }
 
+  private[this] var hasFailed: Boolean = false
+
+  /**
+   * Mark this compilation run as containing a failure.
+   *
+   * This is useful for open class hierarchies that cannot be soundly verified if
+   * some compilation unit contained a failure. This property won't show up in the
+   * dependency graph so we explicitly track such problematic states.
+   */
+  final def failed(): Unit = synchronized(hasFailed = true)
+
   /**
    * To be called once every compilation unit were extracted.
    */
   final def checkpoint(): Option[xt.Symbols] = synchronized {
-    if (hasPersistentCache) {
+    if (hasFailed) {
+      deferredClasses.clear()
+      deferredFunctions.clear()
+      deferredNodes.clear()
+      recentClasses.clear()
+      recentFunctions.clear()
+      knownOpenClasses.clear()
+      deferredMethods.clear()
+      hasFailed = false
+      None
+    } else if (hasPersistentCache) {
       val res = process(deferredClasses, deferredFunctions)
       persistentCache = None // remove the persistent cache after it's used once, the ICG can take over from here.
       deferredClasses.clear()