Add support for extracting from Tasty (#1606)

* Add support for separate compilation

* Load Stainless standard library from the classpath

* Fix spurious duplicate loads of Tasty units

* Fix LibrarySuite test

build.sbt

@@ -303,8 +303,6 @@ lazy val `stainless-library` = (project in file("frontends") / "library")
   .settings(
     name := "stainless-library",
     scalaVersion := stainlessLibScalaVersion,
-    // don't publish binaries - stainless-library is only consumed as a sources component
-    packageBin / publishArtifact := false,
     crossVersion := CrossVersion.binary,
     Compile / scalaSource := baseDirectory.value / "stainless"
   )
@@ -343,6 +341,7 @@ lazy val `stainless-dotty` = (project in file("frontends/dotty"))
     },
   )
   .dependsOn(`stainless-core`)
+  .dependsOn(`stainless-library`)
   .dependsOn(inox % "test->test;it->test,it")
   .configs(IntegrationTest)
 

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

@@ -74,6 +74,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
     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"),
     frontend.optExtraResolvers -> Description(General, "Extra resolvers to use to fetch extra source dependencies"),
+    frontend.optClasspath -> Description(General, "Add the specified directory to the classpath"),
     utils.Caches.optCacheDir -> Description(General, "Specify the directory in which cache files should be stored"),
     utils.Caches.optBinaryCache -> Description(General, "Set Binary mode for the cache instead of Hash mode, i.e., the cache will contain the entire VC and program in serialized format. This is less space efficient."),
     testgen.optOutputFile -> Description(TestsGeneration, "Specify the output file"),

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

