cleans up

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -67,7 +67,8 @@ case class PPreamble(
                       // after this program is initialized
                       initPosts: Vector[PExpression],
                       imports: Vector[PImport],
-                    ) extends PNode with PUnorderedScope // imports are in program scopes
+                      positions: PositionManager,
+                    ) extends PNode with PUnorderedScope
 
 
 class PositionManager(val positions: Positions) extends Messaging(positions) {

src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala

@@ -69,7 +69,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
   // preamble
 
   def showPreamble(p: PPreamble): Doc = p match {
-    case PPreamble(packageClause, progPosts, imports) =>
+    case PPreamble(packageClause, progPosts, imports, _) =>
       showPreamble(packageClause, progPosts, imports)
   }
 

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -2192,7 +2192,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     val packageClause: PPackageClause = visitNode(ctx.packageClause())
     val initPosts: Vector[PExpression] = visitListNode[PExpression](ctx.initPost())
     val importDecls = ctx.importDecl().asScala.toVector.flatMap(visitImportDecl)
-    PPreamble(packageClause, initPosts, importDecls).at(ctx)
+    PPreamble(packageClause, initPosts, importDecls, pom).at(ctx)
   }
 
   /**

src/main/scala/viper/gobra/frontend/Parser.scala

@@ -7,8 +7,6 @@
 package viper.gobra.frontend
 
 import com.typesafe.scalalogging.LazyLogging
-import org.bitbucket.inkytonik.kiama.rewriting.Cloner.{rewrite, topdown}
-import org.bitbucket.inkytonik.kiama.rewriting.PositionedRewriter.strategyWithName
 import org.bitbucket.inkytonik.kiama.rewriting.{Cloner, PositionedRewriter, Strategy}
 import org.bitbucket.inkytonik.kiama.util.{Positions, Source}
 import org.bitbucket.inkytonik.kiama.util.Messaging.{error, message}
@@ -20,7 +18,6 @@ import org.antlr.v4.runtime.atn.PredictionMode
 import org.antlr.v4.runtime.misc.ParseCancellationException
 import viper.gobra.frontend.GobraParser.{ExprOnlyContext, ImportDeclContext, PreambleContext, SourceFileContext, SpecMemberContext, StmtOnlyContext, TypeOnlyContext}
 import viper.gobra.frontend.PackageResolver.{AbstractImport, AbstractPackage, BuiltInImport, RegularImport, RegularPackage}
-import viper.gobra.frontend.info.Info.{getCacheKey, typeInfoCache}
 import viper.gobra.util.GobraExecutionContext
 import viper.silver.ast.SourcePosition
 
@@ -94,13 +91,14 @@ object Parser {
       private def fastParse(preprocessedInput: Vector[Source]): Set[(AbstractImport, Option[SourcePosition])] = {
         def getImportPaths(preprocessedSource: Source): Set[(RegularImport, Option[SourcePosition])] = {
           processPreamble(preprocessedSource)(config)
-            .map(preambleManager => {
-              preambleManager.preamble.imports
+            .map(preamble => {
+              val pom = preamble.positions
+              preamble.imports
                 .map(importNode => {
-                  val nodeStart = preambleManager.pom.positions.getStart(importNode)
-                  val nodeFinish = preambleManager.pom.positions.getFinish(importNode)
+                  val nodeStart = pom.positions.getStart(importNode)
+                  val nodeFinish = pom.positions.getFinish(importNode)
                   val nodePos = (nodeStart, nodeFinish) match {
-                    case (Some(start), Some(finish)) => Some(preambleManager.pom.translate(start, finish))
+                    case (Some(start), Some(finish)) => Some(pom.translate(start, finish))
                     case _ => None
                   }
                   (RegularImport(importNode.importPath), nodePos)
@@ -178,29 +176,28 @@ object Parser {
     sources
   }
 
-  case class PreambleManager(preamble: PPreamble, pom: PositionManager)
   /**
     * Parses a source's preamble containing all (file-level) imports; This function expects that the input has already
     * been preprocessed
     */
