[Plugin] Translation of Entity Verification Results

src/main/scala/viper/silver/frontend/SilFrontend.scala

@@ -215,13 +215,41 @@ trait SilFrontend extends DefaultFrontend {
     }
   }
 
-  override def verification() = {
+  override def verification(): Unit = {
+    def filter(input: Program): Result[Program]  = {
+      _plugins.beforeMethodFilter(input) match {
+        case Some(inputPlugin) =>
+          // Filter methods according to command-line arguments.
+          val verifyMethods =
+            if (config != null && config.methods() != ":all") Seq("methods", config.methods())
+            else inputPlugin.methods map (_.name)
+
+          val methods = inputPlugin.methods filter (m => verifyMethods.contains(m.name))
+          val program = Program(inputPlugin.domains, inputPlugin.fields, inputPlugin.functions, inputPlugin.predicates, methods, inputPlugin.extensions)(inputPlugin.pos, inputPlugin.info, inputPlugin.errT)
+
+          _plugins.beforeVerify(program) match {
+            case Some(programPlugin) => Succ(programPlugin)
+            case None => Fail(_plugins.errors)
+          }
+
+        case None => Fail(_plugins.errors)
+      }
+    }
+
+    if (state == DefaultStates.ConsistencyCheck && _errors.isEmpty) {
+      filter(_program.get) match {
+        case Succ(program) => _program = Some(program)
+        case Fail(errors) => _errors ++= errors
+      }
+    }
     super.verification()
-    _verificationResult = _verificationResult.map(_plugins.mapVerificationResult)
+    _verificationResult = _verificationResult.map(_plugins.mapVerificationResult(_program.get, _))
   }
 
   def finish(): Unit = {
-    _plugins.beforeFinish(result) match {
+    val res = _plugins.beforeFinish(result)
+    _verificationResult = Some(res)
+    res match {
       case Success =>
         reporter report OverallSuccessMessage(verifier.name, getTime)
       case f: Failure =>
@@ -301,32 +329,12 @@ trait SilFrontend extends DefaultFrontend {
   }
 
   def doConsistencyCheck(input: Program): Result[Program]= {
-    def filter(input: Program): Result[Program]  = {
-      _plugins.beforeMethodFilter(input) match {
-        case Some(inputPlugin) =>
-          // Filter methods according to command-line arguments.
-          val verifyMethods =
-            if (config != null && config.methods() != ":all") Seq("methods", config.methods())
-            else inputPlugin.methods map (_.name)
-
-          val methods = inputPlugin.methods filter (m => verifyMethods.contains(m.name))
-          val program = Program(inputPlugin.domains, inputPlugin.fields, inputPlugin.functions, inputPlugin.predicates, methods, inputPlugin.extensions)(inputPlugin.pos, inputPlugin.info)
-
-          _plugins.beforeVerify(program) match {
-            case Some(programPlugin) => Succ(programPlugin)
-            case None => Fail(_plugins.errors)
-          }
-
-        case None => Fail(_plugins.errors)
-      }
-    }
-
     var errors = input.checkTransitively
     if (backendTypeFormat.isDefined)
       errors = errors ++ Consistency.checkBackendTypes(input, backendTypeFormat.get)
-    if (errors.isEmpty)
-      filter(input)
-    else
+    if (errors.isEmpty) {
+      Succ(input)
+    } else
       Fail(errors)
   }
 }

src/main/scala/viper/silver/plugin/PluginTemplate.scala

@@ -8,6 +8,7 @@ package viper.silver.plugin
 
 import viper.silver.ast.Program
 import viper.silver.parser.PProgram
+import viper.silver.reporter.Entity
 import viper.silver.verifier.{AbstractError, VerificationResult}
 
 // The aim of this file is just to give a skeleton implementation to copy for a particular plugin implementation.
@@ -53,13 +54,23 @@ class PluginTemplate extends SilverPlugin {
       */
     override def beforeVerify(input: Program) : Program = ???
 
+    /** Called after the verification of an entity. Error transformation should happen here.
+      * This will only be called if verification took place.
+      *
+      * @param entity Entity to which `input` belongs
+      * @param input Result of verification
+      * @return Modified result
+      */
+    override def mapEntityVerificationResult(entity: Entity, input: VerificationResult): VerificationResult = ???
+
     /** Called after the verification. Error transformation should happen here.
       * This will only be called if verification took place.
       *
+      * @param program Viper AST
       * @param input Result of verification
       * @return Modified result
       */
-    override def mapVerificationResult(input: VerificationResult): VerificationResult = ???
+    override def mapVerificationResult(program: Program, input: VerificationResult): VerificationResult = ???
 
     /** Called after the verification just before the result is printed. Will not be called in tests.
       * This will also be called even if verification did not take place (i.e. an error during parsing/translation occurred).

src/main/scala/viper/silver/plugin/SilverPlugin.scala

@@ -10,7 +10,7 @@ import ch.qos.logback.classic.Logger
 import viper.silver.ast.Program
 import viper.silver.frontend.SilFrontendConfig
 import viper.silver.parser.{FastParser, PProgram}
-import viper.silver.reporter.Reporter
+import viper.silver.reporter.{Entity, Reporter}
 import viper.silver.verifier.{AbstractError, VerificationResult}
 
 import scala.annotation.unused
@@ -74,13 +74,23 @@ trait SilverPlugin {
     */
   def beforeVerify(input: Program) : Program = input
 
+  /** Called after the verification of an entity. Error transformation should happen here.
+    * This will only be called if verification took place.
+    *
+    * @param entity Entity to which `input` belongs
+    * @param input Result of verification
+    * @return Modified result
+    */
+  def mapEntityVerificationResult(entity: Entity, input: VerificationResult): VerificationResult = input
+
   /** Called after the verification. Error transformation should happen here.
     * This will only be called if verification took place.
     *
+    * @param program Viper AST
     * @param input Result of verification
     * @return Modified result
     */
-  def mapVerificationResult(input: VerificationResult): VerificationResult = input
+  def mapVerificationResult(program: Program, input: VerificationResult): VerificationResult = input
 
   /** Called after the verification just before the result is printed. Will not be called in tests.
     * This will also be called even if verification did not take place (i.e. an error during parsing/translation occurred).

src/main/scala/viper/silver/plugin/SilverPluginManager.scala

@@ -10,7 +10,7 @@ import ch.qos.logback.classic.Logger
 import viper.silver.ast._
 import viper.silver.frontend.SilFrontendConfig
 import viper.silver.parser.{FastParser, PProgram}
-import viper.silver.reporter.Reporter
+import viper.silver.reporter.{Entity, Reporter}
 import viper.silver.verifier.{AbstractError, VerificationResult}
 
 /** Manage the loaded plugins and execute them during the different hooks (see [[viper.silver.plugin.SilverPlugin]]).
@@ -54,8 +54,11 @@ class SilverPluginManager(val plugins: Seq[SilverPlugin]) {
   def beforeVerify(input: Program): Option[Program] =
     foldWithError(input)((inp, plugin) => plugin.beforeVerify(inp))
 
-  def mapVerificationResult(input: VerificationResult): VerificationResult =
-    plugins.foldLeft(input)((inp, plugin) => plugin.mapVerificationResult(inp))
+  def mapEntityVerificationResult(entity: Entity, input: VerificationResult): VerificationResult =
+    plugins.foldLeft(input)((inp, plugin) => plugin.mapEntityVerificationResult(entity, inp))
+
+  def mapVerificationResult(program: Program, input: VerificationResult): VerificationResult =
+    plugins.foldLeft(input)((inp, plugin) => plugin.mapVerificationResult(program, inp))
 
   def beforeFinish(input: VerificationResult): VerificationResult =
     plugins.foldLeft(input)((inp, plugin) => plugin.beforeFinish(inp))

src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala

@@ -15,6 +15,7 @@ import viper.silver.verifier.{ConsistencyError, Failure, Success, VerificationRe
 import viper.silver.verifier.errors.PreconditionInAppFalse
 import fastparse._
 import viper.silver.parser.FastParserCompanion.whitespace
+import viper.silver.reporter.Entity
 
 import scala.annotation.unused
 import scala.collection.immutable.ListMap
@@ -95,10 +96,16 @@ class PredicateInstancePlugin(@unused reporter: viper.silver.reporter.Reporter,
     newProgram
   }
 
+  override def mapEntityVerificationResult(entity: Entity, input: VerificationResult): VerificationResult =
+    translateVerificationResult(input)
+
   /**
    * Initiate the error transformer for possibly predicate instances related errors
    */
-  override def mapVerificationResult(input: VerificationResult): VerificationResult = {
+  override def mapVerificationResult(@unused program: Program, input: VerificationResult): VerificationResult =
+    translateVerificationResult(input)
+
+  private def translateVerificationResult(input: VerificationResult): VerificationResult = {
     input match {
       case Success => input
       case Failure(errors) =>

src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala

@@ -11,7 +11,7 @@ import viper.silver.ast.pretty.FastPrettyPrinter.{ContOps, text, toParenDoc}
 import viper.silver.ast.pretty.PrettyPrintPrimitives
 
 /** An `FailureExpectedInfo` info that tells us that this assert is a refute. */
-case object RefuteInfo extends FailureExpectedInfo
+case class RefuteInfo(refute: Refute) extends FailureExpectedInfo
 
 case class Refute(exp: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends ExtensionStmt {
   override lazy val prettyPrint: PrettyPrintPrimitives#Cont = text("refute") <+> toParenDoc(exp)

src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala

@@ -12,6 +12,7 @@ import viper.silver.ast._
 import viper.silver.parser.FastParserCompanion.whitespace
 import viper.silver.parser.FastParser
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
+import viper.silver.reporter.Entity
 import viper.silver.verifier._
 import viper.silver.verifier.errors.AssertFailed
 
@@ -27,8 +28,6 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
   /** Keyword used to define refute statements. */
   private val refuteKeyword: String = "refute"
 
-  private var refuteAsserts: Map[Position, Refute] = Map()
-
   /** Parser for refute statements. */
   def refute[_: P]: P[PRefute] =
     FP(keyword(refuteKeyword) ~/ exp).map{ case (pos, e) => PRefute(e)(pos) }
@@ -46,40 +45,62 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
    * Remove refute statements from the AST and add them as non-det asserts.
    * The ⭐ is nice since such a variable name cannot be parsed, but will it cause issues?
    */
-  override def beforeVerify(input: Program): Program =
-    ViperStrategy.Slim({
-      case r@Refute(exp) => {
-        this.refuteAsserts += (r.pos -> r)
-        Seqn(Seq(
-          If(LocalVar(s"__plugin_refute_nondet${this.refuteAsserts.size}", Bool)(r.pos),
-            Seqn(Seq(
-              Assert(exp)(r.pos, RefuteInfo),
-              Inhale(BoolLit(false)(r.pos))(r.pos)
-            ), Seq())(r.pos),
-            Seqn(Seq(), Seq())(r.pos))(r.pos)
+  override def beforeVerify(input: Program): Program = {
+    val transformedMethods = input.methods.map(method => {
+      var refutesInMethod = 0
+      ViperStrategy.Slim({
+        case r@Refute(exp) =>
+          refutesInMethod += 1
+          val nonDetLocalVarDecl = LocalVarDecl(s"__plugin_refute_nondet$refutesInMethod", Bool)(r.pos)
+          Seqn(Seq(
+            If(nonDetLocalVarDecl.localVar,
+              Seqn(Seq(
+                Assert(exp)(r.pos, RefuteInfo(r)),
+                Inhale(BoolLit(false)(r.pos))(r.pos)
+              ), Seq())(r.pos),
+              Seqn(Seq(), Seq())(r.pos))(r.pos)
           ),
-          Seq(LocalVarDecl(s"__plugin_refute_nondet${this.refuteAsserts.size}", Bool)(r.pos))
-        )(r.pos)
-      }
-    }).recurseFunc({
-      case Method(_, _, _, _, _, body) => Seq(body)
-    }).execute(input)
+            Seq(nonDetLocalVarDecl)
+          )(r.pos)
+      }).recurseFunc({
+        case Method(_, _, _, _, _, body) => Seq(body)
+      }).execute[Method](method)
+    })
+    Program(input.domains, input.fields, input.functions, input.predicates, transformedMethods, input.extensions)(input.pos, input.info, input.errT)
+  }
+
+  /** Remove refutation related errors for the current entity and add refuteAsserts in this entity that didn't report an error. */
+  override def mapEntityVerificationResult(entity: Entity, input: VerificationResult): VerificationResult =
+    mapVerificationResultsForNode(entity, input)
 
-  /** Remove refutation related errors and add refuteAsserts that didn't report an error. */
-  override def mapVerificationResult(input: VerificationResult): VerificationResult = {
-    val errors: Seq[AbstractError] = (input match {
-      case Success => Seq()
-      case Failure(errors) => {
-        errors.filter {
-          case AssertFailed(a, _, _) if a.info == RefuteInfo => {
-            this.refuteAsserts -= a.pos
-            false
-          }
-          case _ => true
-        }
+  /** Remove refutation related errors (for all entities) and add refuteAsserts (for all entities) that didn't report an error. */
+  override def mapVerificationResult(program: Program, input: VerificationResult): VerificationResult =
+    mapVerificationResultsForNode(program, input)
+
+  private def mapVerificationResultsForNode(n: Node, input: VerificationResult): VerificationResult = {
+    val (refutesForWhichErrorOccurred, otherErrors) = input match {
+      case Success => (Seq.empty, Seq.empty)
+      case Failure(errors) => errors.partitionMap {
+        case AssertFailed(NodeWithInfo(RefuteInfo(r)), _, _) => Left((r, r.pos))
+        case err => Right(err)
       }
-    }) ++ this.refuteAsserts.map(r => RefuteFailed(r._2, RefutationTrue(r._2.exp)))
-    if (errors.length == 0) Success
+    }
+    val refutesContainedInNode = n.collect {
+      case NodeWithInfo(RefuteInfo(r)) => (r, r.pos)
+    }
+    // note that we include positional information in `refutesForWhichErrorOccurred` and `refutesContainedInNode` such
+    // that we do not miss errors just because the same refute statement occurs multiple times
+    val refutesForWhichNoErrorOccurred = refutesContainedInNode.filterNot(refutesForWhichErrorOccurred.contains(_))
+    val missingErrorsInNode = refutesForWhichNoErrorOccurred.map{
+      case (refute, _) => RefuteFailed(refute, RefutationTrue(refute.exp))
+    }
+
+    val errors = otherErrors ++ missingErrorsInNode
+    if (errors.isEmpty) Success
     else Failure(errors)
   }
 }
+
+object NodeWithInfo {
+  def unapply(node : Node) : Option[Info] = Some(node.meta._2)
+}

src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala

@@ -13,10 +13,11 @@ import viper.silver.parser._
 import viper.silver.plugin.standard.predicateinstance.PPredicateInstance
 import viper.silver.plugin.standard.termination.transformation.Trafo
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
-import viper.silver.verifier.errors.AssertFailed
+import viper.silver.verifier.errors.{AssertFailed, PreconditionInAppFalse}
 import viper.silver.verifier._
 import fastparse._
 import viper.silver.parser.FastParserCompanion.whitespace
+import viper.silver.reporter.Entity
 
 import scala.annotation.unused
 
@@ -121,10 +122,16 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
     }
   }
 
+  override def mapEntityVerificationResult(entity: Entity, input: VerificationResult): VerificationResult =
+    translateVerificationResult(input)
+
   /**
-   * Call the error transformation on possibly termination related errors.
-   */
-  override def mapVerificationResult(input: VerificationResult): VerificationResult = {
+    * Call the error transformation on possibly termination related errors.
+    */
+  override def mapVerificationResult(@unused program: Program, input: VerificationResult): VerificationResult =
+    translateVerificationResult(input)
+
+  private def translateVerificationResult(input: VerificationResult): VerificationResult = {
     if (deactivated) return input // if decreases checks are deactivated no verification result mapping is required.
 
     input match {