saves ongoing work

src/main/antlr4/GobraParser.g4

@@ -39,6 +39,10 @@ sourceFile:
     (specMember | declaration | ghostMember) eos
   )* EOF;
 
+// `preamble` is a second entry point allowing us to parse only the top of a source.
+// That's also why we don not enforce EOF at the end.
+preamble: (initPost eos)* packageClause eos (importDecl eos)*;
+
 initPost: INIT_POST expression;
 
 importPre: IMPORT_PRE expression;

src/main/java/viper/gobra/frontend/GobraParserBaseVisitor.java

@@ -1,3 +1,4 @@
+// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.12.0
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.AbstractParseTreeVisitor;
 
@@ -9,6 +10,7 @@
  * @param <T> The return type of the visit operation. Use {@link Void} for
  * operations with no return type.
  */
+@SuppressWarnings("CheckReturnValue")
 public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> implements GobraParserVisitor<T> {
 	/**
 	 * {@inheritDoc}
@@ -52,6 +54,13 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitSourceFile(GobraParser.SourceFileContext ctx) { return visitChildren(ctx); }
+	/**
+	 * {@inheritDoc}
+	 *
+	 * <p>The default implementation returns the result of calling
+	 * {@link #visitChildren} on {@code ctx}.</p>
+	 */
+	@Override public T visitPreamble(GobraParser.PreambleContext ctx) { return visitChildren(ctx); }
 	/**
 	 * {@inheritDoc}
 	 *
@@ -1529,4 +1538,4 @@ public class GobraParserBaseVisitor<T> extends AbstractParseTreeVisitor<T> imple
 	 * {@link #visitChildren} on {@code ctx}.</p>
 	 */
 	@Override public T visitEos(GobraParser.EosContext ctx) { return visitChildren(ctx); }
-}
+}

src/main/java/viper/gobra/frontend/GobraParserVisitor.java

@@ -1,3 +1,4 @@
+// Generated from src/main/antlr4/GobraParser.g4 by ANTLR 4.12.0
 package viper.gobra.frontend;
 import org.antlr.v4.runtime.tree.ParseTreeVisitor;
 
@@ -45,6 +46,12 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitSourceFile(GobraParser.SourceFileContext ctx);
+	/**
+	 * Visit a parse tree produced by {@link GobraParser#preamble}.
+	 * @param ctx the parse tree
+	 * @return the visitor result
+	 */
+	T visitPreamble(GobraParser.PreambleContext ctx);
 	/**
 	 * Visit a parse tree produced by {@link GobraParser#initPost}.
 	 * @param ctx the parse tree
@@ -1348,4 +1355,4 @@ public interface GobraParserVisitor<T> extends ParseTreeVisitor<T> {
 	 * @return the visitor result
 	 */
 	T visitEos(GobraParser.EosContext ctx);
-}
+}

src/main/scala/viper/gobra/Gobra.scala

@@ -12,11 +12,11 @@ import java.nio.file.Paths
 import java.util.concurrent.ExecutionException
 import com.typesafe.scalalogging.StrictLogging
 import org.slf4j.LoggerFactory
-import viper.gobra.ast.frontend.PPackage
 import viper.gobra.ast.internal.Program
 import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, ConstantPropagation, InternalTransform, OverflowChecksTransform}
 import viper.gobra.backend.BackendVerifier
-import viper.gobra.frontend.info.Info.Context
+import viper.gobra.frontend.PackageResolver.{AbstractPackage, RegularPackage}
+import viper.gobra.frontend.Parser.ParseSuccessResult
 import viper.gobra.frontend.info.{Info, TypeInfo}
 import viper.gobra.frontend.{Config, Desugar, PackageInfo, Parser, ScallopGobraConfig}
 import viper.gobra.reporting._
@@ -28,6 +28,7 @@ import viper.silver.{ast => vpr}
 
 import java.time.format.DateTimeFormatter
 import java.time.LocalTime
