improves reporting of consistency errors and errors resulting from ap…

…plying Viper transformers

src/main/scala/viper/gobra/Gobra.scala

@@ -293,7 +293,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
 
   private def performViperEncoding(program: Program, config: Config, pkgInfo: PackageInfo): Either[Vector[VerifierError], BackendVerifier.Task] = {
     if (config.shouldViperEncode) {
-      Right(Translator.translate(program, pkgInfo)(config))
+      Translator.translate(program, pkgInfo)(config)
     } else {
       Left(Vector())
     }

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

@@ -173,6 +173,14 @@ case class GeneratedViperMessage(taskName: String, inputs: Vector[String], vprAs
   lazy val vprAstFormatted: String = silver.ast.pretty.FastPrettyPrinter.pretty(vprAst())
 }
 
+case class TransformerFailureMessage(inputs: Vector[String], result: Vector[VerifierError]) extends GobraMessage {
+  override val name: String = s"transformer_failure_message"
+
+  override def toString: String = s"transformer_failure_message(" +
+    s"files=$inputs, " +
+    s"failures=${result.map(_.toString).mkString(",")})"
+}
+
 case class ChoppedViperMessage(inputs: Vector[String], idx: Int, vprAst: () => vpr.Program, backtrack: () => BackTranslator.BackTrackInfo) extends GobraMessage {
   override val name: String = s"chopped_viper_message"
 

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

@@ -66,6 +66,7 @@ case class FileWriterReporter(name: String = "filewriter_reporter",
     }
     case m:ParserErrorMessage if streamErrs => m.result.foreach(err => logger.error(s"Error at: ${err.formattedMessage}"))
     case m:TypeCheckFailureMessage if streamErrs => m.result.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}"))
     case _ => // ignore
   }
 

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

@@ -56,11 +56,15 @@ case class DiamondError(message: String) extends VerifierError {
   val id = "diamond_error"
 }
 
-case class TimeoutError(message: String) extends  VerifierError {
+case class TimeoutError(message: String) extends VerifierError {
   val position: Option[SourcePosition] = None
   val id = "timeout_error"
 }
 
+case class ConsistencyError(message: String, position: Option[SourcePosition]) extends VerifierError {
+  val id = "consistency_error"
+}
+
 sealed trait VerificationError extends VerifierError {
 
   def info: Source.Verifier.Info

src/main/scala/viper/gobra/translator/Translator.scala

@@ -10,17 +10,28 @@ package viper.gobra.translator
 import viper.gobra.ast.internal.Program
 import viper.gobra.backend.BackendVerifier
 import viper.gobra.frontend.{Config, PackageInfo}
-import viper.gobra.reporting.GeneratedViperMessage
+import viper.gobra.reporting.{ConsistencyError, GeneratedViperMessage, TransformerFailureMessage, VerifierError}
 import viper.gobra.translator.context.DfltTranslatorConfig
 import viper.gobra.translator.encodings.programs.ProgramsImpl
 import viper.gobra.translator.transformers.{AssumeTransformer, TerminationTransformer, ViperTransformer}
 import viper.gobra.util.Violation
+import viper.silver.ast.{AbstractSourcePosition, SourcePosition}
 import viper.silver.ast.pretty.FastPrettyPrinter
+import viper.silver.verifier.AbstractError
 import viper.silver.{ast => vpr}
 
 object Translator {
 
-  def translate(program: Program, pkgInfo: PackageInfo)(config: Config): BackendVerifier.Task = {
+  private def createConsistencyErrors(errs: Seq[AbstractError]): Vector[ConsistencyError] =
+    errs.map(err => {
+      val pos = err.pos match {
+        case sp: AbstractSourcePosition => Some(new SourcePosition(sp.file, sp.start, sp.end))
+        case _ => None
+      }
+      ConsistencyError(err.readableMessage, pos)
+    }).toVector
+
+  def translate(program: Program, pkgInfo: PackageInfo)(config: Config): Either[Vector[VerifierError], BackendVerifier.Task] = {
     val translationConfig = new DfltTranslatorConfig()
     val programTranslator = new ProgramsImpl()
     val task = programTranslator.translate(program)(translationConfig)
@@ -30,17 +41,25 @@ object Translator {
       new TerminationTransformer
     )
 
-    val transformedTask = transformers.foldLeft(task) {
-      case (t, transformer) => transformer.transform(t)
-        .fold(errs => Violation.violation(s"Applying transformer ${transformer.getClass.getSimpleName} resulted in errors: ${errs.toString}"), identity)
+    val transformedTask = transformers.foldLeft[Either[Vector[VerifierError], BackendVerifier.Task]](Right(task)) {
+      case (Right(t), transformer) => transformer.transform(t).left.map(createConsistencyErrors)
+      case (errs, _) => errs
     }
 
     if (config.checkConsistency) {
-      val errors = transformedTask.program.checkTransitively
-      if (errors.nonEmpty) Violation.violation(errors.toString)
+      transformedTask
+        .flatMap(task => {
+          val consistencyErrs = task.program.checkTransitively
+          if (consistencyErrs.isEmpty) Right(())
+          else Left(createConsistencyErrors(consistencyErrs))
+        })
+        .left.map(errs => Violation.violation(errs.toString))
     }
 
-    config.reporter report GeneratedViperMessage(config.taskName, config.packageInfoInputMap(pkgInfo).map(_.name), () => sortAst(transformedTask.program), () => transformedTask.backtrack)
+    val inputs = config.packageInfoInputMap(pkgInfo).map(_.name)
+    transformedTask.fold(
+      errs => config.reporter report TransformerFailureMessage(inputs, errs),
+      task => config.reporter report GeneratedViperMessage(config.taskName, inputs, () => sortAst(task.program), () => task.backtrack))
     transformedTask
   }