-
Notifications
You must be signed in to change notification settings - Fork 256
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
Fix: Compilation of continue labels no longer crashing in Go #4171
Fix: Compilation of continue labels no longer crashing in Go #4171
Conversation
@@ -0,0 +1,13 @@ | |||
// RUN: %testDafnyForEachCompiler "%s" |
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.
@robin-aws your script required me to change my test for the Go compiler to every compiler. Nice job!
@@ -1835,9 +1835,11 @@ protected class ClassWriter : IClassWriter { | |||
} | |||
|
|||
protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool createContinueLabel, ConcreteSyntaxTree wr) { | |||
wr.WriteLine("{"); |
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.
Instead of explicitly adding the open and close curly braces, change the var w = wr.Fork();
line to
var w = wr.NewBlock(open: BlockStyle.Brace);
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.
I can't because we need to add a label right after the final closing brace (line 1843), unless you have another suggestion?
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.
I don't see that the label after the closing brace is a problem, but I now see that the goto between the fork point and the closing curly is. So, the Fork
is necessary, after all. My bad.
However, when I now look at that, it seems that both the forked w
and the goto ...
are not indented inside the curly braces. The best way to fix that is to use a NewBlock
.
In summary, would the following body of CreateLabeledCode
work for you?
var wBody = wr.NewBlock(open: BlockStyle.Brace);
var w = wBody.Fork();
var prefix = createContinueLabel ? "C" : "L";
wBody.WriteLine($"goto {prefix}{label};");
wr.Fork(-1).WriteLine($"{prefix}{label}:");
return w;
Test/git-issues/git-issue-3978.dfy
Outdated
|
||
method Main() returns () | ||
{ | ||
for v_int_7 := 3 to 18 |
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.
I see this is how the bug report showed the code. Still, I would suggest renaming v_int_7
and v_int_93
to something like x
and y
.
Test/git-issues/git-issue-3978.dfy
Outdated
@@ -0,0 +1,13 @@ | |||
// RUN: %testDafnyForEachCompiler "%s" | |||
|
|||
method Main() returns () |
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.
Remove returns ()
@@ -1835,9 +1835,11 @@ protected class ClassWriter : IClassWriter { | |||
} | |||
|
|||
protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool createContinueLabel, ConcreteSyntaxTree wr) { | |||
wr.WriteLine("{"); |
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.
I don't see that the label after the closing brace is a problem, but I now see that the goto between the fork point and the closing curly is. So, the Fork
is necessary, after all. My bad.
However, when I now look at that, it seems that both the forked w
and the goto ...
are not indented inside the curly braces. The best way to fix that is to use a NewBlock
.
In summary, would the following body of CreateLabeledCode
work for you?
var wBody = wr.NewBlock(open: BlockStyle.Brace);
var w = wBody.Fork();
var prefix = createContinueLabel ? "C" : "L";
wBody.WriteLine($"goto {prefix}{label};");
wr.Fork(-1).WriteLine($"{prefix}{label}:");
return w;
This PR fixes #3978
Our compiler hit the problem stated there: golang/go#27165
I haven't tested if this problem is fixed in a more recent version of the Go compiler, but a workaround I found is to wrap the labelled code with curly braces, so that the goto escape the scope when jumping to the label, hence Go does not complain anymore about jumping over variable declaration
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.