[Draft] NET/Java library prefixes

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -191,9 +191,17 @@ public string SanitizedName {
   }
 
   string compileName;
+  bool hasFoundCodeLocationPrefix;
 
   public string GetCompileName(DafnyOptions options) {
-    if (compileName != null) {
+    // The code generator may not have populated its module-name-to-code-location-prefix map
+    //   when this module's compilename is first called.
+    // Until the map has been populated and this module's compile name has the code location prefix,
+    //   it must check to see if the map has been populated.
+    // Even if the current module is not using code location prefixes,
+    //   it may be depending on a module that is,
+    //   and must do this check.
+    if (compileName != null && hasFoundCodeLocationPrefix) {
       return compileName;
     }
 
@@ -204,7 +212,10 @@ public string GetCompileName(DafnyOptions options) {
     var externArgs = options.DisallowExterns ? null : Attributes.FindExpressions(this.Attributes, "extern");
     var nonExternSuffix = (options.Get(CommonOptionBag.AddCompileSuffix) && Name != "_module" && Name != "_System" ? "_Compile" : "");
     if (externArgs != null && 1 <= externArgs.Count && externArgs[0] is StringLiteralExpr) {
-      compileName = (string)((StringLiteralExpr)externArgs[0]).Value;
+      // If compiled with a code location prefix,
+      // prepend it to the extern module name.
+      // Note: this does NOT prepend any outer-module prefix.
+      compileName = options.Backend.MaybePrependModuleNameWithCodeLocationPrefix((string)((StringLiteralExpr)externArgs[0]).Value);
     } else if (externArgs != null) {
       compileName = Name + nonExternSuffix;
     } else {
@@ -217,10 +228,15 @@ public string GetCompileName(DafnyOptions options) {
         // Use an "underscore-escaped" character as a module name separator, since
         // underscores are already used as escape characters in SanitizeName()
         compileName = EnclosingModule.GetCompileName(options) + options.Backend.ModuleSeparator + NonglobalVariable.SanitizeName(Name);
+      } else if (options.Backend.MaybePrependModuleNameWithCodeLocationPrefix(Name) != Name) {
+        // Here, the code generator has a code location prefix for the given module name.
+        // If the code generator has populated its module name to package name map with this module,
+        //   the compileName can now be "cached".
+        hasFoundCodeLocationPrefix = true;
+        compileName = options.Backend.MaybePrependModuleNameWithCodeLocationPrefix(Name);
       } else {
         compileName = NonglobalVariable.SanitizeName(Name);
       }
-
       compileName += nonExternSuffix;
     }
 

Source/DafnyCore/Backends/CSharp/CsharpBackend.cs

@@ -1,13 +1,15 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
+using System.CommandLine;
 using System.IO;
 using System.Linq;
 using System.Reflection;
 using System.Text.Json;
 using System.Threading.Tasks;
 using Microsoft.CodeAnalysis;
 using Microsoft.CodeAnalysis.CSharp;
+using DafnyCore.Options;
 
 namespace Microsoft.Dafny.Compilers;
 
@@ -23,6 +25,15 @@ protected override SinglePassCodeGenerator CreateCodeGenerator() {
   public override bool IsStable => true;
   public override string TargetExtension => "cs";
 
+  public bool NetNamespaceMode { get; set; } = true;
+  public string NetNamespace;
+
+  public static readonly Option<string> NetNamespaceCliOption = new("--dotnet-namespace",
+    @"This Option is used to specify the .NET namespace for the translated code".TrimStart()) {
+  };
+  public override IEnumerable<Option<string>> SupportedOptions => new List<Option<string>> { NetNamespaceCliOption };
+
+
   // True if the most recently visited AST has a method annotated with {:synthesize}:
 
   public override string GetCompileName(bool isDefaultModule, string moduleName, string compileName) {
@@ -164,5 +175,10 @@ public override void PopulateCoverageReport(CoverageReport coverageReport) {
   }
 
   public CsharpBackend(DafnyOptions options) : base(options) {
+    try {
+      TranslationRecord.RegisterLibraryChecks(new Dictionary<Option, OptionCompatibility.OptionCheck> {
+        { NetNamespaceCliOption, OptionCompatibility.NoOpOptionCheck }
+      });
+    } catch ( System.ArgumentException ex) {}
   }
 }

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -22,6 +22,11 @@ namespace Microsoft.Dafny.Compilers {
   public class CsharpCodeGenerator : SinglePassCodeGenerator {
     protected bool Synthesize = false;
 
+    private bool NetNamespaceMode;
+    private string NetNamespace;
+
+    private Dictionary<string, string> moduleToNamespace = new Dictionary<string, string>();
+
     public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
       Feature.SubsetTypeTests,
       Feature.TuplesWiderThan20,
@@ -30,6 +35,11 @@ public class CsharpCodeGenerator : SinglePassCodeGenerator {
     };
 
     public CsharpCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
+      var netNamespace = Options.Get(CsharpBackend.NetNamespaceCliOption);
+      NetNamespaceMode = netNamespace != null;
+      if (NetNamespaceMode) {
+        NetNamespace = netNamespace.ToString();
+      }
     }
 
     const string DafnyISet = "Dafny.ISet";
@@ -65,6 +75,43 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
       }
     }
 
+    protected override void OrganizeModules(Program program, out List<ModuleDefinition> modules) {
+      modules = new List<ModuleDefinition>();
+      foreach (var m in program.CompileModules) {
+        if (!m.IsDefaultModule && !m.Name.Equals("_System")) {
+
+          var translatedRecord = program.Compilation.AlreadyTranslatedRecord;
+          translatedRecord.OptionsByModule.TryGetValue(m.FullDafnyName, out var moduleOptions);
+          object dependencyModuleName = null;
+          moduleOptions?.TryGetValue(CsharpBackend.NetNamespaceCliOption.Name, out dependencyModuleName);
+
+          var dependencyModuleNameStr = (string)dependencyModuleName;
+
+          if (string.IsNullOrEmpty(dependencyModuleNameStr)) {
+            dependencyModuleNameStr = NetNamespace;
+          }
+
+          moduleToNamespace.Add(m.GetCompileName(Options), dependencyModuleNameStr);
+
+          modules.Add(m);
+        }
+      }
+      foreach (var m in program.CompileModules) {
+        if (m.Name.Equals("_System")) {
+          moduleToNamespace.Add(m.GetCompileName(Options), NetNamespace);
+
+          modules.Add(m);
+        }
+      }
+      foreach (var m in program.CompileModules) {
+        if (m.IsDefaultModule) {
+          moduleToNamespace.Add(m.GetCompileName(Options), "dafny_");
+
+          modules.Add(m);
+        }
+      }
+    }
+
     protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);
       wr.WriteLine("// To recompile, you will need the libraries");
@@ -1284,6 +1331,31 @@ void GenerateIsMethod(RedirectingTypeDecl declWithConstraints, ConcreteSyntaxTre
       }
     }
 
+    public override string MaybePrependModuleNameWithCodeLocationPrefix(string moduleName) {
+      var sanitizedName = moduleName.TrimEnd('.');
+
+      // Need to look up prefixes in case of externs.
+      // ex. {:extern "Signature.ECDSA", "Sign"}
+      // moduleName will be `Signature.ECDSA.`
+      // However, there is only a dtr entry for "Signature".
+      // prefixes will be ["Signature", "Signature.ECDSA"],
+      // and the matching prefix will prepend the namespace prefix.
+      var prefixes = sanitizedName.Split('.').Select((s, i) => string.Join(".", sanitizedName.Split('.').Take(i + 1))).ToList();
+
+      foreach (string prefix in prefixes) {
+        if (moduleToNamespace.ContainsKey(prefix)) {
+          // If entry is empty, assume it's in the current module
+          if (string.IsNullOrEmpty(moduleToNamespace[prefix])) {
+            return moduleName;
+          }
+          // Otherwise, prepend the namespace to the moduleName
+          return moduleToNamespace[prefix] + "." + moduleName;
+        }
+      }
+      // In all other cases, return the original moduleName
+      return moduleName;
+    }
+
     void DeclareBoxedNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
       // instance field:  public TargetRepresentation _value;
       var targetTypeName = nt.NativeType == null ? TypeName(nt.BaseType, wr, nt.tok) : GetNativeTypeName(nt.NativeType);

Source/DafnyCore/Backends/ExecutableBackend.cs

@@ -27,6 +27,10 @@ protected ExecutableBackend(DafnyOptions options) : base(options) {
 
   public override string ModuleSeparator => CodeGenerator.ModuleSeparator;
 
+  public override string MaybePrependModuleNameWithCodeLocationPrefix(string moduleName) { 
+    return CodeGenerator.MaybePrependModuleNameWithCodeLocationPrefix(moduleName);
+  }
+
   public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
     ProcessTranslationRecords(dafnyProgram, dafnyProgramName, output);
     CheckInstantiationReplaceableModules(dafnyProgram);

Source/DafnyCore/Backends/ExternExtensions.cs

@@ -21,7 +21,7 @@ public static bool IsExtern(this IAttributeBearingDeclaration declaration, Dafny
           name = externArgs[0].AsStringLiteral();
           return true;
         } else if (externArgs.Count == 2 && externArgs[0] is StringLiteralExpr && externArgs[1] is StringLiteralExpr) {
-          qualification = externArgs[0].AsStringLiteral();
+          qualification = options.Backend.MaybePrependModuleNameWithCodeLocationPrefix(externArgs[0].AsStringLiteral());
           name = externArgs[1].AsStringLiteral();
           return true;
         }

Source/DafnyCore/Backends/Java/JavaBackend.cs

@@ -1,11 +1,13 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using DafnyCore.Options;
 
 namespace Microsoft.Dafny.Compilers;
 
@@ -17,6 +19,16 @@ public class JavaBackend : ExecutableBackend {
   public override bool IsStable => true;
   public override string TargetExtension => "java";
 
+  private bool AddedCliOption = false;
+
+  public bool JavaPackageMode { get; set; } = true;
+  public string JavaPackageName;
+
+  public static readonly Option<string> JavaPackageNameCliOption = new("--java-package-name",
+    @"This Option is used to specify the Java Package Name for the translated code".TrimStart()) {
+  };
+  public override IEnumerable<Option<string>> SupportedOptions => new List<Option<string>> { JavaPackageNameCliOption };
+
   public override string TargetBasename(string dafnyProgramName) =>
     JavaCodeGenerator.TransformToClassName(base.TargetBasename(dafnyProgramName));
 
@@ -34,9 +46,22 @@ public override void CleanSourceDirectory(string sourceDirectory) {
   }
 
   protected override SinglePassCodeGenerator CreateCodeGenerator() {
+    var javaPackageName = Options.Get(JavaPackageNameCliOption);
+    JavaPackageMode = javaPackageName != null;
+    if (JavaPackageMode) {
+      JavaPackageName = javaPackageName;
+    }
     return new JavaCodeGenerator(Options, Reporter);
   }
 
+
+
+  public override string GetCompileName(bool isDefaultModule, string moduleName, string compileName) {
+    return isDefaultModule
+      ? PublicIdProtect(compileName)
+      : base.GetCompileName(isDefaultModule, moduleName, compileName);
+  }
+
   private void EmitRuntimeJar(string targetDirectory) {
     // Since DafnyRuntime.jar is binary, we can't use ReadRuntimeSystem
     var jarName = "DafnyRuntime.jar";
@@ -188,5 +213,14 @@ private static string FindPackageName(string externFilename) {
   private static readonly Regex PackageLine = new Regex(@"^\s*package\s+([a-zA-Z0-9_]+)\s*;$");
 
   public JavaBackend(DafnyOptions options) : base(options) {
+    try {
+      TranslationRecord.RegisterLibraryChecks(new Dictionary<Option, OptionCompatibility.OptionCheck> {
+        { JavaPackageNameCliOption, OptionCompatibility.NoOpOptionCheck }
+      });
+    // JavaBackend, and only JavaBackend, seems to be created multiple times,
+    // resulting in the CLI option being added multiple times,
+    // which throws an exception.
+    // Workaround: Swallow "multiple times" exceptions.
+    } catch ( System.ArgumentException ex) {}
   }
 }