From edddc68337c8936f0a2a4413cac20fe2135c8816 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Tue, 3 Jan 2023 17:22:47 +0100
Subject: [PATCH 1/5] adds another hook for plugins to translate entity
 verification results and adapts the plugins

---
 .../viper/silver/plugin/PluginTemplate.scala  | 10 +++
 .../viper/silver/plugin/SilverPlugin.scala    | 11 ++-
 .../silver/plugin/SilverPluginManager.scala   |  5 +-
 .../PredicateInstancePlugin.scala             |  9 +-
 .../plugin/standard/refute/RefutePlugin.scala | 86 +++++++++++++------
 .../termination/TerminationPlugin.scala       | 15 +++-
 6 files changed, 104 insertions(+), 32 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/PluginTemplate.scala b/src/main/scala/viper/silver/plugin/PluginTemplate.scala
index 8031d77b9..d0bfe92d4 100644
--- a/src/main/scala/viper/silver/plugin/PluginTemplate.scala
+++ b/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,6 +54,15 @@ 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.
       *
diff --git a/src/main/scala/viper/silver/plugin/SilverPlugin.scala b/src/main/scala/viper/silver/plugin/SilverPlugin.scala
index 3b6cc8ddd..39738f0b6 100644
--- a/src/main/scala/viper/silver/plugin/SilverPlugin.scala
+++ b/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,6 +74,15 @@ 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.
     *
