Too much assumed about temporary or unassigned variables

[RustanLeino]

The following program verifies and compiles, but crashes at run time:

predicate method {:opaque} P<W>(w: W) {
  true
}

method M<W>(s: seq<W>) returns (ghost r: W)
{
  var b := exists w: W :: P(w);
  ghost var w: W :| b ==> P(w); // BOGUS: this should be flagged as an error, because the type W may be empty
  if s != [] {
    var cand: W := GimmieOne(s);
  }
  return w;
}

method GimmieOne<W>(s: seq<W>) returns (c: W)
  requires s != []
{
  return s[0];
}

type Empty = x: int | false witness *

method Main() {
  var w := M<Empty>([]); // it's impossible for w to have a value, so the verifier (correctly) assumes false here
  var x := 3 / 0;
}

$ dafny /compile:3 test.dfy

Dafny program verifier finished with 3 verified, 0 errors
Running...

Error: Execution resulted in exception: Exception has been thrown by the target of an invocation.
System.DivideByZeroException: Attempted to divide by zero.
   at System.Numerics.BigInteger.op_Division(BigInteger dividend, BigInteger divisor)
   at System.Numerics.BigInteger.Divide(BigInteger dividend, BigInteger divisor)
   at Dafny.Helpers.EuclideanDivision(BigInteger a, BigInteger b)
   at _module.__default._Main()
   at Dafny.Helpers.WithHaltHandling(Action action)
   at __CallToMain.Main(String[] args)

Diagnosis

The problem has to do with where-clause assumptions that are generated for variables. Here's some context.

The verifier translates a local variable x of a type X into a similar local variable in Boogie. If BX is the Boogie type that includes all Dafny-X values, then the Boogie declaration looks something like this:

var x: BX;

The Boogie type BX may be bigger than the Dafny type X, so the verifier adds the more precise information using assumptions. Boogie's where clauses give a convenient place to hang such an assumption. So, in the typical case, the Boogie declaration of x looks something like:

var x: BX where $Is(x, X);

This is fine as long as long as X denotes a nonempty type.

If X denotes a possibly empty type, then Dafny puts into effect a definite-assignment rule. This rule, which is enforced by the verifier, checks that any use of the variable x is preceded by an assignment to x. For the sake of soundness, the verifier must arrange that $Is(x, X) does not get assumed until after x has been assigned. This is done by emitting a second Boogie variable, named defass$x. This variable is set to true when x is assigned. So, in the case that X denotes a possibly empty type, the declarations generated are:

var defass$x: bool;
var x: BX where defass$x ==> $Is(x, X);

So far, all good. The Dafny verifier incorporates this design. But there are two places where an incorrect where clause is generated.

One place is for temporary variables. In particular, for a Dafny call x := MyMethod();, the verifier generates

rhs$0 := MyMethod();
x := rhs$0;
defass$x := true;  // (this line is included only if X is a possibly empty type)

and for a simultaneous assignment x, y := E, F;, the verifier generates

rhs$0 := E;
rhs$1 := F;
x := rhs$0;
y := rhs$0;
defass$x := true;  // (this line is included only if X is a possibly empty type)
defass$y := true;  // (this line is included only if the type of y is a possibly empty type)

The problem is that the temporary variable rhs$0 (and similar for rhs$1) is currently declared with a where clause:

var rhs$0: BX where $Is(rhs$0, X)`;

A temporary variable does not need a where clause. (And even if it did have one, it would need to replicate the definite-assignment mechanism. But it doesn't need a where clause at all.) So, this is one problem that should be fixed.

The other place where an incorrect where clause is generated is when the Dafny program declares and immediately assigns a variable, like var x := E;. In this case, every Dafny use of the variable x will be after x has been assigned, so there seems to be no reason to bring in the defass$x mechanism. Wrong! While the Dafny part of the argument I made is correct, the Boogie where clause will be available even before the Dafny initialization x := E; has happened. The verifier gets this wrong. It should apply this optimization only for nonempty types.

PS. If the Dafny statement var cand: W := GimmieOne(s); in the program above is broken up into a declaration var cand: W; and an assignment cand := GimmieOne(s);, then one runs into a bug in the compiler. That bug has already been reported in #1553.