Discrepancy between Carbon knownfolded permissions and Silicon predicate snapshots

[gauravpartha]

Both backends currently use techniques to record resources that are folded into predicates. Carbon uses a knownfolded permission approach (based on an extension of [1]) and Silicon uses a predicate snapshot approach. Both approaches can be seen as approximating the same semantics. However, the approaches provide different approximations, which can lead to different results. This is fine if we agree that the Viper semantics should be a more abstract one but it also might be that we want to unify the two backends in order to give consistent results across tools.

The following example illustrates one discrepancy due to the use of the two approaches:

field f: Int

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

method m(x: Ref)
    requires acc(x.f) && x.f == 3
{
    fold P(x)
    exhale acc(x.f, 1/2)
    inhale acc(x.f, 1/2)

    assert x.f == 3
    /* The assertion is verified in the knownfolded approach, but fails in the 
       snapshot based approach.
       Modifying the inhale statement to `unfold P(x)` leads to the assertion
       being verified in both approaches. 
       */
}

[1] S. Heule, I. T. Kassios, P. Müller, and A. J. Summers: Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions; ECOOP 2013