Gobra CLI Input Documentation

[ArquintL]

Extends banner to explain the 3 different modes for providing inputs to Gobra.

@reviewers: Please let me know whether this is (1) understandable and (2) sufficient.

[Dspil]

Maybe I am biased because I already know what the flags do but the description seems sufficient

[Felalolf]

to my understanding the project root is relevant to resolve Go's package imports. Why is there no optional project root for -i. Also, if the project root works the same for any input kind, then maybe the project root can be explained as a separate entity.

[ArquintL]

This is what I tried to clarify on line 383:
You have the option --include in mind, which is indeed applicable to all 3 modes.
However, --projectRoot specifies a root directory based on which a unique identifier for each package should be derived (this is imho the only use case). This unique identifier is then used for caching purposes and the idea was that the same project on different computers (and thus different absolute paths) come up with the same unique package identifier (since the paths relative to the project root should be the same if configured correctly), such that cache files can be shared between machines

[ArquintL]

Getting back to your original question, I honestly don't recall why we explicitly excluded the project root option from -i. It might be related to the fact that the provided files might not fully represent a package (e.g. the files are located in different folders but all have the same package clause or only a subset of files of a package has been provided)

[Felalolf]

In the explanation, I believe it is still a good idea to give a separate explanation for --projectRoot if its semantics can be explained independent of the mode. Currently, it is also not clear to me what kind of criteria the argument to --projectRoot has to satisfy.

[Felalolf]

It seems to me that mode 2 and 3 are a bit confusing. Mode 2 could take a list of packages and then verify them. Mode 3 could take a list of dictonaries and verify all packages found therein (where one can still blacklist packages). The project root is a separate entity that just influences how package names are resolved. Then we would have an option to verify single files, single packages, and entire projects. Mode 2 could maybe even also use -i.

[ArquintL]

Isn't that what we have?
I think of these modes as follows:

• mode 1: take these files and verify them, don't care about where they are located in the filesystem
• mode 2: take these packages (specified via the directory in which they are located) and verify them
• mode 3: take this module / repo / ... and verify the packages in there (or only a subset as specified via includePackages and excludePackages)

[Felalolf]

I think the confusion comes from the concrete flags and mode 3. For mode 3, the repo is given in a roundabout way through --projectRoot which otherwise has a different purpose. The --includePackages is counterintuitive to me because it specifies additional packages in a command that is supposed to verify all packages in folders; "Verify all packages in my project, ... and also these ones". If mode 3 takes a list of dictonaries, then the --includePackages becomes redundant (and maybe mode 2 also becomes redundant). Regarding the flags, I think --dictonaries for packages and --recursive for something that currently does not have a provided target (like -d /wireguard -r) is a bit counterintuitive.

[jcp19]

I agree that the current separation between mode 2 and mode 3 is confusing, but at least the current description describes accurately what these modes do. From my perspective, --recursive should be an option for mode two, instead of a separate option (this way, we might be able to deprecate --projectRoot). Given this, we might want to change the flags already in this PR and change the corresponding description, or we might merge the description as is at the moment and later change it when we change the modes in a different PR

[ArquintL]

@jcp19 Felix suggested to merge the 2nd and 3rd input mode: -d <list of dirs> --projectRoot <optional project root> takes the provided list of directories and searches (recursively!) for packages in them. --includePackage and --excludePackage would control which packages end up being verified.
We were also thinking about good default values and I'd suggest the following: --projectRoot defaults to the current working directory (as of now). -d has to list at least one directory. (We could also default to the current directory or the project root but I don't see such a huge benefit justifying the added complexity of explaining what the default is)

Would this suggestion work for you / verified SCION? Or do you need something specifically from today's 2nd mode that would no longer be possible?

[jcp19]

@jcp19 Felix suggested to merge the 2nd and 3rd input mode: -d <list of dirs> --projectRoot <optional project root> takes the provided list of directories and searches (recursively!) for packages in them. --includePackage and --excludePackage would control which packages end up being verified. We were also thinking about good default values and I'd suggest the following: --projectRoot defaults to the current working directory (as of now). -d has to list at least one directory. (We could also default to the current directory or the project root but I don't see such a huge benefit justifying the added complexity of explaining what the default is)

Would this suggestion work for you / verified SCION? Or do you need something specifically from today's 2nd mode that would no longer be possible?

I would strongly oppose having the recursive mode take over the place of the directory mode for the following reasons:

• to me, it is a lot more common to verify a single package (i.e., the package I am verifying at the moment) instead of its entire list of dependencies.
• To have the behavior that I want, I would need to pass even more flags (by means of the include and exclude packages), which makes the usual case for me quite laborious. In particular, if the packages passed to includePackages are themselves verified recursively, I would need to pass a single package and exclude all its dependencies. For reference, the router package of scion depends directly on, at least, 35 packages.
• From a usability standpoint, having the recursive mode by default sounds odd and may surprise users - for example, most command line tools I know allow you to apply a command recursively (usually, with -r or -R), but I don't recall seeing one command that does it by default.

If we were to delete a mode, I would delete the recursive mode but keep the option --recursive (to the directory mode, that is) and I would drop the includePackages option, which to me always felt redundant. Instead, we could verify recursively the list of packages passed to the directory mode, with the exception of those listed in excludePackages.

[ArquintL]

Interesting! For me, includePackages is very handy:
I configure the Gobra command once more a particular module (consisting of various packages in its subfolders) by specifying the project root (i.e. the current directory) and the include paths (i.e. some directory to which I've downloaded (external) dependencies). I then either verify all packages in the module or individual ones by using includePackages.

includePackages is by no means recursive and (as soon as it's provided) acts as an allow list such that only the listed packages are verified (independently of the directories (whether recursive or not) provided as input to Gobra)

[jcp19]

includePackages is by no means recursive and (as soon as it's provided) acts as an allow list such that only the listed packages are verified (independently of the directories (whether recursive or not) provided as input to Gobra)

Why do you prefer includePackages over passing a list of directories to the directory mode? Is it because that way you can only pass the package name instead of the full path? I wonder if we could combine the two in the directory mode

[ArquintL]

I'd say that's the reason. More specifically, if I don't add --includePackages it will verify all and if I provide it (usually with only a single package name) verification is restricted. This seems more elegant to me that either specifying 8 or 9 paths to different packages (when I want to verify them all) or use 2 completely different set of commands to invoke Gobra

[jcp19]

The problem is that you may have different packages with the same name, in which case this approach is no longer expressive enough

[ArquintL]

The problem is that you may have different packages with the same name, in which case this approach is no longer expressive enough

That's correct. I think in that case one must resort to the directory mode