diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala index 3884b00c0fe0b7eefb99d68a04aa0d528afe9672..839dda206b4a702ad5011049a38c76d7dcd21478 100644 --- a/src/main/scala/leon/SharedOptions.scala +++ b/src/main/scala/leon/SharedOptions.scala @@ -18,6 +18,8 @@ object SharedOptions extends LeonComponent { val optStrictPhases = LeonFlagOptionDef("strict", "Terminate after each phase if there is an error", true) + val optBenchmark = LeonFlagOptionDef("benchmark", "Dump benchmarking information in a data file", false) + val optXLang = LeonFlagOptionDef("xlang", "Support for extra program constructs (imperative,...)", false) val optWatch = LeonFlagOptionDef("watch", "Rerun pipeline when file changes", false) @@ -71,6 +73,7 @@ object SharedOptions extends LeonComponent { override val definedOptions: Set[LeonOptionDef[Any]] = Set( optStrictPhases, + optBenchmark, optXLang, optFunctions, optSelectedSolvers, diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala index 26216a3c2510982046b534d91e5679cf63e33925..4f33a52bcad13061572f2811510b0d9ea6ed90c9 100644 --- a/src/main/scala/leon/repair/Repairman.scala +++ b/src/main/scala/leon/repair/Repairman.scala @@ -30,7 +30,7 @@ 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 + val doBenchmark = ctx.findOptionOrDefault(SharedOptions.optBenchmark) var program = initProgram @@ -81,7 +81,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout val timeVerify = timer.stop - if (storeBenchmarks) { + if (doBenchmark) { val be = (BenchmarkEntry.fromContext(ctx) ++ Map( "function" -> fd.id.name, "time_tests" -> timeTests, diff --git a/testcases/repair/report.html b/testcases/repair/report.html index 09aca483a9786fdf1bd97b4733f66a67f6eca94a..91a45bc552688cadbe3f77c7a6c11d29c95eebb0 100644 --- a/testcases/repair/report.html +++ b/testcases/repair/report.html @@ -10,9 +10,9 @@ } function initGraph(data) { - $('#container').highcharts({ + $('#overview').highcharts({ title: { - text: 'Leon Benchmarks', + text: 'Overview', x: -20 //center }, @@ -34,7 +34,6 @@ }, tooltip: { headerFormat: '<b>{series.name}</b><br>', - pointFormat: '{point.x:%e. %b}: {point.y:,.0f} ms' }, legend: { @@ -56,10 +55,74 @@ }); } + function specificGraph(serie) { + var dataTests = []; + var dataRepair = []; + var dataVerification = []; + + for (var i = 0, r; r = serie.data[i]; i++) { + dataTests.push([1000*r.ts, r.time_tests]); + dataVerification.push([1000*r.ts, r.time_verification]); + dataRepair.push([1000*r.ts, r.time_synthesis]); + } + + $('#specific').highcharts({ + chart: { + type: 'area' + }, + title: { + text: serie.name + }, + 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: { + pointFormat: '{point.y:,.0f} ms' + }, + plotOptions: { + area: { + stacking: 'normal', + lineColor: '#666666', + lineWidth: 1, + marker: { + lineWidth: 1, + lineColor: '#666666' + } + } + }, + series: [{ + name: 'Verification', + data: dataVerification + }, { + name: 'Repair', + data: dataRepair + }, { + name: 'Tests', + data: dataTests + }] + }); + } + + var data = []; + var dataMap = {} + $(function () { - function processData(data) { - var seriesMap = {}; + function processData() { + dataMap = {}; for (var i = 0, r; r = data[i]; i++) { var parts = r.files.split("/") @@ -70,26 +133,59 @@ "data": [] }; - if (name in seriesMap) { - serie = seriesMap[name] + if (name in dataMap) { + serie = dataMap[name] } - serie.data.push([1000 * r.ts, r.time_synthesis+r.time_tests]) + serie.data.push(r) + +/*)*/ - seriesMap[name] = serie + dataMap[name] = serie } - console.log(seriesMap) + } + function overviewGraph() { var res = []; - for (k in seriesMap) { - res.push(seriesMap[k]) + for (k in dataMap) { + var serie = dataMap[k]; + + res.push({ + "name": serie.name, + "data": serie.data.map(function(r) { + return { + x: 1000 * r.ts, + y: r.time_synthesis+r.time_tests, + t: r.time_tests, + r: r.time_synthesis + }; + }) + }) } initGraph(res) } + function specificGraphs() { + var sel = ['<option value=""> -- Select one -- </option>'] + + for (s in dataMap) { + var r = dataMap[s] + sel.push('<option value="'+s+'">'+r.name+'</option>'); + } + + $("#graphSelect").html(sel.join("")); + + $("#graphSelect").unbind("change").change(function() { + var sel = $(this).find(":selected").val() + + specificGraph(dataMap[sel]); + }); + + } + function handleFileSelect(evt) { var files = evt.target.files; // FileList object @@ -101,8 +197,12 @@ reader.onload = (function(theFile) { return function(e) { - var json = JSON.parse(e.target.result); - processData(json) + data = JSON.parse(e.target.result); + + processData() + + overviewGraph() + specificGraphs() }; })(f); @@ -118,6 +218,10 @@ <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> + <h2>Overview</h2> + <div id="overview" style="min-width: 310px; height: 400px; margin: 0 auto"></div> + <h2>Details</h2> + <select id="graphSelect"></select> + <div id="specific" style="min-width: 310px; height: 400px; margin: 0 auto"></div> </body> </html>