perf: fix #1116

src/col/vct/col/origin/Origin.scala

@@ -55,15 +55,6 @@ trait OriginContent {
  */
 trait NameStrategy extends OriginContent
 
-case class SimpleSourceName(name: String) extends NameStrategy {
-  override def name(tail: Origin): Option[Name] =
-    Some(Name.Preferred(
-      tail.span[NameStrategy]._1.originContents.collect {
-        case NamePrefix(prefix) => prefix
-      }.reverse :+ name
-    ))
-}
-
 case class PreferredName(preferredName: Seq[String]) extends NameStrategy {
   override def name(tail: Origin): Option[Name] =
     Some(Name.Preferred(

src/col/vct/col/serialize/SerializeOrigin.scala

@@ -1,14 +1,21 @@
 package vct.col.serialize
 
 import vct.col.ast.{serialize => ser}
-import vct.col.origin.Origin
+import vct.col.origin._
 
 import scala.annotation.unused
 
 object SerializeOrigin {
   def deserialize(@unused origin: ser.Origin): Origin =
-    Origin(Nil)
+    Origin(origin.content.map(_.content).map {
+      case ser.OriginContent.Content.SourceName(name) => SourceName(name.name)
+      case ser.OriginContent.Content.PreferredName(name) => PreferredName(name.preferredName)
+    })
 
   def serialize(@unused origin: Origin): ser.Origin =
-    ser.Origin(Nil)
+    ser.Origin(origin.originContents.flatMap {
+      case SourceName(name) => Seq(ser.OriginContent.Content.SourceName(ser.SourceName(name)))
+      case PreferredName(preferredName) => Seq(ser.OriginContent.Content.PreferredName(ser.PreferredName(preferredName)))
+      case _ => Nil
+    }.map(ser.OriginContent(_)))
 }

src/main/vct/cache/Caches.scala

@@ -0,0 +1,33 @@
+package vct.cache
+
+import com.typesafe.scalalogging.LazyLogging
+import hre.cache.Cache
+import vct.main.BuildInfo
+
+import java.nio.file.Path
+
+case object Caches extends LazyLogging {
+  // Val's, so that multiple VerCors runs in one JVM (e.g. tests) benefit from a shared cache even when the cache is
+  // variate.
+  lazy val getLibraryCache: Path = getDirectory(BuildInfo.currentCommit).resolve("library")
+
+  lazy val getCarbonDirectory: Path = getViperDirectory(BuildInfo.carbonCommit).resolve("carbon").resolve("verified")
+  lazy val getSiliconDirectory: Path = getViperDirectory(BuildInfo.siliconCommit).resolve("silicon").resolve("verified")
+
+  private def getDirectory(keys: String*): Path = {
+    val variate = BuildInfo.gitHasChanges != "false"
+
+    if(variate) {
+      logger.warn("Caching is enabled, but results will be discarded, since there were uncommitted changes at compilation time.")
+    }
+
+    Cache.getDirectory(variate, keys)
+  }
+
+  private def getViperDirectory(backendCommit: String): Path =
+    getDirectory(
+      BuildInfo.currentCommit,
+      BuildInfo.silverCommit,
+      backendCommit,
+    )
+}

src/main/vct/importer/Util.scala

@@ -1,14 +1,18 @@
 package vct.importer
 
-import hre.io.Readable
-import vct.col.ast.{JavaClass, JavaNamespace, Program}
+import hre.io.{RWFile, Readable}
+import vct.cache.Caches
+import vct.col.ast.{Deserialize, JavaClass, JavaNamespace, Program, Serialize}
 import vct.col.origin.{Blame, Origin, ReadableOrigin, VerificationFailure}
 import vct.col.rewrite.Disambiguate
 import vct.main.stages.Resolution
 import vct.parsers.{ColJavaParser, ColPVLParser}
 import vct.parsers.transform.ConstantBlameProvider
 import vct.result.VerificationError.UserError
 
+import java.nio.file.Files
+import scala.util.Using
+
 case object Util {
   case object LibraryFileBlame extends Blame[VerificationFailure] {
     override def blame(error: VerificationFailure): Unit =
@@ -22,10 +26,29 @@ case object Util {
   }
 
   def loadPVLLibraryFile[G](readable: Readable): Program[G] = {
-    val res = ColPVLParser(Origin(Seq(ReadableOrigin(readable))), ConstantBlameProvider(LibraryFileBlame)).parse(readable)
-    val context = Resolution(ConstantBlameProvider(LibraryFileBlame)).run(res)
-    val unambiguousProgram: Program[_] = Disambiguate().dispatch(context.tasks.head.program)
-    unambiguousProgram.asInstanceOf[Program[G]]
+    val text = readable.readToCompletion()
+    val cacheDir = Caches.getLibraryCache.resolve("%02x" format text.hashCode())
+    val pinnedLibrary = cacheDir.resolve("library.in")
+    val result = cacheDir.resolve("library.colpb")
+
+    if(!Files.exists(cacheDir) || RWFile(pinnedLibrary.toFile).readToCompletion() != text) {
+      val res = ColPVLParser(Origin(Seq(ReadableOrigin(readable))), ConstantBlameProvider(LibraryFileBlame)).parse(readable)
+      val context = Resolution(ConstantBlameProvider(LibraryFileBlame)).run(res)
+      val unambiguousProgram: Program[_] = Disambiguate().dispatch(context.tasks.head.program)
+
+      Files.createDirectories(cacheDir)
+      Using(Files.newOutputStream(pinnedLibrary)) { out =>
+        out.write(text.getBytes)
+      }
+
+      Using(Files.newOutputStream(result)) { out =>
+        Serialize.serialize(unambiguousProgram).writeTo(out)
+      }
+    }
+
+    Using(Files.newInputStream(result)) { in =>
+      Deserialize.deserializeProgram[G](vct.col.ast.serialize.Program.parseFrom(in), 0)
+    }.get
   }
 
   case class JavaLoadError(error: String) extends UserError {

src/main/vct/main/stages/Backend.scala

@@ -3,7 +3,7 @@ package vct.main.stages
 import hre.io.{RWFile, Writeable}
 import hre.progress.Progress
 import hre.stages.Stage
-import vct.cache.VerificationCache
+import vct.cache.Caches
 import vct.col.ast.{Program, Serialize, Verification, VerificationContext}
 import vct.col.origin.ExpectedError
 import vct.col.rewrite.Generation
@@ -50,15 +50,15 @@ case object Backend {
         traceBranchConditions = options.devSiliconTraceBranchConditions,
         branchConditionReportInterval = options.devSiliconBranchConditionReportInterval,
         options = options.backendFlags,
-      ), options.backendFile, if(options.devCache) Some(VerificationCache.getSiliconDirectory) else None)
+      ), options.backendFile, if(options.devCache) Some(Caches.getSiliconDirectory) else None)
 
     case types.Backend.Carbon => SilverBackend(Carbon(
       z3Path = options.z3Path,
       boogiePath = options.boogiePath,
       printFile = options.devViperProverLogFile,
       proverLogFile = options.devCarbonBoogieLogFile,
       options = options.backendFlags,
-    ), options.backendFile, Some(VerificationCache.getCarbonDirectory))
+    ), options.backendFile, if(options.devCache) Some(Caches.getSiliconDirectory) else None)
   }
 }
 

src/serialize/vct/col/ast/serialize/Origin.proto

@@ -8,10 +8,15 @@ message Origin {
 
 message OriginContent {
   oneof content {
-    DummyOriginContent dummy = 9999;
+    SourceName source_name = 1;
+    PreferredName preferred_name = 2;
   }
 }
 
-message DummyOriginContent {
+message SourceName {
+  required string name = 1;
+}
 
+message PreferredName {
+  repeated string preferred_name = 1;
 }

test/main/vct/test/integration/helper/VercorsSpec.scala

@@ -89,7 +89,7 @@ abstract class VercorsSpec extends AnyFlatSpec {
               Options.parse((Seq("--backend", "silicon") ++ flags).toArray).get,
               inputs
             )
-          case types.Backend.Carbon => Verify.verifyWithCarbon(inputs)
+          case types.Backend.Carbon =>
             Verify.verifyWithOptions(
               Options.parse((Seq("--backend", "carbon") ++ flags).toArray).get,
               inputs