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]

what about include paths (-I) and --projectRoot? Is there a criteria for things commands whose paths are resolved? And for those commands where we resolve the paths, are they resolved against the current path?

[jcp19]

I feel like this use of implicit affords us very little, and I would rather have the more predictable behaviour and maintainability of having toInputConfigOption as a regular (static) method, rather than an extension method.

[jcp19]

hmm, what's the point of passing the jar here? given that a user has to call gobra (and select the jar there), this feels redundant

[jcp19]

I guess this is the input to -p

[jcp19]

I don't oppose dropping this for json configs.