Filter assertions

Makefile

@@ -73,7 +73,7 @@ z3-ubuntu:
 	chmod +x ${DIR}/Binaries/z3/bin/z3-*
 
 format:
-	dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
+	dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
 
 clean:
 	(cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)

Source/DafnyCore/AST/Tokens.cs

@@ -109,6 +109,13 @@ public IToken WithVal(string newVal) {
     };
   }
 
+  public int CompareTo(Boogie.IToken other) {
+    if (line != other.line) {
+      return line.CompareTo(other.line);
+    }
+    return col.CompareTo(other.col);
+  }
+
   public override int GetHashCode() {
     return pos;
   }
@@ -189,6 +196,10 @@ public virtual IToken Prev {
   public int CompareTo(IToken other) {
     return WrappedToken.CompareTo(other);
   }
+
+  public int CompareTo(Boogie.IToken other) {
+    return WrappedToken.CompareTo(other);
+  }
 }
 
 public static class TokenExtensions {

Source/DafnyCore/DafnyConsolePrinter.cs

@@ -20,7 +20,7 @@ public class DafnyConsolePrinter : ConsolePrinter {
     }
   }
 
-  private readonly static ConditionalWeakTable<DafnyOptions, ConcurrentDictionary<Uri, List<string>>> fsCaches = new();
+  private static readonly ConditionalWeakTable<DafnyOptions, ConcurrentDictionary<Uri, List<string>>> fsCaches = new();
 
   private DafnyOptions options;
 
@@ -29,28 +29,28 @@ public record VCResultLogEntry(
     int VCNum,
     DateTime StartTime,
     TimeSpan RunTime,
-    ProverInterface.Outcome Outcome,
+    SolverOutcome Outcome,
     List<(Boogie.IToken Tok, string Description)> Asserts,
     IEnumerable<TrackedNodeComponent> CoveredElements,
     int ResourceCount);
   public record VerificationResultLogEntry(
-    ConditionGeneration.Outcome Outcome,
+    VcOutcome Outcome,
     TimeSpan RunTime,
     int ResourceCount,
     List<VCResultLogEntry> VCResults,
     List<Counterexample> Counterexamples);
   public record ConsoleLogEntry(ImplementationLogEntry Implementation, VerificationResultLogEntry Result);
 
-  public static VerificationResultLogEntry DistillVerificationResult(VerificationResult verificationResult) {
+  public static VerificationResultLogEntry DistillVerificationResult(ImplementationRunResult verificationResult) {
     return new VerificationResultLogEntry(
-      verificationResult.Outcome, verificationResult.End - verificationResult.Start,
-      verificationResult.ResourceCount, verificationResult.VCResults.Select(DistillVCResult).ToList(), verificationResult.Errors);
+      verificationResult.VcOutcome, verificationResult.End - verificationResult.Start,
+      verificationResult.ResourceCount, verificationResult.RunResults.Select(DistillVCResult).ToList(), verificationResult.Errors);
   }
 
-  private static VCResultLogEntry DistillVCResult(VCResult r) {
-    return new VCResultLogEntry(r.vcNum, r.startTime, r.runTime, r.outcome,
-        r.asserts.Select(a => (a.tok, a.Description.SuccessDescription)).ToList(), r.coveredElements,
-        r.resourceCount);
+  private static VCResultLogEntry DistillVCResult(VerificationRunResult r) {
+    return new VCResultLogEntry(r.VcNum, r.StartTime, r.RunTime, r.Outcome,
+        r.Asserts.Select(a => (a.tok, a.Description.SuccessDescription)).ToList(), r.CoveredElements,
+        r.ResourceCount);
   }
 
   public ConcurrentBag<ConsoleLogEntry> VerificationResults { get; } = new();
@@ -153,7 +153,7 @@ public override void ReportBplError(Boogie.IToken tok, string message, bool erro
     }
   }
 
-  public override void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result) {
+  public override void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result) {
     var impl = new ImplementationLogEntry(implementation.VerboseName, implementation.tok);
     VerificationResults.Add(new ConsoleLogEntry(impl, DistillVerificationResult(result)));
   }

Source/DafnyCore/DafnyCore.csproj

@@ -33,7 +33,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.10" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.11" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

Source/DafnyCore/Generic/BatchErrorReporter.cs

@@ -9,8 +9,7 @@ public class BatchErrorReporter : ErrorReporter {
 
   public void CopyDiagnostics(ErrorReporter intoReporter) {
     foreach (var diagnostic in AllMessages) {
-      intoReporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token,
-        diagnostic.Message);
+      intoReporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token, diagnostic.Message);
     }
   }
 

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -3,7 +3,6 @@
 using System.IO;
 using System.Linq;
 using DafnyCore;
