match-optimization removes expressions before they are verified

[RustanLeino]

Early in its pipeline, Dafny rewrites match expressions and match statements into more primitive match constructs. The rewrite also does some optimizations, one of which has the effect of changing

match E
case _ => S

to just S. This is a legal transformation for verified code, since expressions (here, E) have no side effects. The problem is that the transformation is done before the program is verified, and in particular before E has been checked to be well-formed. Or, to point fingers elsewhere, the verifier is currently verifying the rewritten program whereas it should be verifying the original program.

I believe the original expression E is available in Dafny's internal AST, so the fix would be that the verifier should reach for it to check that E is well-formed. Note, if issue https://github.com/dafny-lang/dafny/issues/1715 is dealt with, then that may cause some changes in the process of rewriting match constructs, in which case the solution to the current issue may also be affected.

Test cases

datatype R = R(int)

method M(x: int) {
  match R(x / 0) // BOGUS: the verifier should report an error here
  case _ => print "hello\n";
}

function method F(x: int): int {
  match R(x / 0) // BOGUS: the verifier should report an error here
  case _ => 3
}

method Main() {
  M(10);
  print F(10), "\n";
}

Because of the issue, the two errors in this program are not reported, but they should be.

[cpitclaudel]

What's particularly interesting is that this does not lead to a soundness issue, right? It could even be debatable whether there's anything broken here to fix, since Dafny expressions are pure.

This reminds me of a famous "bug" in Coq's termination checker, which lets you write this:

Fixpoint f (n: nat) : nat :=
  let _ := f n in
  2.

Regardless it's probably better to fix this, if only to reduce surprises.

[robin-aws]

I'd call it a bug personally: yes Dafny expressions are pure, but they are not lazily evaluated. The runtime semantics of something like match R(x / 0) case _ => ... should be "evaluate the match expression and then select the matching case branch and...". That means the correct runtime behavior should be a crash, but this optimization changes that into a successful calculation.

I do agree it's not a soundness bug since it turns an invalid program that should crash into one that doesn't.

[cpitclaudel]

It's debatable whether match R(x / 0) case _ => ... has runtime semantics at all, because it's an invalid program. Do we really want to give semantics to invalid programs?