Skip to content

Stabilize support for friend package invariants #830

@jcp19

Description

@jcp19

Friend clauses have been introduced in #810, but the heuristics used to match the packages mentioned in the friends clauses with the packages that receive the resources are still very finicky and config dependent, and they do not work in our test suit (although they work when running outside the test suite).

This issue keeps track of two tasks that need to be done before this feature is stable:

  • make the heuristics to match the packages independent of the config
  • add a check that friendsClauses do not create loops in forwarding resources (this is prevented by the checks for that import relations are acyclical - for a package to send packages to itself, it must be able to import itself and state permission preconditions. that is not possible, as cyclical imports are rejected by the compiler. This generalizes to chains of imports with more than one package.
  • rename friend clauses to "friend package invariants" to make it clear that, logically, friend clauses are (logically) just a special case of a package invariant, and change syntax accordingly
  • provide good error messages

To allow for a once and for all specification of packages from the standard library, instead of having to provide the path to friend package in the friend package invariant, we could have introduce a key. All keys could be resolved, once per project, in a project config file.

pkg1/f.go

package pkg1

// @ friend pkgInvariant "key1" acc(&X)

var X/*@@@*/ int 

pkg2/f.go

package pkg2

// @ importRequires acc(&X)
import pkg1

project file (declared once per project, every package is verified against it):

{
    "pkg1": {
        "key1": PATH/TO/PKG2
    }
}

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions