Generalization of VSI towards job pipelining + streaming AST construction messages + adaptation to latest changes in Silver

.github/workflows/release.yml

@@ -1,19 +1,28 @@
+name: Release Nightly (Under Construction)
+
 on:
-  push:
-    types: [created]
-name: Handle Push
+  workflow_dispatch:
+
 jobs:
-  generate:
-    name: Create nigtly artifacts
-    runs-on: ubuntu-latest
+  nightly:
+    runs-on: ubuntu-16.04
     steps:
-      - name: Checkout the repository
-        uses: actions/checkout@master
-      - name: Generate the artifacts
-        uses: skx/github-action-build@master
-      - name: Upload the artifacts
-        uses: skx/github-action-publish-binaries@master
+      - name: Get Current Date
+        id: date
+        run: echo "::set-output name=DATE::$(date +'%Y-%m-%d')"
+
+      - name: Generate atrifact
+        run: mkdir -p target/scala-2.13; echo "Hello Viper" > target/scala-2.13/viper.jar
+
+      - name: Publish Nightly Artifact
         env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-        with:
-          args: 'example-*'
+          FILE: target/scala-2.13/viper.jar
+          NIGHTLY_RELEASE_ID: 36021300
+          ARTIFACT_NAME: viper-nightly-${{ steps.date.outputs.DATE }}.jar
+        run: |
+          echo Publishing $FILE as $ARTIFACT_NAME ...;
+          curl -H "Accept: application/vnd.github.v3+json" \
+               -H "Content-Type: $(file -b --mime-type $FILE)" \
+               -H "Authorization: Bearer ${{ secrets.GITHUB_TOKEN }}" \
+               --data-binary @$FILE \
+               "https://uploads.github.com/repos/aterga/viperserver/releases/$NIGHTLY_RELEASE_ID/assets?name=$ARTIFACT_NAME"

.github/workflows/scala.yml

@@ -1,12 +1,12 @@
-name: Scala CI
+name: Check, Build, Test, Publish Nightly
 
 on:
   push:
   pull_request:
 
 jobs:
   check-headers:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-16.04
     steps:
       - name: Checkout ViperServer repo
         uses: actions/checkout@v2
@@ -17,54 +17,88 @@ jobs:
           config: ./.github/license-check/config.json
           strict: true
 
-  build:
-    runs-on: ubuntu-latest
+  test:
+    runs-on: ubuntu-16.04
     steps:
-    - name: Checkout ViperServer
-      uses: actions/checkout@v2
-      with:
-        path: viperServer
-    - name: Checkout Silver
-      uses: actions/checkout@v2
-      with:
-        repository: viperproject/silver
-        path: silver
-    - name: Checkout Silicon
-      uses: actions/checkout@v2
-      with:
-        repository: viperproject/silicon
-        path: silicon
-    - name: Checkout Carbon
-      uses: actions/checkout@v2
-      with:
-        repository: viperproject/carbon
-        path: carbon
-
-    - name: Symbolically link Silver to Carbon
-      run: cd carbon; ln --symbolic ../silver
-    - name: Symbolically link Silver to Silicon
-      run: cd silicon; ln --symbolic ../silver
-    - name: Symbolically link Silver to ViperServer
-      run: cd viperServer; ln --symbolic ../silver
-    - name: Symbolically link Carbon to ViperServer
-      run: cd viperServer; ln --symbolic ../carbon
-    - name: Symbolically link Silicon to ViperServer
-      run: cd viperServer; ln --symbolic ../silicon
-
-    - name: Install Z3
-      run: sudo apt-get update -y; sudo apt-get install -y z3
+      - name: Get Current Date
+        id: date
+        run: echo "::set-output name=DATE::$(date +'%Y-%m-%d')"
+
+      - name: Checkout ViperServer
+        uses: actions/checkout@v2
+        with:
+          path: viperServer
+      - name: Checkout Silver
+        uses: actions/checkout@v2
+        with:
+          repository: viperproject/silver
+          path: silver
+      - name: Checkout Silicon
+        uses: actions/checkout@v2
+        with:
+          repository: viperproject/silicon
+          path: silicon
+      - name: Checkout Carbon
+        uses: actions/checkout@v2
+        with:
+          repository: viperproject/carbon
+          path: carbon
 
