fix: Escape names of nested modules in C# and Java (dafny-lang#5049)

Fixes dafny-lang#5048. --------- Co-authored-by: Rustan Leino <[email protected]>
Dargones · Feb 9, 2024 · c8e288d · c8e288d
1 parent 693baaf
commit c8e288d
Show file tree

Hide file tree

Showing 6 changed files with 36 additions and 8 deletions.
diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs
@@ -266,9 +266,14 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
       return wr.NewBlock($"public static void _StaticMain(Dafny.ISequence<Dafny.ISequence<{CharTypeName}>> {argsParameterName})");
     }
 
+    string IdProtectModule(string moduleName) {
+      return string.Join(".", moduleName.Split(".").Select(IdProtect));
+    }
+
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
       string libraryName /*?*/, ConcreteSyntaxTree wr) {
-      return wr.NewBlock($"namespace {IdProtect(moduleName)}", " // end of " + $"namespace {IdProtect(moduleName)}");
+      moduleName = IdProtectModule(moduleName);
+      return wr.NewBlock($"namespace {moduleName}", " // end of " + $"namespace {moduleName}");
     }
 
     protected override string GetHelperModuleName() => DafnyHelpersClass;
@@ -1213,7 +1218,11 @@ string DtCtorName(DatatypeCtor ctor) {
       Contract.Ensures(Contract.Result<string>() != null);
 
       var dt = ctor.EnclosingDatatype;
-      var dtName = dt.EnclosingModuleDefinition.TryToAvoidName ? IdName(dt) : dt.GetFullCompileName(Options);
+      var dtName = IdName(dt);
+      if (!dt.EnclosingModuleDefinition.TryToAvoidName) {
+        dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + dtName;
+      }
+
       return dt.IsRecordType ? dtName : dtName + "_" + ctor.GetCompileName(Options);
     }
 
@@ -2472,7 +2481,7 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null,
       if ((cl is DatatypeDecl)
           && !ignoreInterface
           && (member is null || !NeedsCustomReceiver(member))) {
-        return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + DtTypeName(cl, false);
+        return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + DtTypeName(cl, false);
       }
 
       if (cl.EnclosingModuleDefinition.TryToAvoidName) {
@@ -2482,7 +2491,7 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null,
       if (cl.IsExtern(Options, out _, out _)) {
         return cl.EnclosingModuleDefinition.GetCompileName(Options) + "." + cl.GetCompileName(Options);
       }
-      return IdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdProtect(cl.GetCompileName(Options));
+      return IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdProtect(cl.GetCompileName(Options));
     }
 
     protected override void EmitThis(ConcreteSyntaxTree wr, bool callToInheritedMember) {
@@ -2496,7 +2505,7 @@ protected override void EmitThis(ConcreteSyntaxTree wr, bool callToInheritedMemb
 
     protected override void EmitDatatypeValue(DatatypeValue dtv, string typeDescriptorArguments, string arguments, ConcreteSyntaxTree wr) {
       var dt = dtv.Ctor.EnclosingDatatype;
-      var dtName = dt.GetFullCompileName(Options);
+      var dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdName(dt);
 
       var nonGhostInferredTypeArgs = SelectNonGhost(dt, dtv.InferredTypeArgs);
       var typeParams = nonGhostInferredTypeArgs.Count == 0 ? "" : $"<{TypeNames(nonGhostInferredTypeArgs, wr, dtv.tok)}>";

diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
@@ -374,8 +374,13 @@ private void EmitImport(Import import, ConcreteSyntaxTree importWriter) {
       importWriter.WriteLine($"import {import.Path.Replace('/', '.')}.*;");
     }
 
+    string IdProtectModule(string moduleName) {
+      return string.Join(".", moduleName.Split(".").Select(IdProtect));
+    }
+
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
       string libraryName /*?*/, ConcreteSyntaxTree wr) {
+      moduleName = IdProtectModule(moduleName);
       if (isDefault) {
         // Fold the default module into the main module
         moduleName = "_System";
@@ -824,7 +829,7 @@ protected string FullTypeName(UserDefinedType udt, MemberDecl member, bool useCo
       } else if (cl.EnclosingModuleDefinition.GetCompileName(Options) == ModuleName || cl.EnclosingModuleDefinition.TryToAvoidName) {
         return IdProtect(cl.GetCompileName(Options));
       } else {
-        return IdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdProtect(cl.GetCompileName(Options));
+        return IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdProtect(cl.GetCompileName(Options));
       }
     }
 
@@ -2248,7 +2253,7 @@ string DtCtorName(DatatypeCtor ctor) {
       if (dt is TupleTypeDecl tupleDecl) {
         return DafnyTupleClass(tupleDecl.NonGhostDims);
       }
-      var dtName = IdProtect(dt.GetFullCompileName(Options));
+      var dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdName(dt);
       return dt.IsRecordType ? dtName : dtName + "_" + ctor.GetCompileName(Options);
     }
     string DtCreateName(DatatypeCtor ctor) {
@@ -2657,7 +2662,9 @@ protected override void EmitDatatypeValue(DatatypeValue dtv, string typeDescript
 
     void EmitDatatypeValue(DatatypeDecl dt, DatatypeCtor ctor, List<Type> typeArgs, bool isCoCall,
       string typeDescriptorArguments, string arguments, ConcreteSyntaxTree wr) {
-      var dtName = dt is TupleTypeDecl tupleDecl ? DafnyTupleClass(tupleDecl.NonGhostDims) : dt.GetFullCompileName(Options);
+      var dtName = dt is TupleTypeDecl tupleDecl
+        ? DafnyTupleClass(tupleDecl.NonGhostDims)
+        : IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdName(dt);
       var typeParams = typeArgs.Count == 0 ? "" : $"<{BoxedTypeNames(typeArgs, wr, dt.tok)}>";
       var sep = typeDescriptorArguments.Length != 0 && arguments.Length != 0 ? ", " : "";
       if (!isCoCall) {

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5048.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5048.dfy
@@ -0,0 +1,9 @@
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"
+
+module A.try {
+  datatype Dt = Dt
+}
+
+method Main() {
+  print A.try.Dt, "\n";
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5048.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5048.dfy.expect
@@ -0,0 +1 @@
+try.Dt.Dt
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5048.dfy.rs.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5048.dfy.rs.expect
@@ -0,0 +1 @@
+A.try.Dt.Dt
diff --git a/docs/dev/news/5049.fix b/docs/dev/news/5049.fix
@@ -0,0 +1 @@
+Escape names of nested modules in C# and Java