From a084aae453162b798497354e39c6096d951b5929 Mon Sep 17 00:00:00 2001 From: mario-bucev Date: Tue, 1 Nov 2022 20:12:40 +0100 Subject: [PATCH] Upgrade to Scala 3.2 (#1317) --- .larabot.conf | 8 +- build.sbt | 20 +-- .../scala/stainless/ast/Deconstructors.scala | 8 +- .../main/scala/stainless/ast/SymbolOps.scala | 6 +- .../stainless/codegen/CodeGeneration.scala | 10 +- .../stainless/codegen/CompilationUnit.scala | 4 +- .../evaluators/CodeGenEvaluator.scala | 4 +- .../extraction/imperative/AntiAliasing.scala | 14 +- .../imperative/EffectsAnalyzer.scala | 4 +- .../ImperativeCodeElimination.scala | 4 +- .../imperative/TransformerWithType.scala | 12 +- .../extraction/imperative/Trees.scala | 2 +- .../extraction/innerclasses/Definitions.scala | 2 +- .../extraction/innerclasses/Types.scala | 2 +- .../extraction/methods/MethodLifting.scala | 2 +- .../extraction/methods/Sealing.scala | 2 +- .../extraction/methods/SuperCalls.scala | 4 +- .../stainless/extraction/oo/Definitions.scala | 2 +- .../extraction/oo/TransformerWithType.scala | 20 +-- .../extraction/oo/TypeEncoding.scala | 2 +- .../termination/InductElimination.scala | 2 +- .../stainless/extraction/throwing/Trees.scala | 2 +- .../extraction/xlang/PartialFunctions.scala | 2 +- .../extraction/xlang/TreeSanitizer.scala | 4 +- .../stainless/genc/ir/Referentiator.scala | 2 +- .../scala/stainless/genc/ir/Transformer.scala | 2 +- .../genc/phases/ArraysLengthsExtraction.scala | 2 +- .../stainless/genc/phases/ExtraOps.scala | 2 +- .../stainless/genc/phases/Scala2IRPhase.scala | 8 +- .../scala/stainless/solvers/InoxEncoder.scala | 4 +- .../stainless/termination/ChainBuilder.scala | 2 +- .../termination/ChainProcessor.scala | 128 +++++++++--------- .../termination/DecreasesProcessor.scala | 2 +- .../termination/MeasureInference.scala | 2 +- .../stainless/testgen/ScalaTestGen.scala | 2 +- .../transformers/lattices/Core.scala | 32 ++--- .../verification/DefaultTactic.scala | 4 +- .../verification/VerificationChecker.scala | 36 ++--- .../verification/valid/Streams.scala | 2 +- .../frontends/dotc/CodeExtraction.scala | 4 +- .../frontends/dotc/StainlessExtraction.scala | 58 ++++---- .../library/stainless/collection/List.scala | 20 +-- frontends/library/stainless/lang/Either.scala | 2 +- .../frontends/scalac/CodeExtraction.scala | 2 +- project/build.properties | 2 +- 45 files changed, 231 insertions(+), 229 deletions(-) diff --git a/.larabot.conf b/.larabot.conf index 0922cfae1c..a34b3ba686 100644 --- a/.larabot.conf +++ b/.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" diff --git a/build.sbt b/build.sbt index 27bfd807fc..b8627c15fe 100644 --- a/build.sbt +++ b/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 diff --git a/core/src/main/scala/stainless/ast/Deconstructors.scala b/core/src/main/scala/stainless/ast/Deconstructors.scala index fe5fad1b0d..ea1a99b171 100644 --- a/core/src/main/scala/stainless/ast/Deconstructors.scala +++ b/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)) }) diff --git a/core/src/main/scala/stainless/ast/SymbolOps.scala b/core/src/main/scala/stainless/ast/SymbolOps.scala index b9854bb0c9..7353bc88ac 100644 --- a/core/src/main/scala/stainless/ast/SymbolOps.scala +++ b/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)) diff --git a/core/src/main/scala/stainless/codegen/CodeGeneration.scala b/core/src/main/scala/stainless/codegen/CodeGeneration.scala index ae3472921a..3ba0790a65 100644 --- a/core/src/main/scala/stainless/codegen/CodeGeneration.scala +++ b/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;") diff --git a/core/src/main/scala/stainless/codegen/CompilationUnit.scala b/core/src/main/scala/stainless/codegen/CompilationUnit.scala index 434f233279..c944da7866 100644 --- a/core/src/main/scala/stainless/codegen/CompilationUnit.scala +++ b/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 } diff --git a/core/src/main/scala/stainless/evaluators/CodeGenEvaluator.scala b/core/src/main/scala/stainless/evaluators/CodeGenEvaluator.scala index d97b24533e..ba1343741d 100644 --- a/core/src/main/scala/stainless/evaluators/CodeGenEvaluator.scala +++ b/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 } diff --git a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala index a787bab547..1cc09e03cd 100644 --- a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala +++ b/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) diff --git a/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala b/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala index 278cc07a66..6a4f817c59 100644 --- a/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala +++ b/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 diff --git a/core/src/main/scala/stainless/extraction/imperative/ImperativeCodeElimination.scala b/core/src/main/scala/stainless/extraction/imperative/ImperativeCodeElimination.scala index 7cdf1282c9..b16bc0b29d 100644 --- a/core/src/main/scala/stainless/extraction/imperative/ImperativeCodeElimination.scala +++ b/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) } diff --git a/core/src/main/scala/stainless/extraction/imperative/TransformerWithType.scala b/core/src/main/scala/stainless/extraction/imperative/TransformerWithType.scala index 2ae9bae1e5..05d580760f 100644 --- a/core/src/main/scala/stainless/extraction/imperative/TransformerWithType.scala +++ b/core/src/main/scala/stainless/extraction/imperative/TransformerWithType.scala @@ -37,7 +37,7 @@ 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()), @@ -45,7 +45,7 @@ trait TransformerWithType extends oo.TransformerWithType { ).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) => diff --git a/core/src/main/scala/stainless/extraction/imperative/Trees.scala b/core/src/main/scala/stainless/extraction/imperative/Trees.scala index 5893951892..0c417d219b 100644 --- a/core/src/main/scala/stainless/extraction/imperative/Trees.scala +++ b/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) diff --git a/core/src/main/scala/stainless/extraction/innerclasses/Definitions.scala b/core/src/main/scala/stainless/extraction/innerclasses/Definitions.scala index 13a9eef46e..7ffafd6e84 100644 --- a/core/src/main/scala/stainless/extraction/innerclasses/Definitions.scala +++ b/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 diff --git a/core/src/main/scala/stainless/extraction/innerclasses/Types.scala b/core/src/main/scala/stainless/extraction/innerclasses/Types.scala index a7448ec6ae..e311c1fec2 100644 --- a/core/src/main/scala/stainless/extraction/innerclasses/Types.scala +++ b/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 diff --git a/core/src/main/scala/stainless/extraction/methods/MethodLifting.scala b/core/src/main/scala/stainless/extraction/methods/MethodLifting.scala index 81b910387f..9ba16a88ec 100644 --- a/core/src/main/scala/stainless/extraction/methods/MethodLifting.scala +++ b/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) } diff --git a/core/src/main/scala/stainless/extraction/methods/Sealing.scala b/core/src/main/scala/stainless/extraction/methods/Sealing.scala index ccf9ef1d54..5ac6dbf261 100644 --- a/core/src/main/scala/stainless/extraction/methods/Sealing.scala +++ b/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 diff --git a/core/src/main/scala/stainless/extraction/methods/SuperCalls.scala b/core/src/main/scala/stainless/extraction/methods/SuperCalls.scala index 0ddb55a0af..b58dc6121c 100644 --- a/core/src/main/scala/stainless/extraction/methods/SuperCalls.scala +++ b/core/src/main/scala/stainless/extraction/methods/SuperCalls.scala @@ -93,14 +93,14 @@ class SuperCalls(override val s: Trees, override val t: Trees) override protected final val sortCache = new ExtractionCache[s.ADTSort, SortResult]({ (sort, context) => val symbols = context.symbols - val collector = new SuperCollector()(using symbols) + val collector = new SuperCollector(using symbols) collector.traverse(sort) SortKey(sort) + SetKey(collector.getSupers)(using symbols) }) override protected final val classCache = new ExtractionCache[s.ClassDef, ClassResult]({ (cd, context) => val symbols = context.symbols - val collector = new SuperCollector()(using symbols) + val collector = new SuperCollector(using symbols) collector.traverse(cd) ClassKey(cd) + SetKey(collector.getSupers)(using symbols) }) diff --git a/core/src/main/scala/stainless/extraction/oo/Definitions.scala b/core/src/main/scala/stainless/extraction/oo/Definitions.scala index 7d7301ab58..df2d3be73e 100644 --- a/core/src/main/scala/stainless/extraction/oo/Definitions.scala +++ b/core/src/main/scala/stainless/extraction/oo/Definitions.scala @@ -26,7 +26,7 @@ trait Definitions extends innerfuns.Trees { self: Trees => val allAncestors = parents.flatMap(_.lookupClass).flatMap(tcd => tcd +: tcd.ancestors) 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 diff --git a/core/src/main/scala/stainless/extraction/oo/TransformerWithType.scala b/core/src/main/scala/stainless/extraction/oo/TransformerWithType.scala index dbabe39568..17f2919668 100644 --- a/core/src/main/scala/stainless/extraction/oo/TransformerWithType.scala +++ b/core/src/main/scala/stainless/extraction/oo/TransformerWithType.scala @@ -62,7 +62,7 @@ trait TransformerWithType extends TreeTransformer { t.Let(transform(vd), transform(e, vd.getType), transform(b, tpe)).copiedFrom(expr) case s.Application(caller, args) => - val s.FunctionType(from, to) = widen(caller.getType) + val s.FunctionType(from, to) = widen(caller.getType): @unchecked t.Application( transform(caller, s.FunctionType(from, tpe)), (args zip from) map (p => transform(p._1, p._2)) @@ -221,11 +221,11 @@ trait TransformerWithType extends TreeTransformer { t.FiniteSet(elems map (transform(_, base)), transform(base)).copiedFrom(expr) case s.SetAdd(set, elem) => - val st @ s.SetType(base) = widen(set.getType) + val st @ s.SetType(base) = widen(set.getType): @unchecked t.SetAdd(transform(set, st), transform(elem, base)).copiedFrom(expr) case s.ElementOfSet(elem, set) => - val st @ s.SetType(base) = widen(set.getType) + val st @ s.SetType(base) = widen(set.getType): @unchecked t.ElementOfSet(transform(elem, base), transform(set, st)).copiedFrom(expr) case s.SubsetOf(s1, s2) => @@ -251,11 +251,11 @@ trait TransformerWithType extends TreeTransformer { ).copiedFrom(expr) case s.BagAdd(bag, elem) => - val bt @ s.BagType(base) = widen(bag.getType) + val bt @ s.BagType(base) = widen(bag.getType): @unchecked t.BagAdd(transform(bag, bt), transform(elem, base)).copiedFrom(expr) case s.MultiplicityInBag(elem, bag) => - val bt @ s.BagType(base) = widen(bag.getType) + val bt @ s.BagType(base) = widen(bag.getType): @unchecked t.MultiplicityInBag(transform(elem, base), transform(bag, bt)).copiedFrom(expr) case s.BagIntersection(b1, b2) => @@ -279,15 +279,15 @@ trait TransformerWithType extends TreeTransformer { ).copiedFrom(expr) case s.MapApply(map, key) => - val mt @ s.MapType(from, _) = widen(map.getType) + val mt @ s.MapType(from, _) = widen(map.getType): @unchecked t.MapApply(transform(map, mt), transform(key, from)).copiedFrom(expr) case s.MapUpdated(map, key, value) => - val mt @ s.MapType(from, to) = widen(map.getType) + val mt @ s.MapType(from, to) = widen(map.getType): @unchecked t.MapUpdated(transform(map, mt), transform(key, from), transform(value, to)).copiedFrom(expr) case s.MapMerge(mask, map1, map2) => - val mt @ s.MapType(from, to) = widen(map1.getType) + val mt @ s.MapType(from, to) = widen(map1.getType): @unchecked t.MapMerge(transform(mask, s.SetType(from)), transform(map1, mt), transform(map2, mt)) // Stainless expressions @@ -346,7 +346,7 @@ trait TransformerWithType extends TreeTransformer { t.ArraySelect(transform(array), transform(index, s.Int32Type())).copiedFrom(expr) case s.ArrayUpdated(array, index, value) => - val at @ s.ArrayType(base) = widen(array.getType) + val at @ s.ArrayType(base) = widen(array.getType): @unchecked t.ArrayUpdated( transform(array, at), transform(index, s.Int32Type()), @@ -373,7 +373,7 @@ trait TransformerWithType extends TreeTransformer { ).copiedFrom(expr) case s.ApplyLetRec(id, tparams, tpe, tps, args) => - val s.FunctionType(from, _) = s.typeOps.instantiateType(tpe.getType, (tparams zip tps).toMap) + val s.FunctionType(from, _) = s.typeOps.instantiateType(tpe.getType, (tparams zip tps).toMap): @unchecked t.ApplyLetRec( transform(id), tparams map (tp => transform(tp).asInstanceOf[t.TypeParameter]), diff --git a/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala b/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala index b8e21a0007..29af64efda 100644 --- a/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala +++ b/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala @@ -90,7 +90,7 @@ class TypeEncoding(override val s: Trees, override val t: Trees) } private[this] def erased[T <: s.Type](tpe: T): T = { - val s.NAryType(tps, recons) = tpe + val s.NAryType(tps, recons) = tpe: @unchecked recons(tps.map(tp => s.AnyType().copiedFrom(tp))).copiedFrom(tpe).asInstanceOf[T] } diff --git a/core/src/main/scala/stainless/extraction/termination/InductElimination.scala b/core/src/main/scala/stainless/extraction/termination/InductElimination.scala index 0ca09ccf00..b725229b62 100644 --- a/core/src/main/scala/stainless/extraction/termination/InductElimination.scala +++ b/core/src/main/scala/stainless/extraction/termination/InductElimination.scala @@ -20,7 +20,7 @@ class InductElimination(override val s: Trees)(override val t: s.type) import dsl._ protected class TransformerContext(using val symbols: Symbols) - override protected def getContext(syms: Symbols) = new TransformerContext()(using syms) + override protected def getContext(syms: Symbols) = new TransformerContext(using syms) override protected def extractFunction(tcontext: TransformerContext, fd: FunDef): FunDef = { val syms = tcontext.symbols diff --git a/core/src/main/scala/stainless/extraction/throwing/Trees.scala b/core/src/main/scala/stainless/extraction/throwing/Trees.scala index c018a80aa0..8905b67f62 100644 --- a/core/src/main/scala/stainless/extraction/throwing/Trees.scala +++ b/core/src/main/scala/stainless/extraction/throwing/Trees.scala @@ -182,7 +182,7 @@ trait TreeDeconstructor extends imperative.TreeDeconstructor { case s.Try(body, cases, fin) => val (cids, cvs, ces, ctps, crecons) = deconstructCases(cases) (cids, cvs, (body +: ces) ++ fin, ctps, Seq(), (ids, vs, es, tps, _) => { - val newBody +: rest = es + val newBody +: rest = es: @unchecked val (nes, newFin) = if (fin.isEmpty) (rest, None) else (rest.init, rest.lastOption) t.Try(newBody, crecons(ids, vs, nes, tps), newFin) }) diff --git a/core/src/main/scala/stainless/extraction/xlang/PartialFunctions.scala b/core/src/main/scala/stainless/extraction/xlang/PartialFunctions.scala index 4695d9e7ca..7b1d4ba48d 100644 --- a/core/src/main/scala/stainless/extraction/xlang/PartialFunctions.scala +++ b/core/src/main/scala/stainless/extraction/xlang/PartialFunctions.scala @@ -42,7 +42,7 @@ class PartialFunctions(override val s: Trees)(override val t: s.type) override def transform(e: Expr): Expr = super.transform(e) match { case fi @ FunctionInvocation(ast.SymbolIdentifier("stainless.lang.PartialFunction.apply"), _, _) => - val FunctionInvocation(_, froms :+ to, Seq(fun)) = fi + val FunctionInvocation(_, froms :+ to, Seq(fun)) = fi: @unchecked val ct = ClassType(optPFClass.get.id, Seq(tupleTypeWrap(froms), to)) val (pre, body) = fun match { diff --git a/core/src/main/scala/stainless/extraction/xlang/TreeSanitizer.scala b/core/src/main/scala/stainless/extraction/xlang/TreeSanitizer.scala index 1f4dc0313d..81090b0a86 100644 --- a/core/src/main/scala/stainless/extraction/xlang/TreeSanitizer.scala +++ b/core/src/main/scala/stainless/extraction/xlang/TreeSanitizer.scala @@ -309,7 +309,7 @@ trait TreeSanitizer { self => errors += MalformedStainlessCode(e, "Testing lambdas for equality in non-ghost code is unsound") case tp => - val TypeOperator(es, _) = tp + val TypeOperator(es, _) = tp: @unchecked es.foreach(rec) } @@ -386,7 +386,7 @@ trait TreeSanitizer { self => errors += MalformedStainlessCode(l, "Calling a method or function on `this` within an invariant is unsound") case e => - val Operator(es, _) = e + val Operator(es, _) = e: @unchecked es.foreach(checkThisUsage) } } diff --git a/core/src/main/scala/stainless/genc/ir/Referentiator.scala b/core/src/main/scala/stainless/genc/ir/Referentiator.scala index bdc2688ad3..8ad827187f 100644 --- a/core/src/main/scala/stainless/genc/ir/Referentiator.scala +++ b/core/src/main/scala/stainless/genc/ir/Referentiator.scala @@ -69,7 +69,7 @@ final class Referentiator(val ctx: inox.Context) extends Transformer(LIR, RIR) { override def rec(prog: Prog)(using env: Env): to.Prog = { if (prog.decls.nonEmpty) { val modes = prog.decls.map(_._2) - val (to.Block(newDecls), newEnv0) = recImpl(Block(prog.decls.map(_._1)))(using env.copy(inGlobalDeclarations = true)) + val (to.Block(newDecls), newEnv0) = recImpl(Block(prog.decls.map(_._1)))(using env.copy(inGlobalDeclarations = true)): @unchecked val newEnv = newEnv0.copy(inGlobalDeclarations = false) to.Prog( newDecls.map(_.asInstanceOf[to.Decl]).zip(modes), diff --git a/core/src/main/scala/stainless/genc/ir/Transformer.scala b/core/src/main/scala/stainless/genc/ir/Transformer.scala index 44eb63eb25..19a0cbda51 100644 --- a/core/src/main/scala/stainless/genc/ir/Transformer.scala +++ b/core/src/main/scala/stainless/genc/ir/Transformer.scala @@ -52,7 +52,7 @@ abstract class Transformer[From <: IR, To <: IR](final val from: From, final val protected def rec(prog: Prog)(using Env): to.Prog = { if (prog.decls.nonEmpty) { val modes = prog.decls.map(_._2) - val (to.Block(newDecls), newEnv) = recImpl(Block(prog.decls.map(_._1))) + val (to.Block(newDecls), newEnv) = recImpl(Block(prog.decls.map(_._1))): @unchecked to.Prog( newDecls.map(_.asInstanceOf[to.Decl]).zip(modes), prog.functions.map(rec(_)(using newEnv)), diff --git a/core/src/main/scala/stainless/genc/phases/ArraysLengthsExtraction.scala b/core/src/main/scala/stainless/genc/phases/ArraysLengthsExtraction.scala index e840d0510f..03a98484e5 100644 --- a/core/src/main/scala/stainless/genc/phases/ArraysLengthsExtraction.scala +++ b/core/src/main/scala/stainless/genc/phases/ArraysLengthsExtraction.scala @@ -52,7 +52,7 @@ object ArraysLengthsExtraction { case HasADTInvariant(inv) => val invFd = syms.getFunction(inv) val Seq(tthisVd) = invFd.params - val TopLevelAnds(conjuncts) = invFd.fullBody + val TopLevelAnds(conjuncts) = invFd.fullBody: @unchecked conjuncts.collect(e => e match { case Equals(ArrayLength(ClassSelector(tthis: Variable, array)), EvalBV(bv)) if tthisVd.id == tthis.id && cd.fields.map(_.id).contains(array) => diff --git a/core/src/main/scala/stainless/genc/phases/ExtraOps.scala b/core/src/main/scala/stainless/genc/phases/ExtraOps.scala index b6653aef17..8ac13211ed 100644 --- a/core/src/main/scala/stainless/genc/phases/ExtraOps.scala +++ b/core/src/main/scala/stainless/genc/phases/ExtraOps.scala @@ -79,7 +79,7 @@ private[genc] object ExtraOps { def getManualType: ManualType = { assert(isManuallyTyped) - val Seq(StringLiteral(alias), StringLiteral(includes0)) = cd.extAnnotations(manualTypeAnnotation) + val Seq(StringLiteral(alias), StringLiteral(includes0)) = cd.extAnnotations(manualTypeAnnotation): @unchecked val include = if (includes0.isEmpty) None else Some(includes0) ManualType(alias, include) diff --git a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala index bc216a5574..cf1440ca19 100644 --- a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala +++ b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala @@ -546,7 +546,7 @@ private class S2IRImpl(override val s: tt.type, // Now proceed with the body val body: CIR.FunBody = if (fa.isManuallyDefined) { - val Seq(StringLiteral(code), StringLiteral(headerIncludes0), StringLiteral(cIncludes0)) = fa.extAnnotations(manualDefAnnotation) + val Seq(StringLiteral(code), StringLiteral(headerIncludes0), StringLiteral(cIncludes0)) = fa.extAnnotations(manualDefAnnotation): @unchecked val headerIncludes = if (headerIncludes0.isEmpty) Nil else { headerIncludes0 split ':' }.toSeq @@ -915,7 +915,7 @@ private class S2IRImpl(override val s: tt.type, CIR.Assign(CIR.ArrayAccess(rec(array), rec(index)), rec(value)) case Swap(array1, index1, array2, index2) => - val ArrayType(base) = array1.getType + val ArrayType(base) = array1.getType: @unchecked val a1 = rec(array1) val a2 = rec(array2) val i1 = rec(index1) @@ -993,10 +993,10 @@ private class S2IRImpl(override val s: tt.type, case BVNarrowingCast(e, t) => CIR.IntegralCast(rec(e), rec(t).asInstanceOf[CIR.PrimitiveType].primitive.asInstanceOf[PT.IntegralPrimitiveType]) case BVUnsignedToSigned(e) => - val BVType(false, size) = e.getType + val BVType(false, size) = e.getType: @unchecked CIR.IntegralCast(rec(e), rec(BVType(true, size)).asInstanceOf[CIR.PrimitiveType].primitive.asInstanceOf[PT.IntegralPrimitiveType]) case BVSignedToUnsigned(e) => - val BVType(true, size) = e.getType + val BVType(true, size) = e.getType: @unchecked CIR.IntegralCast(rec(e), rec(BVType(false, size)).asInstanceOf[CIR.PrimitiveType].primitive.asInstanceOf[PT.IntegralPrimitiveType]) case MatchExpr(scrutinee, cases) => convertPatMap(scrutinee, cases) diff --git a/core/src/main/scala/stainless/solvers/InoxEncoder.scala b/core/src/main/scala/stainless/solvers/InoxEncoder.scala index c61402758c..0cda276865 100644 --- a/core/src/main/scala/stainless/solvers/InoxEncoder.scala +++ b/core/src/main/scala/stainless/solvers/InoxEncoder.scala @@ -171,7 +171,7 @@ private class TreeEncoder[Prog <: Program](val sourceProgram: Prog) case s.ArrayUpdated(array, index, value) => val na = transform(array) - val t.ADTType(_, tps) = transform(array.getType) + val t.ADTType(_, tps) = transform(array.getType): @unchecked t.ADT(arrayCons.id, tps, Seq( t.MapUpdated(t.ADTSelector(na, arr).copiedFrom(e), transform(index), transform(value)).copiedFrom(e), t.ADTSelector(na, size).copiedFrom(e) @@ -181,7 +181,7 @@ private class TreeEncoder[Prog <: Program](val sourceProgram: Prog) t.ADTSelector(transform(array), size).copiedFrom(e) case s.Application(caller, args) => - val s.FunctionType(from, to) = caller.getType + val s.FunctionType(from, to) = caller.getType: @unchecked t.Application(transform(caller).copiedFrom(e), args map transform).copiedFrom(e) case s.SizedADT(sort, tps, args, size) => transform(s.ADT(sort, tps, args)) diff --git a/core/src/main/scala/stainless/termination/ChainBuilder.scala b/core/src/main/scala/stainless/termination/ChainBuilder.scala index 1de92cf54f..cf78751115 100644 --- a/core/src/main/scala/stainless/termination/ChainBuilder.scala +++ b/core/src/main/scala/stainless/termination/ChainBuilder.scala @@ -77,7 +77,7 @@ trait ChainBuilder extends RelationBuilder { self: Strengthener with OrderingRel case Some((subloop, chains, signature)) if signature == funDefChainSignature(funDef) => subloop -> chains case _ => { def chains(seen: Set[FunDef], chain: List[Relation]): (Set[FunDef], Set[Chain]) = { - val Relation(_, _, FunctionInvocation(id, _, _), _) :: _ = chain + val Relation(_, _, FunctionInvocation(id, _, _), _) :: _ = chain: @unchecked val fd = getFunction(id) if (!transitivelyCalls(fd, funDef)) { diff --git a/core/src/main/scala/stainless/termination/ChainProcessor.scala b/core/src/main/scala/stainless/termination/ChainProcessor.scala index 536e0b1d6e..9d3cb63eea 100644 --- a/core/src/main/scala/stainless/termination/ChainProcessor.scala +++ b/core/src/main/scala/stainless/termination/ChainProcessor.scala @@ -36,8 +36,6 @@ class ChainProcessor(override val checker: ProcessingPipeline) strengthenPostconditions(problem.funSet) strengthenApplications(problem.funSet) - val api = getAPI - reporter.debug("- Running ChainBuilder") val chainsMap = problem.funSet.map { funDef => funDef -> getChains(funDef) @@ -49,40 +47,41 @@ class ChainProcessor(override val checker: ProcessingPipeline) if (loopPoints.size > 1) { reporter.debug("-+> Multiple looping points, can't build chain proof") - return None - } - - val bases: Seq[FunDef] = - {if (loopPoints.nonEmpty) loopPoints - else chainsMap.collect { - case (fd, (fds, chains)) if chains.nonEmpty => fd - }}.toList - - findDecrease(bases,chainsMap,checker.program.symbols) match { - case (cs, Some(base), Some(reconstr)) => - annotateChains(cs,base,reconstr) - Some(problem.funDefs.map { fd => - measureCache.get(fd) match { - case Some(measure) => - val inductiveLemmas = - Some((ordering.getPostconditions, ordering.insertedApps)) - Cleared(fd, Some(measure), inductiveLemmas) - case None => - throw FailedMeasureInference(fd, - s"No measure annotated in function `${fd.id}` which was cleared in chain processor.") - } - }) - case _ => None + None + } else { + val bases: Seq[FunDef] = { + if (loopPoints.nonEmpty) loopPoints + else chainsMap.collect { + case (fd, (fds, chains)) if chains.nonEmpty => fd + } + }.toList + + findDecrease(bases, chainsMap, checker.program.symbols) match { + case (cs, Some(base), Some(reconstr)) => + annotateChains(cs, base, reconstr) + Some(problem.funDefs.map { fd => + measureCache.get(fd) match { + case Some(measure) => + val inductiveLemmas = + Some((ordering.getPostconditions, ordering.insertedApps)) + Cleared(fd, Some(measure), inductiveLemmas) + case None => + throw FailedMeasureInference(fd, + s"No measure annotated in function `${fd.id}` which was cleared in chain processor.") + } + }) + case _ => None + } } } - def findDecrease(bases: Seq[FunDef], chainsMap: Map[FunDef,(Set[FunDef], Set[Chain])], syms: Symbols): (Seq[Chain], Option[FunDef], Option[Expr => Expr]) = { + def findDecrease(bases: Seq[FunDef], chainsMap: Map[FunDef, (Set[FunDef], Set[Chain])], syms: Symbols): (Seq[Chain], Option[FunDef], Option[Expr => Expr]) = { val depth: Int = 1 // Number of unfoldings val api = getAPI - def solveIter(i: Int,allChains: Set[Chain],cs: Set[Chain],base: FunDef): (Set[Chain], Option[Expr => Expr]) = { + def solveIter(i: Int, allChains: Set[Chain], cs: Set[Chain], base: FunDef): (Set[Chain], Option[Expr => Expr]) = { reporter.debug("-+> Iteration #" + i) - if(i < 0) (cs,None) + if (i < 0) (cs, None) else { val e1s = cs.toSeq.map { chain => val (path, args) = chain.loop @@ -93,10 +92,10 @@ class ChainProcessor(override val checker: ProcessingPipeline) val decreases: Option[(Expr, Expr, Expr => Expr)] = formulas.find { case (query, _, _) => api.solveVALID(query).contains(true) } - if (decreases.isDefined) (cs,Some(decreases.get._3)) + if (decreases.isDefined) (cs, Some(decreases.get._3)) else { val newChains = cs.flatMap(c1 => allChains.flatMap(c2 => c1 compose c2)) - solveIter(i-1,allChains,newChains, base) + solveIter(i - 1, allChains, newChains, base) } } } @@ -106,8 +105,8 @@ class ChainProcessor(override val checker: ProcessingPipeline) val chains = chainsMap(base)._2 val allChains = chainsMap(base)._2 reporter.debug("- Searching for size decrease") - val (cs,reconstr) = solveIter(depth, allChains,chains, base) - if(reconstr.isDefined) (cs.toSeq, Some(base), reconstr) + val (cs, reconstr) = solveIter(depth, allChains, chains, base) + if (reconstr.isDefined) (cs.toSeq, Some(base), reconstr) else solveBase(bs) case Nil => (Seq(), None, None) } @@ -120,25 +119,26 @@ class ChainProcessor(override val checker: ProcessingPipeline) */ private val measureCache: MutableMap[FunDef, Expr] = MutableMap.empty - def annotateChains(cs: Seq[Chain],base: FunDef,recons: Expr => Expr): Unit = { + def annotateChains(cs: Seq[Chain], base: FunDef, recons: Expr => Expr): Unit = { /* Stores for a function f an index i the measure expressions holding for those values leaving the chains in i steps. If i = -1 then the value loops. */ - val annotationMap: MutableMap[(FunDef,Int),Seq[(Expr,Expr)]] = - MutableMap.empty[(FunDef,Int), Seq[(Expr,Expr)]].withDefaultValue(Seq()) + val annotationMap: MutableMap[(FunDef, Int), Seq[(Expr, Expr)]] = + MutableMap.empty[(FunDef, Int), Seq[(Expr, Expr)]].withDefaultValue(Seq()) /* Gives the index of f in chain c. */ def domIndex(rs: Seq[Relation], f: FunDef, i: Int): Int = rs match { - case Relation(fd,_,fi,_) :: _ if (fd.id == f.id) => i - case Relation(fd,_,fi,_) :: _ if (fi.id == f.id) => i+1 - case r :: rs => domIndex(rs,f,i+1) + case Relation(fd, _, fi, _) :: _ if fd.id == f.id => i + case Relation(fd, _, fi, _) :: _ if fi.id == f.id => i + 1 + case r :: rs => domIndex(rs, f, i + 1) case _ => -1 } - val M = cs.map{ c => c.size }.max + val M = cs.map { c => c.size }.max def measure(expr: Seq[Expr]) = ordering.measure(Seq(recons(tupleWrap(expr)))) + def tupleMeasure(expr: Expr, j: Int, k: Int) = tupleWrap(Seq(expr, IntegerLiteral(j), IntegerLiteral(k))) @@ -146,64 +146,64 @@ class ChainProcessor(override val checker: ProcessingPipeline) def annotateBase(base: FunDef, cs: Seq[Chain]) = { val args = measure(base.params.map(_.toVariable)) val baseCond = - orJoin(cs.map{ c => Chain(c.relations).loop._1.toClause }) - val baseMeasure = tupleMeasure(args,0,0) - annotationMap += ((base,-1) -> (annotationMap((base,-1)) :+ (baseCond,baseMeasure))) + orJoin(cs.map { c => Chain(c.relations).loop._1.toClause }) + val baseMeasure = tupleMeasure(args, 0, 0) + annotationMap += ((base, -1) -> (annotationMap((base, -1)) :+ (baseCond, baseMeasure))) } def annotateLoops(base: FunDef, cs: Seq[Chain]) = { // I assume the chains cs start at base for (c <- cs; member <- c.fds if member.id != base.id) { - val i = domIndex(c.relations,member,0) + val i = domIndex(c.relations, member, 0) val domRelations = c.relations.drop(i) // annotate looping condition - val (domRpath,args1) = Chain(domRelations).loop + val (domRpath, args1) = Chain(domRelations).loop val margs1 = bindingsToLets(domRpath.bindings, measure(args1)) val cond1 = domRpath.toClause - val measure1 = tupleMeasure(margs1,M-i,M) - annotationMap += ((member,-1) -> (annotationMap((member,-1)) :+ (cond1,measure1))) + val measure1 = tupleMeasure(margs1, M - i, M) + annotationMap += ((member, -1) -> (annotationMap((member, -1)) :+ (cond1, measure1))) // annotate escaping steps var relations = domRelations.dropRight(1) - while(!relations.isEmpty){ - val (path,_) = Chain(relations).loop + while (relations.nonEmpty) { + val (path, _) = Chain(relations).loop val steps = relations.size val cond2 = path.toClause - val measure2 = tupleMeasure(IntegerLiteral(0),0,M-(steps)) - annotationMap += ((member,steps) -> (annotationMap((member,steps)) :+ (cond2,measure2))) + val measure2 = tupleMeasure(IntegerLiteral(0), 0, M - (steps)) + annotationMap += ((member, steps) -> (annotationMap((member, steps)) :+ (cond2, measure2))) relations = relations.dropRight(1) } val noCond = not(cond1) - val noMeasure = tupleMeasure(IntegerLiteral(0),0,M-i) - annotationMap += ((member,0) -> (annotationMap((member,0)) :+ (noCond,noMeasure))) + val noMeasure = tupleMeasure(IntegerLiteral(0), 0, M - i) + annotationMap += ((member, 0) -> (annotationMap((member, 0)) :+ (noCond, noMeasure))) } } def buildMeasure(): Unit = { - val default = tupleMeasure(IntegerLiteral(0),0,M) + val default = tupleMeasure(IntegerLiteral(0), 0, M) /* Annotation map with format: f -> (index -> Seq(values)) */ val indexedByFun = annotationMap.groupBy(_._1._1) - .view.mapValues(_.map{ case (k,v) => k._2 -> v }) + .view.mapValues(_.map { case (k, v) => k._2 -> v }) .toMap - for((k,v) <- indexedByFun.toSeq) yield { - val orderedMeasures: List[(Int, Seq[(Expr,Expr)])] = v.toList.sortBy(_._1) + for ((k, v) <- indexedByFun.toSeq) yield { + val orderedMeasures: List[(Int, Seq[(Expr, Expr)])] = v.toList.sortBy(_._1) /* Measures has -1 at the end and flattened */ - val measures: List[(Int, Seq[(Expr,Expr)])] = - if(orderedMeasures.head._1 == -1){ + val measures: List[(Int, Seq[(Expr, Expr)])] = + if (orderedMeasures.head._1 == -1) { orderedMeasures.tail ++ orderedMeasures.head._2.map(m => -1 -> Seq(m)).toList } else { orderedMeasures.tail } - val measure = measures.foldLeft(default){ case (acc,(_, seq)) => - if(!seq.isEmpty){ + val measure = measures.foldLeft(default) { case (acc, (_, seq)) => + if (seq.nonEmpty) { val expr = seq.head._2 - IfExpr(orJoin(seq.map(_._1)),expr,acc) + IfExpr(orJoin(seq.map(_._1)), expr, acc) } else { acc } @@ -214,8 +214,8 @@ class ChainProcessor(override val checker: ProcessingPipeline) } annotateBase(base, cs) - annotateLoops(base,cs) + annotateLoops(base, cs) buildMeasure() - } + } } diff --git a/core/src/main/scala/stainless/termination/DecreasesProcessor.scala b/core/src/main/scala/stainless/termination/DecreasesProcessor.scala index df86dd2279..09671dbb32 100644 --- a/core/src/main/scala/stainless/termination/DecreasesProcessor.scala +++ b/core/src/main/scala/stainless/termination/DecreasesProcessor.scala @@ -166,7 +166,7 @@ class DecreasesProcessor(override val checker: ProcessingPipeline) builtIf } - val (rel, expr, index) :: rest = measures // safe because of precondition + val (rel, expr, index) :: rest = measures: @unchecked // safe because of precondition val path = rel match { case Some(r) => r.path; case None => Path.empty } val flat = flatten(expr, Seq(IntegerLiteral(index))) diff --git a/core/src/main/scala/stainless/termination/MeasureInference.scala b/core/src/main/scala/stainless/termination/MeasureInference.scala index 1f1d0398cb..e10246382a 100644 --- a/core/src/main/scala/stainless/termination/MeasureInference.scala +++ b/core/src/main/scala/stainless/termination/MeasureInference.scala @@ -66,7 +66,7 @@ class MeasureInference(override val s: Trees, override val t: Trees)(using overr private def size(v: Variable): Expr = { require(v.getType.isInstanceOf[ADTType]) - val ADTType(id, tps) = v.getType + val ADTType(id, tps) = v.getType: @unchecked FunctionInvocation(sizes.fullSizeId(symbols.sorts(id)), tps, Seq(v)).setPos(v) } } diff --git a/core/src/main/scala/stainless/testgen/ScalaTestGen.scala b/core/src/main/scala/stainless/testgen/ScalaTestGen.scala index c2b9631ec2..198583db8b 100644 --- a/core/src/main/scala/stainless/testgen/ScalaTestGen.scala +++ b/core/src/main/scala/stainless/testgen/ScalaTestGen.scala @@ -18,7 +18,7 @@ object ScalaTestGen { import stainless.trees._ private val testCaseFnRegex: Regex = """\s*def testCase(\d+): Unit = (.+)""".r - private val importsRegex: Regex = """import ((?:\w+\.)*)(?:(\w+)|\{((?:\w+\s*,\s*)*\w+)\})""".r("path", "iden", "idens") + private val importsRegex: Regex = """import ((?\w+\.)*)(?(\w+)|\{((?\w+\s*,\s*)*\w+)\})""".r def generateTestCases(origSyms: xt.Symbols) (p: inox.Program {val trees: stainless.trees.type}) diff --git a/core/src/main/scala/stainless/transformers/lattices/Core.scala b/core/src/main/scala/stainless/transformers/lattices/Core.scala index 492e033cff..81830edf8a 100644 --- a/core/src/main/scala/stainless/transformers/lattices/Core.scala +++ b/core/src/main/scala/stainless/transformers/lattices/Core.scala @@ -403,7 +403,7 @@ trait Core extends Definitions { ocbsl => if (Thread.interrupted()) throw new InterruptedException() def inlineAppliedLambda(cLam: Code, in: Code): (Occurrences, Code, PartialCodeRes) = { - val Signature(Label.Lambda(params), Seq(body)) = code2sig(cLam) + val Signature(Label.Lambda(params), Seq(body)) = code2sig(cLam): @unchecked object inliner extends CodeTransformer { override type Extra = Unit @@ -633,7 +633,7 @@ trait Core extends Definitions { ocbsl => CodeRes.ifExpr(rcond, rthenn, rels, tpe) case e: (Lambda | Choose | Forall) => - val (lab: Label.LambdaLike, body) = e match { + val (lab: Label.LambdaLike, body) = (e match { case Lambda(params, body) => val vParams = params.map(vd => idOfVariable(vd.toVariable)) (Label.Lambda(vParams), body) @@ -643,7 +643,7 @@ trait Core extends Definitions { ocbsl => case Forall(params, pred) => val vParams = params.map(vd => idOfVariable(vd.toVariable)) (Label.Forall(vParams), pred) - } + }): @unchecked val rbody = codeOfExpr(body)(using env.incIf(lab)) CodeRes.lambdaLike(lab, rbody, tpe) @@ -654,12 +654,12 @@ trait Core extends Definitions { ocbsl => codeOfExpr(body)(using env, re.ctxs, subst + (vd.toVariable -> re.terminal)) case e: (Assume | Assert | Require | Decreases) => - val (lab: Label.AssumeLike, pred, body) = e match { + val (lab: Label.AssumeLike, pred, body) = (e match { case Assume(pred, body) => (Label.Assume, pred, body) case Assert(pred, _, body) => (Label.Assert, pred, body) case Require(pred, body) => (Label.Require, pred, body) case Decreases(measure, body) => (Label.Decreases, measure, body) - } + }): @unchecked val rpred = codeOfExpr(pred) assert(rpred.ctxs.isLitVarOrBoundDef(rpred.terminal)) codeOfExpr(body)(using env, rpred.ctxs.withAssumeLike(lab, rpred.terminal)) @@ -674,10 +674,10 @@ trait Core extends Definitions { ocbsl => case FunctionInvocation(id, tps, args) => codeOfExprsBound(args, tpe)(mkFunInvoc(id, tps, _)) case Application(callee, args) => codeOfExprsBound(callee +: args, tpe) { case cCallee +: cArgs => mkApp(cCallee, cArgs) } case IsConstructor(e, id) => - val adt @ ADTType(_, _) = e.getType + val adt @ ADTType(_, _) = e.getType: @unchecked codeOfExprsBound(e, tpe)(mkIsCtor(_, adt, id)) case s @ ADTSelector(e, selector) => - val adt @ ADTType(_, _) = e.getType + val adt @ ADTType(_, _) = e.getType: @unchecked codeOfExprsBound(e, tpe)(mkADTSelector(_, adt, s.constructor, selector)) case Annotated(e, flags) => codeOfExprsBound(e, tpe)(mkAnnot(_, flags)) @@ -841,7 +841,7 @@ trait Core extends Definitions { ocbsl => val (rsubs, subst2) = recHelper(subScruts, subps) (LabelledPattern.ADT(id, tps, rsubs), subst2) case TuplePattern(_, subps) => - val tt@TupleType(_) = codeTpe(scrut) + val tt@TupleType(_) = codeTpe(scrut): @unchecked val subScruts = tupleSubscrutinees(scrut, tt) val (rsubs, subst2) = recHelper(subScruts, subps) (LabelledPattern.TuplePattern(rsubs), subst2) @@ -1116,7 +1116,7 @@ trait Core extends Definitions { ocbsl => val fstTry: Option[CodeRes] = { def unplugBranch(branch: Code, branchCtx: Ctxs): CodeRes = { - val Some((branchCr0, _)) = unplugged(branch)(using env, branchCtx) + val Some((branchCr0, _)) = unplugged(branch)(using env, branchCtx): @unchecked assert(branchCtx.isPrefixOf(branchCr0.ctxs)) // resCtxs is like branchCr0.ctx but without the Assumed(cond) (or Assumed(neg(cond))) coming from branchCtx val resCtxs = condCtxs.addExtraWithoutAssumed(branchCr0.ctxs) @@ -1545,7 +1545,7 @@ trait Core extends Definitions { ocbsl => def mkElidable(caseRhs: Code, caseCtxs: Ctxs, rhsCtxs: Ctxs): SimplifiedCases.ElidableMatchExpr = { assert(ctxs.isPrefixOf(caseCtxs)) assert(caseCtxs.isPrefixOf(rhsCtxs)) - val Some((rhsUnpl, _)) = unplugged(caseRhs)(using env, rhsCtxs) + val Some((rhsUnpl, _)) = unplugged(caseRhs)(using env, rhsCtxs): @unchecked assert(rhsCtxs.isPrefixOf(rhsUnpl.ctxs)) // Here, we remove all `Assumed` coming from the guard and the pattern. // These are not needed anymore because we will simplify the match expression away. @@ -2106,7 +2106,7 @@ trait Core extends Definitions { ocbsl => val Seq(e) = eargs IsConstructor(e, id) case Label.Application => - val callee +: theArgs = eargs + val callee +: theArgs = eargs: @unchecked Application(callee, theArgs) case Label.Equals => @@ -2130,7 +2130,7 @@ trait Core extends Definitions { ocbsl => case lab@(Label.Plus | Label.Times) => assert(eargs.size >= 2) val recons: (Expr, Expr) => Expr = if (lab == Label.Plus) Plus.apply else Times.apply - val e1 +: e2 +: rest = eargs + val e1 +: e2 +: rest = eargs: @unchecked rest.foldLeft(recons(e1, e2))(recons) case Label.Minus => val Seq(lhs, rhs) = eargs @@ -2213,7 +2213,7 @@ trait Core extends Definitions { ocbsl => case Label.FiniteArray(base) => FiniteArray(eargs, base) case Label.LargeArray(elemsIndices, base) => - val elems :+ default :+ size = eargs + val elems :+ default :+ size = eargs: @unchecked LargeArray(elemsIndices.zip(elems).toMap, default, size, base) case Label.ArraySelect => val Seq(arr, i) = eargs @@ -2226,7 +2226,7 @@ trait Core extends Definitions { ocbsl => ArrayLength(arr) case Label.FiniteMap(keyTpe, valueTpe) => - val exprElems :+ exprDefault = eargs + val exprElems :+ exprDefault = eargs: @unchecked val paired = exprElems.grouped(2).map { case Seq(k, v) => (k, v) }.toSeq FiniteMap(paired, exprDefault, keyTpe, valueTpe) case Label.MapApply => @@ -2284,7 +2284,7 @@ trait Core extends Definitions { ocbsl => val rsubs = recHelper(adtSubScrutinees(scrut, ADTType(id, tps)), subps) ADTPattern(bdg, id, tps, rsubs) case LabelledPattern.TuplePattern(subps) => - val tt@TupleType(bases) = codeTpe(scrut) + val tt@TupleType(bases) = codeTpe(scrut): @unchecked assert(bases.size == subps.size) val rsubs = recHelper(tupleSubscrutinees(scrut, tt), subps) TuplePattern(bdg, rsubs) @@ -2923,7 +2923,7 @@ trait Core extends Definitions { ocbsl => PatBdgsAndConds(newCtxs, subscruts ++ recBdgs, adtPatCond +: recPatConds) case LabelledPattern.TuplePattern(subps) => - val tt@TupleType(bases) = codeTpe(scrut) + val tt@TupleType(bases) = codeTpe(scrut): @unchecked assert(bases.size == subps.size) val subscruts = tupleSubscrutinees(scrut, tt) val PatBdgsAndConds(newCtxs, recBdgs, recPatConds) = recHelper(ctxs, subscruts, subps) diff --git a/core/src/main/scala/stainless/verification/DefaultTactic.scala b/core/src/main/scala/stainless/verification/DefaultTactic.scala index 5f85791c2b..d66c0a376b 100644 --- a/core/src/main/scala/stainless/verification/DefaultTactic.scala +++ b/core/src/main/scala/stainless/verification/DefaultTactic.scala @@ -35,7 +35,7 @@ trait DefaultTactic extends Tactic { Seq() case _ => - val Lambda(Seq(res), b @ TopLevelAnds(es)) = lambda + val Lambda(Seq(res), b @ TopLevelAnds(es)) = lambda: @unchecked val body = andJoin(es.filterNot { case Annotated(e, flags) => flags contains DropConjunct case p: Passes => true @@ -49,7 +49,7 @@ trait DefaultTactic extends Tactic { } } - val Lambda(Seq(res), b @ TopLevelAnds(es)) = lambda + val Lambda(Seq(res), b @ TopLevelAnds(es)) = lambda: @unchecked val examples = es collect { case p: Passes => p.asConstraint } val examplesPost = if (examples.nonEmpty) Seq(Let(res, e, andJoin(examples)).copiedFrom(e)) else Seq() diff --git a/core/src/main/scala/stainless/verification/VerificationChecker.scala b/core/src/main/scala/stainless/verification/VerificationChecker.scala index 4c952b71f5..1d31b0d301 100644 --- a/core/src/main/scala/stainless/verification/VerificationChecker.scala +++ b/core/src/main/scala/stainless/verification/VerificationChecker.scala @@ -231,23 +231,25 @@ trait VerificationChecker { self => evaluator.eval(wrapped, model) } - val newArgs = evaledArgs.map { - case Successful(e) => e - case RuntimeError(msg) => return failure(s"- ADT inv. argument leads to runtime error: $msg") - case EvaluatorError(msg) => return failure(s"- ADT inv. argument leads to evaluator error: $msg") + val (newArgs, errs) = evaledArgs.partitionMap { + case Successful(e) => Left(e) + case RuntimeError(msg) => Right(failure(s"- ADT inv. argument leads to runtime error: $msg")) + case EvaluatorError(msg) => Right(failure(s"- ADT inv. argument leads to evaluator error: $msg")) } - - val newAdt = ADT(adt.id, adt.tps, newArgs) - val adtVar = Variable(FreshIdentifier("adt"), adt.getType(using symbols), Seq()) - val newInv = FunctionInvocation(invId, inv.tps, Seq(adtVar)) - val newModel = inox.Model(program)(model.vars + (adtVar.toVal -> newAdt), model.chooses) - val newCondition = exprOps.replace(Map(inv -> newInv), vc.condition) - - evaluator.eval(newCondition, newModel) match { - case Successful(BooleanLiteral(false)) => success - case Successful(_) => failure("- Invalid model.") - case RuntimeError(msg) => failure(s"- Model leads to runtime error: $msg") - case EvaluatorError(msg) => failure(s"- Model leads to evaluation error: $msg") + if (errs.nonEmpty) errs.head + else { + val newAdt = ADT(adt.id, adt.tps, newArgs) + val adtVar = Variable(FreshIdentifier("adt"), adt.getType(using symbols), Seq()) + val newInv = FunctionInvocation(invId, inv.tps, Seq(adtVar)) + val newModel = inox.Model(program)(model.vars + (adtVar.toVal -> newAdt), model.chooses) + val newCondition = exprOps.replace(Map(inv -> newInv), vc.condition) + + evaluator.eval(newCondition, newModel) match { + case Successful(BooleanLiteral(false)) => success + case Successful(_) => failure("- Invalid model.") + case RuntimeError(msg) => failure(s"- Model leads to runtime error: $msg") + case EvaluatorError(msg) => failure(s"- Model leads to evaluation error: $msg") + } } } @@ -317,7 +319,7 @@ trait VerificationChecker { self => VCResult(VCStatus.Valid, s.getResultSolver.map(_.name), Some(time)) case SatWithModel(model) if checkModels && vc.kind.isInstanceOf[VCKind.AdtInvariant] => - val VCKind.AdtInvariant(invId) = vc.kind + val VCKind.AdtInvariant(invId) = vc.kind: @unchecked val status = checkAdtInvariantModel(vc, invId, model) VCResult(status, s.getResultSolver.map(_.name), Some(time)) diff --git a/frontends/benchmarks/verification/valid/Streams.scala b/frontends/benchmarks/verification/valid/Streams.scala index e9a795a0a6..f60f3b5818 100644 --- a/frontends/benchmarks/verification/valid/Streams.scala +++ b/frontends/benchmarks/verification/valid/Streams.scala @@ -27,7 +27,7 @@ object Stream { decreases(n) indexedAt(n, Stream[BigInt](0, (() => indexedAt(n-1, Stream[BigInt](1, (() => - zipWith[BigInt,BigInt,BigInt](n - 2, (a, b) => a + b, fib(n - 2), fib(n - 1).tail()) + zipWith[BigInt,BigInt,BigInt](n - 2, (a, b) => a + b, fib(n - 2): (Stream[BigInt] @indexedAtAnnot(n - 2)), (fib(n - 1): (Stream[BigInt] @indexedAtAnnot(n - 2))).tail()) ))) ))) } diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala index 85c4cbedd2..83ae3d733b 100644 --- a/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala +++ b/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala @@ -1735,8 +1735,8 @@ class CodeExtraction(inoxCtx: inox.Context, symbolMapping: SymbolMapping)(using case ExCastCall(expr, from, to) => // Double check that we are dealing with regular integer types - val xt.BVType(true, size) = extractType(from)(using dctx, NoSourcePosition) - val newType @ xt.BVType(true, newSize) = extractType(to)(using dctx, NoSourcePosition) + val xt.BVType(true, size) = extractType(from)(using dctx, NoSourcePosition): @unchecked + val newType @ xt.BVType(true, newSize) = extractType(to)(using dctx, NoSourcePosition): @unchecked if (size > newSize) xt.BVNarrowingCast(extractTree(expr), newType) else xt.BVWideningCast(extractTree(expr), newType) 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 d3a249d1fa..359861872e 100644 --- a/frontends/dotty/src/main/scala/stainless/frontends/dotc/StainlessExtraction.scala +++ b/frontends/dotty/src/main/scala/stainless/frontends/dotc/StainlessExtraction.scala @@ -30,8 +30,8 @@ class StainlessExtraction(val inoxCtx: inox.Context) { val unit = ctx.compilationUnit val tree = unit.tpdTree val (id, stats) = tree match { - case pd @ PackageDef(refTree, lst) => - val id = lst.collectFirst { case PackageDef(ref, stats) => ref } match { + case pd@PackageDef(_, lst) => + val id = lst.collectFirst { case PackageDef(ref, _) => ref } match { case Some(ref) => extractRef(ref) case None => FreshIdentifier(unit.source.file.name.replaceFirst("[.][^.]+$", "")) } @@ -44,41 +44,41 @@ class StainlessExtraction(val inoxCtx: inox.Context) { fragmentChecker.ghostChecker(tree) fragmentChecker.checker(tree) - if (!fragmentChecker.hasErrors()) { - val (imports, unitClasses, unitFunctions, unitTypeDefs, subs, classes, functions, typeDefs) = { - // 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 - // that just wraps the annotated function in a try-catch. - // The catch clause intercepts CommandLineParser.ParseError exceptions, causing recovery failure in - // later Stainless phases so we simply drop that synthetic class. - val filteredStats = findMain(stats) - .map(name => stats.filter { - case TypeDef(n, _) => name != n.toTermName - case _ => true - }).getOrElse(stats) - try - extraction.extractStatic(filteredStats) - catch { - case UnsupportedCodeException(pos, msg) => - inoxCtx.reporter.error(pos, msg) - return None - case e => throw e - } - } - assert(unitFunctions.isEmpty, "Packages shouldn't contain functions") + if (!fragmentChecker.hasErrors()) tryExtractUnit(extraction, unit, id, stats) + else None + } + private def tryExtractUnit(extraction: CodeExtraction, + unit: CompilationUnit, + id: Identifier, + stats: List[tpd.Tree])(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 + // that just wraps the annotated function in a try-catch. + // The catch clause intercepts CommandLineParser.ParseError exceptions, causing recovery failure in + // later Stainless phases so we simply drop that synthetic class. + val filteredStats = findMain(stats) + .map(name => stats.filter { + case TypeDef(n, _) => name != n.toTermName + case _ => true + }).getOrElse(stats) + 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)) - } else { - None + } catch { + case UnsupportedCodeException(pos, msg) => + inoxCtx.reporter.error(pos, msg) + None + case e => throw e } } - def findMain(stats: List[tpd.Tree])(using DottyContext): Option[TermName] = { + private def findMain(stats: List[tpd.Tree])(using DottyContext): Option[TermName] = { val trAcc = new tpd.TreeAccumulator[Option[TermName]] { override def apply(found: Option[TermName], tree: tpd.Tree)(using DottyContext): Option[TermName] = { if (found.isDefined) found diff --git a/frontends/library/stainless/collection/List.scala b/frontends/library/stainless/collection/List.scala index cfce5f970e..5171a8a451 100644 --- a/frontends/library/stainless/collection/List.scala +++ b/frontends/library/stainless/collection/List.scala @@ -31,7 +31,7 @@ sealed abstract class List[T] { else 1 + tSize } }) ensuring(res => 0 <= res && res <= Int.MaxValue) - + @isabelle.function(term = "List.list.set") def content: Set[T] = this match { case Nil() => Set() @@ -56,13 +56,13 @@ sealed abstract class List[T] { def head: T = { require(this != Nil[T]()) - val Cons(h, _) = this + val Cons(h, _) = this: @unchecked // Be quiet! h } def tail: List[T] = { require(this != Nil[T]()) - val Cons(_, t) = this + val Cons(_, t) = this: @unchecked t } @@ -138,7 +138,7 @@ sealed abstract class List[T] { else i )) } - + def drop(i: BigInt): List[T] = { (this, i) match { case (Nil(), _) => Nil[T]() case (Cons(h, t), i) => @@ -169,7 +169,7 @@ sealed abstract class List[T] { } ensuring { res => res.content.subsetOf(this.content) } - + def slice(from: BigInt, to: BigInt): List[T] = { require(0 <= from && from <= to && to <= size) drop(from).take(to-from) @@ -397,7 +397,7 @@ sealed abstract class List[T] { def updated(i: BigInt, y: T): List[T] = { require(0 <= i && i < this.size) - this match { + (this: @unchecked) match { case Cons(x, tail) if i == 0 => Cons[T](y, tail) case Cons(x, tail) => @@ -407,14 +407,14 @@ sealed abstract class List[T] { def iupdated(i: Int, y: T): List[T] = { require(0 <= i && i < isize) - this match { + (this: @unchecked) match { case Cons(x, tail) if i == 0 => Cons[T](y, tail) case Cons(x, tail) => Cons[T](x, tail.iupdated(i - 1, y)) } } - + private def insertAtImpl(pos: BigInt, l: List[T]): List[T] = { require(0 <= pos && pos <= size) if(pos == BigInt(0)) { @@ -524,7 +524,7 @@ sealed abstract class List[T] { def scanRight[R](z: R)(f: (T,R) => R): List[R] = { this match { case Nil() => z :: Nil[R]() case Cons(h, t) => - val rest@Cons(h1,_) = t.scanRight(z)(f) + val rest@Cons(h1,_) = t.scanRight(z)(f): @unchecked f(h, h1) :: rest }} ensuring { !_.isEmpty } @@ -810,7 +810,7 @@ object ListSpecs { require (!l.isEmpty) (l.head == l.reverse.last) }.holds because { - val Cons(x, xs) = l; + val Cons(x, xs) = l: @unchecked; { (x :: xs).head ==| trivial | x ==| snocLast(xs.reverse, x) | diff --git a/frontends/library/stainless/lang/Either.scala b/frontends/library/stainless/lang/Either.scala index 6d938bb9c3..c216e2f6ea 100644 --- a/frontends/library/stainless/lang/Either.scala +++ b/frontends/library/stainless/lang/Either.scala @@ -26,7 +26,7 @@ sealed abstract class Either[A, B] { def get: B = { require(isRight) - val Right(value) = this + val Right(value) = this: @unchecked value } } diff --git a/frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala b/frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala index 9a20cf2e0b..8bd8871c52 100644 --- a/frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala +++ b/frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala @@ -366,7 +366,7 @@ trait CodeExtraction extends ASTExtractors { } private def extractObject(obj: ModuleDef): (xt.ModuleDef, Seq[xt.ClassDef], Seq[xt.FunDef], Seq[xt.TypeDef], Option[Identifier]) = { - val ExObjectDef(_, template) = obj + val ExObjectDef(_, template) = obj: @unchecked val (imports, classes, functions, typeDefs, subs, allClasses, allFunctions, allTypeDefs, companionOf) = extractStatic(template.body) diff --git a/project/build.properties b/project/build.properties index bb3a9b7dc6..6a9f038894 100644 --- a/project/build.properties +++ b/project/build.properties @@ -1 +1 @@ -sbt.version=1.5.6 +sbt.version=1.7.3