Speed up dafny verify by reducing memory pressure

Source/DafnyCore/Generic/LazyConcurrentDictionary.cs

@@ -62,4 +62,8 @@ public bool TryGetValue(TKey key, out TValue? value) {
   }
 
   public TValue this[TKey key] => underlyingDictionary[key].Value;
+
+  public bool Remove(TKey key) {
+    return underlyingDictionary.TryRemove(key, out _);
+  }
 }

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -14,10 +14,12 @@ public class CommonOptionBag {
 
   public static void EnsureStaticConstructorHasRun() { }
 
-  public static readonly Option<bool> ProgressOption =
-    new("--progress", "While verifying, output information that helps track progress") {
-      IsHidden = true
-    };
+  public enum ProgressLevel { None, Symbol, VerificationJobs }
+  public static readonly Option<ProgressLevel> ProgressOption =
+    new("--progress", $"While verifying, output information that helps track progress. " +
+                      $"Use '{ProgressLevel.Symbol}' to show progress across symbols such as methods and functions. " +
+                      $"Verification of a symbol is usually split across several jobs. " +
+                      $"Use {ProgressLevel.VerificationJobs} to additionally show progress across jobs.");
 
   public static readonly Option<string> LogLocation =
     new("--log-location", "Sets the directory where to store log files") {

Source/DafnyCore/Pipeline/Compilation.cs

@@ -332,9 +332,6 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
         tasksForModule = await translatedModules.GetOrAdd(containingModule, async () => {
           var result = await verifier.GetVerificationTasksAsync(boogieEngine, resolution, containingModule,
             cancellationSource.Token);
-          foreach (var task in result) {
-            cancellationSource.Token.Register(task.Cancel);
-          }
 
           return result.GroupBy(t => ((IToken)t.ScopeToken).GetFilePosition()).ToDictionary(
             g => g.Key,
@@ -433,6 +430,11 @@ private void HandleStatusUpdate(ICanVerify canVerify, IVerificationTask verifica
 
   public void CancelPendingUpdates() {
     cancellationSource.Cancel();
+    foreach (var (_, tasks) in tasksPerVerifiable) {
+      foreach (var task in tasks) {
+        task.Cancel();
+      }
+    }
   }
 
   public async Task<TextEditContainer?> GetTextEditToFormatCode(Uri uri) {
@@ -507,7 +509,7 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name,
 
     // This reports problems that are not captured by counter-examples, like a time-out
     // 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(),
+    var boogieEngine = new ExecutionEngine(options, new EmptyVerificationResultCache(),
       CustomStackSizePoolTaskScheduler.Create(0, 0));
     boogieEngine.ReportOutcome(null, outcome, outcomeError => errorReporter.ReportBoogieError(outcomeError, null, false),
       name, token, null, TextWriter.Null,
@@ -579,4 +581,12 @@ public static VcOutcome GetOutcome(SolverOutcome outcome) {
         throw new ArgumentOutOfRangeException(nameof(outcome), outcome, null);
     }
   }
+
+  public void ClearModuleCache(ModuleDefinition moduleDefinition) {
+    translatedModules.Remove(moduleDefinition);
+  }
+
+  public void ClearCanVerifyCache(ICanVerify canVerify) {
+    tasksPerVerifiable.Remove(canVerify);
+  }
 }

Source/DafnyDriver/CliCanVerifyState.cs

@@ -10,5 +10,5 @@ public record CliCanVerifyState {
   public Func<IVerificationTask, bool> TaskFilter = _ => true;
   public readonly TaskCompletionSource Finished = new();
   public readonly ConcurrentQueue<(IVerificationTask Task, Completed Result)> CompletedParts = new();
-  public readonly ConcurrentBag<IVerificationTask> Tasks = new();
+  public int TaskCount;
 }

Source/DafnyDriver/CliCompilation.cs

@@ -45,7 +45,7 @@ private CliCompilation(
     options.RunningBoogieFromCommandLine = true;
 
     var input = new CompilationInput(options, 0, options.DafnyProject);
-    var executionEngine = new ExecutionEngine(options, new VerificationResultCache(), DafnyMain.LargeThreadScheduler);
+    var executionEngine = new ExecutionEngine(options, new EmptyVerificationResultCache(), DafnyMain.LargeThreadScheduler);
     Compilation = createCompilation(executionEngine, input);
   }
 
@@ -162,10 +162,10 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
       if (ev is CanVerifyPartsIdentified canVerifyPartsIdentified) {
         var canVerifyResult = canVerifyResults[canVerifyPartsIdentified.CanVerify];
         foreach (var part in canVerifyPartsIdentified.Parts.Where(canVerifyResult.TaskFilter)) {
-          canVerifyResult.Tasks.Add(part);
+          Interlocked.Increment(ref canVerifyResult.TaskCount);
         }
 
-        if (canVerifyResult.CompletedParts.Count == canVerifyResult.Tasks.Count) {
+        if (canVerifyResult.CompletedParts.Count == canVerifyResult.TaskCount) {
           canVerifyResult.Finished.SetResult();
         }
       }
@@ -184,17 +184,17 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
         var canVerifyResult = canVerifyResults[boogieUpdate.CanVerify];
         canVerifyResult.CompletedParts.Enqueue((boogieUpdate.VerificationTask, completed));
 
-        if (Options.Get(CommonOptionBag.ProgressOption)) {
+        if (Options.Get(CommonOptionBag.ProgressOption) == CommonOptionBag.ProgressLevel.VerificationJobs) {
           var token = BoogieGenerator.ToDafnyToken(false, boogieUpdate.VerificationTask.Split.Token);
           var runResult = completed.Result;
           var timeString = runResult.RunTime.ToString("g");
           Options.OutputWriter.WriteLine(
-            $"Verified part #{boogieUpdate.VerificationTask.Split.SplitIndex}, {canVerifyResult.CompletedParts.Count}/{canVerifyResult.Tasks.Count} of {boogieUpdate.CanVerify.FullDafnyName}" +
+            $"Verified part #{boogieUpdate.VerificationTask.Split.SplitIndex}, {canVerifyResult.CompletedParts.Count}/{canVerifyResult.TaskCount} of {boogieUpdate.CanVerify.FullDafnyName}" +
             $", on line {token.line}, " +
             $"{DescribeOutcome(Compilation.GetOutcome(runResult.Outcome))}" +
             $" (time: {timeString}, resource count: {runResult.ResourceCount})");
         }
-        if (canVerifyResult.CompletedParts.Count == canVerifyResult.Tasks.Count) {
+        if (canVerifyResult.CompletedParts.Count == canVerifyResult.TaskCount) {
           canVerifyResult.Finished.TrySetResult();
         }
       }
@@ -216,42 +216,53 @@ public async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily(int? randomSeed)
     canVerifies = FilterCanVerifies(canVerifies, out var line);
     VerifiedAssertions = line != null;
 
-    var orderedCanVerifies = canVerifies.OrderBy(v => v.Tok.pos).ToList();
-    foreach (var canVerify in orderedCanVerifies) {
-      var results = new CliCanVerifyState();
-      canVerifyResults[canVerify] = results;
-      if (line != null) {
-        results.TaskFilter = t => KeepVerificationTask(t, line.Value);
-      }
+    int done = 0;
 
-      var shouldVerify = await Compilation.VerifyCanVerify(canVerify, results.TaskFilter, randomSeed);
-      if (!shouldVerify) {
-        orderedCanVerifies.Remove(canVerify);
-      }
-    }
+    var canVerifiesPerModule = canVerifies.ToList().GroupBy(c => c.ContainingModule).ToList();
+    foreach (var canVerifiesForModule in canVerifiesPerModule.
+               OrderBy(v => v.Key.Tok.pos)) {
+      var orderedCanVerifies = canVerifiesForModule.OrderBy(v => v.Tok.pos).ToList();
+      foreach (var canVerify in orderedCanVerifies) {
+        var results = new CliCanVerifyState();
+        canVerifyResults[canVerify] = results;
+        if (line != null) {
+          results.TaskFilter = t => KeepVerificationTask(t, line.Value);
+        }
 
-    int done = 0;
-    foreach (var canVerify in orderedCanVerifies) {
-      var results = canVerifyResults[canVerify];
-      try {
-        if (Options.Get(CommonOptionBag.ProgressOption)) {
-          await Options.OutputWriter.WriteLineAsync($"Verified {done}/{orderedCanVerifies.Count} symbols. Waiting for {canVerify.FullDafnyName} to verify.");
+        var shouldVerify = await Compilation.VerifyCanVerify(canVerify, results.TaskFilter, randomSeed);
+        if (!shouldVerify) {
+          canVerifies.ToList().Remove(canVerify);
         }
-        await results.Finished.Task;
-        done++;
-      } catch (ProverException e) {
-        Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, e.Message);
-        yield break;
-      } catch (OperationCanceledException) {
-
-      } catch (Exception e) {
-        Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok,
-          $"Internal error occurred during verification: {e.Message}\n{e.StackTrace}");
-        throw;
       }
-      yield return new CanVerifyResult(canVerify, results.CompletedParts.Select(c => new VerificationTaskResult(c.Task, c.Result.Result)).ToList());
 
-      canVerifyResults.Remove(canVerify); // Free memory
+      foreach (var canVerify in orderedCanVerifies) {
+        var results = canVerifyResults[canVerify];
+        try {
+          if (Options.Get(CommonOptionBag.ProgressOption) > CommonOptionBag.ProgressLevel.None) {
+            await Options.OutputWriter.WriteLineAsync(
+              $"Verified {done}/{canVerifies.ToList().Count} symbols. Waiting for {canVerify.FullDafnyName} to verify.");
+          }
+
+          await results.Finished.Task;
+          done++;
+        } catch (ProverException e) {
+          Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, e.Message);
+          yield break;
+        } catch (OperationCanceledException) {
+
+        } catch (Exception e) {
+          Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok,
+            $"Internal error occurred during verification: {e.Message}\n{e.StackTrace}");
+          throw;
+        }
+
+        yield return new CanVerifyResult(canVerify,
+          results.CompletedParts.Select(c => new VerificationTaskResult(c.Task, c.Result.Result)).ToList());
+
+        canVerifyResults.Remove(canVerify); // Free memory
+        Compilation.ClearCanVerifyCache(canVerify);
+      }
+      Compilation.ClearModuleCache(canVerifiesForModule.Key);
     }
   }
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Iterators.dfy.expect

@@ -11,15 +11,6 @@ Iterators.dfy(177,27): Error: assertion might not hold
 Iterators.dfy(208,6): Error: an assignment to _new is only allowed to shrink the set
 Iterators.dfy(212,20): Error: assertion might not hold
 Iterators.dfy(234,20): Error: assertion might not hold
-Iterators.dfy(251,9): Error: decreases clause might not decrease
-Iterators.dfy(274,9): Error: decreases clause might not decrease
-Iterators.dfy(284,31): Error: decreases clause might not decrease
-Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause
-Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause
-Iterators.dfy(326,31): Error: cannot prove termination; try supplying a decreases clause
-Iterators.dfy(343,9): Error: decreases clause might not decrease
-Iterators.dfy(353,31): Error: cannot prove termination; try supplying a decreases clause
-Iterators.dfy(370,9): Error: decreases clause might not decrease
 Iterators.dfy(413,16): Error: this invariant could not be proved to be maintained by the loop
  Related message: loop invariant violation
 Iterators.dfy(414,21): Error: this invariant could not be proved to be maintained by the loop
@@ -40,5 +31,14 @@ Iterators.dfy(461,21): Error: this invariant could not be proved to be maintaine
  Related message: loop invariant violation
 Iterators.dfy(470,4): Error: possible violation of yield-ensures condition
 Iterators.dfy(451,21): Related location: this proposition could not be proved
+Iterators.dfy(251,9): Error: decreases clause might not decrease
+Iterators.dfy(274,9): Error: decreases clause might not decrease
+Iterators.dfy(284,31): Error: decreases clause might not decrease
+Iterators.dfy(296,9): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(317,9): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(326,31): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(343,9): Error: decreases clause might not decrease
+Iterators.dfy(353,31): Error: cannot prove termination; try supplying a decreases clause
+Iterators.dfy(370,9): Error: decreases clause might not decrease
 
 Dafny program verifier finished with 35 verified, 30 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/OpaqueFunctions.dfy.expect

@@ -1,3 +1,5 @@
+OpaqueFunctions.dfy(214,15): Error: assertion might not hold
+OpaqueFunctions.dfy(229,19): Error: assertion might not hold
 OpaqueFunctions.dfy(38,15): Error: assertion might not hold
 OpaqueFunctions.dfy(69,7): Error: a precondition for this call could not be proved
 OpaqueFunctions.dfy(35,15): Related location: this is the precondition that could not be proved
@@ -20,8 +22,6 @@ OpaqueFunctions.dfy(157,20): Error: assertion might not hold
 OpaqueFunctions.dfy(160,20): Error: assertion might not hold
 OpaqueFunctions.dfy(165,31): Error: assertion might not hold
 OpaqueFunctions.dfy(181,12): Error: assertion might not hold
-OpaqueFunctions.dfy(214,15): Error: assertion might not hold
-OpaqueFunctions.dfy(229,19): Error: assertion might not hold
 OpaqueFunctions.dfy(246,11): Error: assertion might not hold
 OpaqueFunctions.dfy(261,11): Error: assertion might not hold
 OpaqueFunctions.dfy(326,16): Error: assertion might not hold

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.expect

@@ -4,7 +4,6 @@ Termination.dfy(126,16): Error: decreases expression must be bounded below by 0
 Termination.dfy(255,34): Error: cannot prove termination; try supplying a decreases clause
 Termination.dfy(296,2): Error: decreases expression might not decrease
 Termination.dfy(361,46): Error: decreases clause might not decrease
-Termination.dfy[TerminationRefinement1](441,5): Error: decreases clause might not decrease
 Termination.dfy(534,2): Error: decreases expression might not decrease
 Termination.dfy(542,2): Error: decreases expression might not decrease
 Termination.dfy(549,2): Error: decreases expression might not decrease
@@ -21,5 +20,6 @@ Termination.dfy(730,2): Error: decreases expression might not decrease
 Termination.dfy(806,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy[TerminationRefinement1](441,5): Error: decreases clause might not decrease
 
 Dafny program verifier finished with 108 verified, 23 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy.refresh.expect

@@ -4,7 +4,6 @@ Termination.dfy(126,16): Error: decreases expression must be bounded below by 0
 Termination.dfy(255,34): Error: cannot prove termination; try supplying a decreases clause
 Termination.dfy(296,2): Error: decreases expression might not decrease
 Termination.dfy(361,46): Error: decreases clause might not decrease
-Termination.dfy[TerminationRefinement1](441,5): Error: decreases clause might not decrease
 Termination.dfy(534,2): Error: decreases expression might not decrease
 Termination.dfy(542,2): Error: decreases expression might not decrease
 Termination.dfy(549,2): Error: decreases expression might not decrease
@@ -22,5 +21,6 @@ Termination.dfy(806,2): Error: cannot prove termination; try supplying a decreas
 Termination.dfy(923,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 Termination.dfy(1178,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 Termination.dfy(1194,2): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy[TerminationRefinement1](441,5): Error: decreases clause might not decrease
 
 Dafny program verifier finished with 107 verified, 24 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInferenceRefresh.dfy.expect

@@ -1,9 +1,9 @@
 TypeInferenceRefresh.dfy(445,11): Warning: the modify statement with a block statement is deprecated
 TypeInferenceRefresh.dfy(807,4): Warning: this branch is redundant
-TypeInferenceRefresh.dfy(102,31): Error: value does not satisfy the subset constraints of 'SubsetType'
-TypeInferenceRefresh.dfy(107,31): Error: value does not satisfy the subset constraints of 'SubsetType'
 TypeInferenceRefresh.dfy(145,30): Error: element might not be in domain
 TypeInferenceRefresh.dfy(216,26): Error: result of operation might violate newtype constraint for 'int8'
+TypeInferenceRefresh.dfy(102,31): Error: value does not satisfy the subset constraints of 'SubsetType'
+TypeInferenceRefresh.dfy(107,31): Error: value does not satisfy the subset constraints of 'SubsetType'
 TypeInferenceRefresh.dfy(630,40): Error: value does not satisfy the subset constraints of 'nat'
 TypeInferenceRefresh.dfy(630,43): Error: value does not satisfy the subset constraints of 'nat'
 TypeInferenceRefresh.dfy(630,47): Error: value does not satisfy the subset constraints of 'nat'

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-977.dfy.expect

@@ -36,7 +36,6 @@ git-issue-977.dfy(71,4): Info: ensures RicochetOrd(m, num)
 git-issue-977.dfy(110,9): Info: Some instances of this call are not inlined.
 git-issue-977.dfy(143,9): Info: Some instances of this call are not inlined.
 git-issue-977.dfy(162,2): Info: Some instances of this call are not inlined.
-git-issue-977.dfy(220,11): Info: Some instances of this call are not inlined.
 git-issue-977.dfy(39,11): Error: assertion might not hold
 git-issue-977.dfy(14,20): Related location: this proposition could not be proved
 git-issue-977.dfy(9,7): Related location: this proposition could not be proved
@@ -46,5 +45,6 @@ git-issue-977.dfy(9,7): Related location: this proposition could not be proved
 git-issue-977.dfy(43,11): Error: assertion might not hold
 git-issue-977.dfy(30,20): Related location: this proposition could not be proved
 git-issue-977.dfy(9,7): Related location: this proposition could not be proved
+git-issue-977.dfy(220,11): Info: Some instances of this call are not inlined.
 
 Dafny program verifier finished with 20 verified, 3 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy

@@ -1,4 +1,4 @@
-// RUN: %verify --progress --cores 1 "%s" > "%t"
+// RUN: %verify --progress Symbol --cores 1 "%s" > "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK-L:Verified 0/5 symbols. Waiting for smallPrime to verify.
 // CHECK-L:Verified 2/5 symbols. Waiting for posIdMeth to verify.

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/filter-symbol.dfy.expect

@@ -1,19 +1,19 @@
 
 Dafny program verifier finished with 0 verified, 0 errors
-filter-symbol.dfy(12,29): Error: a postcondition could not be proved on this return path
-filter-symbol.dfy(12,23): Related location: this is the postcondition that could not be proved
 filter-symbol.dfy(14,27): Error: a postcondition could not be proved on this return path
 filter-symbol.dfy(14,21): Related location: this is the postcondition that could not be proved
+filter-symbol.dfy(12,29): Error: a postcondition could not be proved on this return path
+filter-symbol.dfy(12,23): Related location: this is the postcondition that could not be proved
 filter-symbol.dfy(19,29): Error: a postcondition could not be proved on this return path
 filter-symbol.dfy(19,23): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 0 verified, 3 errors
 filter-symbol.dfy(12,29): Error: a postcondition could not be proved on this return path
 filter-symbol.dfy(12,23): Related location: this is the postcondition that could not be proved
-filter-symbol.dfy(19,29): Error: a postcondition could not be proved on this return path
-filter-symbol.dfy(19,23): Related location: this is the postcondition that could not be proved
 filter-symbol.dfy(21,27): Error: a postcondition could not be proved on this return path
 filter-symbol.dfy(21,21): Related location: this is the postcondition that could not be proved
+filter-symbol.dfy(19,29): Error: a postcondition could not be proved on this return path
+filter-symbol.dfy(19,23): Related location: this is the postcondition that could not be proved
 
 Dafny program verifier finished with 0 verified, 3 errors
 filter-symbol.dfy(12,29): Error: a postcondition could not be proved on this return path