No flatten for most backends #5528

keyboardDrummer · 2024-06-05T09:19:17Z

Description

Do not flatten matches for most backends. Such flattening can cause the generated code size to be the square of the input code size. Removing the flattening leads to a huge decrease in the size of the generated C# code inside the Dafny codebase. It goes from ~14K lines to ~7K.

The compilation of nested matches is done as follows:

datatype TX = X(x1arg: TY, x2arg: TY)
datatype TY = Y(yarg: int)
datatype TZ = Z(zarg: TW)
datatype TW = W(warg: int)

method M(a: TX) {
  match a
    case X(Y(b),Z(W(c)) => <body1>
    case r => <body2>
}

Is roughly compiled into

// Same datatypes

method M(a: TX) {
  var unmatched := true;
  if (unmatched && a is X) {
    var x1arg1 = ((X)a).1;
    if (x1 is Y) {
      var b = ((Y)x1arg1).1;
      var x2arg2 := ((X)a).2; 
      if (x2 is Z) {
        var zarg1 := ((Z)x2arg2).1;
        if (x4 is W) {
          var c := ((W)zarg1).1;
          unmatched := false;
          <body1>
        }
      } 
    }
  }
  if (unmatched) {
    var r := a;
    <body2>
  }
}

Caveats

Maintainability

To reduce the required work, Java and Dafny back-ends still compile using flattened matches

Ideally the transformation would be a Dafny-to-Dafny source transformation, instead of a customization of SinglePassCompiler. However, Dafny does not allow using statements in expression contexts, and this is needed for the transformation. I think it would be good to have an intermediate Dafny that does allow this, similar to what @cpitclaudel 's Dafny-in-Dafny compiler allowed, and then to define the rewrite that this PR introduces using a Dafny source translation.

Improvement

For C# we could generate much nicer code, since C# allows declaring new variables inside expressions using x is T xAsType expressions. We could get rid of the nested if statements and the unmatched variable. However, I'll leave this for future work.

How has this been tested?

Performance change. No additional tests added.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

… match expressions in an expression context

This reverts commit 846ad62.

… into noFlattenForCSharp

robin-aws · 2024-06-05T15:37:46Z

Just for my own understanding, why did the original code generation lead to only a quadratic increase in code size? I would think that it would be a factor of the number of other data constructors, and be worse than quadratic for more nested matches, i.e. if the example above had lots of data constructors for each datatype, I'd expect the worst case to be something like O(|TX| * |TZ| * |TW|)

keyboardDrummer · 2024-06-05T15:43:39Z

Just for my own understanding, why did the original code generation lead to only a quadratic increase in code size? I would think that it would be a factor of the number of other data constructors, and be worse than quadratic for more nested matches, i.e. if the example above had lots of data constructors for each datatype, I'd expect the worst case to be something like O(|TX| * |TZ| * |TW|)

I guess if your nested match occurs in a case that gets copied, like a default case, then it could be exponential yes.

But if your nested match occurs in a case that does not get copied, then the nesting has no particular effect.

However, regardless of nesting, for each match in the original program, the amount of flattened cases will be the number of constructors of the datatype, so the size will be #matches * #ofConstructors for a program where all matches match on the same datatype and all constructor are part of that datatype. The C# code that was generated for our Rust back-end was large simply because of this, not because of nested matches.

keyboardDrummer · 2024-06-05T15:59:17Z

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs

@@ -12,562 +19,658 @@
 namespace Microsoft.Dafny.Compilers {
 public abstract partial class SinglePassCodeGenerator {

- public virtual void EmitExpr(Expression expr, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {


Applied a resharper refactoring to turn the if's into a switch statement. No actual changes to this method except for NestedMatchExpr, which now calls into a method.

keyboardDrummer · 2024-06-05T16:01:25Z

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs

@@ -11,8 +18,6 @@

 namespace Microsoft.Dafny.Compilers {
 public abstract partial class SinglePassCodeGenerator {
-
-
 protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts = null) {


Applied a resharper refactoring to turn the if's into a switch statement. No actual changes to this method except for NestedMatchStmt, which now calls into a method.

keyboardDrummer · 2024-06-05T16:01:54Z

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs

@@ -460,5 +509,162 @@ public abstract partial class SinglePassCodeGenerator {
 }
 }
 }
+
+ protected virtual void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {


This is where the changes in this file start.

keyboardDrummer · 2024-06-05T16:02:08Z

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs

 // We end with applying the source expression to the delegate we just built
 EmitExpr(e.Source, inLetExprBody, wArg, wStmts);
 }
+
+ protected virtual void EmitNestedMatchExpr(NestedMatchExpr match, bool inLetExprBody, ConcreteSyntaxTree output, ConcreteSyntaxTree wStmts) {


This is where the changes in this file start.

MikaelMayer

This looks good to me.

MikaelMayer · 2024-06-05T14:28:22Z

.github/workflows/msbuild.yml

@@ -67,7 +67,7 @@ jobs:

 integration-tests:
 needs: check-deep-tests
- if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
+ if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests') || contains(github.event.pull_request.labels.*.name, 'run-integration-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))


Go ahead there is no copyright on that one :-)

MikaelMayer · 2024-06-05T14:31:02Z

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -2668,5 +2669,18 @@ private class ExprLvalue : ILvalue {
 AddUnsupported("<i>EmitHaltRecoveryStmt</i>");
 }

+ protected override void EmitNestedMatchExpr(NestedMatchExpr match, bool inLetExprBody, ConcreteSyntaxTree output,
+ ConcreteSyntaxTree wStmts) {
+ EmitExpr(match.Flattened, inLetExprBody, output, wStmts);


That's the right way, thanks. I'll see later how we can actually replace that.

MikaelMayer · 2024-06-05T14:33:58Z

Source/DafnyCore/Backends/Rust/RustBackend.cs

@@ -82,8 +82,8 @@ public class RustBackend : DafnyExecutableBackend {
 stream.CopyTo(outFile);
 });

- using (var cargoToml = new FileStream(Path.Combine(targetDirectory, "Cargo.toml"), FileMode.Create, FileAccess.Write)) {
- using var cargoTomlWriter = new StreamWriter(cargoToml);
+ await using (var cargoToml = new FileStream(Path.Combine(targetDirectory, "Cargo.toml"), FileMode.Create, FileAccess.Write)) {


NIce optimization.

keyboardDrummer added 30 commits May 29, 2024 14:43

Add patterns/codeSize test

97d81e2

Update codeSize test

e77441a

Split off statement part from SPCG

547317f

Draft of nested match compiler

55b4cde

Save

b4bc5cf

Generated code looks good upon visual inspection

f10aa78

Generated code compiles and runs

ee9ae6f

Move NestedMatch generation to just C#

069dddb

Attempt at implementation for expressions

da513a0

Ran formatter

88536c8

Fixes

f13be6e

Update C# code generator zo it also uses custom generation for nested…

a61d607

… match expressions in an expression context

Regen GeneratedFromDafny code

846ad62

Revert "Regen GeneratedFromDafny code"

85c1b20

This reverts commit 846ad62.

Fix gen

3660a37

Fixes for generics

26000a5

Update generated files

2805584

Merge branch 'master' into noFlattenForCSharp

09f39f8

Fix bug related to disjoint patterns

82a5d71

Merge branch 'noFlattenForCSharp' of github.com:keyboardDrummer/dafny…

c32be6f

… into noFlattenForCSharp

Merge remote-tracking branch 'origin/master' into noFlattenForCSharp

861cee7

Fix literal pattern bug

1e25d7b

Remove DatatypeWrapperEraser.IsErasableDatatypeWrapper check

6791e43

Ran formatter

eedcf47

Fix bug in disjunctive assignments

6f981ab

Merge branch 'master' into noFlattenForCSharp

0bd8c0d

Trigger CI

903f2bf

Merge branch 'noFlattenForCSharp' of github.com:keyboardDrummer/dafny…

5d9dc07

… into noFlattenForCSharp

Fixes

9477c6f

Refactoring

b919fa8

keyboardDrummer added 14 commits June 3, 2024 19:28

Add force integration tests code

c6de95b

Merge branch 'master' into noFlattenForCSharp

0672492

Convert if else chains to switch

3c86dd7

Merge commit 'a748799eef1d7~1' into noFlattenForCSharp

e45420a

Merge commit 'a748799eef1d7' into noFlattenForCSharp

b8de307

Merge remote-tracking branch 'origin/master' into noFlattenForCSharp

f97bf09

Ran formatter

75bb47e

Refactoring

e1bb707

Further refactoring

dbcb4a4

Further refactoring

420a13b

Attempt at using nested matches for all backends

5f860c9

Use flattened matches for DafnyCodeGenerator

808d090

Reintroduce flattening for Java

126344a

Fixes

a1011f7

keyboardDrummer changed the title ~~No flatten for all backends~~ No flatten for most backends Jun 5, 2024

Remove codeSize test

387b35f

keyboardDrummer marked this pull request as ready for review June 5, 2024 11:19

keyboardDrummer enabled auto-merge (squash) June 5, 2024 11:19

keyboardDrummer requested a review from MikaelMayer June 5, 2024 11:19

Update expect files

49e0c55

keyboardDrummer mentioned this pull request Jun 5, 2024

Do not flatten matches for C# #5509

Closed

keyboardDrummer commented Jun 5, 2024

View reviewed changes

MikaelMayer approved these changes Jun 5, 2024

View reviewed changes

keyboardDrummer merged commit 5b048ff into dafny-lang:master Jun 5, 2024
21 checks passed

keyboardDrummer deleted the noFlattenForAllBackends branch June 5, 2024 22:32

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

No flatten for most backends #5528

No flatten for most backends #5528

keyboardDrummer commented Jun 5, 2024 •

edited

Loading

robin-aws commented Jun 5, 2024

keyboardDrummer commented Jun 5, 2024 •

edited

Loading

keyboardDrummer Jun 5, 2024 •

edited

Loading

keyboardDrummer Jun 5, 2024

keyboardDrummer Jun 5, 2024

keyboardDrummer Jun 5, 2024

MikaelMayer left a comment

MikaelMayer Jun 5, 2024

MikaelMayer Jun 5, 2024

MikaelMayer Jun 5, 2024

No flatten for most backends #5528

No flatten for most backends #5528

Conversation

keyboardDrummer commented Jun 5, 2024 • edited Loading

Description

Caveats

Maintainability

Improvement

How has this been tested?

robin-aws commented Jun 5, 2024

keyboardDrummer commented Jun 5, 2024 • edited Loading

keyboardDrummer Jun 5, 2024 • edited Loading

Choose a reason for hiding this comment

keyboardDrummer Jun 5, 2024

Choose a reason for hiding this comment

keyboardDrummer Jun 5, 2024

Choose a reason for hiding this comment

keyboardDrummer Jun 5, 2024

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

MikaelMayer Jun 5, 2024

Choose a reason for hiding this comment

MikaelMayer Jun 5, 2024

Choose a reason for hiding this comment

MikaelMayer Jun 5, 2024

Choose a reason for hiding this comment

keyboardDrummer commented Jun 5, 2024 •

edited

Loading

keyboardDrummer commented Jun 5, 2024 •

edited

Loading

keyboardDrummer Jun 5, 2024 •

edited

Loading