Configure Gobra via JSON

[ArquintL]

This PR pushes @jcp19's idea further to use a JSON file to configure Gobra by integrating the parsing of the JSON file into Gobra. The accepted JSON structure follows gobrago with the following differences:

• the module-level and package-level JSON files are called gobra-mod.json and gobra.json, respectively
• the module-level JSON file has two fields, installation_cfg and default_job_cfg
• if a field is present in the package-level JSON (a so-called job configuration) then it takes precedence over the module-level field (the default job configuration). This also applies to options expressed in a other field. In particular, these options are parsed and merged with the other non-other fields, constituting a configuration after merging. I.e., this merging is happening before applying the precedence rule that overwrites module-level options.

In addition, the following design choices have been made:

• --config <path> is used to configure Gobra
• <path> must exist and can either be one of the following:
  • a path to a package-level JSON file in which case the Gobra files in the same folder as the JSON file are considered a package and are verified
  • a path to a directory in which case the Gobra files in this folder are considered a package and are verified. A package-level JSON file is optional
• In this configuration mode, only --printConfig is additionally permitted to display the actually used configuration. All other options result in an error. If --printConfig is not provided, Gobra prints a short note stating with configuration files have been considered.
• In this configuration mode, the module-level JSON file is mandatory, which is located by traversing the filesystem starting from <path> towards the filesystem's root directory

[jcp19]

@ArquintL this is marked as a draft PR but you asked for the review. Should I provide feedback on the implementation already? regarding the cli options, I would opt for one of the following:

1. make it an error to provide additional flags when --config <path> is passed
2. whatever flags passed on the CI would override those in the config (this is useful if you want to mostly reuse the config, but try out different options quickly), and I would produce a message saying that this is the case

[ArquintL]

@jcp19 This PR is in draft mode as the design choices are more like suggestions. Code-wise, I do not have any additional changes planned so I'd appreciate a code review. We currently do not have a JSON field for every existing CLI option but if necessary, we can always add more (in separate PRs)

[jcp19]

High-level questions about the design:

