Encoding mismatches result in runtime crashes in customer code compiled to Go

[cpitclaudel]

Input:

method Main() {
  var escaped := "\u00E9"; // UTF-16 version of é
  var unescaped := "é";

  print |escaped|, "\n";
  print |unescaped|, "\n";
  print "'", escaped, "'", "\n";
  print "'", unescaped, "'", "\n";

  assert |escaped| == 1;
  assert |unescaped| == 1;

  if |escaped| == 2 {
    print 1 / 0;
  }

  if |unescaped| == 2 {
    print 1 / 0;
  }
}

Output, with go:

2
2
'%!v(PANIC=String method: interface conversion: interface {} is nil, not dafny.Char)'
'%!v(PANIC=String method: interface conversion: interface {} is nil, not dafny.Char)'
[Program halted] division by zero

What leads to the issue:

1. The Dafny file is read as UTF-8. In memory, escaped is represented as 6 C# "chars", and unescaped as one C# char (UCS2)
2. At verification time, both of these are treated as one-character strings
3. When compiled to go, both strings are encoded as UTF-8 and printed to a go file, so the go file contains the same string literals as the Dafny file. This is doubly wrong: the escaped string has a different meaning in Go, and the unescaped string ends up written as two bytes in the target file (utf-8)
4. The StringToSeq function in the Go runtime does not encode to UTF-16 before converting, so for unescaped the final byte sequence is the UTF-8 one (length = 2)

#2926 currently fixes the issue with unescaped, but not with escaped.

[robin-aws]

Thanks for writing this up. As discussed I've updated #2926 to account for this case too - have a look and make sure my test cases are thorough enough!

[robin-aws]

#2926 currently fixes the issue with unescaped, but not with escaped.

Other way around as it turns out: it should fix both, but I'm not claiming to fix unescaped characters because I had to remove the corresponding flaky tests until we address #2976

[robin-aws]

#3016 finished addressing this by adding the missing tests.