Add several new-style command-line options (#3568)

* `--error-limit` is available everywhere
* `--solver-log` is available for `verify` and `measure-complexity`
* `--solver-plugin` is available for `verify` and `measure-complexity`
* `--resource-limit` is available for `verify` and `measure-complexity`
* `--isolate-assertions` and `--format` are also available for `verify` with `--format` renamed `--log-format`

Addresses #3468

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT
license.

Co-authored-by: David Cok <david.r.cok@gmail.com>

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -2,11 +2,15 @@
 using System.CommandLine;
 using System.IO;
 using System.Linq;
+using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
 
 public class CommonOptionBag {
 
+  public static readonly Option<int> ErrorLimit =
+    new("--error-limit", () => 5, "Set the maximum number of errors to report (0 for unlimited).");
+
   public static readonly Option<bool> ManualLemmaInduction =
     new("--manual-lemma-induction", "Turn off automatic induction for lemmas.");
 
@@ -45,6 +49,21 @@ datatype with a single non-ghost constructor that has a single
     "Allow variables to be read before they are assigned, but only if they have an auto-initializable type or if they are ghost and have a nonempty type.") {
   };
 
+  public static readonly Option<bool> IsolateAssertions = new("--isolate-assertions", @"Verify each assertion in isolation.");
+
+  public static readonly Option<List<string>> VerificationLogFormat = new("--log-format", $@"
+Logs verification results using the given test result format. The currently supported formats are `trx`, `csv`, and `text`. These are: the XML-based format commonly used for test results for .NET languages, a custom CSV schema, and a textual format meant for human consumption. You can provide configuration using the same string format as when using the --logger option for dotnet test, such as: --format ""trx;LogFileName=<...>"");
+
+The `trx` and `csv` formats automatically choose an output file name by default, and print the name of this file to the console. The `text` format prints its output to the console by default, but can send output to a file given the `LogFileName` option.
+
+The `text` format also includes a more detailed breakdown of what assertions appear in each assertion batch. When combined with the {CommonOptionBag.IsolateAssertions.Name} option, it will provide approximate time and resource use costs for each assertion, allowing identification of especially expensive assertions.".TrimStart()) {
+    ArgumentHelpName = "configuration"
+  };
+
+  public static readonly Option<uint> SolverResourceLimit = new("--resource-limit", @"Specify the maximum resource limit (rlimit) value to pass to Z3. Multiplied by 1000 before sending to Z3.");
+  public static readonly Option<string> SolverPlugin = new("--solver-plugin", @"Specify a plugin to use to solve verification conditions (instead of an external Z3 process).");
+  public static readonly Option<string> SolverLog = new("--solver-log", @"Specify a file to use to log the SMT-Lib text sent to the solver.");
+
   public static readonly Option<IList<string>> Libraries = new("--library",
     @"
 The contents of this file and any files it includes can be referenced from other files as if they were included. 
@@ -164,6 +183,7 @@ static CommonOptionBag() {
     DafnyOptions.RegisterLegacyBinding(WarnMissingConstructorParenthesis,
       (options, value) => { options.DisallowConstructorCaseWithoutParentheses = value; });
     DafnyOptions.RegisterLegacyBinding(WarningAsErrors, (options, value) => { options.WarningsAsErrors = value; });
+    DafnyOptions.RegisterLegacyBinding(ErrorLimit, (options, value) => { options.ErrorLimit = value; });
     DafnyOptions.RegisterLegacyBinding(VerifyIncludedFiles,
       (options, value) => { options.VerifyAllModules = value; });
 
@@ -197,6 +217,18 @@ static CommonOptionBag() {
 
     DafnyOptions.RegisterLegacyBinding(Verbose, (o, v) => o.CompileVerbose = v);
     DafnyOptions.RegisterLegacyBinding(DisableNonLinearArithmetic, (o, v) => o.DisableNLarith = v);
+
+    DafnyOptions.RegisterLegacyBinding(VerificationLogFormat, (o, v) => o.VerificationLoggerConfigs = v);
+    DafnyOptions.RegisterLegacyBinding(IsolateAssertions, (o, v) => o.VcsSplitOnEveryAssert = v);
+    DafnyOptions.RegisterLegacyBinding(SolverResourceLimit, (o, v) => o.ResourceLimit = v);
+    DafnyOptions.RegisterLegacyBinding(SolverPlugin, (o, v) => {
+      if (v is not null) {
+        o.ProverDllName = v;
+        o.TheProverFactory = ProverFactory.Load(o.ProverDllName);
+      }
+    });
+    DafnyOptions.RegisterLegacyBinding(SolverLog, (o, v) => o.ProverLogFilePath = v);
+
     DafnyOptions.RegisterLegacyBinding(EnforceDeterminism, (options, value) => {
       options.ForbidNondeterminism = value;
       options.DefiniteAssignmentLevel = 4;

Source/DafnyCore/Options/ICommandSpec.cs

@@ -18,21 +18,24 @@ static ICommandSpec() {
 
   public static IEnumerable<Option> FormatOptions => new Option[] {
     CommonOptionBag.Check,
-    CommonOptionBag.StdIn,
     CommonOptionBag.Verbose,
     CommonOptionBag.FormatPrint,
     DeveloperOptionBag.UseBaseFileName
   }.Concat(ParserOptions);
 
   public static IReadOnlyList<Option> VerificationOptions = new Option[] {
-    CommonOptionBag.StdIn,
     CommonOptionBag.RelaxDefiniteAssignment,
     BoogieOptionBag.VerificationTimeLimit,
     CommonOptionBag.VerifyIncludedFiles,
     CommonOptionBag.ManualLemmaInduction,
     CommonOptionBag.SolverPath,
     CommonOptionBag.DisableNonLinearArithmetic,
+    CommonOptionBag.IsolateAssertions,
     BoogieOptionBag.BoogieArguments,
+    CommonOptionBag.VerificationLogFormat,
+    CommonOptionBag.SolverResourceLimit,
+    CommonOptionBag.SolverPlugin,
+    CommonOptionBag.SolverLog,
   }.ToList();
 
   public static IReadOnlyList<Option> TranslationOptions = new Option[] {
@@ -59,13 +62,15 @@ static ICommandSpec() {
   });
 
   public static IReadOnlyList<Option> ParserOptions = new List<Option>(new Option[] {
+    CommonOptionBag.StdIn,
     BoogieOptionBag.Cores,
     CommonOptionBag.Libraries,
     CommonOptionBag.Plugin,
     CommonOptionBag.Prelude,
     Function.FunctionSyntaxOption,
     CommonOptionBag.QuantifierSyntax,
     CommonOptionBag.UnicodeCharacters,
+    CommonOptionBag.ErrorLimit,
   });
 
   public static IReadOnlyList<Option> ResolverOptions = new List<Option>(new Option[] {

Source/DafnyDriver/Commands/MeasureComplexityCommand.cs

@@ -9,16 +9,12 @@ public class MeasureComplexityCommand : ICommandSpec {
   public IEnumerable<Option> Options => new Option[] {
     Iterations,
     RandomSeed,
-    Format,
-    IsolateAssertions,
   }.Concat(ICommandSpec.VerificationOptions).
     Concat(ICommandSpec.ResolverOptions);
 
   static MeasureComplexityCommand() {
     DafnyOptions.RegisterLegacyBinding(Iterations, (o, v) => o.RandomSeedIterations = (int)v);
     DafnyOptions.RegisterLegacyBinding(RandomSeed, (o, v) => o.RandomSeed = (int)v);
-    DafnyOptions.RegisterLegacyBinding(IsolateAssertions, (o, v) => o.VcsSplitOnEveryAssert = v);
-    DafnyOptions.RegisterLegacyBinding(Format, (o, v) => o.VerificationLoggerConfigs = v);
   }
 
   private static readonly Option<uint> RandomSeed = new("--random-seed", () => 0U,
@@ -29,16 +25,6 @@ static MeasureComplexityCommand() {
     ArgumentHelpName = "n"
   };
 
-  private static readonly Option<bool> IsolateAssertions = new("--isolate-assertions", @"Verify each assertion in isolation.");
-
-  private static readonly Option<List<string>> Format = new("--format", $@"
-Logs verification results using the given test result format. The currently supported formats are `trx`, `csv`, and `text`. These are: the XML-based format commonly used for test results for .NET languages, a custom CSV schema, and a textual format meant for human consumption. You can provide configuration using the same string format as when using the --logger option for dotnet test, such as: --format ""trx;LogFileName=<...>"");
-  
-The `trx` and `csv` formats automatically choose an output file name by default, and print the name of this file to the console. The `text` format prints its output to the console by default, but can send output to a file given the `LogFileName` option.
-
-The `text` format also includes a more detailed breakdown of what assertions appear in each assertion batch. When combined with the {IsolateAssertions.Name} option, it will provide approximate time and resource use costs for each assertion, allowing identification of especially expensive assertions.".TrimStart()) {
-    ArgumentHelpName = "configuration"
-  };
 
   public Command Create() {
     var result = new Command("measure-complexity", "(Experimental) Measure the complexity of verifying the program.");

Test/cli/errorLimit.dfy

@@ -0,0 +1,11 @@
+// RUN: %exits-with 4 %baredafny verify %args --error-limit=2 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+method m(x: int) {
+  if x == 1 {
+    assert x != 1;
+  } else if x == 2 {
+    assert x != 2;
+  } else if x == 3 {
+    assert x != 3;
+  }
+}

Test/cli/errorLimit.dfy.expect

@@ -0,0 +1,4 @@
+errorLimit.dfy(5,13): Error: assertion might not hold
+errorLimit.dfy(7,13): Error: assertion might not hold
+
+Dafny program verifier finished with 0 verified, 2 errors

Test/cli/solverLog.dfy

@@ -0,0 +1,7 @@
+// RUN: %baredafny verify %args --solver-log="log.smt2" --resource-limit 10 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %OutputCheck --file-to-check "log.smt2" "%s"
+// CHECK: rlimit 10000
+method m() {
+  assert 1 + 1 == 2;
+}

Test/cli/solverLog.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

Test/logger/CSVLogger.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny measure-complexity --format:csv";"LogFileName="%t.csv" "%s"
+// RUN: %exits-with 4 %baredafny verify --log-format:csv";"LogFileName="%t.csv" "%s"
 // RUN: %OutputCheck --file-to-check "%t.csv" "%s"
 
 // CHECK: TestResult\.DisplayName,TestResult\.Outcome,TestResult\.Duration,TestResult\.ResourceCount

Test/logger/TextLogger.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny measure-complexity --format:text --isolate-assertions "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --log-format:text --isolate-assertions "%s" > "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK: Overall outcome: Errors
 // CHECK: Overall time: .*

Test/logger/TextLoggerBatch.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny measure-complexity --format:text "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --log-format:text "%s" > "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK: Overall outcome: Errors
 // CHECK: Overall time: .*

Test/logger/VerificationLogger.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny measure-complexity --iterations=2 --random-seed=1 --format:trx";"LogFileName="%t.trx" "%s"
+// RUN: %exits-with 4 %baredafny measure-complexity --iterations=2 --random-seed=1 --log-format:trx";"LogFileName="%t.trx" "%s"
 // RUN: %OutputCheck --file-to-check "%t.trx" "%s"
 
 // CHECK: \<UnitTestResult.* testName="ExampleWithSplits \(correctness\) \(assertion batch 3\)" .*\>