• is the module-level json always required, even when we do not use the --config option? My expectation is that it is not, otherwise it may make it harder for new users to try out Gobra. In addition, what should be the behaviour if a user does not pass the --config flag but still has a module level json, or what happens if they use the -p flag and have a package json there?
• I wonder if the distinction between the fields of the module level and package level still make sense (why can't we have the same set of fields in both?)

[jcp19]

I think that the following design could also work:

• there are two kinds of files which have the same format. Both are optional. One is called gobra-project.json and must be at the project root or at the module root, the other is called gobra.json and must be in the package folder.
• by default, we always determine options based on the following hierarchy: default config (determined by the default options for all flags) < gobra-project.json (if present) < gobra.json (if present) < CLI options provided at the call site < file-level options (*) (the order of the last two is up for debate)
• This chain of options would always be used by default, in all modes (-i, -p, and -r). A short message saying which config files were found and used in the environment should be shown so that they are aware of it and are not confused by the behaviour. If no json files are found, no message is displayed (this keeps the UI light in the likely case users are not using verifying a project, but rather trying out gobra on small files)
• we might consider having a flag to ignore the json files in the surrounding environment, but I don't see when this would be useful

Under this design, the --config flag would not be necessary.

(*) While thinking of how all options relate to each other, and especially, how the configs of each package relate to each other, I was confronted again with the fact that right now, we read all configs of all files, regardless of their packages. I think this is a bad idea, which leads to unexpected results (e.g., if we import a package that was verified for overflow checks, it enables overflow checks for the current package). Maybe we should consider deprecating in-file configs when we introduce the json config, except for tests.

[ArquintL]

is the module-level json always required, even when we do not use the --config option? My expectation is that it is not, otherwise it may make it harder for new users to try out Gobra. In addition, what should be the behaviour if a user does not pass the --config flag but still has a module level json, or what happens if they use the -p flag and have a package json there?

Sorry for the imprecision, it's only mandatory if --config is used. Otherwise, it's simply ignored (same holds for gobra.json files)

I wonder if the distinction between the fields of the module level and package level still make sense (why can't we have the same set of fields in both?)

One can argue whether we should allow installation_cfg on the module-level as well. Would you then rename default_job_cfg to something else such that it's uniform for module- and package-level config files (i.e., omit the "default" part as this becomes implicitly the case via our overwriting semantics for configs)?

there are two kinds of files which have the same format. Both are optional. One is called gobra-project.json and must be at the project root or at the module root, the other is called gobra.json and must be in the package folder.

If both files are optional? How would we identify which folder forms a module's root? By detecting go.mod?

This chain of options would always be used by default, in all modes (-i, -p, and -r)

Not sure whether this is less confusing but I think that this should work. The only weird case affects -r where the behavior is not that clear. I.e., if you invoke Gobra on a package but specify -r, will it iterate over all packages in the module or only over packages in subfolders contained in the current working directory?

[jcp19]

If both files are optional? How would we identify which folder forms a module's root? By detecting go.mod?

Either that or by traversing the directory tree, starting in the current package, and moving from parent to parent until a gobra-project.json is found.

Not sure whether this is less confusing but I think that this should work. The only weird case affects -r where the behavior is not that clear. I.e., if you invoke Gobra on a package but specify -r, will it iterate over all packages in the module or only over packages in subfolders contained in the current working directory?

IIRC, you do not pass a package in the recursive mode, but rather, the project root. So, I guess we would iterate through all packages in that directory. I think we need to think about what should be the roles of the project root and module root (should they be unified somehow?).

[jcp19]

@ArquintL this is marked as a draft PR but you asked for the review. Should I provide feedback on the implementation already? regarding the cli options, I would opt for one of the following:

1. make it an error to provide additional flags when --config <path> is passed
2. whatever flags passed on the CI would override those in the config (this is useful if you want to mostly reuse the config, but try out different options quickly), and I would produce a message saying that this is the case

After additional consideration, I am happy with @ArquintL general proposal, but I would rather choose one of the behaviours I proposed above for the case when we provide more CLI flags in addition to --config. In addition, we should probably show to the user which packages are being verified when the --config option is used, to avoid confusing the user (for example, because they passed the wrong file to a json file). I will proceed with the code review.

[jcp19]

So far, I reviewed up to src/main/scala/viper/gobra/frontend/Config.scala. I will continue the review later

[ArquintL]

@jcp19 Sorry this got quite ugly in the end ^^
The problem was that overriding default job options by job-specific options requires knowing which job-specific options the user actually specified (as opposed to all default ones).
Hence, I introduce InputConfig that corresponds to a directly translation from ScallopGobraConfig, i.e., before we apply any of the complicated transformations to obtain Config. In InputConfig, all non-provided options are simply None and we can perform whatever merge or override operation we want (which btw is not possible on a ScallopGobraConfig as ScallopOptions are immutable.

[jcp19]

In general, it looks ok to me. I have a few minor comments / remarks

[jcp19]

I don't oppose dropping this for json configs.

[ArquintL]

I leave this option for the moment but I've added a long comment mentioning that one might want to drop or move this option. In particular, it could make sense to allow users to specify recursive on the module-level such that verifying the module results in recursively verifying all its packages. However, we would then have to revisit the meaning of recursive as currently recursive, inputs, and directory are mutually exclusive. It would however make sense that each package could specify the files that constitute the package

[Copilot]

Pull request overview

Adds a new --config <path> mode that configures Gobra via JSON files (gobra-mod.json + optional gobra.json), including merging/precedence rules, and refactors configuration parsing/merging to support this workflow.

Changes:

• Introduces JSON config data model + json4s parsing/serialization utilities.
• Refactors CLI/in-file config handling via a new InputConfig representation and adds --printConfig.
• Adds a dedicated test suite and resource fixtures for JSON-config-driven verification.

Reviewed changes

Copilot reviewed 23 out of 24 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
src/main/scala/viper/gobra/frontend/JsonConfig.scala	Adds JSON schema case classes and json4s parsing/serialization helpers.
src/main/scala/viper/gobra/frontend/Config.scala	Major refactor: introduces InputConfig, adds --config/--printConfig, and implements config-file mode resolution/merging.
src/main/scala/viper/gobra/Gobra.scala	Switches in-file config merging to InputConfig and adds printing of resolved config.
src/main/scala/viper/gobra/backend/ViperBackends.scala	Makes backends CLI-enum-friendly (value strings) for reuse in CLI + JSON parsing.
src/test/scala/viper/gobra/GobraPackageTests.scala	Makes createConfig protected to allow reuse by new config tests.
src/test/scala/viper/gobra/GobraConfigTests.scala	Adds tests that run Gobra in --config mode over resource fixtures.
src/test/resources/gobra_config/**	Adds module/package JSON fixtures and corresponding .gobra programs to test precedence/merging.
build.sbt	Adds json4s-native dependency.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Paths.get(input.name).getParent can be null when input.name is a relative path (e.g., "foo.gobra"), which will make parseCliArgs blow up when calling toAbsolutePath on a null base. Consider using Paths.get(input.name).toAbsolutePath.getParent and handling the no-parent case (e.g., fall back to Paths.get(".") or skip path resolution).

Suggested change

	InputConfig.parseCliArgs(configString, Some(Paths.get(input.name).getParent)).map(Some(_))
	val absoluteInputPath = Paths.get(input.name).toAbsolutePath
	val basePath = Option(absoluteInputPath.getParent).getOrElse(Paths.get(".").toAbsolutePath)
	InputConfig.parseCliArgs(configString, Some(basePath)).map(Some(_))

[Copilot]

Input mode validation counts recursive as “present” whenever recursive.value.isDefined, but later rawConfig only treats recursive mode as selected when recursive.value.contains(true). This means a JSON config with "recursive": false (or any source that sets Some(false)) can pass requireOne(...) but then fail to select a mode at runtime. Align validation with mode selection (treat recursive as present only when true), or normalize recursive = Some(false) to None when building InputConfig from JSON.

Suggested change

	mutuallyExclusive(input, directory, recursive, configFile)
	} else {
	// either `input`, `directory` or `recursive` must be provided but not both.
	// this also checks that at least one file or directory is provided in the case of `input` and `directory`.
	requireOne(input, directory, recursive, configFile)
	if (recursive.value.contains(false)) {
	mutuallyExclusive(input, directory, configFile)
	} else {
	mutuallyExclusive(input, directory, recursive, configFile)
	}
	} else {
	// either `input`, `directory` or `recursive` must be provided but not both.
	// this also checks that at least one file or directory is provided in the case of `input` and `directory`.
	if (recursive.value.contains(false)) {
	requireOne(input, directory, configFile)
	} else {
	requireOne(input, directory, recursive, configFile)
	}

[Copilot]

The default “set package directory if no input mode specified” check treats recursive.value.isEmpty as meaning “no recursive mode”, but recursive can be Some(false) (e.g., from JSON). In that case this block will not set directory, and later mode selection uses recursive.value.contains(true) so no mode is selected. Use recursive.value.contains(true) (or the same predicate as rawConfig) when deciding whether to apply the directory fallback.

[Copilot]

other flags from JSON are parsed via InputConfig.fromOtherArgs(...) without (1) validating against Config.validateOtherArgs and (2) resolving any relative paths against the module/job config directory. This makes the disallowedInOther safeguard ineffective (it’s currently unused) and can lead to incorrect path handling if other contains path-related flags. Consider calling Config.validateOtherArgs(...) before parsing, and/or using InputConfig.parseCliArgs(otherArgs, Some(moduleConfigDir/jobConfigDir)) so relative paths resolve consistently.

[Copilot]

The module JSON schema includes installation_cfg (e.g., z3_path), and GobraModuleCfg parses it, but ConfigFileModeConfig never applies moduleCfg.installation_cfg when constructing the final Config. As a result, installation-level settings are silently ignored. Please wire installation_cfg into the resolved configuration (e.g., map z3_path to InputConfig.z3Exe/Config.z3Exe) or remove the field if it’s intentionally out of scope.