Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Nested LetExpr chain compiles to tons of nested Java lambdas, which javac chokes on #3868

Closed
robin-aws opened this issue Apr 13, 2023 · 3 comments · Fixed by #4683 or #5589
Closed

Nested LetExpr chain compiles to tons of nested Java lambdas, which javac chokes on #3868

robin-aws opened this issue Apr 13, 2023 · 3 comments · Fixed by #4683 or #5589
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime

Comments

@robin-aws
Copy link
Member

Dafny version

4.0.0

Code to produce this issue

include "Wrappers.dfy"

module Test {

  import opened Wrappers

  datatype Or = A | B

  function WoahThatsDeep(o: Or, x: string): Option<string> {
    var r :- match o {
      case A =>
        var x1 := x;
        var x2 := x1;
        var x3 := x2;
        var x4 := x3;
        var x5 := x4;
        var x6 := x5;
        var x7 := x6;
        var x8 := x7;
        var x9 := x8;
        var x10 := x9;
        Some(x10)
      case B =>
        Some("hello")
    };
    Some(r)
  }

  method Main() {
    print WoahThatsDeep(A, "42"), "\n";
  }
}

Command to run and resulting output

dafny run -t:java Scratch.dfy

Takes a very long time to compile the resulting Java code, and uses multiple GB of RAM in the process. This example is simplified from a larger example that causes `javac` to run out of memory.

What happened?

The translated java code looks like this:

// Class __default
// Dafny class __default compiled into Java
package Test_Compile;

import Wrappers_Compile.*;

@SuppressWarnings({"unchecked", "deprecation"})
public class __default {
  public __default() {
  }
  public static Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>> WoahThatsDeep(Or o, dafny.DafnySequence<? extends Character> x)
  {
    Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>> _18_valueOrError0 = ((java.util.function.Function<Or, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>)(_source6_boxed0) -> {
      Or _source6 = ((Or)(java.lang.Object)(_source6_boxed0));
      if (_source6.is_A()) {
        return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(x, boxed0 -> {
          dafny.DafnySequence<? extends Character> _pat_let0_0 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed0));
          return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_pat_let0_0, boxed1 -> {
            dafny.DafnySequence<? extends Character> _19_x1 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed1));
            return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_19_x1, boxed2 -> {
              dafny.DafnySequence<? extends Character> _pat_let1_0 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed2));
              return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_pat_let1_0, boxed3 -> {
                dafny.DafnySequence<? extends Character> _20_x2 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed3));
                return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_20_x2, boxed4 -> {
                  dafny.DafnySequence<? extends Character> _pat_let2_0 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed4));
                  return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_pat_let2_0, boxed5 -> {
                    dafny.DafnySequence<? extends Character> _21_x3 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed5));
                    return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_21_x3, boxed6 -> {
                      dafny.DafnySequence<? extends Character> _pat_let3_0 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed6));
                      return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_pat_let3_0, boxed7 -> {
                        dafny.DafnySequence<? extends Character> _22_x4 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed7));
                        return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_22_x4, boxed8 -> {
                          dafny.DafnySequence<? extends Character> _pat_let4_0 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed8));
                          return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_pat_let4_0, boxed9 -> {
                            dafny.DafnySequence<? extends Character> _23_x5 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed9));
                            return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_23_x5, boxed10 -> {
                              dafny.DafnySequence<? extends Character> _pat_let5_0 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed10));
                              return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_pat_let5_0, boxed11 -> {
                                dafny.DafnySequence<? extends Character> _24_x6 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed11));
                                return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_24_x6, boxed12 -> {
                                  dafny.DafnySequence<? extends Character> _pat_let6_0 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed12));
                                  return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_pat_let6_0, boxed13 -> {
                                    dafny.DafnySequence<? extends Character> _25_x7 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed13));
                                    return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_25_x7, boxed14 -> {
                                      dafny.DafnySequence<? extends Character> _pat_let7_0 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed14));
                                      return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_pat_let7_0, boxed15 -> {
                                        dafny.DafnySequence<? extends Character> _26_x8 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed15));
                                        return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_26_x8, boxed16 -> {
                                          dafny.DafnySequence<? extends Character> _pat_let8_0 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed16));
                                          return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_pat_let8_0, boxed17 -> {
                                            dafny.DafnySequence<? extends Character> _27_x9 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed17));
                                            return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_27_x9, boxed18 -> {
                                              dafny.DafnySequence<? extends Character> _pat_let9_0 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed18));
                                              return ((Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>)(java.lang.Object)(dafny.Helpers.<dafny.DafnySequence<? extends Character>, Wrappers_Compile.Option<dafny.DafnySequence<? extends Character>>>Let(_pat_let9_0, boxed19 -> {
                                                dafny.DafnySequence<? extends Character> _28_x10 = ((dafny.DafnySequence<? extends Character>)(java.lang.Object)(boxed19));
                                                return Wrappers_Compile.Option.<dafny.DafnySequence<? extends Character>>create_Some(_28_x10);
                                              }
                                              )));
                                            }
                                            )));
                                          }
                                          )));
                                        }
                                        )));
                                      }
                                      )));
                                    }
                                    )));
                                  }
                                  )));
                                }
                                )));
                              }
                              )));
                            }
                            )));
                          }
                          )));
                        }
                        )));
                      }
                      )));
                    }
                    )));
                  }
                  )));
                }
                )));
              }
              )));
            }
            )));
          }
          )));
        }
        )));
      } else {
        return Wrappers_Compile.Option.<dafny.DafnySequence<? extends Character>>create_Some(dafny.DafnySequence.asString("hello"));
      }
    }).apply(o);
    if ((_18_valueOrError0).IsFailure(dafny.DafnySequence.<Character>_typeDescriptor(dafny.TypeDescriptor.CHAR))) {
      return (_18_valueOrError0).<dafny.DafnySequence<? extends Character>>PropagateFailure(dafny.DafnySequence.<Character>_typeDescriptor(dafny.TypeDescriptor.CHAR), dafny.DafnySequence.<Character>_typeDescriptor(dafny.TypeDescriptor.CHAR));
    } else {
      dafny.DafnySequence<? extends Character> _29_r = (_18_valueOrError0).Extract(dafny.DafnySequence.<Character>_typeDescriptor(dafny.TypeDescriptor.CHAR));
      return Wrappers_Compile.Option.<dafny.DafnySequence<? extends Character>>create_Some(_29_r);
    }
  }
  public static <__T> Wrappers_Compile.Option<__T> Maybe(dafny.TypeDescriptor<__T> _td___T, __T t)
  {
    return Wrappers_Compile.Option.<__T>create_Some(t);
  }
  public static void Main(dafny.DafnySequence<? extends dafny.DafnySequence<? extends Character>> __noArgsParameter)
  {
    System.out.print(java.lang.String.valueOf(__default.WoahThatsDeep(Test_Compile.Or.create_A(), dafny.DafnySequence.asString("42"))));
    System.out.print((dafny.DafnySequence.asString("\n")).verbatimString());
  }
  public static void __Main(dafny.DafnySequence<? extends dafny.DafnySequence<? extends Character>> args) {
    __default.Main(args);
  }
  private static final dafny.TypeDescriptor<__default> _TYPE = dafny.TypeDescriptor.referenceWithInitializer(__default.class, () -> (__default) null);
  public static dafny.TypeDescriptor<__default> _typeDescriptor() {
    return (dafny.TypeDescriptor<__default>) (dafny.TypeDescriptor<?>) _TYPE;
  }
  @Override
  public java.lang.String toString() {
    return "Test_Compile._default";
  }
}