-using Microsoft.Dafny.Compilers;
 
 namespace Microsoft.Dafny;
 

Source/DafnyCore/Pipeline/Compilation.cs

@@ -50,10 +50,10 @@ public DafnyDiagnostic[] GetDiagnosticsForUri(Uri uri) =>
   /// FilePosition is required because the default module lives in multiple files
   /// </summary>
   private readonly LazyConcurrentDictionary<ModuleDefinition,
-    Task<IReadOnlyDictionary<FilePosition, IReadOnlyList<IImplementationTask>>>> translatedModules = new();
+    Task<IReadOnlyDictionary<FilePosition, IReadOnlyList<IVerificationTask>>>> translatedModules = new();
 
   private readonly ConcurrentDictionary<ICanVerify, Unit> verifyingOrVerifiedSymbols = new();
-  private readonly LazyConcurrentDictionary<ICanVerify, IReadOnlyList<IImplementationTask>> implementationsPerVerifiable = new();
+  private readonly LazyConcurrentDictionary<ICanVerify, IReadOnlyList<IVerificationTask>> tasksPerVerifiable = new();
 
   private DafnyOptions Options => Input.Options;
   public CompilationInput Input { get; }
@@ -237,12 +237,12 @@ private async Task<ResolutionResult> ResolveAsync() {
     }
   }
 
