dafny icon indicating copy to clipboard operation
dafny copied to clipboard

Enable compiling Dafny programs with deeply nested code

Open keyboardDrummer opened this issue 3 years ago • 1 comments

Programs with deeply nested Dafny code will crash the Dafny compiler. Here's an example:

method Main() {
    var c := 1;
    print(c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
+ c + c + c + c + c + c + c
          ), "\n";
}

One way of solving this issue is by no longer letting Dafny traverse the program AST using recursive calls on the call stack, which it does in many parts of its pipeline such as resolution, verification and code generation. PR #2124 uses a trick to use async/await to do recursive calls on a dynamic stack. With that trick Dafny could avoid doing recursive calls on the call stack but it requires moving the relevant code to use async/await, which is a lot of work.

keyboardDrummer avatar May 10 '22 13:05 keyboardDrummer