Bad interaction between tail recursion optimization and lambdas in Java

[cpitclaudel]

The following code compiles to invalid Java code:

datatype T = T() {
  function method Const(): bool { true }
  function method TailRecursive(n: nat): bool {
    if n == 0 then (() => Const())()
    else TailRecursive(n - 1)
  }
}

Dafny -noVerify -compile:4 -compileTarget:java this_bug_java.dfy

Dafny program verifier did not attempt verification
Wrote textual form of target program to this_bug_java-java/this_bug_java.java
Additional target code written to this_bug_java-java/_System/nat.java
Additional target code written to this_bug_java-java/_System/T.java
Additional target code written to this_bug_java-java/dafny/Tuple0.java
Additional target code written to this_bug_java-java/dafny/Function0.java
Picked up JAVA_TOOL_OPTIONS: -Dlog4j2.formatMsgNoLookups=true
this_bug_java-java\_System\T.java:58: error: local variables referenced from a lambda expression must be final or effectively final
          return (_this).Const();
                  ^
1 error
Error while compiling Java files. Process exited with exit code 1

The faulty Java code:

  public boolean TailRecursive(java.math.BigInteger n) {
    T _this = this;
    TAIL_CALL_START: while (true) {
      if ((n).signum() == 0) {
        return (((dafny.Function0<Boolean>)() -> {
          return (_this).Const();
        })).apply();
      } else {
        T _in0 = _this;
        java.math.BigInteger _in1 = (n).subtract((java.math.BigInteger.ONE));
        _this = _in0;
        n = _in1;
        continue TAIL_CALL_START;
      }
    }
  }

While waiting for a fix, affected users can add {:tailrecursion false} in function method {:tailrecursion false} TailRecursive

[cpitclaudel]

Other failing test that uses this:

datatype T = Last(x: bool) | NotLast(next: T) {
  function method FindLast(): bool {
    if this.Last? then (() => x)()
    else this.next.FindLast()
  }
}

[MikaelMayer]

The solution would be to copy the value of _this to a local final variable, e.g. https://stackoverflow.com/a/27593059/1287856