diff --git a/build.sbt b/build.sbt
index 17791adabb504fb507fcf6869308b866761494e6..99f751a6511689c1d6a5ce368d9ebde284ff16d2 100644
--- a/build.sbt
+++ b/build.sbt
@@ -29,7 +29,8 @@ 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",
- "com.storm-enroute" %% "scalameter" % "0.7-SNAPSHOT" % "test"
+ "com.storm-enroute" %% "scalameter" % "0.7-SNAPSHOT" % "test",
+ "com.fasterxml.jackson.module" %% "jackson-module-scala" % "2.6.0-rc2"
)
lazy val scriptName = "leon"
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 43349bffc42ed8c43010db6d249178cb0ecdbbdc..26216a3c2510982046b534d91e5679cf63e33925 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -30,6 +30,8 @@ import scala.concurrent.duration._
class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeoutMs: Option[Long], repairTimeoutMs: Option[Long]) {
val reporter = ctx.reporter
+ val storeBenchmarks = true
+
var program = initProgram
implicit val debugSection = DebugSectionRepair
@@ -41,6 +43,8 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
to.interruptAfter(repairTimeoutMs) {
reporter.info(ASCIIHelpers.title("1. Discovering tests for "+fd.id))
+ val timer = new Timer().start
+
val tb = discoverTests()
if (tb.invalids.nonEmpty) {
@@ -61,11 +65,38 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
printer(tb2.asString("Minimal Failing Tests"))
}
+ val timeTests = timer.stop
+ timer.start
+
val synth = getSynthesizer(tb2)
try {
reporter.info(ASCIIHelpers.title("3. Synthesizing repair"))
- val (search, solutions) = synth.validate(synth.synthesize(), allowPartial = false)
+ val (search0, sols0) = synth.synthesize()
+
+ val timeSynth = timer.stop
+ timer.start
+
+ val (search, solutions) = synth.validate((search0, sols0), allowPartial = false)
+
+ val timeVerify = timer.stop
+
+ if (storeBenchmarks) {
+ val be = (BenchmarkEntry.fromContext(ctx) ++ Map(
+ "function" -> fd.id.name,
+ "time_tests" -> timeTests,
+ "time_synthesis" -> timeSynth,
+ "time_verification" -> timeVerify,
+ "success" -> solutions.nonEmpty,
+ "verified" -> solutions.forall(_._2)
+ ))
+
+ val bh = new BenchmarksHistory("repairs.dat")
+
+ bh += be
+
+ bh.write
+ }
if (synth.settings.generateDerivationTrees) {
val dot = new DotGenerator(search.g)
diff --git a/src/main/scala/leon/utils/Benchmarks.scala b/src/main/scala/leon/utils/Benchmarks.scala
new file mode 100644
index 0000000000000000000000000000000000000000..39b635ba96dbed6ce0ef0f6b51011e165dd5319e
--- /dev/null
+++ b/src/main/scala/leon/utils/Benchmarks.scala
@@ -0,0 +1,70 @@
+package leon
+package utils
+
+import java.io.{File, PrintWriter}
+import scala.io.Source
+
+import com.fasterxml.jackson.databind.{DeserializationFeature, ObjectMapper}
+import com.fasterxml.jackson.module.scala.experimental.ScalaObjectMapper
+import com.fasterxml.jackson.module.scala.DefaultScalaModule
+
+import java.text._
+import java.util.Date
+
+class BenchmarksHistory(file: File) {
+
+ def this(name: String) = {
+ this(new File(name))
+ }
+
+ val mapper = new ObjectMapper() with ScalaObjectMapper
+ mapper.registerModule(DefaultScalaModule)
+
+ private[this] var entries: List[BenchmarkEntry] = {
+ if (file.exists) {
+ val str = Source.fromFile(file).mkString
+
+ mapper.readValue[List[Map[String, Any]]](str).map(BenchmarkEntry(_))
+ } else {
+ Nil
+ }
+ }
+
+ def write(): Unit = {
+ val json = mapper.writeValueAsString(entries.map(_.fields))
+ val pw = new PrintWriter(file)
+ try {
+ pw.write(json)
+ } finally {
+ pw.close
+ }
+ }
+
+ def +=(be: BenchmarkEntry) {
+ entries :+= be
+ }
+
+}
+
+case class BenchmarkEntry(fields: Map[String, Any]) {
+ def +(s: String, v: Any) = {
+ copy(fields + (s -> v))
+ }
+
+ def ++(es: Map[String, Any]) = {
+ copy(fields ++ es)
+ }
+}
+
+object BenchmarkEntry {
+ def fromContext(ctx: LeonContext) = {
+ val date = new Date()
+
+ BenchmarkEntry(Map(
+ "files" -> ctx.files.map(_.getAbsolutePath).mkString(" "),
+ "options" -> ctx.options.mkString(" "),
+ "date" -> new SimpleDateFormat("yyyy-MM-dd HH:mm:ss").format(date),
+ "ts" -> (System.currentTimeMillis() / 1000L)
+ ))
+ }
+}
diff --git a/testcases/repair/report.html b/testcases/repair/report.html
new file mode 100644
index 0000000000000000000000000000000000000000..2634d343c2df19a8a558e87d41840e4ecbf11d14
--- /dev/null
+++ b/testcases/repair/report.html
@@ -0,0 +1,123 @@
+<html>
+ <head>
+ <script src="http://code.jquery.com/jquery-1.11.3.min.js"></script>
+ <script src="http://code.highcharts.com/highcharts.js"></script>
+<script>
+ if (window.File && window.FileReader && window.FileList && window.Blob) {
+ // Great success! All the File APIs are supported.
+ } else {
+ alert('The File APIs are not fully supported in this browser.');
+ }
+
+ function initGraph(data) {
+ $('#container').highcharts({
+ title: {
+ text: 'Leon Benchmarks',
+ x: -20 //center
+ },
+
+ xAxis: {
+ type: 'datetime',
+ dateTimeLabelFormats: { // don't display the dummy year
+ month: '%e. %b',
+ year: '%b'
+ },
+ title: {
+ text: 'Date'
+ }
+ },
+ yAxis: {
+ title: {
+ text: 'Time (ms)'
+ },
+ min: 0
+ },
+ tooltip: {
+ headerFormat: '<b>{series.name}</b><br>',
+ pointFormat: '{point.x:%e. %b}: {point.y:.2f} ms'
+ },
+
+ legend: {
+ layout: 'vertical',
+ align: 'right',
+ verticalAlign: 'middle',
+ borderWidth: 0
+ },
+
+ plotOptions: {
+ spline: {
+ marker: {
+ enabled: true
+ }
+ }
+ },
+
+ series: data
+ });
+ }
+
+ $(function () {
+
+ function processData(data) {
+ var seriesMap = {};
+
+ for (var i = 0, r; r = data[i]; i++) {
+ var parts = r.files.split("/")
+ var name = parts[parts.length-1]+' '+r.function
+
+ var serie = {
+ "name": name,
+ "data": []
+ };
+
+ if (name in seriesMap) {
+ serie = seriesMap[name]
+ }
+
+ serie.data.push([1000 * r.ts, r.time_synthesis])
+
+ seriesMap[name] = serie
+ }
+
+ console.log(seriesMap)
+
+ var res = [];
+
+ for (k in seriesMap) {
+ res.push(seriesMap[k])
+ }
+
+ initGraph(res)
+ }
+
+ function handleFileSelect(evt) {
+ var files = evt.target.files; // FileList object
+
+ graphData = [];
+ // files is a FileList of File objects. List some properties.
+
+ for (var i = 0, f; f = files[i]; i++) {
+ var reader = new FileReader();
+
+ reader.onload = (function(theFile) {
+ return function(e) {
+ var json = JSON.parse(e.target.result);
+ processData(json)
+ };
+ })(f);
+
+ reader.readAsText(f)
+ }
+ }
+
+ document.getElementById('fileLoader').addEventListener('change', handleFileSelect, false);
+ });
+</script>
+ </head>
+ <body>
+ <h1>Leon Benchmarks</h1>
+ <h2>Load Data</h2>
+ <input type="file" id="fileLoader" name="data" />
+ <div id="container" style="min-width: 310px; height: 400px; margin: 0 auto"></div>
+ </body>
+</html>