Disjunctive aliasing constraints and permissions

[viper-admin]

Created by bitbucket user Korbinian Breu on 2014-02-21 09:11 Last updated on 2017-09-23 13:45

#!scala

method foo2(s: Seq[Ref])
  requires |s| > 2 && acc(s[0].f, write) && acc(s[1].f, write)
  requires (forall i2: Int :: i2 in [0..2) ==> s[i2].f == 0)
{}

Alternative syntax with quantified chunks works

#!scala

method foo2korbinian(s:Seq[Ref])
requires |s| > 2
requires forall i:Int :: i in [0..1) ==> acc(s[i].f, write)
requires forall i:Int :: i in [1..2) ==> acc(s[i].f, write)
requires forall i:Int :: i in [0..2) ==> s[i].f == 0
{}

[viper-admin]

@mschwerhoff commented on 2014-02-21 09:38

What's the issue here?

[viper-admin]

Bitbucket user ykass commented on 2014-02-21 15:46

The precondition of foo2 is self-framing, but Silicon reports an error.

[viper-admin]

@mschwerhoff on 2014-03-17 09:45:

• changed component from (none) to Quantified Permissions
• edited the description

[viper-admin]

@mschwerhoff commented on 2014-09-10 13:47

This issue is actually not related to quantified permissions, but it still looks as if the problem were splitting sequences. It verifies in Carbon, however.

[viper-admin]

@mschwerhoff on 2014-09-10 13:47:

• changed component from Quantified Permissions to (none)

[viper-admin]

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

The problem is most likely that Silicon doesn't find a chunk that matches s[i] for an arbitrary i in [0..2). This makes the issue related to https://github.com/viperproject/silicon/issues/16.

[viper-admin]

@mschwerhoff on 2014-10-06 08:21:

• changed component from (none) to Quantified Permissions

[viper-admin]

@mschwerhoff on 2014-10-06 08:22:

• changed component from Quantified Permissions to (none)

[viper-admin]

@mschwerhoff on 2015-06-08 15:20:

• changed component from (none) to Quantified Permissions

[viper-admin]

@mueller55 on 2015-06-11 15:29:

• changed the assignee from (none) to @mschwerhoff

[viper-admin]

@mschwerhoff commented on 2015-07-14 11:48

In order to document the issue, here is a copy of a mail in which I explained the issue:

This issue essentially says that, for a given sequence s, Silicon rejects the method precondition

requires |s| > 2 && acc(s[0].f) && acc(s[1].f)
requires forall i: Int :: i in [0..2) ==> s[i].f == 0
  /* Holds in Carbon, but fails in Silicon */

because access to s[i].f might be missing.

This is not actually a QP-related incompleteness, but rather a known incompleteness due to Silicon's treatment of non-quantified permissions. When checking the above snippet for well-formedness, Silicon essentially executes the following program:

inhale |s| > 2 && acc(s[0].f) && acc(s[1].f)
var i: Int
inhale 0 <= i && i < 2
assert acc(s[i].f) /* Fails */

The problem is that Silicon cannot find a (single) chunk that definitely provides permissions to s[i].f, although the heap in total clearly holds sufficiently many permissions.

Another example (due to Alex) that suffers from the same incompleteness is

inhale acc(x.f) && acc(y.f) && z == x || z == y
assert acc(z.f) /* Fails */

This example can be complicated further by using fractions, e.g 1/2, and by assuming that (z == x1 && z == x2) || (z == x2 && z == x3) || .....

(Side remark: the examples verify if Silicon-QP is used, and if f is "marked" as a quantified field.)

The incompleteness could be overcome by changing Silicon to consider all available chunks when looking for permissions, and to use an algorithm that is similar to that used in QP in order to generate a permission expression that includes all potentially contributing heap chunks. For the examples above:

assert acc(s[i].f)
  ~~> assert (  (s[i] == s[0] ? write : none)
              + (s[i] == s[1] ? write : none)
              + (s[i] == s[2] ? write : none))
             >= write

assert acc(z.f)
  ~~> assert (  (z == x ? write : none)
              + (z == y ? write : none)
             >= write

Field reads and updates would also have to change.

[viper-admin]

@mschwerhoff on 2015-07-14 11:49:

• changed priority from major to minor
• changed component from Quantified Permissions to (none)

[viper-admin]

@mschwerhoff on 2015-11-16 14:46:

• changed kind from bug to enhancement
• edited the title

[viper-admin]

@mueller55 on 2015-11-16 16:42:

• changed the assignee from @mschwerhoff to (none)

[viper-admin]

@mschwerhoff commented on 2016-04-10 17:24

See also https://github.com/viperproject/silicon/issues/36, https://github.com/viperproject/silicon/issues/232

[viper-admin]

@mschwerhoff commented on 2016-06-22 16:34

https://github.com/viperproject/silicon/issues/239 was marked as a duplicate of this issue.

[viper-admin]

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

The non-greedy consume algorithm implemented as part of robinsierra's bachelor's thesis solves this problem. For now, this algorithm is not used by default, it must be chosen explicitly by running Silicon with the command-line option --enableMoreCompleteExhale.