-
Manos Koukoutos authoredManos Koukoutos authored
Reporter.scala 6.57 KiB
/* Copyright 2009-2015 EPFL, Lausanne */
package leon
import utils._
abstract class Reporter(val debugSections: Set[DebugSection]) {
abstract class Severity
case object INFO extends Severity
case object WARNING extends Severity
case object ERROR extends Severity
case object FATAL extends Severity
case object INTERNAL extends Severity
case class DEBUG(section: DebugSection) extends Severity
case class Message(severity: Severity, position: Position, msg: Any)
private var _errorCount : Int = 0
private var _warningCount : Int = 0
final def errorCount : Int = _errorCount
final def warningCount : Int = _warningCount
def account(msg: Message): Message = {
msg.severity match {
case WARNING => _warningCount += 1
case ERROR | FATAL | INTERNAL => _errorCount += 1
case _ =>
}
msg
}
def emit(msg: Message): Unit
def onFatal(): Nothing = {
throw LeonFatalError(None)
}
def onCompilerProgress(current: Int, total: Int) = {}
final def info(pos: Position, msg: Any): Unit = emit(account(Message(INFO, pos, msg)))
final def warning(pos: Position, msg: Any): Unit = emit(account(Message(WARNING, pos, msg)))
final def error(pos: Position, msg: Any): Unit = emit(account(Message(ERROR, pos, msg)))
final def title(pos: Position, msg: Any): Unit = emit(account(Message(INFO, pos, Console.BOLD + msg + Console.RESET)))
final def fatalError(pos: Position, msg: Any): Nothing = {
emit(account(Message(FATAL, pos, msg)))
onFatal()
}
final def internalError(pos: Position, msg : Any) : Nothing = {
emit(account(Message(INTERNAL, pos, msg.toString +
"\nPlease inform the authors of Leon about this message"
)))
onFatal()
}
final def internalAssertion(cond : Boolean, pos: Position, msg : Any) : Unit = {
if (!cond) internalError(pos,msg)
}
def terminateIfError() = {
if (errorCount > 0) {
_errorCount = 0
_warningCount = 0
fatalError("There were errors.")
}
}
// Debugging
private val debugMask = debugSections.foldLeft(0){ _ | _.mask }
def isDebugEnabled(implicit section: DebugSection): Boolean = {
(debugMask & section.mask) == section.mask
}
def ifDebug(pos: Position, body: (Any => Unit) => Any)(implicit section: DebugSection) = {
if (isDebugEnabled) {
body( { (msg: Any) => emit(account(Message(DEBUG(section), pos, msg))) } )
}
}
def whenDebug(pos: Position, section: DebugSection)(body: (Any => Unit) => Any) {
if (isDebugEnabled(section)) {
body( { (msg: Any) => emit(account(Message(DEBUG(section), pos, msg))) } )
}
}
def debug(pos: Position, msg: => Any)(implicit section: DebugSection): Unit = {
ifDebug(pos, debug =>
debug(msg)
)(section)
}
// No-position alternatives
final def info(msg: Any): Unit = info(NoPosition, msg)
final def warning(msg: Any): Unit = warning(NoPosition, msg)
final def error(msg: Any): Unit = error(NoPosition, msg)
final def title(msg: Any): Unit = title(NoPosition, msg)
final def fatalError(msg: Any): Nothing = fatalError(NoPosition, msg)
final def internalError(msg: Any) : Nothing = internalError(NoPosition, msg)
final def internalAssertion(cond : Boolean, msg: Any) : Unit = internalAssertion(cond,NoPosition, msg)
final def debug(msg: => Any)(implicit section: DebugSection): Unit = debug(NoPosition, msg)
final def ifDebug(body: (Any => Unit) => Any)(implicit section: DebugSection): Unit =
ifDebug(NoPosition, body)
final def whenDebug(section: DebugSection)(body: (Any => Unit) => Any): Unit =
whenDebug(NoPosition, section)(body)
}
class DefaultReporter(debugSections: Set[DebugSection]) extends Reporter(debugSections) {
protected def severityToPrefix(sev: Severity): String = sev match {
case ERROR => "["+Console.RED +" Error "+Console.RESET+"]"
case WARNING => "["+Console.YELLOW +"Warning "+Console.RESET+"]"
case INFO => "["+Console.BLUE +" Info "+Console.RESET+"]"
case FATAL => "["+Console.RED+Console.BOLD +" Fatal "+Console.RESET+"]"
case INTERNAL => "["+ Console.BOLD +"Internal"+Console.RESET+"]"
case DEBUG(_) => "["+Console.MAGENTA +" Debug "+Console.RESET+"]"
}
def smartPos(p: Position): String = {
if (p == NoPosition) {
""
} else {
val target = p.file.getAbsolutePath()
val here = new java.io.File(".").getAbsolutePath().stripSuffix(".")
val diff = target.stripPrefix(here)
val filePos = diff+":"
filePos + p + ": "
}
}
def emit(msg: Message) = {
println(reline(severityToPrefix(msg.severity), smartPos(msg.position) + msg.msg.toString))
printLineContent(msg.position)
}
protected var linesOf = Map[java.io.File, List[String]]()
def getLine(pos: Position): Option[String] = {
val lines = linesOf.get(pos.file) match {
case Some(lines) =>
lines
case None =>
val lines = if (pos == NoPosition) {
Nil
} else {
scala.io.Source.fromFile(pos.file).getLines.toList
}
linesOf += pos.file -> lines
lines
}
if (lines.size > pos.line-1 && pos.line >= 0) {
Some(lines(pos.line-1))
} else {
None
}
}
val prefixSize = 11
val blankPrefix = " " * prefixSize
def printLineContent(pos: Position): Unit = {
getLine(pos) match {
case Some(line) =>
println(blankPrefix+line)
pos match {
case rp: RangePosition =>
val bp = rp.focusBegin
val ep = rp.focusEnd
val carret = if (bp.line == ep.line) {
val width = Math.max(ep.col - bp.col, 1)
"^" * width
} else {
val width = Math.max(line.length+1-bp.col, 1)
("^" * width)+"..."
}
println(blankPrefix+(" " * (bp.col - 1) + Console.RED+carret+Console.RESET))
case op: OffsetPosition =>
println(blankPrefix+(" " * (op.col - 1) + Console.RED+"^"+Console.RESET))
}
case None =>
}
}
protected def reline(pfx: String, msg: String) : String = {
pfx+" "+msg.replaceAll("\n", s"\n$pfx ")
}
}
class PlainTextReporter(debugSections: Set[DebugSection]) extends DefaultReporter(debugSections) {
override protected def severityToPrefix(sev: Severity): String = sev match {
case ERROR => "[ Error ]"
case WARNING => "[Warning ]"
case INFO => "[ Info ]"
case FATAL => "[ Fatal ]"
case INTERNAL => "[Internal]"
case DEBUG(_) => "[ Debug ]"
}
}