Fix measure-complexity command (#5138)

### Description
- Fix an unreleased bug that could cause `dafny verify` to stall
- Give meaning to `--iterations` and `--random-seed` options for
`measure-complexity`
- Do iterations one at a time
- Report "Starting verification of iteration {iteration} with seed
{iterationSeed}"); at the start of each iteration
- Add some references to the used random seed in verification logging

### How has this been tested?
- Updated `VerificationLogger.dfy` test

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

Source/DafnyCore/DafnyCore.csproj

@@ -34,7 +34,7 @@
  <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
  <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
  <PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
- <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.12" />
+ <PackageReference Include="Boogie.ExecutionEngine" Version="3.1.1" />
  <PackageReference Include="Tomlyn" Version="0.16.2" />
  </ItemGroup>
 

Source/DafnyCore/Generic/Util.cs

@@ -26,6 +26,12 @@ public static ISet<T> Empty<T>() {
 
  public static class Util {
 
+ public static Task WaitForComplete<T>(this IObservable<T> observable) {
+ var result = new TaskCompletionSource();
+ observable.Subscribe(_ => { }, e => result.SetException(e), () => result.SetResult());
+ return result.Task;
+ }
+
  public static string CapitaliseFirstLetter(this string input) {
  if (input.Length > 0) {
  return char.ToUpper(input[0]) + input.Substring(1);

Source/DafnyCore/Pipeline/Compilation.cs

@@ -57,7 +57,7 @@ public DafnyDiagnostic[] GetDiagnosticsForUri(Uri uri) =>
  private readonly ConcurrentDictionary<ICanVerify, Unit> verifyingOrVerifiedSymbols = new();
  private readonly LazyConcurrentDictionary<ICanVerify, IReadOnlyList<IVerificationTask>> tasksPerVerifiable = new();
 
- private DafnyOptions Options => Input.Options;
+ public DafnyOptions Options => Input.Options;
  public CompilationInput Input { get; }
  public DafnyProject Project => Input.Project;
  private readonly ExecutionEngine boogieEngine;
@@ -225,8 +225,6 @@ private async Task<ResolutionResult> ResolveAsync() {
  await ParsedProgram;
  var resolution = await documentLoader.ResolveAsync(this, transformedProgram!, cancellationSource.Token);
 
- Options.ProcessSolverOptions(errorReporter, Options.DafnyProject.StartingToken);
-
  updates.OnNext(new FinishedResolution(
  resolution,
  GetDiagnosticsCopy()));
@@ -281,10 +279,11 @@ public async Task<bool> VerifyLocation(FilePosition verifiableLocation, bool onl
  return false;
  }
 
- return await VerifyCanVerify(canVerify, _ => true, onlyPrepareVerificationForGutterTests);
+ return await VerifyCanVerify(canVerify, _ => true, null, onlyPrepareVerificationForGutterTests);
  }
 
  public async Task<bool> VerifyCanVerify(ICanVerify canVerify, Func<IVerificationTask, bool> taskFilter,
+ int? randomSeed = 0,
  bool onlyPrepareVerificationForGutterTests = false) {
 
  var resolution = await Resolution;
@@ -293,23 +292,23 @@ public async Task<bool> VerifyCanVerify(ICanVerify canVerify, Func<IVerification
  return false;
  }
 
- if (!onlyPrepareVerificationForGutterTests && !verifyingOrVerifiedSymbols.TryAdd(canVerify, Unit.Default)) {
+ if (!onlyPrepareVerificationForGutterTests && (randomSeed == null && !verifyingOrVerifiedSymbols.TryAdd(canVerify, Unit.Default))) {
  return false;
  }
 
  updates.OnNext(new ScheduledVerification(canVerify));
 
  if (onlyPrepareVerificationForGutterTests) {
- await VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution, taskFilter);
+ await VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution, taskFilter, randomSeed);
  return true;
  }
 
- _ = VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution, taskFilter);
+ _ = VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution, taskFilter, randomSeed);
  return true;
  }
 
  private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterTests, ICanVerify canVerify,
- ResolutionResult resolution, Func<IVerificationTask, bool> taskFilter) {
+ ResolutionResult resolution, Func<IVerificationTask, bool> taskFilter, int? randomSeed) {
  try {
 
  var ticket = verificationTickets.Dequeue(CancellationToken.None);
@@ -345,7 +344,7 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
  updated = true;
  return result;
  });
- if (updated) {
+ if (updated || randomSeed != null) {
  updates.OnNext(new CanVerifyPartsIdentified(canVerify,
  tasksPerVerifiable[canVerify].ToList()));
  }
@@ -355,7 +354,8 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
 
  if (!onlyPrepareVerificationForGutterTests) {
  foreach (var task in tasks.Where(taskFilter)) {
- VerifyTask(canVerify, task);
+ var seededTask = randomSeed == null ? task : task.FromSeed(randomSeed.Value);
+ VerifyTask(canVerify, seededTask);
  }
  }
 

Source/DafnyCore/Pipeline/IProgramVerifier.cs

@@ -8,8 +8,6 @@
 namespace Microsoft.Dafny {
  public record AssertionBatchResult(Implementation Implementation, VerificationRunResult Result);
 
- public record ProgramVerificationTasks(IReadOnlyList<IVerificationTask> Tasks);
-
  /// <summary>
  /// Implementations of this interface are responsible to verify the correctness of a program.
  /// </summary>

Source/DafnyCore/Pipeline/TextDocumentLoader.cs

@@ -52,6 +52,8 @@ private ResolutionResult ResolveInternal(Compilation compilation, Program progra
 
  symbolResolver.ResolveSymbols(compilation, program, cancellationToken);
 
+ compilation.Options.ProcessSolverOptions(compilation.Reporter, compilation.Options.DafnyProject.StartingToken);
+
  List<ICanVerify>? verifiables;
  if (compilation.HasErrors) {
  verifiables = null;

Source/DafnyDriver/CSVTestLogger.cs

@@ -12,7 +12,7 @@ public class CSVTestLogger : ITestLoggerWithParameters {
 
  private readonly ConcurrentBag<TestResult> results = new();
  private TextWriter writer;
- private TextWriter logWriter;
+ private readonly TextWriter logWriter;
  private string writerFilename;
 
  public CSVTestLogger(TextWriter logWriter) {
@@ -76,8 +76,9 @@ private void TestRunCompleteHandler(object sender, TestRunCompleteEventArgs e) {
  writer.WriteLine($"{result.TestCase.DisplayName},{result.Outcome},{result.Duration},{resCount}");
  }
 
- writer.Close();
+ writer.Flush();
  logWriter.WriteLine("Results File: " + Path.GetFullPath(writerFilename));
+ logWriter.Flush();
  }
  }
 }