Permission incompletenesses

[viper-admin]

Created by @mschwerhoff on 2013-04-15 07:14
Last updated on 2017-09-23 13:41

The separation of the symbolic state into a heap and path conditions entails permission-related incompletenesses of various kinds and degrees. Silicon's current implementation several strategies to overcome them, for example

• heap compression if "assert true" is executed
• heap compression after new chunks are produced
• definitely-not-aliases information is computed from the heap when heaps are compressed
• chunks are first looked-up by a syntactic match, if this fails, by a semantic match (asking Z3)

However, several incompletenesses still exist, as illustrated by this test file (tip version).

My suggestion is to define an interface for heap lookups and to implement different heap lookup strategies that will (or can) be used a certain order. Questions to keep in mind are:

• Can the heap stay as it is, that is, without much business logic?
• Can chunks still be created manually or should the heap provide methods such as gainAccess, losePermissions or withChunk?
• Can we hold on to the invariant that if a chunk exists, then its permissions are definitely positive?

---

Attachments:

• incomp2.sil
• perm_incomp.sil

[viper-admin]

@mschwerhoff commented on 2014-01-26 14:05

#51 was marked as a duplicate of this issue.

[viper-admin]

@mschwerhoff on 2014-02-13 07:29:

• changed component from (none) to Permissions

[viper-admin]

@mschwerhoff commented on 2014-03-18 08:57

A partial solution has been implemented with #419. The question about a generalised lookup strategy is still open, however, and of greater interest after Korbinian's extension of Silicon.

[viper-admin]

@mschwerhoff commented on 2014-09-15 14:25

Related:

• Disjunctive aliasing constraints and permissions #72
• Incompleteness due to folding fractional permissions #119
• Different behaviour: impure conditionals vs. conditional permission expressions #205
• Using acc in combination with none fails unexpectedly #217
• Exhale acc(P(x), perm(P(x))) can fail surprisingly due to disjunctive aliasing constraints #232

[viper-admin]

@mschwerhoff commented on 2014-10-06 12:36

Here is another example for an incompleteness. Given the predicate

predicate P(x: Ref) {
  acc(x.f) && (x.f != null ==> acc(P(x)) && unfolding acc(P(x)) in true)
}

one could argue that

unfold acc(P(x))
assert x.f == null

should verify because of unfolding acc(P(x)) in ... in the predicate body. In fact, it will verify in Carbon, but not in Silicon, because the permission-related inconsistency of the state yielded by unfolding acc(P(x)) in ... is not "noticed" by Silicon/Z3.

[viper-admin]

@mschwerhoff commented on 2015-11-20 15:21

Another permission incompleteness is due to separate heap chunks and learning aliasing information after exhaling chunks to aliased receivers:

field f: Int

method test(x: Ref, y: Ref) {
  inhale acc(x.f, 1/2) && acc(y.f, 1/2)
    // x.f |-> vx # 1/2,  y.f |-> vy # 1/2
  inhale x.f == 1
    // x.f |-> vx # 1/2,  y.f |-> vy # 1/2
    // vx == 1
  exhale acc(x.f, 1/2)
  inhale x == y
    // y.f |-> vy # 1/2
    // vx == 1, x == y
  assert y.f == 1
    // Silicon: Assertion y.f == 1 might not hold
    // Because vy == 1 cannot be shown
}

[viper-admin]

@mschwerhoff commented on 2017-01-27 11:27

incomp2.sil illustrates another incompleteness that is currently not overcome by failure-driven state consolidations because these don't attempt proofs by contradiction.

In the example, the state consolidation triggered by failing to assert t != 0 is performed without being aware that t != 0 was to be asserted. That is, the state consolidation is not performed under the assumption that t == 0 were true. However, without effectively attempting a proof by contradiction, the state consolidation does not yield any new assumptions and the assertion will fail a second time.

[viper-admin]

@mschwerhoff on 2017-01-27 11:27:

• changed attachment from (none) to incomp2.sil

[viper-admin]

@mschwerhoff commented on 2017-09-23 13:41

Certain instances of this general completeness issue have been resolved as part of robinsierra's bachelor's thesis.