Unfolding with no permissions and predicate well-definedness

[mschwerhoff]

Consider the following example:

field f: Int

predicate P(x: Ref, y: Ref) {
    acc(x.f) && x.f > 0 && (x.f > 0 ==> y != null) // Is well-defined
}

method test(x: Ref, y: Ref) {
    inhale acc(P(x, y), none)
    unfold acc(P(x, y), none) // Permission-scaled predicate body is no longer well-defined
    assert y != null
}

Silicon reports insufficient permissions to x.f at the unfold statement (because it can't find a heap chunk with non-zero permissions that would allow reading x.f).

Carbon happily verifies the program, although, I would argue, y != null should not be implied if x.f can't even be read.

I would suggest to simply disallow unfolding with no permissions.

[dewert99]

This seems to be able to lead to more general unsoundness as seen in the following example

predicate falze()
{
    false
}

method test(){
    unfold acc(falze(), none)
    assert false
}

This verifies with both backends

[alexanderjsummers]

I think I'm in favour of Malte's suggestion, although we generally allow for none amounts in these positions. For example, inhaling none of a predicate is allowed, as is inhaling acc(pred(x), p) where p is just known to be non-negative. I guess then an unfold acc(pred(x),p) would fail for such an unknown p and would have to be made conditional. Could this be annoying, e.g. for "unfold as much predicate as I have" usages? I'm not sure these are common, but can currently be achieved with unfold acc(pred(x),perm(pred(x))) I guess.

The alternative would be to have the backends explicitly case-split on none values and not use the body in this case. An advantage would be flexibility in the scenarios above (and a bit more consistency with how acc(...,p) can be used elsewhere); a disadvantage would be that after such an unfold one probably expects to know what held in the body?

[dewert99]

This also seems to affect unfolding for example

predicate falze() {
    false
}

method test1() {
    assert unfolding acc(falze(), none) in true
    assert false
}

also verifies with both backends

[mschwerhoff]

You raised an interesting point about "unfold as much predicate as I have", @alexanderjsummers. Conditionals could help here, e.g. if (perm(pred(x))) { unfold acc(pred(x),perm(pred(x))); } (analogously, an implication guarding an unfolding), but a less intrusive solution would be better.

I like the solution you proposed (case split), and regarding your final question: I'd be surprised if it caused problems in situations where code is parametrised with a symbolic permission amount p because, if the predicate (and its unfolding) were really relevant, p would most likely be known to be greater than none.

On the other hand, I'm a bit worried about the effect (on the implementation and performance) that the additional branching will have in Silicon. Regarding performance, the effect would probably be analogous to that of additional user-provided conditionals (as mentioned above), but it will complicate the implementation (unlike user-provided conditionals).

[marcoeilers]

We discussed this in the Viper meeting on September 19th and decided to forbid unfolding with no permissions.