diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala index cb9e18620..a391465f8 100644 --- a/src/main/scala/viper/gobra/Gobra.scala +++ b/src/main/scala/viper/gobra/Gobra.scala @@ -16,6 +16,7 @@ import viper.gobra.ast.frontend.PPackage 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.info.Info.Context import viper.gobra.frontend.info.{Info, TypeInfo} import viper.gobra.frontend.{Config, Desugar, PackageInfo, Parser, ScallopGobraConfig} import viper.gobra.reporting._ @@ -158,7 +159,7 @@ class Gobra extends GoVerifier with GoIdeVerifier { finalConfig <- getAndMergeInFileConfig(config, pkgInfo) _ = setLogLevel(finalConfig) parsedPackage <- performParsing(pkgInfo, finalConfig) - typeInfo <- performTypeChecking(parsedPackage, finalConfig) + typeInfo <- performTypeChecking(parsedPackage, executor, finalConfig) program <- performDesugaring(parsedPackage, typeInfo, finalConfig) program <- performInternalTransformations(program, finalConfig, pkgInfo) viperTask <- performViperEncoding(program, finalConfig, pkgInfo) @@ -243,16 +244,20 @@ class Gobra extends GoVerifier with GoIdeVerifier { private def performParsing(pkgInfo: PackageInfo, config: Config): Either[Vector[VerifierError], PPackage] = { if (config.shouldParse) { + val startMs = System.currentTimeMillis() val sourcesToParse = config.packageInfoInputMap(pkgInfo) - Parser.parse(sourcesToParse, pkgInfo)(config) + val res = Parser.parse(sourcesToParse, pkgInfo)(config) + val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f" + println(s"parser phase done, took ${durationS}s") + res } else { Left(Vector()) } } - private def performTypeChecking(parsedPackage: PPackage, config: Config): Either[Vector[VerifierError], TypeInfo] = { + private def performTypeChecking(parsedPackage: PPackage, executionContext: GobraExecutionContext, config: Config): Either[Vector[VerifierError], TypeInfo] = { if (config.shouldTypeCheck) { - Info.check(parsedPackage, config.packageInfoInputMap(parsedPackage.info), isMainContext = true)(config) + Info.check(parsedPackage, config.packageInfoInputMap(parsedPackage.info), isMainContext = true, context = new Context(executionContext, config))(config) } else { Left(Vector()) } @@ -260,7 +265,11 @@ class Gobra extends GoVerifier with GoIdeVerifier { private def performDesugaring(parsedPackage: PPackage, typeInfo: TypeInfo, config: Config): Either[Vector[VerifierError], Program] = { if (config.shouldDesugar) { - Right(Desugar.desugar(parsedPackage, typeInfo)(config)) + val startMs = System.currentTimeMillis() + val res = Right(Desugar.desugar(parsedPackage, typeInfo)(config)) + val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f" + println(s"desugaring done, took ${durationS}s") + res } else { Left(Vector()) } @@ -282,18 +291,25 @@ class Gobra extends GoVerifier with GoIdeVerifier { // 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. + val startMs = System.currentTimeMillis() var transformations: Vector[InternalTransform] = Vector(CGEdgesTerminationTransform, ConstantPropagation) if (config.checkOverflows) { transformations :+= OverflowChecksTransform } val result = transformations.foldLeft(program)((prog, transf) => transf.transform(prog)) config.reporter.report(AppliedInternalTransformsMessage(config.packageInfoInputMap(pkgInfo).map(_.name), () => result)) + val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f" + println(s"internal transformations done, took ${durationS}s") Right(result) } private def performViperEncoding(program: Program, config: Config, pkgInfo: PackageInfo): Either[Vector[VerifierError], BackendVerifier.Task] = { if (config.shouldViperEncode) { - Right(Translator.translate(program, pkgInfo)(config)) + val startMs = System.currentTimeMillis() + val res = Right(Translator.translate(program, pkgInfo)(config)) + val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f" + println(s"Viper encoding done, took ${durationS}s") + res } else { Left(Vector()) } diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 51da14019..f9a1c9c59 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -16,6 +16,8 @@ import viper.gobra.backend.{ViperBackend, ViperBackends} import viper.gobra.GoVerifier import viper.gobra.frontend.PackageResolver.FileResource import viper.gobra.frontend.Source.getPackageInfo +import viper.gobra.frontend.info.Info.TypeCheckMode +import viper.gobra.frontend.info.Info.TypeCheckMode.TypeCheckMode import viper.gobra.reporting.{FileWriterReporter, GobraReporter, StdIOReporter} import viper.gobra.util.{TypeBounds, Violation} import viper.silver.ast.SourcePosition @@ -68,6 +70,7 @@ object ConfigDefaults { lazy val DefaultEnableLazyImports: Boolean = false lazy val DefaultNoVerify: Boolean = false lazy val DefaultNoStreamErrors: Boolean = false + lazy val DefaultTypeCheckMode: TypeCheckMode = TypeCheckMode.Parallel } case class Config( @@ -118,7 +121,8 @@ case class Config( disableMoreCompleteExhale: Boolean = ConfigDefaults.DefaultDisableMoreCompleteExhale, enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, - noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors + noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors, + typeCheckMode: TypeCheckMode = ConfigDefaults.DefaultTypeCheckMode, ) { def merge(other: Config): Config = { @@ -163,7 +167,8 @@ case class Config( disableMoreCompleteExhale = disableMoreCompleteExhale, enableLazyImports = enableLazyImports || other.enableLazyImports, noVerify = noVerify || other.noVerify, - noStreamErrors = noStreamErrors || other.noStreamErrors + noStreamErrors = noStreamErrors || other.noStreamErrors, + typeCheckMode = typeCheckMode ) } @@ -214,6 +219,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector enableLazyImports: Boolean = ConfigDefaults.DefaultEnableLazyImports, noVerify: Boolean = ConfigDefaults.DefaultNoVerify, noStreamErrors: Boolean = ConfigDefaults.DefaultNoStreamErrors, + typeCheckMode: TypeCheckMode = ConfigDefaults.DefaultTypeCheckMode, ) { def shouldParse: Boolean = true def shouldTypeCheck: Boolean = !shouldParseOnly @@ -268,6 +274,7 @@ trait RawConfig { enableLazyImports = baseConfig.enableLazyImports, noVerify = baseConfig.noVerify, noStreamErrors = baseConfig.noStreamErrors, + typeCheckMode = baseConfig.typeCheckMode, ) } @@ -639,6 +646,19 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals noshort = true, ) + val typeCheckMode: ScallopOption[TypeCheckMode] = choice( + name = "typeCheckMode", + choices = Seq("LAZY", "SEQUENTIAL", "PARALLEL"), + descr = "Specifies the mode in which type-checking is performed.", + default = Some("PARALLEL"), + noshort = true + ).map { + case "LAZY" => TypeCheckMode.Lazy + case "SEQUENTIAL" => TypeCheckMode.Sequential + case "PARALLEL" => TypeCheckMode.Parallel + case _ => ConfigDefaults.DefaultTypeCheckMode + } + /** * Exception handling */ @@ -785,5 +805,6 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals enableLazyImports = enableLazyImports(), noVerify = noVerify(), noStreamErrors = noStreamErrors(), + typeCheckMode = typeCheckMode(), ) } diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index cc107c5d7..96a372934 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -31,6 +31,7 @@ object Desugar { def desugar(pkg: PPackage, info: viper.gobra.frontend.info.TypeInfo)(config: Config): in.Program = { val importsCollector = new PackageInitSpecCollector // independently desugar each imported package. + val importedDesugaringStartMs = System.currentTimeMillis() val importedPrograms = info.context.getContexts map { tI => { val typeInfo: TypeInfo = tI.getTypeInfo val importedPackage = typeInfo.tree.originalRoot @@ -39,12 +40,18 @@ object Desugar { d.registerPackage(importedPackage, importsCollector)(config) (d, d.packageD(importedPackage)) }} + val importedDurationS = f"${(System.currentTimeMillis() - importedDesugaringStartMs) / 1000f}%.1f" + println(s"desugaring imported packages done, took ${importedDurationS}s") + + val desugaringStartMs = System.currentTimeMillis() // desugar the main package, i.e. the package on which verification is performed: val mainDesugarer = new Desugarer(pkg.positions, info) // registers main package to generate proof obligations for its init code mainDesugarer.registerMainPackage(pkg, importsCollector)(config) // combine all desugared results into one Viper program: val internalProgram = combine(mainDesugarer, mainDesugarer.packageD(pkg), importedPrograms) + val durationS = f"${(System.currentTimeMillis() - desugaringStartMs) / 1000f}%.1f" + println(s"desugaring main package done, took ${durationS}s") config.reporter report DesugaredMessage(config.packageInfoInputMap(pkg.info).map(_.name), () => internalProgram) internalProgram } @@ -3455,7 +3462,8 @@ object Desugar { // Collect and register all import-preconditions pkg.imports.foreach{ imp => info.context.getTypeInfo(RegularImport(imp.importPath))(config) match { - case Some(Right(tI)) => + // case Some(Right(tI)) => + case Right(tI) => val desugaredPre = imp.importPres.map(specificationD(FunctionContext.empty(), info)) Violation.violation(!config.enableLazyImports || desugaredPre.isEmpty, s"Import precondition found despite running with ${Config.enableLazyImportOptionPrettyPrinted}") specCollector.addImportPres(tI.getTypeInfo.tree.originalRoot, desugaredPre) diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala index bc80f19e5..947840d11 100644 --- a/src/main/scala/viper/gobra/frontend/Parser.scala +++ b/src/main/scala/viper/gobra/frontend/Parser.scala @@ -22,6 +22,7 @@ import viper.silver.ast.SourcePosition import scala.collection.mutable.ListBuffer import java.security.MessageDigest +import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap} object Parser { @@ -59,7 +60,7 @@ object Parser { type SourceCacheKey = String // cache maps a key (obtained by hasing file path and file content) to the parse result - private var sourceCache: Map[SourceCacheKey, (Either[Vector[ParserError], PProgram], Positions)] = Map.empty + private var sourceCache: ConcurrentMap[SourceCacheKey, (Either[Vector[ParserError], PProgram], Positions)] = new ConcurrentHashMap() /** computes the key for caching a particular source. This takes the name, the specOnly flag, and the file's contents into account */ private def getCacheKey(source: Source, specOnly: Boolean): SourceCacheKey = { @@ -70,7 +71,7 @@ object Parser { } def flushCache(): Unit = { - sourceCache = Map.empty + sourceCache.clear() } private def parseSources(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[VerifierError], PPackage] = { @@ -100,10 +101,11 @@ object Parser { def parseAndStore(): (Either[Vector[ParserError], PProgram], Positions) = { cacheHit = false val res = parseSource(source) - sourceCache += getCacheKey(source, specOnly) -> (res, positions) + // sourceCache.put(getCacheKey(source, specOnly), (res, positions)) (res, positions) } - val (res, pos) = sourceCache.getOrElse(getCacheKey(source, specOnly), parseAndStore()) + // val (res, pos) = sourceCache.getOrElse(getCacheKey(source, specOnly), parseAndStore()) + val (res, pos) = sourceCache.computeIfAbsent(getCacheKey(source, specOnly), _ => parseAndStore()) if (cacheHit) { // a cached AST has been found in the cache. The position manager does not yet have any positions for nodes in // this AST. Therefore, the following strategy iterates over the entire AST and copies positional information diff --git a/src/main/scala/viper/gobra/frontend/TaskManager.scala b/src/main/scala/viper/gobra/frontend/TaskManager.scala new file mode 100644 index 000000000..8413d396b --- /dev/null +++ b/src/main/scala/viper/gobra/frontend/TaskManager.scala @@ -0,0 +1,76 @@ +package viper.gobra.frontend + +import viper.gobra.frontend.info.Info.TypeCheckMode +import viper.gobra.util.{GobraExecutionContext, Violation} + +import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap} +import scala.concurrent.duration.Duration +import scala.concurrent.{Await, Future, Promise} +import scala.util.{Failure, Success} +import scala.jdk.CollectionConverters._ + +trait Job[R] { + private var compututationStarted = false + private val promise: Promise[R] = Promise() + def getFuture: Future[R] = promise.future + protected def compute(): R + + def call(): R = { + getFuture.value match { + case Some(Success(res)) => return res // return already computed type-checker result + case Some(Failure(exception)) => Violation.violation(s"Job resulted in exception: $exception") + case _ => + } + Violation.violation(!compututationStarted, s"Job is already on-going") + compututationStarted = true + val res = compute() + promise.success(res) + res + } +} + +class TaskManager[K, R](config: Config) { + private val jobs: ConcurrentMap[K, Job[R]] = new ConcurrentHashMap() + + /** + * returns true if job has been inserted and thus was previously absent + */ + def addIfAbsent(id: K, job: Job[R], insertOnly: Boolean = false)(executionContext: GobraExecutionContext): Boolean = { + var isAbsent = false + // first insert job, then run it (if necessary) + jobs.computeIfAbsent(id, _ => { + isAbsent = true + job + }) + // now run it but only if it's a new job: + if (isAbsent && !insertOnly) { + config.typeCheckMode match { + case TypeCheckMode.Lazy => // don't do anything as of now + case TypeCheckMode.Sequential => job.call() + case TypeCheckMode.Parallel => Future{ job.call() }(executionContext) + } + } + isAbsent + } + + def getResult(id: K): R = { + val job = jobs.get(id) + Violation.violation(job != null, s"Task $id not found") + getResultFromJob(job) + } + + def getAllResults: Iterable[R] = + jobs.values().asScala.map(getResultFromJob) + + def getAllResultsWithKeys: Iterable[(K, R)] = + jobs.asScala.toVector.map { case (key, job) => (key, getResultFromJob(job)) } + + private def getResultFromJob(job: Job[R]): R = config.typeCheckMode match { + case TypeCheckMode.Lazy => job.call() // we perform the computation now that we need the result + case TypeCheckMode.Sequential => + // note that we cannot await the future here as type-checking of this package might not have started yet. + // Thus, we use `.call()` that either returns a previously calculated type-checking result or will calculate it. + job.call() + case TypeCheckMode.Parallel => Await.result(job.getFuture, 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 234b591fb..9c0ef6a77 100644 --- a/src/main/scala/viper/gobra/frontend/info/Info.scala +++ b/src/main/scala/viper/gobra/frontend/info/Info.scala @@ -7,81 +7,507 @@ package viper.gobra.frontend.info import org.bitbucket.inkytonik.kiama.relation.Tree -import org.bitbucket.inkytonik.kiama.util.Source -import viper.gobra.ast.frontend.{PNode, PPackage} -import viper.gobra.frontend.Config -import viper.gobra.frontend.PackageResolver.{AbstractImport, AbstractPackage} +import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, message, noMessages} +import org.bitbucket.inkytonik.kiama.util.{Position, Source} +import viper.gobra.ast.frontend.{PImport, PNode, PPackage} +import viper.gobra.frontend.{Config, Job, PackageResolver, Parser, Source, TaskManager} +import viper.gobra.frontend.PackageResolver.{AbstractImport, AbstractPackage, BuiltInImport, RegularImport, RegularPackage} +import viper.gobra.frontend.info.Info.TypeCheckMode.TypeCheckMode import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.frontend.info.implementation.typing.ghost.separation.{GhostLessPrinter, GoifyingPrinter} -import viper.gobra.reporting.{CyclicImportError, TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, VerifierError} +import viper.gobra.reporting.{CyclicImportError, NotFoundError, TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, VerifierError} +import viper.gobra.util.{GobraExecutionContext, Violation} +import java.util.concurrent.Callable import scala.collection.immutable.ListMap +import scala.concurrent.duration.Duration +import scala.concurrent.{Await, Future, Promise} +import scala.util.{Failure, Success} object Info { type GoTree = Tree[PNode, PPackage] + /** + * ImportCycle describes a cyclic import. `importClosingCycle` is the AST node that closes the cycle and + * `cyclicPackages` stores the packages involved in the cycle. + */ + case class ImportCycle(importNodeCausingCycle: PImport, importNodeStart: Option[Position], cyclicPackages: Vector[AbstractImport]) + + object TypeCheckMode extends Enumeration { + type TypeCheckMode = Value + val Lazy, Sequential, Parallel = Value + } + /** * All TypeInfo instances share a single context instance. * Therefore, package management is centralized. */ - class Context { - /** stores the results of all imported packages that have been parsed and type checked so far */ - private var contextMap: Map[AbstractPackage, Either[Vector[VerifierError], ExternalTypeInfo]] = ListMap[AbstractPackage, Either[Vector[VerifierError], ExternalTypeInfo]]() + class Context(executionContext: GobraExecutionContext, config: Config) { + /** stores the results of all imported packages that have been parsed so far */ + private var parserContextMap: Map[AbstractPackage, Either[Vector[VerifierError], (Vector[Source], PPackage)]] = ListMap() /** keeps track of the package dependencies that are currently resolved. This information is used to detect cycles */ - private var pendingPackages: Vector[AbstractImport] = Vector() + private var parserPendingPackages: Vector[AbstractImport] = Vector() /** stores all cycles that have been discovered so far */ - private var knownImportCycles: Set[Vector[AbstractImport]] = Set() + var parserKnownImportCycles: Set[ImportCycle] = Set() - def addPackage(importTarget: AbstractImport, typeInfo: ExternalTypeInfo)(config: Config): Unit = { + /* + def parseRecursively(importTarget: AbstractImport)(config: Config): Either[Vector[VerifierError], PPackage] = { val packageTarget = AbstractPackage(importTarget)(config) - pendingPackages = pendingPackages.filterNot(_ == importTarget) - contextMap = contextMap + (packageTarget -> Right(typeInfo)) + parserPendingPackages = parserPendingPackages :+ importTarget + val pkgSources = PackageResolver.resolveSources(importTarget)(config) + .getOrElse(Vector()) + .map(_.source) + val res = for { + nonEmptyPkgSources <- if (pkgSources.isEmpty) + Left(Vector(NotFoundError(s"No source files for package '$importTarget' found"))) + else Right(pkgSources) + parsedProgram <- Parser.parse(nonEmptyPkgSources, Source.getPackageInfo(nonEmptyPkgSources.head, config.projectRoot), specOnly = true)(config) + directImportTargets = parsedProgram.imports.map(i => RegularImport(i.importPath)) + errorsInTransitivePackages = directImportTargets + .map(directImportTarget => { + if (parserPendingPackages.contains(directImportTarget)) { + // package cycle detected + parserKnownImportCycles += parserPendingPackages + Left(Vector(CyclicImportError(s"Cyclic package import detected starting with package '$packageTarget'"))) + } else { + parseRecursively(directImportTarget)(config) + } + }) + .flatMap(_.left.getOrElse(Vector.empty)) + res <- if (errorsInTransitivePackages.isEmpty) Right(parsedProgram) else Left(errorsInTransitivePackages) + } yield res + parserPendingPackages = parserPendingPackages.filterNot(_ == importTarget) + parserContextMap = parserContextMap + (packageTarget -> res) + res } - - def addErrenousPackage(importTarget: AbstractImport, errors: Vector[VerifierError])(config: Config): Unit = { + */ + def parseRecursively(importTarget: AbstractImport)(config: Config): Either[Vector[VerifierError], PPackage] = { val packageTarget = AbstractPackage(importTarget)(config) - pendingPackages = pendingPackages.filterNot(_ == importTarget) - contextMap = contextMap + (packageTarget -> Left(errors)) - } - def getTypeInfo(importTarget: AbstractImport)(config: Config): Option[Either[Vector[VerifierError], ExternalTypeInfo]] = { - val packageTarget = AbstractPackage(importTarget)(config) - contextMap.get(packageTarget) match { - case s@Some(_) => s - case _ => { - // there is no entry yet and package resolution might need to resolve multiple depending packages - // keep track of these packages in pendingPackages until either type information or an error is added to contextMap - if (pendingPackages.contains(importTarget)) { - // package cycle detected - knownImportCycles += pendingPackages - Some(Left(Vector(CyclicImportError(s"Cyclic package import detected starting with package '$packageTarget'")))) - } else { - pendingPackages = pendingPackages :+ importTarget - None - } + // skip packages that we have already parsed: + if (parserContextMap.contains(packageTarget)) { + return parserContextMap(packageTarget) match { + case Right((_, pkg)) => Right(pkg) + case Left(errs) => Left(errs) } } + + println(s"parsing $importTarget") + parserPendingPackages = parserPendingPackages :+ importTarget + val pkgSources = PackageResolver.resolveSources(importTarget)(config) + .getOrElse(Vector()) + .map(_.source) + + val res = for { + nonEmptyPkgSources <- if (pkgSources.isEmpty) + Left(Vector(NotFoundError(s"No source files for package '$importTarget' found"))) + // Left(message(importNode, s"No source files for package '$importTarget' found")) + else Right(pkgSources) + parsedProgram <- Parser.parse(nonEmptyPkgSources, Source.getPackageInfo(nonEmptyPkgSources.head, config.projectRoot), specOnly = true)(config) + errorsInTransitivePackages = parsedProgram.imports + .map(importNode => { + val directImportTarget = RegularImport(importNode.importPath) + if (parserPendingPackages.contains(directImportTarget)) { + // package cycle detected + val importNodeStart = parsedProgram.positions.positions.getStart(importNode) + parserKnownImportCycles += ImportCycle(importNode, importNodeStart, parserPendingPackages) + println(s"cycle detected: ${importTarget} has import ${directImportTarget} that occurs in ${parserKnownImportCycles}") + Left(Vector(CyclicImportError(s"Cyclic package import detected starting with package '$packageTarget'"))) + // val cycle = parserPendingPackages + // Left(message(importNode, s"Package '$importTarget' is part of this import cycle: ${cycle.mkString("[", ", ", "]")}")) + } else { + parseRecursively(directImportTarget)(config) + } + }) + .flatMap(_.left.getOrElse(Vector.empty)) + res <- if (errorsInTransitivePackages.isEmpty) Right(parsedProgram) else Left(errorsInTransitivePackages) + } yield res + /* + val res: Either[Messages, PPackage] = for { + nonEmptyPkgSources <- if (pkgSources.isEmpty) + // Left(Vector(NotFoundError(s"No source files for package '$importTarget' found"))) + Left(message(importNode, s"No source files for package '$importTarget' found")) + else Right(pkgSources) + parsedProgram <- Parser.parse(nonEmptyPkgSources, Source.getPackageInfo(nonEmptyPkgSources.head, config.projectRoot), specOnly = true)(config) + directImportTargets = parsedProgram.imports // .map(i => RegularImport(i.importPath)) + errorsInTransitivePackages: Messages = directImportTargets + .map(directImportTarget => { + if (parserPendingPackages.contains(directImportTarget)) { + // package cycle detected + parserKnownImportCycles += parserPendingPackages + // Left(Vector(CyclicImportError(s"Cyclic package import detected starting with package '$packageTarget'"))) + val cycle = parserPendingPackages + Left(message(importNode, s"Package '$importTarget' is part of this import cycle: ${cycle.mkString("[", ", ", "]")}")) + } else { + parseRecursively(directImportTarget)(config) + } + }) + .flatMap(_.left.getOrElse(noMessages)) + res <- if (errorsInTransitivePackages.isEmpty) Right(parsedProgram) else Left(errorsInTransitivePackages) + } yield res + */ + parserPendingPackages = parserPendingPackages.filterNot(_ == importTarget) + parserContextMap = parserContextMap + (packageTarget -> res.map(pkg => (pkgSources, pkg))) + res + } + + /** + * returns all parser errors and cyclic errors transitively found in imported packages + */ + def computeCycles(importTarget: AbstractImport): Vector[VerifierError] = { + parserPendingPackages = parserPendingPackages :+ importTarget + val abstractPackage = AbstractPackage(importTarget)(config) + val res = for { + res <- parseManager.getResult(abstractPackage) + (_, ast) = res + directImportTargets = ast.imports + errorsInTransitivePackages = directImportTargets + .flatMap(importNode => { + val directImportTarget = RegularImport(importNode.importPath) + if (parserPendingPackages.contains(directImportTarget)) { + // package cycle detected + val importNodeStart = ast.positions.positions.getStart(importNode) + parserKnownImportCycles += ImportCycle(importNode, importNodeStart, parserPendingPackages) + Vector(CyclicImportError(s"Cyclic package import detected starting with package '$directImportTarget'")) + // val cycle = parserPendingPackages + // message(importNode, s"Package '$importTarget' is part of this import cycle: ${cycle.mkString("[", ", ", "]")}") + } else { + computeCycles(directImportTarget) + } + }) + res <- if (errorsInTransitivePackages.isEmpty) Right(ast) else Left(errorsInTransitivePackages) + } yield res + parserPendingPackages = parserPendingPackages.filterNot(_ == importTarget) + res.left.getOrElse(Vector.empty) } + /* + def parseRecursively(pkg: PPackage)(config: Config): Either[Vector[VerifierError], PPackage] = { + val imports = Seq(BuiltInImport) ++ + pkg.imports.map(i => RegularImport(i.importPath)) + imports.map(importTarget => { + parserPendingPackages = parserPendingPackages :+ importTarget + val pkgSources = PackageResolver.resolveSources(importTarget)(config) + .getOrElse(Vector()) + .map(_.source) + val res = for { + nonEmptyPkgSources <- if (pkgSources.isEmpty) + Left(Vector(NotFoundError(s"No source files for package '$importTarget' found"))) + else Right(pkgSources) + parsedProgram <- Parser.parse(nonEmptyPkgSources, Source.getPackageInfo(nonEmptyPkgSources.head, config.projectRoot), specOnly = true)(config) + }) + + } + */ /** * Returns all package names that lie on the cycle of imports or none if no cycle was found */ - def getImportCycle(importTarget: AbstractImport): Option[Vector[AbstractImport]] = knownImportCycles.find(_.contains(importTarget)) + def getParserImportCycle(importTarget: AbstractImport): Option[ImportCycle] = + parserKnownImportCycles.find(_.cyclicPackages.contains(importTarget)) - def getContexts: Iterable[ExternalTypeInfo] = contextMap.values.collect { case Right(info) => info } + case class ParseJob(importTarget: AbstractImport) extends Job[Either[Vector[VerifierError], (Vector[Source], PPackage)]] { + def compute(): Either[Vector[VerifierError], (Vector[Source], PPackage)] = { + println(s"start parsing $importTarget") + val startMs = System.currentTimeMillis() + val pkgSources = PackageResolver.resolveSources(importTarget)(config) + .getOrElse(Vector()) + .map(_.source) + for { + nonEmptyPkgSources <- if (pkgSources.isEmpty) + Left(Vector(NotFoundError(s"No source files for package '$importTarget' found"))) + // Left(message(importNode, s"No source files for package '$importTarget' found")) + else Right(pkgSources) + parsedProgram <- Parser.parse(nonEmptyPkgSources, Source.getPackageInfo(nonEmptyPkgSources.head, config.projectRoot), specOnly = true)(config) + durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f" + _ = println(s"parsing $importTarget done (took ${durationS}s)") + // submit jobs to parse dependent packages: + _ = parsedProgram.imports.foreach(importNode => { + val directImportTarget = RegularImport(importNode.importPath) + val directImportPackage = AbstractPackage(directImportTarget)(config) + parseManager.addIfAbsent(directImportPackage, ParseJob(directImportTarget))(executionContext) + }) + } yield (pkgSources, parsedProgram) + } + } + + val parseManager = new TaskManager[AbstractPackage, Either[Vector[VerifierError], (Vector[Source], PPackage)]](config) + def parse(importTarget: AbstractImport): Unit = { + val abstractPackage = AbstractPackage(importTarget)(config) + val parseJob = ParseJob(importTarget) + parseManager.addIfAbsent(abstractPackage, parseJob)(executionContext) + } + + case class TypeCheckJob(pkgSources: Vector[Source], pkg: PPackage, context: Context) extends Job[Either[Vector[VerifierError], ExternalTypeInfo]] { + def compute(): Either[Vector[VerifierError], ExternalTypeInfo] = { + println(s"start type-checking ${pkg.info.id}") + val startMs = System.currentTimeMillis() + val res = Info.check(pkg, pkgSources, context)(config) + val durationS = f"${(System.currentTimeMillis() - startMs) / 1000f}%.1f" + println(s"type-checking ${pkg.info.id} done (took ${durationS}s)") + res + } + } + + case class FailureJob(errs: Vector[VerifierError]) extends Job[Either[Vector[VerifierError], ExternalTypeInfo]] { + def compute(): Either[Vector[VerifierError], ExternalTypeInfo] = Left(errs) + } + + /* + lazy val typeContextMap: Map[AbstractPackage, Future[Either[Vector[VerifierError], ExternalTypeInfo]]] = + parserContextMap.map{ case (abstractPackage, value) => (abstractPackage, value match { + case Right((pkgSources, pkg)) => + if (parallelizeTypechecking) Future { typeCheck(pkgSources, pkg) }(executionContext) + else { + val res = typeCheck(pkgSources, pkg) + if (res.isLeft) { + println(s"type-checking ${abstractPackage} failed: ${res.left.get}") + } + Future.successful(res) + } + case Left(errs) => Future.successful(Left(errs)) + })} + */ + private val typeCheckManager = new TaskManager[AbstractPackage, Either[Vector[VerifierError], ExternalTypeInfo]](config) + def typeCheck(): Unit = { + /*parserContextMap.foreach { case (abstractPackage, parseResult) => + val typeCheckJob = parseResult match { + case Right((pkgSources, pkg)) => TypeCheckJob(pkgSources, pkg, this) + case Left(errs) => FailureJob(errs) + } + println(s"adding task $abstractPackage") + typeCheckManager.addIfAbsent(abstractPackage, typeCheckJob)(executionContext) + } + */ + parseManager.getAllResultsWithKeys.foreach { case (abstractPackage, parseResult) => + val typeCheckJob = parseResult match { + case Right((pkgSources, pkg)) => TypeCheckJob(pkgSources, pkg, this) + case Left(errs) => FailureJob(errs) + } + println(s"adding task $abstractPackage") + // since we're adding the packages in arbitrary order, we cannot directly run the task in SEQUENTIAL mode because + // depending packages might not have been inserted yet + typeCheckManager.addIfAbsent(abstractPackage, typeCheckJob, insertOnly = config.typeCheckMode == TypeCheckMode.Sequential)(executionContext) + } + } + /* + lazy val jobMap: Map[AbstractPackage, Job] = + parserContextMap.transform { case (_, value) => value match { + case Right((pkgSources, pkg)) => TypeCheckJob(pkgSources, pkg, this) + case Left(errs) => FailureJob(errs) + }} + */ - def getExternalErrors: Vector[VerifierError] = contextMap.values.collect { case Left(errs) => errs }.flatten.toVector + def typeCheckSequentially(): Unit = { + /* + val jobs = jobMap.toVector.sorted(Ordering.by[(AbstractPackage, Job), Int](_._1.hashCode())) + println(s"typeCheckSequentially: ${jobs.map(_._1)}") + jobs.foreach { case (abstractPackage, job) => + // println(s"typeCheckSequentially: $abstractPackage") + job.call() } + */ + // NOP + } + + def typeCheckInParallel(): Unit = { + // NOP + // jobMap.foreach { case (_, job) => Future{ job.call() }(executionContext) } + } + /* + lazy val typeContextMap: Map[AbstractPackage, Future[Either[Vector[VerifierError], ExternalTypeInfo]]] = + jobMap.transform { case (_, job) => job.getFuture } + */ +// /** stores the results of all imported packages that have been parsed and type checked so far */ +// private var contextMap: Map[AbstractPackage, Either[Vector[VerifierError], ExternalTypeInfo]] = ListMap[AbstractPackage, Either[Vector[VerifierError], ExternalTypeInfo]]() +// /** keeps track of the package dependencies that are currently resolved. This information is used to detect cycles */ +// private var pendingPackages: Vector[AbstractImport] = Vector() +// /** stores all cycles that have been discovered so far */ +// private var knownImportCycles: Set[Vector[AbstractImport]] = Set() +// +// def addPackage(importTarget: AbstractImport, typeInfo: ExternalTypeInfo)(config: Config): Unit = { +// val packageTarget = AbstractPackage(importTarget)(config) +// pendingPackages = pendingPackages.filterNot(_ == importTarget) +// contextMap = contextMap + (packageTarget -> Right(typeInfo)) +// } +// +// def addErrenousPackage(importTarget: AbstractImport, errors: Vector[VerifierError])(config: Config): Unit = { +// val packageTarget = AbstractPackage(importTarget)(config) +// pendingPackages = pendingPackages.filterNot(_ == importTarget) +// contextMap = contextMap + (packageTarget -> Left(errors)) +// } +// +// def getTypeInfo(importTarget: AbstractImport)(config: Config): Option[Either[Vector[VerifierError], ExternalTypeInfo]] = { +// val packageTarget = AbstractPackage(importTarget)(config) +// contextMap.get(packageTarget) match { +// case s@Some(_) => s +// case _ => { +// // there is no entry yet and package resolution might need to resolve multiple depending packages +// // keep track of these packages in pendingPackages until either type information or an error is added to contextMap +// if (pendingPackages.contains(importTarget)) { +// // package cycle detected +// knownImportCycles += pendingPackages +// Some(Left(Vector(CyclicImportError(s"Cyclic package import detected starting with package '$packageTarget'")))) +// } else { +// pendingPackages = pendingPackages :+ importTarget +// None +// } +// } +// } +// } +// +// /** +// * Returns all package names that lie on the cycle of imports or none if no cycle was found +// */ +// def getImportCycle(importTarget: AbstractImport): Option[Vector[AbstractImport]] = knownImportCycles.find(_.contains(importTarget)) +// +// def getContexts: Iterable[ExternalTypeInfo] = contextMap.values.collect { case Right(info) => info } +// +// def getExternalErrors: Vector[VerifierError] = contextMap.values.collect { case Left(errs) => errs }.flatten.toVector + + def getContexts: Iterable[ExternalTypeInfo] = + // typeContextMap.values.map(fut => Await.result(fut, Duration.Inf)).collect { case Right(info) => info } + typeCheckManager.getAllResults.collect { case Right(info) => info } + /* + def getTypeInfoNonBlocking(importTarget: AbstractImport)(config: Config): Option[Future[Either[Vector[VerifierError], ExternalTypeInfo]]] = { + val packageTarget = AbstractPackage(importTarget)(config) + typeContextMap.get(packageTarget) + } + + def getTypeInfo(importTarget: AbstractImport)(config: Config): Option[Either[Vector[VerifierError], ExternalTypeInfo]] = + getTypeInfoNonBlocking(importTarget)(config).map(Await.result(_, Duration.Inf)) + + */ + + /* + def startTypeChecking(): Unit = { + config.typeCheckMode match { + case TypeCheckMode.Parallel => typeCheckInParallel() + case TypeCheckMode.Sequential => typeCheckSequentially() + case TypeCheckMode.Lazy => // don't do anything yet + } + } + */ + + def getTypeInfo(importTarget: AbstractImport)(config: Config): Either[Vector[VerifierError], ExternalTypeInfo] = { + val packageTarget = AbstractPackage(importTarget)(config) + /* + Violation.violation(typeContextMap.contains(packageTarget), s"expected that a job for ${packageTarget} but found none") + val fut = typeContextMap(packageTarget) + Await.result(fut, Duration.Inf) + */ + /* + Violation.violation(jobMap.contains(packageTarget), s"expected that a job for ${packageTarget} but found none") + val job = jobMap(packageTarget) + config.typeCheckMode match { + case TypeCheckMode.Lazy => job.call() + case TypeCheckMode.Sequential => + // note that we cannot await the future here as type-checking of this package might not have started yet. + // Thus, we use `.call()` that either returns a previously calculated type-checking result or will calculate it. + job.call() + case TypeCheckMode.Parallel => Await.result(job.getFuture, Duration.Inf) + } + */ + typeCheckManager.getResult(packageTarget) + } } - def check(pkg: PPackage, sources: Vector[Source], context: Context = new Context, isMainContext: Boolean = false)(config: Config): Either[Vector[VerifierError], TypeInfo with ExternalTypeInfo] = { + + def check(pkg: PPackage, sources: Vector[Source], context: Context /*= new Context()*/, isMainContext: Boolean = false)(config: Config): Either[Vector[VerifierError], TypeInfo with ExternalTypeInfo] = { val tree = new GoTree(pkg) // println(program.declarations.head) // println("-------------------") // println(tree) val info = new TypeInfoImpl(tree, context, isMainContext)(config: Config) - val errors = info.errors + def createImportError(importNode: PImport, errs: Vector[VerifierError]): Messages = { + val importTarget = RegularImport(importNode.importPath) + // create an error message located at the import statement to indicate errors in the imported package + // we distinguish between parse and type errors, cyclic imports, and packages whose source files could not be found + val notFoundErr = errs.collectFirst { case e: NotFoundError => e } + // alternativeErr is a function to compute the message only when needed + val alternativeErr = () => context.getParserImportCycle(importTarget) match { + case Some(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("[", ", ", "]")}") + case _ => message(importNode, s"Package '$importTarget' contains errors: $errs") + } + notFoundErr.map(e => message(importNode, e.message)) + .getOrElse(alternativeErr()) + } + + //val parserMessages = noMessages + val parserMessages = if (isMainContext) { + val sequential = false + val parsingStartMs = System.currentTimeMillis() + val messages = if (sequential) { + // parse BuiltInImport + val builtInParseResult = context.parseRecursively(BuiltInImport)(config) + val builtInMessages = if (builtInParseResult.isRight) noMessages else message(pkg, s"Parsing package with Gobra's built-in definitions failed. This is an internal bug.") + + val importedPackagesMessages = pkg.imports.flatMap(importNode => { + val importTarget = RegularImport(importNode.importPath) + val parseResult = context.parseRecursively(importTarget)(config) + parseResult.left.map(errs => createImportError(importNode, errs)).left.getOrElse(noMessages) + }) + + builtInMessages ++ importedPackagesMessages + } else { + // parse BuiltInImport + context.parse(BuiltInImport) + + pkg.imports.foreach(importNode => { + val importTarget = RegularImport(importNode.importPath) + context.parse(importTarget) + }) + + // collect parse errors and cyclic import errors: + val builtInParseErrors = context.computeCycles(BuiltInImport) + val builtInMessages = if (builtInParseErrors.isEmpty) noMessages else message(pkg, s"Parsing package with Gobra's built-in definitions failed. This is an internal bug.") + + val importedPackagesMessages = pkg.imports.flatMap(importNode => { + val importTarget = RegularImport(importNode.importPath) + val parseErrors = context.computeCycles(importTarget) + if (parseErrors.isEmpty) noMessages else createImportError(importNode, parseErrors) + }) + + builtInMessages ++ importedPackagesMessages + } + val durationS = f"${(System.currentTimeMillis() - parsingStartMs) / 1000f}%.1f" + println(s"parsing done, took ${durationS}s, ${messages.length} errors found") + /* + val imports = Vector(BuiltInImport) ++ + pkg.imports.map(i => RegularImport(i.importPath)) + val parseResult = imports.map(importTarget => { + context.parseRecursively(importTarget)(config) + }) + val transitiveParseErrors = parseResult.flatMap(res => res.left.getOrElse(Vector.empty)) + if (transitiveParseErrors.nonEmpty) { + println(s"parse error encountered") + println(transitiveParseErrors) + return Left(transitiveParseErrors) + } + println(s"parsing was fine") + */ + + messages + } else { + noMessages + } + + val typeCheckingStartMs = System.currentTimeMillis() + if (isMainContext && parserMessages.isEmpty) { + // context.startTypeChecking() + context.typeCheck() + } + + // val errors = info.errors + val errors = if (parserMessages.nonEmpty) parserMessages else { + info.errors + } + if (isMainContext && errors.isEmpty) { + val durationS = f"${(System.currentTimeMillis() - typeCheckingStartMs) / 1000f}%.1f" + println(s"type-checking done, took ${durationS}s (in mode ${config.typeCheckMode})") + } val sourceNames = sources.map(_.name) // use `sources` instead of `context.inputs` for reporting such that the message is correctly attributed in case of imports diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala index 896553697..4dc0f9bc9 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala @@ -405,6 +405,7 @@ trait MemberResolution { this: TypeInfoImpl => // TODO: move this method to another file def getTypeChecker(importTarget: AbstractImport, errNode: PNode): Either[Messages, ExternalTypeInfo] = { + /* def parseAndTypeCheck(importTarget: AbstractImport): Either[Vector[VerifierError], ExternalTypeInfo] = { val pkgSources = PackageResolver.resolveSources(importTarget)(config) .getOrElse(Vector()) @@ -425,14 +426,15 @@ trait MemberResolution { this: TypeInfoImpl => ) res } - + */ def createImportError(errs: Vector[VerifierError]): Messages = { // create an error message located at the import statement to indicate errors in the imported package // we distinguish between parse and type errors, cyclic imports, and packages whose source files could not be found val notFoundErr = errs.collectFirst { case e: NotFoundError => e } // alternativeErr is a function to compute the message only when needed - val alternativeErr = () => context.getImportCycle(importTarget) match { - case Some(cycle) => message(errNode, s"Package '$importTarget' is part of this import cycle: ${cycle.mkString("[", ", ", "]")}") + val alternativeErr = () => context.getParserImportCycle(importTarget) match { + case Some(cycle) => + message(errNode, s"Package '$importTarget' is part of the following import cycle that involves the import ${cycle.importNodeCausingCycle}: ${cycle.cyclicPackages.mkString("[", ", ", "]")}") case _ => message(errNode, s"Package '$importTarget' contains errors: $errs") } notFoundErr.map(e => message(errNode, e.message)) @@ -440,7 +442,15 @@ trait MemberResolution { this: TypeInfoImpl => } // check if package was already parsed, otherwise do parsing and type checking: + /* val cachedInfo = context.getTypeInfo(importTarget)(config) - cachedInfo.getOrElse(parseAndTypeCheck(importTarget)).left.map(createImportError) + if (cachedInfo.isEmpty) { + println(s"package $importTarget is not contained in context") + } + Violation.violation(cachedInfo.nonEmpty, s"package $importTarget is not contained in context") + cachedInfo.get.left.map(createImportError) + // cachedInfo.getOrElse(parseAndTypeCheck(importTarget)).left.map(createImportError) + */ + context.getTypeInfo(importTarget)(config).left.map(createImportError) } }