Verification task per split (#841)

Dependent Dafny PR: dafny-lang/dafny#5031 ### Changes - Change the API `executionEngine.GetImplementationTasks` to `executionEngine.GetVerificationTasks`, which returns a task for each statically defined assertion batch. When using the split on every assert option, this will return a verification task for each assertion. ### Testing - Added test SplitOnEveryAssertion --------- Co-authored-by: Aaron Tomb <[email protected]>
boogie-org · Feb 2, 2024 · fbf1aa2 · fbf1aa2
1 parent aa88c55
commit fbf1aa2
Show file tree

Hide file tree

Showing 24 changed files with 925 additions and 793 deletions.
diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
@@ -376,8 +376,7 @@ public bool CheckBooleanAttribute(string name, ref bool result)
         }
         else if (kv.Params.Count == 1)
         {
-          var lit = kv.Params[0] as LiteralExpr;
-          if (lit != null && lit.isBool)
+          if (kv.Params[0] is LiteralExpr { isBool: true } lit)
           {
             result = lit.asBool;
             return true;
@@ -395,7 +394,7 @@ public QKeyValue FindAttribute(string name)
     {
       Contract.Requires(name != null);
       QKeyValue res = null;
-      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next)
+      for (QKeyValue kv = Attributes; kv != null; kv = kv.Next)
       {
         if (kv.Key == name)
         {

diff --git a/Source/Core/Token.cs b/Source/Core/Token.cs
@@ -1,3 +1,4 @@
+using System;
 using System.Text;
 using System.Collections.Generic;
 using System.IO;
@@ -6,7 +7,7 @@
 namespace Microsoft.Boogie
 {
   [Immutable]
-  public interface IToken
+  public interface IToken : IComparable<IToken>
   {
     int kind { get; set; } // token kind
     string filename { get; set; } // token file
@@ -88,5 +89,12 @@ public bool IsValid
     {
       get { return this._filename != null; }
     }
+
+    public int CompareTo(IToken other) {
+      if (line != other.line) {
+        return line.CompareTo(other.line);
+      }
+      return col.CompareTo(other.col);
+    }
   }
 }
diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props
@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.0.10</Version>
+    <Version>3.0.11</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -67,7 +67,7 @@ public ExecutionEngine(ExecutionEngineOptions options, VerificationResultCache c
     public ExecutionEngine(ExecutionEngineOptions options, VerificationResultCache cache, CustomStackSizePoolTaskScheduler scheduler) {
       Options = options;
       Cache = cache;
-      checkerPool = new CheckerPool(options);
+      CheckerPool = new CheckerPool(options);
       verifyImplementationSemaphore = new SemaphoreSlim(Options.VcsCores);
 
       largeThreadScheduler = scheduler;
@@ -79,7 +79,7 @@ public static ExecutionEngine CreateWithoutSharedCache(ExecutionEngineOptions op
     }
 
     public ExecutionEngineOptions Options { get; }
-    private readonly CheckerPool checkerPool;
+    public CheckerPool CheckerPool { get; }
     private readonly SemaphoreSlim verifyImplementationSemaphore;
 
     static DateTime FirstRequestStart;
@@ -652,23 +652,23 @@ private Implementation[] GetPrioritizedImplementations(Program program)
       return stablePrioritizedImpls;
     }
 
-    private async Task<PipelineOutcome> VerifyEachImplementation(TextWriter output, ProcessedProgram processedProgram,
+    private async Task<PipelineOutcome> VerifyEachImplementation(TextWriter outputWriter, ProcessedProgram processedProgram,
       PipelineStatistics stats,
       string programId, ErrorReporterDelegate er, string requestId, Implementation[] stablePrioritizedImpls)
     {
-      var consoleCollector = new ConcurrentToSequentialWriteManager(output);
+      var consoleCollector = new ConcurrentToSequentialWriteManager(outputWriter);
 
       var cts = new CancellationTokenSource();
       RequestIdToCancellationTokenSource.AddOrUpdate(requestId, cts, (k, ov) => cts);
 
       var tasks = stablePrioritizedImpls.Select(async (impl, index) => {
         await using var taskWriter = consoleCollector.AppendWriter();
         var implementation = stablePrioritizedImpls[index];
-        var result = (Completed) await EnqueueVerifyImplementation(processedProgram, stats, programId, er,
-          implementation, cts, taskWriter).ToTask(cts.Token);
-        var output = result.Result.GetOutput(Options.Printer, this, stats, er);
+        var result = await EnqueueVerifyImplementation(processedProgram, stats, programId, er,
+          implementation, cts, taskWriter);
+        var output = result.GetOutput(Options.Printer, this, stats, er);
         await taskWriter.WriteAsync(output);
-        return result.Result;
+        return result;
       }).ToList();
       var outcome = PipelineOutcome.VerificationCompleted;
 
@@ -680,7 +680,7 @@ private async Task<PipelineOutcome> VerifyEachImplementation(TextWriter output,
       } catch(TaskCanceledException) {
         outcome = PipelineOutcome.Cancelled;
       } catch(ProverException e) {
-        Options.Printer.ErrorWriteLine(output, "Fatal Error: ProverException: {0}", e.Message);
+        Options.Printer.ErrorWriteLine(outputWriter, "Fatal Error: ProverException: {0}", e.Message);
         outcome = PipelineOutcome.FatalError;
       }
       finally {
@@ -703,7 +703,7 @@ private async Task<PipelineOutcome> VerifyEachImplementation(TextWriter output,
 
     }
 
-    public IReadOnlyList<IImplementationTask> GetImplementationTasks(Program program) {
+    public IReadOnlyList<IVerificationTask> GetVerificationTasks(Program program) {
       program.Resolve(Options);
       program.Typecheck(Options);
 
@@ -713,16 +713,34 @@ public IReadOnlyList<IImplementationTask> GetImplementationTasks(Program program
       Inline(program);
 
       var processedProgram = PreProcessProgramVerification(program);
-      return GetPrioritizedImplementations(program).Select(implementation => new ImplementationTask(this, processedProgram, implementation)).ToList();
+      return GetPrioritizedImplementations(program).SelectMany(implementation =>
+      {
+        var writer = TextWriter.Null;
+        var vcGenerator = new VerificationConditionGenerator(processedProgram.Program, CheckerPool);
+
+        var run = new ImplementationRun(implementation, writer);
+        var collector = new VerificationResultCollector(Options);
+        vcGenerator.PrepareImplementation(run, collector, out _,
+          out var gotoCmdOrigins,
+          out var modelViewInfo);
+
+        var splits = ManualSplitFinder.FocusAndSplit(Options, run, gotoCmdOrigins, vcGenerator).ToList();
+        for (var index = 0; index < splits.Count; index++) {
+          var split = splits[index];
+          split.SplitIndex = index;
+        }
+
+        return splits.Select(split => new VerificationTask(this, processedProgram, split, modelViewInfo));
+      }).ToList();
     }
 
     /// <returns>
     /// The outer task is to wait for a semaphore to let verification start
     /// The inner task is the actual verification of the implementation
     /// </returns>
-    public IObservable<IVerificationStatus> EnqueueVerifyImplementation(
+    public Task<ImplementationRunResult> EnqueueVerifyImplementation(
       ProcessedProgram processedProgram, PipelineStatistics stats,
-      string programId, ErrorReporterDelegate er, Implementation implementation,
+      string programId, ErrorReporterDelegate errorReporterDelegate, Implementation implementation,
       CancellationTokenSource cts,
       TextWriter taskWriter)
     {
@@ -731,33 +749,37 @@ public IObservable<IVerificationStatus> EnqueueVerifyImplementation(
         old.Cancel();
       }
 
-      return EnqueueVerifyImplementation(processedProgram, stats, programId, er, implementation, cts.Token,
-          taskWriter).Finally(() => ImplIdToCancellationTokenSource.TryRemove(id, out old));
+      try
+      {
+        return EnqueueVerifyImplementation(processedProgram, stats, programId, errorReporterDelegate, implementation,
+          cts.Token, taskWriter);
+      }
+      finally
+      {
+        ImplIdToCancellationTokenSource.TryRemove(id, out old);
+      }
     }
 
     /// <returns>
     /// The outer task is to wait for a semaphore to let verification start
     /// The inner task is the actual verification of the implementation
     /// </returns>
-    public IObservable<IVerificationStatus> EnqueueVerifyImplementation(
+    private async Task<ImplementationRunResult> EnqueueVerifyImplementation(
       ProcessedProgram processedProgram, PipelineStatistics stats,
-      string programId, ErrorReporterDelegate er, Implementation implementation,
+      string programId, ErrorReporterDelegate errorReporterDelegate, Implementation implementation,
       CancellationToken cancellationToken,
       TextWriter taskWriter)
     {
-      var queuedTask = verifyImplementationSemaphore.WaitAsync(cancellationToken);
-
-      // Do not report queued if there is no waiting to be done.
-      var queuedNotification = queuedTask.IsCompleted ? Observable.Empty<IVerificationStatus>() : Observable.Return(new Queued());
-
-      return queuedNotification.Concat(Observable.
-        StartAsync(c => queuedTask).
-        SelectMany((_, c) => 
-          VerifyImplementation(processedProgram, stats, er, cancellationToken, implementation, programId, taskWriter).
-          Finally(() => 
-            verifyImplementationSemaphore.Release())
-        )
-      );
+      await verifyImplementationSemaphore.WaitAsync(cancellationToken);
+      try
+      {
+        return await VerifyImplementation(processedProgram, stats, errorReporterDelegate, 
+          cancellationToken, implementation, programId, taskWriter);
+      }
+      finally
+      {
+        verifyImplementationSemaphore.Release();
+      }
     }
 
     private void TraceCachingForBenchmarking(PipelineStatistics stats,
@@ -819,7 +841,7 @@ private static void CleanupRequest(string requestId)
       }
     }
 
-    private IObservable<IVerificationStatus> VerifyImplementation(
+    private async Task<ImplementationRunResult> VerifyImplementation(
       ProcessedProgram processedProgram,
       PipelineStatistics stats,
       ErrorReporterDelegate er,
@@ -831,22 +853,20 @@ private IObservable<IVerificationStatus> VerifyImplementation(
       ImplementationRunResult implementationRunResult = GetCachedVerificationResult(implementation, traceWriter);
       if (implementationRunResult != null) {
         UpdateCachedStatistics(stats, implementationRunResult.VcOutcome, implementationRunResult.Errors);
-        return Observable.Return(new Completed(implementationRunResult));
+        return implementationRunResult;
       }
       Options.Printer.Inform("", traceWriter); // newline
       Options.Printer.Inform($"Verifying {implementation.VerboseName} ...", traceWriter);
 
-      var afterRunningStates = VerifyImplementationWithoutCaching(processedProgram, stats, er, cancellationToken,
-        programId, implementation, traceWriter).Do(status =>
+      var result = await VerifyImplementationWithoutCaching(processedProgram, stats, er, cancellationToken,
+        programId, implementation, traceWriter);
+      if (0 < Options.VerifySnapshots && !string.IsNullOrEmpty(implementation.Checksum))
       {
-        if (status is Completed completed) {
-          if (0 < Options.VerifySnapshots && !string.IsNullOrEmpty(implementation.Checksum)) {
-            Cache.Insert(implementation, completed.Result);
-          }
-          Options.Printer.ReportEndVerifyImplementation(implementation, completed.Result);
-        }
-      });
-      return Observable.Return(new Running()).Concat(afterRunningStates);
+        Cache.Insert(implementation, result);
+      }
+      Options.Printer.ReportEndVerifyImplementation(implementation, result);
+
+      return result;
     }
 
     public ImplementationRunResult GetCachedVerificationResult(Implementation impl, TextWriter output)
@@ -871,25 +891,24 @@ public ImplementationRunResult GetCachedVerificationResult(Implementation impl,
       return null;
     }
 
-    private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(ProcessedProgram processedProgram,
+    private Task<ImplementationRunResult> VerifyImplementationWithoutCaching(ProcessedProgram processedProgram,
       PipelineStatistics stats, ErrorReporterDelegate er, CancellationToken cancellationToken,
       string programId, Implementation impl, TextWriter traceWriter)
     {
-      var verificationResult = new ImplementationRunResult(impl, programId);
 
-      var batchCompleted = new Subject<(Split split, VerificationRunResult vcResult)>();
-      var completeVerification = largeThreadTaskFactory.StartNew(async () =>
+      var resultTask = largeThreadTaskFactory.StartNew(async () =>
       {
-        var vcgen = new VerificationConditionGenerator(processedProgram.Program, checkerPool);
-        vcgen.CachingActionCounts = stats.CachingActionCounts;
-        verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;
+        var verificationResult = new ImplementationRunResult(impl, programId);
+        var vcGen = new VerificationConditionGenerator(processedProgram.Program, CheckerPool);
+        vcGen.CachingActionCounts = stats.CachingActionCounts;
+        verificationResult.ProofObligationCountBefore = vcGen.CumulativeAssertionCount;
         verificationResult.Start = DateTime.UtcNow;
 
         try
         {
-          (verificationResult.VcOutcome, verificationResult.Errors, verificationResult.VCResults) =
-            await vcgen.VerifyImplementation(new ImplementationRun(impl, traceWriter), batchCompleted, cancellationToken);
-          processedProgram.PostProcessResult(vcgen, impl, verificationResult);
+          (verificationResult.VcOutcome, verificationResult.Errors, verificationResult.RunResults) =
+            await vcGen.VerifyImplementation2(new ImplementationRun(impl, traceWriter), cancellationToken);
+          processedProgram.PostProcessResult(vcGen, impl, verificationResult);
         }
         catch (VCGenException e)
         {
@@ -928,20 +947,18 @@ private IObservable<IVerificationStatus> VerifyImplementationWithoutCaching(Proc
           verificationResult.VcOutcome = VcOutcome.SolverException;
         }
 
-        verificationResult.ProofObligationCountAfter = vcgen.CumulativeAssertionCount;
+        verificationResult.ProofObligationCountAfter = vcGen.CumulativeAssertionCount;
         verificationResult.End = DateTime.UtcNow;
         // `TotalProverElapsedTime` does not include the initial cost of starting
         // the SMT solver (unlike `End - Start` in `VerificationResult`).  It
         // may still include the time taken to restart the prover when running
         // with `vcsCores > 1`.
-        verificationResult.Elapsed = vcgen.TotalProverElapsedTime;
-        verificationResult.ResourceCount = vcgen.ResourceCount;
-
-        batchCompleted.OnCompleted();
-        return new Completed(verificationResult);
+        verificationResult.Elapsed = vcGen.TotalProverElapsedTime;
+        verificationResult.ResourceCount = vcGen.ResourceCount;
+        return verificationResult;
       }, cancellationToken).Unwrap();
 
-      return batchCompleted.Select(t => new BatchCompleted(t.split, t.vcResult)).Merge<IVerificationStatus>(Observable.FromAsync(() => completeVerification));
+      return resultTask;
     }
 
 
@@ -1398,7 +1415,7 @@ private static void WriteErrorInformationToXmlSink(XmlSink sink, ErrorInformatio
 
     public void Dispose()
     {
-      checkerPool.Dispose();
+      CheckerPool.Dispose();
       if (taskSchedulerCreatedLocally) {
         largeThreadScheduler.Dispose();
       }

diff --git a/Source/ExecutionEngine/IVerificationStatus.cs b/Source/ExecutionEngine/IVerificationStatus.cs
@@ -0,0 +1,26 @@
+#nullable enable
+using VC;
+
+namespace Microsoft.Boogie;
+
+public interface IVerificationStatus {}
+
+/// <summary>
+/// Results are available
+/// </summary>
+public record Completed(VerificationRunResult Result) : IVerificationStatus;
+
+/// <summary>
+/// Scheduled to be run but waiting for resources
+/// </summary>
+public record Queued : IVerificationStatus;
+
+/// <summary>
+/// Not scheduled to be run
+/// </summary>
+public record Stale : IVerificationStatus;
+
+/// <summary>
+/// Currently being run
+/// </summary>
+public record Running : IVerificationStatus;
diff --git a/Source/ExecutionEngine/IVerificationTask.cs b/Source/ExecutionEngine/IVerificationTask.cs
@@ -0,0 +1,38 @@
+#nullable enable
+using System;
+using System.Diagnostics;
+using VC;
+
+namespace Microsoft.Boogie;
+
+public interface IVerificationTask {
+  IVerificationStatus CacheStatus { get; }
+  ManualSplit Split { get; }
+
+  /// <summary>
+  /// Associated with the verification scope this task occurs in. Multiple tasks can occur in the same scope
+  /// Boogie's term for a verification scope is an Implementation
+  /// </summary>
+  IToken ScopeToken { get; }
+
+  /// <summary>
+  /// Uniquely identifies the verification scope this task occurs in.
+  /// Boogie's term for a verification scope is an Implementation
+  /// </summary>
+  string ScopeId { get; }
+
+  /// <summary>
+  /// Token that identifies where this task originates from
+  /// </summary>
+  IToken Token { get; }
+
+  /// <summary>
+  /// If not running, start running.
+  /// If already running and not cancelled, return null.
+  /// If already running but being cancelled, queue a new run and return its observable.
+  /// If already running but being cancelled, and a new run is queued, return null.
+  /// </summary>
+  IObservable<IVerificationStatus>? TryRun();
+  bool IsIdle { get; }
+  void Cancel();
+}