Merge remote-tracking branch 'upstream/master' into verification-cove…

…rage-report

Source/Dafny/Dafny.cs

@@ -4,6 +4,6 @@ namespace Dafny;
 
 public class Dafny {
   public static int Main(string[] args) {
-    return DafnyDriver.Main(args);
+    return DafnyCli.Main(args);
   }
 }

Source/DafnyCore/Compilers/Cplusplus/CppCompilerBackend.cs

@@ -1,11 +1,13 @@
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.IO;
 
 namespace Microsoft.Dafny.Compilers;
 
 public class CppCompilerBackend : ExecutableBackend {
+
   protected override SinglePassCompiler CreateCompiler() {
     return new CppCompiler(Options, Reporter, OtherFileNames);
   }
@@ -47,6 +49,14 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
     return 0 == RunProcess(psi, outputWriter, errorWriter);
   }
 
+  public override Command GetCommand() {
+    return new Command(TargetId, $@"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.");
+  }
+
   public override IReadOnlySet<string> SupportedExtensions => new HashSet<string> { ".h" };
 
   public override string TargetName => "C++";

Source/DafnyCore/Compilers/ExecutableBackend.cs

@@ -13,7 +13,7 @@
 
 namespace Microsoft.Dafny.Compilers;
 
-public abstract class ExecutableBackend : Plugins.IExecutableBackend {
+public abstract class ExecutableBackend : IExecutableBackend {
   // May be null for backends that don't use the single-pass compiler logic
   protected SinglePassCompiler compiler;
 

Source/DafnyCore/Compilers/InternalCompilersPluginConfiguration.cs

@@ -6,7 +6,7 @@ internal class InternalCompilersPluginConfiguration : Plugins.PluginConfiguratio
   public static readonly InternalCompilersPluginConfiguration Singleton = new();
 
   public override IExecutableBackend[] GetCompilers(DafnyOptions options) {
-    return new Plugins.IExecutableBackend[] {
+    return new IExecutableBackend[] {
       new CsharpBackend(options),
       new JavaScriptBackend(options),
       new GoBackend(options),

Source/DafnyCore/DafnyOptions.cs

@@ -44,98 +44,7 @@ public class DafnyOptions : Bpl.CommandLineOptions {
     public DafnyProject DafnyProject { get; set; }
     public Command CurrentCommand { get; set; }
 
-    static DafnyOptions() {
-      RegisterLegacyUi(CommonOptionBag.Target, ParseString, "Compilation options", "compileTarget", @"
-cs (default) - Compile to .NET via C#.
-go - Compile to Go.
-js - Compile to JavaScript.
-java - Compile to Java.
-py - Compile to Python.
-cpp - Compile to C++.
-dfy - Compile to Dafny.
-
-Note that the C++ backend 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.".TrimStart(), "cs");
-
-      RegisterLegacyUi(CommonOptionBag.OptimizeErasableDatatypeWrapper, ParseBoolean, "Compilation options", "optimizeErasableDatatypeWrapper", @"
-0 - Include all non-ghost datatype constructors in the compiled code
-1 (default) - In the compiled target code, transform any non-extern
-    datatype with a single non-ghost constructor that has a single
-    non-ghost parameter into just that parameter. For example, the type
-        datatype Record = Record(x: int)
-    is transformed into just 'int' in the target code.".TrimStart(), defaultValue: true);
-
-      RegisterLegacyUi(CommonOptionBag.Output, ParseFileInfo, "Compilation options", "out");
-      RegisterLegacyUi(CommonOptionBag.UnicodeCharacters, ParseBoolean, "Language feature selection", "unicodeChar", @"
-0 - The char type represents any UTF-16 code unit.
-1 (default) - The char type represents any Unicode scalar value.".TrimStart(), defaultValue: true);
-      RegisterLegacyUi(CommonOptionBag.TypeSystemRefresh, ParseBoolean, "Language feature selection", "typeSystemRefresh", @"
-0 (default) - The type-inference engine and supported types are those of Dafny 4.0.
-1 - Use an updated type-inference engine. Warning: This mode is under construction and probably won't work at this time.".TrimStart(), defaultValue: false);
-      RegisterLegacyUi(CommonOptionBag.GeneralTraits, ParseGeneralTraitsOption, "Language feature selection", "generalTraits", @"
-legacy (default) - Every trait implicitly extends 'object', and thus is a reference type. Only traits and reference types can extend traits.
-datatype - A trait is a reference type only if it or one of its ancestor traits is 'object'. Any non-'newtype' type with members can extend traits.
-full - (don't use; not yet completely supported) A trait is a reference type only if it or one of its ancestor traits is 'object'. Any type with members can extend traits.".TrimStart(),
-        CommonOptionBag.GeneralTraitsOptions.Legacy);
-      RegisterLegacyUi(CommonOptionBag.TypeInferenceDebug, ParseBoolean, "Language feature selection", "titrace", @"
-0 (default) - Don't print type-inference debug information.
-1 - Print type-inference debug information.".TrimStart(), defaultValue: false);
-      RegisterLegacyUi(CommonOptionBag.NewTypeInferenceDebug, ParseBoolean, "Language feature selection", "ntitrace", @"
-0 (default) - Don't print debug information for the new type system.
-1 - Print debug information for the new type system.".TrimStart(), defaultValue: false);
-      RegisterLegacyUi(CommonOptionBag.Plugin, ParseStringElement, "Plugins", defaultValue: new List<string>());
-      RegisterLegacyUi(CommonOptionBag.Prelude, ParseFileInfo, "Input configuration", "dprelude");
-
-      RegisterLegacyUi(CommonOptionBag.Libraries, ParseFileInfoElement, "Compilation options", defaultValue: new List<FileInfo>());
-      RegisterLegacyUi(DeveloperOptionBag.ResolvedPrint, ParseString, "Overall reporting and printing", "rprint");
-      RegisterLegacyUi(DeveloperOptionBag.Print, ParseString, "Overall reporting and printing", "dprint");
-
-      RegisterLegacyUi(DafnyConsolePrinter.ShowSnippets, ParseBoolean, "Overall reporting and printing", "showSnippets", @"
-0 (default) - Don't show source code snippets for Dafny messages.
-1 - Show a source code snippet for each Dafny message.".TrimStart());
-
-      RegisterLegacyUi(Microsoft.Dafny.Printer.PrintMode, ParsePrintMode, "Overall reporting and printing", "printMode", legacyDescription: @"
-Everything (default) - Print everything listed below.
-DllEmbed - print the source that will be included in a compiled dll.
-NoIncludes - disable printing of {:verify false} methods
-    incorporated via the include mechanism, as well as datatypes and
-    fields included from other files.
-NoGhost - disable printing of functions, ghost methods, and proof
-    statements in implementation methods. It also disables anything
-    NoIncludes disables.".TrimStart(),
-        argumentName: "Everything|DllEmbed|NoIncludes|NoGhost",
-        defaultValue: PrintModes.Everything);
-
-      RegisterLegacyUi(CommonOptionBag.DefaultFunctionOpacity, ParseDefaultFunctionOpacity, "Language feature selection", "defaultFunctionOpacity", null);
-
-      void ParsePrintMode(Option<PrintModes> option, Bpl.CommandLineParseState ps, DafnyOptions options) {
-        if (ps.ConfirmArgumentCount(1)) {
-          if (ps.args[ps.i].Equals("Everything")) {
-            options.Set(option, PrintModes.Everything);
-          } else if (ps.args[ps.i].Equals("NoIncludes")) {
-            options.Set(option, PrintModes.NoIncludes);
-          } else if (ps.args[ps.i].Equals("NoGhost")) {
-            options.Set(option, PrintModes.NoGhost);
-          } else if (ps.args[ps.i].Equals("DllEmbed")) {
-            // This is called DllEmbed because it was previously only used inside Dafny-compiled .dll files for C#,
-            // but it is now used by the LibraryBackend when building .doo files as well. 
-            options.Set(option, PrintModes.Serialization);
-          } else {
-            InvalidArgumentError(option.Name, ps);
-          }
-        }
-      }
-
-      RegisterLegacyUi(CommonOptionBag.AddCompileSuffix, ParseBoolean, "Compilation options", "compileSuffix");
-
-      RegisterLegacyUi(CommonOptionBag.ReadsClausesOnMethods, 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);
-    }
-
-    private static void ParseDefaultFunctionOpacity(Option<CommonOptionBag.DefaultFunctionOpacityOptions> option, Bpl.CommandLineParseState ps, DafnyOptions options) {
+    public static void ParseDefaultFunctionOpacity(Option<CommonOptionBag.DefaultFunctionOpacityOptions> option, Bpl.CommandLineParseState ps, DafnyOptions options) {
       if (ps.ConfirmArgumentCount(1)) {
         if (ps.args[ps.i].Equals("transparent")) {
           options.Set(option, CommonOptionBag.DefaultFunctionOpacityOptions.Transparent);
@@ -219,7 +128,7 @@ public static void ParseBoolean(Option<bool> option, Bpl.CommandLineParseState p
       }
     }
 
-    private static void ParseGeneralTraitsOption(Option<CommonOptionBag.GeneralTraitsOptions> option, Bpl.CommandLineParseState ps, DafnyOptions options) {
+    public static void ParseGeneralTraitsOption(Option<CommonOptionBag.GeneralTraitsOptions> option, Bpl.CommandLineParseState ps, DafnyOptions options) {
       if (ps.ConfirmArgumentCount(1)) {
         switch (ps.args[ps.i]) {
           case "legacy":
@@ -344,8 +253,6 @@ public enum ContractTestingMode {
     public List<string> DafnyPrintExportedViews = new List<string>();
     public bool Compile = true;
     public List<string> MainArgs = new List<string>();
-    public Command Command = null;
-    public bool Format = false;
     public bool FormatCheck = false;
 
     public string CompilerName;
@@ -413,13 +320,13 @@ public enum IncludesModes {
     public static readonly ReadOnlyCollection<Plugin> DefaultPlugins =
       new(new[] { SinglePassCompiler.Plugin, InternalDocstringRewritersPluginConfiguration.Plugin });
     private IList<Plugin> cliPluginCache;
-    public IList<Plugin> Plugins => cliPluginCache ??= ComputePlugins();
+    public IList<Plugin> Plugins => cliPluginCache ??= ComputePlugins(AdditionalPlugins, AdditionalPluginArguments);
     public List<Plugin> AdditionalPlugins = new();
     public IList<string> AdditionalPluginArguments = new List<string>();
 
-    IList<Plugin> ComputePlugins() {
-      var result = new List<Plugin>(DefaultPlugins.Concat(AdditionalPlugins));
-      foreach (var pluginAndArgument in AdditionalPluginArguments) {
+    public static IList<Plugin> ComputePlugins(List<Plugin> additionalPlugins, IList<string> allArguments) {
+      var result = new List<Plugin>(DefaultPlugins.Concat(additionalPlugins));
+      foreach (var pluginAndArgument in allArguments) {
         try {
           var pluginArray = pluginAndArgument.Split(',');
           var pluginPath = pluginArray[0];
@@ -498,7 +405,7 @@ protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) {
       return ParseBoogieOption(name, ps);
     }
 
-    protected bool ParseBoogieOption(string name, Bpl.CommandLineParseState ps) {
+    private bool ParseBoogieOption(string name, Bpl.CommandLineParseState ps) {
       return base.ParseOption(name, ps);
     }
 
@@ -863,7 +770,7 @@ private static string[] ParseInnerArguments(string argumentsString) {
       ).ToArray();
     }
 
-    protected static void InvalidArgumentError(string name, Bpl.CommandLineParseState ps) {
+    public static void InvalidArgumentError(string name, Bpl.CommandLineParseState ps) {
       ps.Error("Invalid argument \"{0}\" to option {1}", ps.args[ps.i], name);
     }
 

Source/DafnyCore/DooFile.cs

@@ -208,7 +208,7 @@ public static bool CheckOptionMatches(DafnyOptions options, Option option, objec
       return true;
     }
 
-    options.Printer.ErrorWriteLine(Console.Out, $"*** Error: Cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
+    options.Printer.ErrorWriteLine(options.OutputWriter, $"*** Error: Cannot load {libraryFile}: --{option.Name} is set locally to {OptionValueToString(option, localValue)}, but the library was built with {OptionValueToString(option, libraryValue)}");
     return false;
   }