Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add extra lsp features #204

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -8,3 +8,6 @@ ter.bat
ver.bat
.bsp/
logs/
.bloop
.metals
metals.sbt
4 changes: 2 additions & 2 deletions build.sbt
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ lazy val server = (project in file("."))
// General settings
name := "ViperServer",
organization := "viper",
version := "2.0.0", // has to be a proper semver
version := "3.0.0", // has to be a proper semver

// Fork test to a different JVM than SBT's, avoiding SBT's classpath interfering with
// classpath used by Scala's reflection.
Expand All @@ -30,7 +30,7 @@ lazy val server = (project in file("."))
libraryDependencies += "com.typesafe.akka" %% "akka-stream" % "2.6.10",
libraryDependencies += "com.typesafe.akka" %% "akka-stream-testkit" % "2.6.10" % Test,
libraryDependencies += "com.typesafe.akka" %% "akka-http-testkit" % "10.2.1" % Test,
libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.15.0", // Java implementation of language server protocol
libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.20.1", // Java implementation of language server protocol

silicon / excludeFilter := "logback.xml", /* Ignore Silicon's Logback configuration */
carbon / excludeFilter := "logback.xml", /* Ignore Carbon's Logback configuration */
Expand Down
6 changes: 4 additions & 2 deletions src/main/scala/viper/server/core/AstWorker.scala
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ import viper.server.ViperConfig
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

Expand All @@ -26,7 +27,8 @@ case class ServerCrashException(e: Throwable) extends Exception(e)

