Add support for selective verification

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

@@ -32,6 +32,9 @@ case class ViperEnvelope(m: Message) extends Envelope
 class VerificationWorker(private val command: List[String],
                          private val programId: String,
                          private val program: Program,
+                         // Does the verification process target the whole file,
+                         // or just a specific function/method at a specific location?
+                         private val target: Option[SourcePosition],
                          override val logger: Logger,
                          private val config: ViperConfig)
                         (override val executor: VerificationExecutionContext)
@@ -102,6 +105,23 @@ class VerificationWorker(private val command: List[String],
     }
   }
 
+  override def mapEntityVerificationResult(entity: Entity, result: VerificationResult): VerificationResult = {
+    backend.mapEntityVerificationResult(entity, result)
+  }
+
+  override def registerTaskEnd(success: Boolean): Unit = {
+    // We need to enqueue the message for choosing a specific verification target
+    // in the source code here instead of doing it in the constructor
+    // of the verification worker, because at that point the task hasn't been created yet,
+    // and thus the message cant be sent.
+    target match {
+      case Some(t) => enqueueMessage(TargetSelectionReport(t))
+      case _ =>
+    }
+
+    super.registerTaskEnd(success);
+  }
+
   override def call(): Unit = run()
 }
 

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

@@ -12,10 +12,12 @@ import akka.util.Timeout
 import ch.qos.logback.classic.Logger
 import viper.server.ViperConfig
 import viper.server.vsi.{AstHandle, AstJobId, VerJobId, VerificationServer}
+import viper.silver.ast.{Function, HasLineColumn, Method, Node, Program, SourcePosition}
 import viper.silver.ast.Program
 import viper.silver.ast.utility.FileLoader
 import viper.silver.logger.ViperLogger
 
+import scala.collection.immutable.HashSet
 import scala.concurrent.duration._
 import scala.concurrent.Future
 import scala.language.postfixOps
@@ -75,7 +77,7 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
     ast_id
   }
 
