Add support for extracting from Tasty

[mbovel]

This PR enables loading trees from Tasty files located on the class path. This feature:

1. can be used via the newly introduced --classpath option,
2. and is enabled by default to load the Stainless standard library.

Implementation

• Loading trees from Tasty is handled transparently by Dotty. We call .rootTree on the unit’s class symbol, which works because the -Yretain-trees compiler option instructs Dotty to keep Tasty trees.
• Extracting these trees is done in StainlessExtraction.extractTastyUnits. This method is invoked from DottyCompiler.runOn, which runs after all source compilation units have been processed.
• The set of Tasty unit trees to extract is computed as follows:
  • A base set of “used Tasty units” is stored in SymbolMapping. It can be retrieved with SymbolMapping.popUsedTastyUnits(). Symbols are added to this set whenever SymbolMapping.fetch is called and the fetched symbol has corresponding Tasty information.
  • Dependent symbols are discovered transitively in a breadth-first search manner.

Performance

For a file that only uses stainless.lang.{Option,None,Some} for example, this PR reduces the time for a Stainless compilation cycle from ~7 seconds, to ~0.1 second, both in watch mode and in normal mode.

It also reduces the CI time from ~55 minutes to ~32 minutes.

[samuelchassot]

The CI does not run on Draft PR :)

[vkuncak]

Is this anywhere close to working with so few changes? This would be exciting.

[vkuncak]

I'm in favor of mergning early and continue experimenting.
According to stainless/bin/package-standalone.sh, to build the library we use
sbt stainless-library/package stainless-library/packageSrc
Along with changing libfiles.txt , this can be used to test tasty input for the library.

[mbovel]

According to stainless/bin/package-standalone.sh, to build the library we use sbt stainless-library/package stainless-library/packageSrc
Along with changing libfiles.txt , this can be used to test tasty input for the library.

Tasty files don't need to/cannot be passed explicitly. Instead, they are loaded from the class path lazily by Dotty when needed.

In this POC, this is triggered by calling rootTree on a ClassSymbol, from the newly added method StainlessExtraction.extractClasspathUnits:

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

