More robust config creation (#824)

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

@@ -224,7 +224,7 @@ class Gobra extends GoVerifier with GoIdeVerifier {
       }
     })
     val (errors, inFileConfigs) = inFileEitherConfigs.partitionMap(identity)
-    if (errors.nonEmpty) Left(errors.map(ConfigError))
+    if (errors.nonEmpty) Left(errors.flatten)
     else {
       // start with original config `config` and merge in every in file config:
       val mergedConfig = inFileConfigs.flatten.foldLeft(config) {
@@ -349,8 +349,8 @@ object GobraRunner extends GobraFrontend with StrictLogging {
       val scallopGobraConfig = new ScallopGobraConfig(args.toSeq)
       val config = scallopGobraConfig.config
       exitCode = config match {
-        case Left(validationError) =>
-          logger.error(validationError)
+        case Left(errors) =>
+          errors.foreach(err => logger.error(err.formattedMessage))
           1
         case Right(config) =>
           // Print copyright report

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

@@ -17,7 +17,7 @@ import viper.gobra.GoVerifier
 import viper.gobra.frontend.PackageResolver.FileResource
 import viper.gobra.frontend.Source.getPackageInfo
 import viper.gobra.util.TaskManagerMode.{Lazy, Parallel, Sequential, TaskManagerMode}
-import viper.gobra.reporting.{FileWriterReporter, GobraReporter, StdIOReporter}
+import viper.gobra.reporting.{ConfigError, FileWriterReporter, GobraReporter, StdIOReporter, VerifierError}
 import viper.gobra.util.{TaskManagerMode, TypeBounds, Violation}
 import viper.silver.ast.SourcePosition
 
@@ -317,8 +317,8 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
 }
 
 trait RawConfig {
-  /** converts a RawConfig to an actual `Config` for Gobra. Returns Left with an error message if validation fails. */
-  def config: Either[String, Config]
+  /** converts a RawConfig to an actual `Config` for Gobra. Returns Left if validation fails. */
+  def config: Either[Vector[VerifierError], Config]
   protected def baseConfig: BaseConfig
 
   protected def createConfig(packageInfoInputMap: Map[PackageInfo, Vector[Source]]): Config = Config(
@@ -370,20 +370,22 @@ trait RawConfig {
   * This is for example used when parsing in-file configs.
   */
 case class NoInputModeConfig(baseConfig: BaseConfig) extends RawConfig {
-  override lazy val config: Either[String, Config] = Right(createConfig(Map.empty))
+  override lazy val config: Either[Vector[VerifierError], Config] = Right(createConfig(Map.empty))
 }
 
 case class FileModeConfig(inputFiles: Vector[Path], baseConfig: BaseConfig) extends RawConfig {
-  override lazy val config: Either[String, Config] = {
+  override lazy val config: Either[Vector[VerifierError], Config] = {
     val sources = inputFiles.map(path => FileSource(path.toString))
-    if (sources.isEmpty) Left(s"no input files have been provided")
+    if (sources.isEmpty) Left(Vector(ConfigError(s"no input files have been provided")))
     else {
       // we do not check whether the provided files all belong to the same package
       // instead, we trust the programmer that she knows what she's doing.
       // If they do not belong to the same package, Gobra will report an error after parsing.
       // we simply use the first source's package info to create a single map entry:
-      val packageInfoInputMap = Map(getPackageInfo(sources.head, inputFiles.head) -> sources)
-      Right(createConfig(packageInfoInputMap))
+      for {
+        pkgInfo <- getPackageInfo(sources.head, inputFiles.head)
+        packageInfoInputMap = Map(pkgInfo -> sources)
+      } yield createConfig(packageInfoInputMap)
     }
   }
 }
@@ -402,38 +404,49 @@ trait PackageAndRecursiveModeConfig extends RawConfig {
 
 case class PackageModeConfig(projectRoot: Path = ConfigDefaults.DefaultProjectRoot.toPath,
                              inputDirectories: Vector[Path], baseConfig: BaseConfig) extends PackageAndRecursiveModeConfig {
-  override lazy val config: Either[String, Config] = {
+  override lazy val config: Either[Vector[VerifierError], Config] = {
     val (errors, mappings) = inputDirectories.map { directory =>
       val sources = getSources(directory, recursive = false, onlyFilesWithHeader = baseConfig.onlyFilesWithHeader)
       // we do not check whether the provided files all belong to the same package
       // instead, we trust the programmer that she knows what she's doing.
       // If they do not belong to the same package, Gobra will report an error after parsing.
       // we simply use the first source's package info to create a single map entry:
-      if (sources.isEmpty) Left(s"no sources found in directory ${directory}")
-      else Right((getPackageInfo(sources.head, projectRoot), sources))
+      if (sources.isEmpty) Left(Vector(ConfigError(s"no sources found in directory $directory")))
+      else for {
+        pkgInfo <- getPackageInfo(sources.head, projectRoot)
+      } yield pkgInfo -> sources
     }.partitionMap(identity)
-    if (errors.length == 1) Left(errors.head)
-    else if (errors.nonEmpty) Left(s"multiple errors have been found while localizing sources: ${errors.mkString(", ")}")
-    else Right(createConfig(mappings.toMap))
+    if (errors.nonEmpty) {
+        Left(errors.flatten)
+    } else {
+        Right(createConfig(mappings.toMap))
+    }
   }
 }
 
 case class RecursiveModeConfig(projectRoot: Path = ConfigDefaults.DefaultProjectRoot.toPath,
                                includePackages: List[String] = ConfigDefaults.DefaultIncludePackages,
                                excludePackages: List[String] = ConfigDefaults.DefaultExcludePackages,
                                baseConfig: BaseConfig) extends PackageAndRecursiveModeConfig {
-  override lazy val config: Either[String, Config] = {
-    val pkgMap = getSources(projectRoot, recursive = true, onlyFilesWithHeader = baseConfig.onlyFilesWithHeader)
-      .groupBy(source => getPackageInfo(source, projectRoot))
-      // filter packages:
-      .filter { case (pkgInfo, _) => (includePackages.isEmpty || includePackages.contains(pkgInfo.name)) && !excludePackages.contains(pkgInfo.name) }
-      // filter packages with zero source files:
-      .filter { case (_, pkgFiles) => pkgFiles.nonEmpty }
-    if (pkgMap.isEmpty) {
-      Left(s"No packages have been found that should be verified")
-    } else {
-      Right(createConfig(pkgMap))
-    }
+  override lazy val config: Either[Vector[VerifierError], Config] = {
+    val sources = getSources(projectRoot, recursive = true, onlyFilesWithHeader = baseConfig.onlyFilesWithHeader)
+    val (errors, pkgInfos) = sources.map(source => {
+      for {
+        pkgInfo <- getPackageInfo(source, projectRoot)
+      } yield source -> pkgInfo
+    }).partitionMap(identity)
+    for {
+      pkgInfos <- if (errors.nonEmpty) Left(errors.flatten) else Right(pkgInfos)
+      pkgMap = pkgInfos
+        .groupBy { case (_, pkgInfo) => pkgInfo }
+        // we no longer need `pkgInfo` for the values:
+        .transform { case (_, values) => values.map(_._1) }
+        // filter packages:
+        .filter { case (pkgInfo, _) => (includePackages.isEmpty || includePackages.contains(pkgInfo.name)) && !excludePackages.contains(pkgInfo.name) }
+        // filter packages with zero source files:
+        .filter { case (_, pkgFiles) => pkgFiles.nonEmpty }
+      nonEmptyPkgMap <- if (pkgMap.isEmpty) Left(Vector(ConfigError(s"No packages have been found that should be verified"))) else Right(pkgMap)
+    } yield createConfig(nonEmptyPkgMap)
   }
 }
 
@@ -968,7 +981,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
 
   verify()
 
-  lazy val config: Either[String, Config] = rawConfig.config
+  lazy val config: Either[Vector[VerifierError], Config] = rawConfig.config
 
   // note that we use `recursive.isSupplied` instead of `recursive.toOption` because it defaults to `Some(false)` if it
   // was not provided by the user. Specifying a different default value does not seem to be respected.

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

@@ -11,7 +11,7 @@ import org.bitbucket.inkytonik.kiama.rewriting.{Cloner, PositionedRewriter, Stra
 import org.bitbucket.inkytonik.kiama.util.{Positions, Source}
 import org.bitbucket.inkytonik.kiama.util.Messaging.{error, message}
 import viper.gobra.ast.frontend._
-import viper.gobra.frontend.Source.{FromFileSource, TransformableSource}
+import viper.gobra.frontend.Source.{FromFileSource, TransformableSource, getPackageInfo}
 import viper.gobra.reporting.{Source => _, _}
 import org.antlr.v4.runtime.{CharStreams, CommonTokenStream, DefaultErrorStrategy, ParserRuleContext}
 import org.antlr.v4.runtime.atn.PredictionMode
@@ -34,7 +34,7 @@ object Parser extends LazyLogging {
 
   type ParseSuccessResult = (Vector[Source], PPackage)
   type ParseResult = Either[Vector[ParserError], ParseSuccessResult]
-  type ImportToSourceOrErrorMap = Vector[(AbstractPackage, Either[Vector[ParserError], Vector[Source]])]
+  type ImportToPkgInfoOrErrorMap = Vector[(AbstractPackage, Either[Vector[ParserError], (Vector[Source], PackageInfo)])]
   type PreprocessedSources = Vector[Source]
 
   class ParseManager(config: Config)(implicit executor: GobraExecutionContext) extends LazyLogging {
@@ -53,7 +53,7 @@ object Parser extends LazyLogging {
       def pkgInfo: PackageInfo
 
       type ImportErrorFactory = String => Vector[ParserError]
-      protected def getImports(importNodes: Vector[PImport], pom: PositionManager): ImportToSourceOrErrorMap = {
+      protected def getImports(importNodes: Vector[PImport], pom: PositionManager): ImportToPkgInfoOrErrorMap = {
         val explicitImports: Vector[(AbstractImport, ImportErrorFactory)] = importNodes
           .map(importNode => {
             val importErrorFactory: ImportErrorFactory = (errMsg: String) => {
@@ -74,13 +74,13 @@ object Parser extends LazyLogging {
 
         val errsOrSources = imports.map { case (directImportTarget, importErrorFactory) =>
           val directImportPackage = AbstractPackage(directImportTarget)(config)
-          val nonEmptyImportedSources = for {
-            resolveSourceResults <- PackageResolver.resolveSources(directImportTarget)(config)
+          val sourcesAndPkgInfo = for {
+            resolveSourceResults <- PackageResolver.resolveSources(directImportTarget)(config).left.map(importErrorFactory)
             importedSources = resolveSourceResults.map(_.source)
-            nonEmptyImportedSources <- if (importedSources.isEmpty) Left(s"No source files for package '$directImportTarget' found") else Right(importedSources)
-          } yield nonEmptyImportedSources
-          val res = nonEmptyImportedSources.left.map(importErrorFactory)
-          (directImportPackage, res)
+            nonEmptyImportedSources <- if (importedSources.isEmpty) Left(importErrorFactory(s"No source files for package '$directImportTarget' found")) else Right(importedSources)
+            pkgInfo <- getPackageInfo(nonEmptyImportedSources.head, config.projectRoot)
+          } yield (nonEmptyImportedSources, pkgInfo)
+          (directImportPackage, sourcesAndPkgInfo)
         }
         errsOrSources
       }
@@ -99,7 +99,7 @@ object Parser extends LazyLogging {
       def specOnly: Boolean
       var preambleParsingDurationMs: Long = 0
 
-      private def getImportsForPackage(preprocessedSources: Vector[Source]): ImportToSourceOrErrorMap = {
+      private def getImportsForPackage(preprocessedSources: Vector[Source]): ImportToPkgInfoOrErrorMap = {
         val preambles = preprocessedSources
           .map(preprocessedSource => processPreamble(preprocessedSource)(config))
           // we ignore imports in files that cannot be parsed:
@@ -115,8 +115,8 @@ object Parser extends LazyLogging {
 
         // add imported packages to manager if not already
         imports.foreach {
-          case (directImportPackage, Right(nonEmptySources)) =>
-            manager.addIfAbsent(directImportPackage, ParseSourcesJob(nonEmptySources, directImportPackage))
+          case (directImportPackage, Right((nonEmptySources, pkgInfo))) =>
+            manager.addIfAbsent(directImportPackage, ParseSourcesJob(nonEmptySources, pkgInfo))
           case (directImportPackage, Left(errs)) =>
             manager.addIfAbsent(directImportPackage, ParseFailureJob(errs))
         }
@@ -148,9 +148,8 @@ object Parser extends LazyLogging {
     }
 
     /** this job is used to parse all packages that are imported */
-    private case class ParseSourcesJob(override val pkgSources: Vector[Source], pkg: AbstractPackage) extends ParseJob {
+    private case class ParseSourcesJob(override val pkgSources: Vector[Source], override val pkgInfo: PackageInfo) extends ParseJob {
       require(pkgSources.nonEmpty)
-      lazy val pkgInfo: PackageInfo = Source.getPackageInfo(pkgSources.head, config.projectRoot)
       lazy val specOnly: Boolean = true
     }
 

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

@@ -8,12 +8,12 @@ package viper.gobra.frontend
 
 import java.io.Reader
 import java.nio.file.{Files, Path, Paths}
-
 import org.bitbucket.inkytonik.kiama.util.{FileSource, Filenames, IO, Source, StringSource}
+import viper.gobra.reporting.ParserError
 import viper.gobra.util.Violation
 import viper.silver.ast.SourcePosition
-import java.util.Objects
 
+import java.util.Objects
 import viper.gobra.translator.Names
 
 import scala.io.BufferedSource
@@ -51,31 +51,40 @@ object Source {
   /**
    * Returns an object containing information about the package a source belongs to.
    */
-  def getPackageInfo(src: Source, projectRoot: Path): PackageInfo = {
-
-    val isBuiltIn: Boolean = src match {
+  def getPackageInfo(src: Source, projectRoot: Path): Either[Vector[ParserError], PackageInfo] = {
+    val isBuiltIn = src match {
       case FromFileSource(_, _, builtin) => builtin
       case _ => false
     }
-
-    val packageName: String = PackageResolver.getPackageClause(src: Source)
-      .getOrElse(Violation.violation("Missing package clause in " + src.name))
-
-    /**
-     * A unique identifier for packages
-     */
-    val packageId: String = {
-      val prefix = uniquePath(TransformableSource(src).toPath.toAbsolutePath.getParent, projectRoot).toString
-      if(prefix.nonEmpty) {
-        // The - is enough to unambiguously separate the prefix from the package name, since it can't occur in the package name
-        // per Go's spec (https://go.dev/ref/spec#Package_clause)
-        prefix + " - " + packageName
-      } else {
-        // Fallback case if the prefix is empty, for example if the directory of a FileSource is in the current directory
-        packageName
+    val packageNameOrError = PackageResolver.getPackageClause(src).toRight({
+      val pos = Some(SourcePosition(src.toPath, 1, 1))
+      Vector(ParserError("Missing package clause", pos))
+    })
+    for {
+      packageName <- packageNameOrError
+      /** A unique identifier for packages */
+      packageId = {
+        val prefix = uniquePath(TransformableSource(src).toPath.toAbsolutePath.getParent, projectRoot).toString
+        if(prefix.nonEmpty) {
+          // The - is enough to unambiguously separate the prefix from the package name, since it can't occur in the package name
+          // per Go's spec (https://go.dev/ref/spec#Package_clause)
+          prefix + " - " + packageName
+        } else {
+          // Fallback case if the prefix is empty, for example if the directory of a FileSource is in the current directory
+          packageName
+        }
       }
-    }
-    new PackageInfo(packageId, packageName, isBuiltIn)
+    } yield new PackageInfo(packageId, packageName, isBuiltIn)
+  }
+
+  /**
+    * Forcefully tries to create a package info or throws an runtime exception.
+    * Only used for unit tests
+    */
+  def getPackageInfoOrCrash(src: Source, projectRoot: Path): PackageInfo = {
+    Source.getPackageInfo(src, projectRoot).fold(
+      errs => Violation.violation(s"Creating package info failed: ${errs.map(_.formattedMessage).mkString(", ")}"),
+      identity)
   }
 
   /**

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

@@ -19,7 +19,7 @@ import viper.gobra.frontend.Parser.{ParseResult, ParseSuccessResult}
 import viper.gobra.util.TaskManagerMode.{Lazy, Parallel, Sequential}
 import viper.gobra.frontend.info.implementation.TypeInfoImpl
 import viper.gobra.frontend.info.implementation.typing.ghost.separation.{GhostLessPrinter, GoifyingPrinter}
-import viper.gobra.reporting.{CyclicImportError, ParserError, TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, VerifierError}
+import viper.gobra.reporting.{CyclicImportError, TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, VerifierError}
 import viper.gobra.util.{GobraExecutionContext, Job, TaskManager, Violation}
 
 import java.security.MessageDigest
@@ -48,7 +48,7 @@ object Info extends LazyLogging {
     /** keeps track of the package dependencies that are currently resolved. This information is used to detect cycles */
     private var parserPendingPackages: Vector[AbstractImport] = Vector()
 
-    private def getParseResult(abstractPackage: AbstractPackage): Either[Vector[ParserError], ParseSuccessResult] = {
+    private def getParseResult(abstractPackage: AbstractPackage): ParseResult = {
       Violation.violation(parseResults.contains(abstractPackage), s"GetParseResult: expects that $abstractPackage has been parsed")
       parseResults(abstractPackage)
     }

src/test/scala/viper/gobra/GobraPackageTests.scala

@@ -69,7 +69,7 @@ class GobraPackageTests extends GobraTests {
           ))
         } yield config
 
-        val pkgInfo = Source.getPackageInfo(FromFileSource(input.files.head), currentDir)
+        val pkgInfo = Source.getPackageInfoOrCrash(FromFileSource(input.files.head), currentDir)
 
         val config = Config(
           logLevel = Level.INFO,

src/test/scala/viper/gobra/GobraTests.scala

@@ -52,7 +52,7 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll {
     Config(
       logLevel = Level.INFO,
       reporter = StringifyReporter,
-      packageInfoInputMap = Map(Source.getPackageInfo(source, Path.of("")) -> Vector(source)),
+      packageInfoInputMap = Map(Source.getPackageInfoOrCrash(source, Path.of("")) -> Vector(source)),
       checkConsistency = true,
       cacheParserAndTypeChecker = cacheParserAndTypeChecker,
       z3Exe = z3Exe,

src/test/scala/viper/gobra/parsing/GobraParserTests.scala

@@ -49,12 +49,12 @@ class GobraParserTests extends AbstractGobraTests with BeforeAndAfterAll {
 
       override def run(input: AnnotatedTestInput): Seq[AbstractOutput] = {
 
-        val source = FromFileSource(input.file);
+        val source = FromFileSource(input.file)
 
         val config = Config(
           logLevel = Level.INFO,
           reporter = NoopReporter,
-          packageInfoInputMap = Map(Source.getPackageInfo(source, Path.of("")) -> Vector(source)),
+          packageInfoInputMap = Map(Source.getPackageInfoOrCrash(source, Path.of("")) -> Vector(source)),
           z3Exe = z3Exe,
           shouldTypeCheck = false
         )