Unexpected behaviour for well-definedness during exhale

[gauravpartha]

Carbon's well-definedness encoding for an exhale is currently independent from the actual encoding of the actual exhale itself. In particular, the well-definedness encoding does not take side-effects performed during the exhale into account. This has two consequences:

Issue 1: Unexpected error reporting

exhale acc(x.f) && 0/0 == 0

The above code fragment reports a division by 0 well-definedness error in a state with no permission. Since the first conjunct cannot be exhaled one might rather expect an error message saying that acc(x.f) cannot be exhaled (which is what Silicon does)

Issue 2: Potential unsoundness in the presence of permission introspection

inhale acc(x.f)
exhale acc(x.f) && (perm(x.f) == none ==> 0/0 = 0/0)

verifies in Carbon. Currently, Viper's permission introspection during an exhale takes side-effects before the evaluation of the permission introspection into account. That is, perm(x.f) in the exhale should evaluate to none, which means there is a division by 0 well-definedness error (which is also what Silicon reports).

Carbon's encoding of permission introspection in the actual exhale part does take side-effects into account, but the well-definedness check does not. In particular, if one replaces 0/0 by 1 in the example above, then Carbon complains that 0/0 might not be equal to 1.

[gauravpartha]

There is a third issue, which is an incompleteness issue. This is just a different version of Issue 2 mentioned above.

Consider

inhale acc(x.f)
exhale acc(x.f) && (perm(x.f) != none ==> 0/0 == 0/0)

This program should verify, but Carbon reports a well-definedness error, because permission introspection is resolved incorrectly.

The first issue (unexpected error reporting) and the incompleteness issue also shows up for forperm. I am not sure whether one can find an example with forperm that is unsound, because Carbon's well-definedness check will check well-definedness for a superset of the actual values that have nonzero permission (since the well-definedness permission mask contains more permission than the currently active permission mask).

The following example illustrates an incompleteness issue with forperm:

var y: Ref
var z: Ref
inhale acc(y.f) && acc(z.f)
exhale acc(y.f) && forperm x: Ref [x.f] :: x != z ==> 0/0 == 0/0

x must be z in the body of the forperm and thus the body of the forperm is trivially well-defined. However, Carbon still reports a well-definedness error, because it does not take the first conjunct of the exhale (acc(y.f)) into account for the well-definedness check.

[gauravpartha]

#457 fixes this issue.