From de01d2d5cb0d76cb577f068a1d32a7a75f35f302 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 6 May 2015 17:26:41 +0200
Subject: [PATCH] --debug=trees actually debug trees
---
src/main/scala/leon/Main.scala | 18 +++++++++++++++---
src/main/scala/leon/Reporter.scala | 8 ++++++--
.../frontends/scalac/ExtractionPhase.scala | 2 ++
.../scala/leon/utils/PreprocessingPhase.scala | 2 ++
src/main/scala/leon/utils/PrintTreePhase.scala | 18 ++++++++++++++++++
5 files changed, 43 insertions(+), 5 deletions(-)
create mode 100644 src/main/scala/leon/utils/PrintTreePhase.scala
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 5be1d3537..b1840d8d8 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -153,6 +153,14 @@ object Main {
val verifyF = ctx.findOptionOrDefault(optVerify)
val evalF = ctx.findOptionOrDefault(optEval)
+ def debugTrees(title: String): LeonPhase[Program, Program] = {
+ if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) {
+ PrintTreePhase(title)
+ } else {
+ NoopPhase[Program]
+ }
+ }
+
if (helpF) {
displayVersion(ctx.reporter)
displayHelp(ctx.reporter, error = false)
@@ -160,11 +168,15 @@ object Main {
val pipeBegin: Pipeline[List[String], Program] =
if (xlangF)
ExtractionPhase andThen
- PreprocessingPhase
+ debugTrees("Program after extraction") andThen
+ PreprocessingPhase andThen
+ debugTrees("Program after pre-processing")
else
ExtractionPhase andThen
- PreprocessingPhase andThen
- xlang.NoXLangFeaturesChecking
+ debugTrees("Program after extraction") andThen
+ PreprocessingPhase andThen
+ debugTrees("Program after pre-processing")
+ xlang.NoXLangFeaturesChecking
val pipeProcess: Pipeline[Program, Any] = {
if (noopF) RestoreMethods andThen FileOutputPhase
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 52fedd3a8..b326f5146 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -69,14 +69,18 @@ abstract class Reporter(val debugSections: Set[DebugSection]) {
// Debugging
private val debugMask = debugSections.foldLeft(0){ _ | _.mask }
+ def isDebugEnabled(implicit section: DebugSection): Boolean = {
+ (debugMask & section.mask) == section.mask
+ }
+
def ifDebug(body: (Any => Unit) => Any)(implicit section: DebugSection) = {
- if ((debugMask & section.mask) == section.mask) {
+ if (isDebugEnabled) {
body( { (msg: Any) => emit(account(Message(DEBUG(section), NoPosition, msg))) } )
}
}
def whenDebug(section: DebugSection)(body: (Any => Unit) => Any) {
- if ((debugMask & section.mask) == section.mask) {
+ if (isDebugEnabled(section)) {
body( { (msg: Any) => emit(account(Message(DEBUG(section), NoPosition, msg))) } )
}
}
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index c4131034a..80a6691a1 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -6,6 +6,8 @@ package frontends.scalac
import purescala.Definitions.Program
import purescala.Common.FreshIdentifier
+import purescala.ScalaPrinter
+
import utils._
import scala.tools.nsc.{Settings,CompilerCommand}
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 71bec02b1..0f51eb6ed 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -4,6 +4,7 @@ package leon
package utils
import purescala.Definitions.Program
+import purescala.ScalaPrinter
import purescala.{MethodLifting, CompleteAbstractDefinitions}
import synthesis.{ConvertWithOracle, ConvertHoles}
@@ -25,6 +26,7 @@ object PreprocessingPhase extends TransformationPhase {
CompleteAbstractDefinitions andThen
InjectAsserts
+
phases.run(ctx)(p)
}
}
diff --git a/src/main/scala/leon/utils/PrintTreePhase.scala b/src/main/scala/leon/utils/PrintTreePhase.scala
new file mode 100644
index 000000000..c28a90722
--- /dev/null
+++ b/src/main/scala/leon/utils/PrintTreePhase.scala
@@ -0,0 +1,18 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package utils
+
+
+import purescala.Definitions.Program
+
+case class PrintTreePhase(title: String) extends UnitPhase[Program] {
+
+ val name = "Print program"
+ val description = "Display: "+title
+
+ def apply(ctx: LeonContext, p: Program) {
+ ctx.reporter.info(ASCIIHelpers.title(title))
+ ctx.reporter.info(p.asString(ctx))
+ }
+}
--
GitLab