Support for Warnings

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -12,7 +12,7 @@ import org.bitbucket.inkytonik.kiama.util._
 import viper.gobra.ast.frontend.PNode.PPkg
 import viper.gobra.frontend.PackageInfo
 import viper.gobra.frontend.Source.TransformableSource
-import viper.gobra.reporting.VerifierError
+import viper.gobra.reporting.VerifierMessage
 import viper.gobra.util.{Decimal, NumBase}
 import viper.silver.ast.{LineColumnPosition, SourcePosition}
 
@@ -73,7 +73,7 @@ case class PPreamble(
 
 class PositionManager(val positions: Positions) extends Messaging(positions) {
 
-  def translate[E <: VerifierError](
+  def translate[E <: VerifierMessage](
                                      messages: Messages,
                                      errorFactory: (String, Option[SourcePosition]) => E
                                    ): Vector[E] = {
@@ -537,9 +537,11 @@ sealed trait PBinaryExp[L <: PExpressionOrType, R <: PExpressionOrType] extends
   def right: R
 }
 
-case class PEquals(left: PExpressionOrType, right: PExpressionOrType) extends PBinaryExp[PExpressionOrType, PExpressionOrType]
+sealed trait PActualEquality extends PBinaryExp[PExpressionOrType, PExpressionOrType]
 
-case class PUnequals(left: PExpressionOrType, right: PExpressionOrType) extends PBinaryExp[PExpressionOrType, PExpressionOrType]
+case class PEquals(left: PExpressionOrType, right: PExpressionOrType) extends PActualEquality
+
+case class PUnequals(left: PExpressionOrType, right: PExpressionOrType) extends PActualEquality
 
 case class PGhostEquals(left: PExpression, right: PExpression) extends PBinaryGhostExp
 

src/main/scala/viper/gobra/ast/internal/transform/Transformations.scala

@@ -0,0 +1,37 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2025 ETH Zurich.
+
+package viper.gobra.ast.internal.transform
+
+import scalaz.EitherT
+import scalaz.Scalaz.futureInstance
+import viper.gobra.ast.internal.Program
+import viper.gobra.frontend.{Config, PackageInfo}
+import viper.gobra.reporting.AppliedInternalTransformsMessage
+import viper.gobra.util.{GobraExecutionContext, VerifierPhaseNonFinal}
+import viper.gobra.util.VerifierPhase.PhaseResult
+
+object Transformations extends VerifierPhaseNonFinal[(Config, PackageInfo, Program), Program] {
+  override val name: String = "Internal transformations"
+
+  /**
+    * Applies transformations to programs in the internal language. Currently, only adds overflow checks but it can
+    * be easily extended to perform more transformations
+    */
+  override protected def execute(input: (Config, PackageInfo, Program))(implicit executor: GobraExecutionContext): PhaseResult[Program] = {
+    val (config, pkgInfo, program) = input
+    // constant propagation does not cause duplication of verification errors caused
+    // by overflow checks (if enabled) because all overflows in constant declarations
+    // can be found by the well-formedness checks.
+    var transformations: Vector[InternalTransform] = Vector(CGEdgesTerminationTransform, ConstantPropagation)
+    if (config.checkOverflows) {
+      transformations :+= OverflowChecksTransform
+    }
+    val result = transformations.foldLeft(program)((prog, transf) => transf.transform(prog))
+    config.reporter.report(AppliedInternalTransformsMessage(config.packageInfoInputMap(pkgInfo).map(_.name), () => result))
+    EitherT.right(result, Vector.empty)
+  }
+}

src/main/scala/viper/gobra/backend/BackendVerifier.scala

@@ -6,32 +6,51 @@
 
 package viper.gobra.backend
 
+import java.util.concurrent.ExecutionException
+import scala.concurrent.Future
 import viper.gobra.backend.ViperBackends.{CarbonBackend => Carbon}
 import viper.gobra.frontend.{Config, PackageInfo}
 import viper.gobra.reporting.BackTranslator.BackTrackInfo
-import viper.gobra.reporting.{BackTranslator, BacktranslatingReporter, ChoppedProgressMessage}
-import viper.gobra.util.{ChopperUtil, GobraExecutionContext}
+import viper.gobra.reporting.{BackTranslator, BacktranslatingReporter, ChoppedProgressMessage, VerifierResult}
+import viper.gobra.util.VerifierPhase.Warnings
+import viper.gobra.util.Violation.KnownZ3BugException
+import viper.gobra.util.{ChopperUtil, GobraExecutionContext, VerifierPhaseFinal}
 import viper.silver
 import viper.silver.verifier.VerificationResult
 import viper.silver.{ast => vpr}
 
-import scala.concurrent.Future
 
-object BackendVerifier {
+case class Task(program: vpr.Program,
+                backtrack: BackTranslator.BackTrackInfo)
+
+sealed trait Result
+case object Success extends Result
+case class Failure(errors: Vector[silver.verifier.VerificationError],
+                   backtrack: BackTranslator.BackTrackInfo) extends Result
+
+object BackendVerifier extends VerifierPhaseFinal[(Config, PackageInfo, Task, Warnings)] {
 
-  case class Task(
-                   program: vpr.Program,
-                   backtrack: BackTranslator.BackTrackInfo
-                 )
+  override val name: String = "Verification with backend"
+
+  /**
+    * Warnings correspond to warnings that occurred in phases prior to this phase.
+    * This is used to correctly report them via GobraMessages
+    */
+  override protected def execute(input: (Config, PackageInfo, Task, Warnings))(implicit executor: GobraExecutionContext): Future[VerifierResult] = {
+    val (config, pkgInfo, task, warningsFromPreviousPhases) = input
+    verify(task, pkgInfo, warningsFromPreviousPhases)(config)
+      .map(BackTranslator.backTranslate(_, warningsFromPreviousPhases)(config))
+      .recoverWith {
+        case e: ExecutionException if isKnownZ3Bug(e) =>
+          // The Z3 instance died. This is a known issue that is caused by a Z3 bug.
+          Future.failed(new KnownZ3BugException("Encountered a known Z3 bug. Please, execute the file again."))
+      }
+  }
 
-  sealed trait Result
-  case object Success extends Result
-  case class Failure(
-                    errors: Vector[silver.verifier.VerificationError],
-                    backtrack: BackTranslator.BackTrackInfo
-                    ) extends Result
+  override protected def resultIfNotPerformed(input: (Config, PackageInfo, Task, Warnings))(implicit executor: GobraExecutionContext): Future[VerifierResult] =
+    Future.successful(VerifierResult.Success(input._4))
 
-  def verify(task: Task, pkgInfo: PackageInfo)(config: Config)(implicit executor: GobraExecutionContext): Future[Result] = {
+  private def verify(task: Task, pkgInfo: PackageInfo, warnings: Warnings)(config: Config)(implicit executor: GobraExecutionContext): Future[Result] = {
 
     var exePaths: Vector[String] = Vector.empty
 
@@ -49,7 +68,7 @@ object BackendVerifier {
 
     val verificationResults: Future[VerificationResult] =  {
       val verifier = config.backendOrDefault.create(exePaths, config)
-      val reporter = BacktranslatingReporter(config.reporter, task.backtrack, config)
+      val reporter = BacktranslatingReporter(config.reporter, task.backtrack, config, warnings)
 
       if (!config.shouldChop) {
         verifier.verify(config.taskName, reporter, task.program)(executor)
@@ -81,6 +100,20 @@ object BackendVerifier {
     verificationResults.map(convertVerificationResult(_, task.backtrack))
   }
 
+  @scala.annotation.tailrec
+  private def isKnownZ3Bug(e: ExecutionException): Boolean = {
+    def causedByFile(st: Array[StackTraceElement], filename: String): Boolean = {
+      if (st.isEmpty) false
+      else st.head.getFileName == filename
+    }
+
+    e.getCause match {
+      case c: ExecutionException => isKnownZ3Bug(c) // follow nested exception
+      case npe: NullPointerException if causedByFile(npe.getStackTrace, "Z3ProverStdIO.scala") => true
+      case _ => false
+    }
+  }
+
   /**
     * Takes a Viper VerificationResult and converts it to a Gobra Result using the provided backtracking information
     */

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

@@ -7,6 +7,8 @@
 package viper.gobra.frontend
 
 import com.typesafe.scalalogging.LazyLogging
+import scalaz.EitherT
+import scalaz.Scalaz.futureInstance
 import viper.gobra.ast.frontend.{PExpression, AstPattern => ap, _}
 import viper.gobra.ast.{internal => in}
 import viper.gobra.frontend.PackageResolver.RegularImport
@@ -20,8 +22,9 @@ import viper.gobra.reporting.Source.{AutoImplProofAnnotation, ImportPreNotEstabl
 import viper.gobra.reporting.{DesugaredMessage, Source}
 import viper.gobra.theory.Addressability
 import viper.gobra.translator.Names
+import viper.gobra.util.VerifierPhase.PhaseResult
 import viper.gobra.util.Violation.violation
-import viper.gobra.util.{BackendAnnotation, Constants, DesugarWriter, GobraExecutionContext, Violation}
+import viper.gobra.util.{BackendAnnotation, Constants, DesugarWriter, GobraExecutionContext, VerifierPhaseNonFinal, Violation}
 
 import java.util.concurrent.atomic.AtomicLong
 import scala.annotation.{tailrec, unused}
@@ -31,9 +34,12 @@ import scala.concurrent.{Await, Future}
 import scala.reflect.ClassTag
 
 // `LazyLogging` provides us with access to `logger` to emit log messages
-object Desugar extends LazyLogging {
+object Desugar extends VerifierPhaseNonFinal[(Config, viper.gobra.frontend.info.TypeInfo), in.Program] with LazyLogging {
 
-  def desugar(config: Config, info: viper.gobra.frontend.info.TypeInfo)(implicit executionContext: GobraExecutionContext): in.Program = {
+  override val name: String = "Desugaring"
+
+  override protected def execute(input: (Config, viper.gobra.frontend.info.TypeInfo))(implicit executionContext: GobraExecutionContext): PhaseResult[in.Program] = {
+    val (config, info) = input
     val pkg = info.tree.root
     val importsCollector = new PackageInitSpecCollector
 
@@ -77,7 +83,7 @@ object Desugar extends LazyLogging {
     // combine all desugared results into one Viper program:
     val internalProgram = combine(mainDesugarer, mainProgram, importedPrograms)
     config.reporter report DesugaredMessage(config.packageInfoInputMap(pkg.info).map(_.name), () => internalProgram)
-    internalProgram
+    EitherT.right(internalProgram, Vector.empty)
   }
 
   private def combine(mainDesugarer: Desugarer, mainProgram: in.Program, imported: Iterable[(Desugarer, in.Program)]): in.Program = {

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)
+  }
+}