Optimize and refactor verification tests

src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala

@@ -6,7 +6,7 @@ import leon._
 import leon.test._
 
 import leon.verification.{AnalysisPhase,VerificationReport}
-
+import leon.purescala.Definitions.Program
 import leon.frontends.scalac.ExtractionPhase
 import leon.utils.PreprocessingPhase
 
@@ -14,55 +14,14 @@ import _root_.smtlib.interpreters._
 
 import java.io.File
 
-class PureScalaVerificationRegression extends LeonTestSuite {
-  private var counter : Int = 0
-  private def nextInt() : Int = {
-    counter += 1
-    counter
-  }
-  private case class Output(report : VerificationReport, reporter : Reporter)
-
-  private def mkPipeline : Pipeline[List[String], VerificationReport] =
-    ExtractionPhase                andThen
-    PreprocessingPhase             andThen
-    xlang.NoXLangFeaturesChecking  andThen
-    AnalysisPhase
-
-  private def mkTest(file : File, leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {
-    val fullName = file.getPath()
-    val start = fullName.indexOf("regression")
-
-    val displayName = if(start != -1) {
-      fullName.substring(start, fullName.length)
-    } else {
-      fullName
-    }
-
-    test("%3d: %s %s".format(nextInt(), displayName, leonOptions.mkString(" "))) {
-      assert(file.exists && file.isFile && file.canRead,
-             "Benchmark %s is not a readable file".format(displayName))
-
-      val ctx = createLeonContext((file.getPath +: leonOptions) :_*)
-
-      val pipeline = mkPipeline
-
-      if(forError) {
-        intercept[LeonFatalError]{
-          pipeline.run(ctx)(file.getPath :: Nil)
-        }
-      } else {
-        val report = pipeline.run(ctx)(file.getPath :: Nil)
-
-        block(Output(report, ctx.reporter))
-      }
-    }
-  }
-
-  private def forEachFileIn(cat : String, forError: Boolean = false)(block : Output=>Unit) {
-    val fs = filesInResourceDir(
-      "regression/verification/purescala/" + cat,
-      _.endsWith(".scala"))
-
+// 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 PureScalaVerificationRegression extends VerificationRegression {
+  
+  val testDir = "regression/verification/purescala/"
+  val pipeFront = xlang.NoXLangFeaturesChecking
+  val pipeBack = AnalysisPhase
+  val optionVariants: List[List[String]] = {
     val isZ3Available = try {
       new Z3Interpreter()
       true
@@ -73,24 +32,22 @@ class PureScalaVerificationRegression extends LeonTestSuite {
 
     val isCVC4Available = try {
       new CVC4Interpreter()
-      // @EK: CVC4 works on most testcases already, but not all and thus cannot be used in regression.
       true
+      // @EK: CVC4 works on most testcases already, but not all and thus cannot be used in regression.
     } catch {
       case e: java.io.IOException =>
         false
     }
 
-    for(f <- fs) {
-      mkTest(f, List("--feelinglucky"), forError)(block)
-      mkTest(f, List("--codegen", "--evalground", "--feelinglucky"), forError)(block)
-      mkTest(f, List("--solvers=fairz3,enum", "--codegen", "--evalground", "--feelinglucky"), forError)(block)
-      if (isZ3Available) {
-        mkTest(f, List("--solvers=smt-z3", "--feelinglucky"), forError)(block)
-      }
-      if (isCVC4Available) {
-        mkTest(f, List("--solvers=smt-cvc4", "--feelinglucky"), forError)(block)
-      }
-    }
+    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
+    )
   }
   
   forEachFileIn("valid") { output =>

src/test/scala/leon/test/verification/VerificationRegression.scala

+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.test.verification
+
+import leon._
+import leon.test._
+
+import leon.verification.VerificationReport
+import leon.purescala.Definitions.Program
+import leon.frontends.scalac.ExtractionPhase
+import leon.utils.PreprocessingPhase
+
+import _root_.smtlib.interpreters._
+
+import java.io.File
+
+// 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.
+trait VerificationRegression extends LeonTestSuite {
+
+  val optionVariants: List[List[String]]
+  val testDir: String
+
+  private var counter : Int = 0
+  private def nextInt() : Int = {
+    counter += 1
+    counter
+  }
+  private[verification] case class Output(report : VerificationReport, reporter : Reporter)
+ 
+  val pipeFront: Pipeline[Program, Program]
+  val pipeBack : Pipeline[Program, VerificationReport]
+
+  private def mkTest(files: List[String], leonOptions : Seq[String], forError: Boolean)(block: Output=>Unit) = {
+    val extraction = 
+      ExtractionPhase andThen
+      PreprocessingPhase andThen
+      pipeFront
+
+    if(forError) {
+      intercept[LeonFatalError]{
+        extraction.run(createLeonContext((files ++ leonOptions):_*))(files)
+      }
+    } else {
+      val ctx = createLeonContext(leonOptions:_*)
+      val ast = extraction.run(createLeonContext((files ++ leonOptions):_*))(files)
+      val programs = {
+        val (user, lib) = ast.units partition { _.isMainUnit }
+        user map { u => Program(u.id.freshen, u :: lib) }
+      }
+      for (p <- programs; displayName = p.id.name) test("%3d: %s %s".format(nextInt(), displayName, leonOptions.mkString(" "))) {
+        val report = pipeBack.run(ctx)(p)
+        block(Output(report, ctx.reporter))
+      }
+    }
+  }
+
+  private[verification] def forEachFileIn(cat : String, forError: Boolean = false)(block : Output=>Unit) {
+    val fs = filesInResourceDir( testDir + cat, _.endsWith(".scala")).toList
+
+    fs foreach { file => 
+      assert(file.exists && file.isFile && file.canRead,
+        "Benchmark %s is not a readable file".format(file.getName))
+    }
+
+    val files = fs map { _.getPath }
+
+    // If error, try to verify each file separately (and fail for each one)
+    val groupedFiles = if (forError) files map (List(_)) else List(files)
+
+    for (files <- groupedFiles; options <- optionVariants) {
+      mkTest(files, options, forError)(block)
+    }
+  }
+  
+  
+}