@@ -23,6 +23,13 @@ package object frontend {
     */
   object optBatchedProgram extends inox.FlagOptionDef("batched", false)
 
+  object optClasspath extends inox.OptionDef[Option[String]] {
+    val name = "classpath"
+    val default = None
+    val parser = input => Some(Some(input))
+    val usageRhs = "DIR"
+  }
+
   /**
    * Given a context (with its reporter) and a frontend factory, proceed to compile,
    * extract, transform and verify the input programs based on the active components

core/src/main/scala/stainless/verification/VerificationConditions.scala

@@ -27,6 +27,8 @@ case class VC[T <: ast.Trees](val trees: T)(val condition: trees.Expr, val fid:
     val state = Seq(trees, condition, fid, kind, satisfiability)
     state.map(_.hashCode()).foldLeft(0)((a, b) => 31 * a + b)
   }
+
+  override def toString(): String =  s"VC($condition)"
 }
 
 sealed abstract class VCKind(val name: String, val abbrv: String) {

frontends/common/src/it/scala/stainless/LibrarySuite.scala

@@ -31,7 +31,7 @@ abstract class AbstractLibrarySuite(opts: Seq[inox.OptionValue[?]]) extends AnyF
     val ctx: inox.Context = stainless.TestContext(options)
     import ctx.{reporter, given}
 
-    val tryProgram = scala.util.Try(loadFiles(Seq.empty)._2)
+    val tryProgram = scala.util.Try(loadFiles(Main.libraryFiles)._2)
     it("should be extractable") {
       assert(tryProgram.isSuccess, "Extraction crashed with exception")
       assert(reporter.errorCount == 0, "Extraction had errors")

frontends/common/src/test/scala/stainless/InputUtils.scala

@@ -35,7 +35,7 @@ trait InputUtils {
     loadFiles(files, filterOpt, sanitize)
   }
 
-  /** Compile and extract the given files (& the library). */
+  /** Compile and extract the given files. */
   def loadFiles(files: Seq[String], filterOpt: Option[Filter] = None, sanitize: Boolean = true)
                (using ctx: inox.Context): (Seq[xt.UnitDef], Program { val trees: xt.type }) = {
 

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

@@ -8,6 +8,7 @@ import plugins._
 import dotty.tools.dotc.reporting.{Diagnostic, Reporter => DottyReporter}
 import dotty.tools.dotc.interfaces.Diagnostic.{ERROR, WARNING, INFO}
 import dotty.tools.dotc.util.SourcePosition
+import dotty.tools.dotc.core.Symbols.{ClassSymbol => DottyClasSymbol}
 import dotty.tools.io.AbstractFile
 import core.Contexts.{Context => DottyContext, _}
 import core.Phases._
@@ -16,8 +17,11 @@ import typer._
 import frontend.{CallBack, Frontend, FrontendFactory, ThreadedFrontend}
 import Utils._
 
+import inox.DebugSection
+
 import java.io.File
 import java.net.URL
+import DottyReporter.NoReporter
 
 class DottyCompiler(ctx: inox.Context, callback: CallBack) extends Compiler {
   override def phases: List[List[Phase]] = {
@@ -50,7 +54,10 @@ class DottyCompiler(ctx: inox.Context, callback: CallBack) extends Compiler {
 
     override def runOn(units: List[CompilationUnit])(using dottyCtx: DottyContext): List[CompilationUnit] = {
       exportedSymsMapping = exportedSymbolsMapping(ctx, this.start, units)
-      super.runOn(units)
+      val res = super.runOn(units)
+      extraction.extractTastyUnits(exportedSymsMapping, ctx).foreach(extracted =>
+        callback(extracted.file, extracted.unit, extracted.classes, extracted.functions, extracted.typeDefs))
+      res
     }
   }
 
@@ -66,10 +73,13 @@ class DottyCompiler(ctx: inox.Context, callback: CallBack) extends Compiler {
   }
 }
 
-private class DottyDriver(args: Seq[String], compiler: DottyCompiler, reporter: DottyReporter) extends Driver {
+private class DottyDriver(args: Seq[String], compiler: DottyCompiler, reporter: SimpleReporter) extends Driver {
   override def newCompiler(using DottyContext) = compiler
 
-  lazy val files: List[String] = setup(args.toArray, initCtx).map(_._1.map(_.path)).getOrElse(Nil)
+  lazy val files: List[String] =
+    setup(args.toArray, initCtx.fresh.setReporter(NoReporter))
+      .map(_._1.map(_.path))
+      .getOrElse(reporter.reporter.internalError(f"Error parsing arguments from ${args.toList}"))
 
   def run(): Unit = process(args.toArray, reporter)
 }
@@ -139,10 +149,16 @@ object DottyCompiler {
     override val libraryPaths: Seq[String]
   ) extends FrontendFactory {
 
+    /** Overriden to not include library sources. */
+    final override protected def allCompilerArguments(ctx: inox.Context, compilerArgs: Seq[String]): Seq[String] = {
+      val extraSources = extraSourceFiles(ctx)
+      extraCompilerArguments ++ extraSources ++ compilerArgs
+    }
+
     override def apply(ctx: inox.Context, compilerArgs: Seq[String], callback: CallBack): Frontend =
       new ThreadedFrontend(callback, ctx) {
         val args = {
-          // Attempt to find where the Scala 2.13 and 3.0 libs are.
+          // Attempt to find where the Scala 2.13 and 3.0 libs, and the Stainless lib are.
           // The 3.0 library depends on the 2.13, so we need to fetch the later as well.
           val scala213Lib: String = Option(scala.Predef.getClass.getProtectionDomain.getCodeSource) map {
             x => new File(x.getLocation.toURI).getAbsolutePath
@@ -152,9 +168,19 @@ object DottyCompiler {
           val scala3Lib: String = Option(scala.util.NotGiven.getClass.getProtectionDomain.getCodeSource) map {
             x => new File(x.getLocation.toURI).getAbsolutePath
           } getOrElse { ctx.reporter.fatalError("No Scala 3 library found.") }
+          // Find the Stainless library by looking at the location of the `stainless.collection.List`.
+          val stainlessLib: String = Option(stainless.collection.List.getClass.getProtectionDomain.getCodeSource) map {
+            x => new File(x.getLocation.toURI).getAbsolutePath
+          } getOrElse { ctx.reporter.fatalError("No Stainless Library found.") }
+
+          given DebugSection = frontend.DebugSectionFrontend
+          ctx.reporter.debug(s"Scala library 2.13 found at: $scala213Lib")
+          ctx.reporter.debug(s"Scala library 3 found at: $scala3Lib")
+          ctx.reporter.debug(s"Stainless library found at: $stainlessLib")
 
-          val cps = Seq(scala213Lib, scala3Lib).distinct.mkString(java.io.File.pathSeparator)
-          val flags = Seq("-color:never", "-language:implicitConversions", "-Wsafe-init", s"-cp:$cps") // -Ysafe-init is deprecated (SAM 21.08.2024)
+          val extraCps = ctx.options.findOptionOrDefault(frontend.optClasspath).toSeq
+          val cps = (extraCps ++ Seq(stainlessLib, scala213Lib, scala3Lib)).distinct.mkString(java.io.File.pathSeparator)
+          val flags = Seq("-Yretain-trees", "-color:never", "-language:implicitConversions", "-Wsafe-init", s"-cp:$cps") // -Ysafe-init is deprecated (SAM 21.08.2024)
           allCompilerArguments(ctx, compilerArgs) ++ flags
         }
         val compiler: DottyCompiler = new DottyCompiler(ctx, this.callback)
@@ -180,4 +206,4 @@ object DottyCompiler {
         }
       }
   }
-}
+}

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

@@ -3,56 +3,75 @@
 package stainless
 package frontends.dotc
 
+import scala.collection.mutable.{LinkedHashMap, ArrayBuffer}
+
+import dotty.tools.io.AbstractFile
 import dotty.tools.dotc._
 import core.Names._
 import core.Symbols._
+import core.CompilationUnitInfo
 import core.Contexts.{Context => DottyContext}
 import transform._
 import ast.tpd
 import ast.Trees._
 import typer._
 
+import inox.DebugSection
+
 import extraction.xlang.{trees => xt}
-import frontend.{CallBack, Frontend, FrontendFactory, ThreadedFrontend, UnsupportedCodeException}
+import frontend.{CallBack, Frontend, FrontendFactory, ThreadedFrontend, UnsupportedCodeException, DebugSectionFrontend}
 import Utils._
+import stainless.verification.CoqEncoder.m
 
 case class ExtractedUnit(file: String, unit: xt.UnitDef, classes: Seq[xt.ClassDef], functions: Seq[xt.FunDef], typeDefs: Seq[xt.TypeDef])
 
 class StainlessExtraction(val inoxCtx: inox.Context) {
   private val symbolMapping = new SymbolMapping
 
   def extractUnit(exportedSymsMapping: ExportedSymbolsMapping)(using ctx: DottyContext): Option[ExtractedUnit] = {
+    val unit = ctx.compilationUnit
+    val tree = unit.tpdTree
+    extractUnit(tree, unit.source.file, exportedSymsMapping, isFromSource = true)
+  }
+
+  def extractUnit(
+    tree: tpd.Tree,
+    file: AbstractFile,
+    exportedSymsMapping: ExportedSymbolsMapping,
+    isFromSource: Boolean,
+  )(using ctx: DottyContext): Option[ExtractedUnit] = {
     // Remark: the method `extractUnit` is called for each compilation unit (which corresponds more or less to a Scala file)
     // Therefore, the symbolMapping instances needs to be shared accross compilation unit.
     // Since `extractUnit` is called within the same thread, we do not need to synchronize accesses to symbolMapping.
     val extraction = new CodeExtraction(inoxCtx, symbolMapping, exportedSymsMapping)
     import extraction._
 
-    val unit = ctx.compilationUnit
-    val tree = unit.tpdTree
     val (id, stats) = tree match {
-      case pd@PackageDef(_, lst) =>
+      case pd@PackageDef(pid, lst) =>
         val id = lst.collectFirst { case PackageDef(ref, _) => ref } match {
           case Some(ref) => extractRef(ref)
-          case None => FreshIdentifier(unit.source.file.name.replaceFirst("[.][^.]+$", ""))
+          case None => FreshIdentifier(file.name.replaceFirst("[.][^.]+$", ""))
         }
         (id, pd.stats)
       case _ =>
-        (FreshIdentifier(unit.source.file.name.replaceFirst("[.][^.]+$", "")), List.empty)
+        inoxCtx.reporter.info("Empty package definition: " + file.name)
+        (FreshIdentifier(file.name.replaceFirst("[.][^.]+$", "")), List.empty)
     }
 
     val fragmentChecker = new FragmentChecker(inoxCtx)
     fragmentChecker.ghostChecker(tree)
     fragmentChecker.checker(tree)
 
-    if (!fragmentChecker.hasErrors()) tryExtractUnit(extraction, unit, id, stats)
+    if (!fragmentChecker.hasErrors()) tryExtractUnit(extraction, file, id, stats, isFromSource)
     else None
   }
 
   private def tryExtractUnit(extraction: CodeExtraction,
-                             unit: CompilationUnit,
+                             file: AbstractFile,
                              id: Identifier,
-                             stats: List[tpd.Tree])(using DottyContext): Option[ExtractedUnit] = {
+                             stats: List[tpd.Tree],
+                             isFromSource: Boolean
+  )(using DottyContext): Option[ExtractedUnit] = {
     // If the user annotates a function with @main, the compiler will generate a top-level class
     // with the same name as the function.
     // This generated class defines def main(args: Array[String]): Unit
@@ -67,10 +86,8 @@ class StainlessExtraction(val inoxCtx: inox.Context) {
     try {
       val (imports, unitClasses, unitFunctions, _, subs, classes, functions, typeDefs) = extraction.extractStatic(filteredStats)
       assert(unitFunctions.isEmpty, "Packages shouldn't contain functions")
-      val file = unit.source.file.absolute.path
-      val isLibrary = stainless.Main.libraryFiles contains file
-      val xtUnit = xt.UnitDef(id, imports, unitClasses, subs, !isLibrary)
-      Some(ExtractedUnit(file, xtUnit, classes, functions, typeDefs))
+      val xtUnit = xt.UnitDef(id, imports, unitClasses, subs, isFromSource)
+      Some(ExtractedUnit(file.absolute.path, xtUnit, classes, functions, typeDefs))
     } catch {
       case UnsupportedCodeException(pos, msg) =>
         inoxCtx.reporter.error(pos, msg)
@@ -92,4 +109,67 @@ class StainlessExtraction(val inoxCtx: inox.Context) {
     }
     trAcc(None, stats)
   }
+
+  /** Extract units defined in Tasty files.
+    * 
+    * This will only extract units that have not been extracted yet.
+    * 
+    * See [[SymbolMapping.popUsedTastyUnits]] for more information about how
+    * these units are collected.
+    * 
+    * Side-effect: calls [[SymbolMapping.popUsedTastyUnits]].
+    */
+  def extractTastyUnits(exportedSymsMapping: ExportedSymbolsMapping, inoxCtx: inox.Context)(using DottyContext): Seq[ExtractedUnit] = {
+    given DebugSection = DebugSectionFrontend
+
+    def extractTastyUnit(tree: tpd.Tree, info: CompilationUnitInfo): Option[ExtractedUnit] = {
+      val res = extractUnit(tree, info.associatedFile, exportedSymsMapping, isFromSource = false)
+      res match {
+        case Some(extracted) => inoxCtx.reporter.debug(s"- Extracted ${extracted.unit.id}.")
+        case None => inoxCtx.reporter.debug(s"- Failed to extract Tasty unit from ${info.associatedFile.path}.")
+      }
+      res
+    }
+
+    // We avoid extracting Tasty units under `scala` because these are generally
+    // not supported by Stainless, and because only a fragment of the Scala
+    // standard library is available as Tasty files. Trying to extract units
+    // from `scala` would therefore cause missing dependencies errors.  
+    //
+    // TODO(mbovel): However, this is not a general fix. A similar situation
+    // could happen for non-library files: extracting the Tasty unit of a symbol
+    // accessed only from within an `@exern` method could yield failures when
+    // extracting the unit is not required in the first place. This is an edge
+    // case to be addressed later, either by making sure that the body of
+    // `@extern` methods is not visited at all, or by not registering used Tasty
+    // units for symbols accessed only from within `@extern` methods.
+    val unextractedPackages: Set[Symbol] = Set(defn.ScalaPackageClass)
+
+    // Potential performance improvement: share the Map of extracted Tasty units
+    // accross runs, so that we don't extract the same units multiple times in
+    // watch mode. However that could also cause a memory leak if the map is
+    // never cleared. To be investigated.
+    val extractedTastyUnits = LinkedHashMap[tpd.Tree, Option[ExtractedUnit]]()
+
+    var depth = 0
+
+    while depth < 100 do
+      inoxCtx.reporter.debug(f"Extracting Tasty units at depth $depth:")
+      val newUnits =
+        symbolMapping
+          .popUsedTastyUnits()
+          .filterNot((tree, _) => extractedTastyUnits.contains(tree))
+          .filterNot((tree, _) => tree.symbol.ownersIterator.exists(unextractedPackages))
+          .map((tree, info) => tree -> extractTastyUnit(tree, info))
+      if newUnits.isEmpty then
+        inoxCtx.reporter.debug(f"- No more units to extract.")
+        return extractedTastyUnits.values.flatten.toSeq
+      extractedTastyUnits ++= newUnits
+      depth += 1
+
+    // This should not be reached.
+    inoxCtx.reporter.error("Reached maximum depth while extracting Tasty units. This is likely a bug in Stainless.")
+    Nil
+  }
 }
+