From b65b4746dcd7b06a16cf15f430e0f5821f8990af Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Tue, 3 Feb 2015 00:55:26 +0100
Subject: [PATCH] More loggin and automation
---
runTests.sh | 38 +++++++++++++++++++
src/main/scala/leon/repair/RepairPhase.scala | 10 ++++-
src/main/scala/leon/repair/RepairResult.scala | 24 ++++++++++++
src/main/scala/leon/repair/Repairman.scala | 30 ++++++++++++---
4 files changed, 96 insertions(+), 6 deletions(-)
create mode 100755 runTests.sh
create mode 100644 src/main/scala/leon/repair/RepairResult.scala
diff --git a/runTests.sh b/runTests.sh
new file mode 100755
index 000000000..1e71fac49
--- /dev/null
+++ b/runTests.sh
@@ -0,0 +1,38 @@
+#!/bin/bash
+log=repairs.last
+fullLog=repairs.log
+
+echo -n "" > $log;
+
+
+echo "################################" >> $fullLog
+echo "#" `hostname` >> $fullLog
+echo "#" `date +"%d.%m.%Y %T"` >> $fullLog
+echo "#" `git log -1 --pretty=format:"%h - %cd"` >> $fullLog
+echo "################################" >> $fullLog
+echo "# Category, File, function, S, f.S, Tms, Fms, Rms, verif?" >> $fullLog
+
+#All benchmarks:
+./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar1.scala
+./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar2.scala
+./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar3.scala
+./leon --repair --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar4.scala
+
+./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort3.scala
+./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort4.scala
+./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort8.scala
+./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort6.scala
+./leon --repair --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort7.scala
+./leon --repair --solvers=fairz3:enum --functions=insert testcases/repair/HeapSort/HeapSort5.scala
+./leon --repair --solvers=fairz3:enum --functions=makeN testcases/repair/HeapSort/HeapSort9.scala
+
+./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic1.scala
+./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic2.scala
+./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic3.scala
+./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic4.scala
+./leon --repair --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic5.scala
+
+# Average results
+cat $log >> $fullLog
+awk '{ total1 += $6; total2 += $7; total3 += $8; count++ } END { printf "#%69s Avg: %5d, %5d, %5d\n\n", "", total1/count, total2/count, total3/count }' $log >> $fullLog
+
diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
index 34616f594..7714b679b 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -11,6 +11,8 @@ import purescala.TypeTrees._
import purescala.Constructors._
import purescala.DefOps._
+import java.io.FileWriter
+
object RepairPhase extends LeonPhase[Program, Program] {
val name = "Repair"
val description = "Repairing"
@@ -47,7 +49,13 @@ object RepairPhase extends LeonPhase[Program, Program] {
if (toRepair.isEmpty) reporter.warning("No functions found with the given names")
for (fd <- toRepair) {
- new Repairman(ctx, program, fd, verifTimeoutMs).repair()
+ val res = new Repairman(ctx, program, fd, verifTimeoutMs).repair()
+ val fw = new FileWriter("repairs.last", true)
+ try {
+ fw.write(res.toLine)
+ } finally {
+ fw.close
+ }
}
program
diff --git a/src/main/scala/leon/repair/RepairResult.scala b/src/main/scala/leon/repair/RepairResult.scala
new file mode 100644
index 000000000..6d0dba0b1
--- /dev/null
+++ b/src/main/scala/leon/repair/RepairResult.scala
@@ -0,0 +1,24 @@
+package leon
+package repair
+
+import java.io.File
+
+case class RepairResult(f: File,
+ size: Int = -1,
+ name: String = "?",
+ initTime: Option[Long] = None,
+ focusTime: Option[Long] = None,
+ focusSize: Option[Int] = None,
+ repairTime: Option[Long] = None,
+ repairTrusted: Option[Boolean] = None) {
+
+ def toLine = {
+ val benchCat = f.getParentFile().getName()
+ val benchName = f.getName()
+ val benchFun = name
+
+ f"$benchCat%20s, $benchName%20s, $benchFun%20s, $size%3s, ${focusSize.getOrElse("")}%3s, ${initTime.getOrElse("")}%5s, ${focusTime.getOrElse("")}%5s, ${repairTime.getOrElse("")}%5s, ${repairTrusted.getOrElse("")}%5s\n"
+ }
+
+}
+
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index b14e7b6cb..5989941f3 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -37,9 +37,11 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
case class NotValid(passing : List[Example], failing : List[Example]) extends VerificationResult
}
+ var result = RepairResult(ctx.files.head, 0);
+
import VRes._
- def repair() = {
+ def repair(): RepairResult = {
reporter.info(ASCIIHelpers.title("1. Discovering tests for "+fd.id))
val t1 = new Timer().start
discoverTests match {
@@ -49,7 +51,9 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
reporter.info(f" - Passing: ${passingTests.size}%3d")
reporter.info(f" - Failing: ${failingTests.size}%3d")
- reporter.info("Finished in "+t1.stop+"ms")
+ val initTime = t1.stop
+ result = result.copy(initTime = Some(initTime))
+ reporter.info("Finished in "+initTime+"ms")
reporter.info(ASCIIHelpers.title("2. Locating/Focusing synthesis problem"))
@@ -59,12 +63,15 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val p = synth.problem
var solutions = List[Solution]()
+ val focusTime = t2.stop
+ result = result.copy(focusTime = Some(focusTime))
- reporter.info("Finished in "+t2.stop+"ms")
+ reporter.info("Finished in "+focusTime+"ms")
reporter.info(ASCIIHelpers.title("3. Synthesizing"))
reporter.info(p)
+ val t3 = new Timer().start
synth.synthesize() match {
case (search, sols) =>
for (sol <- sols) {
@@ -81,14 +88,17 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
case NotValid(_, _) =>
solutions ::= sol
reporter.warning("Solution is not trusted!")
+ result = result.copy(repairTrusted = Some(false))
case Valid =>
solutions ::= sol
reporter.info("Solution was not trusted but post-validation passed!")
+ result = result.copy(repairTrusted = Some(true))
}
} else {
reporter.info("Found trusted solution!")
solutions ::= sol
+ result = result.copy(repairTrusted = Some(true))
}
}
@@ -100,6 +110,8 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
if (solutions.isEmpty) {
reporter.error(ASCIIHelpers.title("Failed to repair!"))
} else {
+ result = result.copy(repairTime = Some(t3.stop))
+
reporter.info(ASCIIHelpers.title("Repair successful:"))
for ((sol, i) <- solutions.reverse.zipWithIndex) {
reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+":"))
@@ -124,6 +136,8 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
}
}
}
+
+ result
}
def getSynthesizer(passingTests: List[Example], failingTests: List[Example]): Synthesizer = {
@@ -133,8 +147,14 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val (newBody, replacedExpr) = focusRepair(program, fd, passingTests, failingTests)
fd.body = Some(newBody)
- reporter.info("Original body size: "+formulaSize(body))
- reporter.info("Focused expr size : "+formulaSize(replacedExpr))
+
+ val size = formulaSize(body)
+ val focusSize = formulaSize(replacedExpr)
+
+ reporter.info("Original body size: "+size)
+ reporter.info("Focused expr size : "+focusSize)
+
+ result = result.copy(name = fd.id.name, size = size, focusSize = Some(focusSize))
val guide = Guide(replacedExpr)
--
GitLab