Merge branch 'master' into lsp

Author: JonasAlaif

carbon

@@ -1,6 +1,6 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.15.0")
-addSbtPlugin("com.typesafe.sbt" % "sbt-native-packager" % "1.7.6")
-addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.10.0")
+addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "2.3.1")
+addSbtPlugin("com.github.sbt" % "sbt-native-packager" % "1.11.1")
+addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.13.1")

project/plugins.sbt

@@ -12,8 +12,7 @@ import viper.server.utility.AstGenerator
 import viper.server.vsi.AstConstructionException
 import viper.silver.ast.Program
 import viper.silver.ast.utility.FileLoader
-import viper.silver.reporter.{Entity, ExceptionReport}
-import viper.silver.verifier.VerificationResult
+import viper.silver.reporter.ExceptionReport
 
 
 object ViperFileNotFoundException extends AstConstructionException
@@ -65,10 +64,5 @@ class AstWorker(val file: String,
     ast_option
   }
 
-  override def mapEntityVerificationResult(entity: Entity, result: VerificationResult): VerificationResult = {
-    logger.error(s"unexpected operation: AstWorker received an entity success or entity failure message, which should not occur while constructing a Viper AST")
-    ???
-  }
-
   override def call(): Option[Program] = constructAst(args)
 }

silicon

@@ -8,7 +8,7 @@ package viper.server.core
 
 import ch.qos.logback.classic.Logger
 import viper.server.vsi.MessageStreamingTask
-import viper.silver.reporter.{Entity, EntityFailureMessage, EntitySuccessMessage, Message, Reporter, Time, VerificationResultMessage}
+import viper.silver.reporter.{Entity, EntityFailureMessage, EntitySuccessMessage, Message, PluginAwareReporter, Time, VerificationResultMessage}
 import viper.silver.verifier.{Success, VerificationResult}
 
 trait MessageReportingTask[T] extends MessageStreamingTask[T] with ViperPost {
@@ -24,34 +24,18 @@ trait MessageReportingTask[T] extends MessageStreamingTask[T] with ViperPost {
     super.registerTaskEnd(success, logger)
   }
 
-  /** implementations of this functions should let plugins map verification results for each entity */
-  def mapEntityVerificationResult(entity: Entity, result: VerificationResult): VerificationResult
-
-  private def processEntityResultMessage(verifier: String, entity: Entity,
-                                         verificationTime: Time, result: VerificationResult, cached: Boolean): Unit = {
-    val mappedResult = mapEntityVerificationResult(entity, result)
-    enqueueMessage(VerificationResultMessage(verifier, entity, verificationTime, mappedResult, cached))
-  }
-
   // Implementation of the Reporter interface used by the backend.
-  class ActorReporter(tag: String) extends Reporter {
+  class ActorReporter(tag: String) extends PluginAwareReporter {
     val name = s"ViperServer_$tag"
 
-    def report(msg: Message): Unit = {
+    def doReport(msg: Message): Unit = {
       logger.trace(s"ActorReport received msg $msg")
       msg match {
         case m: EntityFailureMessage if m.concerning.info.isCached =>
         case m: EntitySuccessMessage if m.concerning.info.isCached =>
           // Do not re-send messages about AST nodes that have been cached;
           // the information about these nodes is going to be reported anyway.
 
-        // to properly support streaming of (partial) verification results, we must invoke
-        // the plugins to do the post-processing and enqueue the resulting message:
-        case EntitySuccessMessage(verifier, entity, verificationTime, cached) =>
-          processEntityResultMessage(verifier, entity, verificationTime, Success, cached)
-        case EntityFailureMessage(verifier, entity, verificationTime, failure, cached) =>
-          processEntityResultMessage(verifier, entity, verificationTime, failure, cached)
-
         case m =>
           enqueueMessage(m)
       }

src/main/scala/viper/server/core/AstWorker.scala

@@ -102,10 +102,6 @@ class VerificationWorker(private val command: List[String],
     }
   }
 
-  override def mapEntityVerificationResult(entity: Entity, result: VerificationResult): VerificationResult = {
-    backend.mapEntityVerificationResult(entity, result)
-  }
-
   override def call(): Unit = run()
 }
 
@@ -253,11 +249,6 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend,
   private def verification(input: Program): Either[Seq[AbstractError], VerificationResult] =
     Right(_frontend.verifier.verify(input))
 
-  def mapEntityVerificationResult(entity: Entity, verificationResult: VerificationResult): VerificationResult = {
-    if (disablePlugins) verificationResult
-    else _frontend.plugins.mapEntityVerificationResult(entity, verificationResult)
-  }
-
   private def mapVerificationResult(input: Program, result: VerificationResult): VerificationResult =
     if (disablePlugins) result
     else _frontend.plugins.mapVerificationResult(input, result)