From b75e351ff24946dc1988698b88d106b2f2491ad9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Mon, 23 Apr 2012 13:36:38 +0200
Subject: [PATCH] Debug system with level and tags
---
src/main/scala/leon/Logger.scala | 24 +++++++++++++++++++++
src/main/scala/leon/Main.scala | 1 +
src/main/scala/leon/PassManager.scala | 4 ++--
src/main/scala/leon/Settings.scala | 3 ++-
src/main/scala/leon/plugin/LeonPlugin.scala | 6 ++++--
5 files changed, 33 insertions(+), 5 deletions(-)
create mode 100644 src/main/scala/leon/Logger.scala
diff --git a/src/main/scala/leon/Logger.scala b/src/main/scala/leon/Logger.scala
new file mode 100644
index 000000000..fc4942535
--- /dev/null
+++ b/src/main/scala/leon/Logger.scala
@@ -0,0 +1,24 @@
+package leon
+
+object Logger {
+
+ //the debug level to display, from 0 (no debug information) to 5 (very verbose)
+ //var level = 0
+
+ //each debug information is tagged by a string, the tag variable only display the message with a tag in this set
+ //if the set is empty then all tags are displayed
+ //var tags: Set[String] = Set()
+
+ val defaultTag = "main"
+
+ private def output(msg: String, lvl: Int, tag: String) {
+ if(lvl <= Settings.debugLevel) {
+ if(Settings.debugTags.isEmpty || Settings.debugTags.contains(tag)) {
+ println("DEBUG: [" + tag + "] " + msg)
+ }
+ }
+ }
+
+ def debug(msg: String, lvl: Int, tag: String = defaultTag) = output(msg, lvl, tag)
+
+}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 72623c96a..0e4bae512 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -31,6 +31,7 @@ object Main {
}
private def defaultAction(program: Program, reporter: Reporter) : Unit = {
+ Logger.debug("Default action on program: " + program, 5, "main")
val passManager = new PassManager(Seq(ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
val program2 = passManager.run(program)
val analysis = new Analysis(program2, reporter)
diff --git a/src/main/scala/leon/PassManager.scala b/src/main/scala/leon/PassManager.scala
index f2830df79..2ab8f44ad 100644
--- a/src/main/scala/leon/PassManager.scala
+++ b/src/main/scala/leon/PassManager.scala
@@ -6,9 +6,9 @@ class PassManager(passes: Seq[Pass]) {
def run(program: Program): Program = {
passes.foldLeft(program)((pgm, pass) => {
- //println("Running Pass: " + pass.description)
+ Logger.debug("Running Pass: " + pass.description, 1, "passman")
val newPgm = pass(pgm)
- //println("Resulting program: " + newPgm)
+ Logger.debug("Resulting program: " + newPgm, 5, "passman")
newPgm
})
}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 797a209e5..6e469cbe0 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -23,5 +23,6 @@ object Settings {
var useParallel : Boolean = false
// When this is None, use real integers
var bitvectorBitwidth : Option[Int] = None
- var verbose : Boolean = false
+ var debugLevel: Int = 0
+ var debugTags: Set[String] = Set.empty
}
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index 5de24fa44..efdb81c62 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -40,7 +40,8 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
" --quickcheck Use QuickCheck-like random search" + "\n" +
" --parallel Run all solvers in parallel" + "\n" +
" --noLuckyTests Do not perform additional tests to potentially find models early" + "\n" +
- " --verbose Print debugging informations"
+ " --debug=[1-5] Debug level" + "\n" +
+ " --tags=t1:... Filter out debug information that are not of one of the given tags"
)
/** Processes the command-line options. */
@@ -63,7 +64,8 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
case "quickcheck" => leon.Settings.useQuickCheck = true
case "parallel" => leon.Settings.useParallel = true
case "noLuckyTests" => leon.Settings.luckyTest = false
- case "verbose" => leon.Settings.verbose = true
+ case s if s.startsWith("debug=") => leon.Settings.debugLevel = try { s.substring("debug=".length, s.length).toInt } catch { case _ => 0 }
+ case s if s.startsWith("tags=") => leon.Settings.debugTags = Set(splitList(s.substring("tags=".length, s.length)): _*)
case s if s.startsWith("unrolling=") => leon.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => leon.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
case s if s.startsWith("extensions=") => leon.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
--
GitLab