Improve timers collection, usage and display

src/main/scala/leon/LeonContext.scala

@@ -16,5 +16,5 @@ case class LeonContext(
   settings: Settings = Settings(),
   options: Seq[LeonOption] = Seq(),
   files: Seq[File] = Seq(),
-  timers: TimerCollections = new TimerCollections
+  timers: TimerStorage = new TimerStorage
 )

src/main/scala/leon/Main.scala

@@ -222,8 +222,6 @@ object Main {
   }
 
   def main(args : Array[String]) {
-    val timer     = new Timer().start
-
     val argsl = args.toList
 
     // By default we add --library from Main
@@ -256,12 +254,10 @@ object Main {
     try {
       ctx.interruptManager.registerSignalHandler()
 
-      ctx.timers.get("Leon Opts") += timer
-
       // Compute leon pipeline
       val pipeline = computePipeline(ctx.settings)
 
-      timer.restart
+      val timer = ctx.timers.total.start()
 
       // Run pipeline
       pipeline.run(ctx)(args.toList) match {
@@ -274,16 +270,10 @@ object Main {
         case _ =>
       }
 
-      ctx.timers.get("Leon Run") += timer
+      timer.stop()
 
       ctx.reporter.whenDebug(DebugSectionTimers) { debug =>
-        debug("-"*80)
-        debug("Times:")
-        debug("-"*80)
-        for ((name, swc) <- ctx.timers.getAll.toSeq.sortBy(_._1)) {
-          debug(swc.toString)
-        }
-        debug("-"*80)
+        ctx.timers.outputTable(debug)
       }
 
     } catch {

src/main/scala/leon/frontends/scalac/ExtractionPhase.scala

@@ -18,6 +18,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
   implicit val debug = DebugSectionTrees
 
   def run(ctx: LeonContext)(args: List[String]): Program = {
+    val timer = ctx.timers.frontend.start()
 
     val settings = new NSCSettings
 
@@ -55,11 +56,14 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
       //   )
       // }
 
+
       val compiler = new ScalaCompiler(settings, ctx)
       val run = new compiler.Run
       run.compile(command.files)
 
 
+      timer.stop()
+
       val pgm = Program(FreshIdentifier("__program"), compiler.leonExtraction.modules)
       ctx.reporter.debug(pgm.asString(ctx))
       pgm

src/main/scala/leon/solvers/EnumerationSolver.scala

@@ -47,6 +47,7 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
   private var modelMap = Map[Identifier, Expr]()
 
   def check: Option[Boolean] = {
+    val timer = context.timers.solvers.enum.check.start()
     val res = try {
       datagen = Some(new VanuatooDataGen(context, program))
       if (interrupted) {
@@ -71,6 +72,7 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
         None
     }
     datagen = None
+    timer.stop()
     res
   }
 

src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala

@@ -181,7 +181,8 @@ trait AbstractZ3Solver
   var isInitialized = false
   protected[leon] def initZ3() {
     if (!isInitialized) {
-      val initTime     = new Timer().start
+      val timer = context.timers.solvers.z3.init.start()
+
       counter = 0
 
       z3 = new Z3Context(z3cfg)
@@ -199,8 +200,7 @@ trait AbstractZ3Solver
 
       isInitialized = true
 
-      initTime.stop
-      context.timers.get("Z3Solver init") += initTime
+      timer.stop()
     }
   }
 

src/main/scala/leon/solvers/z3/FairZ3Solver.scala

@@ -414,9 +414,11 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
       //reporter.debug("Unroll.  Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString("  &&  "))
       //reporter.debug("Userland Assumptions:\n"+assumptionsAsZ3.mkString("  &&  "))
 
+      val timer = context.timers.solvers.z3.check.start()
       solver.push() // FIXME: remove when z3 bug is fixed
       val res = solver.checkAssumptions((assumptionsAsZ3 ++ unrollingBank.z3CurrentZ3Blockers) :_*)
       solver.pop()  // FIXME: remove when z3 bug is fixed
+      timer.stop()
 
       reporter.debug(" - Finished search with blocked literals")
 
@@ -503,9 +505,11 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
               reporter.debug(" - Running search without blocked literals (w/o lucky test)")
             }
 
+            val timer = context.timers.solvers.z3.check.start()
             solver.push() // FIXME: remove when z3 bug is fixed
             val res2 = solver.checkAssumptions(assumptionsAsZ3 : _*)
             solver.pop()  // FIXME: remove when z3 bug is fixed
+            timer.stop
 
             res2 match {
               case Some(false) =>

src/main/scala/leon/synthesis/SimpleSearch.scala

@@ -149,9 +149,9 @@ class SimpleSearch(synth: Synthesizer,
 
 
   def searchStep() {
-    val t = new Timer().start
+    val timer = synth.context.timers.synthesis.nextLeaf.start()
     val nl = nextLeaf()
-    synth.context.timers.get("Synthesis NextLeaf") += t
+    timer.stop()
 
     nl match {
       case Some(l)  =>
@@ -159,15 +159,15 @@ class SimpleSearch(synth: Synthesizer,
           case al: g.AndLeaf =>
             val sub = expandAndTask(al.task)
 
-            t.restart
+            val timer = synth.context.timers.synthesis.expand.start()
             onExpansion(al, sub)
-            synth.context.timers.get("Synthesis Expand") += t
+            timer.stop()
           case ol: g.OrLeaf =>
             val sub = expandOrTask(ol.task)
 
-            t.restart
+            val timer = synth.context.timers.synthesis.expand.start()
             onExpansion(ol, sub)
-            synth.context.timers.get("Synthesis Expand") += t
+            timer.stop()
         }
       case None =>
         stop()

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -41,18 +41,11 @@ class Synthesizer(val context : LeonContext,
         }
       }
 
-    val ts = System.currentTimeMillis()
+    val t = context.timers.synthesis.search.start()
 
     val res = search.search()
 
-    search match {
-      case pr: ParallelSearch =>
-        context.timers.add(pr.expandTimers)
-        context.timers.add(pr.sendWorkTimers)
-      case _ =>
-    }
-
-    val diff = System.currentTimeMillis()-ts
+    val diff = t.stop()
     reporter.info("Finished in "+diff+"ms")
 
     if (options.generateDerivationTrees) {

src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala

@@ -22,9 +22,6 @@ abstract class AndOrGraphParallelSearch[WC,
 
   var system: ActorSystem = _
 
-  val sendWorkTimers = new TimerCollection("Synthesis-par SendWork")
-  val expandTimers   = new TimerCollection("Synthesis-par Expand")
-
   def search(): Option[(S, Boolean)] = {
     system = ActorSystem("ParallelSearch")
 
@@ -96,8 +93,6 @@ abstract class AndOrGraphParallelSearch[WC,
 
       assert(idleWorkers.size > 0)
 
-      val t = new Timer().start
-
       getNextLeaves(idleWorkers, workingWorkers) match {
         case Nil =>
           if (workingWorkers.isEmpty) {
@@ -118,8 +113,6 @@ abstract class AndOrGraphParallelSearch[WC,
             }
           }
       }
-
-      sendWorkTimers += t
     }
 
     context.setReceiveTimeout(10.seconds)
@@ -136,9 +129,7 @@ abstract class AndOrGraphParallelSearch[WC,
       case WorkerAndTaskDone(w, res) =>
         workers.get(w) match {
           case Some(Some(l: g.AndLeaf)) =>
-            val t = new Timer().start
             onExpansion(l, res)
-            expandTimers += t
             workers += w -> None
           case _ =>
         }
@@ -147,9 +138,7 @@ abstract class AndOrGraphParallelSearch[WC,
       case WorkerOrTaskDone(w, res) =>
         workers.get(w) match {
           case Some(Some(l: g.OrLeaf)) =>
-            val t = new Timer().start
             onExpansion(l, res)
-            expandTimers += t
             workers += w -> None
           case _ =>
         }

src/main/scala/leon/utils/Timer.scala

@@ -3,42 +3,13 @@
 package leon
 package utils
 
-class TimerCollection(val name: String) {
-  var min: Long = 0L
-  var tot: Long = 0L
-  var max: Long = 0L
-  var n: Int = 0
-
-  def +=(sw: Timer) = synchronized { 
-    val ms = sw.getMillis
-    if(n == 0 || ms < min) {
-      min = ms
-    }
-    if(n == 0 || ms > max) {
-      max = ms
-    }
-    n   += 1
-    tot += ms
-  }
-
-  override def toString = {
-    if (n == 0) {
-      "%-30s    N/A".format(name+":")
-    } else if (n > 1) {
-      "%-30s %6d ms (min: %d, avg: %d, max: %d, n: %d)".format(name+":", tot, min, tot/n, max, n)
-    } else {
-      "%-30s %6d ms".format(name+":", tot)
-    }
-  }
-
-  def getMillis = tot
-}
+import scala.language.dynamics
 
 /** Implements a timer for profiling purposes */
-class Timer(name: String = "Timer") {
+class Timer() {
   var beginning: Long = 0L
   var end: Long = 0L
-  var acc: Long = 0L
+  var runs: List[Long] = Nil
 
   def start: this.type = {
     beginning = System.currentTimeMillis
@@ -46,45 +17,148 @@ class Timer(name: String = "Timer") {
     this
   }
 
-  def restart: this.type = { 
+  def restart: this.type = {
     beginning = 0L
     end = 0L
-    acc = 0L
+    runs = Nil
 
     start
   }
 
-  def stop {
-    end        = System.currentTimeMillis
-    acc       += (end - beginning)
-    beginning  = 0L
+  def stop = {
+    end         = System.currentTimeMillis
+    runs      ::= (end - beginning)
+    beginning   = 0L
+    runs.head
   }
 
-  def getMillis: Long = {
-    if (isRunning) {
-      acc + (System.currentTimeMillis-beginning)
+  def isRunning = beginning != 0L
+
+  override def toString = {
+    val n = runs.size
+
+    if (n == 0) {
+      "N/A"
+    } else if (n > 1) {
+      val tot = runs.sum
+      val min = runs.min
+      val max = runs.max
+
+      "(min: %3d, avg: %3d, max: %3d, n: %3d) %6d ms".format(min, tot/n, max, n, tot)
     } else {
-      acc
+      val tot = runs.sum
+
+      "%6d ms".format(tot)
     }
   }
+}
 
-  def isRunning = beginning != 0L
+class TimerStorage extends Dynamic {
+  var keys    = List[String]()
+  var fields  = Map[String, TimerStorage]()
+  var selfTimer: Option[Timer] = None
+
+  def get(name: String): TimerStorage = {
+    fields.get(name) match {
+      case Some(t) =>
+        t
+
+      case None =>
+        val t = new TimerStorage()
+        fields += name -> t
+        keys ::= name
+        t
+    }
+  }
 
-  override def toString = "%20s: %5d%sms".format(name, getMillis, if (isRunning) "..." else "")
-}
+  private def isLastKeys(n: String) = Some(n) == keys.headOption
 
-class TimerCollections {
-  private var all = Map[String, TimerCollection]()
+  def selectDynamic(name: String): TimerStorage = get(name)
 
-  def get(name: String): TimerCollection = all.getOrElse(name, {
-    val sw = new TimerCollection(name)
-    all += name -> sw
-    sw
-  })
 
-  def add(swc: TimerCollection) {
-    all += swc.name -> swc
+  def start() = {
+    if (selfTimer.isEmpty) {
+      selfTimer = Some(new Timer)
+    }
+    selfTimer.get.start
+
+    this
+  }
+
+  def stop() = {
+    selfTimer.get.stop
   }
 
-  def getAll = all
+  def outputTable(printer: String => Unit) = {
+    import utils.ASCIITables._
+
+    var table = Table("Timers")
+
+    table += Row(Seq(
+        Cell("name"),
+        Cell("min"),
+        Cell("avg"),
+        Cell("max"),
+        Cell("n"),
+        Cell("total")
+      ))
+    table += Separator
+
+    var closed = Set[TimerStorage]()
+
+    def output(ts: TimerStorage, path: List[(TimerStorage, String)]): Unit = {
+      val indent = path.map { case (from, name) =>
+        if (closed(from)) {
+          "  "
+        } else if (from.isLastKeys(name)) {
+          closed += from
+          "└ "
+        } else {
+          "├ "
+        }
+      }.reverse.mkString
+
+      (path, ts.selfTimer) match {
+        case ((_, name) :: _, Some(t)) =>
+          val n   = t.runs.size
+          val tot = t.runs.sum
+
+          val (min: String, avg: String, max: String, total: String) = if (n == 0) {
+            ("", "", "", "N/A")
+          } else if (n > 1) {
+            val min = t.runs.min
+            val max = t.runs.max
+            val avg = tot/n
+            (f"$min%d", f"$avg%d", f"$max%d", f"$tot%d")
+          } else {
+            ("", "", "", f"$tot%d")
+          }
+
+          table += Row(Seq(
+            Cell(indent+name),
+            Cell(min),
+            Cell(avg),
+            Cell(max),
+            Cell(n),
+            Cell(tot)
+          ))
+        case ((_, name) :: _, None) =>
+          table += Row(Seq(
+            Cell(indent+name, 6)
+          ))
+        case _ =>
+
+      }
+
+      ts.keys.reverse.map(n => n -> ts.fields(n)).foreach { case (name, nts) =>
+        output(nts, (ts -> name) :: path)
+      }
+    }
+
+    if (fields.nonEmpty) {
+      output(this, Nil)
+    }
+
+    printer(table.render)
+  }
 }