From 690f1f20fd4067e6a7a83c53914b7eeb44019bc2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <MikaelMayer@users.noreply.github.com>
Date: Mon, 1 Apr 2024 06:32:29 -0500
Subject: [PATCH] Fix: Reserved module identifiers correctly escaped in GO
 (#4431)

This PR fixes #4181
I added the corresponding test.
Basically, module identifiers did not go through IdProtect when
compiling to go, both on the declaration site and import site. This PR
fixes that.

<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>
---
 .../Backends/GoLang/GoCodeGenerator.cs        | 28 +++++++++++++------
 Test/git-issues/git-issue-4181.dfy            | 11 ++++++++
 Test/git-issues/git-issue-4181.dfy.expect     |  1 +
 docs/dev/news/4181.fix                        |  1 +
 4 files changed, 32 insertions(+), 9 deletions(-)
 create mode 100644 Test/git-issues/git-issue-4181.dfy
 create mode 100644 Test/git-issues/git-issue-4181.dfy.expect
 create mode 100644 docs/dev/news/4181.fix

diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
index d001837f05..961ed13aa8 100644
--- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
@@ -110,8 +110,8 @@ void EmitImports(ConcreteSyntaxTree wr, out ConcreteSyntaxTree importWriter, out
       }
     }
 
-    public static string TransformToClassName(string baseName) =>
-      Regex.Replace(baseName, "[^_A-Za-z0-9$]", "_");
+    public string TransformToClassName(string baseName) =>
+      IdProtect(Regex.Replace(baseName, "[^_A-Za-z0-9$]", "_"));
 
     public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
       var companion = TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(mainMethod.EnclosingClass), wr, mainMethod.tok, mainMethod);
@@ -167,11 +167,11 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef
         return wr;
       }
 
-      var import = CreateImport(moduleName, isDefault, externModule, libraryName);
+      ModuleName = PublicModuleIdProtect(moduleName);
+      var import = CreateImport(ModuleName, isDefault, externModule, libraryName);
 
       var filename = string.Format("{0}/{0}.go", import.Path);
       var w = wr.NewFile(filename);
-      ModuleName = moduleName;
       EmitModuleHeader(w);
 
       AddImport(import);
@@ -2519,6 +2519,14 @@ public override string PublicIdProtect(string name) {
       }
     }
 
+    public string PublicModuleIdProtect(string name) {
+      if (name == "C") {
+        return "_C";
+      } else {
+        return name;
+      }
+    }
+
     protected override string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null) {
       return UserDefinedTypeName(udt, full: true, member: member);
     }
@@ -2541,28 +2549,30 @@ private string UserDefinedTypeName(UserDefinedType udt, bool full, MemberDecl/*?
     }
 
     private string UserDefinedTypeName(TopLevelDecl cl, bool full, MemberDecl/*?*/ member = null) {
+      var enclosingModuleDefinitionId = PublicModuleIdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options));
       if (IsExternMemberOfExternModule(member, cl)) {
         // omit the default class name ("_default") in extern modules, when the class is used to qualify an extern member
         Contract.Assert(!cl.EnclosingModuleDefinition.IsDefaultModule);  // default module is not marked ":extern"
-        return IdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options));
+        return enclosingModuleDefinitionId;
       } else {
         if (cl.IsExtern(Options, out var qual, out _)) {
           // No need to take into account the second argument to extern, since
           // it'll already be cl.CompileName
           if (qual == null) {
-            if (this.ModuleName == cl.EnclosingModuleDefinition.GetCompileName(Options)) {
+            if (this.ModuleName == enclosingModuleDefinitionId) {
               qual = "";
             } else {
-              qual = cl.EnclosingModuleDefinition.GetCompileName(Options);
+              qual = enclosingModuleDefinitionId;
             }
           }
           // Don't use IdName since that'll capitalize, which is unhelpful for
           // built-in types
           return qual + (qual == "" ? "" : ".") + cl.GetCompileName(Options);
-        } else if (!full || cl.EnclosingModuleDefinition.TryToAvoidName || this.ModuleName == cl.EnclosingModuleDefinition.GetCompileName(Options)) {
+
+        } else if (!full || cl.EnclosingModuleDefinition.TryToAvoidName || this.ModuleName == enclosingModuleDefinitionId) {
           return IdName(cl);
         } else {
-          return cl.EnclosingModuleDefinition.GetCompileName(Options) + "." + IdName(cl);
+          return enclosingModuleDefinitionId + "." + IdName(cl);
         }
       }
     }
diff --git a/Test/git-issues/git-issue-4181.dfy b/Test/git-issues/git-issue-4181.dfy
new file mode 100644
index 0000000000..1f6928be6c
--- /dev/null
+++ b/Test/git-issues/git-issue-4181.dfy
@@ -0,0 +1,11 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+module C {
+  method Test() {
+    print "done\n";
+  }
+}
+
+method Main(){
+  C.Test();
+}
\ No newline at end of file
diff --git a/Test/git-issues/git-issue-4181.dfy.expect b/Test/git-issues/git-issue-4181.dfy.expect
new file mode 100644
index 0000000000..19f86f493a
--- /dev/null
+++ b/Test/git-issues/git-issue-4181.dfy.expect
@@ -0,0 +1 @@
+done
diff --git a/docs/dev/news/4181.fix b/docs/dev/news/4181.fix
new file mode 100644
index 0000000000..2678836452
--- /dev/null
+++ b/docs/dev/news/4181.fix
@@ -0,0 +1 @@
+Reserved module identifiers correctly escaped in GoLang
\ No newline at end of file