From 2491b9f4a3f0c3609c033a3553563b5549f31304 Mon Sep 17 00:00:00 2001 From: mario-bucev Date: Sun, 27 Nov 2022 22:39:04 +0100 Subject: [PATCH] Remove old VC gen (#1347) --- .larabot.conf | 2 +- .../main/scala/stainless/MainHelpers.scala | 1 - core/src/main/scala/stainless/Report.scala | 7 +- .../verification/DefaultTactic.scala | 145 ------------------ .../scala/stainless/verification/Tactic.scala | 54 ------- .../verification/VerificationComponent.scala | 14 +- .../verification/VerificationGenerator.scala | 51 ------ .../scala/stainless/ComponentTestSuite.scala | 4 +- .../src/it/scala/stainless/LibrarySuite.scala | 5 - .../termination/TerminationSuite.scala | 1 - .../TerminationVerificationSuite.scala | 1 - .../verification/TypeCheckerSuite.scala | 94 ------------ .../verification/VerificationSuite.scala | 79 ++++------ .../verification/InliningSuite.scala | 4 +- 14 files changed, 41 insertions(+), 421 deletions(-) delete mode 100644 core/src/main/scala/stainless/verification/DefaultTactic.scala delete mode 100644 core/src/main/scala/stainless/verification/Tactic.scala delete mode 100644 core/src/main/scala/stainless/verification/VerificationGenerator.scala delete mode 100644 frontends/common/src/it/scala/stainless/verification/TypeCheckerSuite.scala diff --git a/.larabot.conf b/.larabot.conf index 6b7b4c8418..7d322f3e57 100644 --- a/.larabot.conf +++ b/.larabot.conf @@ -1,6 +1,6 @@ commands = [ "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\"" + "sbt -batch -Dtest-parallelism=5 \"it:testOnly stainless.GhostRewriteSuite stainless.GenCSuite stainless.ScalacExtractionSuite stainless.LibrarySuite stainless.verification.SMTZ3VerificationSuite stainless.verification.SMTZ3UncheckedSuite stainless.verification.TerminationVerificationSuite stainless.verification.ImperativeSuite stainless.verification.FullImperativeSuite stainless.verification.StrictArithmeticSuite stainless.verification.CodeGenVerificationSuite stainless.verification.SMTCVC4VerificationSuite stainless.verificatoin.SMTCVC4UncheckedSuite stainless.termination.TerminationSuite\"" ] nightly { diff --git a/core/src/main/scala/stainless/MainHelpers.scala b/core/src/main/scala/stainless/MainHelpers.scala index f06f8ec4c9..5ff349c294 100644 --- a/core/src/main/scala/stainless/MainHelpers.scala +++ b/core/src/main/scala/stainless/MainHelpers.scala @@ -51,7 +51,6 @@ trait MainHelpers extends inox.MainHelpers { self => verification.optAdmitAll -> Description(Verification, "Admit all obligations when translated into a coq program"), verification.optStrictArithmetic -> Description(Verification, s"Check arithmetic operations for unintended behavior and overflows (default: true)"), - verification.optTypeChecker -> Description(Verification, "Use the type-checking rules from the calculus to generate verification conditions"), verification.optAdmitVCs -> Description(Verification, "Admit all verification conditions"), verification.optSimplifier -> Description(Verification, "Select which simplifier to use for VC simplification\n" + "Available:\n" + diff --git a/core/src/main/scala/stainless/Report.scala b/core/src/main/scala/stainless/Report.scala index 0411ae6166..ae4acb43d7 100644 --- a/core/src/main/scala/stainless/Report.scala +++ b/core/src/main/scala/stainless/Report.scala @@ -173,7 +173,6 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType => val sd = prepareExtractionSummaryData val admitted = ctx.options.findOptionOrDefault(verification.optAdmitVCs) val termOff = ctx.options.findOptionOrDefault(stainless.termination.optCheckMeasures).isNo - val oldVC = !ctx.options.findOptionOrDefault(verification.optTypeChecker) val cache = ctx.options.findOptionOrDefault(verification.optVCCache) val solvers = ctx.options.findOptionOrDefault(inox.optSelectedSolvers).toSeq.sorted.mkString(", ") val batched = ctx.options.findOptionOrDefault(frontend.optBatchedProgram) @@ -181,7 +180,6 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType => if (isExtendedSummaryOn) { val admitStr = if (admitted) withColor("Admitted VCs", Console.RED, Console.BOLD) else "" val termOffStr = if (termOff) withColor("Termination turned off", Console.RED, Console.BOLD) else "" - val oldVCStr = if (oldVC) withColor("Old VCs generation", Console.RED, Console.BOLD) else "" val cacheStr = if (cache) "Cache used" else "" def touched(sentance: String, ids: Set[Identifier], prefix: String): String = @@ -216,13 +214,12 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType => val solversUsed = s"Solvers used: $solvers" val procMode = s"Processing mode: ${if (batched) "batched" else "partial"}" - val items = Seq(admitStr, termOffStr, oldVCStr, cacheStr, aaStr, reStr, weStr, ieStr, teStr, ceStr, solversUsed, procMode).filter(_.nonEmpty) + val items = Seq(admitStr, termOffStr, cacheStr, aaStr, reStr, weStr, ieStr, teStr, ceStr, solversUsed, procMode).filter(_.nonEmpty) s"""Verification pipeline summary: |${items.mkString(" ", "\n ", "")}""".stripMargin // No join(items) here as their sub-items are already split according to the character limit } else { val admitStr = if (admitted) withColor("admitted VCs", Console.RED, Console.BOLD) else "" val termOffStr = if (termOff) withColor("termination off", Console.RED, Console.BOLD) else "" - val oldVCStr = if (oldVC) withColor("old VCs gen", Console.RED, Console.BOLD) else "" val cacheStr = if (cache) "cache" else "" val aaStr = if (sd.antiAliasing.hasRun) "anti-aliasing" else "" val reStr = if (sd.retAndWhileTran.hasReturnRun) "return transformation" else "" @@ -231,7 +228,7 @@ trait AbstractReport[SelfType <: AbstractReport[SelfType]] { self: SelfType => val teStr = if (sd.typeEncoding.hasRun) "type encoding" else "" val ceStr = if (sd.chooseInjection.hasRun) withColor("choose injection", Console.YELLOW, Console.BOLD) else "" val batchedStr = if (batched) "batched" else "" - val items = Seq(admitStr, termOffStr, oldVCStr, cacheStr, aaStr, reStr, weStr, ieStr, teStr, ceStr, solvers, batchedStr).filter(_.nonEmpty) + val items = Seq(admitStr, termOffStr, cacheStr, aaStr, reStr, weStr, ieStr, teStr, ceStr, solvers, batchedStr).filter(_.nonEmpty) s"""Verification pipeline summary: |${join(items, prefix = " ")}""".stripMargin } diff --git a/core/src/main/scala/stainless/verification/DefaultTactic.scala b/core/src/main/scala/stainless/verification/DefaultTactic.scala deleted file mode 100644 index d66c0a376b..0000000000 --- a/core/src/main/scala/stainless/verification/DefaultTactic.scala +++ /dev/null @@ -1,145 +0,0 @@ -/* Copyright 2009-2021 EPFL, Lausanne */ - -package stainless -package verification - -trait DefaultTactic extends Tactic { - val description = "Default verification condition generation approach" - - import context.{given, _} - import program._ - import program.trees._ - import program.symbols.{given, _} - - protected def getPostconditions(e: Expr, lambda: Lambda): Seq[Expr] = { - def rec(e: Expr, path: Path): Seq[Expr] = e match { - case NoTree(_) => Seq() - case Let(i, e, b) => rec(b, path withBinding (i -> e)) - case Assert(cond, _, body) => rec(body, path withCond cond) - case IfExpr(c, t, e) => rec(t, path withCond c) ++ rec(e, path withCond not(c)) - case MatchExpr(s, cases) => - var soFar = path - (for (MatchCase(pattern, guard, rhs) <- cases) yield { - val guardOrTrue = guard.getOrElse(BooleanLiteral(true)) - - val patternPath = conditionForPattern[Path](s, pattern, includeBinders = true) - val vcs = rec(rhs, soFar merge (patternPath withCond guardOrTrue)) - - val patternPathNeg = conditionForPattern[Path](s, pattern, includeBinders = false) - val guardMapped = exprOps.replaceFromSymbols(mapForPattern(s, pattern), guardOrTrue) - soFar = soFar merge (patternPathNeg withCond guardMapped).negate - vcs - }).flatten - - case p: Passes => - Seq() - - case _ => - 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 - case _ => false - }).copiedFrom(b) - - if (body != BooleanLiteral(true)) { - Seq((path implies Let(res, e, body).copiedFrom(e)).setPos(e)) - } else { - Seq() - } - } - - 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() - - rec(e, Path.empty) ++ examplesPost - } - - def generatePostconditions(id: Identifier): Seq[VC] = { - val fd = getFunction(id) - (fd.postcondition, fd.body) match { - case (Some(post @ Lambda(Seq(res), _)), Some(body)) if !res.flags.contains(DropVCs) => - getPostconditions(body, post).map { vc => - val vcKind = if (fd.flags.exists(_.name == "law")) VCKind.Law else VCKind.Postcondition - VC(exprOps.freshenLocals(implies(fd.precOrTrue, vc)), id, vcKind, false).setPos(vc) - } - case _ => Nil - } - } - - protected def getPrecondition(pre: Expr): Option[Expr] = pre match { - case TopLevelAnds(es) => - val pred = andJoin(es.filterNot { - case Annotated(e, flags) => flags contains DropConjunct - case _ => false - }).copiedFrom(pre) - - if (pred != BooleanLiteral(true)) { - Some(pred) - } else { - None - } - } - - def generatePreconditions(id: Identifier): Seq[VC] = { - val fd = getFunction(id) - - val calls = collectForConditions { - case (fi: FunctionInvocation, path) if fi.tfd.precondition.isDefined => (fi, path) - }(fd.fullBody) - - calls.flatMap { case (fi @ FunctionInvocation(_, _, args), path) => - getPrecondition(fi.tfd.precondition.get).map { pred => - val pre = fi.tfd.withParamSubst(args, pred) - val vc = path implies exprOps.freshenLocals(pre) - val fiS = sizeLimit(fi.asString, 40) - VC(vc, id, VCKind.Info(VCKind.Precondition, s"call $fiS"), false).setPos(fi) - } - } - } - - // FIXME(gsps): Should also filter individual conjuncts? - protected def annotatedAsUnchecked(e: Expr): Boolean = e match { - case Annotated(_, flags) if flags.contains(DropConjunct) => true - case _ => false - } - - def generateCorrectnessConditions(id: Identifier): Seq[VC] = { - // We don't collect preconditions here, because these are handled by generatePreconditions - collectForConditions { - case (m @ MatchExpr(scrut, cases), path) => - val condition = path implies orJoin(cases map (matchCaseCondition[Path](scrut, _).toClause)) - VC(condition, id, VCKind.ExhaustiveMatch, false).setPos(m) - - case (e @ Error(_, _), path) => - val condition = Not(path.toClause) - VC(condition, id, VCKind.Assert, false).setPos(e) - - case (a @ Assert(cond, optErr, _), path) if !annotatedAsUnchecked(cond) => - val condition = path implies cond - val kind = VCKind.fromErr(optErr) - VC(condition, id, kind, false).setPos(a) - - case (c @ Choose(res, pred), path) if !(res.flags contains DropVCs) => - if (path.conditions.isEmpty && exprOps.variablesOf(c).isEmpty) { - VC(pred, id, VCKind.Info(VCKind.Choose, "check-sat"), true).setPos(c) - } else { - val condition = path implies Not(Forall(Seq(res), Not(pred))) - VC(condition, id, VCKind.Choose, false).setPos(c) - } - - case (a @ ADT(aid, tps, args), path) if a.getConstructor.sort.hasInvariant => - val invId = a.getConstructor.sort.invariant.get.id - val condition = path implies FunctionInvocation(invId, tps, Seq(a)) - VC(condition, id, VCKind.AdtInvariant(invId), false).setPos(a) - }(getFunction(id).fullBody) - } -} - -object DefaultTactic { - def apply(p: StainlessProgram, ctx: inox.Context): DefaultTactic { val program: p.type } = new DefaultTactic { - val program: p.type = p - val context = ctx - } -} diff --git a/core/src/main/scala/stainless/verification/Tactic.scala b/core/src/main/scala/stainless/verification/Tactic.scala deleted file mode 100644 index 3e4dbe4115..0000000000 --- a/core/src/main/scala/stainless/verification/Tactic.scala +++ /dev/null @@ -1,54 +0,0 @@ -/* Copyright 2009-2021 EPFL, Lausanne */ - -package stainless -package verification - -import scala.collection.mutable.ListBuffer - -trait Tactic { - val program: Program - val context: inox.Context - val description: String - - import program.trees._ - import program.symbols.{given, _} - - protected type VC = verification.VC[program.trees.type] - protected def VC(cond: program.trees.Expr, id: Identifier, kind: VCKind, satisfiability: Boolean): VC = - verification.VC(program.trees)(cond, id, kind, satisfiability) - - protected def collectForConditions[T](pf: PartialFunction[(Expr, Path),T])(e: Expr): Seq[T] = { - val results: ListBuffer[T] = new ListBuffer - val lifted = pf.lift - - transformWithPC(e, true /* recurse into types */)((e, path, op) => e match { - case Annotated(_, flags) if flags contains DropVCs => e - case _ => - lifted(e, path).foreach(results += _) - op.sup(e, path) - }) - - results.toList - } - - def generateVCs(id: Identifier): Seq[VC] = { - generatePostconditions(id) ++ - generatePreconditions(id) ++ - generateCorrectnessConditions(id) - } - - def generatePostconditions(id: Identifier): Seq[VC] - def generatePreconditions(id: Identifier): Seq[VC] - def generateCorrectnessConditions(id: Identifier): Seq[VC] - - protected def sizeLimit(s: String, limit: Int) = { - require(limit > 3) - // Crop the call to display it properly - val res = s.takeWhile(_ != '\n').take(limit) - if (res == s) { - res - } else { - res + " ..." - } - } -} diff --git a/core/src/main/scala/stainless/verification/VerificationComponent.scala b/core/src/main/scala/stainless/verification/VerificationComponent.scala index 09598c7999..d41a85a10a 100644 --- a/core/src/main/scala/stainless/verification/VerificationComponent.scala +++ b/core/src/main/scala/stainless/verification/VerificationComponent.scala @@ -18,11 +18,6 @@ import stainless.termination.MeasureInference */ object optStrictArithmetic extends inox.FlagOptionDef("strict-arithmetic", true) -/** - * Generate VC via the System FR type-checker instead of the ad-hoc DefaultTactic. - */ -object optTypeChecker extends inox.FlagOptionDef("type-checker", true) - /** * Verify program using Coq */ @@ -106,13 +101,8 @@ class VerificationRun private(override val component: VerificationComponent.type val vcGenEncoder = assertionEncoder - val vcs = if (context.options.findOptionOrDefault(optTypeChecker)) - context.timers.verification.get("type-checker").run { - TypeChecker(vcGenEncoder.targetProgram, context).checkFunctionsAndADTs(functions) - } - else { - reporter.warning("Old VC generation is deprecated and scheduled for removal in 1.0") - VerificationGenerator.gen(vcGenEncoder.targetProgram, context)(functions) + val vcs = context.timers.verification.get("type-checker").run { + TypeChecker(vcGenEncoder.targetProgram, context).checkFunctionsAndADTs(functions) } if (!functions.isEmpty) { diff --git a/core/src/main/scala/stainless/verification/VerificationGenerator.scala b/core/src/main/scala/stainless/verification/VerificationGenerator.scala deleted file mode 100644 index 62cbb2c1a2..0000000000 --- a/core/src/main/scala/stainless/verification/VerificationGenerator.scala +++ /dev/null @@ -1,51 +0,0 @@ -/* Copyright 2009-2021 EPFL, Lausanne */ - -package stainless -package verification - -trait VerificationGenerator { self => - val program: Program - - import program._ - import program.symbols.{given, _} - import program.trees._ - import CallGraphOrderings.{given, _} - - type VC = verification.VC[program.trees.type] - - protected def getTactic(fd: FunDef): Tactic { val program: self.program.type } - - def generateVCs(funs: Seq[Identifier]): Seq[VC] = { - val vcs: Seq[VC] = (for (id <- funs) yield { - val fd = getFunction(id) - val tactic = getTactic(fd) - - if (exprOps.BodyWithSpecs(fd.fullBody).hasBody) { - tactic.generateVCs(id) - } else { - Nil - } - }).flatten - - vcs.sortBy(vc => (getFunction(vc.fid), - if (vc.kind.underlying == VCKind.Precondition) 0 - else if (vc.kind.underlying == VCKind.Assert) 1 - else 2 - )) - } - -} - -object VerificationGenerator { - - def gen(p: StainlessProgram, ctx: inox.Context)(funs: Seq[Identifier]): Seq[VC[p.trees.type]] = { - object generator extends VerificationGenerator { - val program: p.type = p - - protected def getTactic(fd: p.trees.FunDef) = DefaultTactic(p, ctx) - } - - generator.generateVCs(funs) - } - -} diff --git a/frontends/common/src/it/scala/stainless/ComponentTestSuite.scala b/frontends/common/src/it/scala/stainless/ComponentTestSuite.scala index a2c7d10820..dcc3c3dad1 100644 --- a/frontends/common/src/it/scala/stainless/ComponentTestSuite.scala +++ b/frontends/common/src/it/scala/stainless/ComponentTestSuite.scala @@ -17,7 +17,6 @@ trait ComponentTestSuite extends inox.TestSuite with inox.ResourceUtils with Inp override def configurations: Seq[Seq[inox.OptionValue[_]]] = Seq( Seq( - verification.optTypeChecker(true), inox.optSelectedSolvers(Set("smt-z3:z3-4.8.12")), inox.optTimeout(300.seconds), verification.optStrictArithmetic(false), @@ -31,8 +30,7 @@ trait ComponentTestSuite extends inox.TestSuite with inox.ResourceUtils with Inp override protected def optionsString(options: inox.Options): String = { "solvr=" + options.findOptionOrDefault(inox.optSelectedSolvers).head + " " + "lucky=" + options.findOptionOrDefault(inox.solvers.unrolling.optFeelingLucky) + " " + - "check=" + options.findOptionOrDefault(inox.solvers.optCheckModels) + " " - "type-checker=" + options.findOptionOrDefault(verification.optTypeChecker) + "check=" + options.findOptionOrDefault(inox.solvers.optCheckModels) } protected def filter(ctx: inox.Context, name: String): FilterStatus = Test diff --git a/frontends/common/src/it/scala/stainless/LibrarySuite.scala b/frontends/common/src/it/scala/stainless/LibrarySuite.scala index 23cf73c067..7fb34c4666 100644 --- a/frontends/common/src/it/scala/stainless/LibrarySuite.scala +++ b/frontends/common/src/it/scala/stainless/LibrarySuite.scala @@ -56,11 +56,6 @@ abstract class AbstractLibrarySuite(opts: Seq[inox.OptionValue[_]]) extends AnyF } class LibrarySuite extends AbstractLibrarySuite(Seq( - verification.optTypeChecker(false) -)) - -class TypeCheckerLibrarySuite extends AbstractLibrarySuite(Seq( - verification.optTypeChecker(true), termination.optInferMeasures(true), termination.optCheckMeasures(YesNoOnly.Yes), )) diff --git a/frontends/common/src/it/scala/stainless/termination/TerminationSuite.scala b/frontends/common/src/it/scala/stainless/termination/TerminationSuite.scala index 858dc7998e..da028a2dde 100644 --- a/frontends/common/src/it/scala/stainless/termination/TerminationSuite.scala +++ b/frontends/common/src/it/scala/stainless/termination/TerminationSuite.scala @@ -16,7 +16,6 @@ class TerminationSuite extends VerificationComponentTestSuite { override def configurations = super.configurations.map { seq => Seq( - optTypeChecker(true), optInferMeasures(true), optCheckMeasures(YesNoOnly.Only), ) ++ seq diff --git a/frontends/common/src/it/scala/stainless/verification/TerminationVerificationSuite.scala b/frontends/common/src/it/scala/stainless/verification/TerminationVerificationSuite.scala index ed69c9d6eb..c327f28399 100644 --- a/frontends/common/src/it/scala/stainless/verification/TerminationVerificationSuite.scala +++ b/frontends/common/src/it/scala/stainless/verification/TerminationVerificationSuite.scala @@ -10,7 +10,6 @@ class TerminationVerificationSuite extends VerificationComponentTestSuite { override def configurations = super.configurations.map { seq => Seq( optFailInvalid(true), - verification.optTypeChecker(true), termination.optInferMeasures(false), termination.optCheckMeasures(YesNoOnly.No), ) ++ seq diff --git a/frontends/common/src/it/scala/stainless/verification/TypeCheckerSuite.scala b/frontends/common/src/it/scala/stainless/verification/TypeCheckerSuite.scala deleted file mode 100644 index 36bc2cfa18..0000000000 --- a/frontends/common/src/it/scala/stainless/verification/TypeCheckerSuite.scala +++ /dev/null @@ -1,94 +0,0 @@ -/* Copyright 2009-2021 EPFL, Lausanne */ - -package stainless -package verification - -import scala.concurrent.duration._ - -import org.scalatest._ - -trait TypeCheckerSuite extends VerificationComponentTestSuite { - - override def configurations = super.configurations.map { seq => - Seq(optTypeChecker(true)) ++ seq - } - - override def filter(ctx: inox.Context, name: String): FilterStatus = name match { - case "verification/invalid/ForallAssoc" => Ignore // Hangs - - // unknown/timeout VC but counter-example not found - case "verification/invalid/BadConcRope" => Ignore - - // Lemmas used in one equation can leak in other equations due to https://github.com/epfl-lara/inox/issues/139 - case "verification/invalid/Equations1" => Ignore - case "verification/invalid/Equations2" => Ignore - case "verification/invalid/Equations3" => Ignore - - case _ => super.filter(ctx, name) - } - - // Scala 2 BitVectors tests leverages the fact that `==` can be used to compare two unrelated types. - // For instance, if we have x: Int42, then x == 42 is legal. - // In Scala 3, however, this expression is ill-formed because Int42 and Int (the widened type of 42) are unrelated. - // Therefore, all BitVectors tests for Scala 3 must perform a conversion for literals - // (e.g. the above expression is rewritten to x == (42: Int42)) - def bitVectorsTestDiscarding(file: String): Boolean = { - val scala2BitVectors = Set("MicroTests/scalac/BitVectors1.scala", "MicroTests/scalac/BitVectors2.scala", "MicroTests/scalac/BitVectors3.scala") - val scala3BitVectors = Set("MicroTests/dotty/BitVectors1.scala", "MicroTests/dotty/BitVectors2.scala", "MicroTests/dotty/BitVectors3.scala") - - (isScala3 || !scala3BitVectors.exists(t => file.endsWith(t))) && - (isScala2 || !scala2BitVectors.exists(t => file.endsWith(t))) - } - - testPosAll("verification/valid", recursive = true, bitVectorsTestDiscarding) - - testNegAll("verification/invalid") - - // Tests that should be rejected, but aren't - testPosAll("verification/false-valid") -} - -class SMTZ3TypeCheckerSuite extends TypeCheckerSuite { - override def configurations = super.configurations.map { - seq => Seq( - inox.optSelectedSolvers(Set("smt-z3:z3-4.8.12")), - inox.solvers.optCheckModels(true) - ) ++ seq - } - - override def filter(ctx: inox.Context, name: String): FilterStatus = name match { - case _ => super.filter(ctx, name) - } -} - -class SMTCVC4TypeCheckerSuite extends TypeCheckerSuite { - override def configurations = super.configurations.map { - seq => Seq( - inox.optSelectedSolvers(Set("smt-cvc4")), - inox.solvers.optCheckModels(true) - ) ++ seq - } - - override def filter(ctx: inox.Context, name: String): FilterStatus = name match { - // Same ignores as SMTCVC4VerificationSuite - case "verification/valid/ArraySlice" => Ignore - case "verification/valid/BigIntMonoidLaws" => Ignore - case "verification/valid/BigIntRing" => Ignore - case "verification/valid/ConcRope" => Ignore - case "verification/valid/CovariantList" => Ignore - case "verification/valid/Huffman" => Ignore - case "verification/valid/InnerClasses4" => Ignore - case "verification/valid/Iterables" => Ignore - case "verification/valid/List" => Ignore - case "verification/valid/MoreExtendedEuclidGCD" => Ignore - case "verification/valid/MoreExtendedEuclidReachability" => Ignore - case "verification/valid/Overrides" => Ignore - case "verification/valid/PartialCompiler" => Ignore - case "verification/valid/PartialKVTrace" => Ignore - case "verification/valid/ReachabilityChecker" => Ignore - case "verification/valid/TestPartialFunction" => Ignore - case "verification/valid/TestPartialFunction3" => Ignore - - case _ => super.filter(ctx, name) - } -} diff --git a/frontends/common/src/it/scala/stainless/verification/VerificationSuite.scala b/frontends/common/src/it/scala/stainless/verification/VerificationSuite.scala index ef524a9e34..1be7b3bd71 100644 --- a/frontends/common/src/it/scala/stainless/verification/VerificationSuite.scala +++ b/frontends/common/src/it/scala/stainless/verification/VerificationSuite.scala @@ -3,22 +3,17 @@ package stainless package verification +import scala.concurrent.duration._ + import org.scalatest._ trait VerificationSuite extends VerificationComponentTestSuite { - override def configurations = super.configurations.map { seq => - Seq(optTypeChecker(false)) ++ seq - } - - override protected def optionsString(options: inox.Options): String = { - super.optionsString(options) + - (if (options.findOptionOrDefault(evaluators.optCodeGen)) " codegen" else "") - } - override def filter(ctx: inox.Context, name: String): FilterStatus = name match { - case "verification/valid/Streams" => Ignore // only for TypeCheckerSuite - case "verification/invalid/ForallAssoc" => Ignore // Hangs + case "verification/invalid/ForallAssoc" => Ignore // Hangs + + // unknown/timeout VC but counter-example not found + case "verification/invalid/BadConcRope" => Ignore // Lemmas used in one equation can leak in other equations due to https://github.com/epfl-lara/inox/issues/139 case "verification/invalid/Equations1" => Ignore @@ -28,13 +23,25 @@ trait VerificationSuite extends VerificationComponentTestSuite { case _ => super.filter(ctx, name) } - testPosAll("verification/valid") + // Scala 2 BitVectors tests leverages the fact that `==` can be used to compare two unrelated types. + // For instance, if we have x: Int42, then x == 42 is legal. + // In Scala 3, however, this expression is ill-formed because Int42 and Int (the widened type of 42) are unrelated. + // Therefore, all BitVectors tests for Scala 3 must perform a conversion for literals + // (e.g. the above expression is rewritten to x == (42: Int42)) + def bitVectorsTestDiscarding(file: String): Boolean = { + val scala2BitVectors = Set("MicroTests/scalac/BitVectors1.scala", "MicroTests/scalac/BitVectors2.scala", "MicroTests/scalac/BitVectors3.scala") + val scala3BitVectors = Set("MicroTests/dotty/BitVectors1.scala", "MicroTests/dotty/BitVectors2.scala", "MicroTests/dotty/BitVectors3.scala") + + (isScala3 || !scala3BitVectors.exists(t => file.endsWith(t))) && + (isScala2 || !scala2BitVectors.exists(t => file.endsWith(t))) + } + + testPosAll("verification/valid", recursive = true, bitVectorsTestDiscarding) testNegAll("verification/invalid") // Tests that should be rejected, but aren't testPosAll("verification/false-valid") - } class SMTZ3VerificationSuite extends VerificationSuite { @@ -46,13 +53,6 @@ class SMTZ3VerificationSuite extends VerificationSuite { } override def filter(ctx: inox.Context, name: String): FilterStatus = name match { - // Flaky on smt-z3 for some reason - case "verification/valid/MergeSort2" => Ignore - case "verification/valid/IntSetInv" => Ignore - - // Too slow on smt-z3, even for nightly build - case "verification/valid/BitsTricksSlow" => Skip - case _ => super.filter(ctx, name) } } @@ -81,41 +81,28 @@ class SMTCVC4VerificationSuite extends VerificationSuite { override def configurations = super.configurations.map { seq => Seq( inox.optSelectedSolvers(Set("smt-cvc4")), - inox.solvers.optCheckModels(true), - evaluators.optCodeGen(true) + inox.solvers.optCheckModels(true) ) ++ seq } override def filter(ctx: inox.Context, name: String): FilterStatus = name match { - // Requires non-linear resonning, unsupported by CVC4 - case "verification/valid/Overrides" => Ignore - case "verification/valid/TestPartialFunction" => Ignore - case "verification/valid/TestPartialFunction3" => Ignore - case "verification/valid/BigIntRing" => Ignore + case "verification/valid/ArraySlice" => Ignore case "verification/valid/BigIntMonoidLaws" => Ignore - case "verification/valid/InnerClasses4" => Ignore - - // assertion failed in `compileLambda` - case "verification/valid/GodelNumbering" => Ignore - - // This test is flaky on CVC4 + case "verification/valid/BigIntRing" => Ignore + case "verification/valid/ConcRope" => Ignore case "verification/valid/CovariantList" => Ignore - - // Requires map with non-default values, unsupported by CVC4 - case "verification/valid/ArraySlice" => Ignore + case "verification/valid/Huffman" => Ignore + case "verification/valid/InnerClasses4" => Ignore case "verification/valid/Iterables" => Ignore - - // These tests are too slow on CVC4 and make the regression unstable - case "verification/valid/ConcRope" => Ignore - case "verification/invalid/BadConcRope" => Ignore - - // These tests make CVC4 crash + case "verification/valid/List" => Ignore + case "verification/valid/MoreExtendedEuclidGCD" => Ignore + case "verification/valid/MoreExtendedEuclidReachability" => Ignore + case "verification/valid/Overrides" => Ignore case "verification/valid/PartialCompiler" => Ignore case "verification/valid/PartialKVTrace" => Ignore - - // Codegen assertion error, unsupported by CVC4 - // => Ignored until #681 fixed - case "verification/invalid/BodyEnsuring" => Ignore + case "verification/valid/ReachabilityChecker" => Ignore + case "verification/valid/TestPartialFunction" => Ignore + case "verification/valid/TestPartialFunction3" => Ignore case _ => super.filter(ctx, name) } diff --git a/frontends/common/src/test/scala/stainless/verification/InliningSuite.scala b/frontends/common/src/test/scala/stainless/verification/InliningSuite.scala index b16785c32b..bbfd4ff304 100644 --- a/frontends/common/src/test/scala/stainless/verification/InliningSuite.scala +++ b/frontends/common/src/test/scala/stainless/verification/InliningSuite.scala @@ -52,13 +52,13 @@ class InliningSuite extends AnyFunSuite with InputUtils { test("Conditions of inlined functions should not be checked") { val fun1 = program.lookup[FunDef]("Test.fun1") - val vcs = VerificationGenerator.gen(program, ctx)(Seq(fun1.id)) + val vcs = TypeChecker(program, ctx).checkFunctionsAndADTs(Seq(fun1.id)) assert(vcs.size == 1) } test("Precondition of inlined functions should be checked") { val fun2 = program.lookup[FunDef]("Test.fun2") - val vcs = VerificationGenerator.gen(program, ctx)(Seq(fun2.id)) + val vcs = TypeChecker(program, ctx).checkFunctionsAndADTs(Seq(fun2.id)) assert(vcs.size == 4) } }