From 1be039deb78eef7ea9265a7d84625f454cc21cc4 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 10 Feb 2014 13:04:04 +0100
Subject: [PATCH] Improve debugging for trees. asString now preferred over
toString.
---
src/main/scala/leon/LeonOption.scala | 2 +-
src/main/scala/leon/Reporter.scala | 23 ++-------------
src/main/scala/leon/Settings.scala | 2 ++
.../codegen/runtime/ChooseEntryPoint.scala | 2 +-
.../leon/evaluators/RecursiveEvaluator.scala | 4 +--
src/main/scala/leon/purescala/Common.scala | 6 ++++
.../scala/leon/purescala/Definitions.scala | 10 -------
.../scala/leon/purescala/PrettyPrinter.scala | 5 ++++
.../scala/leon/purescala/PrinterOptions.scala | 19 +++++++++++-
src/main/scala/leon/purescala/Trees.scala | 4 +--
src/main/scala/leon/purescala/TypeTrees.scala | 4 +--
src/main/scala/leon/solvers/Solver.scala | 2 ++
.../leon/solvers/combinators/DNFSolver.scala | 6 ++--
.../solvers/combinators/UnrollingSolver.scala | 2 +-
src/main/scala/leon/synthesis/Rules.scala | 2 +-
.../scala/leon/synthesis/rules/Cegis.scala | 2 +-
.../leon/termination/ChainProcessor.scala | 2 +-
.../scala/leon/termination/Processor.scala | 2 ++
src/main/scala/leon/utils/DebugSections.scala | 29 +++++++++++++++++++
.../leon/verification/AnalysisPhase.scala | 4 +--
20 files changed, 81 insertions(+), 51 deletions(-)
create mode 100644 src/main/scala/leon/utils/DebugSections.scala
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index d1379cf38..a40f2d4c7 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -56,7 +56,7 @@ object ListValue {
if (value == "off") {
None
} else {
- Some(value.split(':').map(_.trim).filter(!_.isEmpty))
+ Some(value.split("[:,]").map(_.trim).filter(!_.isEmpty))
}
}
}
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 1cd2585a0..dc8669399 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -2,6 +2,8 @@
package leon
+import utils._
+
import purescala.Definitions.Definition
import purescala.Trees.Expr
import purescala.PrettyPrinter
@@ -88,24 +90,3 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
throw LeonFatalError(msg.toString)
}
}
-
-@implicitNotFound("No implicit debug section found in scope. You need define an implicit DebugSection to use debug/ifDebug")
-sealed abstract class DebugSection(val name: String, val mask: Int)
-
-case object DebugSectionSolver extends DebugSection("solver", 1 << 0)
-case object DebugSectionSynthesis extends DebugSection("synthesis", 1 << 1)
-case object DebugSectionTimers extends DebugSection("timers", 1 << 2)
-case object DebugSectionOptions extends DebugSection("options", 1 << 3)
-case object DebugSectionVerification extends DebugSection("verification", 1 << 4)
-case object DebugSectionTermination extends DebugSection("termination", 1 << 5)
-
-object DebugSections {
- val all = Set[DebugSection](
- DebugSectionSolver,
- DebugSectionSynthesis,
- DebugSectionTimers,
- DebugSectionOptions,
- DebugSectionTermination,
- DebugSectionVerification
- )
-}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index d280e6344..63f116d7c 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -2,6 +2,8 @@
package leon
+import utils.DebugSection
+
case class Settings(
val strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
val debugSections: Set[DebugSection] = Set(), // Enables debug message for the following sections
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index 0316953f1..cf6a7ac28 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -68,7 +68,7 @@ object ChooseEntryPoint {
val total = System.currentTimeMillis-tStart;
ctx.reporter.debug("Synthesis took "+total+"ms")
- ctx.reporter.debug("Finished synthesis with "+leonRes)
+ ctx.reporter.debug("Finished synthesis with "+leonRes.asString(ctx))
unit.exprToJVM(leonRes)
case Some(false) =>
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 246e7f654..d644dc234 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -367,7 +367,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program) extends Evalu
import solvers.z3.FairZ3Solver
import purescala.TreeOps.simplestValue
- implicit val debugSection = DebugSectionSynthesis
+ implicit val debugSection = utils.DebugSectionSynthesis
val p = synthesis.Problem.fromChoose(choose)
@@ -401,7 +401,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program) extends Evalu
val total = System.currentTimeMillis-tStart;
ctx.reporter.debug("Synthesis took "+total+"ms")
- ctx.reporter.debug("Finished synthesis with "+leonRes)
+ ctx.reporter.debug("Finished synthesis with "+leonRes.asString(ctx))
leonRes
case Some(false) =>
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 89fc30674..ca6b4fc0f 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -19,6 +19,12 @@ object Common {
}
this
}
+
+ override def toString: String = PrettyPrinter(this)
+
+ def asString(implicit ctx: LeonContext): String = {
+ ScalaPrinter(this, ctx)
+ }
}
// the type is left blank (Untyped) for Identifiers that are not variables
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 832c514ab..c5bcead22 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -13,7 +13,6 @@ object Definitions {
sealed abstract class Definition extends Tree {
val id: Identifier
- override def toString: String = PrettyPrinter(this)
override def hashCode : Int = id.hashCode
override def equals(that : Any) : Boolean = that match {
case t : Definition => t.id == this.id
@@ -56,15 +55,6 @@ object Definitions {
def isRecursive(f1: FunDef) = mainModule.isRecursive(f1)
def caseClassDef(name: String) = mainModule.caseClassDef(name)
- def writeScalaFile(filename: String) {
- import java.io.FileWriter
- import java.io.BufferedWriter
- val fstream = new FileWriter(filename)
- val out = new BufferedWriter(fstream)
- out.write(ScalaPrinter(this))
- out.close
- }
-
def duplicate = {
copy(mainModule = mainModule.copy(defs = mainModule.defs.collect {
case fd: FunDef => fd.duplicate
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 98345cba1..562ea2500 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -531,6 +531,11 @@ abstract class PrettyPrinterFactory {
printer.pp(tree, None)(opts.baseIndent)
printer.toString
}
+
+ def apply(tree: Tree, ctx: LeonContext): String = {
+ val opts = PrinterOptions.fromContext(ctx)
+ apply(tree, opts)
+ }
}
object PrettyPrinter extends PrettyPrinterFactory {
diff --git a/src/main/scala/leon/purescala/PrinterOptions.scala b/src/main/scala/leon/purescala/PrinterOptions.scala
index 597c15c68..65c4017e0 100644
--- a/src/main/scala/leon/purescala/PrinterOptions.scala
+++ b/src/main/scala/leon/purescala/PrinterOptions.scala
@@ -1,4 +1,7 @@
-package leon.purescala
+package leon
+package purescala
+
+import utils._
case class PrinterOptions (
baseIndent: Int = 0,
@@ -6,3 +9,17 @@ case class PrinterOptions (
printTypes: Boolean = false,
printUniqueIds: Boolean = false
)
+
+object PrinterOptions {
+ def fromContext(ctx: LeonContext): PrinterOptions = {
+ val debugTrees = ctx.settings.debugSections contains DebugSectionTrees
+ val debugPositions = ctx.settings.debugSections contains DebugSectionPositions
+
+ PrinterOptions(
+ baseIndent = 0,
+ printPositions = debugPositions,
+ printTypes = debugTrees,
+ printUniqueIds = debugTrees
+ )
+ }
+}
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 2052034fa..938ff8407 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -15,9 +15,7 @@ object Trees {
/* EXPRESSIONS */
- abstract class Expr extends Tree with Typed with Serializable {
- override def toString: String = PrettyPrinter(this)
- }
+ abstract class Expr extends Tree with Typed with Serializable
trait Terminal {
self: Expr =>
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 61918e5a2..cd83cd8eb 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -49,9 +49,7 @@ object TypeTrees {
}
- sealed abstract class TypeTree extends Tree {
- override def toString: String = PrettyPrinter(this)
- }
+ sealed abstract class TypeTree extends Tree
// returns the number of distinct values that inhabit a type
sealed abstract class TypeSize extends Serializable
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index b4edadedb..be9b144c5 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -12,6 +12,8 @@ trait Solver {
def name: String
val context: LeonContext
+ implicit lazy val leonContext = context
+
def assertCnstr(expression: Expr): Unit
def check: Option[Boolean]
diff --git a/src/main/scala/leon/solvers/combinators/DNFSolver.scala b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
index 507106bd1..9a36612b1 100644
--- a/src/main/scala/leon/solvers/combinators/DNFSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
@@ -33,15 +33,15 @@ class DNFSolver(val context: LeonContext,
var result : Option[Boolean] = None
- debugS("Before NNF:\n" + expr)
+ debugS("Before NNF:\n" + expr.asString)
val nnfed = nnf(expr, false)
- debugS("After NNF:\n" + nnfed)
+ debugS("After NNF:\n" + nnfed.asString)
val dnfed = dnf(nnfed)
- debugS("After DNF:\n" + dnfed)
+ debugS("After DNF:\n" + dnfed.asString)
val candidates : Seq[Expr] = dnfed match {
case Or(es) => es
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 301260440..17dbabe8f 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -38,7 +38,7 @@ class UnrollingSolver(val context: LeonContext, underlyings: SolverFactory[Incre
def check : Option[Boolean] = theConstraint.map { expr =>
val solver = underlyings.getNewSolver//SimpleSolverAPI(underlyings)
- debugS("Check called on " + expr + "...")
+ debugS("Check called on " + expr.asString + "...")
val template = getTemplate(expr)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 619d8926b..bede19443 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -85,7 +85,7 @@ abstract class Rule(val name: String) {
def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replace(what.map(w => Variable(w._1) -> w._2), in)
- implicit val debugSection = DebugSectionSynthesis
+ implicit val debugSection = leon.utils.DebugSectionSynthesis
val forward: List[Solution] => Option[Solution] = {
case List(s) =>
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index b588357fc..3bb6d950f 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -559,7 +559,7 @@ case object CEGIS extends Rule("CEGIS") {
sctx.reporter.ifDebug { debug =>
debug("UNROLLING: ")
for (c <- clauses) {
- debug(" - " + c)
+ debug(" - " + c.asString(sctx.context))
}
debug("CLOSED Bs "+closedBs)
}
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index 6ac33d59b..8b4b69dde 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -18,7 +18,7 @@ class ChainProcessor(checker: TerminationChecker,
val chainComparator = new ChainComparator(structuralSize)
def run(problem: Problem): (TraversableOnce[Result], TraversableOnce[Problem]) = {
- implicit val debugSection = DebugSectionTermination
+ implicit val debugSection = utils.DebugSectionTermination
reporter.debug("- Running ChainProcessor")
val allChainMap : Map[FunDef, Set[Chain]] = problem.funDefs.map(funDef => funDef -> chainBuilder.run(funDef)).toMap
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 8b3a8e36e..c26879a16 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -1,6 +1,8 @@
package leon
package termination
+import utils._
+
import purescala.Trees._
import purescala.TreeOps._
import purescala.Common._
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
new file mode 100644
index 000000000..b399a19d9
--- /dev/null
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -0,0 +1,29 @@
+package leon
+package utils
+
+import scala.annotation.implicitNotFound
+
+@implicitNotFound("No implicit debug section found in scope. You need define an implicit DebugSection to use debug/ifDebug")
+sealed abstract class DebugSection(val name: String, val mask: Int)
+
+case object DebugSectionSolver extends DebugSection("solver", 1 << 0)
+case object DebugSectionSynthesis extends DebugSection("synthesis", 1 << 1)
+case object DebugSectionTimers extends DebugSection("timers", 1 << 2)
+case object DebugSectionOptions extends DebugSection("options", 1 << 3)
+case object DebugSectionVerification extends DebugSection("verification", 1 << 4)
+case object DebugSectionTermination extends DebugSection("termination", 1 << 5)
+case object DebugSectionTrees extends DebugSection("trees", 1 << 6)
+case object DebugSectionPositions extends DebugSection("positions", 1 << 7)
+
+object DebugSections {
+ val all = Set[DebugSection](
+ DebugSectionSolver,
+ DebugSectionSynthesis,
+ DebugSectionTimers,
+ DebugSectionOptions,
+ DebugSectionVerification,
+ DebugSectionTermination,
+ DebugSectionTrees,
+ DebugSectionPositions
+ )
+}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index dc67963e7..42d952565 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -19,7 +19,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val name = "Analysis"
val description = "Leon Verification"
- implicit val debugSection = DebugSectionVerification
+ implicit val debugSection = utils.DebugSectionVerification
override val definedOptions : Set[LeonOptionDef] = Set(
LeonValueOptionDef("functions", "--functions=f1:f2", "Limit verification to f1,f2,..."),
@@ -72,7 +72,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
reporter.info("Now considering '" + vcInfo.kind + "' VC for " + funDef.id + "...")
reporter.debug("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
- reporter.debug(simplifyLets(vc))
+ reporter.debug(simplifyLets(vc).asString(vctx.context))
// try all solvers until one returns a meaningful answer
solvers.find(sf => {
--
GitLab