Upgrade to Scala 3.2 (#1317)

.larabot.conf

@@ -1,13 +1,13 @@
 commands = [
-    "sbt -batch -Dparallel=5 test"
-    "sbt -batch -Dparallel=5 \"it:testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.TypeCheckerLibrarySuite stainless.ScalacExtractionSuite stainless.LibrarySuite stainless.verification.SMTZ3TypeCheckerSuite stainless.verification.SMTZ3VerificationSuite stainless.verification.SMTZ3UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.verification.CodeGenVerificationSuite stainless.verification.SMTCVC4TypeCheckerSuite stainless.verification.SMTCVC4VerificationSuite stainless.verificatoin.SMTCVC4UncheckedSuite stainless.termination.TerminationSuite\""
+    "sbt -batch -Dtest-parallelism=5 test"
+    "sbt -batch -Dtest-parallelism=5 \"it:testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.TypeCheckerLibrarySuite stainless.ScalacExtractionSuite stainless.LibrarySuite stainless.verification.SMTZ3TypeCheckerSuite stainless.verification.SMTZ3VerificationSuite stainless.verification.SMTZ3UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.verification.CodeGenVerificationSuite stainless.verification.SMTCVC4TypeCheckerSuite stainless.verification.SMTCVC4VerificationSuite stainless.verificatoin.SMTCVC4UncheckedSuite stainless.termination.TerminationSuite\""
 ]
 
 nightly {
   commands = [
     "sbt universal:stage"
-    "sbt -batch -Dparallel=5 test"
-    "sbt -batch -Dparallel=5 it:test"
+    "sbt -batch -Dtest-parallelism=5 test"
+    "sbt -batch -Dtest-parallelism=5 it:test"
     "bash bin/external-tests.sh --only-scalac"
     "bash bin/external-tests.sh --only-dotty"
     "sbt -batch scripted"

build.sbt

@@ -22,8 +22,8 @@ val osArch = System.getProperty("sun.arch.data.model")
 
 val circeVersion = "0.14.1"
 
-lazy val nParallel = {
-  val p = System.getProperty("parallel")
+lazy val nTestParallelism = {
+  val p = System.getProperty("test-parallelism")
   if (p ne null) {
     try {
       p.toInt
@@ -36,7 +36,7 @@ lazy val nParallel = {
 }
 
 // The Scala version with which Stainless is compiled.
-val stainlessScalaVersion = "3.0.2"
+val stainlessScalaVersion = "3.2.0"
 // Stainless supports Scala 2.13 and Scala 3.0 programs.
 val frontendScalacVersion = "2.13.6"
 val frontendDottyVersion = stainlessScalaVersion
@@ -115,8 +115,6 @@ lazy val commonSettings: Seq[Setting[_]] = artifactSettings ++ Seq(
   // disable documentation packaging in universal:stage to speedup development
   Compile / packageDoc / mappings := Seq(),
 
-  Global / concurrentRestrictions += Tags.limitAll(nParallel),
-
   Compile / sourcesInBase := false,
 
   run / Keys.fork := true,
@@ -146,8 +144,6 @@ lazy val stainlessLibSettings: Seq[Setting[_]] = artifactSettings ++ Seq(
   // disable documentation packaging in universal:stage to speedup development
   Compile / packageDoc / mappings := Seq(),
 
-  Global / concurrentRestrictions += Tags.limitAll(nParallel),
-
   Compile / sourcesInBase := false,
 
   run / Keys.fork := true,
@@ -260,10 +256,14 @@ def commonFrontendSettings(compilerVersion: String): Seq[Setting[_]] = Defaults.
     Seq(main)
   }) ++
   inConfig(IntegrationTest)(Defaults.testTasks ++ Seq(
-    logBuffered := (nParallel > 1),
-    parallelExecution := (nParallel > 1)
+    logBuffered := (nTestParallelism > 1),
+    parallelExecution := (nTestParallelism > 1),
   ))
 
+Global / concurrentRestrictions := Seq(
+  Tags.limit(Tags.Test, nTestParallelism)
+)
+
 val scriptSettings: Seq[Setting[_]] = Seq(
   extraClasspath := {
     ((Compile / classDirectory).value.getAbsolutePath +: (Compile / dependencyClasspath).value.map(_.data.absolutePath))
@@ -275,7 +275,7 @@ val scriptSettings: Seq[Setting[_]] = Seq(
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 
 // lazy val inox = RootProject(file("../inox"))
-lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "1c8c0bac611ad4edc2c5b209deea9c75359d51b1")
+lazy val inox = ghProject("https://github.com/epfl-lara/inox.git", "1499384f950d7b0202c1303c00e8cdd1bcb6ca45")
 lazy val cafebabe = ghProject("https://github.com/epfl-lara/cafebabe.git", "616e639b34379e12b8ac202849de3ebbbd0848bc")
 
 // Allow integration test to use facilities from regular tests

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

@@ -123,10 +123,10 @@ trait TreeDeconstructor extends inox.ast.TreeDeconstructor {
           rtps = nextTps
 
           if (hasGuard) {
-            val guard +: rhs +: pes = currEs
+            val guard +: rhs +: pes = currEs: @unchecked
             t.MatchCase(precons(currIds, currVs, pes, currTps).setPos(patternPos), Some(guard), rhs).setPos(cazePos)
           } else {
-            val rhs +: pes = currEs
+            val rhs +: pes = currEs: @unchecked
             t.MatchCase(precons(currIds, currVs, pes, currTps).setPos(patternPos), None, rhs).setPos(cazePos)
           }
         }
@@ -153,14 +153,14 @@ trait TreeDeconstructor extends inox.ast.TreeDeconstructor {
     case s.MatchExpr(scrut, cases) =>
       val (cids, cvs, ces, ctps, crecons) = deconstructCases(cases)
       (cids, cvs, scrut +: ces, ctps, Seq(), (ids, vs, es, tps, _) => {
-        val newScrut +: nes = es
+        val newScrut +: nes = es: @unchecked
         t.MatchExpr(newScrut, crecons(ids, vs, nes, tps))
       })
 
     case s.Passes(in, out, cases) =>
       val (cids, cvs, ces, ctps, crecons) = deconstructCases(cases)
       (cids, cvs, Seq(in, out) ++ ces, ctps, Seq(), (ids, vs, es, tps, _) => {
-        val newIn +: newOut +: nes = es
+        val newIn +: newOut +: nes = es: @unchecked
         t.Passes(newIn, newOut, crecons(ids, vs, nes, tps))
       })
 

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

@@ -83,7 +83,7 @@ trait SymbolOps extends inox.ast.SymbolOps with TypeOps { self =>
         pp.empty withCond isCons(in, id) merge bind(ob, in) merge subTests
 
       case TuplePattern(ob, subps) =>
-        val TupleType(tpes) = in.getType
+        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
@@ -139,7 +139,7 @@ trait SymbolOps extends inox.ast.SymbolOps with TypeOps { self =>
         bindIn(b) ++ together
 
       case TuplePattern(b, subps) =>
-        val TupleType(tpes) = in.getType
+        val TupleType(tpes) = in.getType: @unchecked
         assert(tpes.size == subps.size)
 
         val maps = subps.zipWithIndex.map { case (p, i) => mapForPattern(tupleSelect(in, i+1, subps.size), p)}
@@ -177,7 +177,7 @@ trait SymbolOps extends inox.ast.SymbolOps with TypeOps { self =>
         }
 
         val (branches, elze) = if (assumeExhaustive) {
-          val (cases :+ ((_, rhs, _))) = condsAndRhs
+          val (cases :+ ((_, rhs, _))) = condsAndRhs: @unchecked
           (cases, rhs)
         } else {
           (condsAndRhs, Error(m.getType, "match exhaustiveness").copiedFrom(m))

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

@@ -745,7 +745,7 @@ trait CodeGeneration { self: CompilationUnit =>
     case Tuple(es) => mkTuple(es, ch)
 
     case TupleSelect(t, i) =>
-      val TupleType(bs) = t.getType
+      val TupleType(bs) = t.getType: @unchecked
       mkExpr(t,ch)
       ch << Ldc(i - 1)
       ch << InvokeVirtual(TupleClass, "get", s"(I)L$ObjectClass;")
@@ -838,7 +838,7 @@ trait CodeGeneration { self: CompilationUnit =>
       }
 
     case MapApply(m, k) =>
-      val MapType(_, tt) = m.getType
+      val MapType(_, tt) = m.getType: @unchecked
       mkExpr(m, ch)
       mkBoxedExpr(k, ch)
       ch << InvokeVirtual(MapClass, "get", s"(L$ObjectClass;)L$ObjectClass;")
@@ -1249,7 +1249,7 @@ trait CodeGeneration { self: CompilationUnit =>
     val (l: Lambda, deps) = normalizeStructure(matchToIfThenElse(
       replaceFromSymbols((vars zip freshVars).toMap, lambda),
       assumeExhaustive = false
-    ))
+    )): @unchecked
 
     val (afName, closures, tparams, consSig) = compileLambda(l, locals.params)
     val closureTypes = variablesOf(l).map(v => v.id -> v.getType).toMap
@@ -1562,8 +1562,8 @@ trait CodeGeneration { self: CompilationUnit =>
       case BVType(_, s) => ch << NOP
     }
 
-    val BVType(_, oldSize) = from
-    val BVType(_, newSize) = to
+    val BVType(_, oldSize) = from: @unchecked
+    val BVType(_, newSize) = to: @unchecked
     ch << Comment(s"Applying BVCast on BitVector instance: $oldSize -> $newSize")
     ch << Ldc(newSize)
     ch << InvokeVirtual(BitVectorClass, "cast", s"(I)L$BitVectorClass;")

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

@@ -184,7 +184,7 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val
       m
 
     case lambda: Lambda =>
-      val (l: Lambda, deps) = normalizeStructure(matchToIfThenElse(lambda, assumeExhaustive = false))
+      val (l: Lambda, deps) = normalizeStructure(matchToIfThenElse(lambda, assumeExhaustive = false)): @unchecked
       if (deps.forall { case (_, e, conds) => isValue(e) && conds.isEmpty }) {
         val (afName, closures, tparams, consSig) = compileLambda(l, Seq.empty)
         val depsMap = deps.map { case (v, dep, _) => v.id -> valueToJVM(dep) }.toMap
@@ -254,7 +254,7 @@ class CompilationUnit(val program: Program, val context: inox.Context)(using val
           arr
         }
 
-        val ArrayType(underlying) = a.getType
+        val ArrayType(underlying) = a.getType: @unchecked
         underlying match {
           case Int8Type() =>
             allocArray { case Int8Literal(v) => v }

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

@@ -126,12 +126,12 @@ class CodeGenEvaluator(override val program: Program,
 
       val groundForall = exprOps.replaceFromSymbols(inputsMap, tpForall)
 
-      val BooleanLiteral(res) = try {
+      val BooleanLiteral(res) = (try {
         self.onForallInvocation(groundForall.asInstanceOf[Forall])
       } catch {
         case e: java.lang.RuntimeException =>
           throw new runtime.CodeGenRuntimeException(e.getMessage)
-      }
+      }): @unchecked
 
       res
     }

core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala

@@ -609,7 +609,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
             Ensuring(transform(body, env), Lambda(params, transform(post, env)).copiedFrom(l)).copiedFrom(e)
 
           case l @ Lambda(params, body) =>
-            val ft @ FunctionType(_, _) = l.getType
+            val ft @ FunctionType(_, _) = l.getType: @unchecked
             val ownEffects = functionTypeEffects(ft)
             val aliasedParams: Seq[ValDef] = params.zipWithIndex.flatMap {
               case (vd, i) if ownEffects.contains(i) => Some(vd)
@@ -674,7 +674,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
           case app @ Application(callee, args) =>
             checkAliasing(app, args, env)
 
-            val ft @ FunctionType(from, to) = callee.getType
+            val ft @ FunctionType(from, to) = callee.getType: @unchecked
             val ftEffects = functionTypeEffects(ft)
             if (ftEffects.nonEmpty) {
               val nfi = Application(
@@ -754,7 +754,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
     def updatedTarget(target: Target, newValue: Expr): Expr = {
       def rec(receiver: Expr, path: Seq[Accessor]): Expr = path match {
         case ADTFieldAccessor(id) :: fs =>
-          val adt @ ADTType(_, tps) = receiver.getType
+          val adt @ ADTType(_, tps) = receiver.getType: @unchecked
           val tcons = adt.getSort.constructors.find(_.fields.exists(_.id == id)).get
           val r = rec(Annotated(ADTSelector(receiver, id).copiedFrom(newValue), Seq(DropVCs)).copiedFrom(newValue), fs)
 
@@ -785,7 +785,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
           }).copiedFrom(newValue)
 
         case TupleFieldAccessor(index) :: fs =>
-          val tt @ TupleType(_) = receiver.getType
+          val tt @ TupleType(_) = receiver.getType: @unchecked
           val r = rec(Annotated(TupleSelect(receiver, index).copiedFrom(newValue), Seq(DropVCs)).copiedFrom(newValue), fs)
 
           Tuple((1 to tt.dimension).map { i =>
@@ -1142,7 +1142,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
 
         case _: (And | Or | Implies | Not) =>
           // Similar to if-then-else, we may not hoist expression out of these expressions (in particular && || and ==> are short-circuiting)
-          val Operator(args, recons) = e
+          val Operator(args, recons) = e: @unchecked
           (identity, recons(args.map(normalize)).copiedFrom(e))
 
         case Operator(args, recons) =>
@@ -1276,7 +1276,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
       def normalizeCall(call: Application | FunctionInvocation | ApplyLetRec): (Expr => Expr, Expr) = {
         val (ft, args, ctxCallee: (Expr => Expr), recons: (Seq[Expr] => Expr)) = call match {
           case app @ Application(callee, args) =>
-            val ft @ FunctionType(_, _) = callee.getType
+            val ft @ FunctionType(_, _) = callee.getType: @unchecked
             val (ctxCallee, normCallee) = doNormalize(callee)
             val recons: Seq[Expr] => Expr = Application(normCallee, _).copiedFrom(app)
             (ft, args, ctxCallee, recons)
@@ -1297,7 +1297,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
       // as the set of targets for immutable types is empty.
       def selectionNeedsNorm(e: ClassSelector | TupleSelect | ADTSelector): Boolean = e match {
         case ClassSelector(recv, sel) =>
-          val ct @ ClassType(_, _) = recv.getType
+          val ct @ ClassType(_, _) = recv.getType: @unchecked
           isMutableType(e.getType) || ct.getField(sel).get.flags.contains(IsVar)
         case TupleSelect(_, _) =>
           isMutableType(e.getType)

core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala

@@ -756,7 +756,7 @@ trait EffectsAnalyzer extends oo.CachingPhase {
   def isReferentiallyTransparent(e: Expr)(using syms: Symbols): Boolean = e match {
     case Variable(_, tpe, flags) => !flags.contains(IsVar) && !syms.isMutableType(tpe)
     case ClassSelector(expr, field) =>
-      val c @ ClassType(_, _) = expr.getType
+      val c @ ClassType(_, _) = expr.getType: @unchecked
       !c.getField(field).get.flags.contains(IsVar) && isReferentiallyTransparent(expr)
     case _: (ArraySelect | MutableMapApply) => false
     case _: (Literal[t] | Lambda) => true
@@ -840,7 +840,7 @@ trait EffectsAnalyzer extends oo.CachingPhase {
         rec(o, env) ++ rec(v, env) ++ effect(o, env).map(_.precise(accessor))
 
       case Application(callee, args) =>
-        val ft @ FunctionType(_, _) = callee.getType
+        val ft @ FunctionType(_, _) = callee.getType: @unchecked
         val effects = functionTypeEffects(ft)
         rec(callee, env) ++ args.flatMap(rec(_, env)) ++
         args.map(effect(_, env)).zipWithIndex

core/src/main/scala/stainless/extraction/imperative/ImperativeCodeElimination.scala

@@ -44,7 +44,7 @@ class ImperativeCodeElimination(override val s: Trees)(override val t: s.type)
     def toFunction(expr: Expr)(using state: State): (Expr, Expr => Expr, Map[Variable, Variable]) = {
       import state._
 
-      val (res, scope, fun): (Expr, Expr => Expr, Map[Variable, Variable]) = expr match {
+      val (res, scope, fun): (Expr, Expr => Expr, Map[Variable, Variable]) = (expr match {
         case LetVar(vd, e, b) =>
           val newVd = vd.freshen
           val (rhsVal, rhsScope, rhsFun) = toFunction(e)
@@ -400,7 +400,7 @@ class ImperativeCodeElimination(override val s: Trees)(override val t: s.type)
             (argVal +: accArgs, newScope, argFun ++ accFun)
           }
           (recons(recArgs).setPos(n), scope, fun)
-      }
+      }): @unchecked
 
       (res.ensurePos(expr.getPos), scope, fun)
     }

core/src/main/scala/stainless/extraction/imperative/TransformerWithType.scala

@@ -37,15 +37,15 @@ trait TransformerWithType extends oo.TransformerWithType {
       ).copiedFrom(expr)
 
     case s.ArrayUpdate(array, index, value) =>
-      val at @ s.ArrayType(base) = widen(array.getType)
+      val at @ s.ArrayType(base) = widen(array.getType): @unchecked
       t.ArrayUpdate(
         transform(array, at),
         transform(index, s.Int32Type()),
         transform(value, base)
       ).copiedFrom(expr)
 
     case s.Swap(array1, index1, array2, index2) =>
-      val at @ s.ArrayType(base) = widen(array1.getType)
+      val at @ s.ArrayType(base) = widen(array1.getType): @unchecked
       t.Swap(
         transform(array1, at),
         transform(index1, s.Int32Type()),
@@ -59,19 +59,19 @@ trait TransformerWithType extends oo.TransformerWithType {
       )
 
     case s.MutableMapApply(map, index) =>
-      val mmt @ s.MutableMapType(from, to) = widen(map.getType)
+      val mmt @ s.MutableMapType(from, to) = widen(map.getType): @unchecked
       t.MutableMapApply(transform(map, mmt), transform(index, from)).copiedFrom(expr)
 
     case s.MutableMapUpdate(map, key, value) =>
-      val mmt @ s.MutableMapType(from, to) = widen(map.getType)
+      val mmt @ s.MutableMapType(from, to) = widen(map.getType): @unchecked
       t.MutableMapUpdate(transform(map, mmt), transform(key, from), transform(value, to)).copiedFrom(expr)
 
     case s.MutableMapUpdated(map, key, value) =>
-      val mmt @ s.MutableMapType(from, to) = widen(map.getType)
+      val mmt @ s.MutableMapType(from, to) = widen(map.getType): @unchecked
       t.MutableMapUpdated(transform(map, mmt), transform(key, from), transform(value, to)).copiedFrom(expr)
 
     case s.MutableMapDuplicate(map) =>
-      val mmt @ s.MutableMapType(from, to) = widen(map.getType)
+      val mmt @ s.MutableMapType(from, to) = widen(map.getType): @unchecked
       t.MutableMapDuplicate(transform(map, mmt)).copiedFrom(expr)
 
     case s.Old(e) =>

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

@@ -632,7 +632,7 @@ class ExprOps(override val trees: Trees) extends oo.ExprOps(trees) { self =>
     def rec(e: Expr): Expr = subst.get(e) match {
       case Some(img) => img
       case None =>
-        val Operator(es, recons) = e
+        val Operator(es, recons) = e: @unchecked
         val newEs = es.map(rec)
         if ((es zip newEs) exists (p => p._1 ne p._2)) {
           recons(newEs).copiedFrom(e)

core/src/main/scala/stainless/extraction/innerclasses/Definitions.scala

@@ -26,7 +26,7 @@ trait Definitions extends methods.Trees { self: Trees =>
 
       val typedMap = allAncestors.groupBy(_.cd).map { case (cd, tcds) =>
         val tps = cd.typeArgs.zipWithIndex.map { case (tp, i) =>
-          val insts @ (head +: tail) = tcds.map(_.tps(i))
+          val insts @ (head +: tail) = tcds.map(_.tps(i)): @unchecked
           if (tp.isCovariant) s.greatestLowerBound(insts)
           else if (tp.isContravariant) s.leastUpperBound(insts)
           else if (tail.forall(_ == head)) head

core/src/main/scala/stainless/extraction/innerclasses/Types.scala

@@ -43,7 +43,7 @@ trait Types extends methods.Trees { self: Trees =>
         val typedMap = allAncestors.groupBy(_.id).map { case (id, cts) =>
           val tps = cts.head.typeArgs.zipWithIndex.map { case (tp, i) =>
             val preInsts = cts.map(_.tps(i))
-            val insts @ (head +: tail) = preInsts.map(i => typeOps.instantiateType(i, subst))
+            val insts @ (head +: tail) = preInsts.map(i => typeOps.instantiateType(i, subst)): @unchecked
             if (tp.isCovariant) s.greatestLowerBound(insts)
             else if (tp.isContravariant) s.leastUpperBound(insts)
             else if (tail.forall(_ == head)) head

core/src/main/scala/stainless/extraction/methods/MethodLifting.scala

@@ -289,7 +289,7 @@ class MethodLifting(override val s: Trees, override val t: oo.Trees)
       }
       (subCalls, elze)
     } else {
-      val conds :+ ((_, elze: t.Expr)) = subCalls
+      val conds :+ ((_, elze: t.Expr)) = subCalls: @unchecked
       (conds, elze)
     }
 

core/src/main/scala/stainless/extraction/methods/Sealing.scala

@@ -79,7 +79,7 @@ class Sealing(override val s: Trees)(override val t: s.type)
     }
   }
 
-  override protected def getContext(syms: Symbols) = new TransformerContext()(using syms)
+  override protected def getContext(syms: Symbols) = new TransformerContext(using syms)
 
   // For each class, we add a sealed flag, and optionally add a dummy subclass
   // with the corresponding methods