Input File Filtering (#434)

* unifies source file search for inputs and imports, fixes filtering of path containing 'testdata'

* implements CR suggestions by Joao

* rewrites handling of CLI options in regards to inputs, fixes parsing file inputs with positional information

* fixes unit tests

* adapts unit tests to new config options

* implements CR suggestions by Joao

* splits CLI parsing into two steps and adds besides the input file and recusive mode a package mode

* fixes verification of empty directories in  mode

* passes actually the  flag to the relevant methods

* fixes 2 bugs where non-text files would be tried to be decoded and read and where we cannot resolve the qualifier for a package

* implements CR suggestions by Joao

* sets log level based on final config

* fixes evaluation of  option

* fixes Gobra to verify entire package if no line numbers are specified

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

@@ -6,9 +6,12 @@
 
 package viper.gobra
 
+import ch.qos.logback.classic.Logger
+
 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, OverflowChecksTransform}
@@ -143,8 +146,9 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     implicit val _executor: GobraExecutionContext = executor
 
     val task = Future {
-      val finalConfig = getAndMergeInFileConfig(config, pkgInfo)
       for {
+        finalConfig <- getAndMergeInFileConfig(config, pkgInfo)
+        _ = setLogLevel(finalConfig)
         parsedPackage <- performParsing(pkgInfo, finalConfig)
         typeInfo <- performTypeChecking(parsedPackage, finalConfig)
         program <- performDesugaring(parsedPackage, typeInfo, finalConfig)
@@ -194,35 +198,44 @@ class Gobra extends GoVerifier with GoIdeVerifier {
     * These in-file command options get combined for all files and passed to ScallopGobraConfig.
     * The current config merged with the newly created config is then returned
     */
-  def getAndMergeInFileConfig(config: Config, pkgInfo: PackageInfo): Config = {
-    val inFileConfigs = config.packageInfoInputMap(pkgInfo).flatMap(input => {
+  def getAndMergeInFileConfig(config: Config, pkgInfo: PackageInfo): Either[Vector[VerifierError], Config] = {
+    val inFileEitherConfigs = config.packageInfoInputMap(pkgInfo).map(input => {
       val content = input.content
       val configs = for (m <- inFileConfigRegex.findAllMatchIn(content)) yield m.group(1)
       if (configs.isEmpty) {
-        None
+        Right(None)
       } else {
         // our current "merge" strategy for potentially different, duplicate, or even contradicting configurations is to concatenate them:
         val args = configs.flatMap(configString => configString.split(" ")).toList
         // skip include dir checks as the include should only be parsed and is not resolved yet based on the current directory
-        val inFileConfig = new ScallopGobraConfig(args, isInputOptional = true, skipIncludeDirChecks = true).config
-        // modify all relative includeDirs such that they are resolved relatively to the current file:
-        val resolvedConfig = inFileConfig.copy(includeDirs = inFileConfig.includeDirs.map(
-          // it's important to convert includeDir to a string first as `path` might be a ZipPath and `includeDir` might not
-          includeDir => Paths.get(input.name).getParent.resolve(includeDir.toString)))
-        Some(resolvedConfig)
+        for {
+          inFileConfig <- new ScallopGobraConfig(args, isInputOptional = true, skipIncludeDirChecks = true).config
+          resolvedConfig = inFileConfig.copy(includeDirs = inFileConfig.includeDirs.map(
+            // it's important to convert includeDir to a string first as `path` might be a ZipPath and `includeDir` might not
+            includeDir => Paths.get(input.name).getParent.resolve(includeDir.toString)))
+        } yield Some(resolvedConfig)
       }
     })
+    val (errors, inFileConfigs) = inFileEitherConfigs.partitionMap(identity)
+    if (errors.nonEmpty) Left(errors.map(ConfigError))
+    else {
+      // start with original config `config` and merge in every in file config:
+      val mergedConfig = inFileConfigs.flatten.foldLeft(config) {
+        case (oldConfig, fileConfig) => oldConfig.merge(fileConfig)
+      }
+      Right(mergedConfig)
+    }
+  }
 
-    // start with original config `config` and merge in every in file config:
-    inFileConfigs.foldLeft(config){ case (oldConfig, fileConfig) => oldConfig.merge(fileConfig) }
+  private def setLogLevel(config: Config): Unit = {
+    LoggerFactory.getLogger(GoVerifier.rootLogger)
+      .asInstanceOf[Logger]
+      .setLevel(config.logLevel)
   }
 
   private def performParsing(pkgInfo: PackageInfo, config: Config): Either[Vector[VerifierError], PPackage] = {
     if (config.shouldParse) {
-      val sourcesToParse = config.packageInfoInputMap(pkgInfo).filter {
-        // only parses sources with header when running in this mode
-        p => !config.onlyFilesWithHeader || Config.sourceHasHeader(p)
-      }
+      val sourcesToParse = config.packageInfoInputMap(pkgInfo)
       Parser.parse(sourcesToParse, pkgInfo)(config)
     } else {
       Left(Vector())
@@ -295,12 +308,17 @@ object GobraRunner extends GobraFrontend with StrictLogging {
     try {
       val scallopGobraConfig = new ScallopGobraConfig(args.toSeq)
       val config = scallopGobraConfig.config
-      // Print copyright report
-      config.reporter report CopyrightReport(s"${GoVerifier.name} ${GoVerifier.version}\n${GoVerifier.copyright}")
-
-      exitCode = verifier.verifyAllPackages(config)(executor) match {
-        case VerifierResult.Failure(_) => 1
-        case _ => 0
+      exitCode = config match {
+        case Left(validationError) =>
+          logger.error(validationError)
+          1
+        case Right(config) =>
+          // Print copyright report
+          config.reporter report CopyrightReport(s"${GoVerifier.name} ${GoVerifier.version}\n${GoVerifier.copyright}")
+          verifier.verifyAllPackages(config)(executor) match {
+            case VerifierResult.Failure(_) => 1
+            case _ => 0
+          }
       }
     } catch {
       case e: UglyErrorMessage =>

src/main/scala/viper/gobra/backend/ViperBackends.scala

@@ -67,7 +67,7 @@ object ViperBackends {
       server.getOrElse({
         var serverConfig = List("--logLevel", config.logLevel.levelStr)
         if(config.cacheFile.isDefined) {
-          serverConfig = serverConfig.appendedAll(List("--cacheFile", config.cacheFile.get))
+          serverConfig = serverConfig.appendedAll(List("--cacheFile", config.cacheFile.get.toString))
         }
 
         val createdServer = new ViperCoreServer(new ViperConfig(serverConfig))(executionContext)