Including verification dependencies breaks imports

[HSMF]

In a setup containing nested projects, such as when including dependencies as git submodules, importing packages from that dependency is not possible.

Below is a simplified structure from including viperproject/gobra-libs:

├── main.gobra
└── pkg
    ├── math
    │   └── math.gobra
    └── util
        └── util.gobra

main.gobra

package main
//+gobra

import "pkg/math"

func client() {
	assert math.Bar() == 1
}

pkg/util/util.gobra

package util
//+gobra

ghost
decreases
pure func Foo() int {
	return 1
}

pkg/math/math.gobra

package math
//+gobra

import "util"

ghost
decreases
pure func Bar() int {
	return util.Foo()
}

---

Verifying pkg on its own works fine: Running gobra -r -I . in pkg yields no errors.

Verifying the client project, however, does not work: gobra -I . -p . yields the following error:

19:13:19.993 [thread-6] ERROR viper.gobra.reporting.FileWriterReporter - Error at: <./pkg/math/math.gobra:4:8> ./pkg/math/math.gobra:4:8:error: Explicit qualifier could not be derived (reason: 'No existing directory found for import path 'util'')
import "util"
       ^

19:13:20.000 [thread-14] ERROR viper.gobra.reporting.FileWriterReporter - Error at: <./main.gobra:3:8> ./main.gobra:3:8:error: Package contains 1 error(s): ./pkg/math/math.gobra:4:8:error: Explicit qualifier could not be derived (reason: 'No existing directory found for import path 'util'')
import "util"
       ^

import "pkg/math"
       ^

Note that changing the import in pkg/math from import "util" to import "pkg/util" is not sufficient, as this will break verification of pkg on its own.

[ArquintL]

This issue describes the current behavior of Gobra. The Go language specification is very ambiguous about what ImportPath's semantics are (see here). I'm thus wondering what the expected behavior / the behavior of the Go compiler are. @HSMF Does this structure stem from an existing package hierarchy that should be verified? I tried to recreate this in Go playground but could not get it to work without using modules. For projects that consist of multiple packages, I usually resort to using Go modules. Is this not an option here?

[jcp19]

@ArquintL we are verifying parts of the go standard library and we are trying to import gobra-libs there to avoid doing everything from scratch. How would you use modules here for this particular case?

[ArquintL]

@jcp19 I'm happy to discuss this in person but I can spontaneously think of the following options:

• make gobra-libs a module, which seems to already be the case. You could then use the module system to specify gobra-libs as a dependency of the standard library. I guess it's a bit weird to import a presumably ghost-only package but if you make the import non-ghost, you can build up on Go's tooling to fetch modules from a repository. I also have my own tooling to symlink these downloaded modules to make configuring Gobra easier to find them. Biggest downside imho is that you have to make the standard library a module too (I don't know whether this is already the case) and that you don't get any tooling from Go if gobra-libs is a truly ghost and gets ghost-imported.
• add gobra-libs (manually) as a submodule to the standard library's root folder (or some special .verification subfolder) and configure Gobra accordingly, i.e., -I . and -I .verification, respectively. This corresponds to the directory structure as outlined in this issue. What I would however change is that pkg/math/math.gobra should import "util" as import "pkg/util" where pkg is the module name, such as gobra-libs. To verify pkg / gobra-libs, one can use --module pkg such that Gobra ignores this prefix for all imports within this module. This differs from the example stated in this issue. While writing these lines, I became unsure whether import "util" is correct too (would be nice to check this with the Go compiler). A quick search lead to the following evidence that import "pkg/util" is correct:
  • default Go playground for multiple files (which uses modules): Package foo is imported as import "play.ground/foo"
  • this StackOverflow issue seems to suggest that the Go compiler cannot handle an import like import "util" unless you cleverly configure the GOPATH to consider the directory in which folder util` is.
  • I read the Go module reference as stating in the glossary for "module path" and "package path" that import paths should be prefixed with the module name.