Incorrect optimization for inhale-exhale expressions

[gauravpartha]

Carbon omits well-definedness checks for inhale and exhale of assertions in cases where Carbon has already checked that those assertions are self-framing. For example, Carbon emits a single self-framing check for every precondition and then omits the well-definedness check when exhaling preconditions as part of a method call. This optimization is in general correct, but Carbon also applies it in cases where the assertions contain perm expressions in which case it is incorrect, because Carbon always does self-framing checks starting from the empty mask.

The following example, which verifies in Carbon, shows the incorrect behavior:

field f: Ref
field g: Int

method callee(x: Ref) 
    requires [true, perm(x.f) > none ==> 0/0 == 0/0 ]
{ 
}

method caller(x: Ref) {
    inhale acc(x.f)
    callee(x)
}

The call to callee should fail, because perm(x.f) evaluates to 1 and thus there is a division by 0. In the self-framing check of callee's precondition Carbon does not catch any error because perm(x.f) evaluates to 0 in that context.

[marcoeilers]

Note: I thought at first that this could be fixed by just doing the self-framing check for the exhale version of the precondition from an arbitrary valid mask instead of an empty mask. However, that still would not work in cases like this:

field f: Ref

method callee(x: Ref) 
    requires acc(x.f) && [true, perm(x.f) < write ==> 0/0 == 0/0 ]
{ 
}

method caller(x: Ref) {
    inhale acc(x.f)
    callee(x)
}

Here, the condition perm(x.f) < write will always be true for a caller exhaling the precondition, but it's never true after inhaling the first conjunct of the precondition (in the well-definedness check) from any valid state, i.e. any mask without negative permissions.