Merge branch 'master' into onlyClaimVerificationMemoryPerModule

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