Try to make Go imports specialized to the importing module

dafny-lang · Oct 9, 2024 · 22a1bf7 · 22a1bf7
1 parent 1c28462
commit 22a1bf7
Show file tree

Hide file tree

Showing 10 changed files with 60 additions and 28 deletions.
diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/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}");

diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/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";

diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/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);

diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
@@ -106,14 +106,19 @@ private bool IsDafnySequence(TopLevelDecl d) =>
 
     private string DafnySequenceCompanion => $"{HelperModulePrefix}Companion_Sequence_";
 
-    void EmitModuleHeader(ConcreteSyntaxTree wr) {
+    void EmitModuleHeader(ConcreteSyntaxTree wr, ModuleDefinition module) {
       wr.WriteLine("// Package {0}", ModuleName);
       wr.WriteLine("// Dafny module {0} compiled into Go", ModuleName);
       wr.WriteLine();
       wr.WriteLine("package {0}", ModuleName);
       wr.WriteLine();
-      // This is a non-main module; it only imports things declared before it, so we don't need these writers
-      EmitImports(wr, out _, out _);
+      EmitImports(wr, out var importWriter, out var dummyImportWriter);
+      foreach (var alias in module.TopLevelDecls.OfType<ImportModuleDecl>()) {
+        var importedDef = alias.TargetQId.Decl.Signature.ModuleDef;
+        var externModule = GetExternalModuleFromModule(importedDef, out var libraryName);
+        var import = CreateImport(importedDef.GetCompileName(Options), false, externModule, libraryName); 
+        EmitImport(import, importWriter, dummyImportWriter);
+      }
       wr.WriteLine();
       wr.WriteLine("type {0} struct{{}}", DummyTypeName);
       wr.WriteLine();
@@ -193,7 +198,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) {
@@ -213,7 +218,7 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef
       var import = CreateImport(ModuleName, isDefault, externModule, libraryName);
       var filename = string.Format("{0}/{0}.go", import.Path);
       var w = wr.NewFile(filename);
-      EmitModuleHeader(w);
+      EmitModuleHeader(w, module);
 
       import.Path = goModuleName + import.Path;
       AddImport(import);

diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/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) {

diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/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) {

diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/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 + "." : "";
 

diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
@@ -187,7 +187,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.
@@ -1570,18 +1571,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
 
       DetectAndMarkCapitalizationConflicts(module);
 
-      ModuleDefinition externModule = null;
-      string libraryName = null;
-      if (!Options.DisallowExterns) {
-        var args = Attributes.FindExpressions(module.Attributes, "extern");
-        if (args != null) {
-          if (args.Count == 2) {
-            libraryName = (string)(args[1] as StringLiteralExpr)?.Value;
-          }
-
-          externModule = module;
-        }
-      }
+      var externModule = GetExternalModuleFromModule(module, out var libraryName);
 
       if (!ShouldCompileModule(program, module)) {
         DependOnModule(program, module, externModule, libraryName);
@@ -1590,7 +1580,8 @@ 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)) {
@@ -1714,6 +1705,24 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
       enclosingModule = null;
     }
 
+    protected ModuleDefinition GetExternalModuleFromModule(ModuleDefinition module, out string libraryName)
+    {
+      ModuleDefinition externModule = null;
+      libraryName = null;
+      if (!Options.DisallowExterns) {
+        var args = Attributes.FindExpressions(module.Attributes, "extern");
+        if (args != null) {
+          if (args.Count == 2) {
+            libraryName = (string)(args[1] as StringLiteralExpr)?.Value;
+          }
+
+          externModule = module;
+        }
+      }
+
+      return externModule;
+    }
+
     private void DetectAndMarkCapitalizationConflicts(ModuleDefinition module) {
       foreach (TopLevelDecl d in module.TopLevelDecls) {
         if (d is DatatypeDecl datatypeDecl) {

diff --git a/...stFiles/LitTests/LitTest/comp/moduleDatatypeNameCollision/moduleDatatypeNameCollision.dfy b/...stFiles/LitTests/LitTest/comp/moduleDatatypeNameCollision/moduleDatatypeNameCollision.dfy
@@ -1,9 +1,18 @@
 // RUN: %run --target go %s > %t
 // RUN: %diff "%s.expect" "%t"
 
-module DuplicateName {
+module Producer {
   const x := 3 
 }
+module DuplicateName {
+  // Adding an actual import so we can test that we're not breaking that
+  import Producer
+
+  // ProblemModule must come after DuplicateName in the topologic sort, so DuplicateName is compiled before ProblemModule
+  // This way, an import to DuplicateName ends up in ProblemModule, which triggers the bug
+  import ProblemModule
+  const y := Producer.x 
+}
 
 module ProblemModule {
   datatype DuplicateName = DuplicateName
@@ -12,6 +21,6 @@ module ProblemModule {
 import D = DuplicateName
 
 method Main() {
-  print D.x;
+  print D.y;
 }
 
diff --git a/.../LitTests/LitTest/comp/moduleDatatypeNameCollision/moduleDatatypeNameCollision.dfy.expect b/.../LitTests/LitTest/comp/moduleDatatypeNameCollision/moduleDatatypeNameCollision.dfy.expect
@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+3