Lines 110 to 122 in 46e3dcd

	def extractClasspathUnits(exportedSymsMapping: ExportedSymbolsMapping, inoxCtx: inox.Context)(using DottyContext): Seq[ExtractedUnit] = {
	@scala.annotation.tailrec
	def loop(units: Map[ClassSymbol, ExtractedUnit]): Seq[ExtractedUnit] =
	val newUnits =
	symbolMapping
	.getUsedTastyClasses()
	.filterNot(units.contains)
	.map(sym => sym -> extractUnit(sym.rootTree, sym.sourceOfClass, exportedSymsMapping, isFromSource = false).get)
	.toMap
	if (newUnits.isEmpty) units.values.toSeq
	else loop(units ++ newUnits)
	loop(Map.empty)

---

4c908a8 enables to separately compile a.scala and then verify a dependent file b.scala with Stainless like this:

bovel@laraserver4:/localhome/bovel/stainless$ scala compile a.scala -d out

bovel@laraserver4:/localhome/bovel/stainless$ frontends/dotty/target/universal/stage/bin/stainless-dotty --classpath=out b.scala
[  Info  ] Stainless library found at: /localhome/bovel/stainless/frontends/dotty/target/universal/stage/lib/ch.epfl.lara.stainless-library-0.9.8.9-14-g81f18e9-SNAPSHOT.jar
[  Info  ] Compiling with standard Scala 3.5.2 compiler front end...
[  Info  ] Extracted classpath unit: a
[  Info  ] Finished compiling
[  Info  ] Preprocessing finished      
[  Info  ] Finished lowering the symbols          
[  Info  ] Finished generating VCs                
[  Info  ] Starting verification...
[  Info  ]  Verified: 1 / 1                     
[  Info  ] Done in 1.16s
[  Info  ]   ┌───────────────────┐
[  Info  ] ╔═╡ stainless summary ╞═════════════════════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └───────────────────┘                                                                                 ║
[  Info  ] ║ b.scala:6:5:            g   precond. (call f(x))                valid from cache                0.0   ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 1    valid: 1    (1 from cache, 0 trivial) invalid: 0    unknown: 0    time:    0.01           ║
[  Info  ] ╚═══════════════════════════════════════════════════════════════════════════════════════════════════════╝
[  Info  ] Verification pipeline summary:
[  Info  ]   cache, nativez3, non-batched
[  Info  ] Shutting down executor service.

given:

// a.scala
package liba

object A:
  def f(x: Int): Int =
    require(x > 0)
    x

and:

// b.scala
package libb

object B:
  def g() =
    val x = -1
    liba.A.f(x)

[mbovel]

@samuelchassot: the bug I was chasing yesterday was due to the isMain field of UnitDef:

stainless/core/src/main/scala/stainless/extraction/xlang/Trees.scala

Line 28 in fdf67d4

isMain: Boolean

which is used only from the ComponentTestSuite:

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

Line 60 in fdf67d4

if unit.isMain

not being correctly computed:

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

Lines 71 to 72 in fdf67d4

	val isLibrary = stainless.Main.libraryFiles contains file
	val xtUnit = xt.UnitDef(id, imports, unitClasses, subs, !isLibrary)

as it was only false for units coming from library sources but not when loading them from the class path. I adapted it to be always false when reading units from the class path.

[mbovel]

Comparing the last successful CI run on main (https://github.com/epfl-lara/stainless/actions/runs/12195696068/job/34021825652) and the last CI run on this PR (https://github.com/epfl-lara/stainless/actions/runs/12199627173/job/34033919695?pr=1606), everything seems fine:

➜  ~/Desktop grep "Tests:" main.txt             
2024-12-06T08:47:39.5309238Z [info] Tests: succeeded 19, failed 0, canceled 0, ignored 0, pending 0
2024-12-06T08:53:24.2885785Z [info] Tests: succeeded 52, failed 0, canceled 0, ignored 0, pending 0
2024-12-06T09:37:33.4031429Z [info] Tests: succeeded 2942, failed 0, canceled 0, ignored 169, pending 0
➜  ~/Desktop grep "Tests:" pr.txt  
2024-12-06T13:29:55.2845908Z [info] Tests: succeeded 19, failed 0, canceled 0, ignored 0, pending 0
2024-12-06T13:30:12.9407870Z [info] Tests: succeeded 52, failed 0, canceled 0, ignored 0, pending 0
2024-12-06T13:50:22.0754541Z [info] Tests: succeeded 2942, failed 0, canceled 0, ignored 169, pending 0

Runtimes are 55 minutes for main and 25 minutes for this PR.

However, there is at least one thing wrong: scalac is invoked with invalid arguments at some points:

➜  ~/Desktop grep "Usage:" main.txt
➜  ~/Desktop grep -B 2 -A 10 "Usage:" pr.txt
2024-12-06T13:32:52.3296078Z [info] -  48: termination/valid/i1405b  (25 milliseconds)
2024-12-06T13:32:52.3296878Z [info] -  49: termination/valid/i731a  (364 milliseconds)
2024-12-06T13:32:52.3627559Z Usage: scalac <options> <source files>
2024-12-06T13:32:52.3628189Z where possible standard options include:
2024-12-06T13:32:52.3628627Z                            {  
2024-12-06T13:32:52.3629176Z           -D<property=value>  Pass -D<property=value> directly to the runtime
2024-12-06T13:32:52.3629742Z                               system.
2024-12-06T13:32:52.3630240Z                     -J<flag>  Pass -J<flag> directly to the runtime system.
2024-12-06T13:32:52.3630900Z                           -P  Pass an option to a plugin, e.g. -P:<plugin>:<opt>
2024-12-06T13:32:52.3631462Z                           -V  Print a synopsis of verbose options.
2024-12-06T13:32:52.3631996Z                           -W  Print a synopsis of warning options.
2024-12-06T13:32:52.3632520Z                       -Wconf  Configure compiler warnings.
2024-12-06T13:32:52.3633082Z                      -Werror  Fail the compilation if there are any warnings.

I need to check what's going there. My guess would be that the detected class path for the Stainless standard library is invalid there. It's strange that it is not detected as an error.

Edit: this comes from the setup of LibrarySuite.

Edit 2: fixed. The list of library files now needs to be passed explicitly.

[mbovel]

Nightly failing for uarray: https://github.com/epfl-lara/stainless/actions/runs/12201564125/job/34040256144#step:9:1580.

[vkuncak]

@mbovel this class wraps existing Scala classes into Stainless ones. I don't know how to do it otherwise in Stainless and it's important functionality. So, we need to avoid triggering the warning and just silently ignore types that are annotated as @extern. The error message actually links to the documentation: https://epfl-lara.github.io/stainless/wrap.html So, we would like this to continue to work as we move to tasty.

[vkuncak]

I don't know why the problem is triggered now, but not in the existing solution. I can confirm that replacing

      val content = new Array[T](size)

with

      val content = (??? : Array[T])

makes it pass. Hence, it appers that new is somehow being traversed despite the @extern annotation on the method, and this triggers the extraction of library code.

[vkuncak]

For now, I have committed a workaround in uarray by putting the problematic new Array[T] in a method marked by @ignore, so the bolts should work ; you can rebase and we can merge.

[mbovel]

For now, I have committed a workaround in uarray by putting the problematic new Array[T] in a method marked by @ignore, so the bolts should work ; you can rebase and we can merge.

This is not needed anymore. I am now avoiding to extract Tasty units under scala and java to avoid triggering these issues later in the pipeline.

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 quite an edge case, I think it could be fixed later.

I should add a comment here.

[mbovel]

Done 👍

[mbovel]

I rebased on top of main and updated the PR description.

The CI passes.