Filter assertions

Makefile

@@ -62,7 +62,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);