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.