diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala index 1299f37..0e64254 100644 --- a/src/main/scala/viper/server/core/VerificationWorker.scala +++ b/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() } diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala index 0f4508f..b090d1c 100644 --- a/src/main/scala/viper/server/core/ViperCoreServer.scala +++ b/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) { diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala index 45ac04c..e2e1dbe 100644 --- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala +++ b/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 */ diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala index 100eb08..265990e 100644 --- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala +++ b/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) diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala index 23d605a..1928b8a 100644 --- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala +++ b/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 { diff --git a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala index 00920d7..0f81451 100644 --- a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala +++ b/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 { diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala index 86fcb4d..4852bc8 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala +++ b/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") diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index 3d6240d..0c4b5d4 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/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)