Unexpected behavior with WhereClause and Assignment in while loops

[hmc-cs-dzhang]

Why can I assert false in the following code?

procedure bar() {
  var x: int where x == 5;
  while (x == 5) {
      x := x + 1;
  }
  assert false; // Verifies
} 

On the other hand, when you use a where clause and assignment outside of a while loop, the following does not verify (as expected):

procedure foo() {
  var x: int where x == 5;
  x := x + 1;
  assert false;  // Can't assert false here; x is 6 and everything is fine
}

According to This Is Boogie 2, the above while loop translates to

procedure bar2() {
  var x: int where x == 5;
  goto Head;

Head:
    goto Body, GuardedDone;
Body:
    assume x == 5;
    x := x + 1;
    goto Head;
GuardedDone:
    assume x != 5; goto Done;
Done:
    assert false;  // still allowed to assert false.
}

and we're still allowed to assert false. Naively, it seems like the line assume x != 5 combined with the where clause allows boogie to assert false. However, there is a path from Head to Body to Head to GuardedDone where we assign to x, which allows us to ignore the where clause. Also, if we change the line goto Head; under the Body label to goto GuardedDone; then we are no longer able to assert false.

As a beginner, this result feels very counterintuitive -- I don't see any obvious unsoundness in bar or bar2. Can someone provide a bit of intuition about what's going on?

Thanks, Daniel

[RustanLeino]

This is working as designed. The where clause is used by Boogie anytime that Boogie has the occasion to give an arbitrary value to a variable. This happens on entry to a procedure, on return from calls, in loop heads, and in havoc statements. By writing where x == 5, you are basically stating the assumption that x will always be 5, and under such an assumption, there is no feasible code path after the loop, because the loop will terminate only if x is not 5 and your where assumption says x will always be 5.

where clauses are an advanced feature in Boogie. It's a feature you'll want to use if you're writing a verifier for a source language that guarantees certain invariants, like type invariants. For example, suppose the source language that you're translating into Boogie is a safe language with dynamic object allocation. You may then want to give Boogie the information that all variables of a reference type point to some allocated object (in other words, you're encoding the knowledge that there are no dangling references in the source language). You would do this using a where clause, perhaps like this:

var x: ref where x == null || isAllocated(x);

This is appropriate, because the source language offers no way to obtain a reference to a non-allocated object, and verification will need this assumption.

If Boogie had no where clauses, you could simulate them yourself in many places by adding explicit assume statements. However, it's awkward to do this well for loops, where Boogie is the one that cuts the loop and, in effect, introduces in the loop head a havoc statement for every loop target. Since where clauses apply in those places, you don't have to figure out yourself which variables are loop targets---instead, if Boogie determines that a variable is a loop target, it will also apply the where condition for you.

To see how this applies to your loop above, let's manually apply the loop-cutting that Boogie performs. (If you want to see more details of this for a particular example, use Boogie's /traceverify switch.) Boogie will determine that Head is a loop head for the loop that also includes block Body. The loop targets (that is, the variables syntactically assigned to) of these two blocks is x. Thus, Boogie breaks up the loop in bar2 as follows:

procedure bar2() {
  var x: int where x == 5;
  goto Head;

Head:
    havoc x;  // set loop targets to arbitrary values
    goto Body, GuardedDone;
Body:
    assume x == 5;
    x := x + 1;
    assume false;  // the back-edge "goto Head" is replaced by "assume false" by the transformation

GuardedDone:
    assume x != 5; goto Done;
Done:
    assert false;  // still allowed to assert false.
}

Because you declared x with a where clause, the havoc x in the loop head is in effect

havoc x; assume x == 5;

Now, I hope you'll see that there is no feasible code path from Head to GuardedDone.

Rustan