Malformed Java target code for unreachable code

[RustanLeino]

The following code is legal in Dafny:

method Main() {
  print "hello\n";
  label L: {
    print "inside block\n";
    break L;
    print "never get here\n";
  }
  print "one\n";
}

It compiles to more-or-less the same code in Java. However, the Java compiler produces an error about the unreachable statement (the one after the break), which causes the Dafny compiler to crash.

Repro:

$ dafny /compile:3 test.dfy /spillTargetCode:1 /compileTarget:java
Dafny 2.3.0.10506

Dafny program verifier finished with 0 verified, 0 errors
Compiled program written to test/test.java
Additional code written to test/_System/nat.java
Additional code written to test/_System/__default.java
/Users/leino/Documents/dafny/test/_System/__default.java:19: error: unreachable statement
            System.out.print(dafny.DafnySequence.asString("never get here\n").verbatimString());
            ^
1 error
[ERROR] FATAL UNHANDLED EXCEPTION: System.Exception: Error while compiling Java files. Process exited with exit code 1
  at Microsoft.Dafny.JavaCompiler.CompileTargetProgram (System.String dafnyProgramName, System.String targetProgramText, System.String callToMain, System.String targetFilename, System.Collections.ObjectModel.ReadOnlyCollection`1[T] otherFileNames, System.Boolean hasMain, System.Boolean runAfterCompile, System.IO.TextWriter outputWriter, System.Object& compilationResult) [0x001d3] in <697ffa4f1bf04fb289586c266c8e6dec>:0
...

[davidcok]

Rustan, Does the Dafny compiler infrastructure have any cross-language reachability analysis to apply here? As the compiler does not produce a Java AST, but just the textual output through the TargetWriters, it seems the analysis must be performed on the Dafny AST.

[davidcok]

Note that it is the JVM that forbids unreachable code, not the Java compiler itself. So we will have to hack something into the compiler to catch the cases of unreachableness that Java does, or else just tell the Java users - don't do that.