Setting up the stage for CodeGen

src/main/scala/leon/codegen/CodeGen.scala

+package leon
+package codegen
+
+import purescala.Common._
+import purescala.Definitions._
+
+object CodeGenPhase extends LeonPhase[Program,CompilationResult] {
+  val name = "CodeGen"
+  val description = "Compiles a Leon program into Java methods"
+
+  def run(ctx : LeonContext)(p : Program) : CompilationResult = {
+    CompilationResult(successful = true)
+  } 
+}

src/main/scala/leon/codegen/CompilationResult.scala

+package leon
+package codegen
+
+case class CompilationResult(
+  successful : Boolean = false
+)

src/test/resources/regression/codegen/purescala/Prog001.scala

+object Prog001 {
+  def plus(x : Int, y : Int) : Int = x + y
+}

src/test/resources/regression/codegen/purescala/README

+This directory contains PureScala programs for which compilation (codegen)
+should always succeed entirely.

src/test/scala/leon/test/Test.scala

-package leon.test
-
-import org.scalatest.FunSuite
-
-class Test extends FunSuite {
-  test("Tests work.") {
-    assert(true)
-  }
-}

src/test/scala/leon/test/TestUtils.scala

+package leon
+package test
+
+import java.io.File
+
+object TestUtils {
+  private val all : String=>Boolean = (s : String) => true
+
+  def filesInResourceDir(dir : String, filter : String=>Boolean = all) : Iterable[File] = {
+    import scala.collection.JavaConversions._
+
+    val d = this.getClass.getClassLoader.getResource(dir)
+
+    if(d == null || d.getProtocol != "file") {
+      assert(false, "Tests have to be run from within `sbt`, for otherwise the test files will be harder to access (and we dislike that).")
+    }
+
+    val asFile = new File(d.toURI())
+
+    asFile.listFiles().filter(f => filter(f.getPath()))
+  }
+}

src/test/scala/leon/test/codegen/CodeGenRegression.scala

+package leon.test
+package codegen
+
+import leon._
+import leon.plugin.ExtractionPhase
+import leon.codegen.CodeGenPhase
+import leon.codegen.CompilationResult
+
+import org.scalatest.FunSuite
+
+import java.io.File
+
+import TestUtils._
+
+class CodeGenRegression extends FunSuite {
+  private var counter : Int = 0
+  private def nextInt() : Int = {
+    counter += 1
+    counter
+  }
+
+  private case class Output(result : CompilationResult, reporter : Reporter)
+
+  private def mkPipeline : Pipeline[List[String],CompilationResult] =
+    ExtractionPhase andThen CodeGenPhase
+
+  private def mkTest(file : File)(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("PureScala program %3d: [%s]".format(nextInt(), displayName)) {
+      assert(file.exists && file.isFile && file.canRead,
+             "Benchmark [%s] is not a readable file".format(displayName))
+      val ctx = LeonContext(
+        settings = Settings(
+          synthesis = false,
+          xlang     = false,
+          verify    = false
+        ),
+        files = List(file),
+        reporter = new SilentReporter
+      )
+
+      val pipeline = mkPipeline
+
+      val result = pipeline.run(ctx)(file.getPath :: Nil)
+
+      block(Output(result, ctx.reporter))
+    }
+  }
+
+  private def forEachFileIn(cat : String)(block : Output=>Unit) {
+    val fs = filesInResourceDir(
+      "regression/codegen/" + cat,
+      _.endsWith(".scala"))
+
+    for(f <- fs) {
+      mkTest(f)(block)
+    }
+  }
+  
+  forEachFileIn("purescala") { output =>
+    val Output(result, reporter) = output
+    assert(result.successful, "Compilation should be successful.")
+    assert(reporter.errorCount === 0)
+    assert(reporter.warningCount === 0)
+  }
+}

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

 package leon
 package test
+package verification
 
 import leon.verification.{AnalysisPhase,VerificationReport}
 
@@ -7,7 +8,9 @@ import org.scalatest.FunSuite
 
 import java.io.File
 
-class PureScalaPrograms extends FunSuite {
+import TestUtils._
+
+class PureScalaVerificationRegression extends FunSuite {
   private var counter : Int = 0
   private def nextInt() : Int = {
     counter += 1
@@ -50,22 +53,17 @@ class PureScalaPrograms extends FunSuite {
     }
   }
 
-  private def forEachFileIn(dirName : String)(block : Output=>Unit) {
-    import scala.collection.JavaConversions._
-
-    val dir = this.getClass.getClassLoader.getResource(dirName)
-
-    if(dir == null || dir.getProtocol != "file") {
-      assert(false, "Tests have to be run from within `sbt`, for otherwise " +
-                    "the test files will be harder to access (and we dislike that).")
-    }
+  private def forEachFileIn(cat : String)(block : Output=>Unit) {
+    val fs = filesInResourceDir(
+      "regression/verification/purescala/" + cat,
+      _.endsWith(".scala"))
 
-    for(f <- (new File(dir.toURI())).listFiles() if f.getPath().endsWith(".scala")) {
+    for(f <- fs) {
       mkTest(f)(block)
     }
   }
   
-  forEachFileIn("regression/verification/purescala/valid") { output =>
+  forEachFileIn("valid") { output =>
     val Output(report, reporter) = output
     assert(report.totalConditions === report.totalValid,
            "All verification conditions ("+report.totalConditions+") should be valid.")
@@ -73,7 +71,7 @@ class PureScalaPrograms extends FunSuite {
     assert(reporter.warningCount === 0)
   }
 
-  forEachFileIn("regression/verification/purescala/invalid") { output =>
+  forEachFileIn("invalid") { output =>
     val Output(report, reporter) = output
     assert(report.totalInvalid > 0,
            "There should be at least one invalid verification condition.")