From 12ec4ec806fccff55cb24d1a441bc6db739fc363 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Thu, 20 May 2021 11:31:43 +0200 Subject: [PATCH] unifies HTTP and LSP frontend of ViperServer and makes it configurable via CLI args --- .../viper/server/LanguageServerRunner.scala | 50 ------------ src/main/scala/viper/server/ViperConfig.scala | 42 +++++++++- .../viper/server/ViperServerRunner.scala | 79 +++++++++++++++++-- .../core/VerificationExecutionContext.scala | 10 ++- .../viper/server/core/ViperCoreServer.scala | 7 +- .../frontends/http/ViperHttpServer.scala | 7 +- .../viper/server/frontends/lsp/Receiver.scala | 9 ++- .../frontends/lsp/ViperServerService.scala | 5 +- 8 files changed, 129 insertions(+), 80 deletions(-) delete mode 100644 src/main/scala/viper/server/LanguageServerRunner.scala diff --git a/src/main/scala/viper/server/LanguageServerRunner.scala b/src/main/scala/viper/server/LanguageServerRunner.scala deleted file mode 100644 index e7d5dbaf..00000000 --- a/src/main/scala/viper/server/LanguageServerRunner.scala +++ /dev/null @@ -1,50 +0,0 @@ -// This Source Code Form is subject to the terms of the Mozilla Public -// License, v. 2.0. If a copy of the MPL was not distributed with this -// file, You can obtain one at http://mozilla.org/MPL/2.0/. -// -// Copyright (c) 2011-2020 ETH Zurich. - -import java.io.IOException -import java.net.Socket - -import org.eclipse.lsp4j.jsonrpc.Launcher -import viper.server.ViperConfig -import viper.server.frontends.lsp.{Coordinator, CustomReceiver, IdeLanguageClient} - - -object LanguageServerRunner { - - private var _config: ViperConfig = _ - - def main(args: Array[String]): Unit = { - _config = new ViperConfig(args.toSeq) - _config.verify() - val port = _config.port.getOrElse(0) - runServer(port) - } - - def runServer(port: Int): Unit = { - // start listening on port - try { - val socket = new Socket("localhost", port) - val localAddress = socket.getLocalAddress.getHostAddress - - Coordinator.port = socket.getPort - Coordinator.url = localAddress - - println(s"preparing to listen on ${Coordinator.url}:${Coordinator.port}") - - val server: CustomReceiver = new CustomReceiver() - val launcher = Launcher.createLauncher(server, classOf[IdeLanguageClient], socket.getInputStream, socket.getOutputStream) - server.connect(launcher.getRemoteProxy) - - // start listening on input stream in a new thread: - val fut = launcher.startListening() - // wait until stream is closed again - fut.get() - } catch { - case e: IOException => println(s"IOException occurred: ${e.toString}") - } - } -} - diff --git a/src/main/scala/viper/server/ViperConfig.scala b/src/main/scala/viper/server/ViperConfig.scala index 6271fdcb..afa5a6e4 100644 --- a/src/main/scala/viper/server/ViperConfig.scala +++ b/src/main/scala/viper/server/ViperConfig.scala @@ -8,7 +8,8 @@ package viper.server import java.io.File -import org.rogach.scallop.{ScallopConf, ScallopOption, singleArgConverter} +import org.rogach.scallop.{ScallopConf, ScallopOption, numberHandler, singleArgConverter} +import viper.server.core.DefaultVerificationExecutionContext import viper.server.utility.Helpers.{canonizedFile, validatePath} import viper.server.utility.ibm @@ -52,6 +53,18 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) { hidden = false ) + val SERVER_MODE_LSP = "LSP" + val SERVER_MODE_HTTP = "HTTP" + private val server_modes = Array(SERVER_MODE_LSP, SERVER_MODE_HTTP) + + val serverMode: ScallopOption[String] = opt[String]("serverMode", + descr = s"One of the supported protocols: ${server_modes.mkString(",")}.", + default = Some(SERVER_MODE_HTTP), + validate = (ll: String) => server_modes.contains(ll.toUpperCase), + noshort = true, + hidden = false + )(singleArgConverter(level => level.toUpperCase)) + val port: ScallopOption[Int] = opt[Int]("port", 'p', descr = ("Specifies the port on which ViperServer will be started." + s"The port must be an integer in range [${ibm.Socket.MIN_PORT_NUMBER}-${ibm.Socket.MAX_PORT_NUMBER}]" @@ -83,4 +96,29 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) { noshort = false, hidden = false ) -} \ No newline at end of file + + val nThreads: ScallopOption[Int] = opt[Int]( + name = "nThreads", + descr = s"Maximal number of threads that should be used (not taking threads used by backend into account)\n" + + s"Values below ${DefaultVerificationExecutionContext.minNumberOfThreads} (the minimum) will be set to the minimum.\n" + + s"The default value is the maximum of ${DefaultVerificationExecutionContext.minNumberOfThreads} and the number of available processors", + default = Some(Math.max(DefaultVerificationExecutionContext.minNumberOfThreads, Runtime.getRuntime.availableProcessors())), + noshort = true + )(singleArgConverter(input => { + // parse option as int and check bounds + val n = input.toInt + n match { + case n if n < DefaultVerificationExecutionContext.minNumberOfThreads => DefaultVerificationExecutionContext.minNumberOfThreads + case n => n + } + }, numberHandler("Int"))) + + /** + * Exception handling + */ + /** + * Epilogue + */ + + verify() +} diff --git a/src/main/scala/viper/server/ViperServerRunner.scala b/src/main/scala/viper/server/ViperServerRunner.scala index a8036928..4e6e1d7f 100644 --- a/src/main/scala/viper/server/ViperServerRunner.scala +++ b/src/main/scala/viper/server/ViperServerRunner.scala @@ -6,22 +6,85 @@ package viper.server -import viper.server.core.DefaultVerificationExecutionContext +import java.io.IOException +import java.net.{ServerSocket, Socket} + +import org.eclipse.lsp4j.jsonrpc.Launcher +import org.eclipse.lsp4j.jsonrpc.Launcher.Builder +import viper.server.core.{DefaultVerificationExecutionContext, VerificationExecutionContext} import viper.server.frontends.http.ViperHttpServer +import viper.server.frontends.lsp.{Coordinator, CustomReceiver, IdeLanguageClient} object ViperServerRunner { var viperServerHttp: ViperHttpServer = _ - /** Start VCS in HTTP mode. - * */ - def startHttpServer(args: Array[String]): Unit = { - val executor = new DefaultVerificationExecutionContext() - viperServerHttp = new ViperHttpServer(args)(executor) + def main(args: Array[String]): Unit = { + val config = new ViperConfig(args) + val executor = new DefaultVerificationExecutionContext(threadPoolSize = Some(config.nThreads())) + if (config.serverMode() == config.SERVER_MODE_LSP) { + runLspServer(config)(executor) + } else if (config.serverMode() == config.SERVER_MODE_HTTP) { + startHttpServer(config)(executor) + } else { + throw new RuntimeException(s"unknown server mode ${config.serverMode()}") + } + } + + /** + * Start VCS in HTTP mode. + */ + def startHttpServer(config: ViperConfig)(executor: VerificationExecutionContext): Unit = { + viperServerHttp = new ViperHttpServer(config)(executor) viperServerHttp.start() } - def main(args: Array[String]): Unit = { - startHttpServer(args) + /** + * Start VCS in LSP mode. + */ + private def runLspServer(config: ViperConfig)(executor: VerificationExecutionContext): Unit = { + try { + val serverSocket = new ServerSocket(config.port()) + announcePort(serverSocket.getLocalPort) + println(s"going to listen on port ${serverSocket.getLocalPort} for LSP") + + Coordinator.port = serverSocket.getLocalPort + Coordinator.url = serverSocket.getInetAddress.getHostAddress + + val socket = serverSocket.accept() + println(s"client got connected") + // TODO add support for multiple clients connecting to this server + + val server: CustomReceiver = new CustomReceiver()(executor) + val launcher = createLauncher(server, socket)(executor) + server.connect(launcher.getRemoteProxy) + // start listening on input stream in a new thread: + val future = launcher.startListening() + // wait until stream is closed again + future.get() + println("listener thread from server has stopped") + executor.terminate() + println("executor service has been shut down") + } catch { + case e: IOException => println(s"IOException occurred: ${e.toString}") + } } + + private def announcePort(port: Int): Unit = { + // write port number in a predefined format to standard output such that clients can parse it + // do not change this format without adapting clients such as the Viper-IDE client + // regex for parsing: "" + println(s"") + } + + private def createLauncher(server: CustomReceiver, socket: Socket)(executor: VerificationExecutionContext): Launcher[IdeLanguageClient] = + // Launcher.createLauncher cannot be called as we want to pass in an executor service + // Hence, we directly use Launcher.Builder: + new Builder[IdeLanguageClient]() + .setLocalService(server) + .setRemoteInterface(classOf[IdeLanguageClient]) + .setInput(socket.getInputStream) + .setOutput(socket.getOutputStream) + .setExecutorService(executor.executorService) + .create() } diff --git a/src/main/scala/viper/server/core/VerificationExecutionContext.scala b/src/main/scala/viper/server/core/VerificationExecutionContext.scala index dac2c462..000b2774 100644 --- a/src/main/scala/viper/server/core/VerificationExecutionContext.scala +++ b/src/main/scala/viper/server/core/VerificationExecutionContext.scala @@ -15,6 +15,7 @@ import scala.concurrent.duration.FiniteDuration import scala.concurrent.{Await, ExecutionContext, ExecutionContextExecutorService, Future} trait VerificationExecutionContext extends ExecutionContext { + def executorService: ExecutorService def actorSystem: ActorSystem def submit(r: Runnable): java_concurrent.Future[_] /** terminate executor and actor system */ @@ -42,10 +43,13 @@ object DefaultVerificationExecutionContext { * use the provided verification execution context whenever an actor or any task requiring a separate thread is * executed. */ -class DefaultVerificationExecutionContext(actorSystemName: String = "Actor_System", threadNamePrefix: String = "thread") extends VerificationExecutionContext { - protected lazy val nThreads: Int = Math.max(DefaultVerificationExecutionContext.minNumberOfThreads, Runtime.getRuntime.availableProcessors()) +class DefaultVerificationExecutionContext(actorSystemName: String = "Actor_System", + threadNamePrefix: String = "thread", + threadPoolSize: Option[Int] = None) extends VerificationExecutionContext { + protected lazy val nThreads: Int = threadPoolSize.getOrElse( + Math.max(DefaultVerificationExecutionContext.minNumberOfThreads, Runtime.getRuntime.availableProcessors())) protected lazy val threadStackSize: Long = 128L * 1024L * 1024L // 128M seems to consistently be recommended by Silicon and Carbon - protected lazy val executorService: ExecutorService = Executors.newFixedThreadPool( + override def executorService: ExecutorService = Executors.newFixedThreadPool( nThreads, new ThreadFactory { import java.util.concurrent.atomic.AtomicInteger diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala index ff4711ea..a8556996 100644 --- a/src/main/scala/viper/server/core/ViperCoreServer.scala +++ b/src/main/scala/viper/server/core/ViperCoreServer.scala @@ -18,13 +18,11 @@ import scala.concurrent.duration._ import scala.concurrent.Future import scala.language.postfixOps -class ViperCoreServer(val _args: Array[String])(implicit val executor: VerificationExecutionContext) extends VerificationServer with ViperPost { +class ViperCoreServer(val config: ViperConfig)(implicit val executor: VerificationExecutionContext) extends VerificationServer with ViperPost { override type AST = Program // --- VCS : Configuration --- - protected var _config: ViperConfig = _ - final def config: ViperConfig = _config override lazy val askTimeout: Timeout = Timeout(config.actorCommunicationTimeout() milliseconds) @@ -37,9 +35,6 @@ class ViperCoreServer(val _args: Array[String])(implicit val executor: Verificat * will result in an IllegalStateException. * */ def start(): Unit = { - _config = new ViperConfig(_args.toIndexedSeq) - config.verify() - _logger = ViperLogger("ViperServerLogger", config.getLogFileWithGuarantee, config.logLevel()) println(s"Writing [level:${config.logLevel()}] logs into " + s"${if (!config.logFile.isSupplied) "(default) " else ""}journal: ${logger.file.get}") diff --git a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala index a79bdf1c..fcd220d7 100644 --- a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala +++ b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala @@ -28,13 +28,10 @@ import viper.silver.reporter.Message import scala.util.{Failure, Success, Try} -class ViperHttpServer(_args: Array[String])(executor: VerificationExecutionContext) - extends ViperCoreServer(_args)(executor) with VerificationServerHttp { +class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContext) + extends ViperCoreServer(config)(executor) with VerificationServerHttp { override def start(): Unit = { - _config = new ViperConfig(_args.toIndexedSeq) - config.verify() - _logger = ViperLogger("ViperServerLogger", config.getLogFileWithGuarantee, config.logLevel()) println(s"Writing [level:${config.logLevel()}] logs into ${if (!config.logFile.isSupplied) "(default) " else ""}journal: ${logger.file.get}") diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala index f512b77f..e607e148 100644 --- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala +++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala @@ -11,7 +11,8 @@ import java.util.concurrent.{CompletableFuture => CFuture} import org.eclipse.lsp4j.jsonrpc.services.{JsonNotification, JsonRequest} import org.eclipse.lsp4j.services.{LanguageClient, LanguageClientAware} import org.eclipse.lsp4j.{DidChangeConfigurationParams, DidChangeTextDocumentParams, DidCloseTextDocumentParams, DidOpenTextDocumentParams, DocumentSymbolParams, InitializeParams, InitializeResult, InitializedParams, Location, Range, ServerCapabilities, SymbolInformation, TextDocumentPositionParams, TextDocumentSyncKind} -import viper.server.core.DefaultVerificationExecutionContext +import viper.server.ViperConfig +import viper.server.core.VerificationExecutionContext import viper.server.frontends.lsp.LogLevel._ import viper.server.frontends.lsp.VerificationState._ @@ -151,7 +152,7 @@ abstract class StandardReceiver extends LanguageClientAware { } } -class CustomReceiver extends StandardReceiver { +class CustomReceiver()(executor: VerificationExecutionContext) extends StandardReceiver { @JsonNotification(S2C_Commands.FileClosed) def onFileClosed(uri: String): Unit = { @@ -186,8 +187,8 @@ class CustomReceiver extends StandardReceiver { } else { throw new Throwable("Unexpected Backend") } - val executor = new DefaultVerificationExecutionContext() - Coordinator.verifier = new ViperServerService(Array())(executor) + val config = new ViperConfig(Seq()) + Coordinator.verifier = new ViperServerService(config)(executor) Coordinator.verifier.setReady(Coordinator.backend) } catch { case e: Throwable => Log.debug("Error handling swap backend request: " + e) diff --git a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala index 2690ddb1..1d689a57 100644 --- a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala +++ b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala @@ -12,6 +12,7 @@ import java.util.concurrent.{CompletableFuture => CFuture} import akka.actor.{PoisonPill, Props} import akka.pattern.ask import akka.util.Timeout +import viper.server.ViperConfig import viper.server.core.{VerificationExecutionContext, ViperBackendConfig, ViperCache, ViperCoreServer} import viper.server.frontends.lsp.VerificationState.Stopped import viper.server.utility.AstGenerator @@ -24,8 +25,8 @@ import scala.compat.java8.FutureConverters._ import scala.concurrent.Future import scala.concurrent.duration._ -class ViperServerService(args: Array[String])(override implicit val executor: VerificationExecutionContext) - extends ViperCoreServer(args)(executor) with VerificationServer { +class ViperServerService(config: ViperConfig)(override implicit val executor: VerificationExecutionContext) + extends ViperCoreServer(config)(executor) with VerificationServer { protected var timeout: Int = _