From c8e288dc43a00d52c4ee679abc04887b06ffa3ad Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 9 Feb 2024 21:17:01 +0100 Subject: [PATCH] fix: Escape names of nested modules in C# and Java (#5049) Fixes #5048. --------- Co-authored-by: Rustan Leino --- .../Compilers/CSharp/Compiler-Csharp.cs | 19 ++++++++++++++----- .../DafnyCore/Compilers/Java/Compiler-java.cs | 13 ++++++++++--- .../LitTest/git-issues/git-issue-5048.dfy | 9 +++++++++ .../git-issues/git-issue-5048.dfy.expect | 1 + .../git-issues/git-issue-5048.dfy.rs.expect | 1 + docs/dev/news/5049.fix | 1 + 6 files changed, 36 insertions(+), 8 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5048.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5048.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5048.dfy.rs.expect create mode 100644 docs/dev/news/5049.fix diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs index 42827684967..5c2d90c1abd 100644 --- 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> {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() != 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 index e166717d4f9..539ff1ef470 100644 --- 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 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 new file mode 100644 index 00000000000..8de0259104b --- /dev/null +++ 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 new file mode 100644 index 00000000000..154455f20d5 --- /dev/null +++ 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 new file mode 100644 index 00000000000..aa161fe8ea1 --- /dev/null +++ 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 new file mode 100644 index 00000000000..dab5ebee68f --- /dev/null +++ b/docs/dev/news/5049.fix @@ -0,0 +1 @@ +Escape names of nested modules in C# and Java