-    - name: Set up JDK 1.8
-      uses: actions/setup-java@v1
-      with:
-        java-version: 1.11
+      - name: Symbolically link Silver to Carbon
+        run: cd carbon; ln --symbolic ../silver
+      - name: Symbolically link Silver to Silicon
+        run: cd silicon; ln --symbolic ../silver
+      - name: Symbolically link Silver to ViperServer
+        run: cd viperServer; ln --symbolic ../silver
+      - name: Symbolically link Carbon to ViperServer
+        run: cd viperServer; ln --symbolic ../carbon
+      - name: Symbolically link Silicon to ViperServer
+        run: cd viperServer; ln --symbolic ../silicon
+
+      - name: Install Z3
+        env: 
+          Z3_VERSION: 4.8.9
+          Z3_PLATFORM: x64
+          Z3_OS: ubuntu-16.04
+        run: |
+          export Z3=z3-$Z3_VERSION-$Z3_PLATFORM-$Z3_OS; 
+          curl -J -L https://github.com/Z3Prover/z3/releases/download/z3-$Z3_VERSION/$Z3.zip > z3.zip; 
+          unzip z3.zip; 
+          sudo ln -s $(pwd)/$Z3/bin/z3 /usr/bin/z3
 
-    - name: Install SBT
-      run: echo "deb https://dl.bintray.com/sbt/debian /" | sudo tee -a /etc/apt/sources.list.d/sbt.list; curl -sL "https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x2EE0EA64E40A89B84B2DF73499E82A75642AC823" | sudo apt-key add; sudo apt-get update; sudo apt-get install sbt
+      - name: Set up JDK 15
+        uses: actions/setup-java@v1
+        with:
+          java-version: '15.0.1'
+          architecture: x64
+
+      - name: Install SBT
+        run: |
+          echo "deb https://dl.bintray.com/sbt/debian /" | sudo tee -a /etc/apt/sources.list.d/sbt.list; 
+          curl -sL "https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x2EE0EA64E40A89B84B2DF73499E82A75642AC823" | sudo apt-key add; 
+          sudo apt-get update; sudo apt-get install sbt
+
+      - name: test project
+        run: |
+          cd viperServer; 
+          export Z3_EXE="/usr/bin/z3"; 
+          env > print_dir.txt; 
+          sbt test
 
-    - name: Assemble project
-      run: cd viperServer; sbt assembly
-
-    - name: test project
-      run: cd viperServer; export Z3_EXE="/usr/bin/z3"; env > print_dir.txt; sbt test
+      - name: Assemble the fat JAR file
+        run: |
+          cd viperServer; 
+          sbt assembly
 
+      - name: Publish Nightly Artifact
+        env:
+          FILE: viperServer/target/scala-2.13/viper.jar
+          NIGHTLY_RELEASE_ID: 36021300
+          ARTIFACT_NAME: viper-nightly-${{ steps.date.outputs.DATE }}.jar
+        run: |
+          echo Publishing $FILE as $ARTIFACT_NAME ...;
+          curl -H "Accept: application/vnd.github.v3+json" \
+               -H "Content-Type: $(file -b --mime-type $FILE)" \
+               -H "Authorization: Bearer ${{ secrets.GITHUB_TOKEN }}" \
+               --data-binary @$FILE \
+               "https://uploads.github.com/repos/${{ github.repository }}/releases/$NIGHTLY_RELEASE_ID/assets?name=$ARTIFACT_NAME"

README.md

@@ -4,7 +4,7 @@
 
 This is ViperServer, an HTTP server that manages verification requests to different tools from the Viper tool stack.
 
