Strange behaviour of unconstrained quantified permissions

[viper-admin]

Created by @alexanderjsummers on 2018-06-04 15:54
Last updated on 2018-06-06 10:25

In the following example, an assumption guarantees that a particular field location is not given permission by a quantified permission, but the permission is still available in practice. I suspect this is related to an unsoundness in the axiomatisation (see this Carbon issue and its accompanying test case in the test suite), but it is not possible to e.g. prove false.

#!scala
field val : Int

function bool2Ref(b: Bool) : Ref

method m(x:Ref)
  requires forall b:Bool :: acc(bool2Ref(b).val)
  requires x != bool2Ref(true) && x != bool2Ref(false)
  {
    x.val := 4 // should fail (but doesn't)
    assert false // does fail
  } 

[viper-admin]

@alexanderjsummers on 2018-06-04 15:55:

• edited the description

[viper-admin]

@alexanderjsummers commented on 2018-06-04 16:08

I suspect there to be an unsoundness here, but it's a bit more hidden than in the Carbon issue (linked). It seems to me that there is an explicit notion of the codomain of the mapping (from quantifier instances to references) not accounted for in the current axiomatisation.

[viper-admin]

@alexanderjsummers on 2018-06-04 16:08:

• changed priority from major to critical

[viper-admin]

@mschwerhoff commented on 2018-06-05 07:16

Yes, the finiteness of the Boolean domain most likely causes an unsoundness since it is not accounted for in the current encoding. A sound encoding is given in my thesis on page 108.

[viper-admin]

@alexanderjsummers on 2018-06-06 10:25:

• edited the description

[marcoeilers]

Fixed.