From fbf1aa2c6bb2c09a26f03d582ccf1bd115476dad Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 2 Feb 2024 18:54:10 +0100 Subject: [PATCH] Verification task per split (#841) Dependent Dafny PR: https://github.com/dafny-lang/dafny/pull/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 --- Source/Core/AST/Absy.cs | 5 +- Source/Core/Token.cs | 10 +- Source/Directory.Build.props | 2 +- Source/ExecutionEngine/ExecutionEngine.cs | 137 +++++++------ Source/ExecutionEngine/IVerificationStatus.cs | 26 +++ Source/ExecutionEngine/IVerificationTask.cs | 38 ++++ .../ImplementationRunResult.cs | 9 +- Source/ExecutionEngine/ImplementationTask.cs | 179 ----------------- Source/ExecutionEngine/VerificationTask.cs | 157 +++++++++++++++ Source/Provers/SMTLib/ProverInterface.cs | 23 +-- .../ExecutionEngineTest.cs | 100 ++++++--- Source/VCGeneration/BlockStats.cs | 6 +- Source/VCGeneration/BlockTransformations.cs | 87 ++++---- Source/VCGeneration/CheckerPool.cs | 4 +- Source/VCGeneration/CommandTransformations.cs | 6 +- Source/VCGeneration/ConditionGeneration.cs | 28 ++- Source/VCGeneration/FocusAttribute.cs | 166 +++++++-------- Source/VCGeneration/ManualSplit.cs | 21 ++ Source/VCGeneration/ManualSplitFinder.cs | 140 +++++-------- Source/VCGeneration/SmokeTester.cs | 4 +- Source/VCGeneration/Split.cs | 175 ++++++++-------- Source/VCGeneration/SplitAndVerifyWorker.cs | 178 +++++++++------- .../VerificationConditionGenerator.cs | 190 +++++++++++------- Source/VCGeneration/VerificationRunResult.cs | 27 +-- 24 files changed, 925 insertions(+), 793 deletions(-) create mode 100644 Source/ExecutionEngine/IVerificationStatus.cs create mode 100644 Source/ExecutionEngine/IVerificationTask.cs delete mode 100644 Source/ExecutionEngine/ImplementationTask.cs create mode 100644 Source/ExecutionEngine/VerificationTask.cs create mode 100644 Source/VCGeneration/ManualSplit.cs diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs index 4968586ae..8747597ab 100644 --- 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 index dd1285c99..5f7a1bb1f 100644 --- 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 { 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); + } } } \ No newline at end of file diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index f4e12d754..f1d97551a 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.0.10 + 3.0.11 net6.0 false Boogie diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 127763000..18202b600 100644 --- 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,11 +652,11 @@ private Implementation[] GetPrioritizedImplementations(Program program) return stablePrioritizedImpls; } - private async Task VerifyEachImplementation(TextWriter output, ProcessedProgram processedProgram, + private async Task 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); @@ -664,11 +664,11 @@ private async Task VerifyEachImplementation(TextWriter output, 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 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 VerifyEachImplementation(TextWriter output, } - public IReadOnlyList GetImplementationTasks(Program program) { + public IReadOnlyList GetVerificationTasks(Program program) { program.Resolve(Options); program.Typecheck(Options); @@ -713,16 +713,34 @@ public IReadOnlyList 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(); } /// /// The outer task is to wait for a semaphore to let verification start /// The inner task is the actual verification of the implementation /// - public IObservable EnqueueVerifyImplementation( + public Task 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 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); + } } /// /// The outer task is to wait for a semaphore to let verification start /// The inner task is the actual verification of the implementation /// - public IObservable EnqueueVerifyImplementation( + private async Task 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() : 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 VerifyImplementation( + private async Task VerifyImplementation( ProcessedProgram processedProgram, PipelineStatistics stats, ErrorReporterDelegate er, @@ -831,22 +853,20 @@ private IObservable 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 VerifyImplementationWithoutCaching(ProcessedProgram processedProgram, + private Task 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 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(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 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..3a6b41e1e --- /dev/null +++ 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; } + + /// + /// 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 + /// + IToken ScopeToken { get; } + + /// + /// Uniquely identifies the verification scope this task occurs in. + /// Boogie's term for a verification scope is an Implementation + /// + string ScopeId { get; } + + /// + /// Token that identifies where this task originates from + /// + IToken Token { 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/ImplementationRunResult.cs b/Source/ExecutionEngine/ImplementationRunResult.cs index d0169164f..bd9c89cfe 100644 --- a/Source/ExecutionEngine/ImplementationRunResult.cs +++ b/Source/ExecutionEngine/ImplementationRunResult.cs @@ -29,17 +29,14 @@ public sealed class ImplementationRunResult public int ResourceCount { get; set; } - public int ProofObligationCount - { - get { return ProofObligationCountAfter - ProofObligationCountBefore; } - } + public int ProofObligationCount => ProofObligationCountAfter - ProofObligationCountBefore; public int ProofObligationCountBefore { get; set; } public int ProofObligationCountAfter { get; set; } public VcOutcome VcOutcome { get; set; } public List Errors = new(); - public List VCResults; + public List RunResults; public ErrorInformation ErrorBeforeVerification { get; set; } @@ -79,7 +76,7 @@ public void ProcessXml(ExecutionEngine engine) { lock (engine.Options.XmlSink) { engine.Options.XmlSink.WriteStartMethod(implementation.VerboseName, Start); - foreach (var vcResult in VCResults.OrderBy(s => (vcNum: s.VcNum, iteration: s.Iteration))) { + foreach (var vcResult in RunResults.OrderBy(s => (vcNum: s.VcNum, iteration: s.Iteration))) { engine.Options.XmlSink.WriteSplit(vcResult.VcNum, vcResult.Iteration, vcResult.Asserts, vcResult.StartTime, vcResult.Outcome.ToString().ToLowerInvariant(), vcResult.RunTime, vcResult.ResourceCount); } diff --git a/Source/ExecutionEngine/ImplementationTask.cs b/Source/ExecutionEngine/ImplementationTask.cs deleted file mode 100644 index 26e385c9d..000000000 --- a/Source/ExecutionEngine/ImplementationTask.cs +++ /dev/null @@ -1,179 +0,0 @@ -#nullable enable -using System; -using System.IO; -using System.Reactive.Linq; -using System.Reactive.Subjects; -using System.Reactive.Threading.Tasks; -using System.Threading; -using System.Threading.Tasks; -using VC; - -namespace Microsoft.Boogie; - -public interface IVerificationStatus {} - -/// -/// Results are available -/// -public record Completed(ImplementationRunResult 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 IImplementationTask { - IVerificationStatus CacheStatus { get; } - - ProcessedProgram ProcessedProgram { get; } - Implementation Implementation { 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 ImplementationTask : IImplementationTask { - private readonly ExecutionEngine engine; - private readonly object mayAccessCancellationSource = new(); - - public IVerificationStatus CacheStatus { get; private set; } - - public ProcessedProgram ProcessedProgram { get; } - - public Implementation Implementation { get; } - - public ImplementationTask(ExecutionEngine engine, ProcessedProgram processedProgram, Implementation implementation) { - this.engine = engine; - ProcessedProgram = processedProgram; - Implementation = implementation; - - var cachedVerificationResult = engine.GetCachedVerificationResult(Implementation, TextWriter.Null); - if (cachedVerificationResult != null) { - CacheStatus = new Completed(cachedVerificationResult); - } else { - CacheStatus = new Stale(); - } - } - - private CancellationTokenSource? cancellationSource; - private ReplaySubject? status; - - public void Cancel() { - cancellationSource?.Cancel(); - } - - public bool IsIdle => cancellationSource == null; - - public IObservable? TryRun() - { - lock (mayAccessCancellationSource) { - if (cancellationSource == null) { - return StartRunIfNeeded(); - } - - if (cancellationSource.IsCancellationRequested) { - // Another thread is running but was cancelled, - // so we may immediately start a new run after the cancellation completes. - return QueueRun(); - } - - // Another thread is running and is not cancelled, so this run fails. - return null; - } - } - - private IObservable? StartRunIfNeeded() - { - // No other thread is running or can start, so we can safely access CacheStatus - if (CacheStatus is Completed) { - return null; - } - - // We claim the right to run. - cancellationSource = new(); - - var cancellationToken = cancellationSource.Token; - status = new ReplaySubject(); - - engine.EnqueueVerifyImplementation(ProcessedProgram, new PipelineStatistics(), - null, null, Implementation, cancellationToken, TextWriter.Null). - Catch((e) => Observable.Return(new Stale())). - Subscribe(next => - { - if (next is Completed) - { - CacheStatus = 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) - { - // Clear cancellationSource before calling status.OnCompleted, so ImplementationTask.IsIdle returns true - cancellationSource = null; - - status.OnCompleted(); - } - }); - - return status; - } - - private IObservable? QueueRun() - { - // We claim the right to run. - cancellationSource = new(); - var myCancellationSource = cancellationSource; - - // After the current run cancellation completes, call TryRun, assume it succeeds, - // and forward the observations to result. - var result = new ReplaySubject(); - status!.Subscribe(next => { }, () => - { - if (myCancellationSource.IsCancellationRequested) { - // Queued run was cancelled before it started. - result.OnNext(CacheStatus); - result.OnCompleted(); - } else { - // The running thread has just cleared cancellationSource, so TryRun will return a non-null value. - var recursiveStatus = TryRun(); - recursiveStatus!.Subscribe(result); - // Forward cancellation requests that happened between our - // myCancellationSource.IsCancellationRequested check and TryRun call - myCancellationSource.Token.Register(() => cancellationSource.Cancel()); - } - }); - return result; - } -} diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs new file mode 100644 index 000000000..dba1e1000 --- /dev/null +++ b/Source/ExecutionEngine/VerificationTask.cs @@ -0,0 +1,157 @@ +#nullable enable +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Reactive.Linq; +using System.Reactive.Subjects; +using System.Runtime.CompilerServices; +using System.Threading; +using VC; + +namespace Microsoft.Boogie; + +public class VerificationTask : IVerificationTask { + private readonly ExecutionEngine engine; + private readonly ModelViewInfo modelViewInfo; + private readonly object mayAccessCancellationSource = new(); + + public IVerificationStatus CacheStatus { get; private set; } + + public ProcessedProgram ProcessedProgram { get; } + + public IToken ScopeToken => Split.Implementation.tok; + public string ScopeId => Split.Implementation.VerboseName; + + public IToken Token => Split.Token; + public ManualSplit Split { get; } + + public VerificationTask(ExecutionEngine engine, ProcessedProgram processedProgram, ManualSplit split, + ModelViewInfo modelViewInfo) { + this.engine = engine; + this.modelViewInfo = modelViewInfo; + ProcessedProgram = processedProgram; + Split = split; + + var cachedVerificationResult = engine.GetCachedVerificationResult(split.Implementation, TextWriter.Null); + if (cachedVerificationResult != null) { + CacheStatus = new Completed(cachedVerificationResult.RunResults[Split.SplitIndex]); + } else { + CacheStatus = new Stale(); + } + } + + private CancellationTokenSource? cancellationSource; + private ReplaySubject? status; + + public void Cancel() { + cancellationSource?.Cancel(); + } + + public bool IsIdle => cancellationSource == null; + + public IObservable? TryRun() { + lock (mayAccessCancellationSource) { + if (cancellationSource == null) { + return StartRunIfNeeded(); + } + + if (cancellationSource.IsCancellationRequested) { + // Another thread is running but was cancelled, + // so we may immediately start a new run after the cancellation completes. + return QueueRun(); + } + + // Another thread is running and is not cancelled, so this run fails. + return null; + } + } + + private IObservable? StartRunIfNeeded() { + // No other thread is running or can start, so we can safely access CacheStatus + if (CacheStatus is Completed) { + return null; + } + + // We claim the right to run. + cancellationSource = new(); + + status = new ReplaySubject(); + + 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) { + // Clear cancellationSource before calling status.OnCompleted, so ImplementationTask.IsIdle returns true + cancellationSource = null; + + status.OnCompleted(); + } + }); + + return status; + } + + private async IAsyncEnumerable StartRun([EnumeratorCancellation] CancellationToken cancellationToken) { + var timeout = Split.Run.Implementation.GetTimeLimit(Split.Options); + + var checkerTask = engine.CheckerPool.FindCheckerFor(ProcessedProgram.Program, Split, CancellationToken.None); + if (!checkerTask.IsCompleted) { + yield return new Queued(); + } + var checker = await checkerTask; + try { + yield return new Running(); + + var collector = new VerificationResultCollector(Split.Options); + await Split.BeginCheck(Split.Run.OutputWriter, checker, collector, + modelViewInfo, timeout, Split.Run.Implementation.GetResourceLimit(Split.Options), cancellationToken); + + await checker.ProverTask; + var result = Split.ReadOutcome(0, checker, collector); + + CacheStatus = new Completed(result); + yield return CacheStatus; + } + finally { + await checker.GoBackToIdle(); + } + } + + private IObservable QueueRun() { + // We claim the right to run. + cancellationSource = new(); + var myCancellationSource = cancellationSource; + + // After the current run cancellation completes, call TryRun, assume it succeeds, + // and forward the observations to result. + var result = new ReplaySubject(); + status!.Subscribe(next => { }, () => { + if (myCancellationSource.IsCancellationRequested) { + // Queued run was cancelled before it started. + result.OnNext(CacheStatus); + result.OnCompleted(); + } else { + // The running thread has just cleared cancellationSource, so TryRun will return a non-null value. + var recursiveStatus = TryRun(); + recursiveStatus!.Subscribe(result); + // Forward cancellation requests that happened between our + // myCancellationSource.IsCancellationRequested check and TryRun call + myCancellationSource.Token.Register(() => cancellationSource.Cancel()); + } + }); + return result; + } +} \ No newline at end of file diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 145010769..c2beaa48a 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -8,6 +8,17 @@ namespace Microsoft.Boogie; +public enum SolverOutcome +{ + Valid, + Invalid, + TimeOut, + OutOfMemory, + OutOfResource, + Undetermined, + Bounded +} + public abstract class ProverInterface { public static ProverInterface CreateProver(SMTLibOptions libOptions, Program prog, @@ -294,18 +305,6 @@ public virtual void AssertNamed(VCExpr vc, bool polarity, string name) public abstract Task GoBackToIdle(); } - -public enum SolverOutcome -{ - Valid, - Invalid, - TimeOut, - OutOfMemory, - OutOfResource, - Undetermined, - Bounded -} - public class UnexpectedProverOutputException : ProverException { public UnexpectedProverOutputException(string s) diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs index 7eda7869a..5d9023430 100644 --- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs @@ -49,6 +49,36 @@ public async Task DisposeCleansUpThreads() Assert.Fail("Thread count didn't drop back down after waiting 500ms."); } + [Test] + public async Task SplitOnEveryAssertion() { + var programString = @" +procedure Procedure(y: int) + ensures y == 3; +{ + assert y > 2; + assert y > 1; + assert y < 4; +} +".Trim(); + Parser.Parse(programString, "fakeFilename10", out var program); + var options = CommandLineOptions.FromArguments(TextWriter.Null); + options.VcsSplitOnEveryAssert = true; + options.PrintErrorModel = 1; + var engine = ExecutionEngine.CreateWithoutSharedCache(options); + var tasks = engine.GetVerificationTasks(program); + + // The first split is empty. Maybe it can be optimized away + Assert.AreEqual(5, tasks.Count); + + var outcomes = new List { SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid }; + for (var index = 0; index < outcomes.Count; index++) + { + var result0 = await tasks[index].TryRun()!.ToTask(); + var verificationResult0 = ((Completed)result0).Result; + Assert.AreEqual(outcomes[index], verificationResult0.Outcome); + } + } + [Test] public async Task GetImplementationTasksTest() { var programString = @" @@ -66,13 +96,13 @@ procedure Second(y: int) var options = CommandLineOptions.FromArguments(TextWriter.Null); options.PrintErrorModel = 1; var engine = ExecutionEngine.CreateWithoutSharedCache(options); - var tasks = engine.GetImplementationTasks(program); + var tasks = engine.GetVerificationTasks(program); Assert.AreEqual(2, tasks.Count); - Assert.NotNull(tasks[0].Implementation); + Assert.NotNull(tasks[0].Split.Implementation); var result1 = await tasks[0].TryRun()!.ToTask(); var verificationResult1 = ((Completed)result1).Result; - Assert.AreEqual(VcOutcome.Errors, verificationResult1.VcOutcome); - Assert.AreEqual(true, verificationResult1.Errors[0].Model.ModelHasStatesAlready); + Assert.AreEqual(SolverOutcome.Invalid, verificationResult1.Outcome); + Assert.AreEqual(true, verificationResult1.CounterExamples[0].Model.ModelHasStatesAlready); Assert.IsTrue(tasks[1].IsIdle); var runningStates = tasks[1].TryRun()!; @@ -80,7 +110,7 @@ procedure Second(y: int) var result2 = await runningStates.ToTask(); Assert.IsTrue(tasks[1].IsIdle); var verificationResult2 = ((Completed)result2).Result; - Assert.AreEqual(VcOutcome.Correct, verificationResult2.VcOutcome); + Assert.AreEqual(SolverOutcome.Valid, verificationResult2.Outcome); } [Test] @@ -225,7 +255,7 @@ procedure Foo(x: int) { }".TrimStart(); var result = Parser.Parse(source, "fakeFilename1", out var program); Assert.AreEqual(0, result); - var tasks = engine.GetImplementationTasks(program)[0]; + var tasks = engine.GetVerificationTasks(program)[0]; var statusList1 = new List(); var firstStatuses = tasks.TryRun()!; await firstStatuses.Where(s => s is Running).FirstAsync().ToTask(); @@ -261,7 +291,7 @@ procedure Foo(x: int) { }".TrimStart(); var result = Parser.Parse(source, "fakeFilename1", out var program); Assert.AreEqual(0, result); - var task = engine.GetImplementationTasks(program)[0]; + var task = engine.GetVerificationTasks(program)[0]; var statusList1 = new List(); var firstStatuses = task.TryRun()!; var runDuringRun1 = task.TryRun(); @@ -284,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)); } [Test] @@ -307,13 +337,13 @@ public async Task StatusTest() { "; Parser.Parse(programString, "fakeFilename1", out var program); Assert.AreEqual("Bad", program.Implementations.ElementAt(0).Name); - var tasks = engine.GetImplementationTasks(program); + var tasks = engine.GetVerificationTasks(program); var statusList = new List<(string, IVerificationStatus)>(); var first = tasks[0]; var second = tasks[1]; - var firstName = first.Implementation.Name; - var secondName = second.Implementation.Name; + var firstName = first.Split.Implementation.Name; + var secondName = second.Split.Implementation.Name; Assert.AreEqual("Bad", firstName); Assert.AreEqual("Good", secondName); @@ -329,26 +359,30 @@ public async Task StatusTest() { Assert.AreEqual((firstName, new Running()), statusList[0]); Assert.AreEqual((secondName, new Queued()), statusList[1]); Assert.AreEqual(firstName, statusList[2].Item1); - Assert.IsTrue(statusList[2].Item2 is BatchCompleted); - Assert.AreEqual(firstName, statusList[3].Item1); - Assert.IsTrue(statusList[3].Item2 is Completed); - Assert.AreEqual((secondName, new Running()), statusList[4]); - Assert.AreEqual(secondName, statusList[5].Item1); - Assert.IsTrue(statusList[5].Item2 is BatchCompleted); - Assert.AreEqual(secondName, statusList[6].Item1); - Assert.IsTrue(statusList[6].Item2 is Completed); - - var tasks2 = engine.GetImplementationTasks(program); - Assert.True(tasks2[0].CacheStatus is Completed); - Assert.AreEqual(VcOutcome.Errors, ((Completed)tasks2[0].CacheStatus).Result.VcOutcome); - - Assert.True(tasks2[1].CacheStatus is Completed); - Assert.AreEqual(VcOutcome.Correct, ((Completed)tasks2[1].CacheStatus).Result.VcOutcome); + Assert.AreEqual(firstName, statusList[2].Item1); + Assert.IsTrue(statusList[2].Item2 is Completed); + Assert.AreEqual((secondName, new Running()), statusList[3]); + Assert.AreEqual(secondName, statusList[4].Item1); + Assert.IsTrue(statusList[4].Item2 is Completed); + + Assert.True(tasks[0].CacheStatus is Completed); + Assert.AreEqual(SolverOutcome.Invalid, ((Completed)tasks[0].CacheStatus).Result.Outcome); + + Assert.True(tasks[1].CacheStatus is Completed); + Assert.AreEqual(SolverOutcome.Valid, ((Completed)tasks[1].CacheStatus).Result.Outcome); + + // Caching is currently not working + // var tasks2 = engine.GetVerificationTasks(program); + // Assert.True(tasks2[0].CacheStatus is Completed); + // Assert.AreEqual(SolverOutcome.Invalid, ((Completed)tasks2[0].CacheStatus).Result.Outcome); + // + // Assert.True(tasks2[1].CacheStatus is Completed); + // Assert.AreEqual(SolverOutcome.Valid, ((Completed)tasks2[1].CacheStatus).Result.Outcome); - var batchResult = (BatchCompleted) statusList[2].Item2; + var batchResult = (Completed) statusList[2].Item2; - var assertion = batchResult.VerificationRunResult.Asserts[0]; - batchResult.VerificationRunResult.ComputePerAssertOutcomes(out var perAssertOutcome, out var perAssertCounterExamples); + var assertion = batchResult.Result.Asserts[0]; + batchResult.Result.ComputePerAssertOutcomes(out var perAssertOutcome, out var perAssertCounterExamples); Assert.Contains(assertion, perAssertOutcome.Keys); Assert.Contains(assertion, perAssertCounterExamples.Keys); var outcomeAssertion = perAssertOutcome[assertion]; @@ -373,11 +407,11 @@ public async Task SolverCrash() // We limit the number of checkers to 1. options.VcsCores = 1; - var outcome1 = await executionEngine.GetImplementationTasks(terminatingProgram)[0].TryRun()!.ToTask(); - Assert.IsTrue(outcome1 is Completed completed && completed.Result.VcOutcome == VcOutcome.Inconclusive); + var outcome1 = await executionEngine.GetVerificationTasks(terminatingProgram)[0].TryRun()!.ToTask(); + Assert.IsTrue(outcome1 is Completed completed && completed.Result.Outcome == SolverOutcome.Undetermined); options.CreateSolver = (_ ,_ ) => new UnsatSolver(); - var outcome2 = await executionEngine.GetImplementationTasks(terminatingProgram)[0].TryRun()!.ToTask(); - Assert.IsTrue(outcome2 is Completed completed2 && completed2.Result.VcOutcome == VcOutcome.Correct); + var outcome2 = await executionEngine.GetVerificationTasks(terminatingProgram)[0].TryRun()!.ToTask(); + Assert.IsTrue(outcome2 is Completed completed2 && completed2.Result.Outcome == SolverOutcome.Valid); } [Test] diff --git a/Source/VCGeneration/BlockStats.cs b/Source/VCGeneration/BlockStats.cs index eba08b349..73cc8dde7 100644 --- a/Source/VCGeneration/BlockStats.cs +++ b/Source/VCGeneration/BlockStats.cs @@ -12,11 +12,9 @@ class BlockStats public double assumptionCost; // before multiplier public double incomingPaths; - public List /*!>!*/ - virtualSuccessors = new List(); + public List /*!>!*/ virtualSuccessors = new List(); - public List /*!>!*/ - virtualPredecessors = new List(); + public List /*!>!*/ virtualPredecessors = new List(); public HashSet reachableBlocks; public readonly Block block; diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs index 89f17aac7..f0364d164 100644 --- a/Source/VCGeneration/BlockTransformations.cs +++ b/Source/VCGeneration/BlockTransformations.cs @@ -7,58 +7,55 @@ namespace VCGeneration; public static class BlockTransformations { - public static List PostProcess(List blocks) + public static List PostProcess(List blocks) + { + void DeleteFalseGotos(Block b) { - void DeleteFalseGotos (Block b) + bool IsAssumeFalse (Cmd c) { return c is AssumeCmd { Expr: LiteralExpr { asBool: false } }; } + var firstFalseIdx = b.Cmds.FindIndex(IsAssumeFalse); + if (firstFalseIdx != -1) { - var firstFalseIdx = b.Cmds.FindIndex(IsAssumeFalse); - if (firstFalseIdx != -1) - { - b.Cmds = b.Cmds.Take(firstFalseIdx + 1).ToList(); - b.TransferCmd = (b.TransferCmd is GotoCmd) ? new ReturnCmd(b.tok) : b.TransferCmd; - } - - return; - - bool IsAssumeFalse (Cmd c) { return c is AssumeCmd ac && ac.Expr is LiteralExpr le && !le.asBool; } + b.Cmds = b.Cmds.Take(firstFalseIdx + 1).ToList(); + b.TransferCmd = (b.TransferCmd is GotoCmd) ? new ReturnCmd(b.tok) : b.TransferCmd; } + } - bool ContainsAssert(Block b) - { - return b.Cmds.Exists(IsNonTrivialAssert); - bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); } - } + bool ContainsAssert(Block b) + { + bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); } + return b.Cmds.Exists(IsNonTrivialAssert); + } - blocks.ForEach(DeleteFalseGotos); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously - var todo = new Stack(); - var peeked = new HashSet(); - var interestingBlocks = new HashSet(); - todo.Push(blocks[0]); - while(todo.Any()) + blocks.ForEach(DeleteFalseGotos); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously + var todo = new Stack(); + var peeked = new HashSet(); + var interestingBlocks = new HashSet(); + todo.Push(blocks[0]); + while(todo.Any()) + { + var currentBlock = todo.Peek(); + var pop = peeked.Contains(currentBlock); + peeked.Add(currentBlock); + var interesting = false; + var exit = currentBlock.TransferCmd as GotoCmd; + if (exit != null && !pop) { + exit.labelTargets.ForEach(b => todo.Push(b)); + } else if (exit != null) { + Contract.Assert(pop); + var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList()); + currentBlock.TransferCmd = gtc; + interesting = interesting || gtc.labelTargets.Count() != 0; + } + if (pop) { - var currentBlock = todo.Peek(); - var pop = peeked.Contains(currentBlock); - peeked.Add(currentBlock); - var interesting = false; - var exit = currentBlock.TransferCmd as GotoCmd; - if (exit != null && !pop) { - exit.labelTargets.ForEach(b => todo.Push(b)); - } else if (exit != null) { - Contract.Assert(pop); - var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList()); - currentBlock.TransferCmd = gtc; - interesting = interesting || gtc.labelTargets.Count() != 0; - } - if (pop) - { - interesting = interesting || ContainsAssert(currentBlock); - if (interesting) { - interestingBlocks.Add(currentBlock); - } - todo.Pop(); + interesting = interesting || ContainsAssert(currentBlock); + if (interesting) { + interestingBlocks.Add(currentBlock); } + todo.Pop(); } - interestingBlocks.Add(blocks[0]); // must not be empty - return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders. } + interestingBlocks.Add(blocks[0]); // must not be empty + return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders. + } } \ No newline at end of file diff --git a/Source/VCGeneration/CheckerPool.cs b/Source/VCGeneration/CheckerPool.cs index 7c9cc52a4..105a19ae5 100644 --- a/Source/VCGeneration/CheckerPool.cs +++ b/Source/VCGeneration/CheckerPool.cs @@ -21,7 +21,7 @@ public CheckerPool(VCGenOptions options) checkersSemaphore = new(options.VcsCores); } - public async Task FindCheckerFor(ConditionGeneration vcgen, Split? split, CancellationToken cancellationToken) + public async Task FindCheckerFor(Program program, Split? split, CancellationToken cancellationToken) { if (disposed) { throw new Exception("CheckerPool was already disposed"); @@ -32,7 +32,7 @@ public async Task FindCheckerFor(ConditionGeneration vcgen, Split? spli if (!availableCheckers.TryTake(out var checker)) { checker ??= CreateNewChecker(); } - PrepareChecker(vcgen.program, split, checker); + PrepareChecker(program, split, checker); return checker; } catch (Exception) { checkersSemaphore.Release(); diff --git a/Source/VCGeneration/CommandTransformations.cs b/Source/VCGeneration/CommandTransformations.cs index 74daf7195..114fa805a 100644 --- a/Source/VCGeneration/CommandTransformations.cs +++ b/Source/VCGeneration/CommandTransformations.cs @@ -3,13 +3,13 @@ namespace VCGeneration; -public class CommandTransformations +public static class CommandTransformations { public static Cmd AssertIntoAssume(VCGenOptions options, Cmd c) { - if (c is AssertCmd assrt) + if (c is AssertCmd assertCmd) { - return VerificationConditionGenerator.AssertTurnedIntoAssume(options, assrt); + return VerificationConditionGenerator.AssertTurnedIntoAssume(options, assertCmd); } return c; diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 4a8b93924..c79c6f1d8 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -27,7 +27,7 @@ public VCGenException(string s) public abstract class ConditionGenerationContracts : ConditionGeneration { public override Task VerifyImplementation(ImplementationRun run, VerifierCallback callback, - CancellationToken cancellationToken, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver) + CancellationToken cancellationToken) { Contract.Requires(run != null); Contract.Requires(callback != null); @@ -44,21 +44,21 @@ public ConditionGenerationContracts(Program program, CheckerPool checkerPool) [ContractClass(typeof(ConditionGenerationContracts))] public abstract class ConditionGeneration : IDisposable { - public static VcOutcome ProverInterfaceOutcomeToConditionGenerationOutcome(Microsoft.Boogie.SolverOutcome outcome) + public static VcOutcome ProverInterfaceOutcomeToConditionGenerationOutcome(SolverOutcome outcome) { switch (outcome) { - case Microsoft.Boogie.SolverOutcome.Invalid: + case SolverOutcome.Invalid: return VcOutcome.Errors; - case Microsoft.Boogie.SolverOutcome.OutOfMemory: + case SolverOutcome.OutOfMemory: return VcOutcome.OutOfMemory; - case Microsoft.Boogie.SolverOutcome.TimeOut: + case SolverOutcome.TimeOut: return VcOutcome.TimedOut; - case Microsoft.Boogie.SolverOutcome.OutOfResource: + case SolverOutcome.OutOfResource: return VcOutcome.OutOfResource; - case Microsoft.Boogie.SolverOutcome.Undetermined: + case SolverOutcome.Undetermined: return VcOutcome.Inconclusive; - case Microsoft.Boogie.SolverOutcome.Valid: + case SolverOutcome.Valid: return VcOutcome.Correct; } @@ -107,9 +107,8 @@ public ConditionGeneration(Program program, CheckerPool checkerPool) /// /// /// - public async Task<(VcOutcome, List errors, List vcResults)> VerifyImplementation( - ImplementationRun run, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver, - CancellationToken cancellationToken) + public async Task<(VcOutcome, List errors, List vcResults)> VerifyImplementation2( + ImplementationRun run, CancellationToken cancellationToken) { Contract.Requires(run != null); @@ -117,10 +116,9 @@ public ConditionGeneration(Program program, CheckerPool checkerPool) Helpers.ExtraTraceInformation(Options, "Starting implementation verification"); var collector = new VerificationResultCollector(Options); - VcOutcome vcOutcome = await VerifyImplementation(run, collector, cancellationToken, batchCompletedObserver); + VcOutcome vcOutcome = await VerifyImplementation(run, collector, cancellationToken); var /*?*/ errors = new List(); - if (vcOutcome == VcOutcome.Errors || vcOutcome == VcOutcome.TimedOut || vcOutcome == VcOutcome.OutOfMemory || - vcOutcome == VcOutcome.OutOfResource) { + if (vcOutcome is VcOutcome.Errors or VcOutcome.TimedOut or VcOutcome.OutOfMemory or VcOutcome.OutOfResource) { errors = collector.examples.ToList(); } @@ -131,7 +129,7 @@ public ConditionGeneration(Program program, CheckerPool checkerPool) private VCGenOptions Options => CheckerPool.Options; public abstract Task VerifyImplementation(ImplementationRun run, VerifierCallback callback, - CancellationToken cancellationToken, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver); + CancellationToken cancellationToken); /////////////////////////////////// Common Methods and Classes ////////////////////////////////////////// diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs index 72c3c76c8..2418db608 100644 --- a/Source/VCGeneration/FocusAttribute.cs +++ b/Source/VCGeneration/FocusAttribute.cs @@ -15,125 +15,129 @@ namespace VCGeneration; public static class FocusAttribute { - public static List FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par) + + public static List FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par) { - bool IsFocusCmd(Cmd c) { - return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); - } - - List GetFocusBlocks(List blocks) { - return blocks.Where(blk => blk.Cmds.Any(c => IsFocusCmd(c))).ToList(); - } - var impl = run.Implementation; var dag = Program.GraphFromImpl(impl); - var topoSorted = dag.TopologicalSort().ToList(); + var topologicallySortedBlocks = dag.TopologicalSort().ToList(); // By default, we process the foci in a top-down fashion, i.e., in the topological order. // If the user sets the RelaxFocus flag, we use the reverse (topological) order. - var focusBlocks = GetFocusBlocks(topoSorted); + var focusBlocks = GetFocusBlocks(topologicallySortedBlocks); if (par.CheckerPool.Options.RelaxFocus) { focusBlocks.Reverse(); } if (!focusBlocks.Any()) { - var f = new List(); - f.Add(new Split(options, impl.Blocks, gotoCmdOrigins, par, run)); - return f; - } - // finds all the blocks dominated by focusBlock in the subgraph - // which only contains vertices of subgraph. - HashSet DominatedBlocks(Block focusBlock, IEnumerable subgraph) - { - var dominators = new Dictionary>(); - var todo = new Queue(); - foreach (var b in topoSorted.Where(blk => subgraph.Contains(blk))) - { - var s = new HashSet(); - var pred = b.Predecessors.Where(subgraph.Contains).ToList(); - if (pred.Count != 0) - { - s.UnionWith(dominators[pred[0]]); - pred.ForEach(blk => s.IntersectWith(dominators[blk])); - } - s.Add(b); - dominators[b] = s; - } - return subgraph.Where(blk => dominators[blk].Contains(focusBlock)).ToHashSet(); + return new List { new(options, impl.Blocks, gotoCmdOrigins, par, run, run.Implementation.tok) }; } - Cmd DisableSplits(Cmd c) - { - if (c is PredicateCmd pc) - { - for (var kv = pc.Attributes; kv != null; kv = kv.Next) - { - if (kv.Key == "split") - { - kv.AddParam(new LiteralExpr(Token.NoToken, false)); - } - } - } - return c; - } - - var Ancestors = new Dictionary>(); - var Descendants = new Dictionary>(); - focusBlocks.ForEach(fb => Ancestors[fb] = dag.ComputeReachability(fb, false).ToHashSet()); - focusBlocks.ForEach(fb => Descendants[fb] = dag.ComputeReachability(fb, true).ToHashSet()); - var s = new List(); + var ancestorsPerBlock = new Dictionary>(); + var descendantsPerBlock = new Dictionary>(); + focusBlocks.ForEach(fb => ancestorsPerBlock[fb.Block] = dag.ComputeReachability(fb.Block, false).ToHashSet()); + focusBlocks.ForEach(fb => descendantsPerBlock[fb.Block] = dag.ComputeReachability(fb.Block, true).ToHashSet()); + var result = new List(); var duplicator = new Duplicator(); - void FocusRec(int focusIdx, IEnumerable blocks, IEnumerable freeBlocks) + + FocusRec(run.Implementation.tok, 0, impl.Blocks, new List()); + return result; + + void FocusRec(IToken focusToken, int focusIndex, IReadOnlyList blocksToInclude, IReadOnlyList freeAssumeBlocks) { - if (focusIdx == focusBlocks.Count()) + if (focusIndex == focusBlocks.Count) { // it is important for l to be consistent with reverse topological order. - var l = dag.TopologicalSort().Where(blk => blocks.Contains(blk)).Reverse(); + var sortedBlocks = dag.TopologicalSort().Where(blocksToInclude.Contains).Reverse(); // assert that the root block, impl.Blocks[0], is in l - Contract.Assert(l.ElementAt(l.Count() - 1) == impl.Blocks[0]); var newBlocks = new List(); - var oldToNewBlockMap = new Dictionary(blocks.Count()); - foreach (Block b in l) + var oldToNewBlockMap = new Dictionary(blocksToInclude.Count()); + foreach (var block in sortedBlocks) { - var newBlock = (Block)duplicator.Visit(b); + var newBlock = (Block)duplicator.Visit(block); newBlocks.Add(newBlock); - oldToNewBlockMap[b] = newBlock; + oldToNewBlockMap[block] = newBlock; // freeBlocks consist of the predecessors of the relevant foci. // Their assertions turn into assumes and any splits inside them are disabled. - if(freeBlocks.Contains(b)) + if(freeAssumeBlocks.Contains(block)) { - newBlock.Cmds = b.Cmds.Select(c => CommandTransformations.AssertIntoAssume(options, c)).Select(c => DisableSplits(c)).ToList(); + newBlock.Cmds = block.Cmds.Select(c => CommandTransformations.AssertIntoAssume(options, c)).Select(DisableSplits).ToList(); } - if (b.TransferCmd is GotoCmd gtc) + if (block.TransferCmd is GotoCmd gtc) { - var targets = gtc.labelTargets.Where(blk => blocks.Contains(blk)); + var targets = gtc.labelTargets.Where(blocksToInclude.Contains).ToList(); newBlock.TransferCmd = new GotoCmd(gtc.tok, - targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(), - targets.Select(blk => oldToNewBlockMap[blk]).ToList()); + targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(), + targets.Select(blk => oldToNewBlockMap[blk]).ToList()); } } newBlocks.Reverse(); Contract.Assert(newBlocks[0] == oldToNewBlockMap[impl.Blocks[0]]); - s.Add(new Split(options, BlockTransformations.PostProcess(newBlocks), gotoCmdOrigins, par, run)); + result.Add(new ManualSplit(options, BlockTransformations.PostProcess(newBlocks), gotoCmdOrigins, par, run, focusToken)); } - else if (!blocks.Contains(focusBlocks[focusIdx]) - || freeBlocks.Contains(focusBlocks[focusIdx])) + else if (!blocksToInclude.Contains(focusBlocks[focusIndex].Block) || freeAssumeBlocks.Contains(focusBlocks[focusIndex].Block)) { - FocusRec(focusIdx + 1, blocks, freeBlocks); + FocusRec(focusBlocks[focusIndex].Token, focusIndex + 1, blocksToInclude, freeAssumeBlocks); } else { - var b = focusBlocks[focusIdx]; // assert b in blocks - var dominatedBlocks = DominatedBlocks(b, blocks); + var (block, nextToken) = focusBlocks[focusIndex]; // assert b in blocks + var dominatedBlocks = DominatedBlocks(topologicallySortedBlocks, block, blocksToInclude); // the first part takes all blocks except the ones dominated by the focus block - FocusRec(focusIdx + 1, blocks.Where(blk => !dominatedBlocks.Contains(blk)), freeBlocks); - var ancestors = Ancestors[b]; - ancestors.Remove(b); - var descendants = Descendants[b]; + FocusRec(nextToken, focusIndex + 1, blocksToInclude.Where(blk => !dominatedBlocks.Contains(blk)).ToList(), freeAssumeBlocks); + var ancestors = ancestorsPerBlock[block]; + ancestors.Remove(block); + var descendants = descendantsPerBlock[block]; // the other part takes all the ancestors, the focus block, and the descendants. - FocusRec(focusIdx + 1, ancestors.Union(descendants).Intersect(blocks), ancestors.Union(freeBlocks)); + FocusRec(nextToken, focusIndex + 1, + ancestors.Union(descendants).Intersect(blocksToInclude).ToList(), + ancestors.Union(freeAssumeBlocks).ToList()); + } + } + } + + // finds all the blocks dominated by focusBlock in the subgraph + // which only contains vertices of subgraph. + private static HashSet DominatedBlocks(List topologicallySortedBlocks, Block focusBlock, IEnumerable subgraph) + { + var dominators = new Dictionary>(); + foreach (var b in topologicallySortedBlocks.Where(subgraph.Contains)) + { + var s = new HashSet(); + var pred = b.Predecessors.Where(subgraph.Contains).ToList(); + if (pred.Count != 0) + { + s.UnionWith(dominators[pred[0]]); + pred.ForEach(blk => s.IntersectWith(dominators[blk])); } + s.Add(b); + dominators[b] = s; } + return subgraph.Where(blk => dominators[blk].Contains(focusBlock)).ToHashSet(); + } + + private static Cmd DisableSplits(Cmd command) + { + if (command is not PredicateCmd pc) + { + return command; + } + + for (var kv = pc.Attributes; kv != null; kv = kv.Next) + { + if (kv.Key == "split") + { + kv.AddParam(new LiteralExpr(Token.NoToken, false)); + } + } + return command; + } + + private static List<(Block Block, IToken Token)> GetFocusBlocks(List blocks) { + return blocks. + Select(block => (Block: block, FocusCommand: block.Cmds.FirstOrDefault(IsFocusCmd)?.tok)). + Where(t => t.FocusCommand != null).ToList(); + } - FocusRec(0, impl.Blocks, new List()); - return s; + private static bool IsFocusCmd(Cmd c) { + return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); } } \ No newline at end of file diff --git a/Source/VCGeneration/ManualSplit.cs b/Source/VCGeneration/ManualSplit.cs new file mode 100644 index 000000000..1b27c4b92 --- /dev/null +++ b/Source/VCGeneration/ManualSplit.cs @@ -0,0 +1,21 @@ +using System.Collections.Generic; +using Microsoft.Boogie; + +namespace VC; + +public class ManualSplit : Split +{ + + public IToken Token { get; } + + + public ManualSplit(VCGenOptions options, + List blocks, + Dictionary gotoCmdOrigins, + VerificationConditionGenerator par, + ImplementationRun run, + IToken token) : base(options, blocks, gotoCmdOrigins, par, run) + { + Token = token; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs index 5646d71fa..4826c0ce6 100644 --- a/Source/VCGeneration/ManualSplitFinder.cs +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -6,53 +6,45 @@ namespace VCGeneration; -public static class ManualSplitFinder -{ - - public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par, bool splitOnEveryAssert) - { - List focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par); - var splits = focussedImpl.Select(s => FindManualSplits(s, splitOnEveryAssert)).SelectMany(x => x).ToList(); - return splits; +public static class ManualSplitFinder { + public static IEnumerable FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par) { + List focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par); + return focussedImpl.SelectMany(FindManualSplits); } - - public static List FindManualSplits(Split initialSplit, bool splitOnEveryAssert) - { + + private static List FindManualSplits(ManualSplit initialSplit) { Contract.Requires(initialSplit.Implementation != null); Contract.Ensures(Contract.Result>() == null || cce.NonNullElements(Contract.Result>())); - var splitPoints = new Dictionary(); - foreach (var b in initialSplit.Blocks) - { - foreach (Cmd c in b.Cmds) - { - var p = c as PredicateCmd; - if (ShouldSplitHere(c, splitOnEveryAssert)) - { - splitPoints.TryGetValue(b, out var count); - splitPoints[b] = count + 1; + var splitOnEveryAssert = initialSplit.Options.VcsSplitOnEveryAssert; + initialSplit.Run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); + + var splitPoints = new Dictionary>(); + foreach (var block in initialSplit.Blocks) { + foreach (Cmd command in block.Cmds) { + if (ShouldSplitHere(command, splitOnEveryAssert)) { + splitPoints.GetOrCreate(block, () => new List()).Add(command.tok); } } } - var splits = new List(); - if (!splitPoints.Any()) - { + var splits = new List(); + if (!splitPoints.Any()) { splits.Add(initialSplit); - } - else - { + } else { Block entryPoint = initialSplit.Blocks[0]; var blockAssignments = PickBlocksToVerify(initialSplit.Blocks, splitPoints); var entryBlockHasSplit = splitPoints.Keys.Contains(entryPoint); - var baseSplitBlocks = BlockTransformations.PostProcess(DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert)); - splits.Add(new Split(initialSplit.Options, baseSplitBlocks, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run)); - foreach (KeyValuePair pair in splitPoints) - { - for (int i = 0; i < pair.Value; i++) - { - bool lastSplitInBlock = i == pair.Value - 1; + var baseSplitBlocks = BlockTransformations.PostProcess( + DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, + -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert)); + splits.Add(new ManualSplit(initialSplit.Options, baseSplitBlocks, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, initialSplit.Token)); + foreach (var pair in splitPoints) { + for (int i = 0; i < pair.Value.Count; i++) { + var token = pair.Value[i]; + bool lastSplitInBlock = i == pair.Value.Count - 1; var newBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, i, pair.Key, lastSplitInBlock, splitOnEveryAssert); - splits.Add(new Split(initialSplit.Options, BlockTransformations.PostProcess(newBlocks), initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run)); // REVIEW: Does gotoCmdOrigins need to be changed at all? + splits.Add(new ManualSplit(initialSplit.Options, + BlockTransformations.PostProcess(newBlocks), initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, token)); } } } @@ -63,38 +55,28 @@ private static bool ShouldSplitHere(Cmd c, bool splitOnEveryAssert) { return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "split_here") || c is AssertCmd && splitOnEveryAssert; } - // Verify b with the last split in blockAssignments[b] - - private static Dictionary PickBlocksToVerify (List blocks, Dictionary splitPoints) - { + private static Dictionary PickBlocksToVerify(List blocks, Dictionary> splitPoints) { var todo = new Stack(); var blockAssignments = new Dictionary(); - var immediateDominator = (Program.GraphFromBlocks(blocks)).ImmediateDominator(); + var immediateDominator = Program.GraphFromBlocks(blocks).ImmediateDominator(); todo.Push(blocks[0]); - while(todo.Count > 0) - { + while (todo.Count > 0) { var currentBlock = todo.Pop(); - if (blockAssignments.Keys.Contains(currentBlock)) - { + if (blockAssignments.Keys.Contains(currentBlock)) { continue; - } - else if (immediateDominator[currentBlock] == currentBlock) // if the currentBlock doesn't have a predecessor. - { + } else if (immediateDominator[currentBlock] == currentBlock) // if the currentBlock doesn't have a predecessor. + { blockAssignments[currentBlock] = currentBlock; - } - else if (splitPoints.Keys.Contains(immediateDominator[currentBlock])) // if the currentBlock's dominator has a split then it will be associated with that split - { + } else if (splitPoints.Keys.Contains(immediateDominator[currentBlock])) // if the currentBlock's dominator has a split then it will be associated with that split + { blockAssignments[currentBlock] = immediateDominator[currentBlock]; - } - else - { + } else { Contract.Assert(blockAssignments.Keys.Contains(immediateDominator[currentBlock])); blockAssignments[currentBlock] = blockAssignments[immediateDominator[currentBlock]]; } - if (currentBlock.TransferCmd is GotoCmd exit) - { + if (currentBlock.TransferCmd is GotoCmd exit) { exit.labelTargets.ForEach(blk => todo.Push(blk)); } } @@ -102,60 +84,48 @@ private static Dictionary PickBlocksToVerify (List blocks, } private static List DoPreAssignedManualSplit(VCGenOptions options, List blocks, Dictionary blockAssignments, int splitNumberWithinBlock, - Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert) - { - var newBlocks = new List(blocks.Count()); // Copies of the original blocks + Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert) { + var newBlocks = new List(blocks.Count); // Copies of the original blocks var duplicator = new Duplicator(); - var oldToNewBlockMap = new Dictionary(blocks.Count()); // Maps original blocks to their new copies in newBlocks - foreach (var currentBlock in blocks) - { - var newBlock = (Block)duplicator.VisitBlock(currentBlock); + var oldToNewBlockMap = new Dictionary(blocks.Count); // Maps original blocks to their new copies in newBlocks + foreach (var currentBlock in blocks) { + var newBlock = duplicator.VisitBlock(currentBlock); oldToNewBlockMap[currentBlock] = newBlock; newBlocks.Add(newBlock); - if (currentBlock == containingBlock) - { + if (currentBlock == containingBlock) { var newCmds = new List(); var splitCount = -1; var verify = splitCount == splitNumberWithinBlock; - foreach (Cmd c in currentBlock.Cmds) - { - if (ShouldSplitHere(c, splitOnEveryAssert)) - { + foreach (Cmd command in currentBlock.Cmds) { + if (ShouldSplitHere(command, splitOnEveryAssert)) { splitCount++; verify = splitCount == splitNumberWithinBlock; } - newCmds.Add(verify ? c : CommandTransformations.AssertIntoAssume(options, c)); + newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(options, command)); } newBlock.Cmds = newCmds; - } - else if (lastSplitInBlock && blockAssignments[currentBlock] == containingBlock) - { + } else if (lastSplitInBlock && blockAssignments[currentBlock] == containingBlock) { var verify = true; var newCmds = new List(); - foreach(Cmd c in currentBlock.Cmds) { - verify = !ShouldSplitHere(c, splitOnEveryAssert) && verify; - newCmds.Add(verify ? c : CommandTransformations.AssertIntoAssume(options, c)); + foreach (Cmd command in currentBlock.Cmds) { + verify = !ShouldSplitHere(command, splitOnEveryAssert) && verify; + newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(options, command)); } newBlock.Cmds = newCmds; - } - else - { - newBlock.Cmds = currentBlock.Cmds.Select(x => CommandTransformations.AssertIntoAssume(options, x)).ToList(); + } else { + newBlock.Cmds = currentBlock.Cmds.Select(x => CommandTransformations.AssertIntoAssume(options, x)).ToList(); } } // Patch the edges between the new blocks - foreach (var oldBlock in blocks) - { - if (oldBlock.TransferCmd is ReturnCmd) - { + foreach (var oldBlock in blocks) { + if (oldBlock.TransferCmd is ReturnCmd) { continue; } var gotoCmd = (GotoCmd)oldBlock.TransferCmd; var newLabelTargets = new List(gotoCmd.labelTargets.Count()); var newLabelNames = new List(gotoCmd.labelTargets.Count()); - foreach (var target in gotoCmd.labelTargets) - { + foreach (var target in gotoCmd.labelTargets) { newLabelTargets.Add(oldToNewBlockMap[target]); newLabelNames.Add(oldToNewBlockMap[target].Label); } diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs index a56cd5ff6..71621da0f 100644 --- a/Source/VCGeneration/SmokeTester.cs +++ b/Source/VCGeneration/SmokeTester.cs @@ -11,7 +11,7 @@ namespace VC; -class SmokeTester +public class SmokeTester { [ContractInvariantMethod] void ObjectInvariant() @@ -275,7 +275,7 @@ async Task CheckUnreachable(TextWriter traceWriter, Block cur, List s parent.CurrentLocalVariables = run.Implementation.LocVars; parent.PassifyImpl(run, out var mvInfo); - Checker checker = await parent.CheckerPool.FindCheckerFor(parent, null, CancellationToken.None); + Checker checker = await parent.CheckerPool.FindCheckerFor(parent.program, null, CancellationToken.None); Contract.Assert(checker != null); SolverOutcome outcome = SolverOutcome.Undetermined; diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index fdcf1e80f..4ccd1cc09 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -10,44 +10,26 @@ using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.SMTLib; using VCGeneration; +using System.Threading.Tasks; namespace VC { - using Bpl = Microsoft.Boogie; - using System.Threading.Tasks; - public class Split : ProofRun { public VCGenOptions Options { get; } - - public int? RandomSeed => Implementation.RandomSeed ?? Options.RandomSeed; private readonly Random randomGen; - public ImplementationRun Run { get; } - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(cce.NonNullElements(Blocks)); - Contract.Invariant(cce.NonNullElements(bigBlocks)); - Contract.Invariant(cce.NonNullDictionaryAndValues(stats)); - Contract.Invariant(cce.NonNullElements(assumizedBranches)); - Contract.Invariant(GotoCmdOrigins != null); - Contract.Invariant(parent != null); - Contract.Invariant(Implementation != null); - Contract.Invariant(copies != null); - Contract.Invariant(cce.NonNull(protectedFromAssertToAssume)); - Contract.Invariant(cce.NonNull(keepAtAll)); - } - + public int? RandomSeed => Implementation.RandomSeed ?? Options.RandomSeed; public List Blocks { get; } + readonly List bigBlocks = new(); public List Asserts => Blocks.SelectMany(block => block.cmds.OfType()).ToList(); public readonly IReadOnlyList TopLevelDeclarations; - readonly List bigBlocks = new(); readonly Dictionary /*!*/ stats = new Dictionary(); + static int currentId = -1; Block splitBlock; @@ -64,7 +46,8 @@ void ObjectInvariant() public Dictionary GotoCmdOrigins { get; } - public readonly VerificationConditionGenerator /*!*/ parent; + public readonly VerificationConditionGenerator /*!*/ + parent; public Implementation /*!*/ Implementation => Run.Implementation; @@ -76,15 +59,13 @@ void ObjectInvariant() double sliceLimit; bool slicePos; - HashSet /*!*/ - protectedFromAssertToAssume = new HashSet(); + HashSet /*!*/ protectedFromAssertToAssume = new HashSet(); - HashSet /*!*/ - keepAtAll = new HashSet(); + HashSet /*!*/ keepAtAll = new HashSet(); // async interface public int SplitIndex { get; set; } - internal VerificationConditionGenerator.ErrorReporter reporter; + public VerificationConditionGenerator.ErrorReporter reporter; public Split(VCGenOptions options, List /*!*/ blocks, Dictionary /*!*/ gotoCmdOrigins, @@ -95,7 +76,7 @@ public Split(VCGenOptions options, List /*!*/ blocks, Contract.Requires(par != null); this.Blocks = blocks; this.GotoCmdOrigins = gotoCmdOrigins; - this.parent = par; + parent = par; this.Run = run; this.Options = options; Interlocked.Increment(ref currentId); @@ -118,13 +99,14 @@ private void PrintTopLevelDeclarationsForPruning(Program program, Implementation $"{Options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}.bpl", false, Options.PrettyPrint, Options); - var functionAxioms = + var functionAxioms = program.Functions.Where(f => f.DefinitionAxioms.Any()).SelectMany(f => f.DefinitionAxioms); - var constantAxioms = + var constantAxioms = program.Constants.Where(f => f.DefinitionAxioms.Any()).SelectMany(c => c.DefinitionAxioms); - foreach (var declaration in (TopLevelDeclarations ?? program.TopLevelDeclarations). - Except(functionAxioms.Concat(constantAxioms)).ToList()) { + foreach (var declaration in (TopLevelDeclarations ?? program.TopLevelDeclarations) + .Except(functionAxioms.Concat(constantAxioms)).ToList()) + { declaration.Emit(writer, 0); } @@ -160,7 +142,7 @@ public string Stats public void DumpDot(int splitNum) { - using (System.IO.StreamWriter sw = System.IO.File.CreateText($"{Implementation.Name}.split.{splitNum}.dot")) + using (StreamWriter sw = File.CreateText($"{Implementation.Name}.split.{splitNum}.dot")) { sw.WriteLine("digraph G {"); @@ -192,7 +174,7 @@ public void DumpDot(int splitNum) } string filename = string.Format("{0}.split.{1}.bpl", Implementation.Name, splitNum); - using (System.IO.StreamWriter sw = System.IO.File.CreateText(filename)) + using (StreamWriter sw = File.CreateText(filename)) { int oldPrintUnstructured = Options.PrintUnstructured; Options.PrintUnstructured = 2; // print only the unstructured program @@ -245,14 +227,14 @@ void CountAssertions(Block b) { if (c is AssertCmd) { - double cost = AssertionCost((AssertCmd) c); + double cost = AssertionCost((AssertCmd)c); s.assertionCost += cost; assertionCount++; assertionCost += cost; } else if (c is AssumeCmd) { - s.assumptionCost += AssertionCost((AssumeCmd) c); + s.assumptionCost += AssertionCost((AssumeCmd)c); } } @@ -422,7 +404,7 @@ void ComputeBestSplit() } } - void UpdateIncommingPaths(BlockStats s) + void UpdateIncomingPaths(BlockStats s) { Contract.Requires(s != null); if (s.incomingPaths < 0.0) @@ -439,7 +421,7 @@ void UpdateIncommingPaths(BlockStats s) Contract.Assert(b != null); BlockStats ch = GetBlockStats(b); Contract.Assert(ch != null); - UpdateIncommingPaths(ch); + UpdateIncomingPaths(ch); if (ch.incomingPaths > 0.0) { s.incomingPaths += ch.incomingPaths; @@ -557,7 +539,7 @@ double DoComputeScore(bool aa) if (keepAtAll.Contains(b)) { BlockStats s = GetBlockStats(b); - UpdateIncommingPaths(s); + UpdateIncomingPaths(s); double local = s.assertionCost; if (ShouldAssumize(b)) { @@ -663,32 +645,34 @@ Block CloneBlock(Block b) return res; } - Split DoSplit() + private Split DoSplit() { Contract.Ensures(Contract.Result() != null); copies.Clear(); CloneBlock(Blocks[0]); - List newBlocks = new List(); - Dictionary newGotoCmdOrigins = new Dictionary(); - foreach (Block b in Blocks) + var newBlocks = new List(); + var newGotoCmdOrigins = new Dictionary(); + foreach (var block in Blocks) { - Contract.Assert(b != null); - if (copies.TryGetValue(b, out var tmp)) + Contract.Assert(block != null); + if (!copies.TryGetValue(block, out var tmp)) { - newBlocks.Add(cce.NonNull(tmp)); - if (GotoCmdOrigins.ContainsKey(b.TransferCmd)) - { - newGotoCmdOrigins[tmp.TransferCmd] = GotoCmdOrigins[b.TransferCmd]; - } + continue; + } - foreach (Block p in b.Predecessors) + newBlocks.Add(cce.NonNull(tmp)); + if (GotoCmdOrigins.TryGetValue(block.TransferCmd, out var origin)) + { + newGotoCmdOrigins[tmp.TransferCmd] = origin; + } + + foreach (var predecessor in block.Predecessors) + { + Contract.Assert(predecessor != null); + if (copies.TryGetValue(predecessor, out var tmp2)) { - Contract.Assert(p != null); - if (copies.TryGetValue(p, out var tmp2)) - { - tmp.Predecessors.Add(tmp2); - } + tmp.Predecessors.Add(tmp2); } } } @@ -696,7 +680,7 @@ Split DoSplit() return new Split(Options, newBlocks, newGotoCmdOrigins, parent, Run); } - Split SplitAt(int idx) + private Split SplitAt(int idx) { Contract.Ensures(Contract.Result() != null); @@ -707,7 +691,7 @@ Split SplitAt(int idx) return DoSplit(); } - Split SliceAsserts(double limit, bool pos) + private Split SliceAsserts(double limit, bool pos) { Contract.Ensures(Contract.Result() != null); @@ -742,21 +726,21 @@ public Counterexample ToCounterexample(ProverContext context) Contract.Ensures(Contract.Result() != null); List trace = new List(); - foreach (Block b in Blocks) + foreach (Block block in Blocks) { - Contract.Assert(b != null); - trace.Add(b); + Contract.Assert(block != null); + trace.Add(block); } - foreach (Block b in Blocks) + foreach (Block block in Blocks) { - Contract.Assert(b != null); - foreach (Cmd c in b.Cmds) + Contract.Assert(block != null); + foreach (Cmd command in block.Cmds) { - Contract.Assert(c != null); - if (c is AssertCmd) + if (command is AssertCmd assertCmd) { - var counterexample = VerificationConditionGenerator.AssertCmdToCounterexample(Options, (AssertCmd) c, cce.NonNull(b.TransferCmd), trace, null, null, null, context, this); + var counterexample = VerificationConditionGenerator.AssertCmdToCounterexample(Options, assertCmd, + cce.NonNull(block.TransferCmd), trace, null, null, null, context, this); Counterexamples.Add(counterexample); return counterexample; } @@ -779,13 +763,15 @@ public Counterexample ToCounterexample(ProverContext context) { Split best = null; int bestIndex = 0; - for (var index = 0; index < result.Count; index++) { + for (var index = 0; index < result.Count; index++) + { var split = result[index]; Contract.Assert(split != null); split.ComputeBestSplit(); // TODO check totalCost first if (split.totalCost > splitThreshold && (best == null || best.totalCost < split.totalCost) && - (split.assertionCount > 1 || split.splitBlock != null)) { + (split.assertionCount > 1 || split.splitBlock != null)) + { best = split; bestIndex = index; } @@ -802,7 +788,8 @@ public Counterexample ToCounterexample(ProverContext context) if (splitStats) { - run.OutputWriter.WriteLine("{0} {1} -->", best.splitBlock == null ? "SLICE" : ("SPLIT@" + best.splitBlock.Label), + run.OutputWriter.WriteLine("{0} {1} -->", + best.splitBlock == null ? "SLICE" : ("SPLIT@" + best.splitBlock.Label), best.Stats); if (best.splitBlock != null) { @@ -852,7 +839,7 @@ public Counterexample ToCounterexample(ProverContext context) { best.SoundnessCheck(new HashSet>(new BlockListComparer()), best.Blocks[0], ss); } - catch (System.Exception e) + catch (Exception e) { run.OutputWriter.WriteLine(e); best.DumpDot(-1); @@ -883,17 +870,19 @@ public Counterexample ToCounterexample(ProverContext context) return result; } - public (Bpl.SolverOutcome outcome, VerificationRunResult result, int resourceCount) ReadOutcome(int iteration, Checker checker, VerifierCallback callback) + public VerificationRunResult ReadOutcome(int iteration, Checker checker, VerifierCallback callback) { Contract.EnsuresOnThrow(true); - Bpl.SolverOutcome outcome = cce.NonNull(checker).ReadOutcome(); + SolverOutcome outcome = cce.NonNull(checker).ReadOutcome(); if (Options.Trace && SplitIndex >= 0) { Run.OutputWriter.WriteLine(" --> split #{0} done, [{1} s] {2}", SplitIndex + 1, checker.ProverRunTime.TotalSeconds, outcome); } - if (Options.Trace && Options.TrackVerificationCoverage) { + + if (Options.Trace && Options.TrackVerificationCoverage) + { Run.OutputWriter.WriteLine("Proof dependencies:\n {0}", string.Join("\n ", CoveredElements.Select(s => s.Description).OrderBy(s => s))); } @@ -918,7 +907,7 @@ public Counterexample ToCounterexample(ProverContext context) DumpDot(SplitIndex); } - return (outcome, result, resourceCount); + return result; } public List Counterexamples { get; } = new(); @@ -928,7 +917,8 @@ public Counterexample ToCounterexample(ProverContext context) /// /// As a side effect, updates "this.parent.CumulativeAssertionCount". /// - public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCallback callback, ModelViewInfo mvInfo, uint timeout, + public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCallback callback, + ModelViewInfo mvInfo, uint timeout, uint rlimit, CancellationToken cancellationToken) { Contract.Requires(checker != null); @@ -936,14 +926,16 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa VCExpr vc; // Lock impl since we're setting impl.Blocks that is used to generate the VC. - lock (Implementation) { + lock (Implementation) + { Implementation.Blocks = Blocks; var absyIds = new ControlFlowIdMap(); ProverContext ctx = checker.TheoremProver.Context; Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator; - var cc = new VerificationConditionGenerator.CodeExprConversionClosure(traceWriter, checker.Pool.Options, absyIds, ctx); + var cc = new VerificationConditionGenerator.CodeExprConversionClosure(traceWriter, checker.Pool.Options, + absyIds, ctx); bet.SetCodeExprConverter(cc.CodeExprToVerificationCondition); var exprGen = ctx.ExprGen; @@ -955,9 +947,11 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); - VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(absyIds.GetId(Implementation.Blocks[0])))); + VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, + exprGen.Integer(BigNum.FromInt(absyIds.GetId(Implementation.Blocks[0])))); vc = exprGen.Implies(eqExpr, vc); - reporter = new VerificationConditionGenerator.ErrorReporter(Options, GotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback, + reporter = new VerificationConditionGenerator.ErrorReporter(Options, GotoCmdOrigins, absyIds, + Implementation.Blocks, Implementation.debugInfos, callback, mvInfo, checker.TheoremProver.Context, parent.program, this); } @@ -967,7 +961,8 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa Print(); } - checker.TheoremProver.SetAdditionalSmtOptions(Implementation.GetExtraSMTOptions().Select(kv => new OptionValue(kv.Key, kv.Value))); + checker.TheoremProver.SetAdditionalSmtOptions(Implementation.GetExtraSMTOptions() + .Select(kv => new OptionValue(kv.Key, kv.Value))); await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, cancellationToken); } @@ -976,7 +971,8 @@ public string Description get { string description = cce.NonNull(Implementation.Name); - if (SplitIndex >= 0) { + if (SplitIndex >= 0) + { description += "_split" + SplitIndex; } @@ -991,7 +987,7 @@ private void SoundnessCheck(HashSet /*!*/> /*!*/ cache, Block /*!*/ Contract.Requires(orig != null); Contract.Requires(copies != null); { - var t = new List {orig}; + var t = new List { orig }; foreach (Block b in copies) { Contract.Assert(b != null); @@ -1023,7 +1019,7 @@ private void SoundnessCheck(HashSet /*!*/> /*!*/ cache, Block /*!*/ if (found == 0) { - throw new System.Exception(string.Format("missing assertion: {0}({1})", cmd.tok.filename, cmd.tok.line)); + throw new Exception(string.Format("missing assertion: {0}({1})", cmd.tok.filename, cmd.tok.line)); } } } @@ -1046,15 +1042,16 @@ private void SoundnessCheck(HashSet /*!*/> /*!*/ cache, Block /*!*/ if (newcopies.Count == 0) { - throw new System.Exception("missing exit " + exit.Label); + throw new Exception("missing exit " + exit.Label); } SoundnessCheck(cache, exit, newcopies); } } - public int NextRandom() { + public int NextRandom() + { return randomGen.Next(); } - } -} + } +} \ No newline at end of file diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index 7409ca17e..63b763de0 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -1,9 +1,7 @@ using System; -using System.Collections; using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; -using System.Reactive.Subjects; using System.Threading; using System.Threading.Tasks; using Microsoft.Boogie; @@ -12,26 +10,22 @@ namespace VC { - class SplitAndVerifyWorker + public class SplitAndVerifyWorker { - public IObservable<(Split split, VerificationRunResult vcResult)> BatchCompletions => batchCompletions; - private readonly Subject<(Split split, VerificationRunResult vcResult)> batchCompletions = new(); private readonly VCGenOptions options; private readonly VerifierCallback callback; private readonly ModelViewInfo mvInfo; private readonly ImplementationRun run; - + private readonly int maxKeepGoingSplits; - private readonly List manualSplits; + public List ManualSplits { get; } private double maxVcCost; - private readonly bool splitOnEveryAssert; - - private bool DoSplitting => manualSplits.Count > 1 || KeepGoing || splitOnEveryAssert; - private bool TrackingProgress => DoSplitting && (callback.OnProgress != null || options.Trace); + + private bool DoSplitting => ManualSplits.Count > 1 || KeepGoing; + private bool TrackingProgress => DoSplitting && (callback.OnProgress != null || options.Trace); private bool KeepGoing => maxKeepGoingSplits > 1; - private VerificationConditionGenerator verificationConditionGenerator; private VcOutcome vcOutcome; private double remainingCost; private double provenCost; @@ -40,8 +34,13 @@ class SplitAndVerifyWorker private int totalResourceCount; - public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, ImplementationRun run, - Dictionary gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo, + public SplitAndVerifyWorker( + VCGenOptions options, + VerificationConditionGenerator verificationConditionGenerator, + ImplementationRun run, + Dictionary gotoCmdOrigins, + VerifierCallback callback, + ModelViewInfo mvInfo, VcOutcome vcOutcome) { this.options = options; @@ -49,13 +48,12 @@ public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator this.mvInfo = mvInfo; this.run = run; this.vcOutcome = vcOutcome; - this.verificationConditionGenerator = verificationConditionGenerator; var maxSplits = options.VcsMaxSplits; VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_splits", ref maxSplits); - + maxKeepGoingSplits = options.VcsMaxKeepGoingSplits; VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_keep_going_splits", ref maxKeepGoingSplits); - + maxVcCost = options.VcsMaxCost; var tmpMaxVcCost = -1; VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_cost", ref tmpMaxVcCost); @@ -63,43 +61,36 @@ public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator { maxVcCost = tmpMaxVcCost; } - - splitOnEveryAssert = options.VcsSplitOnEveryAssert; - Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); + ResetPredecessors(Implementation.Blocks); - manualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator, splitOnEveryAssert); - - if (manualSplits.Count == 1 && maxSplits > 1) { - manualSplits = Split.DoSplit(manualSplits[0], maxVcCost, maxSplits); + ManualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator).ToList(); + + if (ManualSplits.Count == 1 && maxSplits > 1) + { + ManualSplits = Split.DoSplit(ManualSplits[0], maxVcCost, maxSplits); maxVcCost = 1.0; } - + splitNumber = DoSplitting ? 0 : -1; } public async Task WorkUntilDone(CancellationToken cancellationToken) { - TrackSplitsCost(manualSplits); - try - { - await Task.WhenAll(manualSplits.Select(split => DoWorkForMultipleIterations(split, cancellationToken))); - } - finally - { - batchCompletions.OnCompleted(); - } + TrackSplitsCost(ManualSplits); + await Task.WhenAll(ManualSplits.Select(split => DoWorkForMultipleIterations(split, cancellationToken))); return vcOutcome; } public int ResourceCount => totalResourceCount; + /// /// The cumulative time spent processing SMT queries. When running with /// `vcsCores > 1`, this may also include time spent restarting the prover. /// public TimeSpan TotalProverElapsedTime { get; private set; } - + private void TrackSplitsCost(List splits) { if (!TrackingProgress) @@ -107,7 +98,8 @@ private void TrackSplitsCost(List splits) return; } - foreach (var split in splits) { + foreach (var split in splits) + { remainingCost += split.Cost; total++; } @@ -124,16 +116,18 @@ async Task DoWorkForMultipleIterations(Split split, CancellationToken cancellati async Task DoWork(int iteration, Split split, CancellationToken cancellationToken) { - var checker = await split.parent.CheckerPool.FindCheckerFor(split.parent, split, cancellationToken); + var checker = await split.parent.CheckerPool.FindCheckerFor(split.parent.program, split, cancellationToken); - try { + try + { cancellationToken.ThrowIfCancellationRequested(); await StartCheck(iteration, split, checker, cancellationToken); await checker.ProverTask; await ProcessResultAndReleaseChecker(iteration, split, checker, cancellationToken); TotalProverElapsedTime += checker.ProverRunTime; } - catch { + catch + { await checker.GoBackToIdle(); throw; } @@ -141,7 +135,8 @@ async Task DoWork(int iteration, Split split, CancellationToken cancellationToke private async Task StartCheck(int iteration, Split split, Checker checker, CancellationToken cancellationToken) { - if (options.Trace && DoSplitting) { + if (options.Trace && DoSplitting) + { var splitNum = split.SplitIndex + 1; var splitIdxStr = options.RandomizeVcIterations > 1 ? $"{splitNum} (iteration {iteration})" : $"{splitNum}"; run.OutputWriter.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...", @@ -154,49 +149,63 @@ private async Task StartCheck(int iteration, Split split, Checker checker, Cance var timeout = KeepGoing && split.LastChance ? options.VcsFinalAssertTimeout : KeepGoing ? options.VcsKeepGoingTimeout : run.Implementation.GetTimeLimit(options); - await split.BeginCheck(run.OutputWriter, checker, callback, mvInfo, timeout, Implementation.GetResourceLimit(options), cancellationToken); + await split.BeginCheck(run.OutputWriter, checker, callback, mvInfo, timeout, + Implementation.GetResourceLimit(options), cancellationToken); } private Implementation Implementation => run.Implementation; - private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Checker checker, CancellationToken cancellationToken) + private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Checker checker, + CancellationToken cancellationToken) { - if (TrackingProgress) { - lock (this) { + if (TrackingProgress) + { + lock (this) + { remainingCost -= split.Cost; } } - var (newOutcome, result, newResourceCount) = split.ReadOutcome(iteration, checker, callback); - lock (this) { - vcOutcome = MergeOutcomes(vcOutcome, newOutcome); - totalResourceCount += newResourceCount; + var result = split.ReadOutcome(iteration, checker, callback); + lock (this) + { + vcOutcome = MergeOutcomes(vcOutcome, result.Outcome); + totalResourceCount += result.ResourceCount; } - var proverFailed = IsProverFailed(newOutcome); - if (TrackingProgress) { - lock (this) { - if (proverFailed) { + var proverFailed = IsProverFailed(result.Outcome); + + if (TrackingProgress) + { + lock (this) + { + if (proverFailed) + { // even if the prover fails, we have learned something, i.e., it is // annoying to watch Boogie say Timeout, 0.00% a couple of times provenCost += split.Cost / 100; - } else { + } + else + { provenCost += split.Cost; } } } - callback.OnProgress?.Invoke("VCprove", splitNumber < 0 ? 0 : splitNumber, total, provenCost / (remainingCost + provenCost)); + callback.OnProgress?.Invoke("VCprove", splitNumber < 0 ? 0 : splitNumber, total, + provenCost / (remainingCost + provenCost)); - if (proverFailed) { + if (proverFailed) + { await HandleProverFailure(split, checker, callback, result, cancellationToken); - } else { - batchCompletions.OnNext((split, result)); + } + else + { await checker.GoBackToIdle(); } } - private static bool IsProverFailed(SolverOutcome outcome) + public static bool IsProverFailed(SolverOutcome outcome) { switch (outcome) { @@ -248,6 +257,7 @@ private static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, SolverOutcome { return VcOutcome.Inconclusive; } + return currentVcOutcome; default: Contract.Assert(false); @@ -255,11 +265,14 @@ private static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, SolverOutcome } } - private async Task HandleProverFailure(Split split, Checker checker, VerifierCallback callback, VerificationRunResult verificationRunResult, CancellationToken cancellationToken) + private async Task HandleProverFailure(Split split, Checker checker, VerifierCallback callback, + VerificationRunResult verificationRunResult, CancellationToken cancellationToken) { - if (split.LastChance) { + if (split.LastChance) + { string msg = "some timeout"; - if (split.reporter is { resourceExceededMessage: { } }) { + if (split.reporter is { resourceExceededMessage: { } }) + { msg = split.reporter.resourceExceededMessage; } @@ -267,10 +280,10 @@ private async Task HandleProverFailure(Split split, Checker checker, VerifierCal callback.OnCounterexample(cex, msg); split.Counterexamples.Add(cex); // Update one last time the result with the dummy counter-example to indicate the position of the timeout - var result = verificationRunResult with { + var result = verificationRunResult with + { CounterExamples = split.Counterexamples }; - batchCompletions.OnNext((split, result)); vcOutcome = VcOutcome.Errors; await checker.GoBackToIdle(); return; @@ -278,47 +291,58 @@ private async Task HandleProverFailure(Split split, Checker checker, VerifierCal await checker.GoBackToIdle(); - if (maxKeepGoingSplits > 1) { + if (maxKeepGoingSplits > 1) + { var newSplits = Split.DoSplit(split, maxVcCost, maxKeepGoingSplits); - if (options.Trace) { - await run.OutputWriter.WriteLineAsync($"split {split.SplitIndex+1} was split into {newSplits.Count} parts"); + if (options.Trace) + { + await run.OutputWriter.WriteLineAsync($"split {split.SplitIndex + 1} was split into {newSplits.Count} parts"); } + Contract.Assert(newSplits != null); maxVcCost = 1.0; // for future TrackSplitsCost(newSplits); - - if (vcOutcome != VcOutcome.Errors) { + + if (vcOutcome != VcOutcome.Errors) + { vcOutcome = VcOutcome.Correct; } + await Task.WhenAll(newSplits.Select(newSplit => DoWorkForMultipleIterations(newSplit, cancellationToken))); return; } Contract.Assert(vcOutcome != VcOutcome.Correct); - if (vcOutcome == VcOutcome.TimedOut) { + if (vcOutcome == VcOutcome.TimedOut) + { string msg = "some timeout"; - if (split.reporter is { resourceExceededMessage: { } }) { + if (split.reporter is { resourceExceededMessage: { } }) + { msg = split.reporter.resourceExceededMessage; } callback.OnTimeout(msg); - } else if (vcOutcome == VcOutcome.OutOfMemory) { + } + else if (vcOutcome == VcOutcome.OutOfMemory) + { string msg = "out of memory"; - if (split.reporter is { resourceExceededMessage: { } }) { + if (split.reporter is { resourceExceededMessage: { } }) + { msg = split.reporter.resourceExceededMessage; } callback.OnOutOfMemory(msg); - } else if (vcOutcome == VcOutcome.OutOfResource) { + } + else if (vcOutcome == VcOutcome.OutOfResource) + { string msg = "out of resource"; - if (split.reporter is { resourceExceededMessage: { } }) { + if (split.reporter is { resourceExceededMessage: { } }) + { msg = split.reporter.resourceExceededMessage; } callback.OnOutOfResource(msg); } - - batchCompletions.OnNext((split, verificationRunResult)); } } -} +} \ No newline at end of file diff --git a/Source/VCGeneration/VerificationConditionGenerator.cs b/Source/VCGeneration/VerificationConditionGenerator.cs index a74738744..516b3d379 100644 --- a/Source/VCGeneration/VerificationConditionGenerator.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -7,7 +7,6 @@ using Microsoft.Boogie.GraphUtil; using System.Diagnostics.Contracts; using System.IO; -using System.Reactive.Subjects; using System.Runtime.CompilerServices; using System.Threading; using Microsoft.BaseTypes; @@ -15,12 +14,26 @@ namespace VC { + using Bpl = Microsoft.Boogie; using System.Threading.Tasks; + + record ImplementationTransformationData + { + + public bool Passified { get; set; } = false; + public bool ConvertedToDAG { get; set; } = false; + public Dictionary GotoCmdOrigins { get; set; } + public ModelViewInfo ModelViewInfo { get; set; } + } + + public class VerificationConditionGenerator : ConditionGeneration { - + private static ConditionalWeakTable implementationData = new(); + + /// /// Constructor. Initializes the theorem prover. /// @@ -58,12 +71,14 @@ public static AssumeCmd AssertTurnedIntoAssume(VCGenOptions options, AssertCmd a } var assume = new AssumeCmd(assrt.tok, expr); - if (expr != Expr.True) { + if (expr != Expr.True) + { // Copy any {:id ...} from the assertion to the assumption, so // we can track it while analyzing verification coverage. But // skip it if it's `true` because that's never useful to track. (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt); } + return assume; } @@ -87,9 +102,11 @@ public CodeExprConversionClosure(TextWriter traceWriter, VCGenOptions options, C this.ctx = ctx; } - public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List bindings, bool isPositiveContext, Dictionary> debugInfos) + public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List bindings, + bool isPositiveContext, Dictionary> debugInfos) { - VerificationConditionGenerator vcgen = new VerificationConditionGenerator(new Program(), new CheckerPool(options)); + VerificationConditionGenerator vcgen = + new VerificationConditionGenerator(new Program(), new CheckerPool(options)); vcgen.variable2SequenceNumber = new Dictionary(); vcgen.incarnationOriginMap = new Dictionary(); vcgen.CurrentLocalVariables = codeExpr.LocVars; @@ -167,6 +184,7 @@ public VCExpr GenerateVCAux(Implementation /*!*/ impl, VCExpr controlFlowVariabl { return VCExpressionGenerator.True; } + return vc; } @@ -179,7 +197,9 @@ public static void CheckIntAttributeOnImpl(ImplementationRun run, string name, r { return; } - run.OutputWriter.WriteLine("ignoring ill-formed {:{0} ...} attribute on {1}, parameter should be an int", name, impl.Name); + + run.OutputWriter.WriteLine("ignoring ill-formed {:{0} ...} attribute on {1}, parameter should be an int", name, + impl.Name); } // If "expand" attribute is supplied, expand any assertion of conjunctions into multiple assertions, one per conjunct @@ -243,7 +263,7 @@ void ExpandAsserts(Implementation impl) return; case BinaryOperator.Opcode.Imp: traverse(depth, args[1], e1 => act(withType(nary, - new NAryExpr(e1.tok, fun, new List() {args[0], e1})))); + new NAryExpr(e1.tok, fun, new List() { args[0], e1 })))); return; } } @@ -260,7 +280,7 @@ void ExpandAsserts(Implementation impl) { NAryExpr def = all.Body as NAryExpr; if (def != null && def.Fun is BinaryOperator && - ((BinaryOperator) (def.Fun)).Op == BinaryOperator.Opcode.Iff) + ((BinaryOperator)(def.Fun)).Op == BinaryOperator.Opcode.Iff) { body = def.Args[1]; ins = all.Dummies; @@ -322,7 +342,7 @@ void ExpandAsserts(Implementation impl) new AssertCmd(e.tok, fe(e)); new_c.Description = a.Description; new_c.Attributes = new QKeyValue(e.tok, "subsumption", - new List() {new LiteralExpr(e.tok, BigNum.FromInt(0))}, a.Attributes); + new List() { new LiteralExpr(e.tok, BigNum.FromInt(0)) }, a.Attributes); newCmds.Add(new_c); }); } @@ -345,18 +365,8 @@ void ExpandAsserts(Implementation impl) public VCGenOptions Options => CheckerPool.Options; - record ImplementationTransformationData { - - public bool Passified { get; set; } = false; - public bool ConvertedToDAG { get; set; } = false; - public Dictionary GotoCmdOrigins { get; set; } - public ModelViewInfo ModelViewInfo { get; set; } - } - - private static ConditionalWeakTable implementationData = new(); - public override async Task VerifyImplementation(ImplementationRun run, VerifierCallback callback, - CancellationToken cancellationToken, IObserver<(Split split, VerificationRunResult vcResult)> batchCompletedObserver) + CancellationToken cancellationToken) { Contract.EnsuresOnThrow(true); @@ -369,27 +379,7 @@ public override async Task VerifyImplementation(ImplementationRun run callback.OnProgress?.Invoke("VCgen", 0, 0, 0.0); - - var data = implementationData.GetOrCreateValue(run.Implementation)!; - if (!data.ConvertedToDAG) { - data.ConvertedToDAG = true; - ConvertCFG2DAG(run); - } - - SmokeTester smokeTester = null; - if (Options.SoundnessSmokeTest) - { - smokeTester = new SmokeTester(this, run, callback); - smokeTester.Copy(); - } - - if (!data.Passified) { - data.Passified = true; - data.GotoCmdOrigins = PassifyImpl(run, out var mvInfo); - data.ModelViewInfo = mvInfo; - - ExpandAsserts(impl); - } + PrepareImplementation(run, callback, out var smokeTester, out var dataGotoCmdOrigins, out var dataModelViewInfo); VcOutcome vcOutcome = VcOutcome.Correct; @@ -409,17 +399,17 @@ public override async Task VerifyImplementation(ImplementationRun run else { // If possible, we use the old counterexample, but with the location information of "a" - var cex = AssertCmdToCloneCounterexample(CheckerPool.Options, a, oldCex, impl.Blocks[0], data.GotoCmdOrigins); + var cex = AssertCmdToCloneCounterexample(CheckerPool.Options, a, oldCex, impl.Blocks[0], + dataGotoCmdOrigins); callback.OnCounterexample(cex, null); } } } } - var worker = new SplitAndVerifyWorker(Options, this, run, data.GotoCmdOrigins, callback, - data.ModelViewInfo, vcOutcome); - worker.BatchCompletions.Subscribe(batchCompletedObserver); - + var worker = new SplitAndVerifyWorker(Options, this, run, dataGotoCmdOrigins, callback, + dataModelViewInfo, vcOutcome); + vcOutcome = await worker.WorkUntilDone(cancellationToken); ResourceCount = worker.ResourceCount; @@ -434,7 +424,43 @@ public override async Task VerifyImplementation(ImplementationRun run return vcOutcome; } - public class ErrorReporter : ProverInterface.ErrorHandler { + public void PrepareImplementation(ImplementationRun run, VerifierCallback callback, + out SmokeTester smokeTester, + out Dictionary gotoCmdOrigins, + out ModelViewInfo modelViewInfo) + { + var data = implementationData.GetOrCreateValue(run.Implementation)!; + if (!data.ConvertedToDAG) + { + data.ConvertedToDAG = true; + ConvertCFG2DAG(run); + } + + smokeTester = null; + if (Options.SoundnessSmokeTest) + { + smokeTester = new SmokeTester(this, run, callback); + smokeTester.Copy(); + } + + if (!data.Passified) + { + data.Passified = true; + data.GotoCmdOrigins = gotoCmdOrigins = PassifyImpl(run, out modelViewInfo); + data.ModelViewInfo = modelViewInfo; + + ExpandAsserts(run.Implementation); + } + else + { + modelViewInfo = data.ModelViewInfo; + gotoCmdOrigins = data.GotoCmdOrigins; + } + + } + + public class ErrorReporter : ProverInterface.ErrorHandler + { private ProofRun split; private new VCGenOptions options; Dictionary gotoCmdOrigins; @@ -448,7 +474,7 @@ public class ErrorReporter : ProverInterface.ErrorHandler { protected VerifierCallback callback; protected ModelViewInfo MvInfo; - internal string resourceExceededMessage; + public string resourceExceededMessage; [ContractInvariantMethod] void ObjectInvariant() @@ -501,7 +527,7 @@ public ErrorReporter(VCGenOptions options, } public override void OnModel(IList labels /*!*/ /*!*/, Model model, - Bpl.SolverOutcome proverOutcome) + SolverOutcome proverOutcome) { // no counter examples reported. if (labels.Count == 0) @@ -612,7 +638,8 @@ public void ConvertCFG2DAG(ImplementationRun run, Dictionary> { var impl = run.Implementation; Contract.Requires(impl != null); - impl.PruneUnreachableBlocks(Options); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization + impl.PruneUnreachableBlocks( + Options); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization CurrentLocalVariables = impl.LocVars; variable2SequenceNumber = new Dictionary(); @@ -642,7 +669,7 @@ public void ConvertCFG2DAG(ImplementationRun run, Dictionary> // below assumes that the start node has no predecessor) impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List(), - new GotoCmd(Token.NoToken, new List {impl.Blocks[0].Label}, new List {impl.Blocks[0]}))); + new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] }))); ResetPredecessors(impl.Blocks); var k = Math.Max(Options.KInductionDepth, @@ -712,7 +739,7 @@ private void ConvertCFG2DAGStandard(Implementation impl, Dictionary 1) @@ -1053,7 +1080,7 @@ private void ConvertCFG2DAGKInduction(Implementation impl, Dictionary {newHeader})); + new GotoCmd(newHeader.tok, new List { newHeader })); impl.Blocks.Add(havocBlock); newHeader.Predecessors.Add(havocBlock); @@ -1130,7 +1157,7 @@ private Block DuplicateLoop(Implementation impl, Graph g, Contract.Assert(b != null); if (!ori2CopiedBlocks.ContainsKey(b)) { - Block copy = (Block) duplicator.Visit(b); + Block copy = (Block)duplicator.Visit(b); copy.Cmds = new List(copy .Cmds); // Philipp Ruemmer commented that this was necessary due to a bug in the Duplicator. That was a long time; worth checking whether this has been fixed copy.Predecessors = new List(); @@ -1248,7 +1275,7 @@ public void DesugarCalls(Implementation impl) } } - public Dictionary PassifyImpl(ImplementationRun run, out ModelViewInfo mvInfo) + public Dictionary PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) { Contract.Requires(run != null); Contract.Requires(program != null); @@ -1294,9 +1321,10 @@ public Dictionary PassifyImpl(ImplementationRun run, out var idExp = new IdentifierExpr(lvar.tok, lvar); if (lvar.TypedIdent.WhereExpr != null) { - var exp = Expr.Binary(lvar.tok, BinaryOperator.Opcode.And, lvar.TypedIdent.WhereExpr, LiteralExpr.Literal(true)); + var exp = Expr.Binary(lvar.tok, BinaryOperator.Opcode.And, lvar.TypedIdent.WhereExpr, + LiteralExpr.Literal(true)); Cmd c = new AssumeCmd(lvar.tok, exp, - new QKeyValue(lvar.tok, "where", new List(new object [] {idExp}), null)); + new QKeyValue(lvar.tok, "where", new List(new object[] { idExp }), null)); cc.Add(c); } else if (QKeyValue.FindBoolAttribute(lvar.Attributes, "assumption")) @@ -1349,8 +1377,8 @@ public Dictionary PassifyImpl(ImplementationRun run, out new LiveVariableAnalysis(Options).ComputeLiveVariables(impl); } - mvInfo = new ModelViewInfo(program, impl); - Convert2PassiveCmd(run, mvInfo); + modelViewInfo = new ModelViewInfo(program, impl); + Convert2PassiveCmd(run, modelViewInfo); if (QKeyValue.FindBoolAttribute(impl.Attributes, "may_unverified_instrumentation")) { @@ -1512,7 +1540,7 @@ static void InstrumentWithMayUnverifiedConditions(Implementation impl, Block uni private static void InstrumentWithCondition(Block block, int idx, HashSet condition) { - var conj = Expr.BinaryTreeAnd(condition.Select(v => (Expr) new IdentifierExpr(Token.NoToken, v)).ToList()); + var conj = Expr.BinaryTreeAnd(condition.Select(v => (Expr)new IdentifierExpr(Token.NoToken, v)).ToList()); block.Cmds.Insert(idx, new AssumeCmd(Token.NoToken, Expr.Not(conj))); } @@ -1810,7 +1838,7 @@ private string GetCallee(Cmd cmd, HashSet inlinedProcs) string procCalled = null; if (cmd is CallCmd) { - var cc = (CallCmd) cmd; + var cc = (CallCmd)cmd; if (inlinedProcs.Contains(cc.Proc.Name)) { procCalled = cc.Proc.Name; @@ -1890,7 +1918,8 @@ static Counterexample TraceCounterexample( if (cmd is AssertCmd && traceNodes.Contains(cmd)) { Counterexample newCounterexample = - AssertCmdToCounterexample(options, (AssertCmd) cmd, transferCmd, trace, augmentedTrace, errModel, mvInfo, context, split); + AssertCmdToCounterexample(options, (AssertCmd)cmd, transferCmd, trace, augmentedTrace, errModel, mvInfo, + context, split); Contract.Assert(newCounterexample != null); newCounterexample.AddCalleeCounterexample(calleeCounterexamples); return newCounterexample; @@ -1924,7 +1953,8 @@ static Counterexample TraceCounterexample( } } - public static Counterexample AssertCmdToCounterexample(VCGenOptions options, AssertCmd cmd, TransferCmd transferCmd, List trace, List augmentedTrace, + public static Counterexample AssertCmdToCounterexample(VCGenOptions options, AssertCmd cmd, TransferCmd transferCmd, + List trace, List augmentedTrace, Model errModel, ModelViewInfo mvInfo, ProverContext context, ProofRun split) { Contract.Requires(cmd != null); @@ -1936,7 +1966,7 @@ public static Counterexample AssertCmdToCounterexample(VCGenOptions options, Ass // See if it is a special assert inserted in translation if (cmd is AssertRequiresCmd) { - AssertRequiresCmd assertCmd = (AssertRequiresCmd) cmd; + AssertRequiresCmd assertCmd = (AssertRequiresCmd)cmd; Contract.Assert(assertCmd != null); CallCounterexample cc = new CallCounterexample(options, trace, augmentedTrace, assertCmd, errModel, mvInfo, context, split, assertCmd.Checksum); @@ -1944,15 +1974,17 @@ public static Counterexample AssertCmdToCounterexample(VCGenOptions options, Ass } else if (cmd is AssertEnsuresCmd) { - AssertEnsuresCmd assertCmd = (AssertEnsuresCmd) cmd; + AssertEnsuresCmd assertCmd = (AssertEnsuresCmd)cmd; Contract.Assert(assertCmd != null); - ReturnCounterexample rc = new ReturnCounterexample(options, trace, augmentedTrace, assertCmd, transferCmd, errModel, mvInfo, + ReturnCounterexample rc = new ReturnCounterexample(options, trace, augmentedTrace, assertCmd, transferCmd, + errModel, mvInfo, context, split, cmd.Checksum); return rc; } else { - AssertCounterexample ac = new AssertCounterexample(options, trace, augmentedTrace, (AssertCmd) cmd, errModel, mvInfo, context, split); + AssertCounterexample ac = new AssertCounterexample(options, trace, augmentedTrace, (AssertCmd)cmd, errModel, + mvInfo, context, split); return ac; } } @@ -1960,7 +1992,8 @@ public static Counterexample AssertCmdToCounterexample(VCGenOptions options, Ass /// /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt". /// - public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assrt, Counterexample cex, + public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assrt, + Counterexample cex, Block implEntryBlock, Dictionary gotoCmdOrigins) { Contract.Requires(assrt != null); @@ -1972,13 +2005,14 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options Counterexample cc; if (assrt is AssertRequiresCmd) { - var aa = (AssertRequiresCmd) assrt; - cc = new CallCounterexample(options, cex.Trace, cex.AugmentedTrace, aa, cex.Model, cex.MvInfo, cex.Context, cex.ProofRun, aa.Checksum); + var aa = (AssertRequiresCmd)assrt; + cc = new CallCounterexample(options, cex.Trace, cex.AugmentedTrace, aa, cex.Model, cex.MvInfo, cex.Context, + cex.ProofRun, aa.Checksum); } else if (assrt is AssertEnsuresCmd && cex is ReturnCounterexample) { - var aa = (AssertEnsuresCmd) assrt; - var oldCex = (ReturnCounterexample) cex; + var aa = (AssertEnsuresCmd)assrt; + var oldCex = (ReturnCounterexample)cex; // The first three parameters of ReturnCounterexample are: List trace, List augmentedTrace, TransferCmd failingReturn, Ensures failingEnsures. // We have the "aa" version of failingEnsures, namely aa.Ensures. The first and third parameters take more work to reconstruct. // (The code here assumes the labels of blocks remain the same. If that's not the case, then it is possible that the trace @@ -2001,7 +2035,7 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options } else if (prevBlock.TransferCmd is GotoCmd) { - var gto = (GotoCmd) prevBlock.TransferCmd; + var gto = (GotoCmd)prevBlock.TransferCmd; Block nb = null; Contract.Assert(gto.labelNames.Count == gto.labelTargets @@ -2055,12 +2089,14 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options } } - cc = new ReturnCounterexample(options, reconstructedTrace ?? cex.Trace, cex.AugmentedTrace, aa, returnCmd ?? oldCex.FailingReturn, + cc = new ReturnCounterexample(options, reconstructedTrace ?? cex.Trace, cex.AugmentedTrace, aa, + returnCmd ?? oldCex.FailingReturn, cex.Model, cex.MvInfo, cex.Context, cex.ProofRun, aa.Checksum); } else { - cc = new AssertCounterexample(options, cex.Trace, cex.AugmentedTrace, assrt, cex.Model, cex.MvInfo, cex.Context, cex.ProofRun); + cc = new AssertCounterexample(options, cex.Trace, cex.AugmentedTrace, assrt, cex.Model, cex.MvInfo, cex.Context, + cex.ProofRun); } return cc; @@ -2394,4 +2430,4 @@ static void RemoveEmptyBlocks(List blocks) } } } -} +} \ No newline at end of file diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs index 5704dca80..b2566f93e 100644 --- a/Source/VCGeneration/VerificationRunResult.cs +++ b/Source/VCGeneration/VerificationRunResult.cs @@ -1,26 +1,17 @@ using System; using System.Collections.Generic; -using System.Diagnostics; using System.Linq; -using System.Threading; using Microsoft.Boogie; -using System.Diagnostics.Contracts; -using System.IO; -using Microsoft.BaseTypes; -using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.SMTLib; namespace VC { - using Bpl = Microsoft.Boogie; - using System.Threading.Tasks; - public record VerificationRunResult ( int VcNum, int Iteration, DateTime StartTime, - Bpl.SolverOutcome Outcome, + SolverOutcome Outcome, TimeSpan RunTime, int MaxCounterExamples, List CounterExamples, @@ -29,12 +20,12 @@ public record VerificationRunResult int ResourceCount, SolverKind? SolverUsed ) { - public void ComputePerAssertOutcomes(out Dictionary perAssertOutcome, + public void ComputePerAssertOutcomes(out Dictionary perAssertOutcome, out Dictionary perAssertCounterExamples) { perAssertOutcome = new(); perAssertCounterExamples = new(); - if (Outcome == Bpl.SolverOutcome.Valid) { - perAssertOutcome = Asserts.ToDictionary(cmd => cmd, assertCmd => Bpl.SolverOutcome.Valid); + if (Outcome == SolverOutcome.Valid) { + perAssertOutcome = Asserts.ToDictionary(cmd => cmd, _ => SolverOutcome.Valid); } else { foreach (var counterExample in CounterExamples) { AssertCmd underlyingAssert; @@ -53,17 +44,17 @@ public void ComputePerAssertOutcomes(out Dictionary