Break down slow test suites

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

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)
   }
 }

src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala → src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala

 /* Copyright 2009-2015 EPFL, Lausanne */
 
-package leon.regression
-package verification
+package leon.regression.verification
+package purescala
 
-import _root_.smtlib.interpreters._
+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 separately.
-class PureScalaVerificationSuite extends VerificationSuite {
-  
+// This is because we compile all tests from each folder together.
+abstract 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
-    }
+  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"),
@@ -44,3 +44,28 @@ class PureScalaVerificationSuite extends VerificationSuite {
   }
 
 }
+
+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
+}