multiple loggers

src/main/scala/Main.scala

@@ -28,8 +28,10 @@ object Main {
       lambdaStores: Flag,
       @arg(name = "boogie-procedure-rg", doc = "Switch version of procedure rely/guarantee checks to emit. (function|ifblock)")
       procedureRG: Option[String],
-      @arg(name = "verbose", short = 'v', doc = "Show extra debugging logs.")
+      @arg(name = "verbose", short = 'v', doc = "Show extra debugging logs (the same as -vl log)")
       verbose: Flag,
+      @arg(name = "vl", doc = s"Show extra debugging logs for a specific logger (${Logger.allLoggers.map(_.name).mkString(", ")}).")
+      verboseLog: Seq[String] = Seq(),
       @arg(name = "analyse", doc = "Run static analysis pass.")
       analyse: Flag,
       @arg(name = "interpret", doc = "Run BASIL IL interpreter.")
@@ -79,7 +81,19 @@ object Main {
 
     Logger.setLevel(LogLevel.INFO)
     if (conf.verbose.value) {
-      Logger.setLevel(LogLevel.DEBUG)
+        Logger.setLevel(LogLevel.DEBUG, true)
+    }
+    for (v <- conf.verboseLog) {
+        Logger.findLoggerByName(v) match {
+            case None => throw Exception(s"Unknown logger: '${v}': allowed are ${Logger.allLoggers.map(_.name).mkString(", ")}")
+            case Some(v) => v.setLevel(LogLevel.DEBUG, true)
+        }
+    }
+
+    if (conf.analysisResults.isDefined || conf.analysisResultsDot.isDefined) {
+        DebugDumpIRLogger.setLevel(LogLevel.INFO)
+    } else {
+        DebugDumpIRLogger.setLevel(LogLevel.OFF)
     }
 
     val rely = conf.procedureRG match {

src/main/scala/analysis/InterprocSteensgaardAnalysis.scala

@@ -2,7 +2,7 @@ package analysis
 
 import analysis.solvers.{Cons, Term, UnionFindSolver, Var}
 import ir.*
-import util.Logger
+import util.SteensLogger
 import scala.collection.mutable
 
 /** Wrapper for variables so we can have Steensgaard-specific equals method indirectly
@@ -142,7 +142,7 @@ class InterprocSteensgaardAnalysis(
   }
 
   private def unify(t1: Term[StTerm], t2: Term[StTerm]): Unit = {
-    //Logger.info(s"univfying constraint $t1 = $t2\n")
+    //SteensLogger.info(s"univfying constraint $t1 = $t2\n")
     solver.unify(t1, t2)
     // note that unification cannot fail, because there is only one kind of term constructor and no constants
   }
@@ -152,8 +152,8 @@ class InterprocSteensgaardAnalysis(
   def pointsTo(): Map[RegisterWrapperEqualSets, Set[RegisterWrapperEqualSets | MemoryRegion]] = {
     val solution = solver.solution()
     val unifications = solver.unifications()
-    Logger.debug(s"Solution: \n${solution.mkString(",\n")}\n")
-    Logger.debug(s"Sets: \n${unifications.values.map { s => s"{ ${s.mkString(",")} }"}.mkString(", ")}")
+    SteensLogger.debug(s"Solution: \n${solution.mkString(",\n")}\n")
+    SteensLogger.debug(s"Sets: \n${unifications.values.map { s => s"{ ${s.mkString(",")} }"}.mkString(", ")}")
 
     val vars = solution.keys.collect { case id: IdentifierVariable => id }
     val emptyMap = Map[RegisterWrapperEqualSets, Set[RegisterWrapperEqualSets | MemoryRegion]]()
@@ -164,7 +164,7 @@ class InterprocSteensgaardAnalysis(
       }.toSet
       a + (v.id -> pt)
     }
-    Logger.debug(s"\nPoints-to:\n${pointsto.map((k, v) => s"$k -> { ${v.mkString(",")} }").mkString("\n")}\n")
+    SteensLogger.debug(s"\nPoints-to:\n${pointsto.map((k, v) => s"$k -> { ${v.mkString(",")} }").mkString("\n")}\n")
     pointsto
   }
 }

src/main/scala/analysis/IrreducibleLoops.scala

@@ -2,7 +2,7 @@ package analysis
 
 import ir.{CFGPosition, Command, IntraProcIRCursor, Program, Procedure, Block, GoTo, IRWalk}
 import util.intrusive_list.IntrusiveList
-import util.Logger
+import util.StaticAnalysisLogger
 
 import scala.collection.mutable
 
@@ -325,8 +325,8 @@ class LoopTransform(loops: Set[Loop]) {
             case _ =>
           }
         case _ =>
-          Logger.error("Unexpected loop originating node - 1")
-          Logger.error(origNode)
+          StaticAnalysisLogger.error("Unexpected loop originating node - 1")
+          StaticAnalysisLogger.error(origNode)
       }
     }
 
@@ -353,11 +353,11 @@ class LoopTransform(loops: Set[Loop]) {
             case _ =>
           }
         case _ =>
-          Logger.error("Unexpected loop originating node - 1")
-          Logger.error(origNode)
+          StaticAnalysisLogger.error("Unexpected loop originating node - 1")
+          StaticAnalysisLogger.error(origNode)
       }
     }
 
     newLoop
   }
-}
+}

src/main/scala/analysis/Lattice.scala

@@ -2,7 +2,7 @@ package analysis
 
 import ir._
 import ir.eval.BitVectorEval
-import util.Logger
+import util.StaticAnalysisLogger
 
 /** Basic lattice
   */
@@ -162,7 +162,7 @@ class ConstantPropagationLattice extends FlatLattice[BitVecLiteral] {
       case (Top, _) => Top
   } catch {
     case e: Exception =>
-      Logger.error(s"Failed on op $op with $a and $b")
+      StaticAnalysisLogger.error(s"Failed on op $op with $a and $b")
       throw e
   }
 

src/main/scala/analysis/MemoryModelMap.scala

@@ -2,7 +2,7 @@ package analysis
 
 import analysis.*
 import ir.*
-import util.Logger
+import util.MRALogger
 
 import scala.collection.immutable.TreeMap
 import scala.collection.mutable
@@ -157,7 +157,7 @@ class MemoryModelMap(val globalOffsets: Map[BigInt, BigInt]) {
     for (dr <- oldRegions) {
       val obj = findDataObject(dr.start)
       if (obj.isEmpty) {
-        Logger.debug(s"Data region $dr not found in the new data map")
+        MRALogger.debug(s"Data region $dr not found in the new data map")
       } else {
         val isRelocated = relocatedDataRegion(dr.start)
         if (isRelocated.isDefined) {
@@ -284,34 +284,34 @@ class MemoryModelMap(val globalOffsets: Map[BigInt, BigInt]) {
           case _: HeapRegion => "  "
           case _: DataRegion => "  "
       }
-      Logger.debug(s"$spacing$range -> $region")
+      MRALogger.debug(s"$spacing$range -> $region")
       if content.contains(region) then
         if content.contains(region) then
           for value <- content(region) do
-            Logger.debug(s"$spacing    $value")
+            MRALogger.debug(s"$spacing    $value")
     }
-    Logger.debug("Stack:")
+    MRALogger.debug("Stack:")
     for name <- localStacks.keys do
       popContext()
       pushContext(name)
-      Logger.debug(s"  Function: $name")
-      if stackMap.nonEmpty then Logger.debug(s"    Local:")
+      MRALogger.debug(s"  Function: $name")
+      if stackMap.nonEmpty then MRALogger.debug(s"    Local:")
       // must sort by ranges
       for ((range, region) <- stackMap) {
         logRegion(range, region)
       }
-      if sharedStackMap.nonEmpty then Logger.debug(s"    Shared:")
+      if sharedStackMap.nonEmpty then MRALogger.debug(s"    Shared:")
       for ((parent, treeMap) <- sharedStackMap) {
-        Logger.debug(s"        Parent: ${parent.name}")
+        MRALogger.debug(s"        Parent: ${parent.name}")
         for ((range, region) <- treeMap) {
           logRegion(range, region, true)
         }
       }
-    Logger.debug("Stack Union-Find Roots:")
+    MRALogger.debug("Stack Union-Find Roots:")
     for name <- localStacks.keys do
       popContext()
       pushContext(name)
-      Logger.debug(s"  Function: $name")
+      MRALogger.debug(s"  Function: $name")
       var parentCount = 0
       // get root regions
       for ((range, region) <- stackMap) {
@@ -320,17 +320,17 @@ class MemoryModelMap(val globalOffsets: Map[BigInt, BigInt]) {
           logRegion(range, root)
           parentCount += 1
       }
-      if parentCount == 0 then Logger.debug("    No root regions") else Logger.debug(s"    Parents: $parentCount/${stackMap.size}")
-    Logger.debug("Shared Stacks:")
+      if parentCount == 0 then MRALogger.debug("    No root regions") else MRALogger.debug(s"    Parents: $parentCount/${stackMap.size}")
+    MRALogger.debug("Shared Stacks:")
     for (name, sharedStacks) <- sharedStacks do
-      Logger.debug(s"  Function: $name")
+      MRALogger.debug(s"  Function: $name")
       for region <- sharedStacks do
-        Logger.debug(s"    $region")
-    Logger.debug("Heap:")
+        MRALogger.debug(s"    $region")
+    MRALogger.debug("Heap:")
     for ((range, region) <- heapMap) {
       logRegion(range, region)
     }
-    Logger.debug("Data:")
+    MRALogger.debug("Data:")
     for ((range, region) <- dataMap) {
       logRegion(range, region)
     }
@@ -441,4 +441,4 @@ class UnionFind {
     }
   }
 
-}
+}

src/main/scala/analysis/MemoryRegionAnalysis.scala

@@ -3,7 +3,7 @@ package analysis
 import ir.eval.BitVectorEval.bv2SignedInt
 import analysis.solvers.SimpleWorklistFixpointSolver
 import ir.*
-import util.Logger
+import util.MRALogger
 
 import scala.collection.mutable
 import scala.collection.mutable.ListBuffer
@@ -59,8 +59,8 @@ trait MemoryRegionAnalysis(val program: Program,
   }
 
   private def stackDetection(stmt: Statement): Unit = {
-    Logger.debug("Stack detection")
-    Logger.debug(spList)
+    MRALogger.debug("Stack detection")
+    MRALogger.debug(spList)
     stmt match {
       case assign: LocalAssign =>
         if (spList.contains(assign.rhs)) {
@@ -174,7 +174,7 @@ trait MemoryRegionAnalysis(val program: Program,
           Set.empty
         // we cannot evaluate this to a concrete value, we need VSA for this
         case _ =>
-          Logger.debug(s"type: ${exp.getClass} $exp\n")
+          MRALogger.debug(s"type: ${exp.getClass} $exp\n")
           throw new Exception("Unknown type")
       }
     }

src/main/scala/analysis/RegionInjector.scala

@@ -2,7 +2,6 @@ package analysis
 
 import ir.eval.BitVectorEval.isNegative
 import ir.*
-import util.Logger
 
 import scala.collection.mutable
 import scala.collection.mutable.ArrayBuffer

src/main/scala/analysis/SummaryGenerator.scala

@@ -3,7 +3,6 @@ package analysis
 import analysis.*
 import ir.*
 import boogie.*
-import util.Logger
 import boogie.SpecGlobal
 
 /**
@@ -180,4 +179,4 @@ class SummaryGenerator(
       }
     }
   }
-}
+}

src/main/scala/analysis/TaintAnalysis.scala

@@ -3,7 +3,6 @@ package analysis
 import analysis.solvers.ForwardIDESolver
 import ir.*
 import boogie.*
-import util.Logger
 
 /**
  * A value which can propogate taint/be tainted.

src/main/scala/analysis/VSA.scala

@@ -7,7 +7,8 @@ import scala.collection.mutable.{ArrayBuffer, HashMap, ListBuffer}
 import java.io.{File, PrintWriter}
 import scala.collection.mutable
 import scala.collection.immutable
-import util.Logger
+import util.VSALogger
+
 
 /** ValueSets are PowerSet of possible values */
 trait Value
@@ -68,7 +69,7 @@ trait ValueSetAnalysis(program: Program,
                 case Some(v: Variable) =>
                   s + (localAssign.lhs -> s(v))
                 case None =>
-                  Logger.debug(s"Too Complex: ${localAssign.rhs}") // do nothing
+                  VSALogger.debug(s"Too Complex: ${localAssign.rhs}") // do nothing
                   s
               }
           }
@@ -84,7 +85,7 @@ trait ValueSetAnalysis(program: Program,
             case Some(v: Variable) =>
               s + (load.lhs -> s(v))
             case None =>
-              Logger.debug(s"Too Complex: ${load.index}") // do nothing
+              VSALogger.debug(s"Too Complex: ${load.index}") // do nothing
               s
           }
         }
@@ -105,7 +106,7 @@ trait ValueSetAnalysis(program: Program,
               case Some(v: Variable) =>
                 s ++ regions.map(r => r -> s(v))
               case None =>
-                Logger.debug(s"Too Complex: $store.value") // do nothing
+                VSALogger.debug(s"Too Complex: $store.value") // do nothing
                 s
             }
         }

src/main/scala/analysis/VariableDependencyAnalysis.scala

@@ -3,7 +3,7 @@ package analysis
 import analysis.solvers.ForwardIDESolver
 import ir.*
 import boogie.*
-import util.Logger
+import util.StaticAnalysisLogger
 import boogie.SpecGlobal
 
 import scala.collection.mutable
@@ -122,7 +122,7 @@ class VariableDependencyAnalysis(
     var varDepsSummariesTransposed = Map[Procedure, Map[Taintable, Set[Taintable]]]()
     scc.flatten.filter(_.blocks.nonEmpty).foreach {
       procedure => {
-        Logger.debug("Generating variable dependencies for " + procedure)
+        StaticAnalysisLogger.debug("Generating variable dependencies for " + procedure)
         val varDepResults = ProcVariableDependencyAnalysis(program, varDepVariables, globals, constProp, varDepsSummariesTransposed, procedure).analyze()
         val varDepMap = varDepResults.getOrElse(IRWalk.lastInProc(procedure).getOrElse(procedure), Map())
         varDepsSummaries += procedure -> varDepMap

src/main/scala/ir/eval/Interpreter.scala

@@ -6,6 +6,7 @@ import util.functional.*
 import util.functional.State.*
 import boogie.Scope
 import scala.collection.WithFilter
+import translating.PrettyPrinter.*
 
 import scala.annotation.tailrec
 import scala.collection.mutable
@@ -34,10 +35,7 @@ case class MemoryError(message: String = "") extends InterpreterError /* An erro
 /* Concrete value type of the interpreter. */
 sealed trait BasilValue(val irType: Option[IRType])
 case class Scalar(value: Literal) extends BasilValue(Some(value.getType)) {
-  override def toString = value match {
-    case b: BitVecLiteral => "0x%x:bv%d".format(b.value, b.size)
-    case c                => c.toString
-  }
+  override def toString = pp_expr(value)
 }
 
 /* Abstract callable function address */