Write Cache to file

build.sbt

@@ -29,7 +29,7 @@ lazy val server = (project in file("."))
         // classpath used by Scala's reflection.
         Test / fork := true,
 
-        // Compilation settings
+        libraryDependencies += "net.liftweb" %% "lift-json" % "3.5.0",
         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",

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

@@ -102,6 +102,15 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
     hidden = false
   )
 
+  val cacheFile: ScallopOption[String] = opt[String]("cacheFile",
+    descr = ("Specifies the file in which the resulting cache of a verification run gets written to."
+      + "If it is not set, the cache is only kept in memory and not written to the file system."
+      ),
+    default = None,
+    noshort = true,
+    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" +

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

@@ -143,7 +143,7 @@ class ViperBackend(private val _frontend: SilFrontend, private val programId: St
         _frontend.logger.debug(s"Verification has failed (errors: ${f.errors.map(_.readableMessage).mkString("\n")}; members: ${_ast.members.map(_.name).mkString(", ")})")
         _frontend.reporter report OverallFailureMessage(_frontend.getVerifierName,
                                                         System.currentTimeMillis() - _frontend.startTime,
-                                                        Failure(f.errors.filter { e => !e.cached }))
+                                                        Failure(f.errors))
       case None =>
     }
   }
@@ -181,8 +181,6 @@ class ViperBackend(private val _frontend: SilFrontend, private val programId: St
     _frontend.setVerificationResult(ver_result)
     _frontend.setState(DefaultStates.Verification)
 
-    _frontend.logger.debug(s"Latest verification result: $ver_result")
-
     val meth_to_err_map: Seq[(Method, Option[List[AbstractVerificationError]])] = methodsToVerify.map((m: Method) => {
       // Results come back irrespective of program Member.
       val cacheable_errors: Option[List[AbstractVerificationError]] = for {
@@ -228,9 +226,12 @@ class ViperBackend(private val _frontend: SilFrontend, private val programId: St
         }
       }
     } else {
-      _frontend.logger.debug(s"Inconsistent error splitting; no cache update for this verification attempt with ProgramID $programId.")
+      _frontend.logger.warn(s"Inconsistent error splitting; no cache update for this verification attempt with ProgramID $programId.")
     }
 
+    // Write cache to file at the end of a verification run
+    ViperCache.writeToFile()
+
     // combine errors:
     if (all_cached_errors.nonEmpty) {
       _frontend.getVerificationResult.get match {

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

@@ -39,7 +39,7 @@ class ViperCoreServer(val config: ViperConfig)(implicit val executor: Verificati
     println(s"Writing [level:${config.logLevel()}] logs into " +
       s"${if (!config.logFile.isSupplied) "(default) " else ""}journal: ${logger.file.get}")
 
-    ViperCache.initialize(logger.get, config.backendSpecificCache())
+    ViperCache.initialize(logger.get, config.backendSpecificCache(), config.cacheFile.toOption)
 
     super.start(config.maximumActiveJobs()) map { _ =>
       logger.get.info(s"ViperCoreServer has started.")

src/main/scala/viper/server/frontends/http/ViperHttpServer.scala

@@ -22,7 +22,7 @@ import viper.server.frontends.http.jsonWriters.ViperIDEProtocol.{AlloyGeneration
 import viper.server.utility.Helpers.{getArgListFromArgString, validateViperFile}
 import viper.server.vsi.Requests.CacheResetRequest
 import viper.server.vsi._
-import viper.silver.logger.ViperLogger
+import viper.silver.logger.{ViperLogger, ViperStdOutLogger}
 import viper.silver.reporter.Message
 
 import scala.concurrent.Future
@@ -35,7 +35,7 @@ class ViperHttpServer(config: ViperConfig)(executor: VerificationExecutionContex
     _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}")
 
-    ViperCache.initialize(logger.get, config.backendSpecificCache())
+    ViperCache.initialize(logger.get, config.backendSpecificCache(), config.cacheFile.toOption)
 
     port = config.port.toOption.getOrElse(0) // 0 causes HTTP server to automatically select a free port
     super.start(config.maximumActiveJobs()).map({ _ =>

src/main/scala/viper/server/vsi/Cache.scala

@@ -8,7 +8,9 @@ package viper.server.vsi
 
 import viper.silver.utility.CacheHelper
 
-import scala.collection.mutable.{ListBuffer, Map => MutableMap}
+import java.security.MessageDigest
+import java.time.Instant
+import scala.collection.mutable.ListBuffer
 
 /** The goal of this generic caching trait is to provide:
   *
@@ -46,10 +48,11 @@ abstract class Cache {
     * The inner map is referred to as the fileCache. As the name indicates, it stores, for each
     * file, a number of hashes and corresponding cache entries.
     */
-  protected val _cache: MutableMap[String, FileCash] = MutableMap()
-  type FileCash = MutableMap[String, List[CacheEntry]]
+  protected var _cache: Cache = Map()
+  type Cache = Map[String, FileCache]
 
-  protected val _program_cache: MutableMap[Ast, MutableMap[CacheableMember, List[Member]]] = MutableMap()
+  type FileCache = Map[String, List[CacheEntry]]
+  protected var _program_cache: Map[String, Map[String, String]] = Map()
 
   /** This method transforms a program and returns verification results based on the cache's
     * current state.
@@ -72,40 +75,40 @@ abstract class Cache {
     //read errors from cache
     val cachable_members = input_prog.decompose()
 
-    val prog_dependencies = _program_cache.find({
-      case (k, _) => k.equals(input_prog)
-    })
+    val input_prog_hex = MessageDigest.getInstance("SHA-1")
+      .digest(input_prog.toString.getBytes("UTF-8"))
+      .map("%02x".format(_)).mkString
 
-    prog_dependencies match {
-      case Some((_, dep_map)) =>
-        cachable_members.foreach(cm => {
-          val dependencies = dep_map(cm)
-          get(file_key, cm, dependencies) match {
-            case Some(matched_entry) =>
-              concerningsToCache += cm.transform
-              cache_entries += matched_entry
-            case None =>
-              //Nothing in cache, request verification
-              concerningsToVerify += cm
-          }
-        })
+    val prog_dependencies = _program_cache.get(input_prog_hex)
+
+    val dep_map = prog_dependencies match {
+      case Some(dep_map) => dep_map
       case None =>
-        val dep_map = MutableMap[CacheableMember, List[Member]]()
+        var dep_map = Map[String, String]()
         cachable_members.foreach(cm => {
-          val dependencies = cm.getDependencies(input_prog)
-          dep_map += (cm -> dependencies)
-          get(file_key, cm, dependencies) match {
-            case Some(matched_entry) =>
-              concerningsToCache += cm.transform
-              cache_entries += matched_entry
-            case None =>
-              //Nothing in cache, request verification
-              concerningsToVerify += cm
-          }
+          val concerning_hash = cm.hash()
+          val dependency_hash = CacheHelper.buildHash(concerning_hash + cm.getDependencies(input_prog).map(_.hash()).mkString(" "))
+          dep_map = dep_map + (concerning_hash -> dependency_hash)
         })
-        _program_cache += (input_prog -> dep_map)
+        _program_cache = _program_cache + (input_prog_hex -> dep_map)
+        dep_map
     }
 
+    cachable_members.foreach(cm => {
+      val concerning_hash = cm.hash()
+      val dependency_hash = dep_map(concerning_hash)
+
+      get(file_key, concerning_hash, dependency_hash) match {
+        case Some(matched_entry) =>
+          matched_entry.lastAccessed = Instant.now()
+          concerningsToCache += cm.transform
+          cache_entries += matched_entry
+        case None =>
+          //Nothing in cache, request verification
+          concerningsToCache += cm
+      }
+    })
+
     val all_concernings: List[CacheableMember] = concerningsToCache.toList ++ concerningsToVerify.toList
     val output_prog: Ast = input_prog.compose(all_concernings)
     (output_prog, cache_entries.toList)
@@ -114,18 +117,13 @@ abstract class Cache {
   /** Utility function to retrieve entries for single members.
     * */
   final def get(file_key: String,
-                key: CacheableMember,
-                dependencies: List[Member]): Option[CacheEntry] = {
-
-    val concerning_hash = key.hash()
-    val dependencies_hash = dependencies.map(_.hash()).mkString(" ")
-    val dependency_hash = CacheHelper.buildHash(concerning_hash + dependencies_hash)
+                concerning_hash: String,
+                dependency_hash: String): Option[CacheEntry] = {
     assert(concerning_hash != null)
-
     for {
       fileCache <- _cache.get(file_key)
       cacheEntries <- fileCache.get(concerning_hash)
-      validEntry <- cacheEntries.find(_.depency_hash == dependency_hash)
+      validEntry <- cacheEntries.find(_.dependencyHash == dependency_hash)
     } yield validEntry
   }
 
@@ -147,7 +145,7 @@ abstract class Cache {
     val concerning_hash = key.hash()
     val dependencies_hash = dependencies.map(_.hash()).mkString(" ")
     val dependency_hash = CacheHelper.buildHash(concerning_hash + dependencies_hash)
-    val new_entry: CacheEntry = new CacheEntry(key, content, dependency_hash)
+    val new_entry: CacheEntry = CacheEntry(key.hash(), content, dependency_hash)
 
     assert(concerning_hash != null)
 
@@ -156,28 +154,32 @@ abstract class Cache {
         val existing_entries = fileCache.getOrElse(concerning_hash, Nil)
         val updated_cacheEntries = new_entry :: existing_entries
 
-        fileCache(concerning_hash) = updated_cacheEntries
+        val updatedFileCache = fileCache + (concerning_hash -> updated_cacheEntries)
+        _cache = _cache + (file_key -> updatedFileCache)
         updated_cacheEntries
       case None =>
         //if file not in cache yet, create new map entry for it. Recall the function.
-        _cache += (file_key -> collection.mutable.Map[String, List[CacheEntry]]())
+        _cache = _cache + (file_key -> Map())
         update(file_key, key, dependencies, content)
     }
   }
 
   /** Resets the cache for a particular file.
     * */
   def forgetFile(file_key: String): Option[String] = {
-    _cache.remove(file_key) match {
+    val elem = _cache.get(file_key) match {
       case Some(_) => Some(file_key)
       case None => None
     }
+    _cache -= file_key
+    elem
   }
 
   /** Resets the entire cache.
     * */
   def resetCache(): Unit = {
-    _cache.clear()
+    _program_cache = Map()
+    _cache = Map()
   }
 }
 
@@ -194,7 +196,7 @@ abstract class Cache {
   *  created. If, at some point, a members dependency hash is no longer equal to the one stored
   *  here, the entry is no longer valid.
   * */
-case class CacheEntry(concerning: CacheableMember, content: CacheContent, depency_hash: String)
+case class CacheEntry(concerningHash: String, content: CacheContent, dependencyHash: String, created: Instant = Instant.now(), var lastAccessed: Instant = Instant.now())
 
 
 // ===== AUXILIARY TRAITS ==================================================================
@@ -245,7 +247,7 @@ trait CacheableMember extends Member {
     * terms of verification.
     *
     * A member may hit the cache, but the attached verification results might be invalid. Reason
-    * for this is that other members in the program have might have changed in such a way that
+    * for this is that other members in the program might have changed in such a way that
     * they influenced this member's verification outcome. These influencing members are called
     * dependencies and need to be checked when retrieving a member's attached result from cache.
     * */