double permission inhale leads to unexpected verifications

Question

I have trouble understanding some behaviour of Viper, which, imho, seems to be a bug.

The following code fails to verify due to a lack of permissions for bar.val_int on the assignment. This makes total sense.

field val_int: Int
method foo() {
   var bar: Ref
   inhale acc(bar.val_int)
   exhale acc(bar.val_int)
   bar.val_int := 2
}

Yet, the following code verifies successfully:

field val_int: Int
method foo() {
   var bar: Ref
   inhale acc(bar.val_int)
   inhale acc(bar.val_int)
   exhale acc(bar.val_int)
   exhale acc(bar.val_int)
   bar.val_int := 2
}

As a matter of fact, one can add an arbitrary number of exhales, as long as there are two inhales (for full permissions) at the top, the code will always verify. Is this a bug, intentional, or am I missing something weird that is happening?

I would have expected the second inhale to have no effect, as a full permission is already held for the heap location. However, even if somehow a double write permission is help (which should be illegal?), then at least I would expect the two exhale statements to revoke these permissions, leaving again no permissions at the moment of assignment.

Malte Schwerhoff · Answer 1 · 2020-06-30T09:51:24.740

Write/full permissions to field locations are exclusive, i.e. it is an implicit invariant of Viper's logic that, given a single location x.f, the total permission amount to x.f is at most write/1. See also the Viper tutorial, in particular this subsection about exclusive permissions.

Due to this invariant, the sequence of inhales — and inhales are basically "just" permission aware assumes — from your second snippet

inhale acc(bar.val_int)
inhale acc(bar.val_int)

is thus equivalent to

assume false

Once false has been assumed (which, if you think operationally, means "this and subsequent code is not reachable"), it doesn't matter which Viper statements follow afterwards. In particular, no sequence of exhales will un-assume false.

Thinking in Proof Rules

If you're more used to thinking in deductive proof rules, consider the following proof rules related to contradictions in propositional logic

   A ∧ ¬A                    A ∧ ¬A 
 ----------     or even:   ----------
   false                       B

which say that false follows from A ∧ ¬A, or rather that any conclusion B follows from such a contradiction.

Basically, Viper's instance of separation logic includes the following related rule:

   acc(x.f, p)  acc(x.f, q)
 ------------------------------ if 1 < p + q
             false

The rule captures aforementioned invariant of the logic that permissions to a field x.f may not exceed full/write permissions, i.e. 1.

In your case, the two inhales establish the necessary premisses, and Viper thus concludes false.

double permission inhale leads to unexpected verifications

1 Answers1

Thinking in Proof Rules