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.

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

Null character escape not encoded correctly in most backends #2928

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

Null character escape not encoded correctly in most backends #2928

robin-aws opened this issue Oct 26, 2022 · 0 comments · Fixed by #3016
Assignees
Labels
lang: c++ Dafny's C++ transpiler and its runtime lang: golang Dafny's transpiler to Go and its runtime lang: java Dafny's Java transpiler and its runtime lang: js Dafny's JavaScript transpiler and its runtime lang: python Dafny's Python transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag

Comments

@robin-aws
Copy link
Member

This program is a doozy, it ONLY runs without crashing on C#:

method Main() {
  var s := "\03";
  assert s[0] == 0 as char;
  assert s[1] == '3';

  expect s[0] == 0 as char;
  expect s[1] == '3';
}

Most backends are not escaping the \0 escape properly, and hence trying to interpret \03 an octal escape. Go attempts to handle this by padding to \003 which is a valid Go escape sequence, but in so doing changes the value of the string!

@robin-aws robin-aws added part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag lang: golang Dafny's transpiler to Go and its runtime lang: js Dafny's JavaScript transpiler and its runtime lang: java Dafny's Java transpiler and its runtime lang: c++ Dafny's C++ transpiler and its runtime lang: python Dafny's Python transpiler and its runtime severity: soundness (crash) labels Oct 26, 2022
@robin-aws robin-aws self-assigned this Oct 26, 2022
robin-aws added a commit that referenced this issue Nov 24, 2022
Implementation of the design from
dafny-lang/rfcs#13.

Resolves #413. Fixes #2928. Fixes #818. Fixes #3058. Fixes #1293. Fixes
#3001.

Depends on #2976 to be fixed for the tests to pass consistently across
platforms.

I've documented some of the less obvious compilation strategy decisions
in `docs/Compilation/StringsAndChars.md`.

<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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
lang: c++ Dafny's C++ transpiler and its runtime lang: golang Dafny's transpiler to Go and its runtime lang: java Dafny's Java transpiler and its runtime lang: js Dafny's JavaScript transpiler and its runtime lang: python Dafny's Python transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant