Problems with selective importing

[jcp19]

The content of imported packages is loaded lazily. While working on the stubs, I came across this bug. I have two source files A and B from different packages and A contains a call to a function defined in B.

• File A

package pkg

import "bug"

func main() {
    bug.F1()
}

• File B

package bug

pred Test() { true }

pure func f() bool {
    return true
}

requires Test()
func F1() {}

requires f()
func F2() {}

If I verify file A in Gobra, I get the following error

[error] Exception in thread "main" java.util.concurrent.ExecutionException: java.lang.RuntimeException: Predicate name Test_bug_F not found in program.
[error] 	at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
[error] 	at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:191)
[error] 	at viper.silicon.Silicon.verify(Silicon.scala:199)
[error] 	at viper.silicon.Silicon.verify(Silicon.scala:157)
[error] 	at viper.gobra.backend.Silicon.$anonfun$verify$1(Silicon.scala:27)
[error] 	at scala.concurrent.Future$.$anonfun$apply$1(Future.scala:672)
[error] 	at scala.concurrent.impl.Promise$Transformation.run(Promise.scala:431)
[error] 	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
[error] 	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
[error] 	at java.base/java.lang.Thread.run(Thread.java:834)
[error] Caused by: java.lang.RuntimeException: Predicate name Test_bug_F not found in program.
[error] 	at scala.sys.package$.error(package.scala:27)
[error] 	at viper.silver.ast.Program.findPredicate(Program.scala:270)
[error] 	at viper.silicon.supporters.qps.PredicateSnapGenerator$$anonfun$setup$1.applyOrElse(PredicateSnapGenerator.scala:26)
[error] 	at viper.silicon.supporters.qps.PredicateSnapGenerator$$anonfun$setup$1.applyOrElse(PredicateSnapGenerator.scala:24)

This occurs because the Test predicate is not included in the final viper file because it is not explicitly accessed. If the main function of A is changed to

func main() {
    fold bug.Test() // added explicit use of the Test predicate
    bug.F1()
}

then everything works again.

An analogous case occurs if I replace F1 with F2 in the main function of file A because the function f() accessed in the contract of F2 is also not explicitly mentioned in A, and thus, it is not added to the final code.

This has subtle consequences in case we ever opt to follow Go's practice of exporting only the upper case names, because we would need to guarantee that all entities accessed in the contract of an exported function/method are also exportable (i.e. have an upper case name).

A potential fix for this would be to perform a transitive closure to detect all dependencies of a function contract or else, to import everything in the final viper file.

[jcp19]

As a workaround, selective importing of a package's contents was disabled for now

[jcp19]

Update: there is a prototype solution on branch fix-selective-import

[Felalolf]

There is a 000166.gobra in our test set, so I assume that this issue has been resolved. Open it again if that is not the case.

[ArquintL]

There is a testcase because we disabled selective imports completely to make it work. This issue however is meant to eventually fix this such that we need to desugar, encode, and possibly verify less

[jcp19]

PR #619 provides a middle a good compromising solution to this issue. In particular, this solution does not desugar any private member, which should make the size of the translations into Viper in projects like SCION much smaller without requiring any extra analysis of the parsed program. The disadvantage is that it may not clean members as aggressively as a dedicated analysis could