-  def verifyWithAstJob(programId: String, ast_id: AstJobId, backend_config: ViperBackendConfig, localLogger: Option[Logger] = None): VerJobId = {
+  def verifyWithAstJob(programId: String, ast_id: AstJobId, backend_config: ViperBackendConfig, localLogger: Option[Logger] = None, verifyTarget: Option[HasLineColumn] = None): VerJobId = {
     val logger = combineLoggers(localLogger)
 
     if (!isRunning) throw new IllegalStateException("Instance of VerificationServer already stopped")
@@ -88,7 +90,44 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
         val task_backend_maybe_fut: Future[Option[VerificationWorker]] =
           handle_future.map((handle: AstHandle[Option[Program]]) => {
             val program_maybe_fut: Future[Option[Program]] = handle.artifact
-            program_maybe_fut.map(_.map(new VerificationWorker(args, programId, _, logger, config)(executor))).recover({
+            program_maybe_fut.map(_.map(p => {
+              val target: Option[(Node, SourcePosition)] = verifyTarget.flatMap(pos => {
+                (p.methods ++ p.functions).collectFirst(m =>  m.pos match {
+                  case p: SourcePosition  if p.start <= pos && p.end.getOrElse(p.start)  >= pos => (m, p)
+                })
+              });
+
+              if (!verifyTarget.isEmpty && target.isEmpty) {
+                logger.warn(s"Tried to verify target at position ${verifyTarget.get}, " +
+                  s"but no method or function exists at that position.")
+              }
+
+              val (updated_program, position) = target match {
+                // Remove unused functions, predicates and methods
+                // and make not-targeted methods abstract
+                case Some(root) => {
+                  val deps = HashSet() ++ (root._1 match {
+                    case m: Method => p.getMethodDependenciesWithMethods(p, m)
+                    case f: Function => p.getFunctionDependencies(p, f)
+                  })
+                  val functions = p.functions.filter(deps.contains(_))
+                  val predicates = p.predicates.filter(deps.contains(_))
+                  // For methods, we additionally make them abstract if they are not the target method
+                  val methods = p.methods.filter(deps.contains(_)).map(m => {
+                    if (m == root._1) {
+                      m
+                    } else {
+                      m.copy(body = None)(m.pos, m.info, m.errT)
+                    }
+                  })
+                  (p.copy(methods = methods, functions = functions, predicates = predicates)(p.pos, p.info, p.errT), Some(root._2))
+                }
+
+                case None => (p, None)
+              }
+
+              new VerificationWorker(args, programId, updated_program, position, logger, config)(executor)
+            })).recover({
               case e: Throwable =>
                 logger.error(s"### An exception has occurred while constructing Viper AST: $e")
                 throw e
@@ -113,7 +152,7 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
     val logger = combineLoggers(localLogger)
 
     val args: List[String] = backend_config.toList
-    val task_backend = new VerificationWorker(args, programId, program, logger, config)(executor)
+    val task_backend = new VerificationWorker(args, programId, program, None, logger, config)(executor)
     val ver_id = initializeVerificationProcess(Future.successful(Some(task_backend)), None)
 
     if (ver_id.id >= 0) {

src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala

@@ -9,6 +9,7 @@ package viper.server.frontends.lsp
 import ch.qos.logback.classic.Logger
 import org.eclipse.lsp4j.Range
 import viper.server.core.VerificationExecutionContext
+import viper.silver.ast.HasLineColumn
 
 import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap}
 import scala.concurrent.Future
@@ -153,11 +154,11 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
   }
 
   /** returns true if verification was started */
-  def startVerification(backendClassName: String, customArgs: String, uri: String, manuallyTriggered: Boolean): Future[Boolean] = {
+  def startVerification(backendClassName: String, customArgs: String, uri: String, manuallyTriggered: Boolean, verifyTarget: Option[HasLineColumn] = None): Future[Boolean] = {
     _previousFile.filter(_ != uri).foreach(resetDiagnosticsOne)
     _previousFile = Some(uri)
     val fm = getFileManager(uri)
-    fm.startVerification(backendClassName, customArgs, fm.content, manuallyTriggered)
+    fm.startVerification(backendClassName, customArgs, fm.content, manuallyTriggered, verifyTarget)
   }
 
   /** returns true if parse/typecheck was started */

src/main/scala/viper/server/frontends/lsp/DataProtocol.scala

@@ -85,6 +85,8 @@ case class VerifyParams (
               manuallyTriggered: Boolean,   // was the verification triggered manually
               workspace: String,            // the path to the open workspace folder
               backend: String,
+              verifyTarget: Position,       // A specific method/function at a position that should be verified,
+                                            // instead of the whole file.
               customArgs: String)            // contains the path of the file that should be verified
 
 case class SettingsError (errorType: SettingsErrorType, msg: String)
@@ -168,6 +170,9 @@ case class StateChangeParams(
               success: Int = NA.id,
               verificationCompleted: Double = -1,
               manuallyTriggered: Double = -1,
+              // The range of the source code that is currently being verified, if for example
+              // a specific method/function is verified instead of the whole file.
+              currentTarget: Range = null,
               filename: String = null,
               backendName: String = null,
               time: Double = -1, /** [sec] */
@@ -191,6 +196,10 @@ case class StopVerificationResponse(success: Boolean)
 
 case class GetLanguageServerUrlResponse(url: String)
 
+case class GetDefinitionsRequest(uri: String)
+
+case class GetDefinitionsResponse(definitions: Array[Definition])
+
 case class RemoveDiagnosticsRequest(uri: String)
 
 case class RemoveDiagnosticsResponse(success: Boolean)

src/main/scala/viper/server/frontends/lsp/Receiver.scala

@@ -13,6 +13,7 @@ import org.eclipse.lsp4j.services.{LanguageClient, LanguageClientAware, Language
 import org.eclipse.lsp4j._
 import viper.server.ViperConfig
 import viper.server.core.VerificationExecutionContext
+import viper.silver.ast.{LineColumnPosition, SourcePosition}
 import viper.viperserver.BuildInfo
 
 import scala.concurrent.Future
@@ -401,7 +402,9 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
       coordinator.stopAllRunningVerifications().map(_ => {
         coordinator.logger.info("start or restart verification")
 
-        coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered).map(verificationStarted => {
+        val verifyTarget = if(data.verifyTarget == null) None else Some(LineColumnPosition(data.verifyTarget.getLine + 1, data.verifyTarget.getCharacter + 1))
+
+        coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered, verifyTarget).map(verificationStarted => {
           if (verificationStarted) {
             coordinator.logger.info("Verification Started")
           } else {

src/main/scala/viper/server/frontends/lsp/ViperServerService.scala

@@ -17,6 +17,7 @@ import viper.server.utility.Helpers.validateViperFile
 import viper.server.vsi.VerificationProtocol.{StopAstConstruction, StopVerification}
 import viper.server.vsi.{AstJobId, DefaultVerificationServerStart, VerHandle, VerJobId}
 import viper.silver.ast.utility.FileLoader
+import viper.silver.ast.HasLineColumn
 
 import scala.concurrent.Future
 import scala.concurrent.duration._
@@ -36,13 +37,13 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve
     requestAst(file, backend, localLogger, loader)
   }
 
-  def verifyAst(astJob: AstJobId, file: String, backend: ViperBackendConfig, localLogger: Option[Logger] = None): VerJobId = {
+  def verifyAst(astJob: AstJobId, file: String, backend: ViperBackendConfig, localLogger: Option[Logger] = None, verifyTarget: Option[HasLineColumn] = None): VerJobId = {
     if (astJob.id < 0) {
       return VerJobId(-1)
     }
     val logger = combineLoggers(localLogger)
 
-    val ver_id = verifyWithAstJob(file, astJob, backend, localLogger)
+    val ver_id = verifyWithAstJob(file, astJob, backend, localLogger, verifyTarget)
     if (ver_id.id >= 0) {
       logger.info(s"Verification process #${ver_id.id} has successfully started.")
     } else {

src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala

@@ -7,6 +7,7 @@
 package viper.server.frontends.lsp.file
 
 import akka.actor.{Actor, PoisonPill, Props, Status}
+import org.eclipse.lsp4j.{Diagnostic, DiagnosticSeverity, DocumentSymbol, Position, PublishDiagnosticsParams, Range, SymbolKind}
 import viper.server.frontends.lsp
 import viper.server.frontends.lsp.VerificationState._
 import viper.server.frontends.lsp.VerificationSuccess._
@@ -45,6 +46,13 @@ trait MessageHandler extends ProjectManager with VerificationManager with Quanti
       var success = NA
       val mt = if (this.manuallyTriggered) 1 else 0
 
+      val target = currentTarget.map(p => {
+        val start = p.start
+        val end = p.end.getOrElse(p.start)
+
+        new Range(new Position(start.line - 1, start.column - 1), new Position(end.line - 1, end.column - 1))
+      }).getOrElse(null)
+
       val isVerifyingStage = true
 
       // do we need to start a followUp Stage?
@@ -55,7 +63,7 @@ trait MessageHandler extends ProjectManager with VerificationManager with Quanti
         coordinator.sendStateChangeNotification(params, Some(this))
 
         // notify client about outcome of verification
-        params = lsp.StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt,
+        params = lsp.StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt, currentTarget=target,
           filename = filename, time = timeMs.toDouble / 1000, verificationCompleted = 1, uri = file_uri,
           error = "")
         coordinator.sendStateChangeNotification(params, Some(this))
@@ -65,7 +73,7 @@ trait MessageHandler extends ProjectManager with VerificationManager with Quanti
         }
       } else {
         success = if (is_aborting) Aborted else Success
-        params = lsp.StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt,
+        params = lsp.StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt, currentTarget=target,
           filename = filename, time = timeMs.toDouble / 1000, verificationCompleted = 0, uri = file_uri,
           error = "")
         coordinator.sendStateChangeNotification(params, Some(this))
@@ -197,6 +205,8 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends
     case WarningsDuringVerification(warnings) =>
       markErrorsAsReported(warnings)
       task.processErrors(backendClassName, warnings)
+    case TargetSelectionReport(ts) =>
+        currentTarget = Some(ts)
     // the completion handler is not yet invoked (but as part of Status.Success)
     case QuantifierChosenTriggersMessage(qexp, triggers, oldTriggers) =>
       coordinator.logger.trace(s"[receive@${task.filename}/${backendClassName.isDefined}] QuantifierChosenTriggersMessage")

src/main/scala/viper/server/frontends/lsp/file/Verification.scala

@@ -25,6 +25,7 @@ import org.eclipse.lsp4j
 import viper.silver.ast.utility.lsp.RangePosition
 import viper.silver.ast.HasLineColumn
 import viper.silver.ast.LineColumnPosition
+import viper.silver.ast.SourcePosition
 
 case class VerificationHandler(server: lsp.ViperServerService, logger: Logger) {
   private var waitingOn: Option[Either[AstJobId, VerJobId]] = None
@@ -131,6 +132,10 @@ trait VerificationManager extends ManagesLeaf {
   var manuallyTriggered: Boolean = _
   var neverParsed: Boolean = true
 
+  // The range of the function/method we are currently verifying, if we are verifying a specific
+  // target instead of the whole file.
+  var currentTarget: Option[SourcePosition] = None
+
   //verification results
   var jid: Int = -1
   var timeMs: Long = 0
@@ -147,6 +152,7 @@ trait VerificationManager extends ManagesLeaf {
 
     is_verifying = true
     is_aborting = false
+    currentTarget = None
     state = Stopped
     neverParsed = false
     timeMs = 0
@@ -201,7 +207,7 @@ trait VerificationManager extends ManagesLeaf {
   }
 
   /** Do full parsing, type checking and verification */
-  def startVerification(backendClassName: String, customArgs: String, loader: FileContent, mt: Boolean): Future[Boolean] = {
+  def startVerification(backendClassName: String, customArgs: String, loader: FileContent, mt: Boolean, verifyTarget: Option[HasLineColumn] = None): Future[Boolean] = {
     val command = getVerificationCommand(backendClassName, customArgs)
     val backend = ViperBackendConfig(command);
 
@@ -214,7 +220,7 @@ trait VerificationManager extends ManagesLeaf {
         case None => return Future.successful(false)
         case Some(ast) => ast
       }
-      val verJob = coordinator.server.verifyAst(astJob, file.toString(), backend, Some(coordinator.localLogger))
+      val verJob = coordinator.server.verifyAst(astJob, file.toString(), backend, Some(coordinator.localLogger), verifyTarget)
       if (verJob.id >= 0) {
         // Execute all handles
         this.resetContainers(false)