Filter assertions (#5031)

### Description
- Allow using `--filter-position` to only verify individual assertions.

The implementation relies on a new version of Boogie, which changes the
API so that Boogie returns not a list of implementations but instead of
a list of 'verification tasks', which map to individual SMT executions
or 'assertion batches'. When using `--isolate-assertions`, each
assertion is given such as task, and it becomes easy to filter these
tasks/assertions based on a file position.

#### Background of some of the code changes
This change in the Boogie API means Dafny is not longer updated when all
the tasks for a particular Boogie implementation are finished, which
effects a few things that rely on all tasks in a Boogie implementation
to be done:
 - Computation of redundant assertions
- Gutter icons (maybe it conceptually does not depend on Boogie
implementations, I'm not sure, but the current implementation cares
about Boogie implementations)

There is no change in behavior for the above, but the code had to be
updated so on the Dafny side we track whether everything for a
particular implementation is done.

### How has this been tested?
- Added new cases to the existing littish test `filter.dfy`
- Some gutter icons tests have been updated, which is I think due to an
improvement. The last batch completed + implementation completed steps
are now combined, so two updates that would always immediately follow
each other are now squashed together.

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

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