Skip to content

Commit 0fa163c

Browse files
ArquintLArquintL
committed
implements Joao's CR suggestions
1 parent 61c691b commit 0fa163c

2 files changed

Lines changed: 106 additions & 82 deletions

File tree

‎src/main/scala/viper/gobra/frontend/Config.scala‎

Lines changed: 105 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -320,22 +320,44 @@ object Config {
320320
val enableLazyImportOptionPrettyPrinted = s"--$enableLazyImportOptionName"
321321

322322
/**
323-
* Parses `args` as CLI options and resolves potential `includeDirs` to `resolveTo` if it's not None.
324-
* Inputs in `configString` are optional.
323+
* Parses `args` as CLI options and resolves path-bearing fields relative to `resolveTo` if it's not None.
324+
* Resolved fields: includeDirs, projectRoot, cacheFile, z3Exe, boogieExe.
325+
* Inputs in `args` are optional.
325326
*/
326327
def parseCliArgs(args: List[String], resolveTo: Option[Path]): Either[Vector[VerifierError], Config] = {
327-
/** skip checks if we resolve include dirs */
328+
/** skip checks if we resolve paths */
328329
val skipIncludeDirChecks = resolveTo.isDefined
329330
for {
330331
config <- new ScallopGobraConfig(args, isInputOptional = true, skipIncludeDirChecks = skipIncludeDirChecks).config
331332
resolvedConfig = resolveTo match {
332333
case None => config
333-
case Some(p) => config.copy(includeDirs = config.includeDirs.map(
334-
// it's important to convert includeDir to a string first as `path` might be a ZipPath and `includeDir` might not
335-
includeDir => p.toAbsolutePath.resolve(includeDir.toString)))
334+
case Some(p) =>
335+
val absBase = p.toAbsolutePath
336+
config.copy(
337+
// convert to string first to handle potential ZipPath vs regular Path mismatch
338+
includeDirs = config.includeDirs.map(d => absBase.resolve(d.toString)),
339+
projectRoot = absBase.resolve(config.projectRoot.toString),
340+
cacheFile = config.cacheFile.map(cf => absBase.resolve(cf.toString)),
341+
z3Exe = config.z3Exe.map(z => absBase.resolve(z).toString),
342+
boogieExe = config.boogieExe.map(b => absBase.resolve(b).toString),
343+
)
336344
}
337345
} yield resolvedConfig
338346
}
347+
348+
/** Options that must not appear in the `other` field of a JSON config because their paths
349+
* cannot be correctly resolved (they are turned into Source objects before path resolution). */
350+
private val disallowedInOther: Set[String] = Set("--input", "-i", "--directory", "-p")
351+
352+
/** Validates that `other` args do not contain disallowed options. */
353+
def validateOtherArgs(args: List[String]): Either[Vector[VerifierError], Unit] = {
354+
val found = args.filter(disallowedInOther.contains)
355+
if (found.nonEmpty)
356+
Left(Vector(ConfigError(
357+
s"The 'other' field in the JSON config must not contain ${found.mkString(", ")}. " +
358+
"Use the dedicated JSON fields (input_files, pkg_path) instead.")))
359+
else Right(())
360+
}
339361
}
340362

341363
// have a look at `Config` to see an inline description of some of these parameters
@@ -534,6 +556,8 @@ case class ConfigFileModeConfig(configFile: File) extends RawConfig {
534556
// file listing settings that are common to the entire module.
535557

536558
private val VerificationJobConfigFilename = "gobra.json"
559+
// A module config file must exist in the directory tree of configFile (i.e., in the same
560+
// directory or any parent directory). Without it, Gobra cannot determine the module-level configuration.
537561
private val ModuleConfigFilename = "gobra-mod.json"
538562

539563
/** The verification job config is optional */
@@ -547,18 +571,21 @@ case class ConfigFileModeConfig(configFile: File) extends RawConfig {
547571
}
548572
if (jobConfigFile.exists() && jobConfigFile.isFile) {
549573
// provide the generic type argument to avoid weird runtime errors even though the
550-
// pretends to not need it!
574+
// Scala compiler pretends to not need it!
551575
GobraJsonConfigHandler
552576
.fromJson[VerificationJobCfg](jobConfigFile)
553577
} else {
578+
// No job config file found; return an empty config (all fields None).
579+
// Missing fields will be filled from the module config's default_job_cfg.
554580
Right(VerificationJobCfg())
555581
}
556582
} else {
557583
Left(Vector(ConfigError(s"The provided config path does not exist: ${configFile.getAbsoluteFile.toString}")))
558584
}
559585
}
560586

