Fix caching for Viper-IDE by reusing the same program ID when verifyi…

…ng (and parsing) the same file (#43)
viperproject · Jul 18, 2021 · dd1fe3f · dd1fe3f
1 parent 3d6d3d2
commit dd1fe3f
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 9 deletions.
diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml
@@ -57,10 +57,9 @@ jobs:
             silicon-ref: "master"
             carbon-ref: "master"
           - name: release
-            # note that v.21.01-release does not work because silver PR #503 is not yet in there
-            silver-ref: "master"
-            silicon-ref: "master"
-            carbon-ref: "master"
+            silver-ref: "21.07-RC"
+            silicon-ref: "21.07-RC"
+            carbon-ref: "21.07-RC"
     steps:
       - name: Checkout ViperServer
         uses: actions/checkout@v2

diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala
@@ -62,12 +62,11 @@ class ViperCoreServer(val config: ViperConfig)(implicit val executor: Verificati
     ast_id
   }
 
-  def verify(ast_id: AstJobId, backend_config: ViperBackendConfig): VerJobId = {
+  def verify(programId: String, ast_id: AstJobId, backend_config: ViperBackendConfig): VerJobId = {
 
     if (!isRunning) throw new IllegalStateException("Instance of VerificationServer already stopped")
     require(backend_config != null)
 
-    val programId = s"ViperAst#${ast_id.id}"
     val args: List[String] = backend_config.toList
 
     ast_jobs.lookupJob(ast_id) match {

diff --git a/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala b/src/main/scala/viper/server/frontends/http/ViperHttpServer.scala
@@ -62,14 +62,15 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex
 
   override def onVerifyPost(vr: Requests.VerificationRequest): ToResponseMarshallable = {
     val arg_list = getArgListFromArgString(vr.arg)
+    val file: String = arg_list.last
+    val arg_list_partial: List[String] = arg_list.dropRight(1)
 
-    if (!validateViperFile(arg_list.last)) {
+    if (!validateViperFile(file)) {
       return VerificationRequestReject("File not found")
     }
 
     val ast_id = requestAst(arg_list)
 
-    val arg_list_partial: List[String] = arg_list.dropRight(1)
     val backend = try {
       ViperBackendConfig(arg_list_partial)
     } catch {
@@ -79,7 +80,7 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex
         return VerificationRequestReject("Invalid arguments for backend.")
     }
 
-    val ver_id = verify(ast_id, backend)
+    val ver_id = verify(file, ast_id, backend)
 
     VerificationRequestAccept(ast_id, ver_id)
   }