fixes reporting of errors in imported packages and reports them as pa…

…rt of type-checking

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

@@ -16,7 +16,7 @@ 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.PackageResolver.{AbstractPackage, RegularPackage}
-import viper.gobra.frontend.Parser.ParseSuccessResult
+import viper.gobra.frontend.Parser.{ParseResult, ParseSuccessResult}
 import viper.gobra.frontend.info.{Info, TypeInfo}
 import viper.gobra.frontend.{Config, Desugar, PackageInfo, Parser, ScallopGobraConfig}
 import viper.gobra.reporting._
@@ -243,7 +243,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
       .setLevel(config.logLevel)
   }
 
-  private def performParsing(config: Config, pkgInfo: PackageInfo)(executor: GobraExecutionContext): Either[Vector[VerifierError], Map[AbstractPackage, ParseSuccessResult]] = {
+  private def performParsing(config: Config, pkgInfo: PackageInfo)(executor: GobraExecutionContext): Either[Vector[VerifierError], Map[AbstractPackage, ParseResult]] = {
     if (config.shouldParse) {
       val startMs = System.currentTimeMillis()
       val res = Parser.parse(config, pkgInfo)(executor)
@@ -257,7 +257,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     }
   }
 
-  private def performTypeChecking(config: Config, pkgInfo: PackageInfo, parseResults: Map[AbstractPackage, ParseSuccessResult])(executor: GobraExecutionContext): Either[Vector[VerifierError], TypeInfo] = {
+  private def performTypeChecking(config: Config, pkgInfo: PackageInfo, parseResults: Map[AbstractPackage, ParseResult])(executor: GobraExecutionContext): Either[Vector[VerifierError], TypeInfo] = {
     if (config.shouldTypeCheck) {
       Info.check(config, RegularPackage(pkgInfo.id), parseResults)(executor)
     } else {

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

@@ -18,6 +18,7 @@ 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.Parser.ParseSuccessResult
 import viper.gobra.util.GobraExecutionContext
 import viper.silver.ast.SourcePosition
 
@@ -57,28 +58,30 @@ object Parser {
         // before parsing, get imports and add these parse jobs
         val imports = fastParse(preprocessedSources)
         val preambleParsingDurationMs = System.currentTimeMillis() - startPreambleParsingMs
-        // val importResults: Set[Either[Vector[VerifierError], Future[ParseResult]]] = imports.map{ case (directImportTarget, importErrorFactory) => {
-        val importResults: Set[Future[ParseResult]] = imports.map { case (directImportTarget, importErrorFactory) =>
+        val importResults: Set[Either[Vector[ParserError], Future[_]]] = imports.map { case (directImportTarget, importErrorFactory) =>
+        // val importResults: Set[Future[ParseResult]] = imports.map { case (directImportTarget, importErrorFactory) =>
             val directImportPackage = AbstractPackage(directImportTarget)(config)
             val nonEmptyImportedSources = for {
               resolveSourceResults <- PackageResolver.resolveSources(directImportTarget)(config)
               importedSources = resolveSourceResults.map(_.source)
               nonEmptyImportedSources <- if (importedSources.isEmpty) Left(s"No source files for package '$directImportTarget' found") else Right(importedSources)
             } yield nonEmptyImportedSources
-
           nonEmptyImportedSources.fold(
             errMsg => {
               val errs = importErrorFactory(errMsg)
               manager.addIfAbsent(directImportPackage, ParseFailureJob(errs))(executionContext)
-              Future.successful(Left(errs))
+              Left(errs)
             },
             nonEmptySources => {
               manager.addIfAbsent(directImportPackage, ParseSourcesJob(nonEmptySources, directImportPackage))(executionContext)
+              Right(manager.getFuture(directImportPackage))
+              /*
               manager.getFuture(directImportPackage).flatten
                 .map {
                   case Left(_) => Left(importErrorFactory(s"Imported package contains errors"))
                   case success => success
                 }(executionContext)
+              */
             })
             /*
             val importedSources = PackageResolver.resolveSources(directImportTarget)(config)
@@ -99,9 +102,23 @@ object Parser {
             */
         }
 
-        // val (importFailures, futs) = importResults.partitionMap(identity)
-        // val flatImportFailures = importFailures.toVector.flatten
+        val (importFailures, futs) = importResults.partitionMap(identity)
+        val flatImportFailures = importFailures.toVector.flatten
+
+        val res: ParseResult = for {
+          _ <- if (flatImportFailures.isEmpty) Right(()) else Left(flatImportFailures)
+          startMs = System.currentTimeMillis()
+          parsedProgram <- Parser.process(preprocessedSources, pkgInfo, specOnly = specOnly)(config)
+          postprocessedProgram <- Parser.postprocess(Right((preprocessedSources, parsedProgram)), specOnly = specOnly)(config)
+          _ = logger.trace {
+            val parsingDurationMs = System.currentTimeMillis() - startMs
+            val parsingDurationS = f"${parsingDurationMs / 1000f}%.1f"
+            val preambleParsingRatio = f"${100f * preambleParsingDurationMs / parsingDurationMs}%.1f"
+            s"parsing ${pkgInfo.id} done (took ${parsingDurationS}s; parsing preamble overhead is ${preambleParsingRatio}%)"
+          }
+        } yield (pkgSources, postprocessedProgram._2) // we use `pkgSources` as the preprocessing of sources should be transparent from the outside
 
+        /*
         val startMs = System.currentTimeMillis()
         val res = for {
           parsedProgram <- Parser.process(preprocessedSources, pkgInfo, specOnly = specOnly)(config)
@@ -112,10 +129,10 @@ object Parser {
           val parsingDurationS = f"${parsingDurationMs / 1000f}%.1f"
           val preambleParsingRatio = f"${100f * preambleParsingDurationMs / parsingDurationMs}%.1f"
           s"parsing ${pkgInfo.id} done (took ${parsingDurationS}s; parsing preamble overhead is ${preambleParsingRatio}%)"
-        }
+        }*/
 
         implicit val executor: GobraExecutionContext = executionContext
-
+        /*
         Future.sequence(importResults)
           .map(dependencyResults => {
             val (importErrors, _) = dependencyResults.partitionMap(identity)
@@ -137,10 +154,9 @@ object Parser {
             }
              */
           })
-        /*
+        */
         Future.sequence(futs)
           .map(_ => res)
-         */
       }
 
       type ImportErrorFactory = String => Vector[ParserError]
@@ -214,6 +230,14 @@ object Parser {
         .collect { case (key, Right(res)) => (key, res) }
         .toMap
     }
+
+    def getResults(executionContext: GobraExecutionContext): Map[AbstractPackage, ParseResult] = {
+      implicit val executor: GobraExecutionContext = executionContext
+      val futs = manager.getAllFutures.map { case (key, fut) => fut.flatten.map(res => (key, res)) }
+      val results = Await.result(Future.sequence(futs), Duration.Inf)
+      results
+        .toMap
+    }
   }
 
   /**
@@ -232,15 +256,15 @@ object Parser {
     *
     */
 
-  def parse(config: Config, pkgInfo: PackageInfo)(executionContext: GobraExecutionContext): Either[Vector[VerifierError], Map[AbstractPackage, ParseSuccessResult]] = {
+  def parse(config: Config, pkgInfo: PackageInfo)(executionContext: GobraExecutionContext): Either[Vector[VerifierError], Map[AbstractPackage, ParseResult]] = {
     val parseManager = new ParseManager(config, executionContext)
     /*
     parseManager.parse(pkgInfo)
     val res = parseManager.getParseResults(executionContext).left.map(errMap => errMap.values.flatten.toVector)
     res
     */
     val res = parseManager.parse(pkgInfo)
-    res.map(_ => parseManager.getSuccessResults(executionContext))
+    res.map(_ => parseManager.getResults(executionContext))
   }
 
   def parse(input: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean = false)(config: Config): Either[Vector[VerifierError], PPackage] = {

src/main/scala/viper/gobra/frontend/info/Info.scala

@@ -13,11 +13,12 @@ import org.bitbucket.inkytonik.kiama.util.{Position, Source}
 import viper.gobra.ast.frontend.{PImport, PNode, PPackage}
 import viper.gobra.frontend.{Config, Job, TaskManager}
 import viper.gobra.frontend.PackageResolver.{AbstractImport, AbstractPackage, BuiltInImport, BuiltInPackage, RegularImport}
-import viper.gobra.frontend.Parser.ParseSuccessResult
+import viper.gobra.frontend.Parser.{ParseResult, ParseSuccessResult}
 import viper.gobra.frontend.TaskManagerMode.{Lazy, Parallel, Sequential}
+import viper.gobra.frontend.info.Info.CycleChecker
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.typing.ghost.separation.{GhostLessPrinter, GoifyingPrinter}
-import viper.gobra.reporting.{TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, VerifierError}
+import viper.gobra.reporting.{CyclicImportError, ParserError, TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, VerifierError}
 import viper.gobra.util.{GobraExecutionContext, Violation}
 
 import java.security.MessageDigest
@@ -46,24 +47,83 @@ object Info extends LazyLogging {
     */
   case class ImportCycle(importNodeCausingCycle: PImport, importNodeStart: Option[Position], cyclicPackages: Vector[AbstractImport])
 
-  class CycleChecker(val config: Config, val parseResults: Map[AbstractPackage, ParseSuccessResult]) extends GetParseResult {
+  class CycleChecker(val config: Config /*, val parseResults: Map[AbstractPackage, ParseSuccessResult]*/, val parseResults: Map[AbstractPackage, ParseResult]) {
     /** keeps track of the package dependencies that are currently resolved. This information is used to detect cycles */
     private var parserPendingPackages: Vector[AbstractImport] = Vector()
 
-    def check(abstractPackage: AbstractPackage): Messages = {
+    private def getParseResult(abstractPackage: AbstractPackage): Either[Vector[ParserError], ParseSuccessResult] = {
+      Violation.violation(parseResults.contains(abstractPackage), s"GetParseResult: expects that $abstractPackage has been parsed")
+      parseResults(abstractPackage)
+    }
+
+    def check(abstractPackage: AbstractPackage): Either[Vector[VerifierError], Map[AbstractPackage, ParseSuccessResult]] = {
+      for {
+        parseResult <- getParseResult(abstractPackage)
+        (_, ast) = parseResult
+        perImportResult = ast.imports.map(importNode => {
+          // val cycles = getCycles(RegularImport(importNode.importPath))
+          /*
+          val cycles = getImportErrors(RegularImport(importNode.importPath))
+          val msgs = createImportError(importNode, cycles)
+          if (msgs.isEmpty) Right(()) else Left(ast.positions.translate(msgs, TypeError).distinct)
+           */
+          val res = getImportErrors(RegularImport(importNode.importPath))
+            .left
+            .map(errs => {
+              val msgs = createImportError(importNode, errs)
+              ast.positions.translate(msgs, TypeError).distinct
+            })
+          res
+        })
+        (errs, _) = perImportResult.partitionMap(identity)
+        _ <- if (errs.nonEmpty) Left(errs.flatten) else Right(())
+        successParseResults = parseResults.collect {
+          case (key, Right(res)) => (key, res)
+        }
+      } yield successParseResults
+      /*
       val (_, ast) = getParseResult(abstractPackage)
-      ast.imports.flatMap(importNode => {
+      val msgs = ast.imports.flatMap(importNode => {
         val cycles = getCycles(RegularImport(importNode.importPath))
         createImportError(importNode, cycles)
       })
+      if (msgs.isEmpty) {
+
+      } else {
+        Left(ast.positions.translate(msgs, TypeError).distinct)
+      }
+      */
     }
 
     /**
       * returns all parser errors and cyclic errors transitively found in imported packages
       */
-    private def getCycles(importTarget: AbstractImport): Vector[ImportCycle] = {
+    private def getImportErrors(importTarget: AbstractImport): Either[Vector[VerifierError], Unit] = {
       parserPendingPackages = parserPendingPackages :+ importTarget
       val abstractPackage = AbstractPackage(importTarget)(config)
+      val res = for {
+        parseResult <- getParseResult(abstractPackage)
+        (_, ast) = parseResult
+        perImportResult = ast.imports.map(importNode => {
+          val directlyImportedTarget = RegularImport(importNode.importPath)
+          if (parserPendingPackages.contains(directlyImportedTarget)) {
+            // package cycle detected
+            val importNodeStart = ast.positions.positions.getStart(importNode)
+            // Vector(ImportCycle(importNode, importNodeStart, parserPendingPackages))
+            val msg = s"Package '$importTarget' is part of the following import cycle that involves the import $importNode$importNodeStart: ${parserPendingPackages.mkString("[", ", ", "]")}"
+            Left(Vector(CyclicImportError(s"Cyclic package import detected starting with package '$msg'")))
+          } else {
+            getImportErrors(directlyImportedTarget)
+          }
+        })
+        (errs, _) = perImportResult.partitionMap(identity)
+        res <- if (errs.nonEmpty) Left(errs.flatten) else Right(())
+      } yield res
+      parserPendingPackages = parserPendingPackages.filterNot(_ == importTarget)
+      res
+    }
+      /*
+    private def getCycles(importTarget: AbstractImport): Vector[ImportCycle] = {
       val (_, ast) = getParseResult(abstractPackage)
       val res = ast.imports.flatMap(importNode => {
         val directlyImportedTarget = RegularImport(importNode.importPath)
@@ -78,13 +138,28 @@ object Info extends LazyLogging {
       parserPendingPackages = parserPendingPackages.filterNot(_ == importTarget)
       res
     }
+       */
 
-    private def createImportError(importNode: PImport, cycles: Vector[ImportCycle]): Messages = {
+    private def createImportError(importNode: PImport, errorsInImportedPackage: Vector[VerifierError]): Messages = {
       val importTarget = RegularImport(importNode.importPath)
+      val (cyclicErrors, nonCyclicErrors) = errorsInImportedPackage.partitionMap {
+        case cyclicErr: CyclicImportError => Left(cyclicErr)
+        case e => Right(e)
+      }
+      if (cyclicErrors.isEmpty) {
+        // nonCyclicErrors.flatMap(err => message(importNode, err.message))
+        message(importNode, s"Package contains ${nonCyclicErrors.length} error(s): ${nonCyclicErrors.map(_.message).mkString(", ")}")
+      } else {
+        cyclicErrors.flatMap(cycle => {
+          // val positionalInfo = cycle.importNodeStart.map(pos => s" at ${pos.format}").getOrElse("")
+          // message(importNode, s"Package '$importTarget' is part of the following import cycle that involves the import ${cycle.importNodeCausingCycle}$positionalInfo: ${cycle.cyclicPackages.mkString("[", ", ", "]")}")
+          message(importNode, cycle.message)
+        })
+      }/*
       cycles.flatMap(cycle => {
         val positionalInfo = cycle.importNodeStart.map(pos => s" at ${pos.format}").getOrElse("")
         message(importNode, s"Package '$importTarget' is part of the following import cycle that involves the import ${cycle.importNodeCausingCycle}$positionalInfo: ${cycle.cyclicPackages.mkString("[", ", ", "]")}")
-      })
+      })*/
     }
   }
 
@@ -99,10 +174,11 @@ object Info extends LazyLogging {
     trait TypeCheckJob {
       protected def typeCheck(pkgSources: Vector[Source], pkg: PPackage, dependentTypeInfo: DependentTypeInfo, isMainContext: Boolean = false): TypeCheckResult = {
         val startMs = System.currentTimeMillis()
+        logger.trace(s"start type-checking ${pkg.info.id}")
         val res = Info.checkSources(pkgSources, pkg, dependentTypeInfo, isMainContext = isMainContext)(config)
         logger.trace {
           val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
-          s"type-checking ${pkg.info.id} done (took ${durationS}s)"
+          s"type-checking ${pkg.info.id} done (took ${durationS}s with ${res.map(info => info.tree.nodes.length.toString).getOrElse("_")} nodes)"
         }
         res
       }
@@ -233,9 +309,28 @@ object Info extends LazyLogging {
     */
   }
 
-  def check(config: Config, abstractPackage: AbstractPackage, parseResults: Map[AbstractPackage, ParseSuccessResult])(executionContext: GobraExecutionContext): TypeCheckResult = {
+  def check(config: Config, abstractPackage: AbstractPackage, /*parseResults: Map[AbstractPackage, ParseSuccessResult]*/ parseResults: Map[AbstractPackage, ParseResult])(executionContext: GobraExecutionContext): TypeCheckResult = {
     // check for cycles
-    val cyclicErrors = new CycleChecker(config, parseResults).check(abstractPackage)
+    // val cyclicErrors = new CycleChecker(config, parseResults).check(abstractPackage)
+    for {
+      successParseResult <- new CycleChecker(config, parseResults).check(abstractPackage)
+        .left.map(errs => {
+          val (sources, pkg) = parseResults(abstractPackage).right.get
+          val sourceNames = sources.map(_.name)
+          config.reporter report TypeCheckFailureMessage(sourceNames, pkg.packageClause.id.name, () => pkg, errs)
+          errs
+        })
+      typeCheckingStartMs = System.currentTimeMillis()
+      context = new Context(config, successParseResult)(executionContext)
+      typeInfo <- context.typeCheck(abstractPackage)
+      _ = logger.debug {
+        val durationS = f"${(System.currentTimeMillis() - typeCheckingStartMs) / 1000f}%.1f"
+        s"type-checking done, took ${durationS}s (in mode ${config.typeCheckMode})"
+      }
+    } yield typeInfo
+
+
+    /*
     if (cyclicErrors.isEmpty) {
       val typeCheckingStartMs = System.currentTimeMillis()
       // add type-checking jobs to context:
@@ -254,6 +349,7 @@ object Info extends LazyLogging {
       config.reporter report TypeCheckFailureMessage(sourceNames, pkg.packageClause.id.name, () => pkg, errors)
       Left(errors)
     }
+     */
   }
 
   type TypeInfoCacheKey = String

src/test/resources/regressions/features/import/import-fail2.gobra

@@ -7,6 +7,6 @@ package main
 
 import (
     // note that package `parse_error` contains a parser error so the qualifier cannot be resolved
-    //:: ExpectedOutput(parser_error)
+    //:: ExpectedOutput(type_error)
     "parse_error"
 )

src/test/resources/regressions/features/import/import1.gobra

@@ -4,27 +4,27 @@
 package main
 
 import fmt "fmt"
-//:: ExpectedOutput(not_found_error)
+//:: ExpectedOutput(parser_error)
 import a "a";
-//:: ExpectedOutput(not_found_error)
+//:: ExpectedOutput(parser_error)
 import (b "b")
-//:: ExpectedOutput(not_found_error)
+//:: ExpectedOutput(parser_error)
 import (c "c");
 import (
-    //:: ExpectedOutput(not_found_error)
+    //:: ExpectedOutput(parser_error)
     d "d"
-    //:: ExpectedOutput(not_found_error)
+    //:: ExpectedOutput(parser_error)
     e "e")
 import (
-    //:: ExpectedOutput(not_found_error)
+    //:: ExpectedOutput(parser_error)
     f "f"
-    //:: ExpectedOutput(not_found_error)
+    //:: ExpectedOutput(parser_error)
     g "g"
 )
 
-//:: ExpectedOutput(not_found_error)
+//:: ExpectedOutput(parser_error)
 import m "lib/mathm" // wrong package name used on purpose such that this test case does not potentially depend on the configured Go path
-//:: ExpectedOutput(not_found_error)
+//:: ExpectedOutput(parser_error)
 import . "lib/mathn"
 
 func test() {

src/test/resources/regressions/features/import/import2.gobra

@@ -3,7 +3,7 @@
 
 package main
 
-//:: ExpectedOutput(not_found_error)
+//:: ExpectedOutput(parser_error)
 import math "lib/mathm" // wrong package name used on purpose such that this test case does not potentially depend on the configured Go path
 
 type cell struct{