From bf8ef03eff6c220081ff60ada5983f7532ed74dd Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 9 Oct 2015 15:14:12 +0200
Subject: [PATCH] Get VerificationSuite up to date
---
.../isabelle/IsabelleVerificationSuite.scala | 10 +---
.../PureScalaVerificationSuite.scala | 5 --
.../verification/VerificationSuite.scala | 60 +++++++++----------
3 files changed, 30 insertions(+), 45 deletions(-)
diff --git a/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala b/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala
index 9892bdbf4..628a523ad 100644
--- a/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala
+++ b/src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala
@@ -1,16 +1,12 @@
package leon.isabelle
-import leon._
-import leon.regression.verification._
-import leon.solvers.isabelle.AdaptationPhase
-import leon.test._
-import leon.verification.AnalysisPhase
+import leon.regression.verification.VerificationSuite
class IsabelleVerificationSuite extends VerificationSuite {
val testDir = "regression/verification/isabelle/"
- val pipeFront = xlang.NoXLangFeaturesChecking
- val pipeBack = AdaptationPhase andThen AnalysisPhase
+ override val isabelle = true
+
val optionVariants: List[List[String]] = List(List("--isabelle:download=true", "--solvers=isabelle"))
}
diff --git a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
index b1ee19996..c54ec2b59 100644
--- a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
@@ -3,9 +3,6 @@
package leon.regression
package verification
-import leon._
-import leon.verification.AnalysisPhase
-
import _root_.smtlib.interpreters._
// If you add another regression test, make sure it contains one object whose name matches the file name
@@ -13,8 +10,6 @@ import _root_.smtlib.interpreters._
class PureScalaVerificationSuite extends VerificationSuite {
val testDir = "regression/verification/purescala/"
- val pipeFront = xlang.NoXLangFeaturesChecking
- val pipeBack = AnalysisPhase
val optionVariants: List[List[String]] = {
val isZ3Available = try {
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index 63bf613d1..dd8b08879 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -5,12 +5,15 @@ package leon.regression.verification
import leon._
import leon.test._
-import leon.verification.VerificationReport
+import leon.utils.UniqueCounter
+import leon.verification.{AnalysisPhase, VerificationReport}
import leon.purescala.Definitions.Program
import leon.frontends.scalac.ExtractionPhase
import leon.utils.PreprocessingPhase
+import leon.solvers.isabelle.AdaptationPhase
+import leon.xlang.FixReportLabels
-import org.scalatest.{Reporter => TestReporter, _}
+import org.scalatest.{Reporter => _, _}
// If you add another regression test, make sure it contains one object whose name matches the file name
// This is because we compile all tests from each folder separately.
@@ -20,28 +23,28 @@ trait VerificationSuite extends LeonRegressionSuite {
val testDir: String
val ignored: Seq[String] = Seq()
+ val desugarXLang: Boolean = false
+ val isabelle: Boolean = false
- private var counter: Int = 0
- private def nextInt(): Int = {
- counter += 1
- counter
- }
+ private val counter = new UniqueCounter[Unit]
+ counter.nextGlobal // Start with 1
- private[verification] case class Output(report: VerificationReport, reporter: Reporter)
-
- val pipeFront: Pipeline[Program, Program]
- val pipeBack : Pipeline[Program, VerificationReport]
+ private case class Output(report: VerificationReport, reporter: Reporter)
- private def mkTest(files: List[String], cat: String, forError: Boolean)(block: Output => Unit) = {
+ private def mkTest(files: List[String], cat: String)(block: Output => Unit) = {
val extraction =
ExtractionPhase andThen
- new PreprocessingPhase andThen // Warning: If XLang at some point inherits this, we need to fix this line
- pipeFront
+ new PreprocessingPhase(desugarXLang)
+
+ val analysis =
+ (if (isabelle) AdaptationPhase else NoopPhase[Program]) andThen
+ AnalysisPhase andThen
+ (if (desugarXLang) FixReportLabels else NoopPhase[VerificationReport])
val ctx = createLeonContext(files:_*)
try {
- val (ctx2, ast) = extraction.run(ctx, files)
+ val (_, ast) = extraction.run(ctx, files)
val programs = {
val (user, lib) = ast.units partition { _.isMainUnit }
user map ( u => Program(u :: lib) )
@@ -50,7 +53,7 @@ trait VerificationSuite extends LeonRegressionSuite {
val displayName = s"$cat/${p.units.head.id.name}.scala"
- val index = nextInt()
+ val index = counter.nextGlobal
val ts = if (ignored exists (_.endsWith(displayName)))
ignore _
else
@@ -58,15 +61,8 @@ trait VerificationSuite extends LeonRegressionSuite {
ts(f"$index%3d: $displayName ${options.mkString(" ")}", Seq()) {
val ctx = createLeonContext(options: _*)
- if (forError) {
- intercept[LeonFatalError] {
- pipeBack.run(ctx, p)
- }
- }
- else {
- val (ctx2, report) = pipeBack.run(ctx, p)
- block(Output(report, ctx2.reporter))
- }
+ val (ctx2, report) = analysis.run(ctx, p)
+ block(Output(report, ctx2.reporter))
}
}
} catch {
@@ -83,7 +79,7 @@ trait VerificationSuite extends LeonRegressionSuite {
}
}
- private[verification] def forEachFileIn(cat: String, forError: Boolean)(block: Output => Unit) {
+ private[verification] def forEachFileIn(cat: String)(block: Output => Unit) {
val fs = filesInResourceDir(testDir + cat, _.endsWith(".scala")).toList
fs foreach { file =>
@@ -93,11 +89,11 @@ trait VerificationSuite extends LeonRegressionSuite {
val files = fs map { _.getPath }
- mkTest(files, cat, forError)(block)
+ mkTest(files, cat)(block)
}
override def run(testName: Option[String], args: Args): Status = {
- forEachFileIn("valid", false) { output =>
+ forEachFileIn("valid") { output =>
val Output(report, reporter) = output
for ((vc, vr) <- report.vrs if vr.isInvalid) {
fail(s"The following verification condition was invalid: $vc @${vc.getPos}")
@@ -108,7 +104,7 @@ trait VerificationSuite extends LeonRegressionSuite {
reporter.terminateIfError()
}
- forEachFileIn("invalid", false) { output =>
+ forEachFileIn("invalid") { output =>
val Output(report, _) = output
assert(report.totalUnknown === 0,
"There should not be unknown verification conditions.")
@@ -116,19 +112,17 @@ trait VerificationSuite extends LeonRegressionSuite {
"There should be at least one invalid verification condition.")
}
- forEachFileIn("unknown", false) { output =>
+ forEachFileIn("unknown") { output =>
val Output(report, reporter) = output
for ((vc, vr) <- report.vrs if vr.isInvalid) {
fail(s"The following verification condition was invalid: $vc @${vc.getPos}")
}
assert(report.totalUnknown > 0,
- "There should be at least one unknown verification conditions.")
+ "There should be at least one unknown verification condition.")
reporter.terminateIfError()
}
- forEachFileIn("error", true) { _ => () }
-
super.run(testName, args)
}
}
--
GitLab