integrates parser warnings into the warnings framework

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -14,8 +14,11 @@ import viper.gobra.ast.frontend._
 import viper.gobra.util.{Binary, Hexadecimal, Octal}
 import viper.gobra.frontend.GobraParser._
 import viper.gobra.frontend.Parser.PRewriter
+import viper.gobra.frontend.Source.TransformableSource
 import viper.gobra.frontend.TranslationHelpers._
+import viper.gobra.reporting.{ParserError, ParserMessage, ParserWarning}
 import viper.gobra.util.Violation.violation
+import viper.silver.ast.{HasLineColumn, LineColumnPosition, SourcePosition}
 
 import scala.StringContext.InvalidEscapeException
 import scala.annotation.unused
@@ -2505,11 +2508,11 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
 
   //region Error reporting and positioning
 
-  private def fail(cause : NamedPositionable, msg : String = "") = {
+  private def fail(cause: NamedPositionable, msg: String = ""): Nothing = {
     throw TranslationFailure(cause, msg)
   }
 
-  private def unexpected(ctx: ParserRuleContext) = {
+  private def unexpected(ctx: ParserRuleContext): Nothing = {
     violation(s"could not translate '${ctx.getText}', got unexpected production '${visitChildren(ctx)}'")
   }
 
@@ -2581,17 +2584,42 @@ trait Named {
 
 // Any object that can be assigned a start and end in a source is positionable
 trait Positionable {
-  val startPos : Position
-  val endPos : Position
-  val startFinish : (Position, Position) = (startPos, endPos)
+  val startPos: Position
+  val endPos: Position
+  val startFinish: (Position, Position) = (startPos, endPos)
+  def start: HasLineColumn = LineColumnPosition(startPos.line, startPos.column)
+  def end: HasLineColumn = LineColumnPosition(endPos.line, endPos.column)
 }
 
 // This trait is used for error messages, here we need both a position and a name.
 sealed trait NamedPositionable extends Named with Positionable
 
+sealed trait TranslationMessage {
+  def toMessage(source: Source): ParserMessage
+}
+
+abstract class TranslationException(message: String) extends Exception(message) with TranslationMessage {
+  def cause: NamedPositionable
+}
+
+case class TranslationFailure(cause: NamedPositionable, details: String = "") extends TranslationException(s"Translation of ${cause.name} ${cause.text} failed${if (details.nonEmpty) ": " + details else "."}") {
+  override def toMessage(source: Source): ParserError = {
+    val pos = Some(SourcePosition(source.toPath, cause.start, cause.end))
+    ParserError(s"$getMessage ${getStackTrace.toVector(1)}", pos)
+  }
+}
 
-class TranslationException(@unused cause: NamedPositionable, msg : String) extends Exception(msg)
+case class TranslationWarning(cause: NamedPositionable, details: String = "") extends TranslationMessage {
+  val message = s"Warning in ${cause.name} ${cause.text}${if (details.nonEmpty) ": " + details else "."}"
+  override def toMessage(source: Source): ParserWarning = {
+    val pos = Some(SourcePosition(source.toPath, cause.start, cause.end))
+    ParserWarning(s"$message", pos)
+  }
+}
 
-case class TranslationFailure(cause: NamedPositionable, msg : String = "") extends TranslationException(cause, s"Translation of ${cause.name} ${cause.text} failed${if (msg.nonEmpty) ": " + msg else "."}")
-case class TranslationWarning(cause: NamedPositionable, msg : String = "") extends TranslationException(cause, s"Warning in ${cause.name} ${cause.text}${if (msg.nonEmpty) ": " + msg else "."}")
-case class UnsupportedOperatorException(cause: NamedPositionable, typ : String, msg : String = "") extends TranslationException(cause, s"Unsupported $typ operation: ${cause.text}.")
+case class UnsupportedOperatorException(cause: NamedPositionable, typ: String, msg: String = "") extends TranslationException(s"Unsupported $typ operation: ${cause.text}.") {
+  override def toMessage(source: Source): ParserError = {
+    val pos = Some(SourcePosition(source.toPath, cause.start, cause.end))
+    ParserError(s"$getMessage ${getStackTrace.toVector(0)}", pos)
+  }
+}

src/main/scala/viper/gobra/frontend/info/Info.scala

@@ -19,7 +19,7 @@ import viper.gobra.frontend.ParserUtils.{ParseResult, ParseSuccessResult}
 import viper.gobra.util.TaskManagerMode.{Lazy, Parallel, Sequential}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.typing.ghost.separation.{GhostLessPrinter, GoifyingPrinter}
-import viper.gobra.reporting.{CyclicImportError, NotFoundError, TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, TypeWarning, VerifierError}
+import viper.gobra.reporting.{CyclicImportError, NotFoundError, TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, TypeMessage, TypeWarning}
 import viper.gobra.util.VerifierPhase.{ErrorsAndWarnings, PhaseResult, Warnings}
 import viper.gobra.util.{GobraExecutionContext, Job, TaskManager, VerifierPhase, VerifierPhaseNonFinal, Violation}
 
@@ -34,9 +34,9 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
   override val name: String = "Type-checking"
 
   type GoTree = Tree[PNode, PPackage]
-  type TypeCheckSuccessResult = (TypeInfo with ExternalTypeInfo, Warnings)
-  type TypeCheckResult = Either[ErrorsAndWarnings, TypeCheckSuccessResult]
-  type DependentTypeCheckResult = Map[AbstractImport, TypeCheckResult]
+  private type TypeCheckSuccessResult = (TypeInfo with ExternalTypeInfo, Vector[TypeWarning])
+  private type TypeCheckResult = Either[Vector[TypeMessage], TypeCheckSuccessResult]
+  private type DependentTypeCheckResult = Map[AbstractImport, TypeCheckResult]
   type DependentTypeInfo = Map[AbstractImport, ExternalTypeInfo]
 
   trait GetParseResult {
@@ -61,7 +61,7 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
     def check(abstractPackage: AbstractPackage): Either[ErrorsAndWarnings, Map[AbstractPackage, ParseSuccessResult]] = {
       for {
         parseResult <- getParseResult(abstractPackage)
-        (_, ast) = parseResult
+        (_, ast, _) = parseResult
         perImportResult = ast.imports.map(importNode => {
           val res = getImportErrors(RegularImport(importNode.importPath))
             .left
@@ -82,12 +82,12 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
     /**
       * returns all parser errors and cyclic errors transitively found in imported packages
       */
-    private def getImportErrors(importTarget: AbstractImport): Either[Vector[VerifierError], Unit] = {
+    private def getImportErrors(importTarget: AbstractImport): Either[ErrorsAndWarnings, Unit] = {
       parserPendingPackages = parserPendingPackages :+ importTarget
       val abstractPackage = AbstractPackage(importTarget)(config)
       val res = for {
         parseResult <- getParseResult(abstractPackage)
-        (_, ast) = parseResult
+        (_, ast, _) = parseResult
         perImportResult = ast.imports.map(importNode => {
           val directlyImportedTarget = RegularImport(importNode.importPath)
           if (parserPendingPackages.contains(directlyImportedTarget)) {
@@ -106,13 +106,14 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
       res
     }
 
-    private def createImportError(importNode: PImport, errorsInImportedPackage: Vector[VerifierError]): Messages = {
-      val (cyclicErrors, nonCyclicErrors) = errorsInImportedPackage.partitionMap {
+    private def createImportError(importNode: PImport, errorsAndWarningsInImportedPackage: ErrorsAndWarnings): Messages = {
+      val (cyclicErrors, others) = errorsAndWarningsInImportedPackage.partitionMap {
         case cyclicErr: CyclicImportError => Left(cyclicErr)
         case e => Right(e)
       }
       if (cyclicErrors.isEmpty) {
-        message(importNode, s"Package contains ${nonCyclicErrors.length} error(s): ${nonCyclicErrors.map(_.message).mkString(", ")}")
+        val (errors, warnings) = VerifierPhase.splitErrorsAndWarnings(others)
+        message(importNode, s"Package contains ${errors.length} error(s) and ${warnings.length} warning(s): ${(errors ++ warnings).map(_.message).mkString(", ")}")
       } else {
         cyclicErrors.flatMap(cycle => message(importNode, cycle.message))
       }
@@ -140,7 +141,7 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
       override def toString: String = s"TypeCheckJob for $abstractPackage"
 
       protected override def sequentialPrecompute(): (Vector[Source], PPackage, Vector[AbstractImport]) = {
-        val (sources, ast) = getParseResult(abstractPackage)
+        val (sources, ast, _) = getParseResult(abstractPackage)
         val importTargets = ast.imports.map(importNode => RegularImport(importNode.importPath))
         val isBuiltIn = abstractPackage == BuiltInPackage
         val dependencies = if (isBuiltIn) importTargets else BuiltInImport +: importTargets
@@ -205,13 +206,15 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
       // check whether there are any import cycles:
       cycleResult <- EitherT.fromEither(Future.successful(new CycleChecker(config, parseResults).check(abstractPackage)))
         .leftMap(errorsAndWarnings => {
-          val (sources, pkg) = parseResult
+          val (sources, pkg, _) = parseResult
           reportTypeCheckFailure(config, sources, pkg, errorsAndWarnings)
           errorsAndWarnings
         })
       typeCheckingStartMs = System.currentTimeMillis()
       context = new Context(config, cycleResult)
-      typeInfo <- EitherT.fromEither(context.typeCheck(abstractPackage))
+      // the following type annotation is necessary to overcome an incompleteness of Scala's type checker:
+      typeCheckRes: Future[Either[ErrorsAndWarnings, (TypeInfo, Warnings)]] = context.typeCheck(abstractPackage)
+      typeInfo <- EitherT.fromEither(typeCheckRes)
       _ = logger.debug {
         val typeCheckingEndMs = System.currentTimeMillis()
         val sumDurationS = f"${context.typeCheckDurationMs.get() / 1000f}%.1f"
@@ -351,7 +354,7 @@ object Info extends VerifierPhaseNonFinal[(Config, PackageInfo, Map[AbstractPack
     }
   }
 
-  private def convertToTypeErrorsAndWarnings(pkg: PPackage, msgs: Messages): Either[ErrorsAndWarnings, Warnings] = {
+  private def convertToTypeErrorsAndWarnings(pkg: PPackage, msgs: Messages): Either[Vector[TypeMessage], Vector[TypeWarning]] = {
     val (warningMsgs, errorMsgs) = msgs.partition(_.severity == Severities.Warning)
 
     // the type checker sometimes produces duplicate errors, which we remove here (e.g., when type checking

src/main/scala/viper/gobra/reporting/Message.scala

@@ -103,12 +103,21 @@ case class ParsedInputMessage(input: String, ast: () => PProgram) extends GobraM
     s"file=$input)"
 }
 
-case class ParserErrorMessage(input: Path, result: Vector[ParserError]) extends GobraMessage {
-  override val name: String = s"parser_error_message"
+case class ParserSuccessMessage(input: Path, warnings: Vector[ParserWarning]) extends GobraMessage {
+  override val name: String = s"parser_success_message"
 
-  override def toString: String = s"parser_error_message(" +
-    s"file=$input), " +
-    s"errors=${result.map(_.toString).mkString(",")})"
+  override def toString: String = s"parser_success_message(" +
+    s"file=$input, " +
+    s"warnings=${warnings.map(_.toString).mkString(",")})"
+}
+
+case class ParserFailureMessage(input: Path, errors: Vector[ParserError], warnings: Vector[ParserWarning]) extends GobraMessage {
+  override val name: String = s"parser_failure_message"
+
+  override def toString: String = s"parser_failure_message(" +
+    s"file=$input, " +
+    s"errors=${errors.map(_.toString).mkString(",")}, " +
+    s"warnings=${warnings.map(_.toString).mkString(",")})"
 }
 
 sealed trait TypeCheckMessage extends GobraMessage {

src/main/scala/viper/gobra/reporting/Reporter.scala

@@ -67,8 +67,14 @@ case class FileWriterReporter(name: String = "filewriter_reporter",
         errors.foreach(err => logger.error(s"Error at: ${err.formattedMessage}"))
       case _ => // ignore
     }
-    case m:ParserErrorMessage if streamErrs => m.result.foreach(err => logger.error(s"Error at: ${err.formattedMessage}"))
-    case m:TypeCheckFailureMessage if streamErrs =>
+    case m: ParserSuccessMessage if streamErrs =>
+      m.warnings.foreach(warning => logger.warn(s"Warning at: ${warning.formattedMessage}"))
+    case m: ParserFailureMessage if streamErrs =>
+      m.warnings.foreach(warning => logger.warn(s"Warning at: ${warning.formattedMessage}"))
+      m.errors.foreach(err => logger.error(s"Error at: ${err.formattedMessage}"))
+    case m: TypeCheckSuccessMessage if streamErrs =>
+      m.warnings.foreach(warning => logger.warn(s"Warning at: ${warning.formattedMessage}"))
+    case m: TypeCheckFailureMessage if streamErrs =>
       m.warnings.foreach(warning => logger.warn(s"Warning at: ${warning.formattedMessage}"))
       m.errors.foreach(err => logger.error(s"Error at: ${err.formattedMessage}"))
     case m:TransformerFailureMessage if streamErrs => m.result.foreach(err => logger.error(s"Error at: ${err.formattedMessage}"))

src/main/scala/viper/gobra/reporting/VerifierMessage.scala

@@ -35,10 +35,6 @@ sealed trait VerifierWarning extends VerifierMessage {
   override def severity: Severity = Severities.Warning
 }
 
-case class TypeWarning(message: String, position: Option[SourcePosition]) extends VerifierWarning {
-  val id = "type_warning"
-}
-
 sealed trait VerifierError extends VerifierMessage {
   override def severity: Severity = Severities.Error
 }
@@ -53,11 +49,23 @@ case class ConfigError(message: String) extends VerifierError {
   val id = "config_error"
 }
 
-case class ParserError(message: String, position: Option[SourcePosition]) extends VerifierError {
+sealed trait ParserMessage extends VerifierMessage
+
+case class ParserWarning(message: String, position: Option[SourcePosition]) extends ParserMessage with VerifierWarning {
+  val id = "parser_warning"
+}
+
+case class ParserError(message: String, position: Option[SourcePosition]) extends ParserMessage with VerifierError {
   val id = "parser_error"
 }
 
-case class TypeError(message: String, position: Option[SourcePosition]) extends VerifierError {
+sealed trait TypeMessage extends VerifierMessage
+
+case class TypeWarning(message: String, position: Option[SourcePosition]) extends TypeMessage with VerifierWarning {
+  val id = "type_warning"
+}
+
+case class TypeError(message: String, position: Option[SourcePosition]) extends TypeMessage with VerifierError {
   val id = "type_error"
 }
 

src/main/scala/viper/gobra/util/VerifierPhase.scala

@@ -10,19 +10,42 @@ import scala.concurrent.Future
 import com.typesafe.scalalogging.LazyLogging
 import scalaz.EitherT
 import scalaz.Scalaz.futureInstance
-import viper.gobra.reporting.{VerifierError, VerifierMessage, VerifierResult, VerifierWarning}
+import viper.gobra.reporting.{ParserError, ParserMessage, ParserWarning, TypeError, TypeMessage, TypeWarning, VerifierError, VerifierMessage, VerifierResult, VerifierWarning}
 import viper.gobra.util.VerifierPhase.PhaseResult
 
 object VerifierPhase {
   type ErrorsAndWarnings = Vector[VerifierMessage]
   type Warnings = Vector[VerifierWarning]
   type PhaseResult[S] = EitherT[ErrorsAndWarnings, Future, (S, Warnings)]
 
-  def splitErrorsAndWarnings(i: ErrorsAndWarnings): (Vector[VerifierError], Warnings) =
-    i.partitionMap {
-      case e: VerifierError => Left(e)
-      case w: VerifierWarning => Right(w)
+  trait Splitter[M <: VerifierMessage, E <: VerifierError, W <: VerifierWarning] {
+    def split(msg: M): Either[E, W]
+  }
+
+  object Splitter {
+    implicit object VerifierSplitter extends Splitter[VerifierMessage, VerifierError, VerifierWarning] {
+      override def split(msg: VerifierMessage): Either[VerifierError, VerifierWarning] = msg match {
+        case e: VerifierError => Left(e)
+        case w: VerifierWarning => Right(w)
+      }
+    }
+    implicit object ParserSplitter extends Splitter[ParserMessage, ParserError, ParserWarning] {
+      override def split(msg: ParserMessage): Either[ParserError, ParserWarning] = msg match {
+        case e: ParserError => Left(e)
+        case w: ParserWarning => Right(w)
+      }
     }
+    implicit object TypeSplitter extends Splitter[TypeMessage, TypeError, TypeWarning] {
+      override def split(msg: TypeMessage): Either[TypeError, TypeWarning] = msg match {
+        case e: TypeError => Left(e)
+        case w: TypeWarning => Right(w)
+      }
+    }
+  }
+
+  def splitErrorsAndWarnings[M <: VerifierMessage, E <: VerifierError, W <: VerifierWarning](i: Vector[M])(implicit splitter: Splitter[M, E, W]): (Vector[E], Vector[W]) = {
+    i.partitionMap { splitter.split }
+  }
 }
 
 trait VerifierPhase[I, R] extends LazyLogging {

src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala

@@ -376,7 +376,7 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
       // try to parse ghostLess string:
       val parseRes = Parser.parseProgram(StringSource(ghostLess, "Ghostless Program"), false)
       parseRes match {
-        case Right(prog) => prog
+        case Right((prog, _)) => prog
         case Left(messages) => fail(s"Parsing failed: $messages")
       }
     }
@@ -415,12 +415,12 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
     def testProg(inputProg: String, expectedErasedProg: String): Assertion = {
       val inputParseAst = Parser.parseProgram(StringSource(inputProg, "Input Program"))
       val ghostlessProg = inputParseAst match {
-        case Right(prog) => ghostLessProg(prog)
+        case Right((prog, _)) => ghostLessProg(prog)
         case Left(msgs) => fail(s"Parsing input program has failed with $msgs")
       }
       val expectedParseAst = Parser.parseProgram(StringSource(expectedErasedProg, "Expected Program"))
       expectedParseAst match {
-        case Right(prog) => equal(ghostlessProg, prog)
+        case Right((prog, _)) => equal(ghostlessProg, prog)
         case Left(msgs) => fail(s"Parsing expected erased program has failed with $msgs")
       }
     }

src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala

@@ -10,15 +10,18 @@ import org.bitbucket.inkytonik.kiama.util.{Source, StringSource}
 import org.scalatest.Assertions.fail
 import viper.gobra.ast.frontend.{PExpression, PImport, PMember, PProgram, PStatement, PType}
 import viper.gobra.frontend.Parser
-import viper.gobra.reporting.ParserError
+import viper.gobra.reporting.{ParserError, ParserMessage, ParserWarning}
 
 import scala.reflect.ClassTag
 
 class ParserTestFrontend {
-  private def parse[T: ClassTag](source: String, parser: Source => Either[Vector[ParserError], T]) : Either[Vector[ParserError], T] =
-    parser(StringSource(source))
+  private def parse[T: ClassTag](source: String, parser: Source => Either[Vector[ParserMessage], (T, Vector[ParserWarning])]) : Either[Vector[ParserError], T] =
+    parser(StringSource(source)).fold(
+      messages => Left(messages.collect { case e: ParserError => e }),
+      { case (ast, _) => Right(ast) }
+    )
 
-  private def parseOrFail[T: ClassTag](source: String, parser: Source => Either[Vector[ParserError], T]): T = {
+  private def parseOrFail[T: ClassTag](source: String, parser: Source => Either[Vector[ParserMessage], (T, Vector[ParserWarning])]): T = {
     parse(source, parser) match {
       case Right(ast) => ast
       case Left(messages) => fail(s"Parsing failed: $messages")