unifies HTTP and LSP frontend of ViperServer and makes it configurabl…

…e via CLI args

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
   )
-}
+
+  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()
+}

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: "<ViperServerPort:(\d+)>"
+    println(s"<ViperServerPort:$port>")
+  }
+
+  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()
 }

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

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

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

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)

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 = _