Precondition information from unfolding unknown when using fractional permission

[viper-admin]

Created by @marcoeilers on 2017-02-14 14:52 Last updated on 2017-05-10 18:34

The following program fails to verify; in the last line of method m, Carbon says the "precondition of function actual might not hold. Assertion req(r) might not hold".

If one removes the fraction 1/2 in the unfolding expression in the precondition, the program verifies.

predicate outer(r: Ref) {inner(r)}
predicate inner(r: Ref) {true}

function req(r: Ref): Bool

function actual(r: Ref): Int
    requires req(r)

method m(r: Ref)
    requires outer(r)
    requires unfolding acc(outer(r), 1/2) in req(r) // remove 1/2 here to make it work
{
    var i: Int := actual(r) // fails
}

---

Attachments:

• test2.bpl
• test1.bpl

[viper-admin]

@marcoeilers commented on 2017-04-23 18:09

I looked into this a little, I think I now have some idea what's going on. In Boogie, at some point during the verification of m, req(Heap, r_1) is assumed. Then all kinds of modifications to the Heap are made, and then later it tries to assert req(Heap, r_1). As far as I can see, this is supposed to work because we learn from the assumption that state(Heap, Mask) ==> req#frame(EmptyFrame, r_1).

But I can't actually assert req#frame(EmptyFrame, r_1) after making the assumption, presumably because state(Heap, Mask) might not hold there, and is only assumed after the heap is modified again (I think to increment the predicate version, in case there is some permission left over; this would therefore not happen if the unfolding completely got rid of the predicate, which would explain why the example verifies if I remove the 1/2).

Should state(Heap, Mask) maybe be assumed before or after req(Heap, r_1) is assumed? Or should req(Heap, r_1) actually be assumed later, after the heap has been modified (and right before state(Heap, Mask) is assumed again)? These are pretty much the only two options I can see right now.

[viper-admin]

@marcoeilers on 2017-04-23 18:09:

• edited the description
• changed priority from major to critical

[viper-admin]

@marcoeilers on 2017-05-02 09:57:

• edited the description

[viper-admin]

@marcoeilers commented on 2017-05-02 10:03

I found what I think is another instance of the same problem:

function SCIONPath_get_hof(self: Ref): Ref
  requires acc(outer(self), wildcard)
{
  (
  let idx_0 == 
  (unfolding acc(outer(self), wildcard) in self.whatever) 
  in 
  (unbox(box(false)) ? null : null))
}

predicate outer(r: Ref) {acc(r.whatever)}

function isBool(r: Ref): Bool
function box(b: Bool): Ref
    ensures isBool(result)
function unbox(r: Ref): Bool
    requires isBool(r)

field whatever: Int

Carbon complains that Precondition of function unbox might not hold. Assertion isBool(box(false)) might not hold.

[viper-admin]

@marcoeilers commented on 2017-05-02 10:05

Attached Boogie file for first example.

[viper-admin]

@marcoeilers on 2017-05-02 10:05:

• changed attachment from (none) to test1.bpl

[viper-admin]

@marcoeilers commented on 2017-05-02 10:06

Attached Boogie file for second example.

[viper-admin]

@marcoeilers on 2017-05-02 10:06:

• changed attachment from (none) to test2.bpl

[viper-admin]

@alexanderjsummers commented on 2017-05-08 21:05

The original problem is now fixed, but I'm leaving the issue open, since the changes suggested to the encoding haven't actually been made yet (and I think they should be). It turns out that a different fix to function framing, and a slightly more-liberal approach to handling unfolding expressions helps already.

[viper-admin]

@alexanderjsummers commented on 2017-05-08 21:05

The changes are in commits https://github.com/viperproject/carbon/commit/eb4a7ca4de00a8e9b5a770101840a7ec135150a2 and https://github.com/viperproject/carbon/commit/94ff859940d681f0fcc748c9611ba8c5eb288236

[viper-admin]

@alexanderjsummers commented on 2017-05-09 13:27

I think the second example is a different problem. In the Boogie code you attached for it, the postcondition of box doesn't even seem to show up. It seems that something about the nesting of the expressions causes Carbon to get confused about how it should be checking/assuming properties of the subexpressions.

[viper-admin]

@marcoeilers commented on 2017-05-10 18:34

Thanks for looking into it; I created a separate issue (https://github.com/viperproject/carbon/issues/200) for the second example.

[gauravpartha]

@marcoeilers Can one close this issue?