-
Notifications
You must be signed in to change notification settings - Fork 260
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.
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
No flatten for most backends #5528
No flatten for most backends #5528
Conversation
… match expressions in an expression context
This reverts commit 846ad62.
… into noFlattenForCSharp
… into noFlattenForCSharp
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 |
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 |
@@ -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) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
@@ -11,8 +18,6 @@ | |||
|
|||
namespace Microsoft.Dafny.Compilers { | |||
public abstract partial class SinglePassCodeGenerator { | |||
|
|||
|
|||
protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts = null) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
@@ -460,5 +509,162 @@ public abstract partial class SinglePassCodeGenerator { | |||
} | |||
} | |||
} | |||
|
|||
protected virtual void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is where the changes in this file start.
// 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) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is where the changes in this file start.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks good to me.
@@ -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' ))) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Go ahead there is no copyright on that one :-)
@@ -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); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That's the right way, thanks. I'll see later how we can actually replace that.
@@ -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)) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
NIce optimization.
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:
Is roughly compiled into
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 nestedif
statements and theunmatched
variable. However, I'll leave this for future work.How has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.