-  public static string GetImplementationName(Implementation implementation) {
-    var prefix = implementation.Name.Split(BoogieGenerator.NameSeparator)[0];
+  public static string GetTaskName(IVerificationTask task) {
+    var prefix = task.ScopeId + task.Split.SplitIndex;
 
     // Refining declarations get the token of what they're refining, so to distinguish them we need to
     // add the refining module name to the prefix.
-    if (implementation.tok is RefinementToken refinementToken) {
+    if (task.ScopeToken is RefinementToken refinementToken) {
       prefix += "." + refinementToken.InheritingModule.Name;
     }
 
@@ -276,10 +276,11 @@ public async Task<bool> VerifyLocation(FilePosition verifiableLocation, bool onl
       return false;
     }
 
-    return await VerifyCanVerify(canVerify, onlyPrepareVerificationForGutterTests);
+    return await VerifyCanVerify(canVerify, _ => true, onlyPrepareVerificationForGutterTests);
   }
 
-  public async Task<bool> VerifyCanVerify(ICanVerify canVerify, bool onlyPrepareVerificationForGutterTests) {
+  public async Task<bool> VerifyCanVerify(ICanVerify canVerify, Func<IVerificationTask, bool> taskFilter,
+    bool onlyPrepareVerificationForGutterTests = false) {
     var resolution = await Resolution;
     var containingModule = canVerify.ContainingModule;
     if (!containingModule.ShouldVerify(resolution.ResolvedProgram.Compilation)) {
@@ -293,22 +294,22 @@ public async Task<bool> VerifyCanVerify(ICanVerify canVerify, bool onlyPrepareVe
     updates.OnNext(new ScheduledVerification(canVerify));
 
     if (onlyPrepareVerificationForGutterTests) {
-      await VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution);
+      await VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution, taskFilter);
       return true;
     }
 
-    _ = VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution);
+    _ = VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution, taskFilter);
     return true;
   }
 
   private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterTests, ICanVerify canVerify,
-    ResolutionResult resolution) {
+    ResolutionResult resolution, Func<IVerificationTask, bool> taskFilter) {
     try {
 
       var ticket = verificationTickets.Dequeue(CancellationToken.None);
       var containingModule = canVerify.ContainingModule;
 
-      IReadOnlyDictionary<FilePosition, IReadOnlyList<IImplementationTask>> tasksForModule;
+      IReadOnlyDictionary<FilePosition, IReadOnlyList<IVerificationTask>> tasksForModule;
       try {
         tasksForModule = await translatedModules.GetOrAdd(containingModule, async () => {
           var result = await verifier.GetVerificationTasksAsync(boogieEngine, resolution, containingModule,
@@ -317,9 +318,9 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
             cancellationSource.Token.Register(task.Cancel);
           }
 
-          return result.GroupBy(t => ((IToken)t.Implementation.tok).GetFilePosition()).ToDictionary(
+          return result.GroupBy(t => ((IToken)t.ScopeToken).GetFilePosition()).ToDictionary(
             g => g.Key,
-            g => (IReadOnlyList<IImplementationTask>)g.ToList());
+            g => (IReadOnlyList<IVerificationTask>)g.ToList());
         });
       } catch (OperationCanceledException) {
         throw;
@@ -328,26 +329,26 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
         throw;
       }
 
-      // For updated to be reliable, ImplementationsPerVerifiable must be Lazy
+      // For updated to be reliable, tasksPerVerifiable must be Lazy
       var updated = false;
-      var tasks = implementationsPerVerifiable.GetOrAdd(canVerify, () => {
+      var tasks = tasksPerVerifiable.GetOrAdd(canVerify, () => {
         var result =
           tasksForModule.GetValueOrDefault(canVerify.NameToken.GetFilePosition()) ??
-          new List<IImplementationTask>(0);
+          new List<IVerificationTask>(0);
 
         updated = true;
         return result;
       });
       if (updated) {
         updates.OnNext(new CanVerifyPartsIdentified(canVerify,
-          implementationsPerVerifiable[canVerify].ToList()));
+          tasksPerVerifiable[canVerify].ToList()));
       }
 
       // When multiple calls to VerifyUnverifiedSymbol are made, the order in which they pass this await matches the call order.
       await ticket;
 
       if (!onlyPrepareVerificationForGutterTests) {
-        foreach (var task in tasks) {
+        foreach (var task in tasks.Where(taskFilter)) {
           VerifyTask(canVerify, task);
         }
       }
@@ -358,16 +359,10 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
     }
   }
 
-  private void VerifyTask(ICanVerify canVerify, IImplementationTask task) {
+  private void VerifyTask(ICanVerify canVerify, IVerificationTask task) {
     var statusUpdates = task.TryRun();
     if (statusUpdates == null) {
       if (task.CacheStatus is Completed completedCache) {
-        foreach (var result in completedCache.Result.VCResults) {
-#pragma warning disable CS8625 // Cannot convert null literal to non-nullable reference type.
-          HandleStatusUpdate(canVerify, task, new BatchCompleted(null /* unused */, result));
-#pragma warning restore CS8625 // Cannot convert null literal to non-nullable reference type.
-        }
-
         HandleStatusUpdate(canVerify, task, completedCache);
       }
 
@@ -399,21 +394,21 @@ public async Task Cancel(FilePosition filePosition) {
     var resolution = await Resolution;
     var canVerify = resolution.ResolvedProgram.FindNode<ICanVerify>(filePosition.Uri, filePosition.Position.ToDafnyPosition());
     if (canVerify != null) {
-      var implementations = implementationsPerVerifiable.TryGetValue(canVerify, out var implementationsPerName)
-        ? implementationsPerName! : Enumerable.Empty<IImplementationTask>();
+      var implementations = tasksPerVerifiable.TryGetValue(canVerify, out var implementationsPerName)
+        ? implementationsPerName! : Enumerable.Empty<IVerificationTask>();
       foreach (var view in implementations) {
         view.Cancel();
       }
       verifyingOrVerifiedSymbols.TryRemove(canVerify, out _);
     }
   }
 
-  private void HandleStatusUpdate(ICanVerify canVerify, IImplementationTask implementationTask, IVerificationStatus boogieStatus) {
-    var tokenString = BoogieGenerator.ToDafnyToken(true, implementationTask.Implementation.tok).TokenToString(Options);
+  private void HandleStatusUpdate(ICanVerify canVerify, IVerificationTask verificationTask, IVerificationStatus boogieStatus) {
+    var tokenString = BoogieGenerator.ToDafnyToken(true, verificationTask.Split.Token).TokenToString(Options);
     logger.LogDebug($"Received Boogie status {boogieStatus} for {tokenString}, version {Input.Version}");
 
     updates.OnNext(new BoogieUpdate(transformedProgram!.ProofDependencyManager, canVerify,
-      implementationTask,
+      verificationTask,
       boogieStatus));
   }
 
@@ -461,7 +456,7 @@ public void Dispose() {
     CancelPendingUpdates();
   }
 
-  public static List<DafnyDiagnostic> GetDiagnosticsFromResult(DafnyOptions options, Uri uri, IImplementationTask task, VCResult result) {
+  public static List<DafnyDiagnostic> GetDiagnosticsFromResult(DafnyOptions options, Uri uri, IVerificationTask task, VerificationRunResult result) {
     var errorReporter = new ObservableErrorReporter(options, uri);
     List<DafnyDiagnostic> diagnostics = new();
     errorReporter.Updates.Subscribe(d => diagnostics.Add(d.Diagnostic));
@@ -471,11 +466,11 @@ public static List<DafnyDiagnostic> GetDiagnosticsFromResult(DafnyOptions option
     return diagnostics.OrderBy(d => d.Token.GetLspPosition()).ToList();
   }
 
-  public static void ReportDiagnosticsInResult(DafnyOptions options, IImplementationTask task, VCResult result,
+  public static void ReportDiagnosticsInResult(DafnyOptions options, IVerificationTask task, VerificationRunResult result,
     ErrorReporter errorReporter) {
-    var outcome = GetOutcome(result.outcome);
-    result.counterExamples.Sort(new CounterexampleComparer());
-    foreach (var counterExample in result.counterExamples) //.OrderBy(d => d.GetLocation()))
+    var outcome = GetOutcome(result.Outcome);
+    result.CounterExamples.Sort(new CounterexampleComparer());
+    foreach (var counterExample in result.CounterExamples) //.OrderBy(d => d.GetLocation()))
     {
       errorReporter.ReportBoogieError(counterExample.CreateErrorInformation(outcome, options.ForceBplErrors));
     }
@@ -484,28 +479,28 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, IImplementati
     // 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.Implementation;
+    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);
+      implementation.GetTimeLimit(options), result.CounterExamples);
   }
 
-  private static ConditionGeneration.Outcome GetOutcome(ProverInterface.Outcome outcome) {
+  public static VcOutcome GetOutcome(SolverOutcome outcome) {
     switch (outcome) {
-      case ProverInterface.Outcome.Valid:
-        return ConditionGeneration.Outcome.Correct;
-      case ProverInterface.Outcome.Invalid:
-        return ConditionGeneration.Outcome.Errors;
-      case ProverInterface.Outcome.TimeOut:
-        return ConditionGeneration.Outcome.TimedOut;
-      case ProverInterface.Outcome.OutOfMemory:
-        return ConditionGeneration.Outcome.OutOfMemory;
-      case ProverInterface.Outcome.OutOfResource:
-        return ConditionGeneration.Outcome.OutOfResource;
-      case ProverInterface.Outcome.Undetermined:
-        return ConditionGeneration.Outcome.Inconclusive;
-      case ProverInterface.Outcome.Bounded:
-        return ConditionGeneration.Outcome.ReachedBound;
+      case SolverOutcome.Valid:
+        return VcOutcome.Correct;
+      case SolverOutcome.Invalid:
+        return VcOutcome.Errors;
+      case SolverOutcome.TimeOut:
+        return VcOutcome.TimedOut;
+      case SolverOutcome.OutOfMemory:
+        return VcOutcome.OutOfMemory;
+      case SolverOutcome.OutOfResource:
+        return VcOutcome.OutOfResource;
+      case SolverOutcome.Undetermined:
+        return VcOutcome.Inconclusive;
+      case SolverOutcome.Bounded:
+        return VcOutcome.ReachedBound;
       default:
         throw new ArgumentOutOfRangeException(nameof(outcome), outcome, null);
     }

Source/DafnyCore/Pipeline/Events/BoogieException.cs

@@ -4,4 +4,4 @@
 
 namespace Microsoft.Dafny;
 
-public record BoogieException(ICanVerify CanVerify, IImplementationTask Task, Exception Exception) : ICompilationEvent;
+public record BoogieException(ICanVerify CanVerify, IVerificationTask Task, Exception Exception) : ICompilationEvent;

Source/DafnyCore/Pipeline/Events/BoogieUpdate.cs

@@ -3,7 +3,7 @@
 namespace Microsoft.Dafny;
 
 public record BoogieUpdate(ProofDependencyManager ProofDependencyManager,
-  ICanVerify CanVerify, IImplementationTask ImplementationTask, IVerificationStatus BoogieStatus)
+  ICanVerify CanVerify, IVerificationTask VerificationTask, IVerificationStatus BoogieStatus)
   : ICompilationEvent {
 
 }

Source/DafnyCore/Pipeline/Events/CanVerifyPartsIdentified.cs

@@ -3,5 +3,5 @@
 
 namespace Microsoft.Dafny;
 
-public record CanVerifyPartsIdentified(ICanVerify CanVerify, IReadOnlyList<IImplementationTask> Parts) : ICompilationEvent {
+public record CanVerifyPartsIdentified(ICanVerify CanVerify, IReadOnlyList<IVerificationTask> Parts) : ICompilationEvent {
 }

Source/DafnyCore/Pipeline/IProgramVerifier.cs

@@ -6,15 +6,15 @@
 using VC;
 
 namespace Microsoft.Dafny {
-  public record AssertionBatchResult(Implementation Implementation, VCResult Result);
+  public record AssertionBatchResult(Implementation Implementation, VerificationRunResult Result);
 
-  public record ProgramVerificationTasks(IReadOnlyList<IImplementationTask> Tasks);
+  public record ProgramVerificationTasks(IReadOnlyList<IVerificationTask> Tasks);
 
   /// <summary>
   /// Implementations of this interface are responsible to verify the correctness of a program.
   /// </summary>
   public interface IProgramVerifier {
-    Task<IReadOnlyList<IImplementationTask>> GetVerificationTasksAsync(ExecutionEngine engine,
+    Task<IReadOnlyList<IVerificationTask>> GetVerificationTasksAsync(ExecutionEngine engine,
       ResolutionResult resolution,
       ModuleDefinition moduleDefinition,
       CancellationToken cancellationToken);