Foundations for testing performance, simplify SBT build

Performance tests are invoked via "sbt perf:test". Currently testing
performance of CEGIS on some random synthesis problems

build.sbt

@@ -7,28 +7,97 @@ organization := "ch.epfl.lara"
 scalaVersion := "2.11.6"
 
 scalacOptions ++= Seq(
-    "-deprecation",
-    "-unchecked",
-    "-feature"
+  "-deprecation",
+  "-unchecked",
+  "-feature"
 )
 
 javacOptions += "-Xlint:unchecked"
 
-
 if(System.getProperty("sun.arch.data.model") == "64") {
   unmanagedBase <<= baseDirectory { base => base / "unmanaged" / "64" }
 } else {
   unmanagedBase <<= baseDirectory { base => base / "unmanaged" / "32" }
 }
 
-resolvers += "Typesafe Repository" at "http://repo.typesafe.com/typesafe/releases/"
+resolvers ++= Seq(
+  "Typesafe Repository" at "http://repo.typesafe.com/typesafe/releases/",
+  "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots"
+)
 
 libraryDependencies ++= Seq(
-    "org.scala-lang" % "scala-compiler" % "2.11.6",
-    "org.scalatest" %% "scalatest" % "2.2.0" % "test",
-    "com.typesafe.akka" %% "akka-actor" % "2.3.4"
+  "org.scala-lang" % "scala-compiler" % "2.11.6",
+  "org.scalatest" %% "scalatest" % "2.2.0" % "test",
+  "com.typesafe.akka" %% "akka-actor" % "2.3.4",
+  "com.storm-enroute" %% "scalameter" % "0.7-SNAPSHOT" % "test"
 )
 