+import scala.annotation.unused
 import scala.concurrent.{Await, Future, TimeoutException}
 
 object GoVerifier {
@@ -158,11 +159,11 @@ class Gobra extends GoVerifier with GoIdeVerifier {
       for {
         finalConfig <- getAndMergeInFileConfig(config, pkgInfo)
         _ = setLogLevel(finalConfig)
-        parsedPackage <- performParsing(pkgInfo, finalConfig)
-        typeInfo <- performTypeChecking(parsedPackage, executor, finalConfig)
-        program <- performDesugaring(parsedPackage, typeInfo, finalConfig)
-        program <- performInternalTransformations(program, finalConfig, pkgInfo)
-        viperTask <- performViperEncoding(program, finalConfig, pkgInfo)
+        parseResults <- performParsing(finalConfig, pkgInfo)(executor)
+        typeInfo <- performTypeChecking(finalConfig, pkgInfo, parseResults)(executor)
+        program <- performDesugaring(finalConfig, typeInfo)(executor)
+        program <- performInternalTransformations(finalConfig, pkgInfo, program)(executor)
+        viperTask <- performViperEncoding(finalConfig, pkgInfo, program)(executor)
       } yield (viperTask, finalConfig)
     }
 
@@ -177,7 +178,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     // directly declaring the parameter implicit somehow does not work as the compiler is unable to spot the inheritance
     implicit val _executor: GobraExecutionContext = executor
     val viperTask = BackendVerifier.Task(ast, backtrack)
-    performVerification(viperTask, config, pkgInfo)
+    performVerification(config, pkgInfo, viperTask)
       .map(BackTranslator.backTranslate(_)(config))
       .recoverWith {
         case e: ExecutionException if isKnownZ3Bug(e) =>
@@ -242,31 +243,46 @@ class Gobra extends GoVerifier with GoIdeVerifier {
       .setLevel(config.logLevel)
   }
 
-  private def performParsing(pkgInfo: PackageInfo, config: Config): Either[Vector[VerifierError], PPackage] = {
+  private def performParsing(config: Config, pkgInfo: PackageInfo)(executor: GobraExecutionContext): Either[Vector[VerifierError], Map[AbstractPackage, ParseSuccessResult]] = {
     if (config.shouldParse) {
       val startMs = System.currentTimeMillis()
-      val sourcesToParse = config.packageInfoInputMap(pkgInfo)
-      val res = Parser.parse(sourcesToParse, pkgInfo)(config)
+      val res = Parser.parse(config, pkgInfo)(executor)
       val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
       println(s"parser phase done, took ${durationS}s")
       res
+      /*
+      val sourcesToParse = config.packageInfoInputMap(pkgInfo)
+      val res = Parser.parse(sourcesToParse, pkgInfo)(config)
+       */
+      /*
+      val parseManager = Parser.parse(pkgInfo)(config, executionContext)
+      config.typeCheckMode match {
+        case TypeCheckMode.Lazy => // don't do anything
+        case TypeCheckMode.Sequential | TypeCheckMode.Parallel =>
+          parseManager.awaitResults()
+          val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
+          println(s"parser phase done, took ${durationS}s")
+          println(s"parsed packages: ${parseManager.getResults.map{ case (pkg, _) => pkg }.mkString(", ")}")
+      }
+      Right(parseManager)
+      */
     } else {
       Left(Vector())
     }
   }
 
-  private def performTypeChecking(parsedPackage: PPackage, executionContext: GobraExecutionContext, config: Config): Either[Vector[VerifierError], TypeInfo] = {
+  private def performTypeChecking(config: Config, pkgInfo: PackageInfo, parseResults: Map[AbstractPackage, ParseSuccessResult])(executor: GobraExecutionContext): Either[Vector[VerifierError], TypeInfo] = {
     if (config.shouldTypeCheck) {
-      Info.check(parsedPackage, config.packageInfoInputMap(parsedPackage.info), isMainContext = true, context = new Context(executionContext, config))(config)
+      Info.check(config, RegularPackage(pkgInfo.id), parseResults)(executor)
     } else {
       Left(Vector())
     }
   }
 
-  private def performDesugaring(parsedPackage: PPackage, typeInfo: TypeInfo, config: Config): Either[Vector[VerifierError], Program] = {
+  private def performDesugaring(config: Config, typeInfo: TypeInfo)(@unused executor: GobraExecutionContext): Either[Vector[VerifierError], Program] = {
     if (config.shouldDesugar) {
       val startMs = System.currentTimeMillis()
-      val res = Right(Desugar.desugar(parsedPackage, typeInfo)(config))
+      val res = Right(Desugar.desugar(typeInfo.tree.root, typeInfo)(config))
       val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
       println(s"desugaring done, took ${durationS}s")
       res
@@ -275,19 +291,11 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     }
   }
 
-  private def performVerification(config: Config, pkgInfo: PackageInfo, ast: vpr.Program, backtrack: BackTranslator.BackTrackInfo)(executor: GobraExecutionContext): Future[VerifierResult] = {
-    if (config.noVerify) {
-      Future(VerifierResult.Success)(executor)
-    } else {
-      verifyAst(config, pkgInfo, ast, backtrack)(executor)
-    }
-  }
-
   /**
     * Applies transformations to programs in the internal language. Currently, only adds overflow checks but it can
     * be easily extended to perform more transformations
     */
-  private def performInternalTransformations(program: Program, config: Config, pkgInfo: PackageInfo): Either[Vector[VerifierError], Program] = {
+  private def performInternalTransformations(config: Config, pkgInfo: PackageInfo, program: Program)(@unused executor: GobraExecutionContext): Either[Vector[VerifierError], Program] = {
     // constant propagation does not cause duplication of verification errors caused
     // by overflow checks (if enabled) because all overflows in constant declarations 
     // can be found by the well-formedness checks.
@@ -303,7 +311,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     Right(result)
   }
 
-  private def performViperEncoding(program: Program, config: Config, pkgInfo: PackageInfo): Either[Vector[VerifierError], BackendVerifier.Task] = {
+  private def performViperEncoding(config: Config, pkgInfo: PackageInfo, program: Program)(@unused executor: GobraExecutionContext): Either[Vector[VerifierError], BackendVerifier.Task] = {
     if (config.shouldViperEncode) {
       val startMs = System.currentTimeMillis()
       val res = Right(Translator.translate(program, pkgInfo)(config))
@@ -315,7 +323,15 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     }
   }
 
-  private def performVerification(viperTask: BackendVerifier.Task, config: Config, pkgInfo: PackageInfo)(implicit executor: GobraExecutionContext): Future[BackendVerifier.Result] = {
+  private def performVerification(config: Config, pkgInfo: PackageInfo, ast: vpr.Program, backtrack: BackTranslator.BackTrackInfo)(executor: GobraExecutionContext): Future[VerifierResult] = {
+    if (config.noVerify) {
+      Future(VerifierResult.Success)(executor)
+    } else {
+      verifyAst(config, pkgInfo, ast, backtrack)(executor)
+    }
+  }
+
+  private def performVerification(config: Config, pkgInfo: PackageInfo, viperTask: BackendVerifier.Task)(implicit executor: GobraExecutionContext): Future[BackendVerifier.Result] = {
     if (config.shouldVerify) {
       BackendVerifier.verify(viperTask, pkgInfo)(config)
     } else {

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

@@ -61,6 +61,15 @@ case class PProgram(
                    ) extends PNode with PUnorderedScope // imports are in program scopes
 
 
+case class PPreamble(
+                      packageClause: PPackageClause,
+                      // init postconditions describe the state and resources right
+                      // after this program is initialized
+                      initPosts: Vector[PExpression],
+                      imports: Vector[PImport],
+                    ) extends PNode with PUnorderedScope // imports are in program scopes
+
+
 class PositionManager(val positions: Positions) extends Messaging(positions) {
 
   def translate[E <: VerifierError](

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

@@ -16,8 +16,7 @@ import viper.gobra.backend.{ViperBackend, ViperBackends}
 import viper.gobra.GoVerifier
 import viper.gobra.frontend.PackageResolver.FileResource
 import viper.gobra.frontend.Source.getPackageInfo
-import viper.gobra.frontend.info.Info.TypeCheckMode
-import viper.gobra.frontend.info.Info.TypeCheckMode.TypeCheckMode
+import viper.gobra.frontend.TaskManagerMode.{Lazy, Parallel, Sequential, TaskManagerMode}
 import viper.gobra.reporting.{FileWriterReporter, GobraReporter, StdIOReporter}
 import viper.gobra.util.{TypeBounds, Violation}
 import viper.silver.ast.SourcePosition
@@ -70,7 +69,7 @@ object ConfigDefaults {
   lazy val DefaultEnableLazyImports: Boolean = false
   lazy val DefaultNoVerify: Boolean = false
   lazy val DefaultNoStreamErrors: Boolean = false
-  lazy val DefaultTypeCheckMode: TypeCheckMode = TypeCheckMode.Parallel
+  lazy val DefaultTypeCheckMode: TaskManagerMode = TaskManagerMode.Parallel
 }
 
 case class Config(
@@ -122,7 +121,7 @@ case class Config(
                    enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                    noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
                    noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors,
-                   typeCheckMode: TypeCheckMode = ConfigDefaults.DefaultTypeCheckMode,
+                   typeCheckMode: TaskManagerMode = ConfigDefaults.DefaultTypeCheckMode,
 ) {
 
   def merge(other: Config): Config = {
@@ -219,7 +218,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                       noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
                       noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors,
-                      typeCheckMode: TypeCheckMode = ConfigDefaults.DefaultTypeCheckMode,
+                      typeCheckMode: TaskManagerMode = ConfigDefaults.DefaultTypeCheckMode,
                      ) {
   def shouldParse: Boolean = true
   def shouldTypeCheck: Boolean = !shouldParseOnly
@@ -646,16 +645,16 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     noshort = true,
   )
 
-  val typeCheckMode: ScallopOption[TypeCheckMode] = choice(
+  val typeCheckMode: ScallopOption[TaskManagerMode] = choice(
     name = "typeCheckMode",
     choices = Seq("LAZY", "SEQUENTIAL", "PARALLEL"),
     descr = "Specifies the mode in which type-checking is performed.",
     default = Some("PARALLEL"),
     noshort = true
   ).map {
-    case "LAZY" => TypeCheckMode.Lazy
-    case "SEQUENTIAL" => TypeCheckMode.Sequential
-    case "PARALLEL" => TypeCheckMode.Parallel
+    case "LAZY" => Lazy
+    case "SEQUENTIAL" => Sequential
+    case "PARALLEL" => Parallel
     case _ => ConfigDefaults.DefaultTypeCheckMode
   }
 

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

@@ -32,8 +32,11 @@ object Desugar {
     val importsCollector = new PackageInitSpecCollector
     // independently desugar each imported package.
     val importedDesugaringStartMs = System.currentTimeMillis()
-    val importedPrograms = info.context.getContexts map { tI => {
-      val typeInfo: TypeInfo = tI.getTypeInfo
+    // val importedPrograms = info.context.getContexts map { tI => {
+    // val importedPrograms = info.dependentTypeInfo.map { case (abstractPackage, tIFn) => {
+    val importedPrograms = info.getTransitiveTypeInfos.map { tI => {
+      val typeInfo = tI.getTypeInfo
+      // val typeInfo: TypeInfo = tIFn().map(_.getTypeInfo).getOrElse(Violation.violation(s"cannot desugar package $abstractPackage for which type-checking failed")) // tI.getTypeInfo
       val importedPackage = typeInfo.tree.originalRoot
       val d = new Desugarer(importedPackage.positions, typeInfo)
       // registers a package to generate proof obligations for its init code
@@ -3460,16 +3463,19 @@ object Desugar {
       }
 
       // Collect and register all import-preconditions
-      pkg.imports.foreach{ imp =>
-        info.context.getTypeInfo(RegularImport(imp.importPath))(config) match {
+      pkg.imports.foreach{ imp => {
+        val importedPackage = RegularImport(imp.importPath)
+        Violation.violation(info.dependentTypeInfo.contains(importedPackage), s"Desugarer expects to have acess to the type information of all imported packages but could not find $importedPackage")
+        // info.context.getTypeInfo(RegularImport(imp.importPath))(config) match {
+        info.dependentTypeInfo(importedPackage)() match {
           // case Some(Right(tI)) =>
           case Right(tI) =>
             val desugaredPre = imp.importPres.map(specificationD(FunctionContext.empty(), info))
             Violation.violation(!config.enableLazyImports || desugaredPre.isEmpty, s"Import precondition found despite running with ${Config.enableLazyImportOptionPrettyPrinted}")
             specCollector.addImportPres(tI.getTypeInfo.tree.originalRoot, desugaredPre)
           case e => Violation.violation(config.enableLazyImports, s"Unexpected value found $e while importing ${imp.importPath} - type information is assumed to be available for all packages when Gobra is executed with lazy imports disabled")
         }
-      }
+      }}
 
       // Collect and register all postconditions of all PPrograms (i.e., files) in pkg
       val pkgPost = pkg.programs.flatMap(_.initPosts).map(specificationD(FunctionContext.empty(), info))

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

@@ -2188,6 +2188,13 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     PProgram(packageClause, initPosts, importDecls, members ++ decls ++ ghostMembers).at(ctx)
   }
 
+  override def visitPreamble(ctx: GobraParser.PreambleContext): PPreamble = {
+    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)
+  }
+
   /**
     * Visists an init postcondition
     * @param ctx the parse tree