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 then it takes precedence over the module-level field. However, the only exception to this is the other field, which is merged by concatenating the list of options from both JSON files

In addition, the following design choices have been made:

• --config <path> is used to configure Gobra, in which case all other CLI options are ignored (should there be any)
• <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
• 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

[jcp19]

and includeDir might not

Do you mean "must not"?

[jcp19]

do I see it correctly that we are only resolving the include directories here? What about the other parameters that may contain paths? (e.g., --includePackages or -i)

[jcp19]

this looks fine to me. An alternative would be to use the builtin Enumeration type in Scala (https://www.scala-lang.org/api/2.13.15/scala/Enumeration.html) which may lead to a shorter implementation.

[jcp19]

typo here?

Suggested change

	// provide the generic type argument to avoid weird runtime errors even though the
	// pretends to not need it!
	// provide the generic type argument to avoid weird runtime errors even though the compiler
	// pretends to not need it!

[jcp19]

I don't understand this. In the case where we do have a file that we want to resolve, doesn't it matter at all if we found the json file or if not? In that case, I would expect that the return type of this function would be Either[Vector[VerifierError], Option[VerificationJobCfg]], and I would expect that we return Right(None) in this case

Update: I guess every every field in this VerificationJobCfg will be an optional, so nevermind what I said. Adding a comment before Right(VerificationJobCfg()) may be helpful to clarify this.

[jcp19]

Can we drop the (_)?

Suggested change

	fieldSelector(jobCfg).orElse(moduleCfg.default_job_cfg.flatMap(fieldSelector(_)))
	fieldSelector(jobCfg).orElse(moduleCfg.default_job_cfg.flatMap(fieldSelector))

[jcp19]

there are a few options that always get the default value (instead of being configurable). Is there a reason for that?

[jcp19]

does this mean that chopping never works if we provide a json config?

[jcp19]

Things get a bit tricky here, but wouldn't it be easier to resolve all paths before merging?

[jcp19]

Maybe we want to disallow passing options that take paths in "other"

[jcp19]

shall we mention here that a module config file must exist in the directory tree?