561-
private lazy val moduleConfig: Either[Vector[VerifierError], GobraModuleCfg] = {
587+
/** Returns the module config together with the directory containing the module config file */
588+
private lazy val moduleConfigWithDir: Either[Vector[VerifierError], (GobraModuleCfg, Path)] = {
562589
var searchDirectory = if (configFile.isFile) configFile.getParentFile else configFile
563590
var moduleConfigFile: Option[File] = None
564591
while (searchDirectory != null) {
@@ -573,134 +600,130 @@ case class ConfigFileModeConfig(configFile: File) extends RawConfig {
573600
moduleConfigFile match {
574601
case Some(file) =>
575602
// provide the generic type argument to avoid weird runtime errors even though the
576-
// pretends to not need it!
603+
// Scala compiler pretends to not need it!
577604
GobraJsonConfigHandler
578605
.fromJson[GobraModuleCfg](file)
606+
.map(cfg => (cfg, file.getParentFile.toPath))
579607
case None =>
580608
Left(Vector(ConfigError(s"Could not find module configuration file $ModuleConfigFilename in the directory or a parent directory of ${configFile.getAbsoluteFile.toString}")))
581609
}
582610
}
583611

584-
private lazy val mergedConfig: Either[Vector[VerifierError], MergedGobraModuleCfg] = (moduleConfig, verificationJobConfig) match {
585-
case (Left(moduleErrors), Left(jobErrors)) => Left(moduleErrors ++ jobErrors)
586-
case (Left(moduleErrors), _) => Left(moduleErrors)
587-
case (_, Left(jobErrors)) => Left(jobErrors)
588-
case (Right(moduleCfg), Right(jobCfg)) =>
589-
def mergeField[T](fieldSelector: VerificationJobCfg => Option[T]): Option[T] =
590-
fieldSelector(jobCfg).orElse(moduleCfg.default_job_cfg.flatMap(fieldSelector(_)))
591-
Right(MergedGobraModuleCfg(
592-
installation_cfg = moduleCfg.installation_cfg.getOrElse(GobraInstallCfg()),
593-
job_cfg = VerificationJobCfg(
594-
assume_injectivity_inhale = mergeField(_.assume_injectivity_inhale),
595-
backend = mergeField(_.backend),
596-
check_consistency = mergeField(_.check_consistency),
597-
overflow = mergeField(_.overflow),
598-
conditionalize_permissions = mergeField(_.conditionalize_permissions),
599-
only_files_with_header = mergeField(_.only_files_with_header),
600-
includes = mergeField(_.includes),
601-
input_files = mergeField(_.input_files),
602-
mce_mode = mergeField(_.mce_mode),
603-
module = mergeField(_.module),
604-
more_joins = mergeField(_.more_joins),
605-
pkg_path = mergeField(_.pkg_path),
606-
parallelize_branches = mergeField(_.parallelize_branches),
607-
print_vpr = mergeField(_.print_vpr),
608-
project_root = mergeField(_.project_root),
609-
recursive = mergeField(_.recursive),
610-
require_triggers = mergeField(_.require_triggers),
611-
// we merge by combining the default and job-specific `other` fields:
612-
other = Some(jobCfg.other.getOrElse(List.empty) ++ moduleCfg.default_job_cfg.flatMap(_.other).getOrElse(List.empty)),
613-
)
614-
))
612+
/** Applies non-None fields from `overrides` directly onto `config`, overriding any existing values.
613+
* Unlike `Config.merge` (which uses OR for booleans, concatenation for lists, etc.), this performs
614+
* direct replacement. Used to apply a higher-priority config level on top of a lower-priority one. */
615+
private def applyJobCfg(config: Config, overrides: VerificationJobCfg): Config = {
616+
config.copy(
617+
moduleName = overrides.module.getOrElse(config.moduleName),
618+
includeDirs = overrides.includes.map(_.map(Paths.get(_)).toVector).getOrElse(config.includeDirs),
619+
projectRoot = overrides.project_root.map(Paths.get(_)).getOrElse(config.projectRoot),
620+
backend = overrides.backend.map(_.underlying).orElse(config.backend),
621+
choppingUpperBound = overrides.chop.getOrElse(config.choppingUpperBound),
622+
checkOverflows = overrides.overflow.getOrElse(config.checkOverflows),
623+
checkConsistency = overrides.check_consistency.getOrElse(config.checkConsistency),
624+
onlyFilesWithHeader = overrides.only_files_with_header.getOrElse(config.onlyFilesWithHeader),
625+
assumeInjectivityOnInhale = overrides.assume_injectivity_inhale.getOrElse(config.assumeInjectivityOnInhale),
626+
parallelizeBranches = overrides.parallelize_branches.getOrElse(config.parallelizeBranches),
627+
conditionalizePermissions = overrides.conditionalize_permissions.getOrElse(config.conditionalizePermissions),
628+
mceMode = overrides.mce_mode.getOrElse(config.mceMode),
629+
requireTriggers = overrides.require_triggers.getOrElse(config.requireTriggers),
630+
moreJoins = overrides.more_joins.getOrElse(config.moreJoins),
631+
)
615632
}
616633

617-
case class MergedGobraModuleCfg(
618-
installation_cfg: GobraInstallCfg,
619-
job_cfg: VerificationJobCfg
620-
)
634+
/** Validates, parses, and merges `other` CLI args into an existing Config.
635+
* Relative paths in `other` are resolved relative to `configDir`. */
636+
private def mergeOtherArgs(config: Config, otherArgs: Option[List[String]], configDir: Path): Either[Vector[VerifierError], Config] = {
637+
val args = otherArgs.getOrElse(List.empty)
638+
for {
639+
_ <- Config.validateOtherArgs(args)
640+
parsed <- if (args.isEmpty) Right(None)
641+
else Config.parseCliArgs(args, Some(configDir)).map(Some(_))
642+
} yield parsed.map(config.merge).getOrElse(config)
643+
}
621644

622-
/** `other` field is not considered for creating the base config */
623-
override protected def baseConfig: BaseConfig = mergedConfig.map(c => {
645+
/** Builds a BaseConfig from the module-level configuration only.
646+
* Options without a dedicated JSON field use their default values but can be configured via `other`. */
647+
override protected def baseConfig: BaseConfig = moduleConfigWithDir.map { case (moduleCfg, _) =>
648+
val defaultJobCfg = moduleCfg.default_job_cfg.getOrElse(VerificationJobCfg())
649+
val installCfg = moduleCfg.installation_cfg.getOrElse(GobraInstallCfg())
624650
val logLevel: Level = ConfigDefaults.DefaultLogLevel
625651
val debug: Boolean = Level.DEBUG.isGreaterOrEqual(logLevel)
626652
BaseConfig(
627653
gobraDirectory = ConfigDefaults.DefaultGobraDirectory,
628-
moduleName = c.job_cfg.module.getOrElse(ConfigDefaults.DefaultModuleName),
629-
includeDirs = c.job_cfg.includes.map(_.map(Paths.get(_))).getOrElse(ConfigDefaults.DefaultIncludeDirs.map(_.toPath)).toVector,
654+
moduleName = defaultJobCfg.module.getOrElse(ConfigDefaults.DefaultModuleName),
655+
includeDirs = defaultJobCfg.includes.map(_.map(Paths.get(_))).getOrElse(ConfigDefaults.DefaultIncludeDirs.map(_.toPath)).toVector,
630656
reporter = FileWriterReporter(
631657
unparse = debug,
632658
eraseGhost = false,
633659
goify = false,
634660
debug = debug,
635661
printInternal = debug,
636-
printVpr = c.job_cfg.print_vpr.getOrElse(debug),
662+
printVpr = defaultJobCfg.print_vpr.getOrElse(debug),
637663
streamErrs = !ConfigDefaults.DefaultNoStreamErrors),
638-
backend = c.job_cfg.backend.map(_.underlying),
664+
backend = defaultJobCfg.backend.map(_.underlying),
639665
isolate = ConfigDefaults.DefaultIsolate,
640-
choppingUpperBound = ConfigDefaults.DefaultChoppingUpperBound,
666+
choppingUpperBound = defaultJobCfg.chop.getOrElse(ConfigDefaults.DefaultChoppingUpperBound),
641667
packageTimeout = ConfigDefaults.DefaultPackageTimeout,
642-
z3Exe = c.installation_cfg.z3_path.orElse(ConfigDefaults.DefaultZ3Exe),
668+
z3Exe = installCfg.z3_path.orElse(ConfigDefaults.DefaultZ3Exe),
643669
boogieExe = ConfigDefaults.DefaultBoogieExe,
644670
logLevel = logLevel,
645671
cacheFile = ConfigDefaults.DefaultCacheFile.map(_.toPath),
646672
shouldParseOnly = ConfigDefaults.DefaultParseOnly,
647673
stopAfterEncoding = ConfigDefaults.DefaultStopAfterEncoding,
648-
checkOverflows = c.job_cfg.overflow.getOrElse(ConfigDefaults.DefaultCheckOverflows),
649-
checkConsistency = c.job_cfg.check_consistency.getOrElse(ConfigDefaults.DefaultCheckConsistency),
674+
checkOverflows = defaultJobCfg.overflow.getOrElse(ConfigDefaults.DefaultCheckOverflows),
675+
checkConsistency = defaultJobCfg.check_consistency.getOrElse(ConfigDefaults.DefaultCheckConsistency),
650676
int32bit = ConfigDefaults.DefaultInt32bit,
651677
cacheParserAndTypeChecker = ConfigDefaults.DefaultCacheParserAndTypeChecker,
652-
onlyFilesWithHeader = c.job_cfg.only_files_with_header.getOrElse(ConfigDefaults.DefaultOnlyFilesWithHeader),
653-
assumeInjectivityOnInhale = c.job_cfg.assume_injectivity_inhale.getOrElse(ConfigDefaults.DefaultAssumeInjectivityOnInhale),
654-
parallelizeBranches = c.job_cfg.parallelize_branches.getOrElse(ConfigDefaults.DefaultParallelizeBranches),
655-
conditionalizePermissions = c.job_cfg.conditionalize_permissions.getOrElse(ConfigDefaults.DefaultConditionalizePermissions),
678+
onlyFilesWithHeader = defaultJobCfg.only_files_with_header.getOrElse(ConfigDefaults.DefaultOnlyFilesWithHeader),
679+
assumeInjectivityOnInhale = defaultJobCfg.assume_injectivity_inhale.getOrElse(ConfigDefaults.DefaultAssumeInjectivityOnInhale),
680+
parallelizeBranches = defaultJobCfg.parallelize_branches.getOrElse(ConfigDefaults.DefaultParallelizeBranches),
681+
conditionalizePermissions = defaultJobCfg.conditionalize_permissions.getOrElse(ConfigDefaults.DefaultConditionalizePermissions),
656682
z3APIMode = ConfigDefaults.DefaultZ3APIMode,
657683
disableNL = ConfigDefaults.DefaultDisableNL,
658-
mceMode = c.job_cfg.mce_mode.getOrElse(ConfigDefaults.DefaultMCEMode),
684+
mceMode = defaultJobCfg.mce_mode.getOrElse(ConfigDefaults.DefaultMCEMode),
659685
enableLazyImports = ConfigDefaults.DefaultEnableLazyImports,
660686
noVerify = ConfigDefaults.DefaultNoVerify,
661687
noStreamErrors = ConfigDefaults.DefaultNoStreamErrors,
662688
parseAndTypeCheckMode = ConfigDefaults.DefaultParseAndTypeCheckMode,
663-
requireTriggers = c.job_cfg.require_triggers.getOrElse(ConfigDefaults.DefaultRequireTriggers),
689+
requireTriggers = defaultJobCfg.require_triggers.getOrElse(ConfigDefaults.DefaultRequireTriggers),
664690
disableSetAxiomatization = ConfigDefaults.DefaultDisableSetAxiomatization,
665691
disableCheckTerminationPureFns = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
666692
unsafeWildcardOptimization = ConfigDefaults.DefaultUnsafeWildcardOptimization,
667-
moreJoins = c.job_cfg.more_joins.getOrElse(ConfigDefaults.DefaultMoreJoins),
693+
moreJoins = defaultJobCfg.more_joins.getOrElse(ConfigDefaults.DefaultMoreJoins),
668694
respectFunctionPrePermAmounts = ConfigDefaults.DefaultRespectFunctionPrePermAmounts,
669695
)
670-
}).getOrElse(BaseConfig())
696+
}.getOrElse(BaseConfig())
671697

672698
override lazy val config: Either[Vector[VerifierError], Config] = {
699+
val jobConfigDir: Path = (if (configFile.isDirectory) configFile else configFile.getParentFile).toPath
673700
for {
674-
mergedConfig <- mergedConfig
675-
config <- (mergedConfig.job_cfg.input_files, mergedConfig.job_cfg.recursive) match {
701+
moduleWithDir <- moduleConfigWithDir
702+
jobCfg <- verificationJobConfig
703+
moduleCfg = moduleWithDir._1
704+
moduleConfigDir = moduleWithDir._2
705+
defaultJobCfg: VerificationJobCfg = moduleCfg.default_job_cfg.getOrElse(VerificationJobCfg())
706+
// Determine verification mode (`jobCfg` takes precedence over `defaultJobCfg`)
707+
initialConfig <- (jobCfg.input_files.orElse(defaultJobCfg.input_files), jobCfg.recursive.orElse(defaultJobCfg.recursive)) match {
676708
case (Some(inputFiles), _) => FileModeConfig(inputFiles.map(Paths.get(_)).toVector, baseConfig).config
677709
case (None, Some(true)) => RecursiveModeConfig(
678-
projectRoot = mergedConfig.job_cfg.project_root.map(Paths.get(_)).getOrElse(ConfigDefaults.DefaultProjectRoot.toPath),
679-
includePackages = mergedConfig.job_cfg.includes.getOrElse(ConfigDefaults.DefaultIncludePackages),
710+
projectRoot = jobCfg.project_root.orElse(defaultJobCfg.project_root).map(Paths.get(_)).getOrElse(ConfigDefaults.DefaultProjectRoot.toPath),
711+
includePackages = jobCfg.includes.orElse(defaultJobCfg.includes).getOrElse(ConfigDefaults.DefaultIncludePackages),
680712
excludePackages = ConfigDefaults.DefaultExcludePackages,
681713
baseConfig = baseConfig,
682714
).config
683715
case (None, _) =>
684-
// we use the provide `configFile` (which either points to a directory or a config file) to
685-
// determine which package to verify
686-
val pathToDirectory = (if (configFile.isDirectory) configFile else configFile.getParentFile).toPath
687716
PackageModeConfig(
688-
projectRoot = mergedConfig.job_cfg.project_root.map(Paths.get(_)).getOrElse(ConfigDefaults.DefaultProjectRoot.toPath),
689-
inputDirectories = Vector(pathToDirectory),
717+
projectRoot = jobCfg.project_root.orElse(defaultJobCfg.project_root).map(Paths.get(_)).getOrElse(ConfigDefaults.DefaultProjectRoot.toPath),
718+
inputDirectories = Vector(jobConfigDir),
690719
baseConfig = baseConfig,
691720
).config
692721
}
693-
otherArgs = mergedConfig.job_cfg.other.getOrElse(List.empty)
694-
otherConfig <- if (otherArgs.isEmpty) Right(None)
695-
else {
696-
// at this point, we do not know anymore from which config file these arguments come from.
697-
// Thus, we do not resolve potential paths.
698-
Config.parseCliArgs(otherArgs, None).map(Some(_))
699-
}
700-
} yield otherConfig match {
701-
case None => config
702-
case Some(o) => config.merge(o)
703-
}
722+
// Module-level config: structured fields (already in baseConfig) + module-level `other` field
723+
moduleLevelConfig <- mergeOtherArgs(initialConfig, defaultJobCfg.other, moduleConfigDir)
724+
// Job-level config applied on top: structured fields + job-level `other` field
725+
finalConfig <- mergeOtherArgs(applyJobCfg(moduleLevelConfig, jobCfg), jobCfg.other, jobConfigDir)
726+
} yield finalConfig
704727
}
705728
}
706729

‎src/main/scala/viper/gobra/frontend/JsonConfig.scala‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -101,6 +101,7 @@ case class VerificationJobCfg(
101101
project_root: Option[String] = None,
102102
recursive: Option[Boolean] = None, // TODO: why would a package specify recursion?
103103
require_triggers: Option[Boolean] = None,
104+
chop: Option[Int] = None,
104105
other: Option[List[String]] = None,
105106
) extends GobraJsonConfig with Resolvable {
106107
type R = VerificationJobCfg

0 commit comments

Comments
 (0)