Introduce Stability command (#3061)

### Changes

- Add the stability command and related options

```
Usage:
  Dafny check-stability [<file>...] [options]

Arguments:
  <file>  input files

Options:
  --iterations <n>                             Attempt to verify each proof n times with n random seeds. If random-seed 
                                               is used, each proof attempt will use a new random seed derived from this 
                                               one. If not, it will use a different seed between iterations. [default: 
                                               10]
  --random-seed <seed>                         Turn on randomization of the input that Boogie passes to the SMT solver 
                                               and turn on randomization in the SMT solver itself. Certain Boogie 
                                               inputs are unstable in the sense that changes to the input that preserve 
                                               its meaning may cause the output to change. This option simulates 
                                               meaning-preserving changes to the input without requiring the user to 
                                               actually make those changes. The input changes are renaming variables 
                                               and reordering declarations in the input, and setting solver options 
                                               that have similar effects. [default: 0]
  --format <configuration>                     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=<...>.z
  
                                               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 isolate-assertions option, it will provide approximate time and 
                                               resource use costs for each assertion, allowing identification of 
                                               especially expensive assertions. []
  --isolate-assertions                         Verify each assertion in isolation. [default: False]

```
### Testing
- Updated existing tests to use the new command and options. Note that
tests for --random-seed and --iterations were and are missing!


<!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md
-->

<!-- Is this a bug fix? Remember to include a test in Test/git-issues/
-->

<!-- Is this a bug fix for an issue introduced in the latest release?
Mention this in the PR details and ensure a patch release is considered
-->

<!-- Does this PR need tests? Add them to `Test/` or to
`Source/*.Test/…` and run them with `dotnet test` -->

<!-- Are you moving a large amount of code? Read CONTRIBUTING.md to
learn how to do that while maintaining git history -->

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

Author: keyboardDrummer

Source/DafnyDriver/Commands/CommandRegistry.cs

@@ -5,7 +5,6 @@
 using System.CommandLine.Parsing;
 using System.IO;
 using System.Linq;
-using System.Threading.Tasks;
 using JetBrains.Annotations;
 using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer;
@@ -31,6 +30,7 @@ static CommandRegistry() {
     AddCommand(new RunCommand());
     AddCommand(new BuildCommand());
     AddCommand(new TranslateCommand());
+    AddCommand(new MeasureComplexityCommand());
     AddCommand(new ServerCommand());
     AddCommand(new TestCommand());
     AddCommand(new GenerateTestsCommand());

Source/DafnyDriver/Commands/MeasureComplexityCommand.cs

@@ -0,0 +1,52 @@
+using System.Collections.Generic;
+using System.CommandLine;
+using System.CommandLine.Invocation;
+using System.Linq;
+
+namespace Microsoft.Dafny;
+
+public class MeasureComplexityCommand : ICommandSpec {
+  public IEnumerable<Option> Options => new Option[] {
+    Iterations,
+    RandomSeed,
+    Format,
+    IsolateAssertions,
+  }.Concat(ICommandSpec.VerificationOptions).
+    Concat(ICommandSpec.CommonOptions);
+
+  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,
+    $"Turn on randomization of the input that Dafny passes to the SMT solver and turn on randomization in the SMT solver itself. Certain Dafny proofs are complex in the sense that changes to the proof that preserve its meaning may cause its verification result to change. This option simulates meaning-preserving changes to the proofs without requiring the user to actually make those changes. The proof changes are renaming variables and reordering declarations in the SMT input passed to the solver, and setting solver options that have similar effects.");
+
+  private static readonly Option<uint> Iterations = new("--iterations", () => 10U,
+    $"Attempt to verify each proof n times with n random seeds, each seed derived from the previous one. {RandomSeed.Name} can be used to specify the first seed, which will otherwise be 0.") {
+    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.");
+    result.AddArgument(ICommandSpec.FilesArgument);
+    return result;
+  }
+
+  public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) {
+    dafnyOptions.Compile = false;
+  }
+}

Test/logger/CSVLogger.dfy

@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %dafny /verificationLogger:csv";"LogFileName="%t.csv" "%s"
+// RUN: %exits-with 4 %baredafny measure-complexity --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 %dafny /compile:0 /verificationLogger:text /vcsSplitOnEveryAssert "%s" > "%t"
+// RUN: %exits-with 4 %baredafny measure-complexity --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 %dafny /compile:0 /verificationLogger:text "%s" > "%t"
+// RUN: %exits-with 4 %baredafny measure-complexity --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 %dafny /verificationLogger:trx";"LogFileName="%t.trx" "%s"
+// RUN: %exits-with 4 %baredafny measure-complexity --iterations=2 --random-seed=1 --format:trx";"LogFileName="%t.trx" "%s"
 // RUN: %OutputCheck --file-to-check "%t.trx" "%s"
 
 // CHECK: \<UnitTestResult.* testName="ExampleWithSplits \(correctness\) \(assertion batch 3\)" .*\>