Better reporting (#1410)

build.sbt

@@ -275,7 +275,7 @@ val scriptSettings: Seq[Setting[_]] = Seq(
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 
 // lazy val inox = RootProject(file("../inox"))
-lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "41ffe806b04769c0d6757ebfeb17a96c7d5efd8a")
+lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "f72ef1a582969859d53b8ba03395d325308e7c03")
 lazy val cafebabe = ghProject("https://github.com/epfl-lara/cafebabe.git", "616e639b34379e12b8ac202849de3ebbbd0848bc")
 
 // Allow integration test to use facilities from regular tests

core/src/main/scala/stainless/Reporter.scala

@@ -11,41 +11,19 @@ abstract class ReportMessage {
 }
 
 class DefaultReporter(debugSections: Set[DebugSection]) extends inox.DefaultReporter(debugSections) {
-  var printingProgress = false
-
-  override def emit(msg: Message): Unit = synchronized {
-    if (printingProgress) {
-      println()
-      printingProgress = false
-    }
+  override def doEmit(msg: Message): Unit = {
     msg.msg match {
       case rm: ReportMessage if rm.sbtPluginOnly => ()
-      case _ => super.emit(msg)
+      case _ => super.doEmit(msg)
     }
   }
-
-  override def onCompilerProgress(current: Int, total: Int): Unit = synchronized {
-    printingProgress = true
-    print("\r" + severityToPrefix(INFO) + s" Verified: $current / $total")
-  }
 }
 
 class PlainTextReporter(debugSections: Set[DebugSection]) extends inox.PlainTextReporter(debugSections) {
-  var printingProgress = false
-
-  override def emit(msg: Message): Unit = synchronized {
-    if (printingProgress) {
-      println()
-      printingProgress = false
-    }
+  override def doEmit(msg: Message): Unit = {
     msg.msg match {
       case rm: ReportMessage if rm.sbtPluginOnly => ()
-      case _ => super.emit(msg)
+      case _ => super.doEmit(msg)
     }
   }
-
-  override def onCompilerProgress(current: Int, total: Int): Unit = synchronized {
-    printingProgress = true
-    print(s"\rVerified: $current / $total")
-  }
 }

core/src/main/scala/stainless/extraction/package.scala

@@ -121,6 +121,7 @@ package object extraction {
     object printer extends Printer { val trees: extraction.trees.type = extraction.trees }
   }
 
+  case class ExtractionFailed() extends Exception
   case class MalformedStainlessCode(tree: inox.ast.Trees#Tree, msg: String)
     extends Exception(msg)
 

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

@@ -3,13 +3,14 @@
 package stainless
 package frontend
 
-import stainless.extraction.xlang.{trees => xt, TreeSanitizer}
+import stainless.extraction.ExtractionFailed
+import stainless.extraction.xlang.{TreeSanitizer, trees as xt}
 import stainless.extraction.utils.DebugSymbols
 import stainless.utils.LibraryFilter
 
-import scala.util.{Try, Success, Failure}
+import scala.util.{Failure, Success, Try}
 import scala.concurrent.Await
-import scala.concurrent.duration._
+import scala.concurrent.duration.*
 
 class BatchedCallBack(components: Seq[Component])(using val context: inox.Context) extends CallBack with StainlessReports { self =>
   import context.reporter
@@ -67,7 +68,10 @@ class BatchedCallBack(components: Seq[Component])(using val context: inox.Contex
   def failed(): Unit = {}
 
   def endExtractions(): Unit = {
-    context.reporter.terminateIfError()
+    if (reporter.errorCount != 0) {
+      reporter.reset()
+      throw ExtractionFailed()
+    }
 
     val allSymbols = xt.NoSymbols
       .withClasses(currentClasses)

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

@@ -1,8 +1,12 @@
 package stainless
 package frontend
 
-import utils.StringUtils
-import extraction.xlang.{trees => xt}
+import utils.{StringUtils, XLangDependenciesFinder}
+import extraction.xlang.trees as xt
+import inox.utils.Position
+import stainless.ast.SymbolIdentifier
+import stainless.extraction.oo.{DefinitionTraverser, Trees}
+import stainless.utils.XLangDependenciesFinder.{DependencyInfo, IdentifierKind}
 
 object DebugSectionRecovery extends inox.DebugSection("recovery")
 
@@ -14,6 +18,7 @@ object DebugSectionRecovery extends inox.DebugSection("recovery")
 sealed abstract class RecoveryResult
 object RecoveryResult {
   final case class Success(symbols: xt.Symbols) extends RecoveryResult
+  // For each definition, the symbol we could not find as well as its occurrences
   final case class Failure(failures: Seq[(xt.Definition, Set[Identifier])]) extends RecoveryResult
 }
 
@@ -47,9 +52,9 @@ class Recovery(symbols: xt.Symbols)(using val context: inox.Context) {
         )
 
         strategy.recover(d, missings(d.id)) match {
-          case Left(errs) =>
+          case Left((d, missing)) =>
             reporter.debug(" => FAIL")
-            Left(errs)
+            Left((d, missing))
 
           case Right(result) =>
             reporter.debug(" => SUCCESS")
@@ -86,7 +91,7 @@ object Recovery {
       symbols.typeDefs.values
     ).toSeq
 
-    val missings = allDefs.toSeq.flatMap { defn =>
+    val missings = allDefs.flatMap { defn =>
       val missingDeps = findMissingDeps(defn, symbols)
       if (missingDeps.isEmpty) None
       else Some(defn.id -> missingDeps)
@@ -96,33 +101,92 @@ object Recovery {
       symbols
     } else {
       val recovery = new Recovery(symbols)
-      val recovered = recovery.recover(missings) match {
+      val recovered = recovery.recover(missings.view.mapValues(_.keySet).toMap) match {
         case RecoveryResult.Success(recovered) =>
           recovered
 
         case RecoveryResult.Failure(errors) =>
-          errors foreach { case (definition, unknowns) =>
-            ctx.reporter.error(
-              s"${definition.id.uniqueName} depends on missing dependencies: " +
-              s"${unknowns map (_.uniqueName) mkString ", "}."
-            )
-          }
+          reportMissingDependencies(errors, missings)
+          hintExternClasses(errors, missings)
           ctx.reporter.fatalError(s"Cannot recover from missing dependencies")
       }
 
       symbols ++ recovered
     }
   }
 
-  private def findMissingDeps(defn: xt.Definition, symbols: xt.Symbols): Set[Identifier] = {
-    val finder = new utils.XLangDependenciesFinder
+  private def findMissingDeps(defn: xt.Definition, symbols: xt.Symbols): Map[Identifier, DependencyInfo] = {
+    val finder = new XLangDependenciesFinder
     val deps = finder(defn)
-    deps.filter { dep =>
+    deps.filter { case (dep, _) =>
       !symbols.classes.contains(dep) &&
       !symbols.functions.contains(dep) &&
       !symbols.typeDefs.contains(dep)
     }
   }
+
+  private def reportMissingDependencies(errs: Seq[(xt.Definition, Set[Identifier])], missings: Map[Identifier, Map[Identifier, DependencyInfo]])(using ctx: inox.Context): Unit = {
+    for (((definition, unknowns), ix) <- errs.sortBy(_._1.id.fullName).zipWithIndex) {
+      val info = missings(definition.id)
+      assert(unknowns.subsetOf(info.keySet))
+      ctx.reporter.error(definition.getPos, s"${definition.id.name} depends on missing dependencies:")
+      val missingInfo = info.filter(p => unknowns(p._1)).toSeq.sortBy(_._1.fullName)
+      for ((unknId, info) <- missingInfo) {
+        reportMissingDependency(unknId, info)
+      }
+
+      if (ix < errs.size - 1) {
+        ctx.reporter.error("")
+      }
+    }
+  }
+
+  private def hintExternClasses(errs: Seq[(xt.Definition, Set[Identifier])], missings: Map[Identifier, Map[Identifier, DependencyInfo]])(using ctx: inox.Context): Unit = {
+    val missing = errs.flatMap(_._2).toSet
+    val someClass = missings.values.flatten.toSeq
+      .sortBy(_._1.fullName)
+      .find { case (id, info) => missing(id) && info.kind == IdentifierKind.Class }
+      .map(_._1)
+    someClass match {
+      case Some(cls) =>
+        ctx.reporter.error(
+          s"""
+            |Hint: to use a class reported as unknown, you may create a new class wrapping it in a field, annotated with @extern.
+            |For instance:
+            |    import stainless.annotation.extern
+            |    class ${cls.name}(@extern underlying: ${cls.fullName}) {
+            |      // ... methods
+            |    }
+            |See https://epfl-lara.github.io/stainless/wrap.html for more information.""".stripMargin)
+      case None =>
+    }
+  }
+
+  private def reportMissingDependency(id: Identifier, info: DependencyInfo)(using ctx: inox.Context): Unit = {
+    def cap(str: String): String = if (str.isEmpty) str else s"${str(0).toUpper}${str.drop(1)}"
+
+    val kindStr = info.kind match {
+      case IdentifierKind.Class => "class"
+      case IdentifierKind.TypeDef => "type definition"
+      case IdentifierKind.MethodOrFunction => "method"
+      case IdentifierKind.TypeSelection => "type selection"
+    }
+    val hint = {
+      id match {
+        case s: SymbolIdentifier =>
+          val orig = s.symbol.path.headOption.filter(hd => hd == "java" || hd == "scala").map(cap)
+          orig.map { orig =>
+            s"Hint: this $kindStr comes from the $orig standard library and is currently not supported."
+          }
+        case _ => None
+      }
+    }
+    ctx.reporter.error(s"${cap(kindStr)} ${id.name}")
+    hint.foreach(ctx.reporter.error)
+    for (pos <- info.positions) {
+      ctx.reporter.error(pos, "")
+    }
+  }
 }
 
 /** A strategy to recover a definition with missing dependencies */

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

@@ -4,21 +4,20 @@ package stainless
 package frontend
 
 import stainless.utils.LibraryFilter
-
-import extraction.xlang.{ TreeSanitizer, trees => xt }
+import extraction.xlang.{TreeSanitizer, trees as xt}
 import extraction.utils.ConcurrentCache
 import extraction.utils.DebugSymbols
-import utils.{ CheckFilter, JsonUtils }
-
-import scala.collection.mutable.{ ListBuffer, Set => MutableSet }
+import utils.{CheckFilter, JsonUtils}
 
-import io.circe._
-import io.circe.syntax._
+import scala.collection.mutable.{ListBuffer, Set as MutableSet}
+import io.circe.*
+import io.circe.syntax.*
+import stainless.extraction.ExtractionFailed
 
 import java.io.File
-import scala.util.{Try, Success, Failure}
-import scala.concurrent.{ Await, Future }
-import scala.concurrent.duration._
+import scala.util.{Failure, Success, Try}
+import scala.concurrent.{Await, Future}
+import scala.concurrent.duration.*
 
 
 class SplitCallBack(components: Seq[Component])(using override val context: inox.Context)
@@ -73,7 +72,10 @@ class SplitCallBack(components: Seq[Component])(using override val context: inox
   final override def failed(): Unit = ()
 
   final override def endExtractions(): Unit = {
-    reporter.terminateIfError()
+    if (reporter.errorCount != 0) {
+      reporter.reset()
+      throw ExtractionFailed()
+    }
 
     processSymbols(symbols)
 

core/src/main/scala/stainless/package.scala

@@ -121,6 +121,9 @@ package object stainless {
     val debugStack = ctx.reporter.debugSections.contains(frontend.DebugSectionStack)
     val isMalformedError =
       e match {
+        case extraction.ExtractionFailed() =>
+          // The errors have already been reported, nothing special to do
+          true
         case extraction.MalformedStainlessCode(tree, msg) =>
           ctx.reporter.error(tree.getPos, msg)
           true

core/src/main/scala/stainless/termination/MeasureInference.scala

@@ -23,6 +23,7 @@ class MeasureInference(override val s: Trees, override val t: Trees)(using overr
   type FunctionResult = (t.FunDef, Postconditions)
 
   given givenDebugSection: DebugSectionMeasureInference.type = DebugSectionMeasureInference
+  private case object MeasureInferenceTag
 
   // Measure inference depends on functions that are mutually recursive with `fd`,
   // so we include all dependencies in the key calculation
@@ -126,7 +127,7 @@ class MeasureInference(override val s: Trees, override val t: Trees)(using overr
 
       case None => try {
         val guarantee = timers.evaluators.termination.inference.run {
-          reporter.debug(s"  - Inferring measure for ${original.id.asString}...")
+          reporter.emit(reporter.ProgressMessage(reporter.INFO, MeasureInferenceTag, s"Inferring measure for ${original.id.asString}..."))
           pipeline.terminates(original)
         }
 
@@ -234,6 +235,8 @@ class MeasureInference(override val s: Trees, override val t: Trees)(using overr
       sortCache.cached(sort, context)(extractSort(context, sort))
     }.toSeq.unzip
 
+    reporter.emit(reporter.ProgressMessage(reporter.INFO, MeasureInferenceTag, s"Measure inference finished"))
+
     (t.NoSymbols.withSorts(sorts).withFunctions(functions ++ sizeFunctions), AllSummaries(fnsSummaries, sortSummaries))
   }
 }