Migrate Stainless to scala 3.5 (#1561)

* updated stainless sources, extraction pipeline, and tests to Scala 3.5!
  * change ensuring infix to .ensuring call
  * remove infix notation for non infix functions in library
  * fix expected output for which Scala changed the format
  * Fix extraction of function type alias
  * change output for some tests as the compiler changed error reporting
  * fix a test failing because of missing parenthesis
---------

Authored-by: Mario Bucev  and Samuel Chassot

build.sbt

@@ -39,7 +39,7 @@ lazy val nTestSuiteParallelism = {
 }
 
 // The Scala version with which Stainless is compiled.
-val stainlessScalaVersion = "3.3.3"
+val stainlessScalaVersion = "3.5.0"
 // Stainless supports Scala 3.3 programs.
 val frontendDottyVersion = stainlessScalaVersion
 // The Stainless libraries use Scala 2.13 and Scala 3.3, and is compatible only with Scala 3.3.
@@ -84,7 +84,8 @@ lazy val commonSettings: Seq[Setting[_]] = artifactSettings ++ Seq(
   scalacOptions ++= Seq(
     "-deprecation",
     "-unchecked",
-    "-feature"
+    "-feature",
+    "-source:3.4-migration", "-rewrite"
   ),
 
   resolvers ++= Resolver.sonatypeOssRepos("releases"),

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

@@ -54,25 +54,25 @@ trait ComponentRun { self =>
       val transformer = new TransformerImpl(extraction.trees, extraction.trees)
       extraction.ExtractionPipeline(transformer)
     } else {
-      val transformer = otherComponents.map(_.lowering).reduceLeft(_ andThen _)
+      val transformer = otherComponents.map(_.lowering).reduceLeft(_ `andThen` _)
       extraction.ExtractionPipeline(transformer)
     }
   }
 
   /* Override point for pipeline extensions in certain components.
    * For example, the partial evaluator and measure inference pipeline in the verification component. */
-  def createPipeline: extraction.StainlessPipeline = pipeline andThen lowering
+  def createPipeline: extraction.StainlessPipeline = pipeline `andThen` lowering
 
-  private[this] final val extractionPipeline = createPipeline andThen extraction.completer(trees)
+  private final val extractionPipeline = createPipeline `andThen` extraction.completer(trees)
 
   /* Override point for filter extensions in certain components.
    * For example, the evaluating component only evaluates parameterless functions. */
   protected def createFilter: CheckFilter { val trees: self.trees.type } = CheckFilter(trees, context)
 
-  private[this] final val extractionFilter = createFilter
+  private final val extractionFilter = createFilter
 
   /** Sends the symbols through the extraction pipeline. */
-  def extract(symbols: xt.Symbols): (trees.Symbols, ExtractionSummary) = 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 {

core/src/main/scala/stainless/Configuration.scala

@@ -46,9 +46,9 @@ object Configuration {
     RecursiveFileFinder.find(isConfigFile)
   }
 
-  val empty: Seq[OptionValue[_]] = Seq.empty
+  val empty: Seq[OptionValue[?]] = Seq.empty
 
-  def get(options: Options, keys: Seq[inox.OptionDef[_]])(using Reporter): Seq[OptionValue[_]] = {
+  def get(options: Options, keys: Seq[inox.OptionDef[?]])(using Reporter): Seq[OptionValue[?]] = {
     import OptionOrDefault._
     options.findOptionOrDefault(optConfigFile) match {
       case Some(file) => parse(file, keys)
@@ -57,13 +57,13 @@ object Configuration {
     }
   }
 
-  def parseDefault(options: Seq[OptionDef[_]])(using Reporter): Seq[OptionValue[_]] = {
+  def parseDefault(options: Seq[OptionDef[?]])(using Reporter): Seq[OptionValue[?]] = {
     findConfigFile() map { file =>
       parse(file, options)
     } getOrElse Seq.empty
   }
 
-  def parse(file: File, options: Seq[OptionDef[_]])(using reporter: Reporter): Seq[OptionValue[_]] = try {
+  def parse(file: File, options: Seq[OptionDef[?]])(using reporter: Reporter): Seq[OptionValue[?]] = try {
     if (!file.exists()) {
       reporter.fatalError(s"Configuration file does not exists: ${file.getAbsolutePath}")
     }

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

@@ -27,7 +27,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
     override def toString: String = "Equivalence checking"
   }
 
-  override protected def getOptions: Map[inox.OptionDef[_], Description] = super.getOptions - inox.solvers.optAssumeChecked ++ Map(
+  override protected def getOptions: Map[inox.OptionDef[?], Description] = super.getOptions - inox.solvers.optAssumeChecked ++ Map(
     optVersion -> Description(General, "Display the version number"),
     optConfigFile -> Description(General, "Path to configuration file, set to false to disable (default: stainless.conf or .stainless.conf)"),
     optFunctions -> Description(General, "Only consider functions f1,f2,..."),
@@ -151,7 +151,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
   protected def newReporter(debugSections: Set[inox.DebugSection]): inox.Reporter =
     new stainless.DefaultReporter(debugSections)
 
-  def getConfigOptions(options: inox.Options)(using inox.Reporter): Seq[inox.OptionValue[_]] = {
+  def getConfigOptions(options: inox.Options)(using inox.Reporter): Seq[inox.OptionValue[?]] = {
     Configuration.get(options, self.options.keys.toSeq)
   }
 
@@ -165,7 +165,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
   }
 
   override
-  protected def processOptions(files: Seq[File], cmdOptions: Seq[inox.OptionValue[_]])
+  protected def processOptions(files: Seq[File], cmdOptions: Seq[inox.OptionValue[?]])
                               (using inox.Reporter): inox.Context = {
     val configOptions = getConfigOptions(inox.Options(cmdOptions))
 
@@ -275,7 +275,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
   }
 
   /** Exports the reports to the given file in JSON format. */
-  private def exportJson(report: Option[AbstractReport[_]], file: String): Unit = {
+  private def exportJson(report: Option[AbstractReport[?]], file: String): Unit = {
     val json = Json.fromFields(report map { r => (r.name -> r.emitJson) })
     JsonUtils.writeFile(new File(file), json)
   }

core/src/main/scala/stainless/ast/Deconstructors.scala

@@ -28,7 +28,7 @@ trait TreeDeconstructor extends inox.ast.TreeDeconstructor {
       })
     case s.LiteralPattern(binder, lit) =>
       (Seq(), binder.map(_.toVariable).toSeq, Seq(lit), Seq(), Seq(), (_, vs, es, _, _) => {
-        t.LiteralPattern(vs.headOption.map(_.toVal), es.head.asInstanceOf[t.Literal[_]])
+        t.LiteralPattern(vs.headOption.map(_.toVal), es.head.asInstanceOf[t.Literal[?]])
       })
     case s.UnapplyPattern(binder, recs, id, tps, subs) =>
       (Seq(id), binder.map(_.toVariable).toSeq, recs, tps, subs, (ids, vs, es, tps, pats) => {

core/src/main/scala/stainless/ast/Expressions.scala

@@ -304,7 +304,7 @@ trait Expressions extends inox.ast.Expressions with Types { self: Trees =>
       }
     }
 
-    def manyJoin(exprs: Seq[Expr]): Expr = many(exprs: _*)
+    def manyJoin(exprs: Seq[Expr]): Expr = many(exprs*)
 
     def unapply(expr: Expr): Option[Seq[Expr]] = expr match {
       case Annotated(And(exprs), flags) if flags.contains(SplitVC) => Some(exprs.toSeq)

core/src/main/scala/stainless/ast/Printers.scala

@@ -65,7 +65,7 @@ trait Printer extends inox.ast.Printer {
     case Ensuring(body, post) =>
       p"""|{
           |  $body
-          |} ensuring {
+          |}.ensuring {
           |  $post
           |}"""
 

core/src/main/scala/stainless/ast/SymbolOps.scala

@@ -30,7 +30,7 @@ trait SymbolOps extends inox.ast.SymbolOps with TypeOps { self =>
     override val t: self.trees.type,
     val symbols: self.symbols.type
   )(using PathProvider[P]) extends TransformerWithPC[P](s, t) {
-    self0: TransformerWithExprOp with TransformerWithTypeOp =>
+    self0: TransformerWithExprOp & TransformerWithTypeOp =>
   }
 
   override protected def transformerWithPC[P <: PathLike[P]](
@@ -67,7 +67,7 @@ trait SymbolOps extends inox.ast.SymbolOps with TypeOps { self =>
       if (!includeBinders) {
         pp.empty
       } else {
-        ob.map(vd => pp.empty withBinding (vd -> to)).getOrElse(pp.empty)
+        ob.map(vd => pp.empty `withBinding` (vd -> to)).getOrElse(pp.empty)
       }
     }
 
@@ -80,20 +80,20 @@ trait SymbolOps extends inox.ast.SymbolOps with TypeOps { self =>
         assert(tcons.fields.size == subps.size)
         val pairs = tcons.fields zip subps
         val subTests = pairs.map(p => apply(Annotated(adtSelector(in, p._1.id), Seq(DropVCs)).copiedFrom(p._1), p._2))
-        pp.empty withCond isCons(in, id) merge bind(ob, in) merge subTests
+        pp.empty `withCond` isCons(in, id) `merge` bind(ob, in) `merge` subTests
 
       case TuplePattern(ob, subps) =>
         val TupleType(tpes) = in.getType: @unchecked
         assert(tpes.size == subps.size)
         val subTests = subps.zipWithIndex.map { case (p, i) => apply(tupleSelect(in, i+1, subps.size), p) }
-        bind(ob, in) merge subTests
+        bind(ob, in) `merge` subTests
 
       case up @ UnapplyPattern(ob, _, _, _, subps) =>
-        val subs = unwrapTuple(up.get(in), subps.size).zip(subps) map (apply _).tupled
-        bind(ob, in) withCond Not(up.isEmpty(in)) merge subs
+        val subs = unwrapTuple(up.get(in), subps.size).zip(subps) map (apply).tupled
+        bind(ob, in) `withCond` Not(up.isEmpty(in)) `merge` subs
 
       case LiteralPattern(ob, lit) =>
-        pp.empty withCond Equals(in, lit) merge bind(ob, in)
+        pp.empty `withCond` Equals(in, lit) `merge` bind(ob, in)
     }
   }
 
@@ -169,7 +169,7 @@ trait SymbolOps extends inox.ast.SymbolOps with TypeOps { self =>
           val map = mapForPattern(scrutV, cse.pattern)
           val patCond = conditionForPattern[Path](scrutV, cse.pattern, includeBinders = false)
           val realCond = cse.optGuard match {
-            case Some(g) => patCond withCond replaceFromSymbols(map, g)
+            case Some(g) => patCond `withCond` replaceFromSymbols(map, g)
             case None => patCond
           }
           val newRhs = replaceFromSymbols(map, cse.rhs)
@@ -214,12 +214,12 @@ trait SymbolOps extends inox.ast.SymbolOps with TypeOps { self =>
     for (c <- cases) yield {
       val g = c.optGuard getOrElse BooleanLiteral(true)
       val cond = conditionForPattern[P](scrut, c.pattern, includeBinders = true)
-      val localCond = pcSoFar merge (cond withCond g)
+      val localCond = pcSoFar `merge` (cond `withCond` g)
 
       // These contain no binders defined in this MatchCase
       val condSafe = conditionForPattern[P](scrut, c.pattern)
       val gSafe = replaceFromSymbols(mapForPattern(scrut, c.pattern), g)
-      pcSoFar = pcSoFar merge (condSafe withCond gSafe).negate
+      pcSoFar = pcSoFar `merge` (condSafe `withCond` gSafe).negate
 
       localCond
     }
@@ -234,7 +234,7 @@ trait SymbolOps extends inox.ast.SymbolOps with TypeOps { self =>
       case Some(g) =>
         // guard might refer to binders
         val map  = mapForPattern(scrut, c.pattern)
-        patternC withCond replaceFromSymbols(map, g)
+        patternC `withCond` replaceFromSymbols(map, g)
 
       case None =>
         patternC

core/src/main/scala/stainless/codegen/CodeGeneration.scala

@@ -119,8 +119,8 @@ trait CodeGeneration { self: CompilationUnit =>
   def defConsToJVMName(cons: ADTConstructor): String = defToJVMName(cons.id)
   def defFnToJVMName(fd: FunDef): String = defToJVMName(fd.id)
 
-  private[this] val sortClassFiles : MutableMap[ADTSort, ClassFile] = MutableMap.empty
-  private[this] val classToSort    : MutableMap[String, ADTSort]    = MutableMap.empty
+  private val sortClassFiles : MutableMap[ADTSort, ClassFile] = MutableMap.empty
+  private val classToSort    : MutableMap[String, ADTSort]    = MutableMap.empty
 
   def getClassSort(sort: ADTSort): ClassFile = synchronized(sortClassFiles.getOrElse(sort, {
     val cf = new ClassFile(defSortToJVMName(sort), None)
@@ -129,8 +129,8 @@ trait CodeGeneration { self: CompilationUnit =>
     cf
   }))
 
-  private[this] val consClassFiles : MutableMap[ADTConstructor, ClassFile] = MutableMap.empty
-  private[this] val classToCons    : MutableMap[String, ADTConstructor]    = MutableMap.empty
+  private val consClassFiles : MutableMap[ADTConstructor, ClassFile] = MutableMap.empty
+  private val classToCons    : MutableMap[String, ADTConstructor]    = MutableMap.empty
 
   def getClassCons(cons: ADTConstructor): ClassFile = synchronized(consClassFiles.getOrElse(cons, {
     val cf = new ClassFile(defConsToJVMName(cons), Some(defSortToJVMName(cons.getSort)))
@@ -139,7 +139,7 @@ trait CodeGeneration { self: CompilationUnit =>
     cf
   }))
 
-  private[this] lazy val static = new ClassFile("<static>", None)
+  private lazy val static = new ClassFile("<static>", None)
 
   protected def compile(): Seq[ClassFile] = {
     for (sort <- sorts.values) {
@@ -157,8 +157,8 @@ trait CodeGeneration { self: CompilationUnit =>
   protected def jvmClassNameToSort(className: String): Option[ADTSort] = classToSort.get(className)
   protected def jvmClassNameToCons(className: String): Option[ADTConstructor] = classToCons.get(className)
 
-  private[this] val sortInfos: ConcurrentMap[ADTSort, (String, String)] = ConcurrentMap.empty
-  private[this] val consInfos: ConcurrentMap[ADTConstructor, (String, String)] = ConcurrentMap.empty
+  private val sortInfos: ConcurrentMap[ADTSort, (String, String)] = ConcurrentMap.empty
+  private val consInfos: ConcurrentMap[ADTConstructor, (String, String)] = ConcurrentMap.empty
 
   protected def getSortInfo(sort: ADTSort): (String, String) = sortInfos.getOrElse(sort, {
     val tpeParam = if (sort.tparams.isEmpty) "" else "[I"
@@ -175,7 +175,7 @@ trait CodeGeneration { self: CompilationUnit =>
     res
   })
 
-  private[this] val funDefInfos: ConcurrentMap[FunDef, (String, String, String)] = ConcurrentMap.empty
+  private val funDefInfos: ConcurrentMap[FunDef, (String, String, String)] = ConcurrentMap.empty
 
   protected def getFunDefInfo(fd: FunDef): (String, String, String) = funDefInfos.getOrElse(fd, {
     val sig = "(L"+MonitorClass+";" +
@@ -276,7 +276,7 @@ trait CodeGeneration { self: CompilationUnit =>
     val m = cf.addMethod(
       typeToJVM(funDef.getType),
       mn,
-      realParams : _*
+      realParams*
     )
 
     m.setFlags((
@@ -344,7 +344,7 @@ trait CodeGeneration { self: CompilationUnit =>
     ch.freeze
   }
 
-  private[this] val lambdaClasses = new Bijection[Lambda, String]
+  private val lambdaClasses = new Bijection[Lambda, String]
 
   protected def jvmClassNameToLambda(className: String): Option[Lambda] = lambdaClasses.getA(className)
 
@@ -1807,7 +1807,7 @@ trait CodeGeneration { self: CompilationUnit =>
         constrParams.map(_._1).zipWithIndex.toMap.view.mapValues(_ + 1).toMap
       }
 
-      val cch = cf.addConstructor(constrParams.map(_._2) : _*).codeHandler
+      val cch = cf.addConstructor(constrParams.map(_._2)*).codeHandler
 
       // Call parent constructor
       cch << ALoad(0)
@@ -1897,7 +1897,7 @@ trait CodeGeneration { self: CompilationUnit =>
         fh.setFlags(FIELD_ACC_PUBLIC)
       }
 
-      val cch = cf.addConstructor(constructorArgs.map(_._2) : _*).codeHandler
+      val cch = cf.addConstructor(constructorArgs.map(_._2)*).codeHandler
 
       if (doInstrument) {
         cch << ALoad(0)

core/src/main/scala/stainless/codegen/CompilationUnit.scala

@@ -38,7 +38,7 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val
 
     def evalToJVM(args: Seq[AnyRef], monitor: Monitor): AnyRef = {
       val allArgs = monitor +: args
-      meth.invoke(null, allArgs.toArray : _*)
+      meth.invoke(null, allArgs.toArray*)
     }
 
     def evalFromJVM(args: Seq[AnyRef], monitor: Monitor): Expr = {
@@ -58,10 +58,10 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val
     }
   }
 
-  private[this] val runtimeCounter = new UniqueCounter[Unit]
+  private val runtimeCounter = new UniqueCounter[Unit]
 
-  private[this] var runtimeTypeToIdMap = Map[Type, Int]()
-  private[this] var runtimeIdToTypeMap = Map[Int, Type]()
+  private var runtimeTypeToIdMap = Map[Type, Int]()
+  private var runtimeIdToTypeMap = Map[Int, Type]()
   protected def getType(id: Int): Type = synchronized(runtimeIdToTypeMap(id))
   protected def registerType(tpe: Type): Int = synchronized(runtimeTypeToIdMap.get(tpe) match {
     case Some(id) => id
@@ -72,15 +72,15 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val
       id
   })
 
-  private[this] var runtimeChooseMap = Map[Int, (Seq[ValDef], Seq[TypeParameter], Choose)]()
+  private var runtimeChooseMap = Map[Int, (Seq[ValDef], Seq[TypeParameter], Choose)]()
   protected def getChoose(id: Int): (Seq[ValDef], Seq[TypeParameter], Choose) = synchronized(runtimeChooseMap(id))
   protected def registerChoose(c: Choose, params: Seq[ValDef], tps: Seq[TypeParameter]): Int = synchronized {
     val id = runtimeCounter.nextGlobal
     runtimeChooseMap += id -> (params, tps, c)
     id
   }
 
-  private[this] var runtimeForallMap = Map[Int, (Seq[TypeParameter], Forall)]()
+  private var runtimeForallMap = Map[Int, (Seq[TypeParameter], Forall)]()
   protected def getForall(id: Int): (Seq[TypeParameter], Forall) = synchronized(runtimeForallMap(id))
   protected def registerForall(f: Forall, tps: Seq[TypeParameter]): Int = synchronized {
     val id = runtimeCounter.nextGlobal
@@ -89,9 +89,9 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val
   }
 
   // Get the Java constructor corresponding to the Case class
-  private[this] val adtConstructors: MutableMap[ADTConstructor, Constructor[_]] = MutableMap.empty
+  private val adtConstructors: MutableMap[ADTConstructor, Constructor[?]] = MutableMap.empty
 
-  private[this] def adtConstructor(cons: ADTConstructor): Constructor[_] =
+  private def adtConstructor(cons: ADTConstructor): Constructor[?] =
     adtConstructors.getOrElse(cons, {
       val cf = getClassCons(cons)
       val klass = loader.loadClass(cf.className)
@@ -103,7 +103,7 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val
       res
     })
 
-  private[this] lazy val tupleConstructor: Constructor[_] = {
+  private lazy val tupleConstructor: Constructor[?] = {
     val tc = loader.loadClass("stainless.codegen.runtime.Tuple")
     val conss = tc.getConstructors.sortBy(_.getParameterTypes.length)
     assert(conss.nonEmpty)
@@ -152,7 +152,7 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val
       try {
         val tpeParam = if (tps.isEmpty) Seq() else Seq(tps.map(registerType).toArray)
         val jvmArgs = monitor +: (tpeParam ++ args.map(valueToJVM))
-        cons.newInstance(jvmArgs.toArray : _*).asInstanceOf[AnyRef]
+        cons.newInstance(jvmArgs.toArray*).asInstanceOf[AnyRef]
       } catch {
         case e : java.lang.reflect.InvocationTargetException => throw e.getCause
       }
@@ -199,7 +199,7 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val
         val conss = lc.getConstructors.sortBy(_.getParameterTypes.length)
         assert(conss.nonEmpty)
         val lambdaConstructor = conss.last
-        lambdaConstructor.newInstance(args.toArray : _*).asInstanceOf[AnyRef]
+        lambdaConstructor.newInstance(args.toArray*).asInstanceOf[AnyRef]
       } else {
         compileExpression(lambda, Seq.empty).evalToJVM(Seq.empty, monitor)
       }
@@ -429,7 +429,7 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val
     val m = cf.addMethod(
       typeToJVM(e.getType),
       "eval",
-      realArgs : _*
+      realArgs*
     )
 
     m.setFlags((