Invariants on labels should be disallowed unless they form loop heads and while loops that are not loop heads should be rejected

[viper-admin]

Created by @alexanderjsummers on 2019-10-30 08:47

Because of how loops are verified, the current meaning of an “invariant” on a label varies significantly depending on whether the label represents the head of a loop or not. Since there is no motivation for “invariant”s on non-loop-head labels, we should make this an error.

It might become frustrating that one cannot manually choose a label to be a loop head, and also cannot see which labels were chosen as loop heads. We could consider providing extra feedback in the corresponding error message, and potentially (in cases for which the choice of loop head is ambiguous) allowing a user to declare that a label is supposed to be a loop head (in fact, once this issue is fixed, an invariant annotation would do just that).

[gauravpartha]

I agree. It's not clear to me whether one should do this before the AST reaches the backends. In Carbon, for example, it would be easy to report this using the new loop infrastructure.

Currently, we have multiple tests in the test suite, which contain labels (as well as while loops) that have invariants but are not loop heads. In one case, I would argue that the test is incorrect even if one just ignored labels with invariants that are not loop heads (taken from all\invariants\loops1.vpr):

method test03(x: Ref)
  requires acc(x.f)
  ensures  acc(x.f) && x.f == old(x.f)
{
  var n1: Int
  var n2: Int

  label lh1 // outer loop head
    invariant acc(x.f, 1/2)

  assert perm(x.f) == 1/2 //POINT A

  label lh2 // inner loop head
    invariant acc(x.f, 1/3)

  assert perm(x.f) == 1/3

  n2 := n2 + 1
  if (n2 == 0) {
    goto endofprogram
  }
  goto lh2 // back-edge inner loop

  // ----- begin dead code
  assert perm(x.f) == 1/2

  n1 := n1 + 1
  if (n1 != 0) {
    goto lh1 // back-edge outer loop
  }

  // ----- end dead code

  label endofprogram
  assert n2 == 0 || n1 == 0
}

In this program, one may think that lh1 is the outer loop head. However, as the comments also indicate, the only candidate for the backedge (goto lh1) is not reachable in the CFG. Thus, lh1 is not a loop head and we should disallow the program (Silicon verifies the assertion which may indicate to the user that this is an actual loop head). Moreover, if one ignored the corresponding invariant, then the assertion at point A should definitely fail.

Another example from the test suite (all\invariants\while3.vpr):

  while (b)
    // invariant !b ==> false
  {
    goto end
    b := false
  }

Here the while loop is not a loop head, because the end of the body is never reached. Even though the invariant is commented out, I think in this case, we should also disallow the program (as we have discussed in the past).

I propose to change all such tests in the test suite where there are labels with invariants that do not form loop heads or while loops that do not form loop heads. Once we have decided who should report (i.e., silver or backends) and how we should report these cases, I guess we can add test cases that check whether the "incorrect loop head error" is reported. But I would like to make the test suite consistent with this view first.
I think the only counterargument is that frontends would have to check whether a while loop/label is really a loop head, which may be cumbersome (for example, a source program may very well just jump out of the loop always).

Do you agree with my proposal or do you have any other thoughts/opinions? @alexanderjsummers @mschwerhoff @dohrau

[fpoli]

Could the label invariant be encoded as an assert <invariant> in case the label is not a loop head?

Anyway, in Prusti we currently encode loops as loop-free Viper CFGs, so it should not change much for us.

[gauravpartha]

Could the label invariant be encoded as an assert <invariant> in case the label is not a loop head?

Anyway, in Prusti we currently encode loops as loop-free Viper CFGs, so it should not change much for us.

This is definitely an option, but might confuse users, since the semantics of a label changes drastically depending on whether the label is a loop head or not (and sometimes it's not clear whether it is a loop head by just quickly looking at the program). I don't have a very strong opinion on this.

Thanks for expressing the Prusti viewpoint!

@marcoeilers @Felalolf : Would Nagini/Voila/Gobra be affected by the above discussion?

[Felalolf]

Currently, Gobra is not using label invariants. I do not have strong feelings about how invariants for non-head labels should be handled.

[marcoeilers]

Nagini and 2Vyper also don't use label invariants and wouldn't be affected.

[mschwerhoff]

Voila also doesn't use labels with invariants.

Generally, I'm also in favour of keeping the semantics simple, and would thus reject non-loop-head labels with invariants. But as a consequence, we might force users to optimise a program in ways that should not matter for verification, as Gaurav's example with the degenerated while-loop shows.

Getting a technical error ("non-loop-head label with invariant found") here might leave users puzzled. Getting a more informative message ("while-loop not actually a loop", or "while-loop body executed at most once") could suggest to users that we perform some kind of control-flow optimisation analysis for finding dead code etc. — which we don't generally do, e.g. we don't reject "if (b || !b) s1 else s2" as being unnecessary complex.

I can imagination that having code rejected for nonobvious reasons can be annoying while working on an example, e.g. in the IDE. During the development, such degenerate control-flow might show up temporarily, but users should not be forced to clean up their programs to keep going.

We could allow any label to have an invariant, and additionally provide an option for switching on (potentially more general) "dead code" checks for users that want such information.

[gauravpartha]

If we allow while loops to exist that are not loop heads (I remember @dohrau mentioning that the CFG detection does not work properly then, so we should get his opinion on this), then we should also decide what the verifier semantics is in such a case. In my opinion, the semantics should always reflect the semantics of the CFG. This means an invariant only has a meaning if it is associated with a loop head (otherwise formalizing the semantics is cumbersome, since the CFG semantics would have to depend on a notion of invariant that does not make any sense at the CFG level).

As an example, Silicon currently frames permission around while loops that are not real loops. In my opinion, this is incorrect (since it's not in-sync with the CFG). See:

field next: Ref

method test10() {
    var b: Bool := true
    var x: Ref
    inhale acc(x.next)
    while (b)
        invariant acc(x.next, 1/2)
    {
        /* succeeds in Silicon: half permission is framed around even though
         * the syntactic while loop is not a real loop
         */
        assert perm(x.next) == 1/2        
        goto end
        b := false
    }

  label end
}