feat: Translation records (#5346)

Source/AutoExtern.Test/Tutorial/ClientApp/GroceryListPrinter.dfy.expect

@@ -2,6 +2,7 @@ Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help
 
 Dafny program verifier did not attempt verification
 Wrote textual form of target program to GroceryListPrinter.cs
+Additional output written to GroceryListPrinter-cs.dtr
 # Printing a grocery list
  (2 items in the list)
 ## Apple: 3 @ 1.00

Source/DafnyCore/AST/CompilationData.cs

@@ -1,5 +1,6 @@
 using System;
 using System.Collections.Generic;
+using DafnyCore.Options;
 
 namespace Microsoft.Dafny;
 
@@ -28,4 +29,6 @@ public class CompilationData {
  // TODO move to DocumentAfterParsing once that's used by the CLI
  [FilledInDuringResolution]
  public ISet<Uri> UrisToCompile;
+
+ public TranslationRecord AlreadyTranslatedRecord { get; set; }
 }

Source/DafnyCore/AST/Members/Method.cs

@@ -4,6 +4,7 @@
 using System.Linq;
 using System.Numerics;
 using DafnyCore;
+using DafnyCore.Options;
 using Microsoft.Dafny.Auditor;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
@@ -20,7 +21,7 @@ public class Method : MethodOrFunction, TypeParameter.ParentType,
  DafnyOptions.RegisterLegacyUi(ReadsClausesOnMethods, DafnyOptions.ParseBoolean, "Language feature selection", "readsClausesOnMethods", @"
 0 (default) - Reads clauses on methods are forbidden.
 1 - Reads clauses on methods are permitted (with a default of 'reads *').".TrimStart(), defaultValue: false);
- DooFile.RegisterLibraryCheck(ReadsClausesOnMethods, DooFile.CheckOptionLocalImpliesLibrary);
+ DooFile.RegisterLibraryCheck(ReadsClausesOnMethods, OptionCompatibility.CheckOptionLocalImpliesLibrary);
  }
 
  public override IEnumerable<INode> Children => new Node[] { Body, Decreases }.Where(x => x != null).

Source/DafnyCore/AST/Members/MethodOrFunction.cs

@@ -2,6 +2,7 @@
 using System.CommandLine;
 using System.Linq;
 using DafnyCore;
+using DafnyCore.Options;
 
 namespace Microsoft.Dafny;
 
@@ -10,7 +11,7 @@ public abstract class MethodOrFunction : MemberDecl {
  "Allow exporting callables with preconditions, and importing callables with postconditions");
 
  static MethodOrFunction() {
- DooFile.RegisterLibraryCheck(AllowExternalContracts, DooFile.CheckOptionLibraryImpliesLocal);
+ DooFile.RegisterLibraryCheck(AllowExternalContracts, OptionCompatibility.CheckOptionLibraryImpliesLocal);
  }
 
  public readonly List<TypeParameter> TypeArgs;

Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs

@@ -3,6 +3,7 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using DafnyCore;
+using DafnyCore.Options;
 
 namespace Microsoft.Dafny;
 
@@ -17,8 +18,8 @@ public class PrintStmt : Statement, ICloneable<PrintStmt>, ICanFormat {
  });
 
  DooFile.RegisterLibraryChecks(
- checks: new Dictionary<Option, DooFile.OptionCheck> {
- { TrackPrintEffectsOption, DooFile.CheckOptionLocalImpliesLibrary }
+ checks: new Dictionary<Option, OptionCompatibility.OptionCheck> {
+ { TrackPrintEffectsOption, OptionCompatibility.CheckOptionLocalImpliesLibrary }
  });
  }
 

Source/DafnyCore/Backends/DafnyExecutableBackend.cs

@@ -31,9 +31,11 @@ public abstract class DafnyExecutableBackend : ExecutableBackend {
  DafnyCodeGenerator = CreateDafnyWrittenCompiler();
  }
 
- public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
+ public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
+ ProcessTranslationRecords(dafnyProgram, dafnyProgramName, output);
  CheckInstantiationReplaceableModules(dafnyProgram);
  ProcessOuterModules(dafnyProgram);
+
  ((DafnyCodeGenerator)codeGenerator).Start();
  codeGenerator.Compile(dafnyProgram, new ConcreteSyntaxTree());
  var dast = ((DafnyCodeGenerator)codeGenerator).Build();

Source/DafnyCore/Backends/ExecutableBackend.cs

