Go libray module support (#5140)

### Description
<!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md
-->
<!-- Is this a bug fix for an issue visible in the latest release?
Mention this in the PR details and ensure a patch release is considered
-->
This PR adds support for passing `--go-module-name` flag to the
translate go command to conform to the Go Module project structure.

Example:

CLI:
`dafny translate go --go-module-name MyModule`

It also uses `dtr` files to fetch the right `go-module-name` for
dependencies.


### How has this been tested?
<!-- Tests can be added to
`Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to
`Source/*.Test/…` and run with `dotnet test` -->

Added integration tests which use checked-in DafnyRuntimeGo libs using
the `replace` `go.mod` directive. See the `go-module` directory.

<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>

---------

Co-authored-by: Robin Salkeld <[email protected]>

.github/workflows/integration-tests-reusable.yml

@@ -91,12 +91,12 @@ jobs:
  - name: Set up oldest supported Go
  uses: actions/setup-go@v5
  with:
- go-version: '1.16'
+ go-version: '1.21'
  cache: false
  - name: Set up goimports
  env:
  GO111MODULE: on
- run: go get golang.org/x/tools/cmd/goimports@release-branch.go1.15
+ run: go install golang.org/x/tools/cmd/goimports@latest
  - name: Set up Python
  uses: actions/setup-python@v5
  with: 

.github/workflows/runtime-tests.yml

@@ -33,12 +33,12 @@ jobs:
  - name: Set up Go
  uses: actions/setup-go@v5
  with:
- go-version: '1.16'
+ go-version: '1.21'
  cache: false
  - name: Set up goimports
  env:
  GO111MODULE: on
- run: go get golang.org/x/tools/cmd/goimports@release-branch.go1.15
+ run: go install golang.org/x/tools/cmd/goimports@latest
  - name: Build Dafny
  run: dotnet build Source/Dafny.sln
  - name: Get Z3

.github/workflows/standard-libraries.yml

@@ -32,12 +32,12 @@ jobs:
  - name: Set up Go
  uses: actions/setup-go@v5
  with:
- go-version: '1.16'
+ go-version: '1.21'
  cache: false
  - name: Set up goimports
  env:
  GO111MODULE: on
- run: go get golang.org/x/tools/cmd/goimports@release-branch.go1.15
+ run: go install golang.org/x/tools/cmd/goimports@latest
  - name: Build Dafny
  run: dotnet build Source/Dafny.sln
  - name: Get Z3

Source/DafnyCore/Backends/Cplusplus/CppBackend.cs

@@ -52,11 +52,13 @@ public class CppBackend : ExecutableBackend {
  }
 
  public override Command GetCommand() {
- return new Command(TargetId, $@"Translate Dafny sources to {TargetName} source and build files.
+ var cmd = base.GetCommand();
+ cmd.Description = $@"Translate Dafny sources to {TargetName} source and build files.
 
 This back-end has various limitations (see Docs/Compilation/Cpp.md).
 This includes lack of support for BigIntegers (aka int), most higher order functions,
-and advanced features like traits or co-inductive types.");
+and advanced features like traits or co-inductive types.";
+ return cmd;
  }
 
  public override IReadOnlySet<string> SupportedExtensions => new HashSet<string> { ".h" };

Source/DafnyCore/Backends/GoLang/GoBackend.cs

@@ -1,10 +1,12 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using DafnyCore.Options;
 using Microsoft.Dafny.Compilers;
 
 namespace Microsoft.Dafny;
@@ -16,12 +18,39 @@ public class GoBackend : ExecutableBackend {
  public override string TargetName => "Go";
  public override bool IsStable => true;
  public override string TargetExtension => "go";
- public override string TargetBaseDir(string dafnyProgramName) =>
- $"{Path.GetFileNameWithoutExtension(dafnyProgramName)}-go/src";
+
+ public override string TargetBaseDir(string dafnyProgramName) {
+ var topLevelDir = $"{Path.GetFileNameWithoutExtension(dafnyProgramName)}-go";
+ if (GoModuleMode) {
+ return topLevelDir;
+ }
+
+ return $"{topLevelDir}/src";
+ }
 
  public override bool SupportsInMemoryCompilation => false;
  public override bool TextualTargetIsExecutable => false;
+
+ public bool GoModuleMode { get; set; } = true;
+ public string GoModuleName;
+
+ public static readonly Option<string> GoModuleNameCliOption = new("--go-module-name",
+ @"This Option is used to specify the Go Module Name for the translated code".TrimStart()) {
+ };
+ public override IEnumerable<Option<string>> SupportedOptions => new List<Option<string>> { GoModuleNameCliOption };
+
+ static GoBackend() {
+ TranslationRecord.RegisterLibraryChecks(new Dictionary<Option, OptionCompatibility.OptionCheck> {
+ { GoModuleNameCliOption, OptionCompatibility.NoOpOptionCheck }
+ });
+ }
+
  protected override SinglePassCodeGenerator CreateCodeGenerator() {
+ var goModuleName = Options.Get(GoModuleNameCliOption);
+ GoModuleMode = goModuleName != null;
+ if (GoModuleMode) {
+ GoModuleName = goModuleName;
+ }
  return new GoCodeGenerator(Options, Reporter);
  }
 
@@ -89,6 +118,15 @@ public class GoBackend : ExecutableBackend {
  }
  }
 
+ // Dafny used to compile to the old Go package system only, but Go has moved on to a module
+ // system. Although compiler has moved to new system, it still doesn't generate the go.mod file which
+ // is required by go run. It also supports backwards compatability with GOPATH hence those env variables
+ // are still being used while running in GOPATH mode.
+ if (GoModuleMode) {
+ Reporter.Info(MessageSource.Compiler, Token.Cli, "go build/run skipped in Go Module Mode");
+ return true;
+ }
+
  List<string> goArgs = new();
  if (run) {
  goArgs.Add("run");
@@ -114,6 +152,7 @@ public class GoBackend : ExecutableBackend {
  }
  output = Path.ChangeExtension(dafnyProgramName, extension);
  } else {
+ // This is used when there is no main method but user has invoked dafny run.
  switch (Environment.OSVersion.Platform) {
  case PlatformID.Unix:
  case PlatformID.MacOSX:
@@ -137,8 +176,6 @@ public class GoBackend : ExecutableBackend {
  var psi = PrepareProcessStartInfo("go", goArgs);
 
  psi.EnvironmentVariables["GOPATH"] = GoPath(targetFilename);
- // Dafny compiles to the old Go package system, whereas Go has moved on to a module
- // system. Until Dafny's Go compiler catches up, the GO111MODULE variable has to be set.
  psi.EnvironmentVariables["GO111MODULE"] = "auto";
 
  return 0 == await RunProcess(psi, outputWriter, errorWriter);

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -10,15 +10,27 @@
 using System.Numerics;
 using System.IO;
 using System.Diagnostics.Contracts;
-using System.Collections.ObjectModel;
 using System.Text.RegularExpressions;
+using DafnyCore;
 using JetBrains.Annotations;
+using Tomlyn.Model;
 using static Microsoft.Dafny.ConcreteSyntaxTreeUtils;
 
 namespace Microsoft.Dafny.Compilers {
  class GoCodeGenerator : SinglePassCodeGenerator {
+ //TODO: This is tentative, update this to point to public module once available.
+ private string DafnyRuntimeGoModule = "github.com/dafny-lang/DafnyRuntimeGo/";
+
+ private bool GoModuleMode;
+ private string GoModuleName;
  public GoCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
+ var goModuleName = Options.Get(GoBackend.GoModuleNameCliOption);
+ GoModuleMode = goModuleName != null;
+ if (GoModuleMode) {
+ GoModuleName = goModuleName.ToString();
+ }
  if (Options?.CoverageLegendFile != null) {
+ //TODO: What's the module name for this?
  Imports.Add(new Import { Name = "DafnyProfiling", Path = "DafnyProfiling" });
  }
  }
@@ -47,7 +59,6 @@ class GoCodeGenerator : SinglePassCodeGenerator {
  private string MainModuleName;
  private static List<Import> StandardImports =
  new List<Import> {
- new Import { Name = "_dafny", Path = "dafny" },
  new Import { Name = "os", Path = "os" },
  };
  private static string DummyTypeName = "Dummy__";
@@ -64,15 +75,22 @@ private struct Import {
 
  wr.WriteLine("package {0}", ModuleName);
  wr.WriteLine();
- // Keep the import writers so that we can import subsequent modules into the main one
- EmitImports(wr, out RootImportWriter, out RootImportDummyWriter);
 
+ string path;
  if (Options.IncludeRuntime) {
  EmitRuntimeSource("DafnyRuntimeGo", wr);
+ path = GoModuleMode ? GoModuleName + "/" : "";
+ } else {
+ path = GoModuleMode ? DafnyRuntimeGoModule : "";
  }
+ Imports.Add(new Import { Name = "_dafny", Path = $"{path}dafny" });
+
  if (Options.Get(CommonOptionBag.UseStandardLibraries)) {
  EmitRuntimeSource("DafnyStandardLibraries_go", wr);
  }
+
+ // Keep the import writers so that we can import subsequent modules into the main one
+ EmitImports(wr, out RootImportWriter, out RootImportDummyWriter);
  }
 
  private string DafnyTypeDescriptor => $"{HelperModulePrefix}TypeDescriptor";
@@ -156,6 +174,7 @@ private struct Import {
  }
  }
 
+
  return new Import { Name = moduleName, Path = pkgName, ExternModule = externModule };
  }
 
@@ -167,21 +186,56 @@ private struct Import {
  return wr;
  }
 
+ var goModuleName = GoModuleMode ? GoModuleName + "/" : "";
+ if (moduleName.Equals("_System")) {
+ if (Options.IncludeRuntime) {
+ goModuleName = GoModuleMode ? GoModuleName + "/" : "";
+ } else {
+ goModuleName = GoModuleMode ? DafnyRuntimeGoModule : "";
+ }
+ }
  ModuleName = PublicModuleIdProtect(moduleName);
  var import = CreateImport(ModuleName, isDefault, externModule, libraryName);
-
  var filename = string.Format("{0}/{0}.go", import.Path);
  var w = wr.NewFile(filename);
  EmitModuleHeader(w);
 
+ import.Path = goModuleName + import.Path;
  AddImport(import);
 
  return w;
  }
 
- protected override void DependOnModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ protected override void DependOnModule(Program program, ModuleDefinition module, ModuleDefinition externModule,
  string libraryName) {
- var import = CreateImport(moduleName, isDefault, externModule, libraryName);
+ var goModuleName = "";
+ if (GoModuleMode) {
+ // "_System" module has a special handling because although it gets translated from a Dafny module,
+ // it is still part of the Dafny Runtime lib so has no associated go module name. It either uses the
+ // project module name if embedded or falls back to the Runtime module name.
+ if (module.GetCompileName(Options).Equals("_System")) {
+ if (Options.IncludeRuntime) {
+ goModuleName = GoModuleName + "/";
+ } else {
+ goModuleName = DafnyRuntimeGoModule;
+ }
+ } else {
+ // For every other Dafny Module, fetch the associated go module name from the dtr structure.
+ var translatedRecord = program.Compilation.AlreadyTranslatedRecord;
+ translatedRecord.OptionsByModule.TryGetValue(module.FullDafnyName, out var moduleOptions);
+ object moduleName = null;
+ moduleOptions?.TryGetValue(GoBackend.GoModuleNameCliOption.Name, out moduleName);
+
+ goModuleName = moduleName is string name ? moduleName + "/" : "";
+ if (String.IsNullOrEmpty(goModuleName)) {
+ Reporter.Warning(MessageSource.Compiler, ResolutionErrors.ErrorId.none, Token.Cli,
+ $"Go Module Name not found for the module {module.GetCompileName(Options)}");
+ }
+ }
+ }
+
+ var import = CreateImport(module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName);
+ import.Path = goModuleName + import.Path;
  AddImport(import);
  }
 

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -89,9 +89,9 @@ class PythonCodeGenerator : SinglePassCodeGenerator {
  return file;
  }
 
- protected override void DependOnModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ protected override void DependOnModule(Program program, ModuleDefinition module, ModuleDefinition externModule,
  string libraryName) {
- moduleName = IdProtect(moduleName);
+ var moduleName = IdProtect(module.GetCompileName(Options));
  Imports.Add(moduleName);
  }
 

Source/DafnyCore/Backends/SinglePassCodeGenerator.cs

@@ -12,6 +12,7 @@
 using System.Numerics;
 using System.IO;
 using System.Diagnostics.Contracts;
+using DafnyCore;
 using JetBrains.Annotations;
 using Microsoft.BaseTypes;
 using static Microsoft.Dafny.GeneratorErrors;
@@ -181,7 +182,7 @@ public abstract class SinglePassCodeGenerator {
  /// Indicates the current program depends on the given module without creating it.
  /// Called when a module is out of scope for compilation, such as when using --library.
  /// </summary>
- protected virtual void DependOnModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+ protected virtual void DependOnModule(Program program, ModuleDefinition module, ModuleDefinition externModule,
  string libraryName /*?*/) { }
  protected abstract string GetHelperModuleName();
  protected interface IClassWriter {
@@ -1519,7 +1520,7 @@ public enum ResolvedUnaryOp { BoolNot, BitwiseNot, Cardinality }
  }
 
  if (!module.ShouldCompile(program.Compilation)) {
- DependOnModule(module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName);
+ DependOnModule(program, module, externModule, libraryName);
  return;
  }
 

