cleanup

build.sbt

@@ -35,6 +35,7 @@ lazy val gobra = (project in file("."))
     libraryDependencies += "org.apache.commons" % "commons-text" % "1.9", // for escaping strings in parser preprocessor
     libraryDependencies += "commons-codec" % "commons-codec" % "1.15", // for obtaining the hex encoding of a string
     libraryDependencies += "org.antlr" % "antlr4-runtime" % "4.12.0",
+    libraryDependencies += "org.scalaz" %% "scalaz-core" % "7.3.7", // used for EitherT
 
     scalacOptions ++= Seq(
       "-encoding", "UTF-8", // Enforce UTF-8, instead of relying on properly set locales

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

@@ -7,11 +7,13 @@
 package viper.gobra
 
 import ch.qos.logback.classic.Logger
+import scalaz.EitherT
 
 import java.nio.file.Paths
 import java.util.concurrent.ExecutionException
 import com.typesafe.scalalogging.StrictLogging
 import org.slf4j.LoggerFactory
+import scalaz.Scalaz.futureInstance
 import viper.gobra.ast.internal.Program
 import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, ConstantPropagation, InternalTransform, OverflowChecksTransform}
 import viper.gobra.backend.BackendVerifier
@@ -28,7 +30,6 @@ 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 {
@@ -142,7 +143,7 @@ trait GoVerifier extends StrictLogging {
     if (allErrors.isEmpty) VerifierResult.Success else VerifierResult.Failure(allErrors)
   }
 
-  protected[this] def verify(pkgInfo: PackageInfo, config: Config)(executor: GobraExecutionContext): Future[VerifierResult]
+  protected[this] def verify(pkgInfo: PackageInfo, config: Config)(implicit executor: GobraExecutionContext): Future[VerifierResult]
 }
 
 trait GoIdeVerifier {
@@ -151,27 +152,23 @@ trait GoIdeVerifier {
 
 class Gobra extends GoVerifier with GoIdeVerifier {
 
-  override def verify(pkgInfo: PackageInfo, config: Config)(executor: GobraExecutionContext): Future[VerifierResult] = {
-    // directly declaring the parameter implicit somehow does not work as the compiler is unable to spot the inheritance
-    implicit val _executor: GobraExecutionContext = executor
-
-    val task = Future {
-      for {
-        finalConfig <- getAndMergeInFileConfig(config, pkgInfo)
-        _ = setLogLevel(finalConfig)
-        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)
-    }
-
-    task.flatMap{
-      case Left(Vector()) => Future(VerifierResult.Success)
-      case Left(errors)   => Future(VerifierResult.Failure(errors))
-      case Right((job, finalConfig)) => performVerification(finalConfig, pkgInfo, job.program,  job.backtrack)(executor)
-    }
+  override def verify(pkgInfo: PackageInfo, config: Config)(implicit executor: GobraExecutionContext): Future[VerifierResult] = {
+    val task = for {
+      finalConfig <- EitherT.fromEither(Future.successful(getAndMergeInFileConfig(config, pkgInfo)))
+      _ = setLogLevel(finalConfig)
+      parseResults <- performParsing(finalConfig, pkgInfo)
+      typeInfo <- performTypeChecking(finalConfig, pkgInfo, parseResults)
+      program <- performDesugaring(finalConfig, typeInfo)
+      program <- performInternalTransformations(finalConfig, pkgInfo, program)
+      viperTask <- performViperEncoding(finalConfig, pkgInfo, program)
+    } yield (viperTask, finalConfig)
+
+    task.foldM({
+      case Vector() => Future(VerifierResult.Success)
+      case errors => Future(VerifierResult.Failure(errors))
+    }, {
+      case (job, finalConfig) => performVerification(finalConfig, pkgInfo, job.program,  job.backtrack)
+    })
   }
 
   override def verifyAst(config: Config, pkgInfo: PackageInfo, ast: vpr.Program, backtrack: BackTranslator.BackTrackInfo)(executor: GobraExecutionContext): Future[VerifierResult] = {
@@ -245,47 +242,47 @@ class Gobra extends GoVerifier with GoIdeVerifier {
 
   // returns `Left(...)` if parsing of the package identified by `pkgInfo` failed. Note that `Right(...)` does not imply
   // that all imported packages have been parsed successfully (this is only checked during type-checking)
-  private def performParsing(config: Config, pkgInfo: PackageInfo)(executor: GobraExecutionContext): Either[Vector[VerifierError], Map[AbstractPackage, ParseResult]] = {
+  private def performParsing(config: Config, pkgInfo: PackageInfo)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, Map[AbstractPackage, ParseResult]] = {
     if (config.shouldParse) {
       val startMs = System.currentTimeMillis()
-      val res = Parser.parse(config, pkgInfo)(executor)
+      val res = Parser.parse(config, pkgInfo)
       logger.debug {
         val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
         s"parser phase done, took ${durationS}s"
       }
       res
     } else {
-      Left(Vector.empty)
+      EitherT.left(Vector.empty)
     }
   }
 
-  private def performTypeChecking(config: Config, pkgInfo: PackageInfo, parseResults: Map[AbstractPackage, ParseResult])(executor: GobraExecutionContext): Either[Vector[VerifierError], TypeInfo] = {
+  private def performTypeChecking(config: Config, pkgInfo: PackageInfo, parseResults: Map[AbstractPackage, ParseResult])(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, TypeInfo] = {
     if (config.shouldTypeCheck) {
-      Info.check(config, RegularPackage(pkgInfo.id), parseResults)(executor)
+      Info.check(config, RegularPackage(pkgInfo.id), parseResults)
     } else {
-      Left(Vector())
+      EitherT.left(Vector.empty)
     }
   }
 
-  private def performDesugaring(config: Config, typeInfo: TypeInfo)(executor: GobraExecutionContext): Either[Vector[VerifierError], Program] = {
+  private def performDesugaring(config: Config, typeInfo: TypeInfo)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, Program] = {
     if (config.shouldDesugar) {
       val startMs = System.currentTimeMillis()
-      val res = Right(Desugar.desugar(config, typeInfo)(executor))
+      val res = EitherT.right[Vector[VerifierError], Future, Program](Desugar.desugar(config, typeInfo)(executor))
       logger.debug {
         val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
         s"desugaring done, took ${durationS}s"
       }
       res
     } else {
-      Left(Vector())
+      EitherT.left(Vector.empty)
     }
   }
 
   /**
     * 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(config: Config, pkgInfo: PackageInfo, program: Program)(@unused executor: GobraExecutionContext): Either[Vector[VerifierError], Program] = {
+  private def performInternalTransformations(config: Config, pkgInfo: PackageInfo, program: Program)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, 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.
@@ -300,24 +297,24 @@ class Gobra extends GoVerifier with GoIdeVerifier {
       s"internal transformations done, took ${durationS}s"
     }
     config.reporter.report(AppliedInternalTransformsMessage(config.packageInfoInputMap(pkgInfo).map(_.name), () => result))
-    Right(result)
+    EitherT.right(result)
   }
 
-  private def performViperEncoding(config: Config, pkgInfo: PackageInfo, program: Program)(@unused executor: GobraExecutionContext): Either[Vector[VerifierError], BackendVerifier.Task] = {
+  private def performViperEncoding(config: Config, pkgInfo: PackageInfo, program: Program)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, BackendVerifier.Task] = {
     if (config.shouldViperEncode) {
       val startMs = System.currentTimeMillis()
-      val res = Right(Translator.translate(program, pkgInfo)(config))
+      val res = EitherT.right[Vector[VerifierError], Future, BackendVerifier.Task](Translator.translate(program, pkgInfo)(config))
       logger.debug {
         val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f"
         s"Viper encoding done, took ${durationS}s"
       }
       res
     } else {
-      Left(Vector())
+      EitherT.left(Vector.empty)
     }
   }
 
-  private def performVerification(config: Config, pkgInfo: PackageInfo, ast: vpr.Program, backtrack: BackTranslator.BackTrackInfo)(executor: GobraExecutionContext): Future[VerifierResult] = {
+  private def performVerification(config: Config, pkgInfo: PackageInfo, ast: vpr.Program, backtrack: BackTranslator.BackTrackInfo)(implicit executor: GobraExecutionContext): Future[VerifierResult] = {
     if (config.noVerify) {
       Future(VerifierResult.Success)(executor)
     } else {

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

@@ -54,7 +54,7 @@ object ConfigDefaults {
   lazy val DefaultInt32bit: Boolean = false
   // the following option is currently not controllable via CLI as it is meaningless without a constantly
   // running JVM. It is targeted in particular to Gobra Server and Gobra IDE
-  lazy val DefaultCacheParser: Boolean = false
+  lazy val DefaultCacheParserAndTypeChecker: Boolean = false
   // this option introduces a mode where Gobra only considers files with a specific annotation ("// +gobra").
   // this is useful when verifying large packages where some files might use some unsupported feature of Gobra,
   // or when the goal is to gradually verify part of a package without having to provide an explicit list of the files
@@ -69,7 +69,7 @@ object ConfigDefaults {
   lazy val DefaultEnableLazyImports: Boolean = false
   lazy val DefaultNoVerify: Boolean = false
   lazy val DefaultNoStreamErrors: Boolean = false
-  lazy val DefaultTypeCheckMode: TaskManagerMode = TaskManagerMode.Parallel
+  lazy val DefaultParseAndTypeCheckMode: TaskManagerMode = TaskManagerMode.Parallel
 }
 
 case class Config(
@@ -105,7 +105,7 @@ case class Config(
                    int32bit: Boolean = ConfigDefaults.DefaultInt32bit,
                    // the following option is currently not controllable via CLI as it is meaningless without a constantly
                    // running JVM. It is targeted in particular to Gobra Server and Gobra IDE
-                   cacheParser: Boolean = ConfigDefaults.DefaultCacheParser,
+                   cacheParserAndTypeChecker: Boolean = ConfigDefaults.DefaultCacheParserAndTypeChecker,
                    // this option introduces a mode where Gobra only considers files with a specific annotation ("// +gobra").
                    // this is useful when verifying large packages where some files might use some unsupported feature of Gobra,
                    // or when the goal is to gradually verify part of a package without having to provide an explicit list of the files
@@ -121,7 +121,7 @@ case class Config(
                    enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                    noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
                    noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors,
-                   typeCheckMode: TaskManagerMode = ConfigDefaults.DefaultTypeCheckMode,
+                   parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode,
 ) {
 
   def merge(other: Config): Config = {
@@ -159,6 +159,7 @@ case class Config(
       shouldVerify = shouldVerify,
       int32bit = int32bit || other.int32bit,
       checkConsistency = checkConsistency || other.checkConsistency,
+      cacheParserAndTypeChecker = cacheParserAndTypeChecker || other.cacheParserAndTypeChecker,
       onlyFilesWithHeader = onlyFilesWithHeader || other.onlyFilesWithHeader,
       assumeInjectivityOnInhale = assumeInjectivityOnInhale || other.assumeInjectivityOnInhale,
       parallelizeBranches = parallelizeBranches,
@@ -167,7 +168,7 @@ case class Config(
       enableLazyImports = enableLazyImports || other.enableLazyImports,
       noVerify = noVerify || other.noVerify,
       noStreamErrors = noStreamErrors || other.noStreamErrors,
-      typeCheckMode = typeCheckMode
+      parseAndTypeCheckMode = parseAndTypeCheckMode
     )
   }
 
@@ -209,7 +210,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       checkOverflows: Boolean = ConfigDefaults.DefaultCheckOverflows,
                       checkConsistency: Boolean = ConfigDefaults.DefaultCheckConsistency,
                       int32bit: Boolean = ConfigDefaults.DefaultInt32bit,
-                      cacheParser: Boolean = ConfigDefaults.DefaultCacheParser,
+                      cacheParserAndTypeChecker: Boolean = ConfigDefaults.DefaultCacheParserAndTypeChecker,
                       onlyFilesWithHeader: Boolean = ConfigDefaults.DefaultOnlyFilesWithHeader,
                       assumeInjectivityOnInhale: Boolean = ConfigDefaults.DefaultAssumeInjectivityOnInhale,
                       parallelizeBranches: Boolean = ConfigDefaults.DefaultParallelizeBranches,
@@ -218,7 +219,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports,
                       noVerify: Boolean = ConfigDefaults.DefaultNoVerify,
                       noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors,
-                      typeCheckMode: TaskManagerMode = ConfigDefaults.DefaultTypeCheckMode,
+                      parseAndTypeCheckMode: TaskManagerMode = ConfigDefaults.DefaultParseAndTypeCheckMode,
                      ) {
   def shouldParse: Boolean = true
   def shouldTypeCheck: Boolean = !shouldParseOnly
@@ -264,7 +265,7 @@ trait RawConfig {
     shouldVerify = baseConfig.shouldVerify,
     shouldChop = baseConfig.shouldChop,
     int32bit = baseConfig.int32bit,
-    cacheParser = baseConfig.cacheParser,
+    cacheParserAndTypeChecker = baseConfig.cacheParserAndTypeChecker,
     onlyFilesWithHeader = baseConfig.onlyFilesWithHeader,
     assumeInjectivityOnInhale = baseConfig.assumeInjectivityOnInhale,
     parallelizeBranches = baseConfig.parallelizeBranches,
@@ -273,7 +274,7 @@ trait RawConfig {
     enableLazyImports = baseConfig.enableLazyImports,
     noVerify = baseConfig.noVerify,
     noStreamErrors = baseConfig.noStreamErrors,
-    typeCheckMode = baseConfig.typeCheckMode,
+    parseAndTypeCheckMode = baseConfig.parseAndTypeCheckMode,
   )
 }
 
@@ -645,17 +646,17 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     noshort = true,
   )
 
-  val typeCheckMode: ScallopOption[TaskManagerMode] = choice(
-    name = "typeCheckMode",
+  val parseAndTypeCheckMode: ScallopOption[TaskManagerMode] = choice(
+    name = "parseAndTypeCheckMode",
     choices = Seq("LAZY", "SEQUENTIAL", "PARALLEL"),
-    descr = "Specifies the mode in which type-checking is performed.",
+    descr = "Specifies the mode in which parsing and type-checking is performed.",
     default = Some("PARALLEL"),
     noshort = true
   ).map {
     case "LAZY" => Lazy
     case "SEQUENTIAL" => Sequential
     case "PARALLEL" => Parallel
-    case _ => ConfigDefaults.DefaultTypeCheckMode
+    case _ => ConfigDefaults.DefaultParseAndTypeCheckMode
   }
 
   /**
@@ -795,7 +796,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     checkOverflows = checkOverflows(),
     checkConsistency = checkConsistency(),
     int32bit = int32Bit(),
-    cacheParser = false, // caching does not make sense when using the CLI. Thus, we simply set it to `false`
+    cacheParserAndTypeChecker = false, // caching does not make sense when using the CLI. Thus, we simply set it to `false`
     onlyFilesWithHeader = onlyFilesWithHeader(),
     assumeInjectivityOnInhale = assumeInjectivityOnInhale(),
     parallelizeBranches = parallelizeBranches(),
@@ -804,6 +805,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     enableLazyImports = enableLazyImports(),
     noVerify = noVerify(),
     noStreamErrors = noStreamErrors(),
-    typeCheckMode = typeCheckMode(),
+    parseAndTypeCheckMode = parseAndTypeCheckMode(),
   )
 }