From 9e28d609b976ba8cbb7d8a60da96ee7e373a65d1 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Thu, 16 Jan 2025 16:02:04 +0100 Subject: [PATCH 01/10] removes Violation in --- src/main/scala/viper/gobra/Gobra.scala | 6 +- .../scala/viper/gobra/frontend/Config.scala | 65 +++++++++++-------- .../scala/viper/gobra/frontend/Parser.scala | 31 +++++---- .../scala/viper/gobra/frontend/Source.scala | 60 +++++++++-------- .../viper/gobra/frontend/info/Info.scala | 2 +- .../scala/viper/gobra/GobraPackageTests.scala | 2 +- src/test/scala/viper/gobra/GobraTests.scala | 2 +- .../gobra/parsing/GobraParserTests.scala | 4 +- .../gobra/parsing/ParserTestFrontend.scala | 14 ++-- 9 files changed, 102 insertions(+), 84 deletions(-) diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala index f3190a3cb..ac193d353 100644 --- a/src/main/scala/viper/gobra/Gobra.scala +++ b/src/main/scala/viper/gobra/Gobra.scala @@ -224,7 +224,7 @@ class Gobra extends GoVerifier with GoIdeVerifier { } }) val (errors, inFileConfigs) = inFileEitherConfigs.partitionMap(identity) - if (errors.nonEmpty) Left(errors.map(ConfigError)) + if (errors.nonEmpty) Left(errors.flatten) else { // start with original config `config` and merge in every in file config: val mergedConfig = inFileConfigs.flatten.foldLeft(config) { @@ -349,8 +349,8 @@ object GobraRunner extends GobraFrontend with StrictLogging { val scallopGobraConfig = new ScallopGobraConfig(args.toSeq) val config = scallopGobraConfig.config exitCode = config match { - case Left(validationError) => - logger.error(validationError) + case Left(errors) => + errors.foreach(err => logger.error(err.formattedMessage)) 1 case Right(config) => // Print copyright report diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 748f78909..43f8f919d 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -17,7 +17,7 @@ import viper.gobra.GoVerifier import viper.gobra.frontend.PackageResolver.FileResource import viper.gobra.frontend.Source.getPackageInfo import viper.gobra.util.TaskManagerMode.{Lazy, Parallel, Sequential, TaskManagerMode} -import viper.gobra.reporting.{FileWriterReporter, GobraReporter, StdIOReporter} +import viper.gobra.reporting.{ConfigError, FileWriterReporter, GobraReporter, StdIOReporter, VerifierError} import viper.gobra.util.{TaskManagerMode, TypeBounds, Violation} import viper.silver.ast.SourcePosition @@ -303,8 +303,8 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector } trait RawConfig { - /** converts a RawConfig to an actual `Config` for Gobra. Returns Left with an error message if validation fails. */ - def config: Either[String, Config] + /** converts a RawConfig to an actual `Config` for Gobra. Returns Left if validation fails. */ + def config: Either[Vector[VerifierError], Config] protected def baseConfig: BaseConfig protected def createConfig(packageInfoInputMap: Map[PackageInfo, Vector[Source]]): Config = Config( @@ -355,20 +355,22 @@ trait RawConfig { * This is for example used when parsing in-file configs. */ case class NoInputModeConfig(baseConfig: BaseConfig) extends RawConfig { - override lazy val config: Either[String, Config] = Right(createConfig(Map.empty)) + override lazy val config: Either[Vector[VerifierError], Config] = Right(createConfig(Map.empty)) } case class FileModeConfig(inputFiles: Vector[Path], baseConfig: BaseConfig) extends RawConfig { - override lazy val config: Either[String, Config] = { + override lazy val config: Either[Vector[VerifierError], Config] = { val sources = inputFiles.map(path => FileSource(path.toString)) - if (sources.isEmpty) Left(s"no input files have been provided") + if (sources.isEmpty) Left(Vector(ConfigError(s"no input files have been provided"))) else { // we do not check whether the provided files all belong to the same package // instead, we trust the programmer that she knows what she's doing. // If they do not belong to the same package, Gobra will report an error after parsing. // we simply use the first source's package info to create a single map entry: - val packageInfoInputMap = Map(getPackageInfo(sources.head, inputFiles.head) -> sources) - Right(createConfig(packageInfoInputMap)) + for { + pkgInfo <- getPackageInfo(sources.head, inputFiles.head) + packageInfoInputMap = Map(pkgInfo -> sources) + } yield createConfig(packageInfoInputMap) } } } @@ -387,19 +389,21 @@ trait PackageAndRecursiveModeConfig extends RawConfig { case class PackageModeConfig(projectRoot: Path = ConfigDefaults.DefaultProjectRoot.toPath, inputDirectories: Vector[Path], baseConfig: BaseConfig) extends PackageAndRecursiveModeConfig { - override lazy val config: Either[String, Config] = { + override lazy val config: Either[Vector[VerifierError], Config] = { val (errors, mappings) = inputDirectories.map { directory => val sources = getSources(directory, recursive = false, onlyFilesWithHeader = baseConfig.onlyFilesWithHeader) // we do not check whether the provided files all belong to the same package // instead, we trust the programmer that she knows what she's doing. // If they do not belong to the same package, Gobra will report an error after parsing. // we simply use the first source's package info to create a single map entry: - if (sources.isEmpty) Left(s"no sources found in directory ${directory}") - else Right((getPackageInfo(sources.head, projectRoot), sources)) + if (sources.isEmpty) Left(Vector(ConfigError(s"no sources found in directory $directory"))) + else for { + pkgInfo <- getPackageInfo(sources.head, projectRoot) + } yield pkgInfo -> sources }.partitionMap(identity) - if (errors.length == 1) Left(errors.head) - else if (errors.nonEmpty) Left(s"multiple errors have been found while localizing sources: ${errors.mkString(", ")}") - else Right(createConfig(mappings.toMap)) + for { + mappings <- if (errors.nonEmpty) Left(errors.flatten) else Right(mappings) + } yield createConfig(mappings.toMap) } } @@ -407,18 +411,25 @@ case class RecursiveModeConfig(projectRoot: Path = ConfigDefaults.DefaultProject includePackages: List[String] = ConfigDefaults.DefaultIncludePackages, excludePackages: List[String] = ConfigDefaults.DefaultExcludePackages, baseConfig: BaseConfig) extends PackageAndRecursiveModeConfig { - override lazy val config: Either[String, Config] = { - val pkgMap = getSources(projectRoot, recursive = true, onlyFilesWithHeader = baseConfig.onlyFilesWithHeader) - .groupBy(source => getPackageInfo(source, projectRoot)) - // filter packages: - .filter { case (pkgInfo, _) => (includePackages.isEmpty || includePackages.contains(pkgInfo.name)) && !excludePackages.contains(pkgInfo.name) } - // filter packages with zero source files: - .filter { case (_, pkgFiles) => pkgFiles.nonEmpty } - if (pkgMap.isEmpty) { - Left(s"No packages have been found that should be verified") - } else { - Right(createConfig(pkgMap)) - } + override lazy val config: Either[Vector[VerifierError], Config] = { + val sources = getSources(projectRoot, recursive = true, onlyFilesWithHeader = baseConfig.onlyFilesWithHeader) + val (errors, pkgInfos) = sources.map(source => { + for { + pkgInfo <- getPackageInfo(source, projectRoot) + } yield source -> pkgInfo + }).partitionMap(identity) + for { + pkgInfos <- if (errors.nonEmpty) Left(errors.flatten) else Right(pkgInfos) + pkgMap = pkgInfos + .groupBy { case (_, pkgInfo) => pkgInfo } + // we no longer need `pkgInfo` for the values: + .transform { case (_, values) => values.map(_._1) } + // filter packages: + .filter { case (pkgInfo, _) => (includePackages.isEmpty || includePackages.contains(pkgInfo.name)) && !excludePackages.contains(pkgInfo.name) } + // filter packages with zero source files: + .filter { case (_, pkgFiles) => pkgFiles.nonEmpty } + nonEmptyPkgMap <- if (pkgMap.isEmpty) Left(Vector(ConfigError(s"No packages have been found that should be verified"))) else Right(pkgMap) + } yield createConfig(nonEmptyPkgMap) } } @@ -943,7 +954,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals verify() - lazy val config: Either[String, Config] = rawConfig.config + lazy val config: Either[Vector[VerifierError], Config] = rawConfig.config // note that we use `recursive.isSupplied` instead of `recursive.toOption` because it defaults to `Some(false)` if it // was not provided by the user. Specifying a different default value does not seem to be respected. diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala index 300a3000f..2408ba941 100644 --- a/src/main/scala/viper/gobra/frontend/Parser.scala +++ b/src/main/scala/viper/gobra/frontend/Parser.scala @@ -11,7 +11,7 @@ import org.bitbucket.inkytonik.kiama.rewriting.{Cloner, PositionedRewriter, Stra import org.bitbucket.inkytonik.kiama.util.{Positions, Source} import org.bitbucket.inkytonik.kiama.util.Messaging.{error, message} import viper.gobra.ast.frontend._ -import viper.gobra.frontend.Source.{FromFileSource, TransformableSource} +import viper.gobra.frontend.Source.{FromFileSource, TransformableSource, getPackageInfo} import viper.gobra.reporting.{Source => _, _} import org.antlr.v4.runtime.{CharStreams, CommonTokenStream, DefaultErrorStrategy, ParserRuleContext} import org.antlr.v4.runtime.atn.PredictionMode @@ -33,8 +33,8 @@ import scala.concurrent.Future object Parser extends LazyLogging { type ParseSuccessResult = (Vector[Source], PPackage) - type ParseResult = Either[Vector[ParserError], ParseSuccessResult] - type ImportToSourceOrErrorMap = Vector[(AbstractPackage, Either[Vector[ParserError], Vector[Source]])] + type ParseResult = Either[Vector[VerifierError], ParseSuccessResult] + type ImportToPkgInfoOrErrorMap = Vector[(AbstractPackage, Either[Vector[VerifierError], (Vector[Source], PackageInfo)])] type PreprocessedSources = Vector[Source] class ParseManager(config: Config)(implicit executor: GobraExecutionContext) extends LazyLogging { @@ -53,7 +53,7 @@ object Parser extends LazyLogging { def pkgInfo: PackageInfo type ImportErrorFactory = String => Vector[ParserError] - protected def getImports(importNodes: Vector[PImport], pom: PositionManager): ImportToSourceOrErrorMap = { + protected def getImports(importNodes: Vector[PImport], pom: PositionManager): ImportToPkgInfoOrErrorMap = { val explicitImports: Vector[(AbstractImport, ImportErrorFactory)] = importNodes .map(importNode => { val importErrorFactory: ImportErrorFactory = (errMsg: String) => { @@ -74,13 +74,13 @@ object Parser extends LazyLogging { val errsOrSources = imports.map { case (directImportTarget, importErrorFactory) => val directImportPackage = AbstractPackage(directImportTarget)(config) - val nonEmptyImportedSources = for { - resolveSourceResults <- PackageResolver.resolveSources(directImportTarget)(config) + val sourcesAndPkgInfo = for { + resolveSourceResults <- PackageResolver.resolveSources(directImportTarget)(config).left.map(importErrorFactory) importedSources = resolveSourceResults.map(_.source) - nonEmptyImportedSources <- if (importedSources.isEmpty) Left(s"No source files for package '$directImportTarget' found") else Right(importedSources) - } yield nonEmptyImportedSources - val res = nonEmptyImportedSources.left.map(importErrorFactory) - (directImportPackage, res) + nonEmptyImportedSources <- if (importedSources.isEmpty) Left(importErrorFactory(s"No source files for package '$directImportTarget' found")) else Right(importedSources) + pkgInfo <- getPackageInfo(nonEmptyImportedSources.head, config.projectRoot) + } yield (nonEmptyImportedSources, pkgInfo) + (directImportPackage, sourcesAndPkgInfo) } errsOrSources } @@ -99,7 +99,7 @@ object Parser extends LazyLogging { def specOnly: Boolean var preambleParsingDurationMs: Long = 0 - private def getImportsForPackage(preprocessedSources: Vector[Source]): ImportToSourceOrErrorMap = { + private def getImportsForPackage(preprocessedSources: Vector[Source]): ImportToPkgInfoOrErrorMap = { val preambles = preprocessedSources .map(preprocessedSource => processPreamble(preprocessedSource)(config)) // we ignore imports in files that cannot be parsed: @@ -115,8 +115,8 @@ object Parser extends LazyLogging { // add imported packages to manager if not already imports.foreach { - case (directImportPackage, Right(nonEmptySources)) => - manager.addIfAbsent(directImportPackage, ParseSourcesJob(nonEmptySources, directImportPackage)) + case (directImportPackage, Right((nonEmptySources, pkgInfo))) => + manager.addIfAbsent(directImportPackage, ParseSourcesJob(nonEmptySources, pkgInfo)) case (directImportPackage, Left(errs)) => manager.addIfAbsent(directImportPackage, ParseFailureJob(errs)) } @@ -148,13 +148,12 @@ object Parser extends LazyLogging { } /** this job is used to parse all packages that are imported */ - private case class ParseSourcesJob(override val pkgSources: Vector[Source], pkg: AbstractPackage) extends ParseJob { + private case class ParseSourcesJob(override val pkgSources: Vector[Source], override val pkgInfo: PackageInfo) extends ParseJob { require(pkgSources.nonEmpty) - lazy val pkgInfo: PackageInfo = Source.getPackageInfo(pkgSources.head, config.projectRoot) lazy val specOnly: Boolean = true } - private case class ParseFailureJob(errs: Vector[ParserError]) extends Job[PreprocessedSources, ParseResult] { + private case class ParseFailureJob(errs: Vector[VerifierError]) extends Job[PreprocessedSources, ParseResult] { override protected def sequentialPrecompute(): PreprocessedSources = Vector.empty override protected def compute(precomputationResult: PreprocessedSources): ParseResult = diff --git a/src/main/scala/viper/gobra/frontend/Source.scala b/src/main/scala/viper/gobra/frontend/Source.scala index 46a258c7b..014393138 100644 --- a/src/main/scala/viper/gobra/frontend/Source.scala +++ b/src/main/scala/viper/gobra/frontend/Source.scala @@ -8,12 +8,12 @@ package viper.gobra.frontend import java.io.Reader import java.nio.file.{Files, Path, Paths} - import org.bitbucket.inkytonik.kiama.util.{FileSource, Filenames, IO, Source, StringSource} +import viper.gobra.reporting.{ParserError, VerifierError} import viper.gobra.util.Violation import viper.silver.ast.SourcePosition -import java.util.Objects +import java.util.Objects import viper.gobra.translator.Names import scala.io.BufferedSource @@ -51,31 +51,39 @@ object Source { /** * Returns an object containing information about the package a source belongs to. */ - def getPackageInfo(src: Source, projectRoot: Path): PackageInfo = { - - val isBuiltIn: Boolean = src match { - case FromFileSource(_, _, builtin) => builtin - case _ => false - } - - val packageName: String = PackageResolver.getPackageClause(src: Source) - .getOrElse(Violation.violation("Missing package clause in " + src.name)) - - /** - * A unique identifier for packages - */ - val packageId: String = { - val prefix = uniquePath(TransformableSource(src).toPath.toAbsolutePath.getParent, projectRoot).toString - if(prefix.nonEmpty) { - // The - is enough to unambiguously separate the prefix from the package name, since it can't occur in the package name - // per Go's spec (https://go.dev/ref/spec#Package_clause) - prefix + " - " + packageName - } else { - // Fallback case if the prefix is empty, for example if the directory of a FileSource is in the current directory - packageName + def getPackageInfo(src: Source, projectRoot: Path): Either[Vector[VerifierError], PackageInfo] = { + for { + packageName <- PackageResolver.getPackageClause(src: Source).toRight({ + val pos = Some(SourcePosition(src.toPath, 0, 0)) + Vector(ParserError("Missing package clause", pos)) + }) + isBuiltIn = src match { + case FromFileSource(_, _, builtin) => builtin + case _ => false } - } - new PackageInfo(packageId, packageName, isBuiltIn) + /** A unique identifier for packages */ + packageId = { + val prefix = uniquePath(TransformableSource(src).toPath.toAbsolutePath.getParent, projectRoot).toString + if(prefix.nonEmpty) { + // The - is enough to unambiguously separate the prefix from the package name, since it can't occur in the package name + // per Go's spec (https://go.dev/ref/spec#Package_clause) + prefix + " - " + packageName + } else { + // Fallback case if the prefix is empty, for example if the directory of a FileSource is in the current directory + packageName + } + } + } yield new PackageInfo(packageId, packageName, isBuiltIn) + } + + /** + * Forcefully tries to create a package info or throws an runtime exception. + * Only use for unit tests + */ + def getPackageInfoOrCrash(src: Source, projectRoot: Path): PackageInfo = { + Source.getPackageInfo(src, projectRoot).fold( + errs => Violation.violation(s"Creating package info failed: ${errs.map(_.formattedMessage).mkString(", ")}"), + identity) } /** diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala index dcf9f341e..c6198617e 100644 --- a/src/main/scala/viper/gobra/frontend/info/Info.scala +++ b/src/main/scala/viper/gobra/frontend/info/Info.scala @@ -48,7 +48,7 @@ object Info extends LazyLogging { /** keeps track of the package dependencies that are currently resolved. This information is used to detect cycles */ private var parserPendingPackages: Vector[AbstractImport] = Vector() - private def getParseResult(abstractPackage: AbstractPackage): Either[Vector[ParserError], ParseSuccessResult] = { + private def getParseResult(abstractPackage: AbstractPackage): ParseResult = { Violation.violation(parseResults.contains(abstractPackage), s"GetParseResult: expects that $abstractPackage has been parsed") parseResults(abstractPackage) } diff --git a/src/test/scala/viper/gobra/GobraPackageTests.scala b/src/test/scala/viper/gobra/GobraPackageTests.scala index 49738fd19..f0c8dd14f 100644 --- a/src/test/scala/viper/gobra/GobraPackageTests.scala +++ b/src/test/scala/viper/gobra/GobraPackageTests.scala @@ -69,7 +69,7 @@ class GobraPackageTests extends GobraTests { )) } yield config - val pkgInfo = Source.getPackageInfo(FromFileSource(input.files.head), currentDir) + val pkgInfo = Source.getPackageInfoOrCrash(FromFileSource(input.files.head), currentDir) val config = Config( logLevel = Level.INFO, diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala index 9de0ce90d..0409c7c5a 100644 --- a/src/test/scala/viper/gobra/GobraTests.scala +++ b/src/test/scala/viper/gobra/GobraTests.scala @@ -52,7 +52,7 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll { Config( logLevel = Level.INFO, reporter = StringifyReporter, - packageInfoInputMap = Map(Source.getPackageInfo(source, Path.of("")) -> Vector(source)), + packageInfoInputMap = Map(Source.getPackageInfoOrCrash(source, Path.of("")) -> Vector(source)), checkConsistency = true, cacheParserAndTypeChecker = cacheParserAndTypeChecker, z3Exe = z3Exe, diff --git a/src/test/scala/viper/gobra/parsing/GobraParserTests.scala b/src/test/scala/viper/gobra/parsing/GobraParserTests.scala index ac6054e12..66e338af3 100644 --- a/src/test/scala/viper/gobra/parsing/GobraParserTests.scala +++ b/src/test/scala/viper/gobra/parsing/GobraParserTests.scala @@ -49,12 +49,12 @@ class GobraParserTests extends AbstractGobraTests with BeforeAndAfterAll { override def run(input: AnnotatedTestInput): Seq[AbstractOutput] = { - val source = FromFileSource(input.file); + val source = FromFileSource(input.file) val config = Config( logLevel = Level.INFO, reporter = NoopReporter, - packageInfoInputMap = Map(Source.getPackageInfo(source, Path.of("")) -> Vector(source)), + packageInfoInputMap = Map(Source.getPackageInfoOrCrash(source, Path.of("")) -> Vector(source)), z3Exe = z3Exe, shouldTypeCheck = false ) diff --git a/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala b/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala index 66fdb06ae..b3222f7ee 100644 --- a/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala +++ b/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala @@ -10,15 +10,15 @@ import org.bitbucket.inkytonik.kiama.util.{Source, StringSource} import org.scalatest.Assertions.fail import viper.gobra.ast.frontend.{PExpression, PImport, PMember, PProgram, PStatement, PType} import viper.gobra.frontend.Parser -import viper.gobra.reporting.ParserError +import viper.gobra.reporting.VerifierError import scala.reflect.ClassTag class ParserTestFrontend { - private def parse[T: ClassTag](source: String, parser: Source => Either[Vector[ParserError], T]) : Either[Vector[ParserError], T] = + private def parse[T: ClassTag](source: String, parser: Source => Either[Vector[VerifierError], T]) : Either[Vector[VerifierError], T] = parser(StringSource(source)) - private def parseOrFail[T: ClassTag](source: String, parser: Source => Either[Vector[ParserError], T]): T = { + private def parseOrFail[T: ClassTag](source: String, parser: Source => Either[Vector[VerifierError], T]): T = { parse(source, parser) match { case Right(ast) => ast case Left(messages) => fail(s"Parsing failed: $messages") @@ -26,12 +26,12 @@ class ParserTestFrontend { } - def parseProgram(source : String) : Either[Vector[ParserError], PProgram] = parse(source, source => Parser.parseProgram(source)) - def parseExp(source : String) : Either[Vector[ParserError], PExpression] = parse(source, Parser.parseExpr) + def parseProgram(source : String) : Either[Vector[VerifierError], PProgram] = parse(source, source => Parser.parseProgram(source)) + def parseExp(source : String) : Either[Vector[VerifierError], PExpression] = parse(source, Parser.parseExpr) def parseExpOrFail(source : String) : PExpression = parseOrFail(source, Parser.parseExpr) - def parseStmt(source : String) : Either[Vector[ParserError], PStatement] = parse(source, Parser.parseStmt) + def parseStmt(source : String) : Either[Vector[VerifierError], PStatement] = parse(source, Parser.parseStmt) def parseStmtOrFail(source : String) : PStatement = parseOrFail(source, Parser.parseStmt) - def parseType(source : String) : Either[Vector[ParserError], PType] = parse(source, Parser.parseType) + def parseType(source : String) : Either[Vector[VerifierError], PType] = parse(source, Parser.parseType) def parseTypeOrFail(source : String) : PType = parseOrFail(source, Parser.parseType) def parseImportDecl(source: String): Vector[PImport] = parseOrFail(source, Parser.parseImportDecl) def parseFunctionDecl(source: String, specOnly: Boolean = false): PMember = parseOrFail(source, (s: Source) => Parser.parseFunction(s, specOnly = specOnly)) From 6be69f4a7b944001adb4b679bc29e9426891500c Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Fri, 17 Jan 2025 13:45:23 +0100 Subject: [PATCH 02/10] fixes invalid position information for parser error --- src/main/scala/viper/gobra/frontend/Source.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/gobra/frontend/Source.scala b/src/main/scala/viper/gobra/frontend/Source.scala index 014393138..c771f9589 100644 --- a/src/main/scala/viper/gobra/frontend/Source.scala +++ b/src/main/scala/viper/gobra/frontend/Source.scala @@ -54,7 +54,7 @@ object Source { def getPackageInfo(src: Source, projectRoot: Path): Either[Vector[VerifierError], PackageInfo] = { for { packageName <- PackageResolver.getPackageClause(src: Source).toRight({ - val pos = Some(SourcePosition(src.toPath, 0, 0)) + val pos = Some(SourcePosition(src.toPath, 1, 1)) Vector(ParserError("Missing package clause", pos)) }) isBuiltIn = src match { From 084c2ed6150987e5e48d9c896d58fae476d7800c Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Fri, 17 Jan 2025 14:01:22 +0100 Subject: [PATCH 03/10] fixes a compiler warning --- src/main/scala/viper/gobra/frontend/info/Info.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/gobra/frontend/info/Info.scala b/src/main/scala/viper/gobra/frontend/info/Info.scala index c6198617e..467040b04 100644 --- a/src/main/scala/viper/gobra/frontend/info/Info.scala +++ b/src/main/scala/viper/gobra/frontend/info/Info.scala @@ -19,7 +19,7 @@ import viper.gobra.frontend.Parser.{ParseResult, ParseSuccessResult} import viper.gobra.util.TaskManagerMode.{Lazy, Parallel, Sequential} 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} +import viper.gobra.reporting.{CyclicImportError, TypeCheckDebugMessage, TypeCheckFailureMessage, TypeCheckSuccessMessage, TypeError, VerifierError} import viper.gobra.util.{GobraExecutionContext, Job, TaskManager, Violation} import java.security.MessageDigest From be9d67d7e146cd198c361b1f8cdefa0ca833e72e Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Sat, 18 Jan 2025 23:09:40 +0100 Subject: [PATCH 04/10] updates ViperServer to 2bba757 --- viperserver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viperserver b/viperserver index e0890869a..2bba7574d 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit e0890869a8f3a53d8de3b8b0c1ee995398a04978 +Subproject commit 2bba7574d2c4df37c7809c514b130842da762176 From 942316d881da4cb27dca3a605fd1080fb6be1c67 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 14:20:16 +0100 Subject: [PATCH 05/10] changes types of parser to only return parser errors --- src/main/scala/viper/gobra/frontend/Parser.scala | 6 +++--- src/main/scala/viper/gobra/frontend/Source.scala | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/Parser.scala b/src/main/scala/viper/gobra/frontend/Parser.scala index 2408ba941..96515b5ba 100644 --- a/src/main/scala/viper/gobra/frontend/Parser.scala +++ b/src/main/scala/viper/gobra/frontend/Parser.scala @@ -33,8 +33,8 @@ import scala.concurrent.Future object Parser extends LazyLogging { type ParseSuccessResult = (Vector[Source], PPackage) - type ParseResult = Either[Vector[VerifierError], ParseSuccessResult] - type ImportToPkgInfoOrErrorMap = Vector[(AbstractPackage, Either[Vector[VerifierError], (Vector[Source], PackageInfo)])] + type ParseResult = Either[Vector[ParserError], ParseSuccessResult] + type ImportToPkgInfoOrErrorMap = Vector[(AbstractPackage, Either[Vector[ParserError], (Vector[Source], PackageInfo)])] type PreprocessedSources = Vector[Source] class ParseManager(config: Config)(implicit executor: GobraExecutionContext) extends LazyLogging { @@ -153,7 +153,7 @@ object Parser extends LazyLogging { lazy val specOnly: Boolean = true } - private case class ParseFailureJob(errs: Vector[VerifierError]) extends Job[PreprocessedSources, ParseResult] { + private case class ParseFailureJob(errs: Vector[ParserError]) extends Job[PreprocessedSources, ParseResult] { override protected def sequentialPrecompute(): PreprocessedSources = Vector.empty override protected def compute(precomputationResult: PreprocessedSources): ParseResult = diff --git a/src/main/scala/viper/gobra/frontend/Source.scala b/src/main/scala/viper/gobra/frontend/Source.scala index c771f9589..3c407ec09 100644 --- a/src/main/scala/viper/gobra/frontend/Source.scala +++ b/src/main/scala/viper/gobra/frontend/Source.scala @@ -9,7 +9,7 @@ package viper.gobra.frontend import java.io.Reader import java.nio.file.{Files, Path, Paths} import org.bitbucket.inkytonik.kiama.util.{FileSource, Filenames, IO, Source, StringSource} -import viper.gobra.reporting.{ParserError, VerifierError} +import viper.gobra.reporting.ParserError import viper.gobra.util.Violation import viper.silver.ast.SourcePosition @@ -51,7 +51,7 @@ object Source { /** * Returns an object containing information about the package a source belongs to. */ - def getPackageInfo(src: Source, projectRoot: Path): Either[Vector[VerifierError], PackageInfo] = { + def getPackageInfo(src: Source, projectRoot: Path): Either[Vector[ParserError], PackageInfo] = { for { packageName <- PackageResolver.getPackageClause(src: Source).toRight({ val pos = Some(SourcePosition(src.toPath, 1, 1)) From 32e4af31202cded632705e62f905e01f8c484040 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 14:21:43 +0100 Subject: [PATCH 06/10] implements CR suggestion by Joao MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- src/main/scala/viper/gobra/frontend/Config.scala | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 43f8f919d..3a23b6db0 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -401,9 +401,11 @@ case class PackageModeConfig(projectRoot: Path = ConfigDefaults.DefaultProjectRo pkgInfo <- getPackageInfo(sources.head, projectRoot) } yield pkgInfo -> sources }.partitionMap(identity) - for { - mappings <- if (errors.nonEmpty) Left(errors.flatten) else Right(mappings) - } yield createConfig(mappings.toMap) + if (errors.nonEmpty) { + Left(errors.flatten) + } else { + Right(createConfig(mappings.toMap)) + } } } From 4f68b39480e75ff5f918e9d401687c6fff8e8d82 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Tue, 21 Jan 2025 15:17:06 +0100 Subject: [PATCH 07/10] Updates ViperServer to latest commit on 'master' --- viperserver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viperserver b/viperserver index 2bba7574d..d66f063eb 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit 2bba7574d2c4df37c7809c514b130842da762176 +Subproject commit d66f063eb43c9565ed05607cae77debfdc2462d3 From 182ac1d67a70625324558eed4fad2d2636b4d7cf Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Wed, 22 Jan 2025 18:18:37 +0100 Subject: [PATCH 08/10] Updates ViperServer to latest commit on 'master' --- viperserver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viperserver b/viperserver index d66f063eb..7fb656ba3 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit d66f063eb43c9565ed05607cae77debfdc2462d3 +Subproject commit 7fb656ba3f5cd910100291cdfc37ea23ff67bf42 From d72d29a7db45b8b96b617ffc8d48c0d5e0306ade Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Wed, 22 Jan 2025 22:06:17 +0100 Subject: [PATCH 09/10] implements CR suggestion by Joao MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- src/main/scala/viper/gobra/frontend/Source.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/gobra/frontend/Source.scala b/src/main/scala/viper/gobra/frontend/Source.scala index 3c407ec09..82a5c21ce 100644 --- a/src/main/scala/viper/gobra/frontend/Source.scala +++ b/src/main/scala/viper/gobra/frontend/Source.scala @@ -78,7 +78,7 @@ object Source { /** * Forcefully tries to create a package info or throws an runtime exception. - * Only use for unit tests + * Only used for unit tests */ def getPackageInfoOrCrash(src: Source, projectRoot: Path): PackageInfo = { Source.getPackageInfo(src, projectRoot).fold( From 1b65121aa9fc8cd9d83538ecc9e7bc85b054880c Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Wed, 22 Jan 2025 22:11:16 +0100 Subject: [PATCH 10/10] implements CR suggestions by Joao --- .../scala/viper/gobra/frontend/Source.scala | 17 +++++++++-------- .../gobra/parsing/ParserTestFrontend.scala | 14 +++++++------- 2 files changed, 16 insertions(+), 15 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/Source.scala b/src/main/scala/viper/gobra/frontend/Source.scala index 82a5c21ce..c6945eebb 100644 --- a/src/main/scala/viper/gobra/frontend/Source.scala +++ b/src/main/scala/viper/gobra/frontend/Source.scala @@ -52,15 +52,16 @@ object Source { * Returns an object containing information about the package a source belongs to. */ def getPackageInfo(src: Source, projectRoot: Path): Either[Vector[ParserError], PackageInfo] = { + val isBuiltIn = src match { + case FromFileSource(_, _, builtin) => builtin + case _ => false + } + val packageNameOrError = PackageResolver.getPackageClause(src).toRight({ + val pos = Some(SourcePosition(src.toPath, 1, 1)) + Vector(ParserError("Missing package clause", pos)) + }) for { - packageName <- PackageResolver.getPackageClause(src: Source).toRight({ - val pos = Some(SourcePosition(src.toPath, 1, 1)) - Vector(ParserError("Missing package clause", pos)) - }) - isBuiltIn = src match { - case FromFileSource(_, _, builtin) => builtin - case _ => false - } + packageName <- packageNameOrError /** A unique identifier for packages */ packageId = { val prefix = uniquePath(TransformableSource(src).toPath.toAbsolutePath.getParent, projectRoot).toString diff --git a/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala b/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala index b3222f7ee..66fdb06ae 100644 --- a/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala +++ b/src/test/scala/viper/gobra/parsing/ParserTestFrontend.scala @@ -10,15 +10,15 @@ import org.bitbucket.inkytonik.kiama.util.{Source, StringSource} import org.scalatest.Assertions.fail import viper.gobra.ast.frontend.{PExpression, PImport, PMember, PProgram, PStatement, PType} import viper.gobra.frontend.Parser -import viper.gobra.reporting.VerifierError +import viper.gobra.reporting.ParserError import scala.reflect.ClassTag class ParserTestFrontend { - private def parse[T: ClassTag](source: String, parser: Source => Either[Vector[VerifierError], T]) : Either[Vector[VerifierError], T] = + private def parse[T: ClassTag](source: String, parser: Source => Either[Vector[ParserError], T]) : Either[Vector[ParserError], T] = parser(StringSource(source)) - private def parseOrFail[T: ClassTag](source: String, parser: Source => Either[Vector[VerifierError], T]): T = { + private def parseOrFail[T: ClassTag](source: String, parser: Source => Either[Vector[ParserError], T]): T = { parse(source, parser) match { case Right(ast) => ast case Left(messages) => fail(s"Parsing failed: $messages") @@ -26,12 +26,12 @@ class ParserTestFrontend { } - def parseProgram(source : String) : Either[Vector[VerifierError], PProgram] = parse(source, source => Parser.parseProgram(source)) - def parseExp(source : String) : Either[Vector[VerifierError], PExpression] = parse(source, Parser.parseExpr) + def parseProgram(source : String) : Either[Vector[ParserError], PProgram] = parse(source, source => Parser.parseProgram(source)) + def parseExp(source : String) : Either[Vector[ParserError], PExpression] = parse(source, Parser.parseExpr) def parseExpOrFail(source : String) : PExpression = parseOrFail(source, Parser.parseExpr) - def parseStmt(source : String) : Either[Vector[VerifierError], PStatement] = parse(source, Parser.parseStmt) + def parseStmt(source : String) : Either[Vector[ParserError], PStatement] = parse(source, Parser.parseStmt) def parseStmtOrFail(source : String) : PStatement = parseOrFail(source, Parser.parseStmt) - def parseType(source : String) : Either[Vector[VerifierError], PType] = parse(source, Parser.parseType) + def parseType(source : String) : Either[Vector[ParserError], PType] = parse(source, Parser.parseType) def parseTypeOrFail(source : String) : PType = parseOrFail(source, Parser.parseType) def parseImportDecl(source: String): Vector[PImport] = parseOrFail(source, Parser.parseImportDecl) def parseFunctionDecl(source: String, specOnly: Boolean = false): PMember = parseOrFail(source, (s: Source) => Parser.parseFunction(s, specOnly = specOnly))