Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Gobra CLI Input Documentation #610

Merged
merged 2 commits into from
Jun 24, 2024
Merged

Gobra CLI Input Documentation #610

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a1b0f8e
improves documentation of Gobra's 3 input modes
ArquintL Feb 2, 2023
529b823
Applies CR suggestions
ArquintL Jun 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/main/scala/viper/gobra/Gobra.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ import scala.concurrent.{Await, Future, TimeoutException}

object GoVerifier {

val copyright = "(c) Copyright ETH Zurich 2012 - 2022"
val copyright = "(c) Copyright ETH Zurich 2012 - 2024"

val name = "Gobra"

Expand Down
32 changes: 28 additions & 4 deletions src/main/scala/viper/gobra/frontend/Config.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -443,8 +443,32 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
)

banner(
s""" Usage: ${GoVerifier.name} -i <input-files> [OPTIONS] OR
| ${GoVerifier.name} -p <directory> [OPTIONS]
s""" ${GoVerifier.name} supports three modes for specifying input files that should be verified:
| ${GoVerifier.name} -i <input-files> [OPTIONS] OR
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

| ${GoVerifier.name} -p <directories> <optional project root> [OPTIONS] OR
| ${GoVerifier.name} -r <optional project root> <optional include and exclude package names> [OPTIONS]
|
| Mode 1 (-i):
| The first mode takes a list of files that must belong to the same package.
| Files belonging to the same package but missing in the list are not considered for type-checking and verification.
| Optionally, positional information can be provided for each file, e.g. <path to file>@42,111, such that only
| members at these positions will be verified.
|
| Mode 2 (-p):
| ${GoVerifier.name} verifies all `.${PackageResolver.gobraExtension}` and `.${PackageResolver.goExtension}` files in the provided directories,
| while treating files in the same directory as belonging to the same package.
| Verifies these packages. The project root (by default the current working directory) is used to derive a
| unique package identifier, since package names might not be unique.
|
| Mode 3 (-r):
| Transitively locates source files in subdirectories relative to the project root (by default the current
| working directory) and groups them to packages based on the relative path and package name.
| --includePackages <package names> and --excludePackages <package names> can be used to allow-
| or block-list packages.
|
| Note that --include <directories> is unrelated to the modes above and controls how ${GoVerifier.name} resolves
| package imports.
|
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

@jcp19 jcp19 Jun 18, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

|
| Options:
|""".stripMargin
Expand Down Expand Up @@ -763,14 +787,14 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals

val noVerify: ScallopOption[Boolean] = opt[Boolean](
name = "noVerify",
descr = s"Skip the verification step performed after encoding the Gobra program into Viper.",
descr = s"Skip the verification step performed after encoding the ${GoVerifier.name} program into Viper.",
default = Some(ConfigDefaults.DefaultNoVerify),
noshort = true,
)

val noStreamErrors: ScallopOption[Boolean] = opt[Boolean](
name = "noStreamErrors",
descr = "Do not stream errors produced by Gobra but instead print them all organized by package in the end.",
descr = s"Do not stream errors produced by ${GoVerifier.name} but instead print them all organized by package in the end.",
default = Some(ConfigDefaults.DefaultNoStreamErrors),
noshort = true,
)
Expand Down
Loading