From 169d0914282e52de162be7f801bc2b36c8c4f8d6 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Wed, 15 Mar 2023 19:46:48 +0100 Subject: [PATCH] fixes parser error messages --- .../scala/viper/gobra/frontend/Parser.scala | 152 ++++++++++++++---- .../viper/gobra/reporting/VerifierError.scala | 3 +- .../features/import/import-fail1.gobra | 10 ++ .../features/import/import-fail2.gobra | 12 ++ .../features/import/import-fail3.gobra | 12 ++ .../invalid_package_clause1.gobra | 4 + .../invalid_package_clause2.gobra | 4 + .../import/parse_error/parse_error.gobra | 8 + .../features/stubs/stubs-fail0.gobra | 9 +- .../features/stubs/stubs-fail1.gobra | 10 -- 10 files changed, 181 insertions(+), 43 deletions(-) create mode 100644 src/test/resources/regressions/features/import/import-fail1.gobra create mode 100644 src/test/resources/regressions/features/import/import-fail2.gobra create mode 100644 src/test/resources/regressions/features/import/import-fail3.gobra create mode 100644 src/test/resources/regressions/features/import/invalid_package_clause/invalid_package_clause1.gobra create mode 100644 src/test/resources/regressions/features/import/invalid_package_clause/invalid_package_clause2.gobra create mode 100644 src/test/resources/regressions/features/import/parse_error/parse_error.gobra delete mode 100644 src/test/resources/regressions/features/stubs/stubs-fail1.gobra diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala index f83a56b86..e42c37afc 100644 --- a/src/main/scala/viper/gobra/frontend/Parser.scala +++ b/src/main/scala/viper/gobra/frontend/Parser.scala @@ -30,7 +30,7 @@ import scala.concurrent.{Await, Future} object Parser { type ParseSuccessResult = (Vector[Source], PPackage) - type ParseResult = Either[Vector[VerifierError], ParseSuccessResult] + type ParseResult = Either[Vector[ParserError], ParseSuccessResult] class ParseManager(config: Config, executionContext: GobraExecutionContext) extends LazyLogging { private val manager = new TaskManager[AbstractPackage, Future[ParseResult]](TaskManagerMode.Parallel) @@ -57,19 +57,50 @@ object Parser { // before parsing, get imports and add these parse jobs val imports = fastParse(preprocessedSources) val preambleParsingDurationMs = System.currentTimeMillis() - startPreambleParsingMs - val futs = imports.map{ case (directImportTarget, optSourcePos) => { + // val importResults: Set[Either[Vector[VerifierError], Future[ParseResult]]] = imports.map{ case (directImportTarget, importErrorFactory) => { + val importResults: Set[Future[ParseResult]] = imports.map { case (directImportTarget, importErrorFactory) => val directImportPackage = AbstractPackage(directImportTarget)(config) + val nonEmptyImportedSources = for { + resolveSourceResults <- PackageResolver.resolveSources(directImportTarget)(config) + importedSources = resolveSourceResults.map(_.source) + nonEmptyImportedSources <- if (importedSources.isEmpty) Left(s"No source files for package '$directImportTarget' found") else Right(importedSources) + } yield nonEmptyImportedSources + + nonEmptyImportedSources.fold( + errMsg => { + val errs = importErrorFactory(errMsg) + manager.addIfAbsent(directImportPackage, ParseFailureJob(errs))(executionContext) + Future.successful(Left(errs)) + }, + nonEmptySources => { + manager.addIfAbsent(directImportPackage, ParseSourcesJob(nonEmptySources, directImportPackage))(executionContext) + manager.getFuture(directImportPackage).flatten + .map { + case Left(_) => Left(importErrorFactory(s"Imported package contains errors")) + case success => success + }(executionContext) + }) + /* val importedSources = PackageResolver.resolveSources(directImportTarget)(config) .getOrElse(Vector()) .map(_.source) if (importedSources.isEmpty) { - manager.addIfAbsent(directImportPackage, ParseFailureJob(Vector(NotFoundError(s"No source files for package '$directImportTarget' found", optSourcePos))))(executionContext) - manager.getFuture(directImportPackage) // we do not flatten here as we only need to await the job's creation + val errMsg = s"No source files for package '$directImportTarget' found" + manager.addIfAbsent(directImportPackage, ParseFailureJob(Vector(NotFoundError(errMsg))))(executionContext) + Future.successful(Left(importErrorFactory(errMsg))) } else { manager.addIfAbsent(directImportPackage, ParseSourcesJob(importedSources, directImportPackage))(executionContext) - manager.getFuture(directImportPackage) // we do not flatten here as we only need to await the job's creation + manager.getFuture(directImportPackage).flatten + .map { + case Left(errs) => Left(importErrorFactory(s"Imported package contains errors")) + case success => success + }(executionContext) } - }} + */ + } + + // val (importFailures, futs) = importResults.partitionMap(identity) + // val flatImportFailures = importFailures.toVector.flatten val startMs = System.currentTimeMillis() val res = for { @@ -84,32 +115,66 @@ object Parser { } implicit val executor: GobraExecutionContext = executionContext + + Future.sequence(importResults) + .map(dependencyResults => { + val (importErrors, _) = dependencyResults.partitionMap(identity) + val flatImportFailures = importErrors.toVector.flatten + if (flatImportFailures.isEmpty) { + // we only post-process if dependent packages where successful + Parser.postprocess(res, specOnly = specOnly)(config) + } else { + config.reporter report ParserErrorMessage(flatImportFailures.head.position.get.file, flatImportFailures) + Left(flatImportFailures) + } + /* + if (dependencyResults.forall(_.isRight)) { + // we only post-process if dependent packages where successful + Parser.postprocess(res, specOnly = specOnly)(config) + } else { + // we return an empty list of errors not to duplicate errors + Left(Vector.empty) + } + */ + }) + /* Future.sequence(futs) .map(_ => res) + */ } - private def fastParse(preprocessedInput: Vector[Source]): Set[(AbstractImport, Option[SourcePosition])] = { - def getImportPaths(preprocessedSource: Source): Set[(RegularImport, Option[SourcePosition])] = { + type ImportErrorFactory = String => Vector[ParserError] + private def fastParse(preprocessedInput: Vector[Source]): Set[(AbstractImport, ImportErrorFactory)] = { + def getImportPaths(preprocessedSource: Source): Set[(RegularImport, ImportErrorFactory)] = { processPreamble(preprocessedSource)(config) .map(preamble => { val pom = preamble.positions preamble.imports .map(importNode => { - val nodeStart = pom.positions.getStart(importNode) - val nodeFinish = pom.positions.getFinish(importNode) - val nodePos = (nodeStart, nodeFinish) match { - case (Some(start), Some(finish)) => Some(pom.translate(start, finish)) - case _ => None + 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), nodePos) + (RegularImport(importNode.importPath), importErrorFactory) }) .toSet }) .getOrElse(Set.empty) } - val builtInImportTuple = (BuiltInImport, None) - preprocessedInput.flatMap(getImportPaths).toSet + builtInImportTuple + val explicitImports: Set[(AbstractImport, ImportErrorFactory)] = preprocessedInput.flatMap(getImportPaths).toSet + if (pkgInfo.isBuiltIn) { + explicitImports + } else { + val builtInImportErrorFactory: ImportErrorFactory = (errMsg: String) => { + val err = Vector(ParserError(errMsg, None)) + config.reporter report ParserErrorMessage(err.head.position.get.file, err) + err + } + val builtInImportTuple = (BuiltInImport, builtInImportErrorFactory) + explicitImports + builtInImportTuple + } } } @@ -126,7 +191,7 @@ object Parser { lazy val specOnly: Boolean = true } - case class ParseFailureJob(errs: Vector[NotFoundError]) extends Job[Future[ParseResult]] { + case class ParseFailureJob(errs: Vector[ParserError]) extends Job[Future[ParseResult]] { override def compute(): Future[ParseResult] = Future.successful[ParseResult](Left(errs)) } @@ -140,6 +205,15 @@ object Parser { if (failedResults.isEmpty) Right(successfulResults.toMap) else Left(failedResults.toMap) } + + def getSuccessResults(executionContext: GobraExecutionContext): Map[AbstractPackage, ParseSuccessResult] = { + implicit val executor: GobraExecutionContext = executionContext + val futs = manager.getAllFutures.map { case (key, fut) => fut.flatten.map(res => (key, res)) } + val results = Await.result(Future.sequence(futs), Duration.Inf) + results + .collect { case (key, Right(res)) => (key, res) } + .toMap + } } /** @@ -160,9 +234,13 @@ object Parser { def parse(config: Config, pkgInfo: PackageInfo)(executionContext: GobraExecutionContext): Either[Vector[VerifierError], Map[AbstractPackage, ParseSuccessResult]] = { val parseManager = new ParseManager(config, executionContext) + /* parseManager.parse(pkgInfo) val res = parseManager.getParseResults(executionContext).left.map(errMap => errMap.values.flatten.toVector) res + */ + val res = parseManager.parse(pkgInfo) + res.map(_ => parseManager.getSuccessResults(executionContext)) } def parse(input: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean = false)(config: Config): Either[Vector[VerifierError], PPackage] = { @@ -205,7 +283,8 @@ object Parser { if (config.cacheParser) parseSourceCached(preprocessedSource) else parseSource(preprocessedSource) } - private def process(preprocessedInputs: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[VerifierError], PPackage] = { + private def process(preprocessedInputs: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[ParserError], PPackage] = { + /* for { parseAst <- parseSources(preprocessedInputs, pkgInfo, specOnly = specOnly)(config) postprocessors = Seq( @@ -217,6 +296,23 @@ object Parser { case (e, _) => e } } yield postprocessedAst + */ + parseSources(preprocessedInputs, pkgInfo, specOnly = specOnly)(config) + } + + private def postprocess(processResult: Either[Vector[ParserError], (Vector[Source], PPackage)], specOnly: Boolean)(config: Config): Either[Vector[ParserError], (Vector[Source], PPackage)] = { + for { + successfulProcessResult <- processResult + (preprocessedInputs, parseAst) = successfulProcessResult + postprocessors = Seq( + new ImportPostprocessor(parseAst.positions.positions), + new TerminationMeasurePostprocessor(parseAst.positions.positions, specOnly = specOnly), + ) + postprocessedAst <- postprocessors.foldLeft[Either[Vector[ParserError], PPackage]](Right(parseAst)) { + case (Right(ast), postprocessor) => postprocessor.postprocess(ast)(config) + case (e, _) => e + } + } yield (preprocessedInputs, postprocessedAst) } type SourceCacheKey = String @@ -226,7 +322,7 @@ object Parser { // we cache entire packages and not individual files (i.e. PProgram) as this saves us from copying over positional information // from one to the other position manager. Also, this transformation of copying positional information results in // differen PPackage instances that is problematic for caching type-check results. - private val packageCache: ConcurrentMap[PackageCacheKey, Either[Vector[VerifierError], PPackage]] = new ConcurrentHashMap() + private val packageCache: ConcurrentMap[PackageCacheKey, Either[Vector[ParserError], PPackage]] = new ConcurrentHashMap() /** computes the key for caching the preamble of a particular source. This takes the name and the source's content into account */ private def getPreambleCacheKey(source: Source): SourceCacheKey = { @@ -249,8 +345,8 @@ object Parser { packageCache.clear() } - private def parseSources(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[VerifierError], PPackage] = { - def parseSourcesCached(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[VerifierError], PPackage] = { + private def parseSources(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[ParserError], PPackage] = { + def parseSourcesCached(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[ParserError], PPackage] = { var cacheHit: Boolean = true val res = packageCache.computeIfAbsent(getPackageCacheKey(sources, pkgInfo, specOnly), _ => { cacheHit = false @@ -267,7 +363,7 @@ object Parser { } /** parses a package not taking the package cache but only the program cache into account */ - private def parseSourcesUncached(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[VerifierError], PPackage] = { + private def parseSourcesUncached(sources: Vector[Source], pkgInfo: PackageInfo, specOnly: Boolean)(config: Config): Either[Vector[ParserError], PPackage] = { val positions = new Positions val pom = new PositionManager(positions) lazy val rewriter = new PRewriter(pom.positions) @@ -388,15 +484,15 @@ object Parser { } } - def postprocess(pkg: PPackage)(config: Config): Either[Vector[VerifierError], PPackage] + def postprocess(pkg: PPackage)(config: Config): Either[Vector[ParserError], PPackage] } private class ImportPostprocessor(override val positions: Positions) extends Postprocessor { /** * Replaces all PQualifiedWoQualifierImport by PQualifiedImport nodes */ - def postprocess(pkg: PPackage)(config: Config): Either[Vector[VerifierError], PPackage] = { - def createError(n: PImplicitQualifiedImport, errorMsg: String): Vector[VerifierError] = { + def postprocess(pkg: PPackage)(config: Config): Either[Vector[ParserError], PPackage] = { + def createError(n: PImplicitQualifiedImport, errorMsg: String): Vector[ParserError] = { val err = pkg.positions.translate(message(n, s"Explicit qualifier could not be derived (reason: '$errorMsg')"), ParserError) config.reporter report ParserErrorMessage(err.head.position.get.file, err) @@ -405,7 +501,7 @@ object Parser { // unfortunately Kiama does not seem to offer a way to report errors while applying the strategy // hence, we keep ourselves track of errors - var failedNodes: Vector[VerifierError] = Vector() + var failedNodes: Vector[ParserError] = Vector() def replace(n: PImplicitQualifiedImport): Option[PExplicitQualifiedImport] = { val qualifier = for { @@ -454,11 +550,11 @@ object Parser { * Note that we do not transform the body of pure functions and pure methods (e.g. by turning the body into a * postcondition) because this would result in a matching loop for recursive functions. */ - def postprocess(pkg: PPackage)(config: Config): Either[Vector[VerifierError], PPackage] = { + def postprocess(pkg: PPackage)(config: Config): Either[Vector[ParserError], PPackage] = { if (specOnly) replaceTerminationMeasures(pkg) else Right(pkg) } - private def replaceTerminationMeasures(pkg: PPackage): Either[Vector[VerifierError], PPackage] = { + private def replaceTerminationMeasures(pkg: PPackage): Either[Vector[ParserError], PPackage] = { def replace(spec: PFunctionSpec): PFunctionSpec = { val replacedMeasures = spec.terminationMeasures.map { case n@PTupleTerminationMeasure(_, cond) => PWildcardMeasure(cond).at(n) diff --git a/src/main/scala/viper/gobra/reporting/VerifierError.scala b/src/main/scala/viper/gobra/reporting/VerifierError.scala index 3798941c1..858c2f2ae 100644 --- a/src/main/scala/viper/gobra/reporting/VerifierError.scala +++ b/src/main/scala/viper/gobra/reporting/VerifierError.scala @@ -28,7 +28,8 @@ sealed trait VerifierError { var cached: Boolean = false } -case class NotFoundError(message: String, position: Option[SourcePosition]) extends VerifierError { +case class NotFoundError(message: String) extends VerifierError { + val position: Option[SourcePosition] = None val id = "not_found_error" } diff --git a/src/test/resources/regressions/features/import/import-fail1.gobra b/src/test/resources/regressions/features/import/import-fail1.gobra new file mode 100644 index 000000000..769bcd13c --- /dev/null +++ b/src/test/resources/regressions/features/import/import-fail1.gobra @@ -0,0 +1,10 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package main + +import ( + // the following package does not exist + //:: ExpectedOutput(parser_error) + "nopackagewhatsoever" +) \ No newline at end of file diff --git a/src/test/resources/regressions/features/import/import-fail2.gobra b/src/test/resources/regressions/features/import/import-fail2.gobra new file mode 100644 index 000000000..d39496255 --- /dev/null +++ b/src/test/resources/regressions/features/import/import-fail2.gobra @@ -0,0 +1,12 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package main + +// ##(-I ./) + +import ( + // note that package `parse_error` contains a parser error so the qualifier cannot be resolved + //:: ExpectedOutput(parser_error) + "parse_error" +) diff --git a/src/test/resources/regressions/features/import/import-fail3.gobra b/src/test/resources/regressions/features/import/import-fail3.gobra new file mode 100644 index 000000000..436d52cd7 --- /dev/null +++ b/src/test/resources/regressions/features/import/import-fail3.gobra @@ -0,0 +1,12 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package main + +// ##(-I ./) + +import ( + // note that `foo` contains a parser error so the qualifier cannot be resolved + //:: ExpectedOutput(parser_error) + "invalid_package_clause" +) diff --git a/src/test/resources/regressions/features/import/invalid_package_clause/invalid_package_clause1.gobra b/src/test/resources/regressions/features/import/invalid_package_clause/invalid_package_clause1.gobra new file mode 100644 index 000000000..5c8815c06 --- /dev/null +++ b/src/test/resources/regressions/features/import/invalid_package_clause/invalid_package_clause1.gobra @@ -0,0 +1,4 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package clause1 diff --git a/src/test/resources/regressions/features/import/invalid_package_clause/invalid_package_clause2.gobra b/src/test/resources/regressions/features/import/invalid_package_clause/invalid_package_clause2.gobra new file mode 100644 index 000000000..716f1038c --- /dev/null +++ b/src/test/resources/regressions/features/import/invalid_package_clause/invalid_package_clause2.gobra @@ -0,0 +1,4 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package clause2 diff --git a/src/test/resources/regressions/features/import/parse_error/parse_error.gobra b/src/test/resources/regressions/features/import/parse_error/parse_error.gobra new file mode 100644 index 000000000..142c3e3a6 --- /dev/null +++ b/src/test/resources/regressions/features/import/parse_error/parse_error.gobra @@ -0,0 +1,8 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package parseError + +// package foo has a source file but an invalid preamble, i.e., fails to parse +//:: ExpectedOutput(parser_error) +imp bla "bla" diff --git a/src/test/resources/regressions/features/stubs/stubs-fail0.gobra b/src/test/resources/regressions/features/stubs/stubs-fail0.gobra index 6ee25b286..f4a5bd7ef 100644 --- a/src/test/resources/regressions/features/stubs/stubs-fail0.gobra +++ b/src/test/resources/regressions/features/stubs/stubs-fail0.gobra @@ -3,7 +3,8 @@ package main -import ( - //:: ExpectedOutput(not_found_error) - "nopackagewhatsoever" -) \ No newline at end of file +import "net" + +// Should fail, package net does not contain member DoesNotExist +//:: ExpectedOutput(type_error) +func closePacketConn(conn net.DoesNotExist) error \ No newline at end of file diff --git a/src/test/resources/regressions/features/stubs/stubs-fail1.gobra b/src/test/resources/regressions/features/stubs/stubs-fail1.gobra deleted file mode 100644 index f4a5bd7ef..000000000 --- a/src/test/resources/regressions/features/stubs/stubs-fail1.gobra +++ /dev/null @@ -1,10 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -package main - -import "net" - -// Should fail, package net does not contain member DoesNotExist -//:: ExpectedOutput(type_error) -func closePacketConn(conn net.DoesNotExist) error \ No newline at end of file