From 0988838c40e3536ab30262f1aee29a4c056881e8 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 30 Jan 2024 15:33:10 +0100 Subject: [PATCH] Expose manual split in verification task --- Source/ExecutionEngine/IVerificationStatus.cs | 26 ++++++ Source/ExecutionEngine/IVerificationTask.cs | 22 +++++ ...lementationTask.cs => VerificationTask.cs} | 89 +++++-------------- .../ExecutionEngineTest.cs | 2 +- Source/VCGeneration/ManualSplitFinder.cs | 8 +- Source/VCGeneration/SplitAndVerifyWorker.cs | 2 +- 6 files changed, 78 insertions(+), 71 deletions(-) create mode 100644 Source/ExecutionEngine/IVerificationStatus.cs create mode 100644 Source/ExecutionEngine/IVerificationTask.cs rename Source/ExecutionEngine/{ImplementationTask.cs => VerificationTask.cs} (70%) diff --git a/Source/ExecutionEngine/IVerificationStatus.cs b/Source/ExecutionEngine/IVerificationStatus.cs new file mode 100644 index 000000000..bf31a4b31 --- /dev/null +++ b/Source/ExecutionEngine/IVerificationStatus.cs @@ -0,0 +1,26 @@ +#nullable enable +using VC; + +namespace Microsoft.Boogie; + +public interface IVerificationStatus {} + +/// +/// Results are available +/// +public record Completed(VerificationRunResult Result) : IVerificationStatus; + +/// +/// Scheduled to be run but waiting for resources +/// +public record Queued : IVerificationStatus; + +/// +/// Not scheduled to be run +/// +public record Stale : IVerificationStatus; + +/// +/// Currently being run +/// +public record Running : IVerificationStatus; \ No newline at end of file diff --git a/Source/ExecutionEngine/IVerificationTask.cs b/Source/ExecutionEngine/IVerificationTask.cs new file mode 100644 index 000000000..6986b5c6a --- /dev/null +++ b/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; } + + /// + /// 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. + /// + IObservable? TryRun(); + bool IsIdle { get; } + void Cancel(); +} \ No newline at end of file diff --git a/Source/ExecutionEngine/ImplementationTask.cs b/Source/ExecutionEngine/VerificationTask.cs similarity index 70% rename from Source/ExecutionEngine/ImplementationTask.cs rename to Source/ExecutionEngine/VerificationTask.cs index 810323386..768aa6696 100644 --- a/Source/ExecutionEngine/ImplementationTask.cs +++ b/Source/ExecutionEngine/VerificationTask.cs @@ -11,47 +11,6 @@ namespace Microsoft.Boogie; -public interface IVerificationStatus {} - -/// -/// Results are available -/// -public record Completed(VerificationRunResult Result) : IVerificationStatus; - -/// -/// Scheduled to be run but waiting for resources -/// -public record Queued : IVerificationStatus; - -/// -/// Not scheduled to be run -/// -public record Stale : IVerificationStatus; - -/// -/// Currently being run -/// -public record Running : IVerificationStatus; - -public record BatchCompleted(Split Split, VerificationRunResult VerificationRunResult) : IVerificationStatus; - -public interface IVerificationTask { - IVerificationStatus CacheStatus { get; } - - ProcessedProgram ProcessedProgram { get; } - Split Split { get; } - - /// - /// 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. - /// - IObservable? 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(_ => 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 QueueRun() }); return result; } -} +} \ No newline at end of file diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs index 21ff19330..964816788 100644 --- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs @@ -314,7 +314,7 @@ procedure Foo(x: int) { var expected2 = new List() { 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] diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs index 26ec528df..3644d36f1 100644 --- a/Source/VCGeneration/ManualSplitFinder.cs +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -8,13 +8,13 @@ namespace VCGeneration; public static class ManualSplitFinder { - public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par) + public static IEnumerable FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par) { List focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par); - return focussedImpl.SelectMany(FindManualSplits).ToList(); + return focussedImpl.SelectMany(FindManualSplits); } - private static List FindManualSplits(ManualSplit initialSplit) + private static List FindManualSplits(ManualSplit initialSplit) { Contract.Requires(initialSplit.Implementation != null); Contract.Ensures(Contract.Result>() == null || cce.NonNullElements(Contract.Result>())); @@ -34,7 +34,7 @@ public static List FocusAndSplit(VCGenOptions options, ImplementationRun } } } - var splits = new List(); + var splits = new List(); if (!splitPoints.Any()) { splits.Add(initialSplit); diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index cbe258df6..d0009a2c7 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/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(); if (ManualSplits.Count == 1 && maxSplits > 1) {