Expose manual split in verification task

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,22 @@
+#nullable enable
+using System;
+using VC;
+
+namespace Microsoft.Boogie;
+
+public interface IVerificationTask {
+  IVerificationStatus CacheStatus { get; }
+
+  ProcessedProgram ProcessedProgram { get; }
+  ManualSplit Split { 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();
+}

Source/ExecutionEngine/ImplementationTask.cs → Source/ExecutionEngine/VerificationTask.cs

@@ -11,47 +11,6 @@
 
 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;
-
-public record BatchCompleted(Split Split, VerificationRunResult VerificationRunResult) : IVerificationStatus;
-
-public interface IVerificationTask {
-  IVerificationStatus CacheStatus { get; }
-
-  ProcessedProgram ProcessedProgram { get; }
-  Split Split { 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();
-}
-
 public class VerificationTask : IVerificationTask {
   private readonly ExecutionEngine engine;
   private readonly ModelViewInfo modelViewInfo;
@@ -61,9 +20,9 @@ public class VerificationTask : IVerificationTask {
 
   public ProcessedProgram ProcessedProgram { get; }
 
-  public Split Split { get; }
+  public ManualSplit Split { get; }
 
-  public VerificationTask(ExecutionEngine engine, ProcessedProgram processedProgram, Split split,
+  public VerificationTask(ExecutionEngine engine, ProcessedProgram processedProgram, ManualSplit split,
     ModelViewInfo modelViewInfo) 
   {
     this.engine = engine;
@@ -121,30 +80,30 @@ public void Cancel() {
     StartRun(cancellationSource.Token).ToObservable().
       Catch<IVerificationStatus, OperationCanceledException>(_ => Observable.Return(new Stale())).
       Subscribe(next =>
-    {
-      status.OnNext(next);
-    }, e =>
-    {
-      // Lock so we may do operations after clearing cancellationSource,
-      // which releases our control over the field status.
-      lock (mayAccessCancellationSource)
       {
-        // Clear cancellationSource before calling status.OnError, so ImplementationTask.IsIdle returns true
-        cancellationSource = null;
-        status.OnError(e);
-      }
-    }, () =>
-    {
-      // Lock so we may do operations after clearing cancellationSource,
-      // which releases our control over the field status.
-      lock (mayAccessCancellationSource)
+        status.OnNext(next);
+      }, e =>
       {
-        // Clear cancellationSource before calling status.OnCompleted, so ImplementationTask.IsIdle returns true
-        cancellationSource = null;
+        // Lock so we may do operations after clearing cancellationSource,
+        // which releases our control over the field status.
+        lock (mayAccessCancellationSource)
+        {
+          // Clear cancellationSource before calling status.OnError, so ImplementationTask.IsIdle returns true
+          cancellationSource = null;
+          status.OnError(e);
+        }
+      }, () =>
+      {
+        // Lock so we may do operations after clearing cancellationSource,
+        // which releases our control over the field status.
+        lock (mayAccessCancellationSource)
+        {
+          // Clear cancellationSource before calling status.OnCompleted, so ImplementationTask.IsIdle returns true
+          cancellationSource = null;
 
-        status.OnCompleted();
-      }
-    });
+          status.OnCompleted();
+        }
+      });
 
     return status;
   }
@@ -215,4 +174,4 @@ private IObservable<IVerificationStatus> QueueRun()
     });
     return result;
   }
-}
+}

Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs

@@ -314,7 +314,7 @@ procedure Foo(x: int) {
     var expected2 = new List<IVerificationStatus>() {
       new Running(), finalResult
     };
-    Assert.AreEqual(expected2, statusList2.Where(s => s is not Queued && s is not BatchCompleted));
+    Assert.AreEqual(expected2, statusList2.Where(s => s is not Queued && s is not Completed));
   }
 
   [Test]

Source/VCGeneration/ManualSplitFinder.cs

@@ -8,13 +8,13 @@ namespace VCGeneration;
 
 public static class ManualSplitFinder
 {
-  public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerificationConditionGenerator par)
+  public static IEnumerable<ManualSplit> FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerificationConditionGenerator par)
   {
     List<ManualSplit> focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par);
-    return focussedImpl.SelectMany(FindManualSplits).ToList();
+    return focussedImpl.SelectMany(FindManualSplits);
   }
 
-  private static List<Split /*!*/> FindManualSplits(ManualSplit initialSplit)
+  private static List<ManualSplit /*!*/> FindManualSplits(ManualSplit initialSplit)
   {
     Contract.Requires(initialSplit.Implementation != null);
     Contract.Ensures(Contract.Result<List<Split>>() == null || cce.NonNullElements(Contract.Result<List<Split>>()));
@@ -34,7 +34,7 @@ public static List<Split> FocusAndSplit(VCGenOptions options, ImplementationRun
         }
       }
     }
-    var splits = new List<Split>();
+    var splits = new List<ManualSplit>();
     if (!splitPoints.Any())
     {
       splits.Add(initialSplit);

Source/VCGeneration/SplitAndVerifyWorker.cs

@@ -60,7 +60,7 @@ public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator
 
 
       ResetPredecessors(Implementation.Blocks);
-      ManualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator);
+      ManualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator).ToList<Split>();
 
       if (ManualSplits.Count == 1 && maxSplits > 1)
       {