From 87acd37ea446d51f7133e1aea45955b1070a8b39 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 21 Mar 2024 17:12:36 -0700 Subject: [PATCH 1/5] fix: Generate proper default string value for JavaScript Fixes #5238 --- .../Backends/JavaScript/JavaScriptCodeGenerator.cs | 2 +- .../LitTests/LitTest/git-issues/git-issue-5238.dfy | 7 +++++++ .../LitTests/LitTest/git-issues/git-issue-5238.dfy.expect | 1 + 3 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy.expect diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index 8b21074b194..c8cf4bf81c5 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -974,7 +974,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree return $"{DafnyMultiSetClass}.Empty"; } else if (xType is SeqType seq) { if (seq.Arg.IsCharType) { - return "''"; + return "_dafny.Seq.UnicodeFromString('')"; } return $"{DafnySeqClass}.of()"; } else if (xType is MapType) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy new file mode 100644 index 00000000000..fa878aeba3e --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy @@ -0,0 +1,7 @@ +// RUN: %testDafnyForEachCompiler "%s" + +method Main() { + var s: seq; + s := *; + print "(", s, ")\n"; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy.expect new file mode 100644 index 00000000000..6a452c185a8 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy.expect @@ -0,0 +1 @@ +() From cbc64cd9d73969fd4b1aca8515ac907b0080c5c7 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 21 Mar 2024 17:14:07 -0700 Subject: [PATCH 2/5] Add release notes --- docs/dev/news/5239.fix | 1 + 1 file changed, 1 insertion(+) create mode 100644 docs/dev/news/5239.fix diff --git a/docs/dev/news/5239.fix b/docs/dev/news/5239.fix new file mode 100644 index 00000000000..901cf9369ba --- /dev/null +++ b/docs/dev/news/5239.fix @@ -0,0 +1 @@ +Fix the default string value emitted for JavaScript From ea03ee6114f136530a29ca3fd3fa010bce6771d7 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 22 Mar 2024 10:27:08 -0700 Subject: [PATCH 3/5] Handle Unicode-or-not default string differently (JavaScript) --- .../Backends/JavaScript/JavaScriptCodeGenerator.cs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index c8cf4bf81c5..40a1be6f276 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -974,7 +974,11 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree return $"{DafnyMultiSetClass}.Empty"; } else if (xType is SeqType seq) { if (seq.Arg.IsCharType) { - return "_dafny.Seq.UnicodeFromString('')"; + if (UnicodeCharEnabled) { + return "_dafny.Seq.UnicodeFromString(\"\")"; + } else { + return "\"\""; + } } return $"{DafnySeqClass}.of()"; } else if (xType is MapType) { From 354c7d6e5bf4504b79d1712d1ccae4a02b7d99e4 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 22 Mar 2024 10:27:23 -0700 Subject: [PATCH 4/5] Add non-Unicode tests --- .../LitTests/LitTest/git-issues/git-issue-5238.dfy | 7 ++++++- .../LitTests/LitTest/git-issues/git-issue-5238.dfy.expect | 4 +++- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy index fa878aeba3e..d8cad9a8676 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy @@ -1,7 +1,12 @@ // RUN: %testDafnyForEachCompiler "%s" +// RUN: %testDafnyForEachCompiler "%s" -- --unicode-char=false method Main() { var s: seq; s := *; - print "(", s, ")\n"; + print "(", s, ") ", s == "", " ", "" == s, " ", |s|, "\n"; + s := ""; + print "(", s, ") ", s == "", " ", "" == s, " ", |s|, "\n"; + s := "hello"; + print "(", s, ") ", s == "", " ", "" == s, " ", |s|, "\n"; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy.expect index 6a452c185a8..c4b6c940a63 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5238.dfy.expect @@ -1 +1,3 @@ -() +() true true 0 +() true true 0 +(hello) false false 5 From 7456fd59ef331b87dedbc19900bede5299f81214 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 22 Mar 2024 10:28:07 -0700 Subject: [PATCH 5/5] Fix Python non-Unicode string default value --- .../Backends/Python/PythonCodeGenerator.cs | 33 ++++++++++++------- 1 file changed, 22 insertions(+), 11 deletions(-) diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs index 1a60c1c31e4..7b61fee09fc 100644 --- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs @@ -713,7 +713,13 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree case RealType: return $"{DafnyRuntimeModule}.BigRational()"; case CollectionType: - return $"{TypeHelperName(xType)}({{}})"; + if (xType is SeqType { Arg: { IsCharType: true } }) { + var wrString = new ConcreteSyntaxTree(); + StringLiteralWrapper(wrString).Write("\"\""); + return wrString.ToString(); + } else { + return $"{TypeHelperName(xType)}({{}})"; + } case UserDefinedType udt: { var cl = udt.ResolvedClass; Contract.Assert(cl != null); @@ -1027,16 +1033,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { } break; case StringLiteralExpr str: - if (UnicodeCharEnabled) { - wr.Write($"{DafnySeqMakerFunction}(map({DafnyRuntimeModule}.CodePoint, "); - TrStringLiteral(str, wr); - wr.Write("))"); - } else { - wr.Write($"{DafnySeqMakerFunction}("); - TrStringLiteral(str, wr); - wr.Write(")"); - } - + TrStringLiteral(str, StringLiteralWrapper(wr)); break; case StaticReceiverExpr: wr.Write(TypeName(e.Type, wr, e.tok)); @@ -1063,6 +1060,20 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { } } + private ConcreteSyntaxTree StringLiteralWrapper(ConcreteSyntaxTree wr) { + ConcreteSyntaxTree wrStringGoesHere; + if (UnicodeCharEnabled) { + wr.Write($"{DafnySeqMakerFunction}(map({DafnyRuntimeModule}.CodePoint, "); + wrStringGoesHere = wr.Fork(); + wr.Write("))"); + } else { + wr.Write($"{DafnySeqMakerFunction}("); + wrStringGoesHere = wr.Fork(); + wr.Write(")"); + } + return wrStringGoesHere; + } + protected override void EmitStringLiteral(string str, bool isVerbatim, ConcreteSyntaxTree wr) { if (!isVerbatim) { wr.Write($"\"{TranslateEscapes(str)}\"");