Add warnings for explicit choose and old VC gen

core/src/main/scala/stainless/Component.scala

@@ -3,8 +3,9 @@
 package stainless
 
 import utils.{CheckFilter, DefinitionIdFinder, DependenciesFinder}
-import extraction.xlang.{trees => xt}
-import io.circe._
+import extraction.xlang.trees as xt
+import io.circe.*
+import stainless.extraction.ExtractionSummary
 
 import scala.concurrent.Future
 
@@ -91,24 +92,24 @@ trait ComponentRun { self =>
   private[this] final val extractionFilter = createFilter
 
   /** Sends the symbols through the extraction pipeline. */
-  def extract(symbols: xt.Symbols): trees.Symbols = extractionPipeline extract symbols
+  def extract(symbols: xt.Symbols): (trees.Symbols, ExtractionSummary) = extractionPipeline extract symbols
 
   /** Sends the program's symbols through the extraction pipeline. */
   def extract(program: inox.Program { val trees: xt.type }): inox.Program {
     val trees: self.trees.type
-  } = inox.Program(trees)(extract(program.symbols))
+  } = inox.Program(trees)(extract(program.symbols)._1)
 
   /** Passes the provided symbols through the extraction pipeline and compute all
     * functions to process that are derived from the provided identifiers. */
   def apply(ids: Seq[Identifier], symbols: xt.Symbols): Future[Analysis] = {
-    val exSymbols = extract(symbols)
+    val (exSymbols, exSummary) = extract(symbols)
     val toProcess = extractionFilter.filter(ids, exSymbols, component)
-    execute(toProcess, exSymbols)
+    execute(toProcess, exSymbols, exSummary)
   }
 
   def apply(id: Identifier, symbols: xt.Symbols): Future[Analysis] =
     apply(Seq(id), symbols)
 
-  private[stainless] def execute(functions: Seq[Identifier], symbols: trees.Symbols): Future[Analysis]
+  private[stainless] def execute(functions: Seq[Identifier], symbols: trees.Symbols, exSummary: ExtractionSummary): Future[Analysis]
 }
 

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

@@ -70,6 +70,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
     genc.optIncludes -> Description(General, "Add includes in GenC output"),
     optWatch -> Description(General, "Re-run stainless upon file changes"),
     optCompact -> Description(General, "Print only invalid elements of summaries"),
+    optExtendedSummary -> Description(General, "Print an extended summary of all Stainless phases"),
     frontend.optBatchedProgram -> Description(General, "Process the whole program together, skip dependency analysis"),
     frontend.optKeep -> Description(General, "Keep library objects marked by @keepFor(g) for some g in g1,g2,... (implies --batched)"),
     frontend.optExtraDeps -> Description(General, "Fetch the specified extra source dependencies and add their source files to the session"),

core/src/main/scala/stainless/Report.scala

@@ -3,11 +3,10 @@
 package stainless
 
 import inox.utils.Position
-import inox.utils.ASCIIHelpers._
-
-import io.circe._
-import io.circe.syntax._
-
+import inox.utils.ASCIIHelpers.*
+import io.circe.*
+import io.circe.syntax.*
+import stainless.extraction._
 import stainless.utils.JsonConvertions.given
 
 case class ReportStats(total: Int, time: Long, valid: Int, validFromCache: Int, invalid: Int, unknown: Int) {
@@ -58,6 +57,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
     val table = emitTable(!compact)(using ctx)
     val asciiOnly = ctx.options.findOptionOrDefault(inox.optNoColors)
     ctx.reporter.info(table.render(asciiOnly))
+    ctx.reporter.info(emitSummary(ctx))
   }
 
   /** Create a new report with *only* the information about the given functions/classes/... */
@@ -71,6 +71,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
   protected type Level = Level.Type
 
   protected[stainless] def annotatedRows: Seq[RecordRow]
