Merge pull request #201 from viperproject/sem-highlight

Add more LSP features

Author: marcoeilers

.gitignore

@@ -8,3 +8,6 @@ ter.bat
 ver.bat
 .bsp/
 logs/
+.bloop
+.metals
+metals.sbt

build.sbt

@@ -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.
@@ -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 */

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

@@ -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
 
@@ -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]] {
 
@@ -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.")

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

@@ -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._
@@ -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) {
@@ -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)
@@ -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)
   }

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

@@ -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

src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala

@@ -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
       }))
   })
 

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

@@ -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) {
@@ -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")
@@ -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.
@@ -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 */
@@ -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 {
@@ -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))
+  }
 }

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

@@ -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 {