Method rename, hopefully fixing Java testing flakiness

dafny-lang · Oct 27, 2022 · 7e3d243 · 7e3d243
1 parent 057bf25
commit 7e3d243
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 6 deletions.
diff --git a/Source/DafnyCore/Compilers/Compiler-go.cs b/Source/DafnyCore/Compilers/Compiler-go.cs
@@ -2097,7 +2097,7 @@ protected void TrCharLiteral(CharLiteralExpr chr, ConcreteSyntaxTree wr) {
       var v = (string)chr.Value;
       wr.Write("_dafny.Char(");
       // See comment in TrStringLiteral for why we can't just translate directly sometimes.
-      if (Util.Escapes(v, false).Any(e => e.StartsWith(@"\u"))) {
+      if (Util.TokensWithEscapes(v, false).Any(e => e.StartsWith(@"\u"))) {
         var c = Util.UnescapedCharacters(v, false).Single();
         wr.Write($"{(int)c}");
       } else {
@@ -2116,7 +2116,7 @@ protected override void TrStringLiteral(StringLiteralExpr str, ConcreteSyntaxTre
       // _dafny.SeqOfString("..."), since there's no way to encode the right data in the Go string literal.
       // Instead, if any escapes are present, just emit a sequence of the direct UTF-16 code units instead.
       var s = (string)str.Value;
-      if (!str.IsVerbatim && Util.Escapes(s, false).Any(e => e.StartsWith(@"\u"))) {
+      if (!str.IsVerbatim && Util.TokensWithEscapes(s, false).Any(e => e.StartsWith(@"\u"))) {
         wr.Write("_dafny.SeqOfChars(");
         var comma = "";
         foreach (var c in Util.UnescapedCharacters(s, str.IsVerbatim)) {

diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs
@@ -2094,7 +2094,7 @@ private string FieldName(Formal formal, int i) {
 
     protected override void EmitPrintStmt(ConcreteSyntaxTree wr, Expression arg) {
       var wStmts = wr.Fork();
-      wr.Write("System.out.print(");
+      wr.Write($"{DafnyHelpersClass}.utf8Out.print(");
       EmitToString(wr, arg, wStmts);
       wr.WriteLine(");");
     }

diff --git a/Source/DafnyCore/Util.cs b/Source/DafnyCore/Util.cs
@@ -203,7 +203,7 @@ public static string RemoveEscaping(string s, bool isVerbatimString) {
     /// </summary>
     public static IEnumerable<char> UnescapedCharacters(string p, bool isVerbatimString) {
       if (isVerbatimString) {
-        foreach (var s in Escapes(p, true)) {
+        foreach (var s in TokensWithEscapes(p, true)) {
           if (s == "\"\"") {
             yield return '"';
           } else {
@@ -213,7 +213,7 @@ public static IEnumerable<char> UnescapedCharacters(string p, bool isVerbatimStr
           }
         }
       } else {
-        foreach (var s in Escapes(p, false)) {
+        foreach (var s in TokensWithEscapes(p, false)) {
           switch (s) {
             case @"\'": yield return '\''; break;
             case @"\""": yield return '"'; break;
@@ -240,7 +240,7 @@ public static IEnumerable<char> UnescapedCharacters(string p, bool isVerbatimStr
     /// For example, "ab\tuv\u12345" may be broken up as ["a", "b", "\t", "u", "v", "\u1234", "5"].
     /// Consecutive non-escaped characters may or may not be enumerated as a single string.
     /// </summary>
-    public static IEnumerable<string> Escapes(string p, bool isVerbatimString) {
+    public static IEnumerable<string> TokensWithEscapes(string p, bool isVerbatimString) {
       Contract.Requires(p != null);
       if (isVerbatimString) {
         var skipNext = false;

diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java
@@ -15,9 +15,20 @@
 import java.util.stream.Collectors;
 import java.util.stream.IntStream;
 import java.util.stream.Stream;
+import java.io.PrintStream;
+import java.io.UnsupportedEncodingException;
 
 public class Helpers {
 
+    public static PrintStream utf8Out;
+    static {
+        try {
+            utf8Out = new PrintStream(System.out, true, "UTF-8");
+        } catch (UnsupportedEncodingException e) {
+            throw new RuntimeException(e);
+        }
+    }
+
     public static DafnySequence<? extends DafnySequence<? extends Character>> FromMainArguments(String[] args) {
        @SuppressWarnings("unchecked")
        TypeDescriptor<DafnySequence<? extends Character>> type = DafnySequence.<Character>_typeDescriptor(TypeDescriptor.CHAR);