-The main two tools currently are:
+The main two Viper tools (a.k.a verification backends) currently are: 
 
 - [Carbon](https://bitbucket.org/viperproject/carbon), a verification condition generation (VCG) backend for the Viper language.
 - [Silicon](https://bitbucket.org/viperproject/silicon), a symbolic execution verification backend.
@@ -14,13 +14,16 @@ The main two tools currently are:
 
 1. Viper IDE: integration of Viper into Visual Studio Code (VS Code). Viper IDE provides the best user experience for Viper.
    More details here: http://viper.ethz.ch/downloads/
-2. Avoid 1-3 second delays caused by JVM startup time. ViperServer offers a robust alternative to, e.g.,
+1. Facilitate the development of verification IDEs for Viper frontends, such as: 
+    - [Gobra](https://github.com/viperproject/gobra), the Viper-based verifier for the Go language
+    - [Prusti](https://github.com/viperproject/prusti-dev/), the Viper-based verifier for the Rust language
+1. Avoid 1-3 second delays caused by JVM startup time. ViperServer offers a robust alternative to, e.g.,
    [Nailgun](https://github.com/facebook/nailgun).
-3. Develop Viper encodings more efficiently with caching.
-4. Interact with Viper tools programmatically using the HTTP API. A reference client implementation (in Python) is
+1. Develop Viper encodings more efficiently with caching.
+1. Interact with Viper tools programmatically using the HTTP API. A reference client implementation (in Python) is
    available via [viper_client](https://bitbucket.org/viperproject/viper_client).
 
-For more details, please visit: http://viper.ethz.ch/downloads/
+For more details about using Viper, please visit: http://viper.ethz.ch/downloads/
 
 
 ### Installation Instructions ###

build.sbt

@@ -9,11 +9,15 @@ lazy val silver = project in file("silver")
 lazy val silicon = project in file("silicon")
 lazy val carbon = project in file("carbon")
 
+lazy val common = (project in file("common"))
+
 // Viper Server specific project settings
 lazy val server = (project in file("."))
     .dependsOn(silver % "compile->compile;test->test")
     .dependsOn(silicon % "compile->compile;test->test")
     .dependsOn(carbon % "compile->compile;test->test")
+    .dependsOn(common)
+    .aggregate(common)
     .enablePlugins(JavaAppPackaging)
     .settings(
         // General settings
@@ -26,16 +30,17 @@ lazy val server = (project in file("."))
         Test / fork := true,
 
         // Compilation settings
-        libraryDependencies += "com.typesafe.akka" %% "akka-actor" % "2.6.10",
-        libraryDependencies += "com.typesafe.akka" %% "akka-http-spray-json" % "10.2.1",
-        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 += "com.typesafe.akka" %% "akka-actor" % "2.5.23",
+        libraryDependencies += "com.typesafe.akka" %% "akka-http-spray-json" % "10.1.8",
+        libraryDependencies += "com.typesafe.akka" %% "akka-stream" % "2.5.23",
+        libraryDependencies += "com.typesafe.akka" %% "akka-stream-testkit" % "2.5.23" % Test,
+        libraryDependencies += "com.typesafe.akka" %% "akka-http-testkit" % "10.1.8" % Test,
+        libraryDependencies += "org.eclipse.lsp4j" % "org.eclipse.lsp4j" % "0.8.1", // Java implementation of language server protocol
 
         // Run settings
         run / javaOptions += "-Xss128m",
 
-        // Test settings.
+        // Test settings
         Test / parallelExecution := false,
 
         // Assembly settings

project/plugins.sbt

@@ -2,5 +2,5 @@
 // http://creativecommons.org/publicdomain/zero/1.0/
 
 addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "0.15.0")
+addSbtPlugin("com.typesafe.sbt" % "sbt-native-packager" % "1.3.12")
 addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.10.0")
-addSbtPlugin("com.typesafe.sbt" % "sbt-native-packager" % "1.7.6")

src/main/scala/viper/server/LanguageServerRunner.scala

@@ -0,0 +1,49 @@
+// 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)
+    _config.verify()
+    val port = _config.port()
+    runServer(port)
+  }
+
+  def runServer(port: Int): Unit = {
+    // start listening on port
+    try {
+      val socket = new Socket("localhost", port)
+      val localAddress = socket.getLocalAddress.getHostAddress
+      println(s"going to listen on $localAddress:$port")
+
+      Coordinator.port = port
+      Coordinator.url = localAddress
+
+      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}")
+    }
+  }
+}
+

src/main/scala/viper/server/ViperConfig.scala

@@ -9,6 +9,7 @@ package viper.server
 import java.io.File
 
 import org.rogach.scallop.{ScallopConf, ScallopOption, singleArgConverter}
+import viper.server.utility.Helpers.{canonizedFile, validatePath}
 import viper.server.utility.ibm
 import viper.server.utility.ibm.Socket
 
@@ -31,24 +32,12 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
       val temp: File = java.io.File.createTempFile("viperserver_journal_" + System.currentTimeMillis(), ".log")
       Some(temp.getAbsolutePath)
     },
-    validate = (path: String) => {
-      val f = canonizedLogFile(path)
-      (f.isFile || f.isDirectory) && f.canWrite || f.getParentFile.canWrite
-    },
+    validate = validatePath,
     noshort = true,
     hidden = false)
 
-  private def canonizedLogFile(some_file_path: String): File = {
-    val f = new File(some_file_path)
-    if (f.isAbsolute) {
-      f
-    } else {
-      java.nio.file.Paths.get(System.getProperty("user.dir"), some_file_path).toFile
-    }
-  }
-
   def getLogFileWithGuarantee: String = {
-    val cf: File = canonizedLogFile(logFile())
+    val cf: File = canonizedFile(logFile())
     if ( cf.isDirectory ) {
       val log: File = java.io.File.createTempFile("viperserver_journal_" + System.currentTimeMillis(), ".log", cf)
       log.toString
@@ -68,7 +57,11 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
     descr = ("Specifies the port on which ViperServer will be started."
       + s"The port must be an integer in range [${Socket.MIN_PORT_NUMBER}-${ibm.Socket.MAX_PORT_NUMBER}]"
       + "If the option is omitted, an available port will be selected automatically."),
-    default = Some(ibm.Socket.findFreePort),
+    default = {
+      val p = ibm.Socket.findFreePort
+      println(s"Automatically selecting port $p ...")
+      Some(p)
+    },
     validate = p => try {
       ibm.Socket.available(p)
     } catch {