+  protected[stainless] def extractionSummary: ExtractionSummary
 
   /** Filter, sort & process rows. */
   private def processRows(full: Boolean)(using ctx: inox.Context): Seq[Row] = {
@@ -86,9 +87,9 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
   private def withColor(str: String, level: Level)(using inox.Context): String =
     withColor(str, colorOf(level))
 
-  private def withColor(str: String, color: String)(using ctx: inox.Context): String =
+  private def withColor(str: String, color: String, style: String = "")(using ctx: inox.Context): String =
     if (ctx.options.findOptionOrDefault(inox.optNoColors)) str
-    else s"$color$str${Console.RESET}"
+    else s"$style$color$str${Console.RESET}"
 
   private def colorOf(level: Level): String = level match {
     case Level.Normal  => Console.GREEN
@@ -132,6 +133,150 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType =>
 
     t
   }
+
+  private def emitSummary(ctx: inox.Context): String = {
+    given inox.Context = ctx
+    def join(strs: Seq[String], prefix: String = "", sep: String = ", ", charsPerLine: Int = 80): String = {
+      def loop(strs: Seq[String], currLine: String, prevLines: String): String = {
+        def flushedCurrLine: String = {
+          if (prevLines.isEmpty) prefix ++ currLine
+          else if (currLine.isEmpty) prevLines
+          else {
+            val sep2 = if (prevLines.endsWith("\n" ++ prefix)) "" else sep
+            prevLines ++ sep2 ++ currLine
+          }
+        }
+
+        strs match {
+          case Seq() => flushedCurrLine
+          case str +: rest =>
+            val newLine = prefix.length + currLine.length + str.length >= charsPerLine &&
+              prefix.length + str.length <= charsPerLine // To guard against strings that are over charsPerLine long
+
+            if (newLine) {
+              val newPrevLines = flushedCurrLine ++ sep ++ "\n" ++ prefix
+              loop(rest, str, newPrevLines)
+            } else {
+              val newCurrLine = if (currLine.isEmpty) str else currLine ++ sep ++ str
+              loop(rest, newCurrLine, prevLines)
+            }
+        }
+      }
+      loop(strs, "", "")
+    }
+    def withMultilineColor(str: String, color: String, style: String = ""): String = {
+      if (ctx.options.findOptionOrDefault(inox.optNoColors)) str // To not unnecessarily process a string that would result in itself anyway...
+      else str.split("\n").map(withColor(_, color, style)).mkString("\n")
+    }
+
+    val sd = prepareExtractionSummaryData
+    val admitted = ctx.options.findOptionOrDefault(verification.optAdmitVCs)
+    val termOff = ctx.options.findOptionOrDefault(stainless.termination.optCheckMeasures).isNo
+    val oldVC = !ctx.options.findOptionOrDefault(verification.optTypeChecker)
+    val cache = ctx.options.findOptionOrDefault(verification.optVCCache)
+    val solvers = ctx.options.findOptionOrDefault(inox.optSelectedSolvers).toSeq.sorted.mkString(", ")
+    val batched = ctx.options.findOptionOrDefault(frontend.optBatchedProgram)
+
+    if (isExtendedSummaryOn) {
+      val admitStr = if (admitted) withColor("Admitted VCs", Console.RED, Console.BOLD) else ""
+      val termOffStr = if (termOff) withColor("Termination turned off", Console.RED, Console.BOLD) else ""
+      val oldVCStr = if (oldVC) withColor("Old VCs generation", Console.RED, Console.BOLD) else ""
+      val cacheStr = if (cache) "Cache used" else ""
+
+      def touched(sentance: String, ids: Set[Identifier], prefix: String): String =
+        s"""$sentance
+           |${join(ids.toSeq.map(_.name).sorted, prefix = prefix)}""".stripMargin
+
+      def touchedFns(phaseName: String, fns: Set[Identifier]): String =
+        touched(s"$phaseName phase transformed the following functions:", fns, " " * 4)
+
+      val aaStr = if (sd.antiAliasing.hasRun) touchedFns("Anti-aliasing", sd.antiAliasing.affectedFns) else ""
+      val reStr = if (sd.retAndWhileTran.hasReturnRun) touchedFns("Return transformation", sd.retAndWhileTran.retAffectedFns) else ""
+      val weStr = if (sd.retAndWhileTran.hasWhileRun) touchedFns("While transformation", sd.retAndWhileTran.whileAffectedFns) else ""
+      val ieStr = if (sd.imperativeElim.hasRun) touchedFns("Imperative elimination", sd.imperativeElim.affectedFns) else ""
+      val teStr = if (sd.typeEncoding.hasRun) {
+        val te = sd.typeEncoding
+        val fns = if (te.affectedFns.nonEmpty) touched("-Functions:", te.affectedFns, " " * 6) else ""
+        val sorts = if (te.affectedSorts.nonEmpty) touched("-Sorts:", te.affectedSorts, " " * 6) else ""
+        val classes = if (te.classes.nonEmpty) touched("-Classes:", te.classes, " " * 6) else ""
+        val items = Seq(fns, sorts, classes).filter(_.nonEmpty).mkString(" " * 4, "\n    ", "")
+        s"""Type-encoding transformed the following:
+           |$items""".stripMargin
+      } else ""
+      val ceStr = if (sd.chooseInjection.hasRun) {
+        val ce = sd.chooseInjection
+        val user = if (ce.affectedUserFns.nonEmpty) withMultilineColor(touched("-User:", ce.affectedUserFns, " " * 6), Console.YELLOW, Console.BOLD) else ""
+        val lib = if (ce.affectedLibFns.nonEmpty) touched("-Library:", ce.affectedLibFns, " " * 6) else ""
+        val items = Seq(user, lib).filter(_.nonEmpty).mkString(" " * 4, "\n    ", "")
+        s"""Choose injected in the following functions:
+           |$items""".stripMargin
+      } else ""
+
+      val solversUsed = s"Solvers used: $solvers"
+      val procMode = s"Processing mode: ${if (batched) "batched" else "partial"}"
+
+      val items = Seq(admitStr, termOffStr, oldVCStr, cacheStr, aaStr, reStr, weStr, ieStr, teStr, ceStr, solversUsed, procMode).filter(_.nonEmpty)
+      s"""Verification pipeline summary:
+         |${items.mkString("  ", "\n  ", "")}""".stripMargin // No join(items) here as their sub-items are already split according to the character limit
+    } else {
+      val admitStr = if (admitted) withColor("admitted VCs", Console.RED, Console.BOLD) else ""
+      val termOffStr = if (termOff) withColor("termination off", Console.RED, Console.BOLD) else ""
+      val oldVCStr = if (oldVC) withColor("old VCs gen", Console.RED, Console.BOLD) else ""
+      val cacheStr = if (cache) "cache" else ""
+      val aaStr = if (sd.antiAliasing.hasRun) "anti-aliasing" else ""
+      val reStr = if (sd.retAndWhileTran.hasReturnRun) "return transformation" else ""
+      val weStr = if (sd.retAndWhileTran.hasWhileRun) "while transformation" else ""
+      val ieStr = if (sd.imperativeElim.hasRun) "imperative elimination" else ""
+      val teStr = if (sd.typeEncoding.hasRun) "type encoding" else ""
+      val ceStr = if (sd.chooseInjection.hasRun) withColor("choose injection", Console.YELLOW, Console.BOLD) else ""
+      val batchedStr = if (batched) "batched" else ""
+      val items = Seq(admitStr, termOffStr, oldVCStr, cacheStr, aaStr, reStr, weStr, ieStr, teStr, ceStr, solvers, batchedStr).filter(_.nonEmpty)
+      s"""Verification pipeline summary:
+         |${join(items, prefix = "  ")}""".stripMargin
+    }
+  }
+
+  private case class SummaryData(
+    antiAliasing: imperative.AntiAliasing.SummaryData = imperative.AntiAliasing.SummaryData(),
+    retAndWhileTran: imperative.ReturnElimination.SummaryData = imperative.ReturnElimination.SummaryData(),
+    imperativeElim: imperative.ImperativeCodeElimination.SummaryData = imperative.ImperativeCodeElimination.SummaryData(),
+    typeEncoding: oo.TypeEncoding.SummaryData = oo.TypeEncoding.SummaryData(),
+    chooseInjection: inlining.ChooseInjector.SummaryData = inlining.ChooseInjector.SummaryData(),
+  ) {
+    def ++(other: SummaryData): SummaryData = SummaryData(
+      antiAliasing ++ other.antiAliasing,
+      retAndWhileTran ++ other.retAndWhileTran,
+      imperativeElim ++ other.imperativeElim,
+      typeEncoding ++ other.typeEncoding,
+      chooseInjection ++ other.chooseInjection
+    )
+    def +(other: imperative.AntiAliasing.SummaryData): SummaryData = copy(antiAliasing = antiAliasing ++ other)
+    def +(other: imperative.ReturnElimination.SummaryData): SummaryData = copy(retAndWhileTran = retAndWhileTran ++ other)
+    def +(other: imperative.ImperativeCodeElimination.SummaryData): SummaryData = copy(imperativeElim = imperativeElim ++ other)
+    def +(other: oo.TypeEncoding.SummaryData): SummaryData = copy(typeEncoding = typeEncoding ++ other)
+    def +(other: inlining.ChooseInjector.SummaryData): SummaryData = copy(chooseInjection = chooseInjection ++ other)
+  }
+
+  private def prepareExtractionSummaryData: SummaryData = {
+    extractionSummary.leafs.foldLeft(SummaryData()) {
+      case (acc, l@ExtractionSummary.Leaf(extraction.imperative.AntiAliasing)) =>
+        acc + l.summary.asInstanceOf[extraction.imperative.AntiAliasing.SummaryData]
+
+      case (acc, l@ExtractionSummary.Leaf(extraction.imperative.ReturnElimination)) =>
+        acc + l.summary.asInstanceOf[extraction.imperative.ReturnElimination.SummaryData]
+
+      case (acc, l@ExtractionSummary.Leaf(extraction.imperative.ImperativeCodeElimination)) =>
+        acc + l.summary.asInstanceOf[extraction.imperative.ImperativeCodeElimination.SummaryData]
+
+      case (acc, l@ExtractionSummary.Leaf(extraction.oo.TypeEncoding)) =>
+        acc + l.summary.asInstanceOf[extraction.oo.TypeEncoding.SummaryData]
+
+      case (acc, l@ExtractionSummary.Leaf(extraction.inlining.ChooseInjector)) =>
+        acc + l.summary.asInstanceOf[extraction.inlining.ChooseInjector.SummaryData]
+
+      case (acc, _) => acc
+    }
+  }
 }
 
 // Provide all the logic for typical Report.