@@ -6,6 +6,7 @@
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
+using DafnyCore.Options;
 using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.Plugins;
 
@@ -25,12 +26,33 @@ public abstract class ExecutableBackend : IExecutableBackend {
 
  public override string ModuleSeparator => CodeGenerator.ModuleSeparator;
 
- public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
+ public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
+ ProcessTranslationRecords(dafnyProgram, dafnyProgramName, output);
  CheckInstantiationReplaceableModules(dafnyProgram);
  ProcessOuterModules(dafnyProgram);
+
  CodeGenerator.Compile(dafnyProgram, output);
  }
 
+ protected void ProcessTranslationRecords(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
+ // Process --translation-record options, since translation may need that data to translate correctly.
+ dafnyProgram.Compilation.AlreadyTranslatedRecord = TranslationRecord.Empty(dafnyProgram);
+ var records = dafnyProgram.Options.Get(TranslationRecords);
+ if (records != null) {
+ foreach (var path in records) {
+ TranslationRecord.ReadValidateAndMerge(dafnyProgram, path.FullName, Token.Cli);
+ }
+ }
+
+ // Write out the translation record for THIS translation before compiling,
+ // in case the compilation process mutates the program.
+ var translationRecord = new TranslationRecord(dafnyProgram);
+ var baseName = Path.GetFileNameWithoutExtension(dafnyProgramName);
+ var dtrFilePath = dafnyProgram.Options.Get(TranslationRecordOutput)?.FullName ?? $"{baseName}-{TargetId}.dtr";
+ var dtrWriter = output.NewFile(dtrFilePath);
+ translationRecord.Write(dtrWriter);
+ }
+
  protected void CheckInstantiationReplaceableModules(Program dafnyProgram) {
  foreach (var compiledModule in dafnyProgram.Modules()) {
  if (compiledModule.Implements is { Kind: ImplementationKind.Replacement }) {
@@ -50,17 +72,27 @@ public abstract class ExecutableBackend : IExecutableBackend {
  }
 
  protected void ProcessOuterModules(Program dafnyProgram) {
- var outerModules = GetOuterModules();
- ModuleDefinition rootUserModule = null;
- foreach (var outerModule in outerModules) {
- var newRoot = new ModuleDefinition(RangeToken.NoToken, new Name(outerModule), new List<IToken>(),
- ModuleKindEnum.Concrete, false,
- null, null, null);
- newRoot.EnclosingModule = rootUserModule;
- rootUserModule = newRoot;
+ // Apply the --outer-module option from any translation records for libraries,
+ // but only to top-level modules.
+ var outerModules = new Dictionary<string, ModuleDefinition>();
+ foreach (var module in dafnyProgram.CompileModules) {
+ if (module.EnclosingModule is not DefaultModuleDefinition) {
+ continue;
+ }
+
+ var recordedOuterModuleName = (string)dafnyProgram.Compilation.AlreadyTranslatedRecord.Get(null, module.FullDafnyName, OuterModule);
+ if (recordedOuterModuleName == null) {
+ continue;
+ }
+
+ var outerModule = outerModules.GetOrCreate(recordedOuterModuleName, () => CreateOuterModule(recordedOuterModuleName));
+ module.EnclosingModule = outerModule;
  }
 
- if (rootUserModule != null) {
+ // Apply the local --output-module option if there is one
+ var outerModuleName = Options.Get(OuterModule);
+ if (outerModuleName != null) {
+ var rootUserModule = outerModules.GetOrCreate(outerModuleName, () => CreateOuterModule(outerModuleName));
  dafnyProgram.DefaultModuleDef.NameNode = rootUserModule.NameNode;
  dafnyProgram.DefaultModuleDef.EnclosingModule = rootUserModule.EnclosingModule;
  }
@@ -70,6 +102,22 @@ public abstract class ExecutableBackend : IExecutableBackend {
  }
  }
 
+ private static ModuleDefinition CreateOuterModule(string moduleName) {
+ var outerModules = moduleName.Split(".");
+
+ ModuleDefinition module = null;
+ foreach (var outerModule in outerModules) {
+ var thisModule = new ModuleDefinition(RangeToken.NoToken, new Name(outerModule), new List<IToken>(),
+ ModuleKindEnum.Concrete, false,
+ null, null, null) {
+ EnclosingModule = module
+ };
+ module = thisModule;
+ }
+
+ return module;
+ }
+
  public override void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection<string> otherFileNames) {
  base.OnPreCompile(reporter, otherFileNames);
  codeGenerator = CreateCodeGenerator();

Source/DafnyCore/Backends/Library/LibraryBackend.cs

@@ -52,7 +52,7 @@ public class LibraryBackend : ExecutableBackend {
  throw new NotSupportedException();
  }
 
- public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
+ public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
  if (!Options.UsingNewCli) {
  throw new UnsupportedFeatureException(dafnyProgram.GetStartOfFirstFileToken(), Feature.LegacyCLI);
  }

Source/DafnyCore/DooFile.cs

@@ -8,6 +8,7 @@
 using System.Text;
 using System.Threading.Tasks;
 using DafnyCore.Generic;
+using DafnyCore.Options;
 using Microsoft.Dafny;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
 using Tomlyn;
@@ -48,7 +49,7 @@ public class ManifestData {
 
  Options = new Dictionary<string, object>();
  foreach (var (option, _) in OptionChecks) {
- var optionValue = GetOptionValue(options, option);
+ var optionValue = options.Get((dynamic)option);
  Options.Add(option.Name, optionValue);
  }
  }
@@ -173,7 +174,8 @@ public class ManifestData {
  }
 
  result.Options.OptionArguments[option] = libraryValue;
- success = success && check(reporter, origin, option, localValue, options.GetPrintPath(libraryFile), libraryValue);
+ var prefix = $"cannot load {options.GetPrintPath(libraryFile)}";
+ success = success && check(reporter, origin, prefix, option, localValue, libraryValue);
  }
 
  if (!success) {
@@ -183,25 +185,6 @@ public class ManifestData {
  return result;
  }
 
- private static object GetOptionValue(DafnyOptions options, Option option) {
- // This is annoyingly necessary because only DafnyOptions.Get<T>(Option<T> option)
- // handles falling back to the configured default option value,
- // whereas the non-generic DafnyOptions.Get(Option option) doesn't.
- // TODO: Move somewhere more generic if this is useful in other cases?
- var optionType = option.ValueType;
- if (optionType == typeof(bool)) {
- return options.Get((Option<bool>)option);
- }
- if (optionType == typeof(string)) {
- return options.Get((Option<string>)option);
- }
- if (optionType == typeof(IEnumerable<string>)) {
- return options.Get((Option<IEnumerable<string>>)option);
- }
-
- throw new ArgumentException();
- }
-
  public void Write(ConcreteSyntaxTree wr) {
  var manifestWr = wr.NewFile(ManifestFileEntry);
  using var manifestWriter = new StringWriter();
@@ -237,88 +220,17 @@ public class ManifestData {
  // more difficult to completely categorize, which is the main reason the LibraryBackend
  // is restricted to only the new CLI.
 
- public delegate bool OptionCheck(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue);
- private static readonly Dictionary<Option, OptionCheck> OptionChecks = new();
+ private static readonly Dictionary<Option, OptionCompatibility.OptionCheck> OptionChecks = new();
  private static readonly HashSet<Option> NoChecksNeeded = new();
 
- public static bool CheckOptionMatches(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue) {
- if (OptionValuesEqual(option, localValue, libraryValue)) {
- return true;
- }
-
- reporter.Error(MessageSource.Project, origin,
- $"cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, " +
- $"but the library was built with {OptionValueToString(option, libraryValue)}");
- return false;
- }
-
- /// Checks that the library option ==> the local option.
- /// E.g. --no-verify: the only incompatibility is if it's on in the library but not locally.
- /// Generally the right check for options that weaken guarantees.
- public static bool CheckOptionLibraryImpliesLocal(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue) {
- if (OptionValuesImplied(libraryValue, localValue)) {
- return true;
- }
-
- reporter.Error(MessageSource.Project, origin, $"cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
- return false;
- }
-
- /// Checks that the local option ==> the library option.
- /// E.g. --track-print-effects: the only incompatibility is if it's on locally but not in the library.
- /// Generally the right check for options that strengthen guarantees.
- public static bool CheckOptionLocalImpliesLibrary(ErrorReporter reporter, IToken origin, Option option, object localValue, string libraryFile, object libraryValue) {
- if (OptionValuesImplied(localValue, libraryValue)) {
- return true;
- }
- reporter.Error(MessageSource.Project, origin, LocalImpliesLibraryMessage(option, localValue, libraryFile, libraryValue));
- return false;
- }
-
- public static string LocalImpliesLibraryMessage(Option option, object localValue, string libraryFile, object libraryValue) {
- return $"cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}";
- }
-
- private static bool OptionValuesEqual(Option option, object first, object second) {
- if (first.Equals(second)) {
- return true;
- }
-
- if (option.ValueType == typeof(IEnumerable<string>)) {
- return ((IEnumerable<string>)first).SequenceEqual((IEnumerable<string>)second);
- }
-
- return false;
- }
-
- public static bool OptionValuesImplied(object first, object second) {
- try {
- return !(bool)first || (bool)second;
- } catch (NullReferenceException) {
- throw new Exception("Comparing options of Doo files created by different Dafny builds. You are probably using a locally built Dafny that has the same version as a different built.");
- }
- }
-
- private static string OptionValueToString(Option option, object value) {
- if (option.ValueType == typeof(IEnumerable<string>)) {
- var values = (IEnumerable<string>)value;
- return $"[{string.Join(',', values)}]";
- }
-
- if (value == null) {
- return "a version of Dafny that does not have this option";
- }
- return value.ToString();
- }
-
- public static void RegisterLibraryCheck(Option option, OptionCheck check) {
+ public static void RegisterLibraryCheck(Option option, OptionCompatibility.OptionCheck check) {
  if (NoChecksNeeded.Contains(option)) {
  throw new ArgumentException($"Option already registered as not needing a library check: {option.Name}");
  }
  OptionChecks.Add(option, check);
  }
 
- public static void RegisterLibraryChecks(IDictionary<Option, OptionCheck> checks) {
+ public static void RegisterLibraryChecks(IDictionary<Option, OptionCompatibility.OptionCheck> checks) {
  foreach (var (option, check) in checks) {
  RegisterLibraryCheck(option, check);
  }

Source/DafnyCore/Options/BoogieOptionBag.cs

@@ -5,6 +5,7 @@
 using System.Linq;
 using System.Transactions;
 using DafnyCore;
+using DafnyCore.Options;
 using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
@@ -138,9 +139,9 @@ public static class BoogieOptionBag {
 
 
  DooFile.RegisterLibraryChecks(
- new Dictionary<Option, DooFile.OptionCheck> {
- { BoogieArguments, DooFile.CheckOptionMatches },
- { NoVerify, DooFile.CheckOptionLibraryImpliesLocal },
+ new Dictionary<Option, OptionCompatibility.OptionCheck> {
+ { BoogieArguments, OptionCompatibility.CheckOptionMatches },
+ { NoVerify, OptionCompatibility.CheckOptionLibraryImpliesLocal },
  }
  );
  DooFile.RegisterNoChecksNeeded(

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -3,6 +3,7 @@
 using System.IO;
 using System.Linq;
 using DafnyCore;
+using DafnyCore.Options;
 using Serilog.Events;
 
 namespace Microsoft.Dafny;
@@ -579,16 +580,16 @@ public enum DefaultFunctionOpacityOptions {
  });
 
  DooFile.RegisterLibraryChecks(
- new Dictionary<Option, DooFile.OptionCheck>() {
- { UnicodeCharacters, DooFile.CheckOptionMatches },
- { EnforceDeterminism, DooFile.CheckOptionLocalImpliesLibrary },
- { RelaxDefiniteAssignment, DooFile.CheckOptionLibraryImpliesLocal },
- { AllowAxioms, DooFile.CheckOptionLibraryImpliesLocal },
- { AllowWarnings, (reporter, origin, option, localValue, libraryFile, libraryValue) => {
- if (DooFile.OptionValuesImplied(libraryValue, localValue)) {
+ new Dictionary<Option, OptionCompatibility.OptionCheck>() {
+ { UnicodeCharacters, OptionCompatibility.CheckOptionMatches },
+ { EnforceDeterminism, OptionCompatibility.CheckOptionLocalImpliesLibrary },
+ { RelaxDefiniteAssignment, OptionCompatibility.CheckOptionLibraryImpliesLocal },
+ { AllowAxioms, OptionCompatibility.CheckOptionLibraryImpliesLocal },
+ { AllowWarnings, (reporter, origin, prefix, option, localValue, libraryValue) => {
+ if (OptionCompatibility.OptionValuesImplied(libraryValue, localValue)) {
  return true;
  }
- string message = DooFile.LocalImpliesLibraryMessage(option, localValue, libraryFile, libraryValue);
+ string message = OptionCompatibility.LocalImpliesLibraryMessage(prefix, option, localValue, libraryValue);
  reporter.Warning(MessageSource.Project, ResolutionErrors.ErrorId.none, origin, message);
  return false;
  }