Dump benchmark data about repair, pretty printing in browser

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"

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)

src/main/scala/leon/utils/Benchmarks.scala

+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)
+    ))
+  }
+}

testcases/repair/report.html

+<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>