Source/DafnyCore/DooFile.cs

@@ -10,7 +10,6 @@
 using DafnyCore.Generic;
 using DafnyCore.Options;
 using Microsoft.Dafny;
-using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
 using Tomlyn;
 using Tomlyn.Helpers;
 using Tomlyn.Model;

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -609,6 +609,7 @@ public enum DefaultFunctionOpacityOptions {
  DooFile.RegisterNoChecksNeeded(ExecutionCoverageReport, false);
  DooFile.RegisterNoChecksNeeded(ExtractCounterexample, false);
  DooFile.RegisterNoChecksNeeded(ShowProofObligationExpressions, false);
+ DooFile.RegisterNoChecksNeeded(GoBackend.GoModuleNameCliOption, false);
  }
 }
 

Source/DafnyCore/Options/TranslationRecord.cs

@@ -4,7 +4,6 @@
 using System.Linq;
 using DafnyCore.Generic;
 using Microsoft.Dafny;
-using Microsoft.Dafny.Plugins;
 using Tomlyn;
 
 namespace DafnyCore.Options;
@@ -21,7 +20,6 @@ public class TranslationRecord {
 
  public Dictionary<string, Dictionary<string, object>> OptionsByModule { get; set; }
 
-
  public TranslationRecord(Program program) {
  FileFormatVersion = CurrentFileFormatVersion;
  DafnyVersion = program.Options.VersionNumber;

Source/DafnyCore/Plugins/IExecutableBackend.cs

@@ -112,6 +112,9 @@ public abstract class IExecutableBackend {
  protected ErrorReporter? Reporter;
  protected ReadOnlyCollection<string>? OtherFileNames;
 
+ // The following lists are the Options supported by the backend.
+ public virtual IEnumerable<Option<string>> SupportedOptions => new List<Option<string>>();
+
  protected IExecutableBackend(DafnyOptions options) {
  Options = options;
  }
@@ -213,7 +216,11 @@ public abstract class IExecutableBackend {
  }
 
  public virtual Command GetCommand() {
- return new Command(TargetId, $"Translate Dafny sources to {TargetName} source and build files.");
+ var cmd = new Command(TargetId, $"Translate Dafny sources to {TargetName} source and build files.");
+ foreach (var supportedOption in SupportedOptions) {
+ cmd.AddOption(supportedOption);
+ }
+ return cmd;
  }
 
  public virtual void PopulateCoverageReport(CoverageReport coverageReport) {

Source/DafnyDriver/Commands/BuildCommand.cs

@@ -9,9 +9,9 @@ public static class BuildCommand {
  result.AddArgument(DafnyCommands.FilesArgument);
  foreach (var option in new Option[] {
  CommonOptionBag.Output,
- }.Concat(DafnyCommands.ExecutionOptions).
- Concat(DafnyCommands.ConsoleOutputOptions).
- Concat(DafnyCommands.ResolverOptions)) {
+ }.Concat(DafnyCommands.ExecutionOptions)
+ .Concat(DafnyCommands.ConsoleOutputOptions)
+ .Concat(DafnyCommands.ResolverOptions)) {
  result.AddOption(option);
  }
 

Source/DafnyDriver/Commands/TranslateCommand.cs

@@ -1,6 +1,5 @@
 using System.Collections.Generic;
 using System.CommandLine;
-using DafnyCore;
 using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.Plugins;