Inhaling negative permission goes to magic

[tdardinier]

Currently, both Silicon and Carbon consider accessibility predicates with negative permissions (such as acc(x.f, -1/2)) as well-defined, but false. Thus, the following program is verified by both Silicon and Carbon:

field f: Int

method main(x: Ref)
{
    inhale acc(x.f, -1/2)
    assert false
}

It is unclear why such a behavior would be useful (and even sound). Treating accessibility predicates with negative permissions as not well-defined seems like a better choice. That is, statements like inhale acc(x.f, -1/2) should actually fail (because they are not well-defined).

[mschwerhoff]

The original motivation were simpler preconditions with symbolic permissions, if I remember correctly. However, the decision was probably heavily influenced by Chalice, which had integer fractions rather than a dedicated permission type. Moreover, most other well-definedness conditions in Viper are either already checked in in- and exhale position (divison by zero, sequence indices), or at least should be (e.g. injectivity of QPs).

Potential technical issue: currently, requires acc(x.f, p) for p: Perm succeeds because none <= p is assumed. Since Perm is encoded as SMT reals, a well-definedness check would fail since p < 0.0 is possible. I don't believe that SMT solvers support unsigned reals/rationals, so explicit assumptions on encoded permissions are necessary, including permission-typed functions, quantified permission-typed expressions, etc., which requires corresponding changes in the backends or frontends.

[mschwerhoff]

Viper meeting 1.7.2021:

• Most symbolic permissions probably need none < p anyway
• Implement by Fr 16.7.2021, for the upcoming release
• Ideally, also implement receiver injectivity checks for QP assertions for upcoming release

[mschwerhoff]

@tdardinier I've created Silver branch silver-issue-522 to host new/changed tests, and I've started changing Silicon . I suggest we both test the backends against the new Silver branch, and coordinate the final mergers.

[marcoeilers]

Since the fix was implemented and merged a while ago, I'll close this.