diff --git a/build.sbt b/build.sbt
index 0df51cc0a0474424c9bf8a67ae8d8d73b98ed688..9c519eef89773aa0dcca229fc1adc9e5c695f0ee 100644
--- a/build.sbt
+++ b/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): _*)
+
diff --git a/project/Build.scala b/project/Build.scala
deleted file mode 100644
index 40f4e2a8e6a94b1296d9d4fccccdce4ea1654a97..0000000000000000000000000000000000000000
--- a/project/Build.scala
+++ /dev/null
@@ -1,87 +0,0 @@
-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")
- }
-}
diff --git a/src/test/resources/regression/performance/cegis/Add.scala b/src/test/resources/regression/performance/cegis/Add.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5931eeb591cf61567d285e68fee9bb49f7c19c07
--- /dev/null
+++ b/src/test/resources/regression/performance/cegis/Add.scala
@@ -0,0 +1,24 @@
+/* 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)
+ }
+ }
+}
diff --git a/src/test/resources/regression/performance/cegis/Distinct.scala b/src/test/resources/regression/performance/cegis/Distinct.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a6fb4881c471d936e3627dcc7dd42e1189bdb89c
--- /dev/null
+++ b/src/test/resources/regression/performance/cegis/Distinct.scala
@@ -0,0 +1,29 @@
+/* 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
+ }
+ }
+}
diff --git a/src/test/resources/regression/performance/cegis/Hole1.scala b/src/test/resources/regression/performance/cegis/Hole1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..354dcb72cefbaa8dd9fb30c4fb10045346c98b96
--- /dev/null
+++ b/src/test/resources/regression/performance/cegis/Hole1.scala
@@ -0,0 +1,17 @@
+/* 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
+ }
+}
diff --git a/src/test/resources/regression/performance/cegis/Length.scala b/src/test/resources/regression/performance/cegis/Length.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2e38e0a1898f67a8bea01a4be5c674943a13dc8c
--- /dev/null
+++ b/src/test/resources/regression/performance/cegis/Length.scala
@@ -0,0 +1,16 @@
+/* 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
+ }}
+
+}
diff --git a/src/test/resources/regression/performance/cegis/Mult.scala b/src/test/resources/regression/performance/cegis/Mult.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9f8f422c689d741bf076605615e3f8cdf3039354
--- /dev/null
+++ b/src/test/resources/regression/performance/cegis/Mult.scala
@@ -0,0 +1,29 @@
+/* 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)
+ }
+ }
+}
diff --git a/src/test/resources/regression/performance/cegis/Squared.scala b/src/test/resources/regression/performance/cegis/Squared.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5d7877469d3cf5015b703e179fde86b8a6a234ea
--- /dev/null
+++ b/src/test/resources/regression/performance/cegis/Squared.scala
@@ -0,0 +1,36 @@
+/* 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)
+ }
+ }
+}
diff --git a/src/test/scala/leon/test/performance/CegisPerformance.scala b/src/test/scala/leon/test/performance/CegisPerformance.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7613168c7ded6c2d188ac987fb93d53c5cf9da55
--- /dev/null
+++ b/src/test/scala/leon/test/performance/CegisPerformance.scala
@@ -0,0 +1,61 @@
+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)
+ }
+ }
+ }
+ }
+ }
+
+}