@@ -191,6 +336,7 @@ class NoReport extends AbstractReport[NoReport] { // can't do this CRTP with obj
   override val name = "no-report"
   override val emitJson = Json.arr()
   override val annotatedRows = Seq.empty
+  override val extractionSummary = ExtractionSummary.NoSummary
   override val stats = ReportStats(0, 0, 0, 0, 0, 0)
   override def filter(ids: Set[Identifier]) = this
   override def ~(other: NoReport) = this

core/src/main/scala/stainless/evaluators/EvaluatorAnalysis.scala

@@ -3,13 +3,16 @@
 package stainless
 package evaluators
 
+import stainless.extraction.ExtractionSummary
+
 trait EvaluatorAnalysis extends AbstractAnalysis {
   import EvaluatorRun.Result
   import EvaluatorReport.Record
 
   val program: StainlessProgram
   val sources: Set[Identifier] // set of functions that were considered for the analysis
   val results: Seq[Result]
+  val extractionSummary: ExtractionSummary
 
   private lazy val records = results map { case Result(fd, status, time) =>
     val textStatus = status match {
@@ -24,6 +27,6 @@ trait EvaluatorAnalysis extends AbstractAnalysis {
 
   override type Report = EvaluatorReport
   override val name = EvaluatorComponent.name
-  override def toReport = new EvaluatorReport(records, sources)
+  override def toReport = new EvaluatorReport(records, sources, extractionSummary)
 }
 

core/src/main/scala/stainless/evaluators/EvaluatorComponent.scala

@@ -3,12 +3,12 @@
 package stainless
 package evaluators
 
-import inox.evaluators.EvaluationResults.{ EvaluatorError, RuntimeError, Successful }
-
-import io.circe._
+import inox.evaluators.EvaluationResults.{EvaluatorError, RuntimeError, Successful}
+import io.circe.*
+import stainless.extraction.ExtractionSummary
 
 import scala.concurrent.Future
-import scala.util.{ Success, Failure }
+import scala.util.{Failure, Success}
 
 object DebugSectionEvaluator extends inox.DebugSection("eval")
 
@@ -71,7 +71,7 @@ class EvaluatorRun private(override val component: EvaluatorComponent.type,
 
   override def createFilter = EvaluatorCheckFilter(trees, context)
 
-  private[stainless] def execute(functions: Seq[Identifier], symbols: Symbols): Future[Analysis] = {
+  override private[stainless] def execute(functions: Seq[Identifier], symbols: Symbols, exSummary: ExtractionSummary): Future[Analysis] = {
     import context.{given, _}
 
     val p = inox.Program(trees)(symbols)
@@ -181,6 +181,7 @@ class EvaluatorRun private(override val component: EvaluatorComponent.type,
       override val program = p
       override val sources = functions.toSet
       override val results = functions map (id => processFunction(symbols.getFunction(id)))
+      override val extractionSummary = exSummary
     })
   }
 }

core/src/main/scala/stainless/evaluators/EvaluatorReport.scala

@@ -4,6 +4,7 @@ package stainless
 package evaluators
 
 import stainless.utils.JsonConvertions.given
+import stainless.extraction.ExtractionSummary
 
 import io.circe._
 import io.circe.syntax._
@@ -38,19 +39,19 @@ object EvaluatorReport {
   given recordEncoder: Encoder[Record] = deriveEncoder
 
   def parse(json: Json) = json.as[(Seq[Record], Set[Identifier])] match {
-    case Right((records, sources)) => new EvaluatorReport(records, sources)
+    case Right((records, sources)) => new EvaluatorReport(records, sources, ExtractionSummary.NoSummary)
     case Left(error) => throw error
   }
 }
 
-class EvaluatorReport(val results: Seq[EvaluatorReport.Record], val sources: Set[Identifier])
+class EvaluatorReport(val results: Seq[EvaluatorReport.Record], val sources: Set[Identifier], override val extractionSummary: ExtractionSummary)
   extends BuildableAbstractReport[EvaluatorReport.Record, EvaluatorReport] {
   import EvaluatorReport.{given, _}
 
   override val encoder = recordEncoder
 
   override def build(results: Seq[Record], sources: Set[Identifier]) =
-    new EvaluatorReport(results, sources)
+    new EvaluatorReport(results, sources, ExtractionSummary.NoSummary)
 
   override val name = EvaluatorComponent.name