Normally a chain of let expressions (i.e. var x1 := x; var x2 := x1; ...) is optimized to compile to a sequence of regular variable declarations in Java, but because this one is inside a match expression rather than at the top level, the optimization isn't currently applied.

What type of operating system are you experiencing the problem on?

Mac
@robin-aws robin-aws added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Apr 13, 2023
@robin-aws
Copy link
Member Author

robin-aws commented Apr 13, 2023 •
edited
Loading

More details: the optimization is only valid when a let expression is used in a context that can emit multiple sequential statements, such as the top-level body of a function. This is why SinglePassCompiler.TrExprOpt (which optimizes in this way) will call TrCasePatternOpt, which will call TrExpr (which doesn't/can't optimize in this way in general).

(Edit: to clarify, I'm referring to multiple sequential target-language statements, so it's likely that SinglePassCompiler is being conservative here and could be more aggressive by default since most target languages support this, even though some would need to opt out such as Python)

The general solution to this is probably to introduce synthetic methods to compute subexpressions, so that the optimization can be applied more consistently. This is also the best way to work around it in source code, ensuring that chained let expressions only appear at the top level (and perhaps we can lint for this in the short term).

@robin-aws robin-aws mentioned this issue Apr 13, 2023
Merged
@alex-chew alex-chew mentioned this issue Apr 13, 2023
Closed
@robin-aws robin-aws added the lang: java Dafny's Java transpiler and its runtime label Apr 17, 2023
@seebees
Copy link

seebees commented Oct 16, 2023

This will also happen for a datatype that has a lot of constructors.
So in your example above we could change it and get the same thing:

include "Wrappers.dfy"

module Test {

  import opened Wrappers

  datatype Or = 
    | A(x1: string, x2: string, x3: string, x4: string, x5: string, x6: string, x7: string, x8: string, x9: string, x10: string)
    | B

  function WoahThatsDeep(o: Or, x: string): Option<string> {
    var r :- match o {
      case A(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) =>
        Some(x10)
      case B =>
        Some("hello")
    };
    Some(r)
  }

  method Main() {
    print WoahThatsDeep(A, "42"), "\n";
  }
}

@RustanLeino RustanLeino mentioned this issue Oct 19, 2023
Merged
RustanLeino added a commit that referenced this issue Nov 1, 2023
@RustanLeino
Emit less nested target code (#4683)
451a9a5 
Emit better target code for match-case expressions. In particular, avoid some deeply nested IIFE's that (were hard for a human to read and) caused the Java compiler to choke.

Fixes #3868 

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
@robin-aws
Copy link
Member Author

Re-opening since it's certainly still possible to hit this, even if the linked PR improved things a lot.

@robin-aws robin-aws reopened this Jun 25, 2024
@robin-aws robin-aws mentioned this issue Jun 28, 2024
Draft
4 tasks
@RustanLeino RustanLeino mentioned this issue Jun 29, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime
Projects
None yet
Milestone
No milestone
2 participants
@seebees @robin-aws