From 7f32830b010455ff2267c6fb2adfc0a7c6539951 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Fri, 30 Jun 2023 14:43:24 +0200 Subject: [PATCH] cleanup --- build.sbt | 1 + src/main/scala/viper/gobra/Gobra.scala | 73 +++++----- .../scala/viper/gobra/frontend/Config.scala | 31 +++-- .../scala/viper/gobra/frontend/Parser.scala | 54 ++------ .../viper/gobra/frontend/TaskManager.scala | 17 +-- .../viper/gobra/frontend/info/Info.scala | 130 ++++-------------- .../scala/viper/gobra/BenchmarkTests.scala | 2 +- src/test/scala/viper/gobra/GobraTests.scala | 19 +-- 8 files changed, 103 insertions(+), 224 deletions(-) diff --git a/build.sbt b/build.sbt index dca34e1c5..ce407ccc9 100644 --- a/build.sbt +++ b/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 diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala index 051117256..38d7b7684 100644 --- a/src/main/scala/viper/gobra/Gobra.scala +++ b/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,39 +242,39 @@ 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) } } @@ -285,7 +282,7 @@ class Gobra extends GoVerifier with GoIdeVerifier { * 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 { diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index cd2c80df7..e39e461fd 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/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(), ) } diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala index 8057b047a..9ef811c57 100644 --- a/src/main/scala/viper/gobra/frontend/Parser.scala +++ b/src/main/scala/viper/gobra/frontend/Parser.scala @@ -16,6 +16,8 @@ import viper.gobra.reporting.{Source => _, _} import org.antlr.v4.runtime.{CharStreams, CommonTokenStream, DefaultErrorStrategy, ParserRuleContext} import org.antlr.v4.runtime.atn.PredictionMode import org.antlr.v4.runtime.misc.ParseCancellationException +import scalaz.EitherT +import scalaz.Scalaz.futureInstance 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.util.{GobraExecutionContext, Violation} @@ -31,11 +33,11 @@ object Parser extends LazyLogging { type ParseSuccessResult = (Vector[Source], PPackage) type ParseResult = Either[Vector[ParserError], ParseSuccessResult] - type PreprocessedSources = Vector[Source] type ImportToSourceOrErrorMap = Vector[(AbstractPackage, Either[Vector[ParserError], Vector[Source]])] + type PreprocessedSources = Vector[Source] - class ParseManager(config: Config, executionContext: GobraExecutionContext) extends LazyLogging { - private val manager = new TaskManager[AbstractPackage, PreprocessedSources, ParseResult](config.typeCheckMode)(executionContext) + class ParseManager(config: Config)(implicit executor: GobraExecutionContext) extends LazyLogging { + private val manager = new TaskManager[AbstractPackage, PreprocessedSources, ParseResult](config.parseAndTypeCheckMode) // note that the returned future might never complete if typeCheckMode is `Lazy` and there is no trigger to actually // execute the parsing of the specified package @@ -50,13 +52,11 @@ object Parser extends LazyLogging { def pkgInfo: PackageInfo type ImportErrorFactory = String => Vector[ParserError] - // protected def getImports(importNodes: Vector[PImport], pom: PositionManager): Set[(AbstractImport, ImportErrorFactory)] = { - protected def getImports(importNodes: Vector[PImport], pom: PositionManager): Vector[(AbstractPackage, Either[Vector[ParserError], Vector[Source]])] = { + protected def getImports(importNodes: Vector[PImport], pom: PositionManager): ImportToSourceOrErrorMap = { val explicitImports: Vector[(AbstractImport, ImportErrorFactory)] = importNodes .map(importNode => { val importErrorFactory: ImportErrorFactory = (errMsg: String) => { val err = pom.translate(message(importNode, errMsg), ParserError) - // config.reporter report ParserErrorMessage(err.head.position.get.file, err) err } (RegularImport(importNode.importPath), importErrorFactory) @@ -82,14 +82,6 @@ object Parser extends LazyLogging { (directImportPackage, res) } errsOrSources - /* - val (errors, sources) = errsOrSources.partitionMap(identity) - if (errors.nonEmpty) { - Left(errors) - } else { - Right(sources) - } - */ } } @@ -161,9 +153,7 @@ object Parser extends LazyLogging { Left(errs) } - def getResults: Map[AbstractPackage, ParseResult] = manager.getAllResultsWithKeys - - def getResultsFut: Future[Map[AbstractPackage, ParseResult]] = manager.getAllResultsWithKeysFut + def getResults: Future[Map[AbstractPackage, ParseResult]] = manager.getAllResultsWithKeys } /** @@ -182,34 +172,18 @@ object Parser extends LazyLogging { * */ - def parse(config: Config, pkgInfo: PackageInfo)(executionContext: GobraExecutionContext): Either[Vector[ParserError], Map[AbstractPackage, ParseResult]] = { - val parseManager = new ParseManager(config, executionContext) + def parse(config: Config, pkgInfo: PackageInfo)(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, Map[AbstractPackage, ParseResult]] = { + val parseManager = new ParseManager(config) parseManager.parse(pkgInfo) - val results = parseManager.getResults - results.get(RegularPackage(pkgInfo.id)) match { - case Some(Right(_)) => Right(results) - case Some(Left(errs)) => Left(errs) - case _ => Violation.violation(s"No parse result for package '$pkgInfo' found") - } - } - - def parseFut(config: Config, pkgInfo: PackageInfo)(executionContext: GobraExecutionContext): Future[Either[Vector[ParserError], Map[AbstractPackage, ParseResult]]] = { - val parseManager = new ParseManager(config, executionContext) - parseManager.parse(pkgInfo) - implicit val executor: GobraExecutionContext = executionContext - for { - results <- parseManager.getResultsFut + val res: Future[Either[Vector[VerifierError], Map[AbstractPackage, ParseResult]]] = for { + results <- parseManager.getResults res = results.get(RegularPackage(pkgInfo.id)) match { case Some(Right(_)) => Right(results) case Some(Left(errs)) => Left(errs) case _ => Violation.violation(s"No parse result for package '$pkgInfo' found") } } yield res - } - - def parse(input: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean = false)(config: Config): Either[Vector[VerifierError], PPackage] = { - val preprocessedInputs = preprocess(input)(config) - process(preprocessedInputs, pkgInfo, specOnly = specOnly)(config) + EitherT.fromEither(res) } private def preprocess(input: Vector[Source])(config: Config): Vector[Source] = { @@ -244,7 +218,7 @@ object Parser extends LazyLogging { res } - if (config.cacheParser) parseSourceCached(preprocessedSource) else parseSource(preprocessedSource) + if (config.cacheParserAndTypeChecker) parseSourceCached(preprocessedSource) else parseSource(preprocessedSource) } private def process(preprocessedInputs: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[ParserError], PPackage] = { @@ -309,7 +283,7 @@ object Parser extends LazyLogging { res } - val parseFn = if (config.cacheParser) { parseSourcesCached _ } else { parseSourcesUncached _ } + val parseFn = if (config.cacheParserAndTypeChecker) { parseSourcesCached _ } else { parseSourcesUncached _ } parseFn(sources, pkgInfo, specOnly)(config) } diff --git a/src/main/scala/viper/gobra/frontend/TaskManager.scala b/src/main/scala/viper/gobra/frontend/TaskManager.scala index 85557cfd5..991949ce4 100644 --- a/src/main/scala/viper/gobra/frontend/TaskManager.scala +++ b/src/main/scala/viper/gobra/frontend/TaskManager.scala @@ -54,7 +54,7 @@ trait Job[I, R] { } } -class TaskManager[K, I, R](mode: TaskManagerMode)(executionContext: GobraExecutionContext) { +class TaskManager[K, I, R](mode: TaskManagerMode)(implicit executor: GobraExecutionContext) { private val jobs: ConcurrentMap[K, Job[I, R]] = new ConcurrentHashMap() def addIfAbsent(id: K, job: Job[I, R]): Unit = { @@ -68,12 +68,12 @@ class TaskManager[K, I, R](mode: TaskManagerMode)(executionContext: GobraExecuti mode match { case Sequential => job.execute() case Lazy => // don't do anything as of now - case Parallel => Future{ job.execute() }(executionContext) + case Parallel => Future{ job.execute() } } } } - def getResultFut(id: K): Future[R] = { + def getResult(id: K): Future[R] = { val job = jobs.get(id) Violation.violation(job != null, s"Task $id not found") mode match { @@ -83,12 +83,11 @@ class TaskManager[K, I, R](mode: TaskManagerMode)(executionContext: GobraExecuti job.getFuture } - def getResult(id: K): R = { - Await.result(getResultFut(id), Duration.Inf) + def getResultBlocking(id: K): R = { + Await.result(getResult(id), Duration.Inf) } - def getAllResultsWithKeysFut: Future[Map[K, R]] = { - implicit val executor: GobraExecutionContext = executionContext + def getAllResultsWithKeys: Future[Map[K, R]] = { val futs = jobs.asScala.toVector.map { case (key, job) => mode match { case Lazy => job.execute() // now we need the job's result @@ -98,8 +97,4 @@ class TaskManager[K, I, R](mode: TaskManagerMode)(executionContext: GobraExecuti } Future.sequence(futs).map(_.toMap) } - - def getAllResultsWithKeys: Map[K, R] = { - Await.result(getAllResultsWithKeysFut, Duration.Inf) - } } diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala index f14877ae7..687730513 100644 --- a/src/main/scala/viper/gobra/frontend/info/Info.scala +++ b/src/main/scala/viper/gobra/frontend/info/Info.scala @@ -10,12 +10,13 @@ import com.typesafe.scalalogging.LazyLogging import org.bitbucket.inkytonik.kiama.relation.Tree import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, message} import org.bitbucket.inkytonik.kiama.util.{Position, Source} +import scalaz.EitherT +import scalaz.Scalaz.futureInstance 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.{ParseResult, ParseSuccessResult} import viper.gobra.frontend.TaskManagerMode.{Lazy, Parallel, Sequential} -import viper.gobra.frontend.info.Info.Context 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} @@ -61,12 +62,6 @@ object Info extends LazyLogging { 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 => { @@ -81,18 +76,6 @@ object Info extends LazyLogging { case (key, Right(res)) => (key, res) } } yield successParseResults - /* - val (_, ast) = getParseResult(abstractPackage) - 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) - } - */ } /** @@ -109,7 +92,6 @@ object Info extends LazyLogging { 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 { @@ -122,44 +104,17 @@ object Info extends LazyLogging { 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) - if (parserPendingPackages.contains(directlyImportedTarget)) { - // package cycle detected - val importNodeStart = ast.positions.positions.getStart(importNode) - Vector(ImportCycle(importNode, importNodeStart, parserPendingPackages)) - } else { - getCycles(directlyImportedTarget) - } - }) - parserPendingPackages = parserPendingPackages.filterNot(_ == importTarget) - res - } - */ 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("[", ", ", "]")}") - })*/ + cyclicErrors.flatMap(cycle => message(importNode, cycle.message)) + } } } @@ -167,8 +122,8 @@ object Info extends LazyLogging { * All TypeInfo instances share a single context instance. * Therefore, package management is centralized. */ - class Context(val config: Config, val parseResults: Map[AbstractPackage, ParseSuccessResult])(val executionContext: GobraExecutionContext) extends GetParseResult { - private val typeCheckManager = new TaskManager[AbstractPackage, (Vector[Source], PPackage, Vector[AbstractImport]), () => TypeCheckResult](config.typeCheckMode)(executionContext) + class Context(val config: Config, val parseResults: Map[AbstractPackage, ParseSuccessResult])(implicit executor: GobraExecutionContext) extends GetParseResult { + private val typeCheckManager = new TaskManager[AbstractPackage, (Vector[Source], PPackage, Vector[AbstractImport]), () => TypeCheckResult](config.parseAndTypeCheckMode) var tyeCheckDurationMs = new AtomicLong(0L) @@ -193,19 +148,19 @@ object Info extends LazyLogging { val (sources, ast, dependencies) = precomputationResult val dependentTypeInfo = dependencies.map(importTarget => { val dependentPackage = AbstractPackage(importTarget)(config) - (importTarget, typeCheckManager.getResult(dependentPackage)) + (importTarget, typeCheckManager.getResultBlocking(dependentPackage)) }) - config.typeCheckMode match { + config.parseAndTypeCheckMode match { case Sequential | Parallel => - val res = typeCheck(sources, ast, dependentTypeInfo.toMap, isMainContext = isMainContext) + val res = typeCheck(sources, ast, dependentTypeInfo.toMap) () => res case Lazy => - lazy val res = typeCheck(sources, ast, dependentTypeInfo.toMap, isMainContext = isMainContext) + lazy val res = typeCheck(sources, ast, dependentTypeInfo.toMap) () => res } } - private def typeCheck(pkgSources: Vector[Source], pkg: PPackage, dependentTypeInfo: DependentTypeInfo, isMainContext: Boolean = false, isLazy: Boolean = false): TypeCheckResult = { + private def typeCheck(pkgSources: Vector[Source], pkg: PPackage, dependentTypeInfo: DependentTypeInfo, isLazy: 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) @@ -222,37 +177,31 @@ object Info extends LazyLogging { } } - def typeCheck(pkg: AbstractPackage): TypeCheckResult = { + def typeCheck(pkg: AbstractPackage): Future[TypeCheckResult] = { typeCheckManager.addIfAbsent(pkg, TypeCheckJob(pkg, isMainContext = true)) - val resFn = typeCheckManager.getResult(pkg) - resFn() - } - - def typeCheckFut(pkg: AbstractPackage): Future[TypeCheckResult] = { - typeCheckManager.addIfAbsent(pkg, TypeCheckJob(pkg, isMainContext = true)) - typeCheckManager.getResultFut(pkg) - .map(resFn => resFn())(executionContext) + typeCheckManager.getResult(pkg) + .map(resFn => resFn()) } } - def check(config: Config, abstractPackage: AbstractPackage, parseResults: Map[AbstractPackage, ParseResult])(executionContext: GobraExecutionContext): TypeCheckResult = { + def check(config: Config, abstractPackage: AbstractPackage, parseResults: Map[AbstractPackage, ParseResult])(implicit executor: GobraExecutionContext): EitherT[Vector[VerifierError], Future, TypeInfo] = { for { // check whether parsing of this package was successful: - parseResult <- parseResults(abstractPackage) + parseResult <- EitherT.fromEither(Future.successful[Either[Vector[VerifierError], ParseSuccessResult]](parseResults(abstractPackage))) // check whether there are any import cycles: - cycleResult <- new CycleChecker(config, parseResults).check(abstractPackage) - .left.map(errs => { + cycleResult <- EitherT.fromEither(Future.successful(new CycleChecker(config, parseResults).check(abstractPackage))) + .leftMap(errs => { val (sources, pkg) = parseResult val sourceNames = sources.map(_.name) config.reporter report TypeCheckFailureMessage(sourceNames, pkg.packageClause.id.name, () => pkg, errs) errs }) typeCheckingStartMs = System.currentTimeMillis() - context = new Context(config, cycleResult)(executionContext) - typeInfo <- context.typeCheck(abstractPackage) + context = new Context(config, cycleResult) + typeInfo <- EitherT.fromEither(context.typeCheck(abstractPackage)) _ = logger.debug { val durationS = f"${(System.currentTimeMillis() - typeCheckingStartMs) / 1000f}%.1f" - s"type-checking done, took ${durationS}s (in mode ${config.typeCheckMode})" + s"type-checking done, took ${durationS}s (in mode ${config.parseAndTypeCheckMode})" } _ = logger.debug { val typeCheckingEndMs = System.currentTimeMillis() @@ -264,39 +213,6 @@ object Info extends LazyLogging { } yield typeInfo } - def checkFut(config: Config, abstractPackage: AbstractPackage, parseResults: Map[AbstractPackage, ParseResult])(executionContext: GobraExecutionContext): Future[TypeCheckResult] = { - implicit val executor: GobraExecutionContext = executionContext - val res = for { - // check whether parsing of this package was successful: - parseResult <- parseResults(abstractPackage) - // check whether there are any import cycles: - cycleResult <- new CycleChecker(config, parseResults).check(abstractPackage) - .left.map(errs => { - val (sources, pkg) = parseResult - val sourceNames = sources.map(_.name) - config.reporter report TypeCheckFailureMessage(sourceNames, pkg.packageClause.id.name, () => pkg, errs) - errs - }) - typeCheckingStartMs = System.currentTimeMillis() - context = new Context(config, cycleResult)(executionContext) - typeInfoFut = for { - typeInfo <- context.typeCheckFut(abstractPackage) - _ = logger.debug { - val durationS = f"${(System.currentTimeMillis() - typeCheckingStartMs) / 1000f}%.1f" - s"type-checking done, took ${durationS}s (in mode ${config.typeCheckMode})" - } - _ = logger.debug { - val typeCheckingEndMs = System.currentTimeMillis() - val sumDurationS = f"${context.tyeCheckDurationMs.get() / 1000f}%.1f" - val overheadMs = (typeCheckingEndMs - typeCheckingStartMs) - context.tyeCheckDurationMs.get() - val overheadS = f"${overheadMs / 1000f}%.1f" - s"type-checking individual packages took ${sumDurationS}s. Overhead for tasks is thus ${overheadS}s (${(100f * overheadMs / (typeCheckingEndMs - typeCheckingStartMs)).toInt}%)" - } - } yield typeInfo - } yield typeInfoFut - res.fold(errs => Future.successful(Left(errs)), identity) - } - type TypeInfoCacheKey = String private val typeInfoCache: ConcurrentMap[TypeInfoCacheKey, TypeInfoImpl] = new ConcurrentHashMap() @@ -339,9 +255,9 @@ object Info extends LazyLogging { typeInfoCache.computeIfAbsent(getCacheKey(pkg, dependentTypeInfo, isMainContext, config), _ => getTypeInfo(pkg, dependentTypeInfo, isMainContext, config)) } - val checkFn = if (config.cacheParser) { getTypeInfoCached _ } else { getTypeInfo _ } + val checkFn = if (config.cacheParserAndTypeChecker) { getTypeInfoCached _ } else { getTypeInfo _ } val info = checkFn(pkg, dependentTypeInfo, isMainContext, config) - if (!cacheHit && config.cacheParser) { + if (!cacheHit && config.cacheParserAndTypeChecker) { logger.trace(s"No cache hit for type info for ${pkg.info.id}") } diff --git a/src/test/scala/viper/gobra/BenchmarkTests.scala b/src/test/scala/viper/gobra/BenchmarkTests.scala index afbe52588..089d522a2 100644 --- a/src/test/scala/viper/gobra/BenchmarkTests.scala +++ b/src/test/scala/viper/gobra/BenchmarkTests.scala @@ -56,7 +56,7 @@ trait GobraFrontendForTesting extends Frontend { val z3PropertyName = "GOBRATESTS_Z3_EXE" val z3Exe: Option[String] = Option(System.getProperty(z3PropertyName)) - protected val executor: GobraExecutionContext = new DefaultGobraExecutionContext() + protected implicit val executor: GobraExecutionContext = new DefaultGobraExecutionContext() protected var config: Option[Config] = None /** Initialize this translator with a given verifier. Only meant to be called once. */ diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala index e22a5ab30..713679558 100644 --- a/src/test/scala/viper/gobra/GobraTests.scala +++ b/src/test/scala/viper/gobra/GobraTests.scala @@ -10,6 +10,7 @@ import java.nio.file.Path import ch.qos.logback.classic.Level import org.bitbucket.inkytonik.kiama.util.Source import org.scalatest.{Args, BeforeAndAfterAll, Status} +import scalaz.Scalaz.futureInstance import viper.gobra.frontend.PackageResolver.RegularPackage import viper.gobra.frontend.Source.FromFileSource import viper.gobra.frontend.TaskManagerMode.{Lazy, Parallel} @@ -35,10 +36,6 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll { var gobraInstance: Gobra = _ var executor: GobraExecutionContext = _ var inputs: Vector[Source] = Vector.empty - // while we could pre-fetch and cache parse and maybe even type-check results, the regression test suite is designed - // in a way that each file is its own test case. However, feeding a map of package infos to Gobra results in Gobra - // considering these files in a Go way, i.e., groups them by package clause. This in turn results in testcase failures - // as errors occur in files technically not under test but in the same directory and having the same package clause. val cacheParserAndTypeChecker = true override def beforeAll(): Unit = { @@ -58,8 +55,7 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll { reporter = NoopReporter, packageInfoInputMap = Map(Source.getPackageInfo(source, Path.of("")) -> Vector(source)), checkConsistency = true, - cacheParser = cacheParserAndTypeChecker, - typeCheckMode = if (cacheParserAndTypeChecker) Parallel else Lazy, + cacheParserAndTypeChecker = cacheParserAndTypeChecker, z3Exe = z3Exe ) @@ -69,13 +65,12 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll { val futs = inputs.map(source => { val config = getConfig(source) val pkgInfo = config.packageInfoInputMap.keys.head - for { - parseResultEither <- Parser.parseFut(config, pkgInfo)(executor) + val fut = for { + parseResult <- Parser.parseFut(config, pkgInfo) pkg = RegularPackage(pkgInfo.id) - typeCheckResultEither <- parseResultEither.fold( - parseErrs => Future.successful(Left(parseErrs)), - parseResult => Info.checkFut(config, pkg, parseResult)(executor)) - } yield typeCheckResultEither + typeCheckResult <- Info.checkFut(config, pkg, parseResult) + } yield typeCheckResult + fut.toEither }) Await.result(Future.sequence(futs), Duration.Inf) println("pre-parsing and pre-typeChecking completed")