-
Notifications
You must be signed in to change notification settings - Fork 261
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: Constant initialization in the Dafny-to-Rust code generator #5837
Conversation
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.
Thanks for the quick fix. As a follow up can we re-enable the Rust backend in %testDafnyForEachCompiler
?
docs/dev/news/5833.fix
Outdated
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.
Intentional?
Have we been announcing bug fixes like this while the Rust code generator isn't fully supported yet?
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'd prefer to leave it quiet too.
@@ -323,6 +323,7 @@ module {:extern "DAST"} DAST { | |||
UnboundedIntRange(start: Expression, up: bool) | | |||
Quantifier(elemType: Type, collection: Expression, is_forall: bool, lambda: Expression) | |||
|
|||
datatype FieldMutability = ConstantField | MutableField | InternalConstantField |
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.
datatype FieldMutability = ConstantField | MutableField | InternalConstantField | |
datatype FieldMutability = ConstantField | ClassMutableField | ClassConstantField |
I didn't understand "InternalConstantField" until I looked at the test.
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.
ClassMutableField is ok, but the last one is really internal, so it should be ClassInternalConstantField, all right?
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.
Thanks for adding the comment, that helps
} else { | ||
r := read_field_macro.Apply1(r); // Already contains a clone. | ||
assert fieldMutability.MutableField?; |
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.
Wouldn't a match statement be a little cleaner? (Instead of the chained if)
…fny-lang/dafny into fix-5833-const-initialization
Fixes #5833
Description
There are now three kinds of generated fields:
::dafny_runtime::Field<...>
to avoid any soundness issue, and use the wrappersread_field
andmodify_field
to read and modify them.Before this PR, only the last two were implemented, which lead to issues when trying to assign the default value of a class constant.
This issue was not captured because the test started to fail but since it's was marked
%testForEachCompiler
and these tests are ignored in the CI, we did not detect it.How has this been tested?
Updated the file classes.dfy. All other tests in comp/rust should pass.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.