class AstWorker(val arg_list: List[String],
override val logger: Logger,
private val config: ViperConfig
private val config: ViperConfig,
private val loader: Option[FileLoader]
)(override val executor: VerificationExecutionContext)
extends MessageReportingTask[Option[Program]] {

Expand All @@ -37,7 +39,7 @@ class AstWorker(val arg_list: List[String],
val astGen = new AstGenerator(logger, reporter, arg_list, disablePlugins = config.disablePlugins())

val ast_option: Option[Program] = try {
astGen.generateViperAst(file)
astGen.generateViperAst(file, loader)
} catch {
case _: java.nio.file.NoSuchFileException =>
logger.error(s"The file ($file) for which verification has been requested was not found.")
Expand Down
12 changes: 9 additions & 3 deletions src/main/scala/viper/server/core/ViperCoreServer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ import ch.qos.logback.classic.Logger
import viper.server.ViperConfig
import viper.server.vsi.{AstHandle, AstJobId, VerJobId, VerificationServer}
import viper.silver.ast.Program
import viper.silver.ast.utility.FileLoader
import viper.silver.logger.ViperLogger

import scala.concurrent.duration._
Expand Down Expand Up @@ -58,10 +59,10 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
}
}

def requestAst(arg_list: List[String], localLogger: Option[Logger] = None): AstJobId = {
def requestAst(arg_list: List[String], localLogger: Option[Logger] = None, loader: Option[FileLoader] = None): AstJobId = {
require(config != null)
val logger = combineLoggers(localLogger)
val task_backend = new AstWorker(arg_list, logger, config)(executor)
val task_backend = new AstWorker(arg_list, logger, config, loader)(executor)
val ast_id = initializeAstConstruction(task_backend)

if (ast_id.id >= 0) {
Expand All @@ -72,6 +73,7 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
}
ast_id
}
def discardAstJobOnCompletion(jid: AstJobId, jobActor: ActorRef): Unit = discardAstOnCompletion(jid, jobActor)

def verifyWithAstJob(programId: String, ast_id: AstJobId, backend_config: ViperBackendConfig, localLogger: Option[Logger] = None): VerJobId = {
val logger = combineLoggers(localLogger)
Expand Down Expand Up @@ -123,7 +125,11 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
ver_id
}

override def streamMessages(jid: VerJobId, clientActor: ActorRef): Option[Future[Done]] = {
override def streamMessages(jid: VerJobId, clientActor: ActorRef, full: Boolean): Option[Future[Done]] = {
globalLogger.info(s"Streaming results for job #${jid.id}.")
super.streamMessages(jid, clientActor, full)
}
override def streamMessages(jid: AstJobId, clientActor: ActorRef): Option[Future[Done]] = {
globalLogger.info(s"Streaming results for job #${jid.id}.")
super.streamMessages(jid, clientActor)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ object ViperCoreServerUtils {
import scala.language.postfixOps

val actor = executor.actorSystem.actorOf(SeqActor.props(jid, core.globalLogger))
val complete_future = core.streamMessages(jid, actor).getOrElse(Future.failed(JobNotFoundException))
val complete_future = core.streamMessages(jid, actor, true).getOrElse(Future.failed(JobNotFoundException))
complete_future.flatMap(_ => {
implicit val askTimeout: Timeout = Timeout(core.config.actorCommunicationTimeout() milliseconds)
(actor ? SeqActor.Result).mapTo[Future[List[Message]]].flatten
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -493,6 +493,8 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs
case q: QuantifierInstantiationsMessage => q.toJson
case q: QuantifierChosenTriggersMessage => q.toJson
case v: VerificationTerminationMessage => v.toJson
case p: PProgramReport => p.semanticAnalysisSuccess.toJson
case w: WarningsDuringVerification => w.toJson
}))
})

Expand Down
148 changes: 91 additions & 57 deletions src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
Original file line number Diff line number Diff line change
Expand Up @@ -7,15 +7,16 @@
package viper.server.frontends.lsp

import ch.qos.logback.classic.Logger
import org.eclipse.lsp4j.DocumentSymbol
import org.eclipse.lsp4j.Range
import viper.server.core.VerificationExecutionContext
import viper.server.frontends.lsp.VerificationState.Ready

import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap}
import scala.collection.mutable.ArrayBuffer
import scala.concurrent.Future
import scala.jdk.CollectionConverters._
import scala.jdk.FutureConverters._
import viper.server.frontends.lsp.file.FileManager
import viper.server.frontends.lsp.file.VerificationManager

/** manages per-client state and interacts with the server instance (which is shared among all clients) */
class ClientCoordinator(val server: ViperServerService)(implicit executor: VerificationExecutionContext) {
Expand Down Expand Up @@ -46,59 +47,41 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
!_exited
}

def addFileIfNecessary(uri: String): Unit = {
logger.trace(s"Adding FileManager for $uri if it does not exist yet")
val coordinator = this
val createFMFunc = new java.util.function.Function[String, FileManager]() {
override def apply(t: String): FileManager = {
logger.trace(s"FileManager created for $uri")
new FileManager(coordinator, uri)
}
def closeFile(uri: String): Unit = {
val toRemove = Option(_files.get(uri)).map(fm => {
fm.isOpen = false
fm.removeDiagnostics()
fm.isRoot
}).getOrElse(false)
if (toRemove) {
logger.trace(s"Removing FileManager for $uri")
_files.remove(uri)
}
// we use `computeIfAbsent` instead of `putIfAbsent` such that a new FileManager is only created if it's absent
_files.computeIfAbsent(uri, createFMFunc)
}

def removeFileIfExists(uri: String): Unit = {
logger.trace(s"Removing FileManager for $uri")
_files.remove(uri)
}

/** clears definitions and symbols associated with a file */
def resetFile(uri: String): Unit = {
Option(_files.get(uri))
.foreach(fm => {
fm.symbolInformation = ArrayBuffer.empty
fm.definitions = ArrayBuffer.empty
})
}

def resetDiagnostics(uri: String): Unit = {
Option(_files.get(uri))
.foreach(fm => fm.resetDiagnostics())
getFileManager(uri).removeDiagnostics()
}

def getSymbolsForFile(uri: String): Array[DocumentSymbol]= {
Option(_files.get(uri))
.map(fm => fm.symbolInformation.toArray)
.getOrElse(Array.empty)
}

def getDefinitionsForFile(uri: String): ArrayBuffer[Definition] = {
Option(_files.get(uri))
.map(fm => fm.definitions)
.getOrElse(ArrayBuffer.empty)
def handleChange(uri: String, range: Range, text: String): Unit = {
val fm = getFileManager(uri)
fm.synchronized {
fm.handleContentChange(range, text)
}
}

/** Checks if verification can be started for a given file.
*
* Informs client differently depending on whether or not verification attempt was triggered manually
* */
def canVerificationBeStarted(uri: String, manuallyTriggered: Boolean): Boolean = {
def canVerificationBeStarted(uri: String, content: String, manuallyTriggered: Boolean): Boolean = {
logger.trace("canVerificationBeStarted")
if (server.isRunning) {
logger.trace("server is running")
addFileIfNecessary(uri)
// This should only be necessary if one wants to verify a closed file for some reason
val fm = getFileManager(uri, Some(content))
// This will be the new project root
makeEmptyRoot(fm)
true
} else {
logger.trace("server is not running")
Expand All @@ -111,16 +94,15 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
}

def stopRunningVerification(uri: String): Future[Boolean] = {
Option(_files.get(uri))
.map(fm => fm.stopVerification()
.map(_ => {
logger.trace(s"stopVerification has completed for ${fm.uri}")
val params = StateChangeParams(Ready.id, verificationCompleted = 0, verificationNeeded = 0, uri = uri)
sendStateChangeNotification(params, Some(fm))
true
})
.recover(_ => false))
.getOrElse(Future.successful(false))
val fm = getFileManager(uri)
fm.stop()
.map(_ => {
logger.trace(s"stopVerification has completed for ${fm.file.uri}")
val params = StateChangeParams(Ready.id, verificationCompleted = 0, verificationNeeded = 0, uri = uri)
sendStateChangeNotification(params, Some(fm))
true
})
.recover(_ => false)
}

/** Stops all running verifications.
Expand All @@ -130,18 +112,26 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
* */
def stopAllRunningVerifications(): Future[Unit] = {
val tasks = _files.values().asScala.map(fm =>
fm.stopVerification().map(_ => {
logger.trace(s"stopVerification has completed for ${fm.uri}")
fm.stop().map(_ => {
logger.trace(s"stopVerification has completed for ${fm.file.uri}")
}))
Future.sequence(tasks).map(_ => {
logger.debug("all running verifications have been stopped")
})
}

/** returns true if verification was started */
def startVerification(backendClassName: String, customArgs: String, uri: String, manuallyTriggered: Boolean): Boolean = {
Option(_files.get(uri))
.exists(fm => fm.startVerification(backendClassName, customArgs, manuallyTriggered))
def startVerification(backendClassName: String, customArgs: String, uri: String, manuallyTriggered: Boolean): Future[Boolean] = {
val fm = getFileManager(uri)
fm.startVerification(backendClassName, customArgs, fm.content, manuallyTriggered)
}

/** returns true if parse/typecheck was started */
def startParseTypecheck(uri: String): Boolean = {
val fm = getFileManager(uri)
val project = Option(_files.get(uri)).flatMap(_.projectRoot).getOrElse(uri)
val root = getFileManager(project)
root.runParseTypecheck(fm.content)
}

/** flushes verification cache, optionally only for a particular file */
Expand Down Expand Up @@ -173,9 +163,9 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
*
* If state change is related to a particular file, its manager's state is also updated.
* */
def sendStateChangeNotification(params: StateChangeParams, task: Option[FileManager]): Unit = {
def sendStateChangeNotification(params: StateChangeParams, task: Option[VerificationManager]): Unit = {
// update file manager's state:
task.foreach(fm => fm.state = VerificationState(params.newState))
task.foreach(vm => vm.state = VerificationState(params.newState))
try {
client.notifyStateChanged(params)
} catch {
Expand Down Expand Up @@ -204,4 +194,48 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
if (!isAlive) return
client.notifyHint(HintMessage(message, showSettingsButton, showViperToolsUpdateButton ))
}

private def getFileManager(uri: String, content: Option[String] = None): FileManager = {
var createdNew = false
val coordinator = this
val createFMFunc = new java.util.function.Function[String, FileManager]() {
override def apply(t: String): FileManager = {
logger.trace(s"FileManager created for $uri")
createdNew = true
FileManager(uri, coordinator, content)
}
}
// we use `computeIfAbsent` instead of `putIfAbsent` such that a new FileManager is only created if it's absent
val fm = _files.computeIfAbsent(uri, createFMFunc)
// Override the content if we are given one and the file manager was not just created
if (!createdNew && content.isDefined) fm.content.set(content.get)
fm
}
def ensureFmExists(uri: String, content: String): FileManager = {
getFileManager(uri, Some(content))
}
def getRoot(uri: String): FileManager = {
val fm = getFileManager(uri)
fm.projectRoot.map(getFileManager(_)).getOrElse(fm)
}

///////////////////////
// Project management
///////////////////////

def addToProject(uri: String, root: String, getContents: Boolean): (Option[String], Option[Set[String]]) = {
getFileManager(uri).addToProject(root, getContents)
}
def removeFromProject(uri: String, root: String) = {
Option(_files.get(uri)).map(_.removeFromProject(root))
}
def makeEmptyRoot(fm: FileManager) = {
for (leaves <- fm.projectLeaves; leaf <- leaves) {
removeFromProject(leaf, fm.file_uri)
}
fm.project = Left(Map())
}
def handleChangeInLeaf(root: String, leaf: String, range: Range, text: String): Unit = {
Option(_files.get(root)).map(_.handleChangeInLeaf(leaf, range, text))
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,10 @@ object C2S_Commands {
// final val GetExecutionTrace = "GetExecutionTrace"
final val RemoveDiagnostics = "RemoveDiagnostics"
final val GetViperFileEndings = "GetViperFileEndings"
final val SetupProject = "SetupProject"
final val FlushCache = "FlushCache"
final val GetIdentifier = "GetIdentifier"
final val GetRange = "GetRange"
}

object S2C_Commands {
Expand Down
Loading
Loading