From ba4e4d30c134a148e66d4ade51f2769cfd9fec47 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Fri, 6 Sep 2013 18:03:10 +0200
Subject: [PATCH] Debug sections become implicit
---
src/main/scala/leon/Main.scala | 5 ++-
src/main/scala/leon/Reporter.scala | 16 +++++--
src/main/scala/leon/solvers/Solver.scala | 2 +
.../scala/leon/solvers/SolverFactory.scala | 2 +
.../leon/solvers/z3/AbstractZ3Solver.scala | 2 -
.../leon/solvers/z3/FairZ3SolverFactory.scala | 42 +++++++++----------
.../leon/verification/AnalysisPhase.scala | 14 +++----
7 files changed, 46 insertions(+), 37 deletions(-)
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 10e5c8953..343ed2da4 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -163,7 +163,7 @@ object Main {
// Create a new reporter taking settings into account
val reporter = new DefaultReporter(settings)
- reporter.ifDebug(ReportingOptions) { debug =>
+ reporter.whenDebug(ReportingOptions) { debug =>
debug("Options considered by Leon:")
for (lo <- leonOptions) lo match {
@@ -235,7 +235,7 @@ object Main {
ctx.timers.get("Leon Run") += timer
- ctx.reporter.ifDebug(ReportingTimers) { debug =>
+ ctx.reporter.whenDebug(ReportingTimers) { debug =>
debug("-"*80)
debug("Times:")
debug("-"*80)
@@ -244,6 +244,7 @@ object Main {
}
debug("-"*80)
}
+
} catch {
case LeonFatalError() => sys.exit(1)
}
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 6b89537c2..98d72ed9f 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -5,6 +5,7 @@ package leon
import purescala.Definitions.Definition
import purescala.Trees.Expr
import purescala.PrettyPrinter
+import scala.annotation.implicitNotFound
abstract class Reporter(settings: Settings) {
def infoFunction(msg: Any) : Unit
@@ -36,17 +37,23 @@ abstract class Reporter(settings: Settings) {
private val debugMask = settings.debugSections.foldLeft(0){ _ | _.mask }
- def ifDebug(section: ReportingSection)(body: (Any => Unit) => Any) {
+ def ifDebug(body: (Any => Unit) => Any)(implicit section: ReportingSection) = {
if ((debugMask & section.mask) == section.mask) {
body(debugFunction)
}
}
- def debug(section: ReportingSection)(msg: => Any) {
- ifDebug(section) { debug =>
- debug(msg)
+ def whenDebug(section: ReportingSection)(body: (Any => Unit) => Any) {
+ if ((debugMask & section.mask) == section.mask) {
+ body(debugFunction)
}
}
+
+ def debug(msg: => Any)(implicit section: ReportingSection) = {
+ ifDebug{ debug =>
+ debug(msg)
+ }(section)
+ }
}
class DefaultReporter(settings: Settings) extends Reporter(settings) {
@@ -82,6 +89,7 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
}
}
+@implicitNotFound("No implicit debug section found in scope. You need define an implicit ReportingSection to use debug/ifDebug")
sealed abstract class ReportingSection(val name: String, val mask: Int)
case object ReportingSolver extends ReportingSection("solver", 1 << 0)
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 3fc361a9c..a4fd36aa6 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -16,4 +16,6 @@ trait Solver extends Interruptible {
def checkAssumptions(assumptions: Set[Expr]): Option[Boolean]
def getModel: Map[Identifier, Expr]
def getUnsatCore: Set[Expr]
+
+ implicit val debugSection = ReportingSolver
}
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index c637f1764..237722428 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -36,4 +36,6 @@ trait SolverFactory[S <: Solver] extends Interruptible with LeonComponent {
new TimeoutSolverFactory[S](this, ms)
}
}
+
+ implicit val debugSection = ReportingSolver
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 75c828e71..7eb358708 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -27,8 +27,6 @@ trait AbstractZ3Solver extends SolverFactory[Solver] {
context.interruptManager.registerForInterrupts(this)
- val debug = context.reporter.debug(ReportingSolver)_
-
private[this] var freed = false
val traceE = new Exception()
diff --git a/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala b/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala
index 3ece4d56c..b4d187894 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala
@@ -133,20 +133,20 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
evalResult match {
case EvaluationResults.Successful(BooleanLiteral(true)) =>
- debug("- Model validated.")
+ reporter.debug("- Model validated.")
(true, asMap)
case EvaluationResults.Successful(BooleanLiteral(false)) =>
- debug("- Invalid model.")
+ reporter.debug("- Invalid model.")
(false, asMap)
case EvaluationResults.RuntimeError(msg) =>
- debug("- Model leads to runtime error.")
+ reporter.debug("- Model leads to runtime error.")
(false, asMap)
case EvaluationResults.EvaluatorError(msg) =>
if (silenceErrors) {
- debug("- Model leads to evaluator error: " + msg)
+ reporter.debug("- Model leads to evaluator error: " + msg)
} else {
reporter.warning("Something went wrong. While evaluating the model, we got this : " + msg)
}
@@ -207,10 +207,10 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
def dumpBlockers = {
blockersInfo.groupBy(_._2._1).toSeq.sortBy(_._1).foreach { case (gen, entries) =>
- debug("--- "+gen)
+ reporter.debug("--- "+gen)
for (((bast), (gen, origGen, ast, fis)) <- entries) {
- debug(". "+bast +" ~> "+fis.map(_.funDef.id))
+ reporter.debug(". "+bast +" ~> "+fis.map(_.funDef.id))
}
}
}
@@ -431,17 +431,17 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
//val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.toSeq.map(toZ3Formula(_).get)
// println("Blocking set : " + blockingSet)
- debug(" - Running Z3 search...")
+ reporter.debug(" - Running Z3 search...")
- // debug("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n"))
- // debug("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
- // debug("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
+ // reporter.debug("Searching in:\n"+solver.getAssertions.toSeq.mkString("\nAND\n"))
+ // reporter.debug("Unroll. Assumptions:\n"+unrollingBank.z3CurrentZ3Blockers.mkString(" && "))
+ // reporter.debug("Userland Assumptions:\n"+assumptionsAsZ3.mkString(" && "))
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
- debug(" - Finished search with blocked literals")
+ reporter.debug(" - Finished search with blocked literals")
res match {
case None =>
@@ -467,8 +467,8 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
val model = modelToMap(z3model, varsInVC)
//lazy val modelAsString = model.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
- //debug("- Found a model:")
- //debug(modelAsString)
+ //reporter.debug("- Found a model:")
+ //reporter.debug(modelAsString)
foundAnswer(Some(true), model)
}
@@ -518,9 +518,9 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
if (!interrupted) {
if (this.feelingLucky) {
// we need the model to perform the additional test
- debug(" - Running search without blocked literals (w/ lucky test)")
+ reporter.debug(" - Running search without blocked literals (w/ lucky test)")
} else {
- debug(" - Running search without blocked literals (w/o lucky test)")
+ reporter.debug(" - Running search without blocked literals (w/o lucky test)")
}
solver.push() // FIXME: remove when z3 bug is fixed
@@ -529,10 +529,10 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
res2 match {
case Some(false) =>
- //debug("UNSAT WITHOUT Blockers")
+ //reporter.debug("UNSAT WITHOUT Blockers")
foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
case Some(true) =>
- //debug("SAT WITHOUT Blockers")
+ //reporter.debug("SAT WITHOUT Blockers")
if (this.feelingLucky && !interrupted) {
// we might have been lucky :D
val (wereWeLucky, cleanModel) = validateModel(solver.getModel, entireFormula, varsInVC, silenceErrors = true)
@@ -552,11 +552,11 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
}
if(!foundDefinitiveAnswer) {
- debug("- We need to keep going.")
+ reporter.debug("- We need to keep going.")
val toRelease = unrollingBank.getZ3BlockersToUnlock
- debug(" - more unrollings")
+ reporter.debug(" - more unrollings")
for(id <- toRelease) {
val newClauses = unrollingBank.unlock(id)
@@ -566,12 +566,12 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
}
}
- debug(" - finished unrolling")
+ reporter.debug(" - finished unrolling")
}
}
}
- //debug(" !! DONE !! ")
+ //reporter.debug(" !! DONE !! ")
if(interrupted) {
None
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 9d6702773..1f2ef2143 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -18,6 +18,8 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val name = "Analysis"
val description = "Leon Verification"
+ implicit val debugSection = ReportingVerification
+
override val definedOptions : Set[LeonOptionDef] = Set(
LeonValueOptionDef("functions", "--functions=f1:f2", "Limit verification to f1,f2,..."),
LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when trying to prove a verification condition.")
@@ -61,8 +63,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val reporter = vctx.reporter
val solvers = vctx.solvers
- val debug = reporter.debug(ReportingVerification)_
-
val interruptManager = vctx.context.interruptManager
for((funDef, vcs) <- vcs.toSeq.sortWith((a,b) => a._1 < b._1); vcInfo <- vcs if !interruptManager.isInterrupted()) {
@@ -70,12 +70,12 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val vc = vcInfo.condition
reporter.info("Now considering '" + vcInfo.kind + "' VC for " + funDef.id + "...")
- debug("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
- debug(simplifyLets(vc))
+ reporter.debug("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
+ reporter.debug(simplifyLets(vc))
// try all solvers until one returns a meaningful answer
solvers.find(se => {
- debug("Trying with solver: " + se.name)
+ reporter.debug("Trying with solver: " + se.name)
val t1 = System.nanoTime
val (satResult, counterexample) = SimpleSolverAPI(se).solveSAT(Not(vc))
val solverResult = satResult.map(!_)
@@ -156,10 +156,8 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val vctx = VerificationContext(ctx, solvers, reporter)
- val debug = reporter.debug(ReportingVerification)_
-
val report = if(solvers.size >= 1) {
- debug("Running verification condition generation...")
+ reporter.debug("Running verification condition generation...")
val vcs = generateVerificationConditions(reporter, program, functionsToAnalyse)
checkVerificationConditions(vctx, vcs)
} else {
--
GitLab