-  private def processPreamble(preprocessedSource: Source)(config: Config): Either[Vector[ParserError], PreambleManager] = {
-    def parseSource(preprocessedSource: Source): Either[Vector[ParserError], PreambleManager] = {
+  private def processPreamble(preprocessedSource: Source)(config: Config): Either[Vector[ParserError], PPreamble] = {
+    def parseSource(preprocessedSource: Source): Either[Vector[ParserError], PPreamble] = {
       val positions = new Positions
       val pom = new PositionManager(positions)
       val parser = new SyntaxAnalyzer[PreambleContext, PPreamble](preprocessedSource, ListBuffer.empty[ParserError], pom, specOnly = true)
-      parser.parse(parser.preamble).map(preamble => PreambleManager(preamble, pom))
+      parser.parse(parser.preamble)
     }
 
     var cacheHit: Boolean = true
-    def parseSourceCached(preprocessedSource: Source): Either[Vector[ParserError], PreambleManager] = {
-      def parseAndStore(): Either[Vector[ParserError], PreambleManager] = {
+    def parseSourceCached(preprocessedSource: Source): Either[Vector[ParserError], PPreamble] = {
+      def parseAndStore(): Either[Vector[ParserError], PPreamble] = {
         cacheHit = false
         parseSource(preprocessedSource)
       }
 
-      val res = preambleCache.computeIfAbsent(getCacheKey(preprocessedSource, specOnly = true), _ => parseAndStore())
+      val res = preambleCache.computeIfAbsent(getPreambleCacheKey(preprocessedSource), _ => parseAndStore())
       if (!cacheHit) {
-        println(s"No cache hit for ${res.map(_.preamble.packageClause.id.name)}'s preamble")
+        println(s"No cache hit for ${res.map(_.packageClause.id.name)}'s preamble")
       }
       res
     }
@@ -224,18 +221,22 @@ object Parser {
 
   type SourceCacheKey = String
   // cache maps a key (obtained by hashing file path and file content) to the parse result
-  private val preambleCache: ConcurrentMap[SourceCacheKey, Either[Vector[ParserError], PreambleManager]] = new ConcurrentHashMap()
+  private val preambleCache: ConcurrentMap[SourceCacheKey, Either[Vector[ParserError], PPreamble]] = new ConcurrentHashMap()
   type PackageCacheKey = String
+  // we cache entire packages and not individual files (i.e. PProgram) as this saves us from copying over positional information
+  // from one to the other position manager. Also, this transformation of copying positional information results in
+  // differen PPackage instances that is problematic for caching type-check results.
   private val packageCache: ConcurrentMap[PackageCacheKey, Either[Vector[VerifierError], PPackage]] = new ConcurrentHashMap()
 
-  /** computes the key for caching a particular source. This takes the name, the specOnly flag, and the file's contents into account */
-  private def getCacheKey(source: Source, specOnly: Boolean): SourceCacheKey = {
-    val key = source.name ++ (if (specOnly) "1" else "0") ++ source.content
+  /** computes the key for caching the preamble of a particular source. This takes the name and the source's content into account */
+  private def getPreambleCacheKey(source: Source): SourceCacheKey = {
+    val key = source.name ++ source.content
     val bytes = MessageDigest.getInstance("MD5").digest(key.getBytes)
     // convert `bytes` to a hex string representation such that we get equality on the key while performing cache lookups
     bytes.map { "%02x".format(_) }.mkString
   }
 
+  /** computes the key for caching a package. This takes the name and the content of each source, the package info and the `specOnly` flag into account */
   private def getPackageCacheKey(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean): PackageCacheKey = {
     val key = sources.map(source => source.name ++ source.content).mkString("") ++ pkgInfo.hashCode.toString ++ (if (specOnly) "1" else "0")
     val bytes = MessageDigest.getInstance("MD5").digest(key.getBytes)

src/main/scala/viper/gobra/frontend/TaskManager.scala

@@ -25,62 +25,28 @@ trait Job[R] {
   private val promise: Promise[R] = Promise()
   def getFuture: Future[R] = promise.future
   protected def compute(): R
-  // private val lock: Object = new AnyRef
 
   def call(): R = {
-    // lock.synchronized {
-      getFuture.value match {
-        case Some(Success(res)) => return res // return already computed type-checker result
-        case Some(Failure(exception)) => Violation.violation(s"Job resulted in exception: $exception")
-        case _ =>
-      }
-      Violation.violation(!compututationStarted, s"Job $this is already on-going")
-      compututationStarted = true
-      val res = try {
-        val res = compute()
-        promise.success(res)
-        res
-      } catch {
-        case e: Exception =>
-          promise.failure(e)
-          throw e
-      }
-      res
-    }
-  // }
-}
-
-/*
-trait Job[R] extends DependentJob[Nothing, R] {
-  val dependencies = Set.empty
-  protected def compute(): R
-
-  override protected def compute(dependentResults: Map[Nothing, R]): R = compute()
-}
-
-trait DependentJob[K, R] {
-  val dependencies: Set[K]
-  private val promise: Promise[R] = Promise()
-  private var compututationStarted = false
-
-  def getFuture: Future[R] = promise.future
-
-  protected def compute(dependentResults: Map[K, R]): R
-
-  def call(dependentResults: Map[K, R]): R = {
     getFuture.value match {
       case Some(Success(res)) => return res // return already computed type-checker result
       case Some(Failure(exception)) => Violation.violation(s"Job resulted in exception: $exception")
       case _ =>
     }
-    Violation.violation(!compututationStarted, s"Job is already on-going")
+    Violation.violation(!compututationStarted, s"Job $this is already on-going")
     compututationStarted = true
-    val res = compute(dependentResults)
-    promise.success(res)
+    val res = try {
+      val res = compute()
+      promise.success(res)
+      res
+    } catch {
+      case e: Exception =>
+        promise.failure(e)
+        // propagate this exception for the case that `call` is executed synchronously:
+        throw e
+    }
     res
   }
 }
- */
 
 class TaskManager[K, R](mode: TaskManagerMode) {
   private val jobs: ConcurrentMap[K, Job[R]] = new ConcurrentHashMap()

src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala

@@ -402,46 +402,7 @@ trait MemberResolution { this: TypeInfoImpl =>
     )
   }
 
-  // TODO: move this method to another file
   def getTypeChecker(importTarget: AbstractImport, errNode: PNode): Either[Messages, ExternalTypeInfo] = {
-    /*
-    def parseAndTypeCheck(importTarget: AbstractImport): Either[Vector[VerifierError], ExternalTypeInfo] = {
-      val pkgSources = PackageResolver.resolveSources(importTarget)(config)
-        .getOrElse(Vector())
-        .map(_.source)
-      val res = for {
-        nonEmptyPkgSources <- if (pkgSources.isEmpty)
-          Left(Vector(NotFoundError(s"No source files for package '$importTarget' found")))
-        else Right(pkgSources)
-        parsedProgram <- Parser.parse(nonEmptyPkgSources, Source.getPackageInfo(nonEmptyPkgSources.head, config.projectRoot), specOnly = true)(config)
-        // TODO maybe don't check whole file but only members that are actually used/imported
-        // By parsing only declarations and their specification, there shouldn't be much left to type check anyways
-        // Info.check would probably need some restructuring to type check only certain members
-        info <- Info.check(parsedProgram, nonEmptyPkgSources, context)(config)
-      } yield info
-      res.fold(
-        errs => context.addErrenousPackage(importTarget, errs)(config),
-        info => context.addPackage(importTarget, info)(config)
-      )
-      res
-    }
-    */
-    /*
-    def createImportError(errs: Vector[VerifierError]): Messages = {
-      // create an error message located at the import statement to indicate errors in the imported package
-      // we distinguish between parse and type errors, cyclic imports, and packages whose source files could not be found
-      val notFoundErr = errs.collectFirst { case e: NotFoundError => e }
-      // alternativeErr is a function to compute the message only when needed
-
-      val alternativeErr = () => context.getParserImportCycle(importTarget) match {
-        case Some(cycle) =>
-          message(errNode, s"Package '$importTarget' is part of the following import cycle that involves the import ${cycle.importNodeCausingCycle}: ${cycle.cyclicPackages.mkString("[", ", ", "]")}")
-        case _ => message(errNode, s"Package '$importTarget' contains errors: $errs")
-      }
-      notFoundErr.map(e => message(errNode, e.message))
-        .getOrElse(alternativeErr())
-    }
-    */
     def createImportError(errs: Vector[VerifierError]): Messages = {
       // create an error message located at the import statement to indicate errors in the imported package
       // we distinguish between regular errors and packages whose source files could not be found (not that cyclic
@@ -453,17 +414,6 @@ trait MemberResolution { this: TypeInfoImpl =>
         .getOrElse(alternativeErr())
     }
 
-    // check if package was already parsed, otherwise do parsing and type checking:
-    /*
-    val cachedInfo = context.getTypeInfo(importTarget)(config)
-    if (cachedInfo.isEmpty) {
-      println(s"package $importTarget is not contained in context")
-    }
-    Violation.violation(cachedInfo.nonEmpty, s"package $importTarget is not contained in context")
-    cachedInfo.get.left.map(createImportError)
-    // cachedInfo.getOrElse(parseAndTypeCheck(importTarget)).left.map(createImportError)
-     */
-    // context.getTypeInfo(importTarget)(config).left.map(createImportError)
     Violation.violation(dependentTypeInfo.contains(importTarget), s"Expected that package ${tree.root.info.id} has access to the type information of package $importTarget")
     dependentTypeInfo(importTarget)().left.map(createImportError)
   }

src/test/scala/viper/gobra/DetailedBenchmarkTests.scala

@@ -115,7 +115,6 @@ class DetailedBenchmarkTests extends BenchmarkTests {
         assert(c.packageInfoInputMap.size == 1)
         val pkgInfo = c.packageInfoInputMap.keys.head
         Info.check(c, RegularPackage(pkgInfo.id), parseResults)(executor)
-        // Info.check(parsedPackage, c.packageInfoInputMap(pkgInfo))(c).map(typeInfo => (parsedPackage, typeInfo))
       })
 
     private val desugaring: NextStep[TypeInfo, Program, Vector[VerifierError]] =