Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Missing coercions in edge cases for characters in Java with --unicode-char #3413

Closed
robin-aws opened this issue Jan 26, 2023 · 0 comments · Fixed by #3630
Closed

Missing coercions in edge cases for characters in Java with --unicode-char #3413

robin-aws opened this issue Jan 26, 2023 · 0 comments · Fixed by #3630
Assignees
@robin-aws
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime
Milestone
Dafny 4.0

Comments

@robin-aws
Copy link
Member

Follow-up from #2818. Test/unicodechars/comp/Arrays.dfy doesn't work for Java because of several cases of missing coercions between int and CodePoint. I have the fixes but they need clean up.
@robin-aws robin-aws self-assigned this Jan 26, 2023
@robin-aws robin-aws added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime labels Jan 26, 2023
@robin-aws robin-aws added this to the Dafny 4.0 milestone Feb 9, 2023
@RustanLeino RustanLeino mentioned this issue Feb 24, 2023
Merged
robin-aws added a commit that referenced this issue Feb 27, 2023
@robin-aws @RustanLeino
@fabiomadge @atomb
fix: Java --unicode-char mode coercion improvements (#3630)
de510d9 
Fixes #3413.

Addresses the issues uncovered during #2818 by adding a `--unicode-char`
mode version of `Test/comp/Arrays.dfy`, which all stem from incomplete
handling of manual boxing/unboxing of the `CodePoint` type at various
Java code generation points. Note this is still incomplete as there must
be other spots that do not handle coercion correctly in general, but
these changes at least cover `Arrays.dfy`.

It turned out that handling arrow coercion as in the Go compiler was not
necessary for Java, because the initial casting of a function reference
as a lambda is where the necessary boxing/unboxing needs to happen
instead anyway. That is, a reference to a Dafny `function f(x: char):
char` has to end up as a Java `Function<CodePoint, CodePoint>` and
therefore be eta expanded from the start.

Also removed the fail-fast behavior from `%testDafnyForEachCompiler` as
I found it more useful for debugging that way.

Also implemented `ConcreteSyntaxTree.Comma` as part of an initial
implementation of Java arrow conversion, which ended up not directly
used but seems useful enough to keep (and I refactored one spot to use
it as an example).

Edit: I've also added a few more similar cases exposed as part of
enabling `/unicodeChar:1` by default for Dafny 4.0:
#3635

Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Fabio Madge <[email protected]>
Co-authored-by: Aaron Tomb <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@robin-aws robin-aws

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime
Projects
None yet
Milestone
Dafny 4.0
Development

Successfully merging a pull request may close this issue.

fix: Java --unicode-char mode coercion improvements robin-aws/dafny
1 participant
@robin-aws