From d8e97ee67e5737d47752e3e3c4529e25f3597f67 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Fri, 17 Feb 2023 12:04:07 -0800
Subject: [PATCH 1/4] Add several new-style command-line options

* `--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`
---
 Source/DafnyCore/Options/CommonOptionBag.cs   | 32 +++++++++++++++++++
 Source/DafnyCore/Options/ICommandSpec.cs      |  6 ++++
 .../Commands/MeasureComplexityCommand.cs      | 14 --------
 Test/cli/errorLimit.dfy                       | 11 +++++++
 Test/cli/errorLimit.dfy.expect                |  4 +++
 Test/cli/solverLog.dfy                        |  7 ++++
 Test/cli/solverLog.dfy.expect                 |  2 ++
 Test/logger/CSVLogger.dfy                     |  2 +-
 Test/logger/TextLogger.dfy                    |  2 +-
 Test/logger/TextLoggerBatch.dfy               |  2 +-
 Test/logger/VerificationLogger.dfy            |  2 +-
 11 files changed, 66 insertions(+), 18 deletions(-)
 create mode 100644 Test/cli/errorLimit.dfy
 create mode 100644 Test/cli/errorLimit.dfy.expect
 create mode 100644 Test/cli/solverLog.dfy
 create mode 100644 Test/cli/solverLog.dfy.expect

diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index c388afcaacc..c2a973e10a6 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/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", "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. 
@@ -163,6 +182,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; });
 
@@ -196,6 +216,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;
diff --git a/Source/DafnyCore/Options/ICommandSpec.cs b/Source/DafnyCore/Options/ICommandSpec.cs
index 9fa9a0c2ca4..cd850a6c50e 100644
--- a/Source/DafnyCore/Options/ICommandSpec.cs
+++ b/Source/DafnyCore/Options/ICommandSpec.cs
@@ -32,7 +32,12 @@ static ICommandSpec() {
     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[] {
@@ -66,6 +71,7 @@ static ICommandSpec() {
     Function.FunctionSyntaxOption,
     CommonOptionBag.QuantifierSyntax,
     CommonOptionBag.UnicodeCharacters,
+    CommonOptionBag.ErrorLimit,
   });
 
   public static IReadOnlyList<Option> ResolverOptions = new List<Option>(new Option[] {
diff --git a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs b/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs
index b56b8b0c340..c3401b12972 100644
--- a/Source/DafnyDriver/Commands/MeasureComplexityCommand.cs
+++ b/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.");
diff --git a/Test/cli/errorLimit.dfy b/Test/cli/errorLimit.dfy
new file mode 100644
index 00000000000..f0804906b13
--- /dev/null
+++ b/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;
+  }
+}
diff --git a/Test/cli/errorLimit.dfy.expect b/Test/cli/errorLimit.dfy.expect
new file mode 100644
index 00000000000..8964779714f
--- /dev/null
+++ b/Test/cli/errorLimit.dfy.expect
@@ -0,0 +1,4 @@
+errorLimit.dfy(7,13): Error: assertion might not hold
+errorLimit.dfy(9,13): Error: assertion might not hold
+
+Dafny program verifier finished with 0 verified, 2 errors
diff --git a/Test/cli/solverLog.dfy b/Test/cli/solverLog.dfy
new file mode 100644
index 00000000000..db4669c889a
--- /dev/null
+++ b/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;
+}
diff --git a/Test/cli/solverLog.dfy.expect b/Test/cli/solverLog.dfy.expect
new file mode 100644
index 00000000000..823a60a105c
--- /dev/null
+++ b/Test/cli/solverLog.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Test/logger/CSVLogger.dfy b/Test/logger/CSVLogger.dfy
index 0fe319cf5c0..e2101d0a9f4 100644
--- a/Test/logger/CSVLogger.dfy
+++ b/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
diff --git a/Test/logger/TextLogger.dfy b/Test/logger/TextLogger.dfy
index b57be9aba7f..fbccaba67a3 100644
--- a/Test/logger/TextLogger.dfy
+++ b/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: .*
diff --git a/Test/logger/TextLoggerBatch.dfy b/Test/logger/TextLoggerBatch.dfy
index 63486ef2313..204cd1e100c 100644
--- a/Test/logger/TextLoggerBatch.dfy
+++ b/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: .*
diff --git a/Test/logger/VerificationLogger.dfy b/Test/logger/VerificationLogger.dfy
index 55cccf49675..0ca3c540135 100644
--- a/Test/logger/VerificationLogger.dfy
+++ b/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\)" .*\>

From 1283f95a04e5bd91a7719e77fb771fb2c6b7ba8d Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Fri, 17 Feb 2023 15:03:17 -0800
Subject: [PATCH 2/4] Make --stdin available more broadly

---
 Source/DafnyCore/Options/ICommandSpec.cs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Source/DafnyCore/Options/ICommandSpec.cs b/Source/DafnyCore/Options/ICommandSpec.cs
index cd850a6c50e..6bb554b5ade 100644
--- a/Source/DafnyCore/Options/ICommandSpec.cs
+++ b/Source/DafnyCore/Options/ICommandSpec.cs
@@ -18,14 +18,12 @@ 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,
@@ -64,6 +62,7 @@ static ICommandSpec() {
   });
 
   public static IReadOnlyList<Option> ParserOptions = new List<Option>(new Option[] {
+    CommonOptionBag.StdIn,
     BoogieOptionBag.Cores,
     CommonOptionBag.Libraries,
     CommonOptionBag.Plugin,

From 409c6f81a236b36aa19be2e22dd49e17e0be8b02 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Fri, 17 Feb 2023 16:07:10 -0800
Subject: [PATCH 3/4] Fix --error-limit to match previous behavior

---
 Source/DafnyCore/Options/CommonOptionBag.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index f59ca82ee91..9c685390378 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -9,7 +9,7 @@ namespace Microsoft.Dafny;
 public class CommonOptionBag {
 
   public static readonly Option<int> ErrorLimit =
-    new("--error-limit", "Set the maximum number of errors to report (0 for unlimited).");
+    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.");

From 05d3bf311a24b051f07e8e16a1d2f887828d0bfe Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Fri, 17 Feb 2023 16:46:47 -0800
Subject: [PATCH 4/4] Fix test output

---
 Test/cli/errorLimit.dfy.expect | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Test/cli/errorLimit.dfy.expect b/Test/cli/errorLimit.dfy.expect
index 8964779714f..a2814ee1f4e 100644
--- a/Test/cli/errorLimit.dfy.expect
+++ b/Test/cli/errorLimit.dfy.expect
@@ -1,4 +1,4 @@
+errorLimit.dfy(5,13): Error: assertion might not hold
 errorLimit.dfy(7,13): Error: assertion might not hold
-errorLimit.dfy(9,13): Error: assertion might not hold
 
 Dafny program verifier finished with 0 verified, 2 errors