diff --git a/src/main/scala/viper/silver/plugin/SilverPluginManager.scala b/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
index a8cd615ce..e3bf9b5c6 100644
--- a/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
+++ b/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,6 +54,9 @@ class SilverPluginManager(val plugins: Seq[SilverPlugin]) {
   def beforeVerify(input: Program): Option[Program] =
     foldWithError(input)((inp, plugin) => plugin.beforeVerify(inp))
 
+  def mapEntityVerificationResult(entity: Entity, input: VerificationResult): VerificationResult =
+    plugins.foldLeft(input)((inp, plugin) => plugin.mapEntityVerificationResult(entity, inp))
+
   def mapVerificationResult(input: VerificationResult): VerificationResult =
     plugins.foldLeft(input)((inp, plugin) => plugin.mapVerificationResult(inp))
 
diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
index ef896f847..22ecfe552 100644
--- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
+++ b/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(input: VerificationResult): VerificationResult =
+    translateVerificationResult(input)
+
+  private def translateVerificationResult(input: VerificationResult): VerificationResult = {
     input match {
       case Success => input
       case Failure(errors) =>
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
index 34b5cc199..73722ee63 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/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
 
@@ -28,6 +29,7 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
   private val refuteKeyword: String = "refute"
 
   private var refuteAsserts: Map[Position, Refute] = Map()
+  private var refuteAssertsPerEntity: Map[(Method, Position), Refute] = Map()
 
   /** Parser for refute statements. */
   def refute[_: P]: P[PRefute] =
@@ -46,40 +48,74 @@ 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 =>
+      ViperStrategy.Slim({
+        case r@Refute(exp) =>
+          this.refuteAsserts += (r.pos -> r)
+          this.refuteAssertsPerEntity += ((method, r.pos) -> r)
+          val refutesInMethod = this.refuteAssertsPerEntity.count {
+            case ((m, _), _) => method == m
+          }
+          val nonDetLocalVarDecl = LocalVarDecl(s"__plugin_refute_nondet$refutesInMethod", Bool)(r.pos)
+          Seqn(Seq(
+            If(nonDetLocalVarDecl.localVar,
+              Seqn(Seq(
+                Assert(exp)(r.pos, RefuteInfo),
+                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 and add refuteAsserts that didn't report an error. */
+  /** 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 = {
+    val occurredNonRefuteErrors = input match {
+      case Success => Seq()
+      case Failure(errors) =>
+        errors.filter {
+          case AssertFailed(a, _, _) if a.info == RefuteInfo =>
+            // remove entries whose method and position match:
+            this.refuteAssertsPerEntity = this.refuteAssertsPerEntity.filter {
+              case ((m, pos), _) if entity == m && a.pos == pos => false
+              case _ => true
+            }
+            false
+          case _ => true
+        }
+    }
+    val missingErrorsInEntity = this.refuteAssertsPerEntity.flatMap {
+      case ((m, _), refute) if entity == m => Some(RefuteFailed(refute, RefutationTrue(refute.exp)))
+      case _ => None
+    }
+    val errors = occurredNonRefuteErrors ++ missingErrorsInEntity
+    if (errors.isEmpty) Success
+    else Failure(errors)
+  }
+
+  /** Remove refutation related errors (for all entities) and add refuteAsserts (for all entities) that didn't report an error. */
   override def mapVerificationResult(input: VerificationResult): VerificationResult = {
-    val errors: Seq[AbstractError] = (input match {
+    val occurredNonRefuteErrors = input match {
       case Success => Seq()
-      case Failure(errors) => {
+      case Failure(errors) =>
         errors.filter {
-          case AssertFailed(a, _, _) if a.info == RefuteInfo => {
+          case AssertFailed(a, _, _) if a.info == RefuteInfo =>
             this.refuteAsserts -= a.pos
             false
-          }
           case _ => true
         }
-      }
-    }) ++ this.refuteAsserts.map(r => RefuteFailed(r._2, RefutationTrue(r._2.exp)))
-    if (errors.length == 0) Success
+    }
+    val missingErrorsInEntity = this.refuteAsserts.map {
+      case (_, refute) => RefuteFailed(refute, RefutationTrue(refute.exp))
+    }
+    val errors = occurredNonRefuteErrors ++ missingErrorsInEntity
+    if (errors.isEmpty) Success
     else Failure(errors)
   }
 }
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index c3ede19fc..657fafb92 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/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(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 {

From 4c256eb982f91f4a1d15ec9080c82367e63d92e1 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 5 Jan 2023 09:52:14 +0100
Subject: [PATCH 2/5] adds Viper AST as parameter to mapVerificationResult,
 moves Refute plugin state to the AST itself

---
 .../viper/silver/frontend/SilFrontend.scala   | 60 ++++++++-------
 .../viper/silver/plugin/PluginTemplate.scala  |  3 +-
 .../viper/silver/plugin/SilverPlugin.scala    |  3 +-
 .../silver/plugin/SilverPluginManager.scala   |  4 +-
 .../PredicateInstancePlugin.scala             |  2 +-
 .../standard/refute/RefuteASTExtension.scala  |  2 +-
 .../plugin/standard/refute/RefutePlugin.scala | 75 +++++++------------
 .../termination/TerminationPlugin.scala       |  2 +-
 src/test/scala/PluginTests.scala              |  7 +-
 9 files changed, 75 insertions(+), 83 deletions(-)

diff --git a/src/main/scala/viper/silver/frontend/SilFrontend.scala b/src/main/scala/viper/silver/frontend/SilFrontend.scala
index fa912b096..3c52d76f3 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontend.scala
+++ b/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)
   }
 }
diff --git a/src/main/scala/viper/silver/plugin/PluginTemplate.scala b/src/main/scala/viper/silver/plugin/PluginTemplate.scala
index d0bfe92d4..668cb567b 100644
--- a/src/main/scala/viper/silver/plugin/PluginTemplate.scala
+++ b/src/main/scala/viper/silver/plugin/PluginTemplate.scala
@@ -66,10 +66,11 @@ class PluginTemplate extends SilverPlugin {
     /** 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).
diff --git a/src/main/scala/viper/silver/plugin/SilverPlugin.scala b/src/main/scala/viper/silver/plugin/SilverPlugin.scala
index 39738f0b6..e0a5fc934 100644
--- a/src/main/scala/viper/silver/plugin/SilverPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/SilverPlugin.scala
@@ -86,10 +86,11 @@ trait SilverPlugin {
   /** 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).
diff --git a/src/main/scala/viper/silver/plugin/SilverPluginManager.scala b/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
index e3bf9b5c6..f8a0a8aab 100644
--- a/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
+++ b/src/main/scala/viper/silver/plugin/SilverPluginManager.scala
@@ -57,8 +57,8 @@ class SilverPluginManager(val plugins: Seq[SilverPlugin]) {
   def mapEntityVerificationResult(entity: Entity, input: VerificationResult): VerificationResult =
     plugins.foldLeft(input)((inp, plugin) => plugin.mapEntityVerificationResult(entity, inp))
 
-  def mapVerificationResult(input: VerificationResult): VerificationResult =
-    plugins.foldLeft(input)((inp, plugin) => plugin.mapVerificationResult(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))
diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
index 22ecfe552..a8e8cc6ef 100644
--- a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
@@ -102,7 +102,7 @@ class PredicateInstancePlugin(@unused reporter: viper.silver.reporter.Reporter,
   /**
    * 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 = {
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala
index 31e230819..ef67564c9 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefuteASTExtension.scala
+++ b/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)
diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
index 73722ee63..07fcbb7de 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -28,9 +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()
-  private var refuteAssertsPerEntity: Map[(Method, Position), Refute] = Map()
-
   /** Parser for refute statements. */
   def refute[_: P]: P[PRefute] =
     FP(keyword(refuteKeyword) ~/ exp).map{ case (pos, e) => PRefute(e)(pos) }
@@ -49,19 +46,16 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
    * The ⭐ is nice since such a variable name cannot be parsed, but will it cause issues?
    */
   override def beforeVerify(input: Program): Program = {
-    val transformedMethods = input.methods.map(method =>
+    val transformedMethods = input.methods.map(method => {
+      var refutesInMethod = 0
       ViperStrategy.Slim({
         case r@Refute(exp) =>
-          this.refuteAsserts += (r.pos -> r)
-          this.refuteAssertsPerEntity += ((method, r.pos) -> r)
-          val refutesInMethod = this.refuteAssertsPerEntity.count {
-            case ((m, _), _) => method == m
-          }
+          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),
+                Assert(exp)(r.pos, RefuteInfo(r)),
                 Inhale(BoolLit(false)(r.pos))(r.pos)
               ), Seq())(r.pos),
               Seqn(Seq(), Seq())(r.pos))(r.pos)
@@ -70,52 +64,39 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
           )(r.pos)
       }).recurseFunc({
         case Method(_, _, _, _, _, body) => Seq(body)
-      }).execute[Method](method))
+      }).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 = {
-    val occurredNonRefuteErrors = input match {
-      case Success => Seq()
-      case Failure(errors) =>
-        errors.filter {
-          case AssertFailed(a, _, _) if a.info == RefuteInfo =>
-            // remove entries whose method and position match:
-            this.refuteAssertsPerEntity = this.refuteAssertsPerEntity.filter {
-              case ((m, pos), _) if entity == m && a.pos == pos => false
-              case _ => true
-            }
-            false
-          case _ => true
-        }
-    }
-    val missingErrorsInEntity = this.refuteAssertsPerEntity.flatMap {
-      case ((m, _), refute) if entity == m => Some(RefuteFailed(refute, RefutationTrue(refute.exp)))
-      case _ => None
-    }
-    val errors = occurredNonRefuteErrors ++ missingErrorsInEntity
-    if (errors.isEmpty) Success
-    else Failure(errors)
-  }
+  override def mapEntityVerificationResult(entity: Entity, input: VerificationResult): VerificationResult =
+    mapVerificationResultsForNode(entity, input)
 
   /** Remove refutation related errors (for all entities) and add refuteAsserts (for all entities) that didn't report an error. */
-  override def mapVerificationResult(input: VerificationResult): VerificationResult = {
-    val occurredNonRefuteErrors = input match {
-      case Success => Seq()
-      case Failure(errors) =>
-        errors.filter {
-          case AssertFailed(a, _, _) if a.info == RefuteInfo =>
-            this.refuteAsserts -= a.pos
-            false
-          case _ => true
-        }
+  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)
+        case err => Right(err)
+      }
     }
-    val missingErrorsInEntity = this.refuteAsserts.map {
-      case (_, refute) => RefuteFailed(refute, RefutationTrue(refute.exp))
+    val refutesContainedInNode = n.collect {
+      case NodeWithInfo(RefuteInfo(r)) => r
     }
-    val errors = occurredNonRefuteErrors ++ missingErrorsInEntity
+    val refutesForWhichNoErrorOccurred = refutesContainedInNode.filterNot(refutesForWhichErrorOccurred.contains(_))
+    val missingErrorsInNode = refutesForWhichNoErrorOccurred.map(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)
+}
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
index 657fafb92..5c3cdf776 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -128,7 +128,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
   /**
     * Call the error transformation on possibly termination 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 = {
diff --git a/src/test/scala/PluginTests.scala b/src/test/scala/PluginTests.scala
index b4bd92be1..ec953e27f 100644
--- a/src/test/scala/PluginTests.scala
+++ b/src/test/scala/PluginTests.scala
@@ -5,7 +5,6 @@
 // Copyright (c) 2011-2021 ETH Zurich.
 
 import java.nio.file.Paths
-
 import org.scalatest.funsuite.AnyFunSuite
 import viper.silver.ast.{LocalVar, Perm, Program}
 import viper.silver.frontend.{SilFrontend, SilFrontendConfig}
@@ -17,6 +16,8 @@ import viper.silver.verifier.reasons.FeatureUnsupported
 import viper.silver.verifier._
 import viper.silver.ast.NoPosition
 
+import scala.annotation.unused
+
 trait TestPlugin {
   def test(): Boolean = true
 }
@@ -148,7 +149,7 @@ class TestPluginMapErrors extends SilverPlugin with TestPlugin with FakeResult {
   var error2: Internal = Internal(FeatureUnsupported(LocalVar("test2", Perm)(), "Test2"))
   var finish = false
 
-  override def mapVerificationResult(input: VerificationResult): VerificationResult = {
+  override def mapVerificationResult(@unused program: Program, input: VerificationResult): VerificationResult = {
     input match {
       case Success =>
 //        println(">>> detected VerificationResult is Success")
@@ -197,7 +198,7 @@ class TestPluginMapVsFinish extends SilverPlugin with TestPlugin {
     input
   }
 
-  override def mapVerificationResult(input: VerificationResult): VerificationResult = {
+  override def mapVerificationResult(@unused program: Program, input: VerificationResult): VerificationResult = {
     assert(!finish)
     input
   }

From f99261c724b05238716cf53330a4095d2cf49777 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 5 Jan 2023 15:30:02 +0100
Subject: [PATCH 3/5] fixes refute plugin to only consider positional
 information when determining whether a verification has occurred or not for a
 given refute statement

---
 .../silver/plugin/standard/refute/RefutePlugin.scala   | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
index 07fcbb7de..a59747517 100644
--- a/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
+++ b/src/main/scala/viper/silver/plugin/standard/refute/RefutePlugin.scala
@@ -81,15 +81,19 @@ class RefutePlugin(@unused reporter: viper.silver.reporter.Reporter,
     val (refutesForWhichErrorOccurred, otherErrors) = input match {
       case Success => (Seq.empty, Seq.empty)
       case Failure(errors) => errors.partitionMap {
-        case AssertFailed(NodeWithInfo(RefuteInfo(r)), _, _) => Left(r)
+        case AssertFailed(NodeWithInfo(RefuteInfo(r)), _, _) => Left((r, r.pos))
         case err => Right(err)
       }
     }
     val refutesContainedInNode = n.collect {
-      case NodeWithInfo(RefuteInfo(r)) => r
+      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(refute => RefuteFailed(refute, RefutationTrue(refute.exp)))
+    val missingErrorsInNode = refutesForWhichNoErrorOccurred.map{
+      case (refute, _) => RefuteFailed(refute, RefutationTrue(refute.exp))
+    }
 
     val errors = otherErrors ++ missingErrorsInNode
     if (errors.isEmpty) Success

From 504198e8b5542fbfb300e9dedb88ec4dbd4348c8 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Thu, 5 Jan 2023 16:08:48 +0100
Subject: [PATCH 4/5] fixes silver unit test

---
 src/test/scala/AstPositionsTests.scala | 63 ++++++++++++--------------
 1 file changed, 28 insertions(+), 35 deletions(-)

diff --git a/src/test/scala/AstPositionsTests.scala b/src/test/scala/AstPositionsTests.scala
index fb1c3b624..c8cdd2c30 100644
--- a/src/test/scala/AstPositionsTests.scala
+++ b/src/test/scala/AstPositionsTests.scala
@@ -111,44 +111,37 @@ class AstPositionsTests extends AnyFunSuite {
         fail("method posts must have start and end positions set")
     }
     // Check position of body
-    if (m.body.get.ss.length == 1) {
-      val block: Stmt = m.body.get.ss(0)
-      block.pos match {
-        case spos: AbstractSourcePosition => {
-          assert(spos.start.line === 5 && spos.end.get.line === 10)
-          assert(spos.start.column === 1 && spos.end.get.column === 2)
-        }
-        case _ =>
-          fail("statements must have start and end positions set")
+    val block = m.body.get
+    block.pos match {
+      case spos: AbstractSourcePosition => {
+        assert(spos.start.line === 5 && spos.end.get.line === 10)
+        assert(spos.start.column === 1 && spos.end.get.column === 2)
       }
-      if (block.isInstanceOf[Seqn]) {
-        // Check position of forall
-        assert(block.asInstanceOf[Seqn].ss.length === 4)
-        val forall: Stmt = block.asInstanceOf[Seqn].ss(0)
-        forall.pos match {
-          case spos: AbstractSourcePosition => {
-            assert(spos.start.line === 6 && spos.end.get.line === 6)
-            assert(spos.start.column === 3 && spos.end.get.column === 48)
-          }
-          case _ =>
-            fail("forall must have start and end positions set")
-        };
-        // Check position of assert
-        val assert_exp: Exp = block.asInstanceOf[Seqn].ss(1).asInstanceOf[Assert].exp
-        assert_exp.pos match {
-          case spos: AbstractSourcePosition => {
-            assert(spos.start.line === 7 && spos.end.get.line === 7)
-            assert(spos.start.column === 10 && spos.end.get.column === 20)
-          }
-          case _ =>
-            fail("forall must have start and end positions set")
-        }
-      } else {
-        fail("Failed to check position of statements in method body due to layout change")
+      case _ =>
+        fail("statements must have start and end positions set")
+    }
+    // Check position of forall
+    assert(block.ss.length === 4)
+    val forall: Stmt = block.ss(0)
+    forall.pos match {
+      case spos: AbstractSourcePosition => {
+        assert(spos.start.line === 6 && spos.end.get.line === 6)
+        assert(spos.start.column === 3 && spos.end.get.column === 48)
       }
-    } else {
-      fail("Failed to check position of statements in method body due to layout change")
+      case _ =>
+        fail("forall must have start and end positions set")
+    };
+    // Check position of assert
+    val assert_exp: Exp = block.ss(1).asInstanceOf[Assert].exp
+    assert_exp.pos match {
+      case spos: AbstractSourcePosition => {
+        assert(spos.start.line === 7 && spos.end.get.line === 7)
+        assert(spos.start.column === 10 && spos.end.get.column === 20)
+      }
+      case _ =>
+        fail("forall must have start and end positions set")
     }
+
     // Check position of second method
     val m2: Method = res.methods(1);
     m2.pos match {

From 98d8c8145471c51507518152a5eda00f48f00423 Mon Sep 17 00:00:00 2001
From: Linard Arquint <linard.arquint@inf.ethz.ch>
Date: Fri, 6 Jan 2023 16:43:16 +0100
Subject: [PATCH 5/5] implements CR suggestions by Marco

---
 src/main/scala/viper/silver/plugin/PluginTemplate.scala | 5 +++--
 src/main/scala/viper/silver/plugin/SilverPlugin.scala   | 5 +++--
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/PluginTemplate.scala b/src/main/scala/viper/silver/plugin/PluginTemplate.scala
index 668cb567b..4c447e4b8 100644
--- a/src/main/scala/viper/silver/plugin/PluginTemplate.scala
+++ b/src/main/scala/viper/silver/plugin/PluginTemplate.scala
@@ -54,8 +54,9 @@ 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.
+    /** Called after the verification of an entity, which is used to stream verification results to the IDE
+      * (which happens as soon as a member has been verified). Error transformation should happen here.
+      * This will only be called if verification of `entity` took place.
       *
       * @param entity Entity to which `input` belongs
       * @param input Result of verification
diff --git a/src/main/scala/viper/silver/plugin/SilverPlugin.scala b/src/main/scala/viper/silver/plugin/SilverPlugin.scala
index e0a5fc934..082a6c353 100644
--- a/src/main/scala/viper/silver/plugin/SilverPlugin.scala
+++ b/src/main/scala/viper/silver/plugin/SilverPlugin.scala
@@ -74,8 +74,9 @@ 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.
+  /** Called after the verification of an entity, which is used to stream verification results to the IDE
+    * (which happens as soon as a member has been verified). Error transformation should happen here.
+    * This will only be called if verification of `entity` took place.
     *
     * @param entity Entity to which `input` belongs
     * @param input Result of verification