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>

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);
  }
  }
  }

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();
+}

Test/git-issues/git-issue-4181.dfy.expect

@@ -0,0 +1 @@
+done

docs/dev/news/4181.fix

@@ -0,0 +1 @@
+Reserved module identifiers correctly escaped in GoLang