Fix: Labels are no longer compiled in the case of variable declarations #2973
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
robin-aws
reviewed
Nov 2, 2022
| @@ -4331,7 +4331,9 @@ private class GetterSetterLvalueImpl : ILvalue { | |||
| // <prelude> // filled via copyInstrWriters -- copies out-parameters used in letexpr to local variables | |||
| // ss // translation of ss has side effect of filling the top copyInstrWriters | |||
| var w = writer; | |||
| if (ss.Labels != null) { | |||
| if (ss.Labels != null && !(ss is VarDeclPattern or VarDeclStmt)) { | |||
There was a problem hiding this comment.
Definitely sounds like a good change, but how confident are we that no other statement cases would similarly be broken by being wrapped in a block?
There was a problem hiding this comment.
The only problem of wrapping with block quotes (at least in javascript), is that it creates a "local scope". Other than that, you can insert {} around any statement without changing its meaning.
Hence, in our case, the only place where this matter is that we are introducing new variables for subsequent statements. All other statements are only modifying existing vars that were already in scope, so they have no reason to be broken by being wrapped into a labelled block.
MikaelMayer
changed the title
Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
robin-aws
approved these changes
Nov 2, 2022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR fixes #2608 and fixes #2576
I added the corresponding test.
Here is the story. Whenever there is a label
L1to a statementS, the JavaScript compiler wraps the statement with curly braces{}and put the label in front of it, like this:The problem was that, if there are labelled variable declarations, they are compiled to
letand not available after}.Looking carefully at it, we don't have goto in Dafny so labels are used only to break out of loops. But these are no loops, only variable declarations. Hence, I claim it make sense to just remove the labels when compiling variable declarations.
The test now passes.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.