Move to a cache using hashes as keys

core/src/main/scala/stainless/MainHelpers.scala

@@ -75,6 +75,7 @@ trait MainHelpers extends inox.MainHelpers { self =>
     frontend.optExtraDeps -> Description(General, "Fetch the specified extra source dependencies and add their source files to the session"),
     frontend.optExtraResolvers -> Description(General, "Extra resolvers to use to fetch extra source dependencies"),
     utils.Caches.optCacheDir -> Description(General, "Specify the directory in which cache files should be stored"),
+    utils.Caches.optBinaryCache -> Description(General, "Set Binary mode for the cache instead of Hash mode, i.e., the cache will contain the entire VC and program in serialized format. This is less space efficient."),
     testgen.optOutputFile -> Description(TestsGeneration, "Specify the output file"),
     testgen.optGenCIncludes -> Description(TestsGeneration, "(GenC variant only) Specify header includes"),
     equivchk.optCompareFuns -> Description(EquivChk, "Only consider functions f1,f2,... for equivalence checking"),

core/src/main/scala/stainless/utils/Caches.scala

@@ -30,6 +30,14 @@ object Caches {
     override val usageRhs = "DIR"
   }
 
+  object optBinaryCache extends inox.FlagOptionDef("binary-cache", false)
+
+  /**
+    * Return the filename for the cache file, depending on the type of cache (Hash or Binary).
+    */
+  def getCacheFilename(ctx: inox.Context): String = 
+    if (ctx.options.findOptionOrDefault(optBinaryCache)) "vccachebin.bin" else "vccachehash.bin" 
+
   /**
    * Get the cache file after creating the cache directory.
    *

core/src/main/scala/stainless/verification/VerificationCache.scala

@@ -15,6 +15,10 @@ import scala.util.{ Success, Failure }
 
 import inox.solvers.SolverFactory
 
+// For Hashing
+import java.security.MessageDigest
+import java.util.HexFormat
+
 object DebugSectionCacheHit extends inox.DebugSection("cachehit")
 object DebugSectionCacheMiss extends inox.DebugSection("cachemiss")
 
@@ -37,6 +41,8 @@ trait VerificationCache extends VerificationChecker { self =>
 
   private lazy val vccache = CacheLoader.get(context)
 
+  private val binaryCacheFlag = context.options.findOptionOrDefault(utils.Caches.optBinaryCache)
+
   override def checkVC(vc: VC, origVC: VC, sf: SolverFactory { val program: self.program.type }) = {
     reporter.debug(s" - Checking cache: '${vc.kind}' VC for ${vc.fid} @${vc.getPos}...")(using DebugSectionVerification)
 
@@ -51,9 +57,16 @@ trait VerificationCache extends VerificationChecker { self =>
       val (canonicalSymbols, canonicalExpr): (Symbols, Expr) =
         utils.Canonization(program)(program.symbols, vc.condition)
 
-      val key = serializer.serialize((vc.satisfiability, canonicalSymbols, canonicalExpr))
 
-      if (vccache `contains` key) {
+      val serialized = serializer.serialize((vc.satisfiability, canonicalSymbols, canonicalExpr))
+
+      val key: CacheKey = if(binaryCacheFlag) {
+                  CacheKey(serialized.bytes)
+                } else {
+                  val bytes = MessageDigest.getInstance("SHA-256").digest(serialized.bytes)
+                  CacheKey(bytes)
+                }
+      if (vccache.contains(key)) {
         reporter.debug(s"Cache hit: '${vc.kind}' VC for ${vc.fid.asString} @${vc.getPos}...")(using DebugSectionVerification)
         given DebugSectionCacheHit.type = DebugSectionCacheHit
         reporter.synchronized {
@@ -68,9 +81,8 @@ trait VerificationCache extends VerificationChecker { self =>
           reporter.ifDebug { debug =>
             given DebugSectionCacheMiss.type = DebugSectionCacheMiss
             given PrinterOptions = new PrinterOptions(printUniqueIds = true, printTypes = true, symbols = Some(canonicalSymbols))
-
+            
             debugVC(vc, origVC)
-
             debug("Canonical symbols:")
             debug(" ## SORTS ##")
             debug(canonicalSymbols.sorts.values.map(_.asString).toList.sorted.mkString("\n\n"))
@@ -103,18 +115,31 @@ object VerificationCache {
   private val serializer = utils.Serializer(stainless.trees)
   import serializer.{given, _}
 
+  object CacheKey{
+    def apply(content: Seq[Byte]): CacheKey = CacheKey(content.toArray)
+  }
+  case class CacheKey(content: Array[Byte]){
+    override def equals(that: Any): Boolean = that match {
+      case c: CacheKey => java.util.Arrays.equals(content, c.content)
+      case _ => false
+    }
+    override val hashCode: Int = java.util.Arrays.hashCode(content)
+
+    def toSeq: Seq[Byte] = content.toSeq
+  }
+
   /** Cache with the ability to save itself to disk. */
   private class Cache(cacheFile: File) {
     // API
-    def contains(key: SerializationResult): Boolean = underlying contains key
-    def +=(key: SerializationResult) = underlying += key -> unusedCacheValue
-    def addPersistently(key: SerializationResult): Unit = {
+    def contains(key: CacheKey): Boolean = underlying contains key
+    def +=(key: CacheKey) = underlying += key -> unusedCacheValue
+    def addPersistently(key: CacheKey): Unit = {
       this += key
-      this.synchronized { serializer.serialize(key, out) }
+      this.synchronized { serializer.serialize(key.toSeq, out) }
     }
 
     // Implementation details
-    private val underlying = TrieMap[SerializationResult, Unit]() // Thread safe
+    private val underlying = TrieMap[CacheKey, Unit]() // Thread safe
     private val unusedCacheValue = ()
 
     // output stream used to save verified VCs
@@ -164,7 +189,7 @@ object VerificationCache {
      *      while being loaded!
      */
     def get(ctx: inox.Context): Cache = this.synchronized {
-      val cacheFile: File = utils.Caches.getCacheFile(ctx, "vccache.bin")
+      val cacheFile: File = utils.Caches.getCacheFile(ctx, utils.Caches.getCacheFilename(ctx))
 
       db.getOrElse(cacheFile, {
         val cache = new Cache(cacheFile)
@@ -174,8 +199,8 @@ object VerificationCache {
 
           try {
             while (true) {
-              val s = serializer.deserialize[SerializationResult](in)
-              cache += s
+              val ck = CacheKey(serializer.deserialize[Seq[Byte]](in))
+              cache += ck
             }
           } catch {
             case e: java.io.EOFException => // Silently consume expected exception.