More loggin and automation

runTests.sh

+#!/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
+

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

src/main/scala/leon/repair/RepairResult.scala

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

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)