Split responsibilities into separate methods in CliCompilation (#5122)

### Description
Split one large method `VerifyAllAndPrintSummary` into 4 smaller ones:
`VerifyAll`, `ReportVerificationDiagnostics`,
`ReportVerificationSummary` and `RecordProofDependencies`.

### How has this been tested?
There are some small changes in output that required expect file updates

<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/Backends/ExecutableBackend.cs

@@ -6,9 +6,10 @@
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
+using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.Plugins;
 
-namespace Microsoft.Dafny.Compilers;
+namespace Microsoft.Dafny;
 
 public abstract class ExecutableBackend : IExecutableBackend {
  // May be null for backends that don't use the single-pass compiler logic

Source/DafnyCore/Backends/GoLang/GoBackend.cs

@@ -5,8 +5,9 @@
 using System.IO;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using Microsoft.Dafny.Compilers;
 
-namespace Microsoft.Dafny.Compilers;
+namespace Microsoft.Dafny;
 
 public class GoBackend : ExecutableBackend {
 
@@ -190,7 +191,7 @@ bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextW
 
  private static string FindPackageName(string externFilename) {
  using var rd = new StreamReader(new FileStream(externFilename, FileMode.Open, FileAccess.Read));
- while (rd.ReadLine() is string line) {
+ while (rd.ReadLine() is { } line) {
  var match = PackageLine.Match(line);
  if (match.Success) {
  return match.Groups[1].Value;

Source/DafnyCore/Pipeline/Compilation.cs

@@ -462,17 +462,21 @@ public void Dispose() {
  CancelPendingUpdates();
  }
 
- public static List<DafnyDiagnostic> GetDiagnosticsFromResult(DafnyOptions options, Uri uri, IVerificationTask task, VerificationRunResult result) {
+ public static List<DafnyDiagnostic> GetDiagnosticsFromResult(DafnyOptions options, Uri uri, ICanVerify canVerify,
+ IVerificationTask task, VerificationRunResult result) {
  var errorReporter = new ObservableErrorReporter(options, uri);
  List<DafnyDiagnostic> diagnostics = new();
  errorReporter.Updates.Subscribe(d => diagnostics.Add(d.Diagnostic));
 
- ReportDiagnosticsInResult(options, task, result, errorReporter);
+ ReportDiagnosticsInResult(options, canVerify.NameToken.val, task.ScopeToken,
+ task.Split.Implementation.GetTimeLimit(options), result, errorReporter);
 
  return diagnostics.OrderBy(d => d.Token.GetLspPosition()).ToList();
  }
 
- public static void ReportDiagnosticsInResult(DafnyOptions options, IVerificationTask task, VerificationRunResult result,
+ public static void ReportDiagnosticsInResult(DafnyOptions options, string name, Boogie.IToken token,
+ uint timeLimit,
+ VerificationRunResult result,
  ErrorReporter errorReporter) {
  var outcome = GetOutcome(result.Outcome);
  result.CounterExamples.Sort(new CounterexampleComparer());
@@ -485,10 +489,9 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, IVerification
  // The Boogie API forces us to create a temporary engine here to report the outcome, even though it only uses the options.
  var boogieEngine = new ExecutionEngine(options, new VerificationResultCache(),
  CustomStackSizePoolTaskScheduler.Create(0, 0));
- var implementation = task.Split.Implementation;
  boogieEngine.ReportOutcome(null, outcome, outcomeError => errorReporter.ReportBoogieError(outcomeError, false),
- implementation.VerboseName, implementation.tok, null, TextWriter.Null,
- implementation.GetTimeLimit(options), result.CounterExamples);
+ name, token, null, TextWriter.Null,
+ timeLimit, result.CounterExamples);
  }
 
  public static VcOutcome GetOutcome(SolverOutcome outcome) {

Source/DafnyCore/ProofDependencyWarnings.cs

@@ -8,17 +8,19 @@
 
 namespace Microsoft.Dafny;
 
+public record VerificationTaskResult(IVerificationTask Task, VerificationRunResult Result);
+
 public class ProofDependencyWarnings {
 
 
- public static void ReportSuspiciousDependencies(DafnyOptions options, IEnumerable<(IVerificationTask Task, Completed Result)> parts,
+ public static void ReportSuspiciousDependencies(DafnyOptions options, IEnumerable<VerificationTaskResult> parts,
  ErrorReporter reporter, ProofDependencyManager manager) {
  foreach (var resultsForScope in parts.GroupBy(p => p.Task.ScopeId)) {
  WarnAboutSuspiciousDependenciesForImplementation(options,
  reporter,
  manager,
  resultsForScope.Key,
- resultsForScope.Select(p => p.Result.Result).ToList());
+ resultsForScope.Select(p => p.Result).ToList());
  }
  }
 

Source/DafnyDriver/CliCanVerifyState.cs

@@ -9,6 +9,6 @@ namespace DafnyDriver.Commands;
 public record CliCanVerifyState {
  public Func<IVerificationTask, bool> TaskFilter = _ => true;
  public readonly TaskCompletionSource Finished = new();
- public readonly ConcurrentBag<(IVerificationTask Task, Completed Result)> CompletedParts = new();
+ public readonly ConcurrentQueue<(IVerificationTask Task, Completed Result)> CompletedParts = new();
  public readonly ConcurrentBag<IVerificationTask> Tasks = new();
 }