Fix tests and error reporting improvements

Author: jad-hamza

.gitignore

@@ -38,6 +38,7 @@ pri-sessions/
 stainless.out/
 repairs.dat
 tmp
+stainless-debug.txt
 
 #eclipse
 .cache

core/src/main/scala/stainless/MainHelpers.scala

@@ -181,7 +181,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
       } catch {
         case e: Throwable =>
           reporter.debug(e)(frontend.DebugSectionFrontend)
-          reporter.error(e.getMessage)
+          reporter.error("There was an error during the watch cycle")
           compiler = newCompiler()
       }
 

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

@@ -94,16 +94,8 @@ class BatchedCallBack(components: Seq[Component])(implicit val context: inox.Con
 
     val reports = runs map { run =>
       val ids = symbols.functions.keys.toSeq
-      val analysis = Try(Await.result(run(ids, symbols, filterSymbols = true), Duration.Inf))
-
-      analysis match {
-        case Success(analysis) =>
-          RunReport(run)(analysis.toReport)
-
-        case Failure(err) =>
-          val msg = s"Run has failed with error: $err\n\n" + err.getStackTrace.map(_.toString).mkString("\n")
-          reporter.fatalError(msg)
-      }
+      val analysis = Await.result(run(ids, symbols, filterSymbols = true), Duration.Inf)
+      RunReport(run)(analysis.toReport)
     }
 
     report = Report(reports)

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

@@ -176,18 +176,8 @@ class SplitCallBack(components: Seq[Component])(override implicit val context: i
     // Dispatch a task to the executor service instead of blocking this thread.
     val componentReports: Seq[Future[RunReport]] = {
       runs map { run =>
-        Try(run(id, syms)) match {
-          case Success(future) =>
-            val runReport = future map { a =>
-              RunReport(run)(a.toReport): RunReport
-            }
-            runReport
-
-          case Failure(err) =>
-            val msg = s"Run has failed with error: $err\n\n" +
-                      err.getStackTrace.map(_.toString).mkString("\n")
-
-            reporter.fatalError(msg)
+        run(id, syms) map { a =>
+          RunReport(run)(a.toReport): RunReport
         }
       }
     }

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

@@ -108,8 +108,8 @@ package object stainless {
     }
   }
 
-  def topLevelErrorHandler[T](e: Throwable)(implicit ctx: inox.Context): T = {
-    ctx.reporter.error("Stainless terminated with an error.")
+  def topLevelErrorHandler(e: Throwable)(implicit ctx: inox.Context): Nothing = {
+    ctx.reporter.error(s"Stainless terminated with an error.")
 
     val sw = new StringWriter
     e.printStackTrace(new PrintWriter(sw))
@@ -119,6 +119,8 @@ package object stainless {
 
     if (ctx.options.findOptionOrDefault(frontend.optPrintStackTrace))
       ctx.reporter.error(sw.toString)
+    else
+      ctx.reporter.error("You may use the option --print-trace to have the stack trace displayed in the output.")
 
     System.exit(2)
     ??? // unreachable

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

@@ -9,15 +9,20 @@ trait MeasureInference
   extends extraction.CachingPhase
     with extraction.SimplyCachedSorts
     with extraction.IdentitySorts
-    with extraction.SimpleFunctions
-    with extraction.SimplyCachedFunctions { self =>
+    with extraction.SimpleFunctions { self =>
 
   val s: Trees
   val t: Trees
   import s._
 
   import context.{options, timers, reporter}
 
+  // Measure inference depends on functions that are mutually recursive with `fd`,
+  // so we include all dependencies in the key calculation
+  override protected final val funCache = new ExtractionCache[s.FunDef, FunctionResult]((fd, context) =>
+    getDependencyKey(fd.id)(context.symbols)
+  )
+
   val sizes: SizeFunctions { val trees: s.type } = new {
     val trees: s.type = self.s
   } with SizeFunctions
@@ -54,14 +59,26 @@ trait MeasureInference
       }
     }
 
-    def needsMeasure(fd: FunDef): Boolean = symbols.isRecursive(fd.id) &&
-      fd.measure(symbols).isEmpty &&
-      symbols.dependencies(fd.id).forall(id =>
-        symbols.lookupFunction(id).forall(fd2 =>
-          !symbols.dependencies(fd2.id).contains(fd.id) ||
-          fd2.measure(symbols).isEmpty
-        )
-      )
+    def needsMeasure(fd: FunDef): Boolean = {
+      if (symbols.isRecursive(fd.id) && fd.measure(symbols).isEmpty) {
+        symbols.dependencies(fd.id).find(id =>
+          symbols.lookupFunction(id).exists(fd2 =>
+            symbols.dependencies(fd2.id).contains(fd.id) &&
+            !fd2.measure(symbols).isEmpty
+          )
+        ) match {
+          case None =>
+            true
+          case Some(id) =>
+            reporter.fatalError(fd.getPos,
+              s"""Function ${fd.id} has no measure annotated, but mutually recursive function ${id} has one.
+                 |Please annotated both with a measure, or none for measure inference.""".stripMargin
+            )
+        }
+      } else {
+        false
+      }
+    }
 
     def inferMeasure(original: FunDef): FunDef = measureCache.get(original) match {
       case Some(measure) =>