Verification task per split

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

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

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>

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

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;

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();
+}