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

Invalid UTF-16 strings cause print to crash on some backends #2925

Closed
robin-aws opened this issue Oct 25, 2022 · 0 comments · Fixed by #2926
Closed

Invalid UTF-16 strings cause print to crash on some backends #2925

robin-aws opened this issue Oct 25, 2022 · 0 comments · Fixed by #2926
Assignees
@robin-aws
Labels
lang: golang Dafny's transpiler to Go and its runtime lang: python Dafny's Python transpiler and its runtime part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant)

Comments

@robin-aws
Copy link
Member 

method Main() {
  print("\uDFFF");
}

Fails to compile on Go, crashes at runtime for Python.
@robin-aws robin-aws added lang: golang Dafny's transpiler to Go and its runtime part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant) lang: python Dafny's Python transpiler and its runtime severity: soundness (crash) labels Oct 25, 2022
@robin-aws robin-aws self-assigned this Oct 25, 2022
@robin-aws robin-aws mentioned this issue Oct 25, 2022
Merged
robin-aws added a commit that referenced this issue Nov 3, 2022
@robin-aws @cpitclaudel
fix: Handle UTF-16 escapes and invalid surrogate sequences in Python …
c81c3ca 
…and Go (#2926)

Fixes #1980. Fixes #2925.

Should fix the root cause of #2934, but I'm not claiming the complete
fix, as attempting to include unescaped, non-ASCII characters in a Dafny
source file is revealing platform-specific headaches in the integration
test runner I'd like to address in a separate PR.

Printing non-ASCII characters, especially invalid UTF-16 sequences, is
still inconsistent across backends, but at least should not crash after
this change. Again this is difficult to test effectively across
platforms in our testing architecture.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Co-authored-by: Clément Pit-Claudel <[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
lang: golang Dafny's transpiler to Go and its runtime lang: python Dafny's Python transpiler and its runtime part: runtime Happens in Dafny's runtime (Add a `lang` tag if relevant)
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Handle UTF-16 escapes and invalid surrogate sequences in Python and Go robin-aws/dafny
1 participant
@robin-aws