Enable compiling Dafny programs with deeply nested code

[keyboardDrummer]

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.

[sorawee]

See also: https://github.com/dafny-lang/dafny/issues/1331