Speed up dafny verify by reducing memory pressure

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.2.5" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.3.3" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

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,9 @@ 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, SymbolParts }
+  public static readonly Option<ProgressLevel> ProgressOption =
+    new("--progress", "While verifying, output information that helps track progress");
 
   public static readonly Option<string> LogLocation =
     new("--log-location", "Sets the directory where to store log files") {

Source/DafnyCore/Pipeline/Compilation.cs

@@ -333,9 +333,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,
@@ -434,6 +431,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) {
@@ -508,7 +510,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,
@@ -580,4 +582,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.SymbolParts) {
           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/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs

@@ -44,7 +44,7 @@ public static VerificationTaskResult VCResultLogEntryToPartialVerificationRunRes
     var mockNumber = 42;
     var mockAsserts = vcResult.Asserts.Select(t => new AssertCmd(t.Tok, null, new DummyProofObligationDescription(t.Description)));
     var runResult = new VerificationRunResult(vcResult.VCNum, mockNumber, vcResult.StartTime, vcResult.Outcome, vcResult.RunTime, mockNumber, null!,
-      mockAsserts.ToList(), vcResult.CoveredElements, vcResult.ResourceCount, null);
+      mockAsserts.ToList(), vcResult.CoveredElements, vcResult.ResourceCount, null, null);
     return new VerificationTaskResult(null, runResult);
   }
 

Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs

@@ -332,7 +332,7 @@ string MoreInformation(Boogie.IToken? token, bool hoveringPostcondition) {
         } else {
           information += GetDescription(returnCounterexample.FailingReturn.Description);
         }
-        information += MoreInformation(returnCounterexample.FailingAssert.tok, currentlyHoveringPostcondition);
+        information += MoreInformation(returnCounterexample.FailingFailingAssert.tok, currentlyHoveringPostcondition);
       } else if (counterexample is CallCounterexample callCounterexample) {
         if (assertionNode.StatusVerification == GutterVerificationStatus.Error &&
             callCounterexample.FailingRequires.Description.SuccessDescription != "assertion always holds"

Source/DafnyTestGeneration/PathBasedModifier.cs

@@ -116,13 +116,13 @@ private IEnumerable<Path> GeneratePaths(Implementation impl, int minPathLength,
           yield return new Path(impl, currPathVariables.ToList(), new() { block },
             currPath.Append(block).ToList());
         } else {
-          if (currPath.Count != 0 && ((GotoCmd)currPath.Last().TransferCmd).labelTargets.Count != 1) {
+          if (currPath.Count != 0 && ((GotoCmd)currPath.Last().TransferCmd).LabelTargets.Count != 1) {
             currPathVariables.Add(blockToVariable[block]); // only constrain the path if there is more than one goto
           }
           currPath.Add(block);
           otherGotos.Add(new List<Block>());
           var gotoCmd = block.TransferCmd as GotoCmd;
-          foreach (var nextBlock in gotoCmd?.labelTargets ?? new List<Block>()) {
+          foreach (var nextBlock in gotoCmd?.LabelTargets ?? new List<Block>()) {
             if (currPathVariables.Contains(blockToVariable[nextBlock])) { // this prevents cycles
               continue;
             }

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'