Abstract interpretation ignores where clauses

[RustanLeino]

Consider the following two procedures, where the only difference is that P states 0 <= N in a requires clause whereas Q states the same condition in a where clause.

procedure P(N: int)
  requires 0 <= N;
{
  var x: int;
  var y: int;

  x := 0;
  y := N;

  while (x < 100) {
    x := x + 1;
    y := y + 1;
  }
}

procedure Q(N: int where 0 <= N)
{
  var x: int;
  var y: int;

  x := 0;
  y := N;

  while (x < 100) {
    x := x + 1;
    y := y + 1;
  }
}

One would expect the two procedures to obtain the same inferred loop invariants, but they don't:

> boogie test.bpl /infer:j /printInstrumented | grep ":inferred"
    assume {:inferred} 0 <= x && x < 101 && 0 <= y;
    assume {:inferred} 0 <= x && x < 101;

Evidently, the where clause on the parameter is not treated in the same way as the requires clause, but I argue they should be.

In fact, according to Boogie's semantics (see This is Boogie 2), where clauses get assumed anywhere the variable is given an arbitrary value. (They are never checked, but that's the intended semantics of where.) In other words, where clauses are

• assumed (for global variables, in-parameters, and local variables) at the start of an implementation body,
• assumed (for the variables listed) after a havoc statement,
• assumed (for loop targets) in the loop head of loops, and
• assume (for out-parameters as well as global variables modified by a call) on return from a call.

So, abstract interpretation ought to pick up on these assumption in all of these places. (It's possible that this is more difficult to implement for loops, since it requires knowing what the loop heads and loop targets are, which perhaps is calculated later in Boogie. But taking where clauses into account on entry to an implementation, after a havoc statement, and on return from a call should be done.)