From cec9364181254f1cf5fd4040488fc13ce9c99a83 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 16 Oct 2015 17:59:49 +0200
Subject: [PATCH] Break down slow test suites
---
.../testcases/TestCasesCompile.scala | 17 ++---
.../PureScalaVerificationSuite.scala | 46 ------------
.../verification/VerificationSuite.scala | 57 ++++++++-------
.../PureScalaVerificationSuite.scala | 71 +++++++++++++++++++
4 files changed, 112 insertions(+), 79 deletions(-)
delete mode 100644 src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
create mode 100644 src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
diff --git a/src/test/scala/leon/regression/testcases/TestCasesCompile.scala b/src/test/scala/leon/regression/testcases/TestCasesCompile.scala
index 994a61901..333413721 100644
--- a/src/test/scala/leon/regression/testcases/TestCasesCompile.scala
+++ b/src/test/scala/leon/regression/testcases/TestCasesCompile.scala
@@ -4,11 +4,10 @@ package leon.regression.testcases
import leon._
import leon.test._
-import org.scalatest.time.SpanSugar._
import java.io.File
-import org.scalatest.ParallelTestExecution
-class TestCasesCompile extends LeonRegressionSuite {
+abstract class TestCasesCompile(testDir: String) extends LeonRegressionSuite {
+
val pipeline = frontends.scalac.ExtractionPhase andThen new utils.PreprocessingPhase(desugarXLang = true)
private def filesIn(path : String): Seq[File] = {
@@ -19,11 +18,7 @@ class TestCasesCompile extends LeonRegressionSuite {
val baseDir = "regression/testcases/"
- val allTests = (filesIn(baseDir+"repair/") ++
- filesIn(baseDir+"runtime/") ++
- filesIn(baseDir+"synthesis/") ++
- filesIn(baseDir+"verification/") ++
- filesIn(baseDir+"web/")).sortBy(_.getAbsolutePath)
+ val allTests = filesIn(baseDir + testDir)
allTests.foreach { f =>
@@ -45,3 +40,9 @@ class TestCasesCompile extends LeonRegressionSuite {
}
}
}
+
+class TestcasesCompile1 extends TestCasesCompile("repair/")
+class TestcasesCompile2 extends TestCasesCompile("runtime/")
+class TestcasesCompile3 extends TestCasesCompile("synthesis/")
+class TestcasesCompile4 extends TestCasesCompile("verification/")
+class TestcasesCompile5 extends TestCasesCompile("web/")
\ No newline at end of file
diff --git a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
deleted file mode 100644
index c54ec2b59..000000000
--- a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
+++ /dev/null
@@ -1,46 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon.regression
-package verification
-
-import _root_.smtlib.interpreters._
-
-// 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.
-class PureScalaVerificationSuite extends VerificationSuite {
-
- val testDir = "regression/verification/purescala/"
-
- val optionVariants: List[List[String]] = {
- val isZ3Available = try {
- Z3Interpreter.buildDefault.free()
- true
- } catch {
- case e: java.io.IOException =>
- false
- }
-
- val isCVC4Available = try {
- CVC4Interpreter.buildDefault.free()
- true
- } catch {
- case e: java.io.IOException =>
- false
- }
-
- List(
- List("--feelinglucky"),
- List("--codegen", "--evalground", "--feelinglucky"),
- List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky")
- ) ++ (
- if (isZ3Available) List(
- List("--solvers=smt-z3", "--feelinglucky")
- ) else Nil
- ) ++ (
- if (isCVC4Available) List(
- List("--solvers=smt-cvc4", "--feelinglucky")
- ) else Nil
- )
- }
-
-}
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index c3bdc3067..06b00e0bb 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -91,37 +91,44 @@ trait VerificationSuite extends LeonRegressionSuite {
mkTest(files, cat)(block)
}
- override def run(testName: Option[String], args: Args): Status = {
- 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}")
- }
- for ((vc, vr) <- report.vrs if vr.isInconclusive) {
- fail(s"The following verification condition was inconclusive: $vc @${vc.getPos}")
- }
- reporter.terminateIfError()
+ protected def testValid() = 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}")
}
-
- forEachFileIn("invalid") { output =>
- val Output(report, _) = output
- assert(report.totalUnknown === 0,
- "There should not be unknown verification conditions.")
- assert(report.totalInvalid > 0,
- "There should be at least one invalid verification condition.")
+ for ((vc, vr) <- report.vrs if vr.isInconclusive) {
+ fail(s"The following verification condition was inconclusive: $vc @${vc.getPos}")
}
+ reporter.terminateIfError()
+ }
- 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 condition.")
+ protected def testInvalid() = forEachFileIn("invalid") { output =>
+ val Output(report, _) = output
+ assert(report.totalUnknown === 0,
+ "There should not be unknown verification conditions.")
+ assert(report.totalInvalid > 0,
+ "There should be at least one invalid verification condition.")
+ }
- reporter.terminateIfError()
+ protected def testUnknown() = 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 condition.")
+
+ reporter.terminateIfError()
+ }
+ protected def testAll() = {
+ testValid()
+ testInvalid()
+ testUnknown()
+ }
+
+ override def run(testName: Option[String], args: Args): Status = {
+ testAll()
super.run(testName, args)
}
}
diff --git a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
new file mode 100644
index 000000000..d308e840f
--- /dev/null
+++ b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
@@ -0,0 +1,71 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.regression.verification
+package purescala
+
+import smtlib.interpreters.{CVC4Interpreter, Z3Interpreter}
+
+// 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 together.
+abstract class PureScalaVerificationSuite extends VerificationSuite {
+
+ val testDir = "regression/verification/purescala/"
+
+ val isZ3Available = try {
+ Z3Interpreter.buildDefault.free()
+ true
+ } catch {
+ case e: java.io.IOException =>
+ false
+ }
+
+ val isCVC4Available = try {
+ CVC4Interpreter.buildDefault.free()
+ true
+ } catch {
+ case e: java.io.IOException =>
+ false
+ }
+
+ val opts: List[List[String]] = {
+ List(
+ List("--feelinglucky"),
+ List("--codegen", "--evalground", "--feelinglucky"),
+ List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky")
+ ) ++ (
+ if (isZ3Available) List(
+ List("--solvers=smt-z3", "--feelinglucky")
+ ) else Nil
+ ) ++ (
+ if (isCVC4Available) List(
+ List("--solvers=smt-cvc4", "--feelinglucky")
+ ) else Nil
+ )
+ }
+
+}
+
+trait PureScalaValidSuite extends PureScalaVerificationSuite {
+ override def testAll() = testValid()
+}
+
+class PureScalaValidSuite1 extends PureScalaValidSuite {
+ val optionVariants = List(opts(0))
+}
+class PureScalaValidSuite2 extends PureScalaValidSuite {
+ val optionVariants = List(opts(1))
+}
+class PureScalaValidSuite3 extends PureScalaValidSuite {
+ val optionVariants = List(opts(2))
+}
+class PureScalaValidSuiteZ3 extends PureScalaValidSuite {
+ val optionVariants = if (isZ3Available) List(opts(3)) else Nil
+}
+class PureScalaValidSuiteCVC4 extends PureScalaValidSuite {
+ val optionVariants = if (isCVC4Available) List(opts(4)) else Nil
+}
+
+class PureScalaInvalidSuite extends PureScalaVerificationSuite {
+ override def testAll() = testInvalid()
+ val optionVariants = opts
+}
--
GitLab