+lazy val scriptName = "leon"
+
+lazy val scriptFile = file(".") / scriptName
+
+clean := {
+  clean.value
+
+  if(scriptFile.exists && scriptFile.isFile) {
+    scriptFile.delete
+  }
+}
+
+lazy val script = taskKey[Unit]("Generate the leon Bash script")
+
+script := {
+  val s = streams.value
+
+  try {
+    val cps = (dependencyClasspath in Compile).value
+    val out = (classDirectory      in Compile).value
+    val res = (resourceDirectory   in Compile).value
+
+    val is64 = System.getProperty("sun.arch.data.model") == "64"
+
+    val f = scriptFile
+    // Paths discovery
+    if(f.exists) {
+      s.log.info("Regenerating '"+f.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
+      f.delete
+    } else {
+      s.log.info("Generating '"+f.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
+    }
+
+    val paths = (res.getAbsolutePath +: out.getAbsolutePath +: cps.map(_.data.absolutePath)).mkString(":")
+
+    IO.write(f, s"""|#!/bin/bash --posix
+                    |
+                    |SCALACLASSPATH="$paths"
+                    |
+                    |java -Xmx2G -Xms512M -classpath $${SCALACLASSPATH} -Dscala.usejavacp=false scala.tools.nsc.MainGenericRunner -classpath $${SCALACLASSPATH} leon.Main $$@ 2>&1 | tee -i last.log
+                    |""".stripMargin)
+
+    f.setExecutable(true)
+  } catch {
+    case e: Throwable =>
+      s.log.error("There was an error while generating the script file: " + e.getLocalizedMessage)
+  }
+}
+
+sourceGenerators in Compile <+= Def.task {
+  val libFiles = ((baseDirectory.value / "library") ** "*.scala").getPaths
+
+  val build = (sourceManaged in Compile).value / "leon" / "Build.scala";
+
+  IO.write(build, s"""|package leon;
+                    |
+                    |object Build {
+                    |  val libFiles = List(
+                    |    ${libFiles.mkString("\"\"\"", "\"\"\",\n    \"\"\"", "\"\"\"")}
+                    |  )
+                    |}""".stripMargin)
+
+  Seq(build)
+}
+
+
 Keys.fork in run := true
 
 Keys.fork in Test := true
@@ -37,10 +106,32 @@ logBuffered in Test := false
 
 javaOptions in Test ++= Seq("-Xss16M", "-Xmx4G", "-XX:MaxPermSize=128M")
 
+testFrameworks += new TestFramework("org.scalameter.ScalaMeterFramework")
+
 parallelExecution in Test := false
 
-testOptions in (Test, test) := Seq(Tests.Filter(s => s.endsWith("LeonAllTests")), Tests.Argument("-oDF"))
+testOptions in (Test, test) := Seq(Tests.Filter(s => s.endsWith("LeonAllTests")), Tests.Argument(TestFrameworks.ScalaCheck, "-oDF"))
 
-testOptions in (Test, testOnly) := Seq(Tests.Argument("-oDF"))
+testOptions in (Test, testOnly) := Seq(Tests.Argument(TestFrameworks.ScalaCheck, "-oDF"))
 
 sourcesInBase in Compile := false
+
+lazy val PerfTest = config("perf") extend(Test)
+
+scalaSource in PerfTest := baseDirectory.value / "src/test/scala/"
+
+parallelExecution in PerfTest := false
+
+testOptions in (PerfTest, test) := Seq(Tests.Filter(s => s.endsWith("PerfTest")))
+
+def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
+
+lazy val bonsai      = ghProject("git://github.com/colder/bonsai.git",     "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
+
+lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "711e9a1ef994935482bc83ff3795a94f637f0a04")
+
+lazy val root = (project in file(".")).
+  configs(PerfTest).
+  dependsOn(bonsai, scalaSmtLib).
+  settings(inConfig(PerfTest)(Defaults.testSettings): _*)
+

project/Build.scala

-import sbt._
-import Process._
-import Keys._
-
-object Leon extends Build {
-  private val scriptName      = "leon"
-
-  def scriptFile      = file(".") / scriptName
-
-  def is64 = System.getProperty("sun.arch.data.model") == "64"
-  def ldLibraryDir32 = file(".") / "lib-bin" / "32"
-  def ldLibraryDir64 = file(".") / "lib-bin" / "64"
-
-  val cleanTask = TaskKey[Unit]("clean", "Cleans up the generated binaries and scripts.") <<= (streams, clean) map { (s,c) =>
-    if(scriptFile.exists && scriptFile.isFile) {
-      scriptFile.delete
-    }
-  }
-
-  val nl = System.getProperty("line.separator")
-
-  val scriptTask = TaskKey[Unit]("script", "Generate the leon Bash script") <<= (streams, dependencyClasspath in Compile, classDirectory in Compile, resourceDirectory in Compile) map { (s, cps, out, res) =>
-    try {
-      val f = file("leon")
-      // Paths discovery
-      if(f.exists) {
-        s.log.info("Regenerating '"+f.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
-        f.delete
-      } else {
-        s.log.info("Generating '"+f.getName+"' script ("+(if(is64) "64b" else "32b")+")...")
-      }
-
-      val paths = (res.getAbsolutePath +: out.getAbsolutePath +: cps.map(_.data.absolutePath)).mkString(":")
-
-      IO.write(f, s"""|#!/bin/bash --posix
-                      |
-                      |SCALACLASSPATH="$paths"
-                      |
-                      |java -Xmx2G -Xms512M -classpath $${SCALACLASSPATH} -Dscala.usejavacp=false scala.tools.nsc.MainGenericRunner -classpath $${SCALACLASSPATH} leon.Main $$@ 2>&1 | tee -i last.log
-                      |""".stripMargin)
-
-      f.setExecutable(true)
-    } catch {
-      case e: Throwable =>
-        s.log.error("There was an error while generating the script file: " + e.getLocalizedMessage)
-    }
-  }
-
-  val sourceGen = {
-    sourceGenerators in Compile += Def.task {
-      val libFiles = ((baseDirectory.value / "library") ** "*.scala").getPaths
-
-      val build = (sourceManaged in Compile).value / "leon" / "Build.scala";
-
-      IO.write(build, s"""|package leon;
-                          |
-                          |object Build {
-                          |  val libFiles = List(
-                          |    ${libFiles.mkString("\"\"\"", "\"\"\",\n    \"\"\"", "\"\"\"")}
-                          |  )
-                          |}""".stripMargin)
-
-      Seq(build)
-    }.taskValue
-  }
-
-  object LeonProject {
-    val settings = Seq(
-      scriptTask,
-      cleanTask,
-      sourceGen
-    )
-  }
-
-  lazy val root = Project(
-    id = "leon",
-    base = file("."),
-    settings = Project.defaultSettings ++ LeonProject.settings
-  ).dependsOn(Github.bonsai, Github.scalaSmtLib)
-
-  object Github {
-    def project(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
-
-    lazy val bonsai      = project("git://github.com/colder/bonsai.git",     "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
-    lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "711e9a1ef994935482bc83ff3795a94f637f0a04")
-  }
-}

src/test/resources/regression/performance/cegis/Add.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Numerals {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n: Num): BigInt = {
+    n match {
+      case Z => 0
+      case S(p) => 1 + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x: Num, y: Num): Num = {
+    choose { (r: Num) =>
+      value(r) == value(x) + value(y)
+    }
+  }
+}

src/test/resources/regression/performance/cegis/Distinct.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Numerals {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n: Num): BigInt = {
+    n match {
+      case Z => 0
+      case S(p) => 1 + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x: Num, y: Num): Num = (x match {
+    case Z => y
+    case S(p) => add(p, S(y))
+  }) ensuring (value(_) == value(x) + value(y))
+
+  def distinct(x: Num, y: Num): Num = {
+    choose { (r : Num) =>
+      r != x && r != y
+    }
+  }
+}

src/test/resources/regression/performance/cegis/Hole1.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+object Holes {
+  def abs3(a: Int) = {
+    if (?(a > 0, a < 0)) {
+      a
+    } else {
+      -a
+    }
+  } ensuring {
+    _ >= 0
+  }
+}

src/test/resources/regression/performance/cegis/Length.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.collection._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Length {
+
+  def foo(l : List[Int]) : Int = 
+    choose { res:Int => (l, res) passes {
+      case Nil() => 0
+      case Cons(a, Nil()) => 2
+      case Cons(_, Cons(_, Cons(_, Cons(_, Nil())))) => 8
+    }}
+
+}

src/test/resources/regression/performance/cegis/Mult.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Numerals {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n: Num): BigInt = {
+    n match {
+      case Z => 0
+      case S(p) => 1 + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x: Num, y: Num): Num = (x match {
+    case Z => y
+    case S(p) => add(p, S(y))
+  }) ensuring (value(_) == value(x) + value(y))
+
+  def mult(x: Num, y: Num): Num = {
+    choose { (r: Num) =>
+      value(r) == value(x) * value(y)
+    }
+  }
+}

src/test/resources/regression/performance/cegis/Squared.scala

+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Numerals {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n:Num) : BigInt = {
+    n match {
+      case Z => 0
+      case S(p) => 1 + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x: Num, y: Num): Num = (x match {
+    case Z => y
+    case S(p) => add(p, S(y))
+  }) ensuring (value(_) == value(x) + value(y))
+
+  def mult(x: Num, y: Num): Num = (y match {
+    case S(p) =>
+      add(mult(x, p), x)
+    case Z =>
+      Z
+  }) ensuring { value(_) == value(x) * value(y) }
+
+  def squared(x: Num): Num = {
+    choose { (r: Num) =>
+      value(r) == value(x) * value(x)
+    }
+  }
+}

src/test/scala/leon/test/performance/CegisPerformance.scala

+import leon._
+import leon.synthesis._
+import leon.synthesis.rules._
+import leon.test._
+import leon.utils._
+import leon.frontends.scalac._
+import leon.purescala.Definitions._
+import org.scalameter.picklers.noPickler._
+
+import org.scalameter.api._
+
+class CegisPerfTest extends PerformanceTest.OfflineRegressionReport {
+
+  override def persistor = new SerializationPersistor
+  override def executor: Executor = LocalExecutor(warmer, aggregator, measurer)
+
+
+  val lt = new LeonTestSuite{}
+
+  val ctxPrograms = for (f <- lt.filesInResourceDir("regression/performance/cegis/", _.endsWith(".scala"))) yield {
+    val extraction =
+      ExtractionPhase andThen
+      PreprocessingPhase
+
+    val leonReporter = new TestSilentReporter
+
+    val paths = List(f.getPath)
+    val ctx = Main.processOptions(paths).copy(reporter = leonReporter,
+                                                       interruptManager = new InterruptManager(leonReporter))
+
+    (f.getName.dropRight(6), ctx, extraction.run(ctx)(paths))
+  }
+
+  val cegisRules = List(
+    OnePoint,
+    Ground,
+    UnusedInput,
+    EquivalentInputs,
+    UnconstrainedOutput,
+    CEGIS,
+    Assert
+  )
+
+  val settings =  SynthesisSettings(timeoutMs = Some(20000), rules = cegisRules)
+
+  performance of "CEGIS" in {
+    for ((name, ctx, pgm) <- ctxPrograms) {
+      measure.method(name) in {
+        using(Gen.unit("test")) in { _ =>
+          val cis = ChooseInfo.extractFromProgram(pgm).filterNot(_.fd.annotations("library"))
+          for (ci <- cis) {
+            val synth = new Synthesizer(ctx, pgm, ci, settings)
+            val s = synth.getSearch
+            val sols = s.search(synth.sctx)
+          }
+        }
+      }
+    }
+  }
+
+}