From 16afdc879edbbf204e7780a9da80f665551cb3c7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <MikaelMayer@users.noreply.github.com>
Date: Thu, 23 Jan 2025 19:58:22 -0600
Subject: [PATCH] Fix: --compile-suffix avoids the extra renaming of homonymous
 classes (#6073)

Fixes #6072

### What was changed?
I changed it so that the comparison between the module name and the
class name is done on the C# string, not the Dafny string vs. C# string.

### How has this been tested?
I added a check to ensure that in the generated C# code, the class named
`A` is not escaped when using `--compile-suffix`

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
---
 .../Backends/CSharp/CsharpCodeGenerator.cs         |  2 +-
 .../LitTests/LitTest/git-issues/git-issue-6014.dfy | 14 +++++++++++++-
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
index d8092b8467..3e76ddfc6f 100644
--- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
@@ -270,7 +270,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
     /// </summary>
     private string protectedTypeName(TopLevelDecl dt) {
       var protectedName = IdName(dt);
-      if (dt.EnclosingModuleDefinition is { Name: var moduleName } && moduleName == protectedName) {
+      if (dt.EnclosingModuleDefinition.GetCompileName(Options) == protectedName) {
         return $"_{protectedName}";
       }
       return protectedName;
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy
index b43e78bfeb..dd98f84d14 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6014.dfy
@@ -1,4 +1,13 @@
-// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" 
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"
+// Extra check for the C# compiler with the --compile-suffix option.
+// RUN: %baredafny build -t:cs --compile-suffix "%s"
+// RUN: %OutputCheck --file-to-check "%S/git-issue-6014.cs" "%s"
+// Just to make sure that if we use --compile-suffix, we don't do the escape
+// CHECK: .*A_Compile\.A.*
+// With the class named B_Compile, it becomes B__Compile so there should be no conflict
+// Adding this test in case someone changes the underscore escaping rules to account for this possibility
+// CHECK: .*B_Compile\.B__Compile.*
+
 
 module State {
 
@@ -23,6 +32,9 @@ module Enclosing {
     datatype A = Whatever
   }
 
+  module B {
+    datatype B_Compile = Whatever
+  }
 }
 
 module UsingEnclosing {