Fix GoLang issue when module and datatype names collide

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -210,13 +210,18 @@ public string SanitizedName {
 
  string compileName;
 
+ public ModuleDefinition GetImplementedModule() {
+ return Implements is { Kind: ImplementationKind.Replacement } ? Implements.Target.Def : null;
+ }
+
  public string GetCompileName(DafnyOptions options) {
  if (compileName != null) {
  return compileName;
  }
 
- if (Implements is { Kind: ImplementationKind.Replacement }) {
- return Implements.Target.Def.GetCompileName(options);
+ var implemented = GetImplementedModule();
+ if (implemented != null) {
+ return implemented.GetCompileName(options);
  }
 
  var externArgs = options.DisallowExterns ? null : Attributes.FindExpressions(this.Attributes, "extern");

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -163,7 +163,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
  wr.WriteLine("#if ISDAFNYRUNTIMELIB");
  }
 
- var dafnyNamespace = CreateModule("Dafny", false, null, null, null, wr);
+ var dafnyNamespace = CreateModule(null, "Dafny", false, null, null, null, wr);
  EmitInitNewArrays(systemModuleManager, dafnyNamespace);
  if (Synthesize) {
  CsharpSynthesizer.EmitMultiMatcher(dafnyNamespace);
@@ -274,7 +274,8 @@ string IdProtectModule(string moduleName) {
  return string.Join(".", moduleName.Split(".").Select(IdProtect));
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+ ModuleDefinition externModule,
  string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
  moduleName = IdProtectModule(moduleName);
  return wr.NewBlock($"namespace {moduleName}", " // end of " + $"namespace {moduleName}");

Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs

@@ -159,7 +159,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
  return wr.NewBlock($"int main(DafnySequence<DafnySequence<char>> {argsParameterName})");
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+ ModuleDefinition externModule,
  string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
  var s = $"namespace {IdProtect(moduleName)} ";
  string footer = "// end of " + s + " declarations";

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -124,7 +124,8 @@ private bool NeedsExternalImport(MemberDecl memberDecl) {
  memberDecl is Function { Body: null } or Method { Body: null };
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+ ModuleDefinition externModule,
  string libraryName, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
  if (currentBuilder is ModuleContainer moduleBuilder) {
  var attributes = (Sequence<DAST.Attribute>)ParseAttributes(moduleAttributes);

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -19,6 +19,13 @@
 
 namespace Microsoft.Dafny.Compilers {
  class GoCodeGenerator : SinglePassCodeGenerator {
+ protected override void EmitStaticExternMethodQualifier(string qual, ConcreteSyntaxTree wr) {
+ if (qual != null) {
+ qual = ImportPrefix + qual;
+ }
+ base.EmitStaticExternMethodQualifier(qual, wr);
+ }
+
  protected override bool RequiresAllVariablesToBeUsed => true;
  private string DafnyRuntimeGoModule = "github.com/dafny-lang/DafnyRuntimeGo/v4/";
 
@@ -32,7 +39,7 @@ public GoCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(opti
  }
  if (Options?.CoverageLegendFile != null) {
  //TODO: What's the module name for this?
- Imports.Add(new Import { Name = "DafnyProfiling", Path = "DafnyProfiling" });
+ ImportsNotFromDafnyModules.Add(new Import { Name = "DafnyProfiling", Path = "DafnyProfiling" });
  }
  }
 
@@ -52,8 +59,10 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
  return $"_default_{tp.GetCompileName(Options)}";
  }
 
- private readonly List<Import> Imports = new(StandardImports);
+ private readonly Dictionary<ModuleDefinition, Import> ModuleImports = new();
+ private readonly List<Import> ImportsNotFromDafnyModules = new(StandardImports);
  private string ModuleName;
+ private ModuleDefinition CurrentModule;
  private ConcreteSyntaxTree RootImportWriter;
  private ConcreteSyntaxTree RootImportDummyWriter;
 
@@ -64,6 +73,7 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
  };
  private static string DummyTypeName = "Dummy__";
 
+ private static string ImportPrefix = "m_";
  private struct Import {
  public string Name, Path;
  public ModuleDefinition ExternModule;
@@ -72,6 +82,7 @@ private struct Import {
  protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
  wr.WriteLine("// Dafny program {0} compiled into Go", program.Name);
 
+ CurrentModule = null;
  ModuleName = MainModuleName = program.MainMethod != null ? "main" : TransformToClassName(Path.GetFileNameWithoutExtension(program.Name));
 
  wr.WriteLine("package {0}", ModuleName);
@@ -84,7 +95,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
  } else {
  path = GoModuleMode ? DafnyRuntimeGoModule : "";
  }
- Imports.Add(new Import { Name = "_dafny", Path = $"{path}dafny" });
+ ImportsNotFromDafnyModules.Add(new Import { Name = "_dafny", Path = $"{path}dafny" });
 
  if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
  EmitRuntimeSource("DafnyStandardLibraries_go", wr);
@@ -123,7 +134,7 @@ void EmitImports(ConcreteSyntaxTree wr, out ConcreteSyntaxTree importWriter, out
  wr.WriteLine(")");
  importDummyWriter = wr.Fork();
  if (ModuleName != "dafny") {
- foreach (var import in Imports) {
+ foreach (var import in ImportsNotFromDafnyModules.Concat(ModuleImports.Values)) {
  EmitImport(import, importWriter, importDummyWriter);
  }
  }
@@ -133,6 +144,7 @@ public string TransformToClassName(string baseName) =>
  IdProtect(Regex.Replace(baseName, "[^_A-Za-z0-9$]", "_"));
 
  public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
+ CurrentModule = null;
  var companion = TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(mainMethod.EnclosingClass), wr, mainMethod.tok, mainMethod);
 
  var wBody = wr.NewNamedBlock("func main()");
@@ -158,7 +170,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
  return wr.NewNamedBlock("func (_this * {0}) Main({1} _dafny.Sequence)", FormatCompanionTypeName(((GoCodeGenerator.ClassWriter)cw).ClassName), argsParameterName);
  }
 
- private Import CreateImport(string moduleName, bool isDefault, ModuleDefinition externModule, string /*?*/ libraryName) {
+ private Import CreateImport(string moduleName, ModuleDefinition externModule,
+ string /*?*/ libraryName) {
  string pkgName;
  if (libraryName != null) {
  pkgName = libraryName;
@@ -176,7 +189,7 @@ private Import CreateImport(string moduleName, bool isDefault, ModuleDefinition
  }
 
 
- return new Import { Name = moduleName, Path = pkgName, ExternModule = externModule };
+ return new Import { Name = ImportPrefix + moduleName, Path = pkgName, ExternModule = externModule };
  }
 
  protected override bool ShouldCompileModule(Program program, ModuleDefinition module) {
@@ -191,7 +204,7 @@ protected override bool ShouldCompileModule(Program program, ModuleDefinition mo
  return true;
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault,
+ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
  ModuleDefinition externModule,
  string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
  if (isDefault) {
@@ -208,13 +221,14 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef
  }
  }
  ModuleName = PublicModuleIdProtect(moduleName);
- var import = CreateImport(ModuleName, isDefault, externModule, libraryName);
+ CurrentModule = module;
+ var import = CreateImport(ModuleName, externModule, libraryName);
  var filename = string.Format("{0}/{0}.go", import.Path);
  var w = wr.NewFile(filename);
  EmitModuleHeader(w);
 
  import.Path = goModuleName + import.Path;
- AddImport(import);
+ AddImport(module, import);
 
  return w;
  }
@@ -253,20 +267,26 @@ protected override void DependOnModule(Program program, ModuleDefinition module,
  }
 
  var publicModuleName = PublicModuleIdProtect(module.GetCompileName(Options));
- var import = CreateImport(publicModuleName, module.IsDefaultModule, externModule, libraryName);
+ var import = CreateImport(publicModuleName, externModule, libraryName);
  import.Path = goModuleName + import.Path;
- AddImport(import);
+ AddImport(module, import);
  }
 
  protected override void FinishModule() {
+ CurrentModule = null;
  ModuleName = MainModuleName;
  }
 
- private void AddImport(Import import) {
+ private void AddImport(ModuleDefinition module, Import import) {
  // Import in root module
  EmitImport(import, RootImportWriter, RootImportDummyWriter);
  // Import in all subsequent modules
- Imports.Add(import);
+ ModuleImports[module] = import;
+ var implemented = module.GetImplementedModule();
+ while (implemented != null) {
+ ModuleImports[implemented] = import;
+ implemented = implemented.GetImplementedModule();
+ }
  }
 
  private void EmitImport(Import import, ConcreteSyntaxTree importWriter, ConcreteSyntaxTree importDummyWriter) {
@@ -1832,10 +1852,10 @@ protected override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, I
  // XXX This duplicates some of the logic in UserDefinedTypeName, but if we
  // don't do it here, we end up passing the name of the module to
  // FormatCompanionName, which doesn't help anyone
- if (type is UserDefinedType udt && udt.ResolvedClass != null && IsExternMemberOfExternModule(member, udt.ResolvedClass)) {
+ if (type is UserDefinedType { ResolvedClass: not null } udt && IsExternMemberOfExternModule(member, udt.ResolvedClass)) {
  // omit the default class name ("_default") in extern modules, when the class is used to qualify an extern member
  Contract.Assert(!udt.ResolvedClass.EnclosingModuleDefinition.IsDefaultModule); // default module is not marked ":extern"
- return IdProtect(udt.ResolvedClass.EnclosingModuleDefinition.GetCompileName(Options));
+ return IdProtect(ModuleImports[udt.ResolvedClass.EnclosingModuleDefinition].Name);
  }
  return TypeName_Related(FormatCompanionName, type, wr, tok, member);
  }
@@ -2683,7 +2703,12 @@ 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));
+ string enclosingModuleDefinitionId;
+ if (CurrentModule == cl.EnclosingModuleDefinition || cl.EnclosingModuleDefinition.IsDefaultModule) {
+ enclosingModuleDefinitionId = PublicModuleIdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options));
+ } else {
+ enclosingModuleDefinitionId = ModuleImports[cl.EnclosingModuleDefinition].Name;
+ }
  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"
@@ -2702,7 +2727,6 @@ private string UserDefinedTypeName(TopLevelDecl cl, bool full, MemberDecl/*?*/ m
  // 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 == enclosingModuleDefinitionId) {
  return IdName(cl);
  } else {

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -379,7 +379,8 @@ string IdProtectModule(string moduleName) {
  return string.Join(".", moduleName.Split(".").Select(IdProtect));
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+ ModuleDefinition externModule,
  string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
  moduleName = IdProtectModule(moduleName);
  if (isDefault) {

Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs

@@ -63,7 +63,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
  return wr.NewBlock($"static Main({argsParameterName})");
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+ ModuleDefinition externModule,
  string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
  moduleName = IdProtect(moduleName);
  if (externModule == null || libraryName != null) {

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -98,7 +98,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
  return mw.NewBlockPy($"def StaticMain({argsParameterName}):");
  }
 
- protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+ ModuleDefinition externModule,
  string libraryName, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
  var pythonModuleName = PythonModuleMode ? PythonModuleName + "." : "";
 

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -12,6 +12,7 @@
 using System.IO;
 using System.Diagnostics.Contracts;
 using DafnyCore;
+using DafnyCore.Options;
 using JetBrains.Annotations;
 using Microsoft.BaseTypes;
 using static Microsoft.Dafny.GeneratorErrors;
@@ -187,7 +188,8 @@ protected virtual bool ShouldCompileModule(Program program, ModuleDefinition mod
  return module.ShouldCompile(program.Compilation);
  }
 
- protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ protected abstract ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+ ModuleDefinition externModule,
  string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr);
  /// <summary>
  /// Indicates the current program depends on the given module without creating it.
@@ -1590,7 +1592,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
 
  Contract.Assert(enclosingModule == null);
  enclosingModule = module;
- var wr = CreateModule(module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName, module.Attributes, programNode);
+ var wr = CreateModule(module, module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName, module.Attributes, programNode);
  var v = new CheckHasNoAssumes_Visitor(this, wr);
  foreach (TopLevelDecl d in module.TopLevelDecls) {
  if (!ProgramResolver.ShouldCompile(d)) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/moduleDatatypeNameCollision/moduleDatatypeNameCollision.dfy

@@ -0,0 +1,18 @@
+// NONUNIFORM: this fails on Java
+// RUN: %run --target go %s > %t
+// RUN: %diff "%s.expect" "%t"
+
+module DuplicateName {
+ const x := 3 
+}
+
+module ProblemModule {
+ datatype DuplicateName = DuplicateName
+}
+
+import D = DuplicateName
+
+method Main() {
+ print D.x;
+}
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/moduleDatatypeNameCollision/moduleDatatypeNameCollision.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+3

Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/GoModule.dfy

@@ -1,7 +1,7 @@
 // NONUNIFORM: Go-specific extern test
 // RUN: %exits-with 3 %run --allow-external-contracts --target go "%s" &> "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
-// CHECK: undefined: GoModuleConversions.ParseURL
+// CHECK: undefined: m_GoModuleConversions.ParseURL
 
 // This test used to work only because of a questionable Go-only feature
 // of mapping a Dafny string directly to a Go string when passed in or out of