diff --git a/build.sbt b/build.sbt index 74c37aed1..d6f8f88e7 100644 --- a/build.sbt +++ b/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) diff --git a/core/src/main/scala/stainless/MainHelpers.scala b/core/src/main/scala/stainless/MainHelpers.scala index 85135bba4..f4bc6a9b7 100644 --- a/core/src/main/scala/stainless/MainHelpers.scala +++ b/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"), diff --git a/core/src/main/scala/stainless/frontend/package.scala b/core/src/main/scala/stainless/frontend/package.scala index c1c4e87aa..fe79b94b0 100644 --- a/core/src/main/scala/stainless/frontend/package.scala +++ b/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 diff --git a/core/src/main/scala/stainless/verification/VerificationConditions.scala b/core/src/main/scala/stainless/verification/VerificationConditions.scala index 220bb36ee..33adf70ae 100644 --- a/core/src/main/scala/stainless/verification/VerificationConditions.scala +++ b/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) { diff --git a/frontends/common/src/it/scala/stainless/LibrarySuite.scala b/frontends/common/src/it/scala/stainless/LibrarySuite.scala index ca645660d..94a1ed637 100644 --- a/frontends/common/src/it/scala/stainless/LibrarySuite.scala +++ b/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") diff --git a/frontends/common/src/test/scala/stainless/InputUtils.scala b/frontends/common/src/test/scala/stainless/InputUtils.scala index 7d8a296af..41b5bdffa 100644 --- a/frontends/common/src/test/scala/stainless/InputUtils.scala +++ b/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 }) = { diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/DottyCompiler.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/DottyCompiler.scala index d0d1d4806..941544bfd 100644 --- a/frontends/dotty/src/main/scala/stainless/frontends/dotc/DottyCompiler.scala +++ b/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 { } } } -} \ No newline at end of file +} diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/StainlessExtraction.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/StainlessExtraction.scala index 9c1984384..080bb1d04 100644 --- a/frontends/dotty/src/main/scala/stainless/frontends/dotc/StainlessExtraction.scala +++ b/frontends/dotty/src/main/scala/stainless/frontends/dotc/StainlessExtraction.scala @@ -3,18 +3,25 @@ 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]) @@ -22,37 +29,49 @@ 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 + } } + diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/SymbolMapping.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/SymbolMapping.scala index 64d2aee84..43b5f1ab1 100644 --- a/frontends/dotty/src/main/scala/stainless/frontends/dotc/SymbolMapping.scala +++ b/frontends/dotty/src/main/scala/stainless/frontends/dotc/SymbolMapping.scala @@ -5,12 +5,14 @@ package frontends.dotc import scala.language.implicitConversions +import dotty.tools.dotc.ast.tpd +import dotty.tools.dotc.core.CompilationUnitInfo import dotty.tools.dotc.core.Flags._ import dotty.tools.dotc.core.Symbols._ import dotty.tools.dotc.core.Contexts._ import stainless.ast.SymbolIdentifier -import scala.collection.mutable.{ Map => MutableMap } +import scala.collection.mutable.{ Map => MutableMap, LinkedHashMap } class SymbolMapping { import SymbolMapping._ @@ -25,10 +27,48 @@ class SymbolMapping { private val s2sAccessor = MutableMap[Symbol, SymbolIdentifier]() private val s2sEnumType = MutableMap[Symbol, SymbolIdentifier]() + /** Returns a mapping from used Dotty unit trees loaded from Tasty files to their + * [[CompilationUnitInfo]]. + * + * Everytime a [[Symbol]] is touched through [[fetch]], we check if it has an + * associated Tasty file. If it does, we register the symbol's root tree + * (which is the tree of the compilation unit containing the symbol's + * definition) and its associated compilation unit info (which contains the + * path to the Tasty file among other things). + * + * We keep this information to later extract compilation units defined in + * Tasty files, in [[StainlessExtraction.extractTastyUnits]]. + * + * This a [[LinkedHashMap]] to keep elements in insertion order (there is no + * efficient immutable equivalent in the Scala standard library). + * + * Side-effect: calling this method clears the internal list of used Tasty + * units. + * + * Potential performance improvement: `Tree.equals` and `Tree.hashCode` might + * be suboptimal. Comparing by reference sould be sufficient. + */ + def popUsedTastyUnits(): LinkedHashMap[tpd.Tree, CompilationUnitInfo] = + val res = usedTastyUnits + usedTastyUnits = LinkedHashMap[tpd.Tree, CompilationUnitInfo]() + res + + private var usedTastyUnits = LinkedHashMap[tpd.Tree, CompilationUnitInfo]() + + private def maybeRegisterTastyUnit(sym: Symbol)(using Context): Unit = { + if (sym.tastyInfo.isDefined) { + val classSym = sym.topLevelClass.asClass + // Below, `classSym.rootTree` returns the tree read from the Tasty file. + // It works because we passed the `-Yretain-trees` option to the compiler. + usedTastyUnits += (classSym.rootTree -> classSym.compilationUnitInfo) + } + } + /** Get the identifier associated with the given [[sym]], creating a new one if needed. */ def fetch(sym: Symbol, mode: FetchingMode)(using Context): SymbolIdentifier = mode match { case Plain => s2s.getOrElseUpdate(sym, { + maybeRegisterTastyUnit(sym) val overrides = sym.allOverriddenSymbols.toSeq val top = overrides.lastOption.getOrElse(sym) if (top eq sym) { @@ -39,6 +79,7 @@ class SymbolMapping { }) case FieldAccessor => s2sAccessor.getOrElseUpdate(sym, { + maybeRegisterTastyUnit(sym) val overrides = sym.allOverriddenSymbols.toSeq val top = overrides.lastOption.getOrElse(sym) if (top eq sym) { @@ -52,6 +93,7 @@ class SymbolMapping { }) case EnumType => s2sEnumType.getOrElseUpdate(sym, { + maybeRegisterTastyUnit(sym) assert(sym.allOverriddenSymbols.isEmpty) SymbolIdentifier(ast.Symbol(symFullName(sym))) }) @@ -66,6 +108,7 @@ class SymbolMapping { res }) } + } object SymbolMapping { @@ -93,4 +136,4 @@ object SymbolMapping { } .mkString(".") } -} \ No newline at end of file +}