Incomplete behaviour when using gotos to jump out of loops

[viper-admin]

Created by @gauravpartha on 2019-04-17 12:57
Last updated on 2019-04-25 09:03

Carbon currently does not behave properly when jumping out of loops. The permissions which are framed away when entering the loop should be added back when jumping out of the loop. Carbon currently does not add those permissions, which means that one ends up with less permission than expected.

The following example shows the issue:

field g: Ref

method m(x: Ref) {
    var c: Int

    inhale acc(x.g)
    while(c > 0) 
    {
        if(c == 5) {
            goto l //when jumping out should go back to previous scope which holds permission to x.g
        }  else {
            c := c-1
        } 
    }

    label l
    //at this point one also needs to take into account the traces which reach via the goto

    inhale c == 5
    //at this point the only traces are those reached via the goto (for all others c <= 0 holds)
    assert perm(x.g) == 0/1 
    /*this assertion should fail, since full permission to x.g is held but
      the assertion succeeds in the current version of Carbon
    */
}

[viper-admin]

@alexanderjsummers commented on 2019-04-25 09:03

I modified the description a bit; since the design of loops/gotos hasn't been pinned down yet, I would rather indicate that the behaviour is currently unexpected.

It's good to have the clear example and issue; the fact that this doesn't work yet in Carbon follows from the fact that there is no proper implementation of gotos with respect to loops/invariants.

[viper-admin]

@alexanderjsummers on 2019-04-25 09:03:

• edited the title
• edited the description

[viper-admin]

@alexanderjsummers commented on 2019-04-25 09:03

Related: #182

[gauravpartha]

Fixed by #389