From 241dfcd7cfd46b96d35db3506e75959118ad8ffd Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 14 Feb 2022 22:21:35 +0100 Subject: [PATCH] fix: Cancellation tokens to cancel and restart checkers (#497) - Enable cancellation while waiting for input from the solver - Only recycle a `Checker` if its associated prover is responsive - Return a `PipelineOutcome.Cancelled` outcome if a request was cancelled. Co-authored-by: Mikael Mayer --- Source/ExecutionEngine/ExecutionEngine.cs | 20 +- Source/Houdini/Checker.cs | 14 +- Source/Provers/SMTLib/NoopSolver.cs | 6 +- Source/Provers/SMTLib/SMTLib.csproj | 4 + Source/Provers/SMTLib/SMTLibProcess.cs | 199 ++++++++---------- .../SMTLib/SMTLibProcessTheoremProver.cs | 150 +++++++------ Source/Provers/SMTLib/SMTLibSolver.cs | 15 +- .../ExecutionEngineTests/CancellationTests.cs | 109 ++++++++++ Source/VCExpr/KeepOriginalNamer.cs | 4 + Source/VCExpr/NormalizeNamer.cs | 4 + Source/VCExpr/RandomiseNamer.cs | 4 + Source/VCExpr/ScopedNamer.cs | 11 - Source/VCExpr/UniqueNamer.cs | 2 - Source/VCGeneration/Checker.cs | 174 ++++++--------- Source/VCGeneration/CheckerPool.cs | 29 ++- Source/VCGeneration/ConditionGeneration.cs | 10 +- Source/VCGeneration/ProverInterface.cs | 25 +-- Source/VCGeneration/Split.cs | 6 +- Source/VCGeneration/SplitAndVerifyWorker.cs | 29 ++- Source/VCGeneration/VCGen.cs | 6 +- 20 files changed, 444 insertions(+), 377 deletions(-) create mode 100644 Source/UnitTests/ExecutionEngineTests/CancellationTests.cs diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 7b8361719..b417374b1 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -204,6 +204,7 @@ public enum PipelineOutcome TypeCheckingError, ResolvedAndTypeChecked, FatalError, + Cancelled, VerificationCompleted } @@ -1053,6 +1054,7 @@ public static PipelineOutcome InferAndVerify(Program program, if (e is OperationCanceledException) { + outcome = PipelineOutcome.Cancelled; return true; } @@ -1148,7 +1150,7 @@ private static void CleanupCheckers(string requestId) { if (RequestIdToCancellationTokenSource.IsEmpty) { - checkerPool.Dispose(); + checkerPool?.Dispose(); checkerPool = null; } } @@ -1207,16 +1209,14 @@ private static void VerifyImplementation(Program program, PipelineStatistics sta CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start); } - try - { - verificationResult.Outcome = vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId); - if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null) - { + try { + var cancellationToken = RequestIdToCancellationTokenSource[requestId].Token; + verificationResult.Outcome = + vcgen.VerifyImplementation(impl, out verificationResult.Errors, requestId, cancellationToken); + if (CommandLineOptions.Clo.ExtractLoops && verificationResult.Errors != null) { var vcg = vcgen as VCGen; - if (vcg != null) - { - for (int i = 0; i < verificationResult.Errors.Count; i++) - { + if (vcg != null) { + for (int i = 0; i < verificationResult.Errors.Count; i++) { verificationResult.Errors[i] = vcg.extractLoopTrace(verificationResult.Errors[i], impl.Name, program, extractLoopMappingInfo); } diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 85c73c983..933d6dee8 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -5,6 +5,7 @@ using Microsoft.BaseTypes; using VC; using System.Linq; +using System.Threading; namespace Microsoft.Boogie.Houdini { @@ -256,7 +257,7 @@ public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionar VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture); proverInterface.BeginCheck(descriptiveName, vc, handler); - ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, errorLimit); + ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, errorLimit, CancellationToken.None).Result; double queryTime = (DateTime.UtcNow - now).TotalSeconds; stats.proverTime += queryTime; @@ -388,8 +389,8 @@ public void Explain(ProverInterface proverInterface, do { hardAssumptions.Add(controlExprNoop); - outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions, out var unsatisfiedSoftAssumptions, - handler); + (outcome, var unsatisfiedSoftAssumptions) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions, + handler, CancellationToken.None).Result; hardAssumptions.RemoveAt(hardAssumptions.Count - 1); if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || @@ -423,9 +424,8 @@ public void Explain(ProverInterface proverInterface, hardAssumptions.Add(softAssumptions[i]); } - var unsatisfiedSoftAssumptions2 = new List(); - outcome = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, out unsatisfiedSoftAssumptions2, - handler); + (outcome, var unsatisfiedSoftAssumptions2) = proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, + handler, CancellationToken.None).Result; if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.OutOfResource || outcome == ProverInterface.Outcome.Undetermined) @@ -506,7 +506,7 @@ public void UpdateUnsatCore(ProverInterface proverInterface, Dictionary(); foreach (int i in unsatCore) diff --git a/Source/Provers/SMTLib/NoopSolver.cs b/Source/Provers/SMTLib/NoopSolver.cs index 51d1fde10..c588ad382 100644 --- a/Source/Provers/SMTLib/NoopSolver.cs +++ b/Source/Provers/SMTLib/NoopSolver.cs @@ -1,4 +1,6 @@ using System; +using System.Threading; +using System.Threading.Tasks; namespace Microsoft.Boogie.SMTLib; @@ -34,11 +36,11 @@ public override void Send(string cmd) } } - public override SExpr GetProverResponse() + public override Task GetProverResponse() { var result = response; response = null; - return result; + return Task.FromResult(result); } public override void NewProblem(string descriptiveName) diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj index e9d63e227..d339f5886 100644 --- a/Source/Provers/SMTLib/SMTLib.csproj +++ b/Source/Provers/SMTLib/SMTLib.csproj @@ -15,4 +15,8 @@ + + + + diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 863180513..5e9d51042 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -4,11 +4,14 @@ using System.Text; using System.Diagnostics; using System.IO; -using System.Threading; using System.Diagnostics.Contracts; +using System.Threading.Tasks; namespace Microsoft.Boogie.SMTLib { + /* + * Not thread-safe. + */ public class SMTLibProcess : SMTLibSolver { readonly Process prover; @@ -57,6 +60,7 @@ public SMTLibProcess(SMTLibOptions libOptions, SMTLibProverOptions options) prover.StartInfo = psi; prover.ErrorDataReceived += prover_ErrorDataReceived; prover.OutputDataReceived += prover_OutputDataReceived; + prover.Exited += prover_Exited; prover.Start(); toProver = prover.StandardInput; prover.BeginErrorReadLine(); @@ -68,6 +72,17 @@ public SMTLibProcess(SMTLibOptions libOptions, SMTLibProverOptions options) } } + private void prover_Exited(object sender, EventArgs e) + { + lock (this) { + while (outputReceivers.TryDequeue(out var source)) { + source.SetResult(null); + } + } + + DisposeProver(); + } + [NoDefaultContract] // important, since we have no idea what state the object might be in when this handler is invoked void ControlCHandler(object o, ConsoleCancelEventArgs a) { @@ -113,68 +128,47 @@ public override void Send(string cmd) toProver.WriteLine(cmd); } - internal Inspector Inspector - { - get { return inspector; } - } + internal Inspector Inspector => inspector; - public override SExpr GetProverResponse() + public override async Task GetProverResponse() { - toProver.Flush(); + await toProver.FlushAsync(); - while (true) - { - var exprs = ParseSExprs(true).ToArray(); - Contract.Assert(exprs.Length <= 1); - if (exprs.Length == 0) - { + while (true) { + var exprs = await ParseSExprs(true).ToListAsync(); + Contract.Assert(exprs.Count <= 1); + if (exprs.Count == 0) { return null; } var resp = exprs[0]; - if (resp.Name == "error") - { - if (resp.Arguments.Length == 1 && resp.Arguments[0].IsId) - { - if (resp.Arguments[0].Name.Contains("max. resource limit exceeded")) - { + if (resp.Name == "error") { + if (resp.Arguments.Length == 1 && resp.Arguments[0].IsId) { + if (resp.Arguments[0].Name.Contains("max. resource limit exceeded")) { return resp; - } - else { + } else { HandleError(resp.Arguments[0].Name); return null; } - } - else { + } else { HandleError(resp.ToString()); return null; } - } - else if (resp.Name == "progress") - { - if (inspector != null) - { + } else if (resp.Name == "progress") { + if (inspector != null) { var sb = new StringBuilder(); - foreach (var a in resp.Arguments) - { - if (a.Name == "labels") - { + foreach (var a in resp.Arguments) { + if (a.Name == "labels") { sb.Append("STATS LABELS"); - foreach (var x in a.Arguments) - { + foreach (var x in a.Arguments) { sb.Append(" ").Append(x.Name); } - } - else if (a.Name.StartsWith(":")) - { + } else if (a.Name.StartsWith(":")) { sb.Append("STATS NAMED_VALUES ").Append(a.Name); - foreach (var x in a.Arguments) - { + foreach (var x in a.Arguments) { sb.Append(" ").Append(x.Name); } - } - else - { + } else { continue; } @@ -182,16 +176,12 @@ public override SExpr GetProverResponse() sb.Clear(); } } - } - else if (resp.Name == "unsupported") - { + } else if (resp.Name == "unsupported") { // Skip -- this may be a benign "unsupported" from a previous command. // Of course, this is suboptimal. We should really be using // print-success to identify the errant command and determine whether // the response is benign. - } - else - { + } else { return resp; } } @@ -226,7 +216,6 @@ public override void Close() } public override event Action ErrorHandler; - int errorCnt; protected override void HandleError(string msg) { @@ -243,13 +232,13 @@ protected override void HandleError(string msg) int linePos; string currLine; - char SkipWs() + async Task SkipWs() { while (true) { if (currLine == null) { - currLine = ReadProver(); + currLine = await ReadProver(); if (currLine == null) { return '\0'; @@ -279,13 +268,13 @@ void Shift() linePos++; } - string ParseId() + async Task ParseId() { var sb = new StringBuilder(); - var beg = SkipWs(); + var begin = await SkipWs(); - var quoted = beg == '"' || beg == '|'; + var quoted = begin == '"' || begin == '|'; if (quoted) { Shift(); @@ -300,7 +289,7 @@ string ParseId() do { sb.Append("\n"); - currLine = ReadProver(); + currLine = await ReadProver(); } while (currLine == ""); if (currLine == null) { @@ -316,7 +305,7 @@ string ParseId() } var c = currLine[linePos++]; - if (quoted && c == beg) + if (quoted && c == begin) { break; } @@ -345,11 +334,11 @@ void ParseError(string msg) HandleError("Error parsing prover output: " + msg); } - IEnumerable ParseSExprs(bool top) + async IAsyncEnumerable ParseSExprs(bool top) { while (true) { - var c = SkipWs(); + var c = await SkipWs(); if (c == '\0') { break; @@ -370,7 +359,7 @@ IEnumerable ParseSExprs(bool top) if (c == '(') { Shift(); - c = SkipWs(); + c = await SkipWs(); if (c == '\0') { ParseError("expecting something after '('"); @@ -382,12 +371,12 @@ IEnumerable ParseSExprs(bool top) } else { - id = ParseId(); + id = await ParseId(); } - var args = ParseSExprs(false).ToArray(); + var args = await ParseSExprs(false).ToListAsync(); - c = SkipWs(); + c = await SkipWs(); if (c == ')') { Shift(); @@ -401,7 +390,7 @@ IEnumerable ParseSExprs(bool top) } else { - id = ParseId(); + id = await ParseId(); yield return new SExpr(id); } @@ -416,42 +405,18 @@ IEnumerable ParseSExprs(bool top) #region handling input from the prover - string ReadProver() + private readonly Queue> outputReceivers = new(); + + Task ReadProver() { - string error = null; - while (true) - { - if (error != null) - { - HandleError(error); - errorCnt++; - error = null; + lock (this) { + if (proverOutput.TryDequeue(out var result)) { + return Task.FromResult(result); } - lock (this) - { - while (proverOutput.Count == 0 && proverErrors.Count == 0 && !prover.HasExited) - { - Monitor.Wait(this, 100); - } - - if (proverErrors.Count > 0) - { - error = proverErrors.Dequeue(); - continue; - } - - if (proverOutput.Count > 0) - { - return proverOutput.Dequeue(); - } - - if (prover.HasExited) - { - DisposeProver(); - return null; - } - } + var taskCompletionSource = new TaskCompletionSource(); + outputReceivers.Enqueue(taskCompletionSource); + return taskCompletionSource.Task; } } @@ -466,35 +431,39 @@ void DisposeProver() void prover_OutputDataReceived(object sender, DataReceivedEventArgs e) { - lock (this) - { - if (e.Data != null) + if (e.Data == null) { - if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name "))) - { - Console.WriteLine("[SMT-OUT-{0}] {1}", smtProcessId, e.Data); - } + return; + } + + if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name "))) + { + Console.WriteLine("[SMT-OUT-{0}] {1}", smtProcessId, e.Data); + } - proverOutput.Enqueue(e.Data); - Monitor.Pulse(this); + lock (this) { + if (outputReceivers.TryDequeue(out var source)) { + source.SetResult(e.Data); + } else { + proverOutput.Enqueue(e.Data); + } } - } } void prover_ErrorDataReceived(object sender, DataReceivedEventArgs e) { - lock (this) - { - if (e.Data != null) + lock (this) { + if (e.Data == null) { - if (options.Verbosity >= 1) - { - Console.WriteLine("[SMT-ERR-{0}] {1}", smtProcessId, e.Data); - } + return; + } - proverErrors.Enqueue(e.Data); - Monitor.Pulse(this); + if (options.Verbosity >= 1) + { + Console.WriteLine("[SMT-ERR-{0}] {1}", smtProcessId, e.Data); } + + HandleError(e.Data); } } diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs index c0313f6ca..a8a8b9be5 100644 --- a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs @@ -8,6 +8,8 @@ using Microsoft.Boogie.TypeErasure; using System.Text; using System.Numerics; +using System.Threading; +using System.Threading.Tasks; namespace Microsoft.Boogie.SMTLib { @@ -48,12 +50,7 @@ public SMTLibProcessTheoremProver(SMTLibOptions libOptions, ProverOptions option InitializeGlobalInformation(); SetupAxiomBuilder(gen); - Namer = (RandomSeed: options.RandomSeed, libOptions.NormalizeNames) switch - { - (null, true) => new NormalizeNamer(), - (null, false) => new KeepOriginalNamer(), - _ => new RandomiseNamer(new Random(options.RandomSeed.Value)) - }; + Namer = GetNamer(libOptions, options); ctx.parent = this; DeclCollector = new TypeDeclCollector(libOptions, Namer); @@ -71,14 +68,19 @@ public SMTLibProcessTheoremProver(SMTLibOptions libOptions, ProverOptions option PrepareCommon(); } } - - private ScopedNamer ResetNamer(ScopedNamer namer) { + + private static ScopedNamer GetNamer(SMTLibOptions libOptions, ProverOptions options, ScopedNamer namer = null) + { return (RandomSeed: options.RandomSeed, libOptions.NormalizeNames) switch { - (null, true) => new NormalizeNamer(namer), - (null, false) => new KeepOriginalNamer(namer), - _ => new RandomiseNamer(namer, new Random(options.RandomSeed.Value)) - }; + (null, true) => NormalizeNamer.Create(namer), + (null, false) => KeepOriginalNamer.Create(namer), + _ => RandomiseNamer.Create(new Random(options.RandomSeed.Value), namer) + }; + } + + private ScopedNamer ResetNamer(ScopedNamer namer) { + return GetNamer(libOptions, options, namer); } public override void AssertNamed(VCExpr vc, bool polarity, string name) @@ -97,6 +99,11 @@ public override void AssertNamed(VCExpr vc, bool polarity, string name) SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name)); } + public override Task GoBackToIdle() + { + return Process.PingPong(); + } + private void SetupAxiomBuilder(VCExpressionGenerator gen) { switch (libOptions.TypeEncodingMethod) @@ -572,7 +579,7 @@ public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler if (Process != null) { - Process.PingPong(); // flush any errors + Process.PingPong().Wait(); // flush any errors Process.NewProblem(descriptiveName); } @@ -600,7 +607,7 @@ private void SendOptimizationRequests() public override void Reset(VCExpressionGenerator gen) { - if (options.Solver == SolverKind.Z3) + if (options.Solver == SolverKind.Z3 || options.Solver == SolverKind.NoOpWithZ3Options) { this.gen = gen; SendThisVC("(reset)"); @@ -623,7 +630,7 @@ public override void Reset(VCExpressionGenerator gen) private void RecoverIfProverCrashedAfterReset() { - if (Process.GetExceptionIfProverDied() is Exception e) + if (Process.GetExceptionIfProverDied().Result is Exception e) { // We recover the process but don't issue the `(reset)` command that fails. SetupProcess(); @@ -632,12 +639,12 @@ private void RecoverIfProverCrashedAfterReset() public override void FullReset(VCExpressionGenerator gen) { - if (options.Solver == SolverKind.Z3) + if (options.Solver == SolverKind.Z3 || options.Solver == SolverKind.NoOpWithZ3Options) { this.gen = gen; SendThisVC("(reset)"); SendThisVC("(set-option :" + Z3.RlimitOption + " 0)"); - Namer.Reset(); + HasReset = true; common.Clear(); SetupAxiomBuilder(gen); Axioms.Clear(); @@ -765,11 +772,11 @@ protected void HandleProverError(string s) } [NoDefaultContract] - public override Outcome CheckOutcome(ErrorHandler handler, int errorLimit) + public override async Task CheckOutcome(ErrorHandler handler, int errorLimit, CancellationToken cancellationToken) { Contract.EnsuresOnThrow(true); - var result = CheckOutcomeCore(handler, errorLimit); + var result = await CheckOutcomeCore(handler, cancellationToken, errorLimit); SendThisVC("(pop 1)"); FlushLogFile(); @@ -777,7 +784,8 @@ public override Outcome CheckOutcome(ErrorHandler handler, int errorLimit) } [NoDefaultContract] - public override Outcome CheckOutcomeCore(ErrorHandler handler, int errorLimit) + public override async Task CheckOutcomeCore(ErrorHandler handler, CancellationToken cancellationToken, + int errorLimit) { Contract.EnsuresOnThrow(true); @@ -806,7 +814,7 @@ public override Outcome CheckOutcomeCore(ErrorHandler handler, int errorLimit) { errorsDiscovered++; - result = GetResponse(); + result = await GetResponse(cancellationToken); var reporter = handler as VC.VCGen.ErrorReporter; // TODO(wuestholz): Is the reporter ever null? @@ -816,7 +824,7 @@ public override Outcome CheckOutcomeCore(ErrorHandler handler, int errorLimit) { UsedNamedAssumes = new HashSet(); SendThisVC("(get-unsat-core)"); - var resp = Process.GetProverResponse(); + var resp = await Process.GetProverResponse().WaitAsync(cancellationToken); if (resp.Name != "") { UsedNamedAssumes.Add(resp.Name); @@ -842,7 +850,7 @@ public override Outcome CheckOutcomeCore(ErrorHandler handler, int errorLimit) } if (libOptions.RunDiagnosticsOnTimeout && result == Outcome.TimeOut) { - result = RunTimeoutDiagnostics(handler, result, ref popLater); + (result, popLater) = await RunTimeoutDiagnostics(handler, result, cancellationToken); } if (globalResult == Outcome.Undetermined) @@ -852,14 +860,14 @@ public override Outcome CheckOutcomeCore(ErrorHandler handler, int errorLimit) if (result == Outcome.Invalid) { - Model model = GetErrorModel(); + Model model = await GetErrorModel(cancellationToken); if (libOptions.SIBoolControlVC) { labels = new string[0]; } else { - labels = CalculatePath(handler.StartingProcId()); + labels = await CalculatePath(handler.StartingProcId(), cancellationToken); if (labels.Length == 0) { // Without a path to an error, we don't know what to report @@ -909,8 +917,21 @@ public override Outcome CheckOutcomeCore(ErrorHandler handler, int errorLimit) } } - private Outcome RunTimeoutDiagnostics(ErrorHandler handler, Outcome result, ref bool popLater) + T WrapInPushPop(ref bool popLater, Func action) { + if (popLater) + { + SendThisVC("(pop 1)"); + } + SendThisVC("(push 1)"); + var result = action(); + popLater = true; + return result; + } + + private async Task<(Outcome, bool)> RunTimeoutDiagnostics(ErrorHandler handler, Outcome result, CancellationToken cancellationToken) + { + bool popLater = false; if (libOptions.TraceDiagnosticsOnTimeout) { Console.Out.WriteLine("Starting timeout diagnostics with initial time limit {0}.", options.TimeLimit); } @@ -929,7 +950,8 @@ private Outcome RunTimeoutDiagnostics(ErrorHandler handler, Outcome result, ref int rem = unverified.Count; if (rem == 0) { if (0 < timedOut.Count) { - result = CheckSplit(timedOut, ref popLater, options.TimeLimit, timeLimitPerAssertion, ref queries); + + result = await WrapInPushPop(ref popLater, () => CheckSplit(timedOut, options.TimeLimit, timeLimitPerAssertion, ref queries, cancellationToken)); if (result == Outcome.Valid) { timedOut.Clear(); } else if (result == Outcome.TimeOut) { @@ -952,8 +974,9 @@ private Outcome RunTimeoutDiagnostics(ErrorHandler handler, Outcome result, ref // It seems like assertions later in the control flow have smaller indexes. var split = new SortedSet(unverified.Where((val, idx) => (rem - idx - 1) < cnt)); Contract.Assert(0 < split.Count); - var splitRes = CheckSplit(split, ref popLater, timeLimitPerAssertion, timeLimitPerAssertion, - ref queries); + + var splitRes = await WrapInPushPop(ref popLater, () => CheckSplit(split, timeLimitPerAssertion, timeLimitPerAssertion, + ref queries, cancellationToken)); if (splitRes == Outcome.Valid) { unverified.ExceptWith(split); frac = 1; @@ -1001,20 +1024,14 @@ private Outcome RunTimeoutDiagnostics(ErrorHandler handler, Outcome result, ref ctx.TimeoutDiagnosticIDToAssertion.Keys.Count)); } - return result; + return (result, popLater); } - private Outcome CheckSplit(SortedSet split, ref bool popLater, uint timeLimit, uint timeLimitPerAssertion, - ref int queries) + private Task CheckSplit(SortedSet split, uint timeLimit, uint timeLimitPerAssertion, + ref int queries, CancellationToken cancellationToken) { uint tla = (uint)(timeLimitPerAssertion * split.Count); - if (popLater) - { - SendThisVC("(pop 1)"); - } - - SendThisVC("(push 1)"); // FIXME: Gross. Timeout should be set in one place! This is also Z3 specific! uint newTimeout = (0 < tla && tla < timeLimit) ? tla : timeLimit; if (newTimeout > 0) @@ -1022,8 +1039,6 @@ private Outcome CheckSplit(SortedSet split, ref bool popLater, uint timeLim SendThisVC(string.Format("(set-option :{0} {1})", Z3.TimeoutOption, newTimeout)); } - popLater = true; - SendThisVC(string.Format("; checking split VC with {0} unverified assertions", split.Count)); var expr = VCExpressionGenerator.True; foreach (var i in ctx.TimeoutDiagnosticIDToAssertion.Keys) @@ -1047,16 +1062,16 @@ private Outcome CheckSplit(SortedSet split, ref bool popLater, uint timeLim FlushLogFile(); SendCheckSat(); queries++; - return GetResponse(); + return GetResponse(cancellationToken); } - public override string[] CalculatePath(int controlFlowConstant) + public async Task CalculatePath(int controlFlowConstant, CancellationToken cancellationToken) { SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " 0)))"); var path = new List(); while (true) { - var response = Process.GetProverResponse(); + var response = await Process.GetProverResponse().WaitAsync(cancellationToken); if (response == null) { break; @@ -1507,7 +1522,7 @@ private void ConvertErrorModel(StringBuilder m) } } - private Model GetErrorModel() + private async Task GetErrorModel(CancellationToken cancellationToken) { if (!libOptions.ExpectingModel) { @@ -1519,7 +1534,7 @@ private Model GetErrorModel() Model theModel = null; while (true) { - var resp = Process.GetProverResponse(); + var resp = await Process.GetProverResponse().WaitAsync(cancellationToken); if (resp == null || Process.IsPong(resp)) { break; @@ -1585,7 +1600,7 @@ private Model GetErrorModel() return theModel; } - private Outcome GetResponse() + private async Task GetResponse(CancellationToken cancellationToken) { var result = Outcome.Undetermined; var wasUnknown = false; @@ -1594,7 +1609,7 @@ private Outcome GetResponse() while (true) { - var resp = Process.GetProverResponse(); + var resp = await Process.GetProverResponse().WaitAsync(cancellationToken); if (resp == null || Process.IsPong(resp)) { break; @@ -1641,7 +1656,7 @@ private Outcome GetResponse() Process.Ping(); while (true) { - var resp = Process.GetProverResponse(); + var resp = await Process.GetProverResponse().WaitAsync(cancellationToken); if (resp == null || Process.IsPong(resp)) { break; @@ -1947,10 +1962,10 @@ public override void SetRlimit(uint limit) options.ResourceLimit = limit; } - public override int GetRCount() + public override async Task GetRCount() { SendThisVC("(get-info :rlimit)"); - var resp = Process.GetProverResponse(); + var resp = await Process.GetProverResponse(); try { return int.Parse(resp[0].Name); @@ -2128,11 +2143,11 @@ Dictionary GetArrayFromArrayExpr(SExpr resp) return dict.Count > 0 ? dict : null; } - public override object Evaluate(VCExpr expr) + public override async Task Evaluate(VCExpr expr) { string vcString = VCExpr2String(expr, 1); SendThisVC("(get-value (" + vcString + "))"); - var resp = Process.GetProverResponse(); + var resp = await Process.GetProverResponse(); if (resp == null) { throw new VCExprEvaluationException(); @@ -2232,10 +2247,9 @@ public override object Evaluate(VCExpr expr) /// static int nameCounter = 0; - public override Outcome CheckAssumptions(List assumptions, out List unsatCore, ErrorHandler handler) + public override async Task<(Outcome, List)> CheckAssumptions(List assumptions, + ErrorHandler handler, CancellationToken cancellationToken) { - unsatCore = new List(); - Push(); // Name the assumptions var nameToAssumption = new Dictionary(); @@ -2254,18 +2268,18 @@ public override Outcome CheckAssumptions(List assumptions, out List Check(); - var outcome = CheckOutcomeCore(handler, libOptions.ErrorLimit); + var outcome = await CheckOutcomeCore(handler, cancellationToken, libOptions.ErrorLimit); if (outcome != Outcome.Valid) { Pop(); - return outcome; + return (outcome, new List()); } Contract.Assert(usingUnsatCore, "SMTLib prover not setup for computing unsat cores"); SendThisVC("(get-unsat-core)"); - var resp = Process.GetProverResponse(); - unsatCore = new List(); + var resp = await Process.GetProverResponse().WaitAsync(cancellationToken); + var unsatCore = new List(); if (resp.Name != "") { unsatCore.Add(nameToAssumption[resp.Name]); @@ -2278,7 +2292,7 @@ public override Outcome CheckAssumptions(List assumptions, out List FlushLogFile(); Pop(); - return outcome; + return (outcome, unsatCore); } public override void Push() @@ -2287,10 +2301,9 @@ public override void Push() DeclCollector.Push(); } - public override Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, - out List unsatisfiedSoftAssumptions, ErrorHandler handler) + public override async Task<(Outcome, List)> CheckAssumptions(List hardAssumptions, List softAssumptions, + ErrorHandler handler, CancellationToken cancellationToken) { - unsatisfiedSoftAssumptions = new List(); // First, convert both hard and soft assumptions to SMTLIB strings List hardAssumptionStrings = new List(); @@ -2313,15 +2326,16 @@ public override Outcome CheckAssumptions(List hardAssumptions, List()); } int k = 0; List relaxVars = new List(); + var unsatisfiedSoftAssumptions = new List(); while (true) { Push(); @@ -2331,7 +2345,7 @@ public override Outcome CheckAssumptions(List hardAssumptions, List hardAssumptions, List hardAssumptions, List ErrorHandler; public abstract void Close(); public abstract void Send(string cmd); - public abstract SExpr GetProverResponse(); + public abstract Task GetProverResponse(); public abstract void NewProblem(string descriptiveName); protected abstract void HandleError(string msg); @@ -17,12 +19,12 @@ public void Ping() Send("(get-info :name)"); } - public void PingPong() + public async Task PingPong() { Ping(); while (true) { - var sx = GetProverResponse(); + var sx = await GetProverResponse(); if (sx == null) { throw new ProverDiedException(); @@ -44,17 +46,16 @@ public bool IsPong(SExpr sx) return sx is { Name: ":name" }; } - public ProverDiedException GetExceptionIfProverDied() + public async Task GetExceptionIfProverDied() { try { - PingPong(); + await PingPong(); + return null; } catch (ProverDiedException e) { return e; } - - return null; } } \ No newline at end of file diff --git a/Source/UnitTests/ExecutionEngineTests/CancellationTests.cs b/Source/UnitTests/ExecutionEngineTests/CancellationTests.cs new file mode 100644 index 000000000..c3893cb4a --- /dev/null +++ b/Source/UnitTests/ExecutionEngineTests/CancellationTests.cs @@ -0,0 +1,109 @@ +using System.Collections.Generic; +using System.IO; +using System.Threading.Tasks; +using Microsoft.Boogie; +using NUnit.Framework; + +namespace ExecutionEngineTests +{ + [TestFixture] + public class CancellationTests + { + public Program GetProgram(string code) { + var options = CommandLineOptions.FromArguments(); + CommandLineOptions.Install(options); + var bplFileName = "1"; + int errorCount = Parser.Parse(code, bplFileName, out Program program, + CommandLineOptions.Clo.UseBaseNameForFileName); + Assert.AreEqual(0, errorCount); + + ExecutionEngine.printer = new ConsolePrinter(); + ExecutionEngine.ResolveAndTypecheck(program, bplFileName, out _); + ExecutionEngine.EliminateDeadVariables(program); + ExecutionEngine.CollectModSets(program); + ExecutionEngine.CoalesceBlocks(program); + ExecutionEngine.Inline(program); + return program; + } + + [Test] + public async Task InferAndVerifyCanBeCancelledWhileWaitingForProver() { + var infiniteProgram = GetProgram(slow); + var terminatingProgram = GetProgram(fast); + + // We limit the number of checkers to 1. + CommandLineOptions.Clo.VcsCores = 1; + + var requestId = ExecutionEngine.FreshRequestId(); + var outcomeTask = Task.Run(() => ExecutionEngine.InferAndVerify(infiniteProgram, new PipelineStatistics(), requestId, null, requestId)); + await Task.Delay(1000); + ExecutionEngine.CancelRequest(requestId); + var outcome = await outcomeTask; + Assert.AreEqual(PipelineOutcome.Cancelled, outcome); + var requestId2 = ExecutionEngine.FreshRequestId(); + var outcome2 = ExecutionEngine.InferAndVerify(terminatingProgram, new PipelineStatistics(), requestId2, null, requestId2); + Assert.AreEqual(PipelineOutcome.VerificationCompleted, outcome2); + } + + private string fast = @" +procedure easy() ensures 1 + 1 == 0; { +} +"; + + string slow = @" + type LayerType; + function {:identity} LitInt(x: int) : int; + axiom (forall x: int :: {:identity} { LitInt(x): int } LitInt(x): int == x); + const $LZ: LayerType; + function $LS(LayerType) : LayerType; + + function Ack($ly: LayerType, m#0: int, n#0: int) : int; + function Ack#canCall(m#0: int, n#0: int) : bool; + axiom (forall $ly: LayerType, m#0: int, n#0: int :: + { Ack($LS($ly), m#0, n#0) } + Ack($LS($ly), m#0, n#0) + == Ack($ly, m#0, n#0)); + axiom (forall $ly: LayerType, m#0: int, n#0: int :: + { Ack($LS($ly), m#0, n#0) } + Ack#canCall(m#0, n#0) + || (m#0 >= LitInt(0) && n#0 >= LitInt(0)) + ==> (m#0 != LitInt(0) + ==> (n#0 == LitInt(0) ==> Ack#canCall(m#0 - 1, LitInt(1))) + && (n#0 != LitInt(0) + ==> Ack#canCall(m#0, n#0 - 1) + && Ack#canCall(m#0 - 1, Ack($ly, m#0, n#0 - 1)))) + && Ack($LS($ly), m#0, n#0) + == (if m#0 == LitInt(0) + then n#0 + 1 + else (if n#0 == LitInt(0) + then Ack($ly, m#0 - 1, LitInt(1)) + else Ack($ly, m#0 - 1, Ack($ly, m#0, n#0 - 1))))); + axiom (forall $ly: LayerType, m#0: int, n#0: int :: + {:weight 3} { Ack($LS($ly), LitInt(m#0), LitInt(n#0)) } + Ack#canCall(LitInt(m#0), LitInt(n#0)) + || (LitInt(m#0) >= LitInt(0) + && LitInt(n#0) >= LitInt(0)) + ==> (LitInt(m#0) != LitInt(0) + ==> (LitInt(n#0) == LitInt(0) + ==> Ack#canCall(LitInt(m#0 - 1), LitInt(1))) + && (LitInt(n#0) != LitInt(0) + ==> Ack#canCall(LitInt(m#0), LitInt(n#0 - 1)) + && Ack#canCall(LitInt(m#0 - 1), + LitInt(Ack($LS($ly), LitInt(m#0), LitInt(n#0 - 1)))))) + && Ack($LS($ly), LitInt(m#0), LitInt(n#0)) + == (if LitInt(m#0) == LitInt(0) + then n#0 + 1 + else (if LitInt(n#0) == LitInt(0) + then Ack($LS($ly), LitInt(m#0 - 1), LitInt(1)) + else Ack($LS($ly), + LitInt(m#0 - 1), + LitInt(Ack($LS($ly), LitInt(m#0), LitInt(n#0 - 1))))))); + + procedure proof() + { + assume Ack#canCall(LitInt(5), LitInt(5)); + assert LitInt(Ack($LS($LS($LZ)), LitInt(5), LitInt(5))) == LitInt(0); + } +"; + } +} \ No newline at end of file diff --git a/Source/VCExpr/KeepOriginalNamer.cs b/Source/VCExpr/KeepOriginalNamer.cs index 8c0450008..821f38b54 100644 --- a/Source/VCExpr/KeepOriginalNamer.cs +++ b/Source/VCExpr/KeepOriginalNamer.cs @@ -13,6 +13,10 @@ public KeepOriginalNamer() public KeepOriginalNamer(ScopedNamer namer) : base(namer) { } + + public static KeepOriginalNamer Create(ScopedNamer namer = null) { + return namer != null ? new KeepOriginalNamer(namer) : new KeepOriginalNamer(); + } public override UniqueNamer Clone() { diff --git a/Source/VCExpr/NormalizeNamer.cs b/Source/VCExpr/NormalizeNamer.cs index f2dd21d83..8f0ebb0c1 100644 --- a/Source/VCExpr/NormalizeNamer.cs +++ b/Source/VCExpr/NormalizeNamer.cs @@ -14,6 +14,10 @@ public NormalizeNamer(ScopedNamer namer) : base(namer) { } + public static NormalizeNamer Create(ScopedNamer namer = null) { + return namer != null ? new NormalizeNamer(namer) : new NormalizeNamer(); + } + protected override string GetModifiedName(string uniqueInherentName) { return "$generated"; diff --git a/Source/VCExpr/RandomiseNamer.cs b/Source/VCExpr/RandomiseNamer.cs index fb7b0355c..4a85f3ff4 100644 --- a/Source/VCExpr/RandomiseNamer.cs +++ b/Source/VCExpr/RandomiseNamer.cs @@ -16,6 +16,10 @@ public RandomiseNamer(ScopedNamer namer, Random random) : base(namer) { this.random = random; } + + public static RandomiseNamer Create(Random random, ScopedNamer namer = null) { + return namer != null ? new RandomiseNamer(namer, random) : new RandomiseNamer(random); + } private RandomiseNamer(RandomiseNamer namer) : base(namer) { diff --git a/Source/VCExpr/ScopedNamer.cs b/Source/VCExpr/ScopedNamer.cs index 6324b628c..c0f206791 100644 --- a/Source/VCExpr/ScopedNamer.cs +++ b/Source/VCExpr/ScopedNamer.cs @@ -52,17 +52,6 @@ protected ScopedNamer(ScopedNamer namer) globalNewToOldName = new(namer.globalNewToOldName); } - public virtual void Reset() - { - GlobalNames.Clear(); - LocalNames.Clear(); - LocalNames.Add(new Dictionary()); - UsedNames.Clear(); - CurrentCounters.Clear(); - GlobalPlusLocalNames.Clear(); - globalNewToOldName.Clear(); - } - [ContractInvariantMethod] private void GlobalNamesInvariantMethod() { diff --git a/Source/VCExpr/UniqueNamer.cs b/Source/VCExpr/UniqueNamer.cs index eb1f332f3..23acbd78d 100644 --- a/Source/VCExpr/UniqueNamer.cs +++ b/Source/VCExpr/UniqueNamer.cs @@ -5,8 +5,6 @@ namespace Microsoft.Boogie.VCExprAST public interface UniqueNamer { string Lookup(Object thingie); - - void Reset(); string GetName(Object thing, string name); void PopScope(); diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs index 48cc8bf66..79d21273c 100644 --- a/Source/VCGeneration/Checker.cs +++ b/Source/VCGeneration/Checker.cs @@ -2,6 +2,7 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; +using System.Threading; using Microsoft.Boogie.VCExprAST; using System.Threading.Tasks; using VC; @@ -60,7 +61,13 @@ public void GoBackToIdle() Contract.Requires(IsBusy); status = CheckerStatus.Idle; - pool.AddChecker(this); + var becameIdle = thmProver.GoBackToIdle().Wait(TimeSpan.FromMilliseconds(100)); + if (becameIdle) { + pool.AddChecker(this); + } else { + pool.CheckerDied(); + Close(); + } } public Task ProverTask { get; set; } @@ -88,22 +95,9 @@ public ProverInterface TheoremProver } } - ///////////////////////////////////////////////////////////////////////////////// - // We share context information for the same program between different Checkers - - ///////////////////////////////////////////////////////////////////////////////// - - /// - /// Constructor. Initialize a checker with the program and log file. - /// Optionally, use prover context provided by parameter "ctx". - /// - public Checker(CheckerPool pool, VC.ConditionGeneration vcgen, Program prog, string /*?*/ logFilePath, bool appendLogFile, - Split split, ProverContext ctx = null) + public Checker(CheckerPool pool, string /*?*/ logFilePath, bool appendLogFile) { - Contract.Requires(vcgen != null); - Contract.Requires(prog != null); this.pool = pool; - this.Program = prog; SolverOptions = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions(); @@ -118,64 +112,29 @@ public Checker(CheckerPool pool, VC.ConditionGeneration vcgen, Program prog, str SolverOptions.Parse(CommandLineOptions.Clo.ProverOptions); - ContextCacheKey key = new ContextCacheKey(prog); - ProverInterface prover; - - if (vcgen.CheckerCommonState == null) - { - vcgen.CheckerCommonState = new Dictionary(); - } - - IDictionary /*!>!*/ - cachedContexts = (IDictionary) vcgen.CheckerCommonState; + var ctx = (ProverContext) CommandLineOptions.Clo.TheProverFactory.NewProverContext(SolverOptions); - if (ctx == null && cachedContexts.TryGetValue(key, out ctx)) - { - ctx = (ProverContext) cce.NonNull(ctx).Clone(); - prover = (ProverInterface) - CommandLineOptions.Clo.TheProverFactory.SpawnProver(CommandLineOptions.Clo, SolverOptions, ctx); - } - else - { - if (ctx == null) - { - ctx = (ProverContext) CommandLineOptions.Clo.TheProverFactory.NewProverContext(SolverOptions); - } - - Setup(prog, ctx, split); - - // we first generate the prover and then store a clone of the - // context in the cache, so that the prover can setup stuff in - // the context to be cached - prover = (ProverInterface) - CommandLineOptions.Clo.TheProverFactory.SpawnProver(CommandLineOptions.Clo, SolverOptions, ctx); - cachedContexts.Add(key, cce.NonNull((ProverContext) ctx.Clone())); - } - - this.thmProver = prover; - this.gen = prover.VCExprGen; + var prover = (ProverInterface) + CommandLineOptions.Clo.TheProverFactory.SpawnProver(CommandLineOptions.Clo, SolverOptions, ctx); + + thmProver = prover; + gen = prover.VCExprGen; } - public void Retarget(Program prog, ProverContext ctx, Split s) + public void Target(Program prog, ProverContext ctx, Split split) { lock (this) { - hasOutput = default(bool); - outcome = default(ProverInterface.Outcome); - outputExn = default(UnexpectedProverOutputException); - handler = default(ProverInterface.ErrorHandler); + hasOutput = default; + outcome = default; + outputExn = default; + handler = default; TheoremProver.FullReset(gen); ctx.Reset(); - Setup(prog, ctx, s); + Setup(prog, ctx, split); } } - public void RetargetWithoutReset(Program prog, ProverContext ctx) - { - ctx.Clear(); - Setup(prog, ctx); - } - private void SetTimeout(uint timeout) { TheoremProver.SetTimeout(Util.BoundedMultiply(timeout, 1000)); @@ -290,56 +249,56 @@ public TimeSpan ProverRunTime get { return proverRunTime; } } - public int ProverResourceCount + public Task GetProverResourceCount() { - get { return thmProver.GetRCount(); } + return thmProver.GetRCount(); } - private void WaitForOutput(object dummy) + private async Task WaitForOutput(object dummy, CancellationToken cancellationToken) { - lock (this) + try { + outcome = await thmProver.CheckOutcome(cce.NonNull(handler), CommandLineOptions.Clo.ErrorLimit, + cancellationToken); + } + catch (OperationCanceledException) { + throw; + } + catch (UnexpectedProverOutputException e) { - try - { - outcome = thmProver.CheckOutcome(cce.NonNull(handler), CommandLineOptions.Clo.ErrorLimit); - } - catch (UnexpectedProverOutputException e) - { - outputExn = e; - } - catch (Exception e) - { - outputExn = new UnexpectedProverOutputException(e.Message); - } - - switch (outcome) - { - case ProverInterface.Outcome.Valid: - thmProver.LogComment("Valid"); - break; - case ProverInterface.Outcome.Invalid: - thmProver.LogComment("Invalid"); - break; - case ProverInterface.Outcome.TimeOut: - thmProver.LogComment("Timed out"); - break; - case ProverInterface.Outcome.OutOfResource: - thmProver.LogComment("Out of resource"); - break; - case ProverInterface.Outcome.OutOfMemory: - thmProver.LogComment("Out of memory"); - break; - case ProverInterface.Outcome.Undetermined: - thmProver.LogComment("Undetermined"); - break; - } + outputExn = e; + } + catch (Exception e) + { + outputExn = new UnexpectedProverOutputException(e.Message); + } - hasOutput = true; - proverRunTime = DateTime.UtcNow - proverStart; + switch (outcome) + { + case ProverInterface.Outcome.Valid: + thmProver.LogComment("Valid"); + break; + case ProverInterface.Outcome.Invalid: + thmProver.LogComment("Invalid"); + break; + case ProverInterface.Outcome.TimeOut: + thmProver.LogComment("Timed out"); + break; + case ProverInterface.Outcome.OutOfResource: + thmProver.LogComment("Out of resource"); + break; + case ProverInterface.Outcome.OutOfMemory: + thmProver.LogComment("Out of memory"); + break; + case ProverInterface.Outcome.Undetermined: + thmProver.LogComment("Undetermined"); + break; } + + hasOutput = true; + proverRunTime = DateTime.UtcNow - proverStart; } - public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, uint timeout, uint rlimit) + public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler, uint timeout, uint rlimit, CancellationToken cancellationToken) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); @@ -362,7 +321,7 @@ public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorH thmProver.BeginCheck(descriptiveName, vc, handler); // gen.ClearSharedFormulas(); PR: don't know yet what to do with this guy - ProverTask = Task.Factory.StartNew(() => { WaitForOutput(null); }, TaskCreationOptions.LongRunning); + ProverTask = WaitForOutput(null, cancellationToken); } public ProverInterface.Outcome ReadOutcome() @@ -408,6 +367,11 @@ public override VCExpressionGenerator VCExprGen } } + public override Task GoBackToIdle() + { + throw new NotImplementedException(); + } + public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) { /*Contract.Requires(descriptiveName != null);*/ @@ -417,7 +381,7 @@ public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler } [NoDefaultContract] - public override Outcome CheckOutcome(ErrorHandler handler, int taskID = -1) + public override Task CheckOutcome(ErrorHandler handler, int taskID, CancellationToken cancellationToken) { //Contract.Requires(handler != null); Contract.EnsuresOnThrow(true); diff --git a/Source/VCGeneration/CheckerPool.cs b/Source/VCGeneration/CheckerPool.cs index 3f973a30c..032f0f723 100644 --- a/Source/VCGeneration/CheckerPool.cs +++ b/Source/VCGeneration/CheckerPool.cs @@ -35,14 +35,14 @@ public Task FindCheckerFor(ConditionGeneration vcgen, Split split = nul return Task.FromResult(result); } - int afterDec = Interlocked.Decrement(ref notCreatedCheckers); - if (afterDec >= 0) { - var checker = CreateNewChecker(vcgen, split); + if (notCreatedCheckers > 0) { + notCreatedCheckers--; + var checker = CreateNewChecker(); + PrepareChecker(vcgen.program, split, checker); Contract.Assert(checker != null); return Task.FromResult(checker); } - Interlocked.Increment(ref notCreatedCheckers); var source = new TaskCompletionSource(); checkerWaiters.Enqueue(source); return source.Task.ContinueWith(t => @@ -55,16 +55,14 @@ public Task FindCheckerFor(ConditionGeneration vcgen, Split split = nul } - private Checker CreateNewChecker(ConditionGeneration vcgen, Split split) + private Checker CreateNewChecker() { var log = options.ProverLogFilePath; if (log != null && !log.Contains("@PROC@") && availableCheckers.Count > 0) { log = log + "." + availableCheckers.Count; - } + } - Checker ch = new Checker(this, vcgen, vcgen.program, options.ProverLogFilePath, options.ProverLogFileAppend, split); - ch.GetReady(); - return ch; + return new Checker(this, log, options.ProverLogFileAppend); } public void Dispose() @@ -88,7 +86,7 @@ void PrepareChecker(Program program, Split split, Checker checker) return; } - checker.Retarget(program, checker.TheoremProver.Context, split); + checker.Target(program, checker.TheoremProver.Context, split); checker.GetReady(); } @@ -112,5 +110,16 @@ public void AddChecker(Checker checker) availableCheckers.Push(checker); } } + + public void CheckerDied() + { + lock (this) { + if (checkerWaiters.TryDequeue(out var waiter)) { + waiter.SetResult(CreateNewChecker()); + } else { + notCreatedCheckers++; + } + } + } } } \ No newline at end of file diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index a86daf2ef..489b7055d 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -22,7 +22,7 @@ public VCGenException(string s) [ContractClassFor(typeof(ConditionGeneration))] public abstract class ConditionGenerationContracts : ConditionGeneration { - public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) + public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback, CancellationToken cancellationToken) { Contract.Requires(impl != null); Contract.Requires(callback != null); @@ -39,8 +39,6 @@ public ConditionGenerationContracts(Program p, CheckerPool checkerPool) [ContractClass(typeof(ConditionGenerationContracts))] public abstract class ConditionGeneration : IDisposable { - protected internal object CheckerCommonState; - public enum Outcome { Correct, @@ -115,7 +113,7 @@ public ConditionGeneration(Program p, CheckerPool checkerPool) /// /// public Outcome VerifyImplementation(Implementation impl, out List /*?*/ errors, - string requestId = null) + string requestId, CancellationToken cancellationToken) { Contract.Requires(impl != null); @@ -127,7 +125,7 @@ public Outcome VerifyImplementation(Implementation impl, out List CheckOutcome(ErrorHandler handler, int errorLimit, CancellationToken cancellationToken); public virtual void LogComment(string comment) { @@ -236,18 +233,20 @@ public virtual void Check() } // (check-sat + get-unsat-core + checkOutcome) - public virtual Outcome CheckAssumptions(List assumptions, out List unsatCore, ErrorHandler handler) + public virtual Task<(Outcome, List)> CheckAssumptions(List assumptions, ErrorHandler handler, + CancellationToken cancellationToken) { throw new NotImplementedException(); } - public virtual Outcome CheckAssumptions(List hardAssumptions, List softAssumptions, - out List unsatisfiedSoftAssumptions, ErrorHandler handler) + public virtual Task<(Outcome, List)> CheckAssumptions(List hardAssumptions, List softAssumptions, + ErrorHandler handler, CancellationToken cancellationToken) { throw new NotImplementedException(); } - public virtual Outcome CheckOutcomeCore(ErrorHandler handler, int taskID = -1) + public virtual Task CheckOutcomeCore(ErrorHandler handler, + CancellationToken cancellationToken, int taskID = -1) { throw new NotImplementedException(); } @@ -267,7 +266,7 @@ public virtual void SetRlimit(uint limit) { } - public virtual int GetRCount() + public virtual Task GetRCount() { throw new NotImplementedException(); } @@ -285,7 +284,7 @@ public class VCExprEvaluationException : Exception { } - public virtual object Evaluate(VCExpr expr) + public virtual Task Evaluate(VCExpr expr) { throw new NotImplementedException(); } @@ -295,4 +294,6 @@ public virtual void AssertNamed(VCExpr vc, bool polarity, string name) { throw new NotImplementedException(); } + + public abstract Task GoBackToIdle(); } \ No newline at end of file diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 618ff8ab7..dd8a1cf3d 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -1299,7 +1299,7 @@ public void ReadOutcome(ref ConditionGeneration.Outcome curOutcome, out bool pro DumpDot(splitNum); } - totalResourceCount += checker.ProverResourceCount; + totalResourceCount += checker.GetProverResourceCount().Result; proverFailed = false; @@ -1350,7 +1350,7 @@ public void ReadOutcome(ref ConditionGeneration.Outcome curOutcome, out bool pro /// /// As a side effect, updates "this.parent.CumulativeAssertionCount". /// - public void BeginCheck(Checker checker, VerifierCallback callback, ModelViewInfo mvInfo, int no, uint timeout, uint rlimit) + public void BeginCheck(Checker checker, VerifierCallback callback, ModelViewInfo mvInfo, int no, uint timeout, uint rlimit, CancellationToken cancellationToken) { Contract.Requires(checker != null); Contract.Requires(callback != null); @@ -1396,7 +1396,7 @@ public void BeginCheck(Checker checker, VerifierCallback callback, ModelViewInfo desc += "_split" + no; } - checker.BeginCheck(desc, vc, reporter, timeout, rlimit); + checker.BeginCheck(desc, vc, reporter, timeout, rlimit, cancellationToken); } } diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index fb1df305c..c58e8279a 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -71,10 +71,10 @@ public SplitAndVerifyWorker(CommandLineOptions options, VCGen vcGen, Implementat splitNumber = DoSplitting ? 0 : -1; } - public async Task WorkUntilDone() + public async Task WorkUntilDone(CancellationToken cancellationToken) { TrackSplitsCost(manualSplits); - await Task.WhenAll(manualSplits.Select(DoWork)); + await Task.WhenAll(manualSplits.Select(split => DoWork(split, cancellationToken))); return outcome; } @@ -94,22 +94,22 @@ private void TrackSplitsCost(List splits) } } - async Task DoWork(Split split) + async Task DoWork(Split split, CancellationToken cancellationToken) { var checker = await split.parent.CheckerPool.FindCheckerFor(split.parent, split); try { - StartCheck(split, checker); + cancellationToken.ThrowIfCancellationRequested(); + StartCheck(split, checker, cancellationToken); await split.ProverTask; - await ProcessResult(split); + await ProcessResult(split, cancellationToken); } - catch { + finally { split.ReleaseChecker(); - throw; } } - private void StartCheck(Split split, Checker checker) + private void StartCheck(Split split, Checker checker, CancellationToken cancellationToken) { int currentSplitNumber = DoSplitting ? Interlocked.Increment(ref splitNumber) - 1 : -1; if (options.Trace && DoSplitting) { @@ -127,10 +127,10 @@ private void StartCheck(Split split, Checker checker) var timeout = KeepGoing && split.LastChance ? options.VcsFinalAssertTimeout : KeepGoing ? options.VcsKeepGoingTimeout : implementation.TimeLimit; - split.BeginCheck(checker, callback, mvInfo, currentSplitNumber, timeout, implementation.ResourceLimit); + split.BeginCheck(checker, callback, mvInfo, currentSplitNumber, timeout, implementation.ResourceLimit, cancellationToken); } - private async Task ProcessResult(Split split) + private async Task ProcessResult(Split split, CancellationToken cancellationToken) { if (TrackingProgress) { lock (this) { @@ -155,16 +155,13 @@ private async Task ProcessResult(Split split) callback.OnProgress?.Invoke("VCprove", splitNumber < 0 ? 0 : splitNumber, total, provenCost / (remainingCost + provenCost)); if (!proverFailed) { - split.ReleaseChecker(); return; } - var newTasks = HandleProverFailure(split); - split.ReleaseChecker(); // Can only be released after the synchronous part of HandleProverFailure. - await newTasks; + await HandleProverFailure(split, cancellationToken); } - private async Task HandleProverFailure(Split split) + private async Task HandleProverFailure(Split split, CancellationToken cancellationToken) { if (split.LastChance) { string msg = "some timeout"; @@ -186,7 +183,7 @@ private async Task HandleProverFailure(Split split) if (outcome != Outcome.Errors) { outcome = Outcome.Correct; } - await Task.WhenAll(newSplits.Select(DoWork)); + await Task.WhenAll(newSplits.Select(newSplit => DoWork(newSplit, cancellationToken))); return; } diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index 194f87f09..e90f516ca 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -351,7 +351,7 @@ bool CheckUnreachable(Block cur, List seq) } ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(absyIds, this.callback), - CommandLineOptions.Clo.SmokeTimeout, CommandLineOptions.Clo.ResourceLimit); + CommandLineOptions.Clo.SmokeTimeout, CommandLineOptions.Clo.ResourceLimit, CancellationToken.None); } ch.ProverTask.Wait(); @@ -805,7 +805,7 @@ void ExpandAsserts(Implementation impl) } } - public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback) + public override Outcome VerifyImplementation(Implementation impl, VerifierCallback callback, CancellationToken cancellationToken) { Contract.EnsuresOnThrow(true); @@ -867,7 +867,7 @@ public override Outcome VerifyImplementation(Implementation impl, VerifierCallba } var worker = new SplitAndVerifyWorker(CommandLineOptions.Clo, this, impl, gotoCmdOrigins, callback, mvInfo, outcome); - outcome = worker.WorkUntilDone().Result; + outcome = worker.WorkUntilDone(cancellationToken).Result; ResourceCount = worker.ResourceCount; if (outcome == Outcome.Correct && smoke_tester != null)