Carbon does not catch predicates that are not well-defined due to multiplication

[gauravpartha]

The following example verifies in Carbon but not in Silicon (there is an analogous example for fold):

field f: Int

predicate P(x: Ref, y: Ref) {
    acc(x.f, 2/1) && y.f > 0
}


method m(x: Ref, y: Ref) {
    inhale acc(P(x, y),1/2)


    unfold acc(P(x,y), 1/2)
}

The example should not verify for multiple reasons:

1. The inhale statement inhales a predicate instance that is not well-defined: acc(P(x,y), ½) corresponds to a predicate instance that satisfies acc(x.f) && y.f > 0. y.f has no meaning here. Thus, one could argue that the existence of the inhale should already be reported as an error. Neither Carbon nor Silicon complain about this inhale.
2. The unfold statement explicitly inhales the body of acc(P(x,y), ½), which is not well-defined. Carbon uses an optimized inhale (i.e., no definedness checks) and thus does not report an error (presumably because Carbon already checked self-framedness of the predicate body). Silicon reports an error for the unfold.

In the above program, the body of P(x) is self-framing, because acc(x.f, 2/1) is unsatisfiable. An analogous example applies for a predicate body that does not have unsatisfiable conjuncts and instead relies on non-aliasing properties (that are not guaranteed anymore once one scales the predicate down via multiplication).

The underlying issue is that the condition “predicate bodies must be self-framing” is not a sufficient condition to guarantee that every predicate instance in a Viper program is well-defined without further checks.

[marcoeilers]

I guess to avoid this we'd either have to re-check well-definedness on unfold, or verify well-definedness using an unknown positive multiplicator?

[gauravpartha]

I guess to avoid this we'd either have to re-check well-definedness on unfold, or verify well-definedness using an unknown positive multiplicator?

In general, yes. But I think there is a fundamental difference between the two. Rechecking well-definedness on unfold (as Silicon does now) would basically allow the inhale to succeed (which it also does for Silicon). I'm wondering whether Viper should in general report an error when there is a predicate instance that is ill-defined (such as acc(P(x,y), 1/2) in the example above). If yes, then rechecking well-definedness on unfold would not be sufficient. In such a case, verifying framedness once-and-for-all using an unknown positive multiplicator would be better.

Edit:
Checking framedness once-and-for-all in the unbounded logic does not work (I thought it might initially). Checking framedness in the unbounded logic amounts to not assuming good state when checking framedness (in the example above, inhaling acc(x.f,2/1) would not go to magic). As @alexanderjsummers noticed, if function preconditions require specific fractions, then checking framedness in the unbounded logic may succeed even though one may not have the necessary permission after multiplication. In general, there is an issue with functions, because one would not be able to show the framedness property for any predicate that contains functions with preconditions that require a specific fraction. @alexanderjsummers suggested that this may be another good reason to actually interpret all permissions in function preconditions as wildcard amounts (as we have discussed in the past).

What do you think? Potentially worth a discussion in a Viper meeting. But maybe in any case it makes sense to just recheck well-definedness of the inhaled body on unfold until we have a decision.

[gauravpartha]

The problem goes beyond Carbon's optimization. viperproject/silver#809 shows an example that Carbon verifies without the optimisations and that Silicon verifies also, but which I think should not be verified. Thus, re-checking well-definedness on unfold may not be sufficient.

[alexanderjsummers]

I think we should check self-framedness with the unknown positive multiplier. This means the check remains attached to the definition where the problem is introduced; dually, it doesn't rely on how the predicate is used in the code (if at all) to detect the issue. However, this will require us to make the long-awaited change to function preconditions too (which I think is agreed on, but I don't know if we finalised a specific design)