Skip to content

Commit

Permalink
merge with master
Browse files Browse the repository at this point in the history
  • Loading branch information
@jcp19
jcp19 committed Jan 23, 2025
2 parents fb6a51e + 41a583e commit 0eb628d
Show file tree
Hide file tree
Showing 15 changed files with 172 additions and 68 deletions.
6 changes: 3 additions & 3 deletions src/main/scala/viper/gobra/Gobra.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/viper/gobra/backend/BackendVerifier.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,14 +41,14 @@ object BackendVerifier {
case _ =>
}

(config.backend, config.boogieExe) match {
(config.backendOrDefault, config.boogieExe) match {
case (Carbon, Some(boogieExe)) =>
exePaths ++= Vector("--boogieExe", boogieExe)
case _ =>
}

val verificationResults: Future[VerificationResult] = {
val verifier = config.backend.create(exePaths, config)
val verifier = config.backendOrDefault.create(exePaths, config)
val reporter = BacktranslatingReporter(config.reporter, task.backtrack, config)

if (!config.shouldChop) {
Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/viper/gobra/backend/Carbon.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ class Carbon(commandLineArguments: Seq[String]) extends ViperVerifier {
val carbonApi: carbon.CarbonFrontendAPI = new CarbonFrontendAPI(reporter)

val startTime = System.currentTimeMillis()
carbonApi.initialize(commandLineArguments ++ Seq("--ignoreFile", "dummy.sil"))
carbonApi.initialize(commandLineArguments)
val result = carbonApi.verify(program)
carbonApi.stop()

Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/viper/gobra/backend/ViperBackends.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ object ViperBackends {
/** returns an existing ViperCoreServer instance or otherwise creates a new one */
protected def getOrCreateServer(config: Config)(executionContext: GobraExecutionContext): ViperCoreServer = {
server.getOrElse({
var serverConfig = List("--disablePlugins", "--logLevel", config.logLevel.levelStr)
var serverConfig = List("--logLevel", config.logLevel.levelStr)
if(config.cacheFile.isDefined) {
serverConfig = serverConfig.appendedAll(List("--cacheFile", config.cacheFile.get.toString))
}
Expand Down Expand Up @@ -180,7 +180,7 @@ object ViperBackends {
case class ViperServerWithCarbon(initialServer: Option[ViperCoreServer] = None) extends ViperServerBackend(initialServer) {
override def getViperVerifierConfig(exePaths: Vector[String], config: Config): ViperVerifierConfig = {
var options: Vector[String] = Vector.empty
options ++= Vector("--logLevel", "ERROR")
// options ++= Vector("--logLevel", "ERROR")
if (config.respectFunctionPrePermAmounts) {
options ++= Vector("--respectFunctionPrePermAmounts")
}
Expand Down
91 changes: 56 additions & 35 deletions src/main/scala/viper/gobra/frontend/Config.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ import viper.gobra.frontend.Config.enableLazyImportOptionPrettyPrinted
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

Expand Down Expand Up @@ -130,7 +130,8 @@ case class Config(
includeDirs: Vector[Path] = ConfigDefaults.DefaultIncludeDirs.map(_.toPath).toVector,
projectRoot: Path = ConfigDefaults.DefaultProjectRoot.toPath,
reporter: GobraReporter = ConfigDefaults.DefaultReporter,
backend: ViperBackend = ConfigDefaults.DefaultBackend,
// `None` indicates that no backend has been specified and instructs Gobra to use the default backend
backend: Option[ViperBackend] = None,
isolate: Option[Vector[SourcePosition]] = None,
choppingUpperBound: Int = ConfigDefaults.DefaultChoppingUpperBound,
packageTimeout: Duration = ConfigDefaults.DefaultPackageTimeout,
Expand Down Expand Up @@ -194,7 +195,12 @@ case class Config(
projectRoot = projectRoot,
includeDirs = (includeDirs ++ other.includeDirs).distinct,
reporter = reporter,
backend = backend,
backend = (backend, other.backend) match {
case (l, None) => l
case (None, r) => r
case (l, r) if l == r => l
case (Some(l), Some(r)) => Violation.violation(s"Unable to merge differing backends from in-file configuration options, got $l and $r")
},
isolate = (isolate, other.isolate) match {
case (None, r) => r
case (l, None) => l
Expand Down Expand Up @@ -240,6 +246,8 @@ case class Config(
} else {
TypeBounds(Int = TypeBounds.IntWith64Bit, UInt = TypeBounds.UIntWith64Bit)
}

val backendOrDefault: ViperBackend = backend.getOrElse(ConfigDefaults.DefaultBackend)
}

object Config {
Expand All @@ -258,7 +266,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
moduleName: String = ConfigDefaults.DefaultModuleName,
includeDirs: Vector[Path] = ConfigDefaults.DefaultIncludeDirs.map(_.toPath).toVector,
reporter: GobraReporter = ConfigDefaults.DefaultReporter,
backend: ViperBackend = ConfigDefaults.DefaultBackend,
backend: Option[ViperBackend] = None,
// list of pairs of file and line numbers. Indicates which lines of files should be isolated.
isolate: List[(Path, List[Int])] = ConfigDefaults.DefaultIsolate,
choppingUpperBound: Int = ConfigDefaults.DefaultChoppingUpperBound,
Expand Down Expand Up @@ -307,8 +315,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(
Expand Down Expand Up @@ -359,20 +367,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)
}
}
}
Expand All @@ -391,38 +401,49 @@ 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))
if (errors.nonEmpty) {
Left(errors.flatten)
} else {
Right(createConfig(mappings.toMap))
}
}
}

case class RecursiveModeConfig(projectRoot: Path = ConfigDefaults.DefaultProjectRoot.toPath,
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)
}
}

Expand Down Expand Up @@ -561,7 +582,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
choices = Seq("SILICON", "CARBON", "VSWITHSILICON", "VSWITHCARBON"),
name = "backend",
descr = "Specifies the used Viper backend. The default is SILICON.",
default = Some("SILICON"),
default = None,
noshort = true
).map{
case "SILICON" => ViperBackends.SiliconBackend
Expand Down Expand Up @@ -860,9 +881,9 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
conflicts(input, List(projectRoot, inclPackages, exclPackages))
conflicts(directory, List(inclPackages, exclPackages))

// must be lazy to guarantee that this value is computed only during the CLI options validation and not before.
lazy val isSiliconBasedBackend = backend.toOption match {
case Some(ViperBackends.SiliconBackend | _: ViperBackends.ViperServerWithSilicon) => true
// must be a function or lazy to guarantee that this value is computed only during the CLI options validation and not before.
private def isSiliconBasedBackend = backend.toOption.getOrElse(ConfigDefaults.DefaultBackend) match {
case ViperBackends.SiliconBackend | _: ViperBackends.ViperServerWithSilicon => true
case _ => false
}

Expand Down Expand Up @@ -966,7 +987,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.
Expand Down Expand Up @@ -1020,7 +1041,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
printInternal = printInternal(),
printVpr = printVpr(),
streamErrs = !noStreamErrors()),
backend = backend(),
backend = backend.toOption,
isolate = isolate,
choppingUpperBound = chopUpperBound(),
packageTimeout = packageTimeoutDuration,
Expand Down
27 changes: 13 additions & 14 deletions src/main/scala/viper/gobra/frontend/Parser.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -34,7 +34,7 @@ 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 ImportToPkgInfoOrErrorMap = Vector[(AbstractPackage, Either[Vector[ParserError], (Vector[Source], PackageInfo)])]
type PreprocessedSources = Vector[Source]

class ParseManager(config: Config)(implicit executor: GobraExecutionContext) extends LazyLogging {
Expand All @@ -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) => {
Expand All @@ -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
}
Expand All @@ -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:
Expand All @@ -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))
}
Expand Down Expand Up @@ -148,9 +148,8 @@ 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
}

Expand Down
Loading

0 comments on commit 0eb628d

Please sign in to comment.