diff --git a/Source/Provers/SMTLib/NoopSolver.cs b/Source/Provers/SMTLib/NoopSolver.cs index 9c8cb0522..15eba5c63 100644 --- a/Source/Provers/SMTLib/NoopSolver.cs +++ b/Source/Provers/SMTLib/NoopSolver.cs @@ -39,7 +39,7 @@ public override void Send(string cmd) public override Task SendRequest(string request, CancellationToken cancellationToken = default) { Send(request); - return GetProverResponse(); + return GetProverResponse(cancellationToken); } public override async Task> SendRequestsAndCloseInput(IReadOnlyList requests, CancellationToken cancellationToken = default) { @@ -49,13 +49,13 @@ public override async Task> SendRequestsAndCloseInput(IRead } var result = new List(); foreach (var request in requests) { - result.Add(await GetProverResponse()); + result.Add(await GetProverResponse(cancellationToken)); } return result; } - protected virtual Task GetProverResponse() + protected virtual Task GetProverResponse(CancellationToken cancellationToken = default) { return Task.FromResult(responses.Count > 0 ? responses.Dequeue() : null); } diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs index 62ceca7ab..c20327d01 100644 --- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs @@ -217,7 +217,7 @@ public async Task CheckSat(CancellationToken cancellationToken, { if (usingUnsatCore) { - var resp = await SendVcRequest("(get-unsat-core)").WaitAsync(cancellationToken); + var resp = await SendVcRequest("(get-unsat-core)", cancellationToken).WaitAsync(cancellationToken); ReportCoveredElements(resp); } } @@ -285,7 +285,7 @@ public async Task CheckSat(CancellationToken cancellationToken, } // TODO seems like there's a sort of empty line being returned that we can use to check that the solver is done, but this code doesn't use it. - private Task SendVcRequest(string s) { + private Task SendVcRequest(string s, CancellationToken cancellationToken = default) { s = Sanitize(s); if (currentLogFile != null) @@ -294,7 +294,7 @@ private Task SendVcRequest(string s) { currentLogFile.Flush(); } - return Process.SendRequest(s); + return Process.SendRequest(s, cancellationToken); } private T WrapInPushPop(ref bool popLater, Func action) @@ -493,7 +493,7 @@ private async Task GetErrorModel(CancellationToken cancellationToken) return null; } - var resp = await SendVcRequest("(get-model)").WaitAsync(cancellationToken); + var resp = await SendVcRequest("(get-model)", cancellationToken).WaitAsync(cancellationToken); return resp != null ? ParseErrorModel(resp) : null; } @@ -502,7 +502,7 @@ private async Task CheckSatAndGetResponse(CancellationToken cance var result = SolverOutcome.Undetermined; var wasUnknown = false; - var checkSatResponse = await SendVcRequest("(check-sat)").WaitAsync(cancellationToken); + var checkSatResponse = await SendVcRequest("(check-sat)", cancellationToken).WaitAsync(cancellationToken); if (checkSatResponse != null) { result = ParseOutcome(checkSatResponse, out wasUnknown); @@ -510,7 +510,7 @@ private async Task CheckSatAndGetResponse(CancellationToken cance if (wasUnknown) { - var getInfoResponse = await SendVcRequest("(get-info :reason-unknown)").WaitAsync(cancellationToken); + var getInfoResponse = await SendVcRequest("(get-info :reason-unknown)", cancellationToken).WaitAsync(cancellationToken); if (getInfoResponse != null) { result = ParseReasonUnknown(getInfoResponse, result); @@ -521,7 +521,7 @@ private async Task CheckSatAndGetResponse(CancellationToken cance } if (options.Solver == SolverKind.Z3) { - resourceCount = ParseRCount(await SendVcRequest($"(get-info :{Z3.RlimitOption})")); + resourceCount = ParseRCount(await SendVcRequest($"(get-info :{Z3.RlimitOption})", cancellationToken)); // Sometimes Z3 doesn't tell us that it ran out of resources if (result != SolverOutcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) { result = SolverOutcome.OutOfResource; @@ -716,7 +716,7 @@ public override int GetRCount() } Contract.Assert(usingUnsatCore, "SMTLib prover not setup for computing unsat cores"); - var resp = await SendVcRequest("(get-unsat-core)").WaitAsync(cancellationToken); + var resp = await SendVcRequest("(get-unsat-core)", cancellationToken).WaitAsync(cancellationToken); var unsatCore = new List(); if (resp is not null && resp.Name != "") { @@ -812,7 +812,7 @@ public override int GetRCount() { foreach (var relaxVar in relaxVars) { - var resp = await SendVcRequest($"(get-value ({relaxVar}))").WaitAsync(cancellationToken); + var resp = await SendVcRequest($"(get-value ({relaxVar}))", cancellationToken).WaitAsync(cancellationToken); if (resp == null) { break; diff --git a/Source/Provers/SMTLib/UnsatSolver.cs b/Source/Provers/SMTLib/UnsatSolver.cs index b21209e6e..c0ecf9827 100644 --- a/Source/Provers/SMTLib/UnsatSolver.cs +++ b/Source/Provers/SMTLib/UnsatSolver.cs @@ -25,10 +25,18 @@ public override void Send(string request) } - protected override async Task GetProverResponse() { - if (responses.Peek().Name == "unsat") { - await semaphore.WaitAsync(); + protected override async Task GetProverResponse(CancellationToken cancellationToken = default) { + if (responses.Count > 0 && responses.Peek().Name == "unsat") { + try { + await semaphore.WaitAsync(cancellationToken); + } + catch (OperationCanceledException) { + // Discard the response this request enqueued so later requests on this + // solver don't pick up a stale "unsat" from a cancelled check-sat. + responses.Dequeue(); + throw; + } } - return await base.GetProverResponse(); + return await base.GetProverResponse(cancellationToken); } } \ No newline at end of file diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs index f992c308e..7b7a60922 100644 --- a/Source/VCGeneration/BlockTransformations.cs +++ b/Source/VCGeneration/BlockTransformations.cs @@ -16,12 +16,21 @@ public static void Optimize(IList blocks) { foreach (var block in blocks) { // make blocks ending in assume false leaves of the CFG-DAG - StopControlFlowAtAssumeFalse(block); + StopControlFlowAtAssumeFalse(block); } DeleteBlocksNotLeadingToAssertions(blocks); DeleteStraightLineBlocksWithoutCommands(blocks); BlockCoalescer.CoalesceInPlace(blocks); + // DeleteBlocksNotLeadingToAssertions rewrites gotos without touching + // Predecessors, and BlockCoalescer replaces a block's TransferCmd with its + // absorbed successor's without updating the downstream Predecessors either. + // Downstream code (notably Split.DoSplit and Split.CountAssertions) relies on + // Predecessors matching the final CFG, so rebuild them here. + foreach (var block in blocks) { + block.Predecessors.Clear(); + } + Implementation.ComputePredecessorsForBlocks(blocks); } private static void StopControlFlowAtAssumeFalse(Block block) diff --git a/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs b/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs index a217ba5be..a114257f5 100644 --- a/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs @@ -142,6 +142,19 @@ async Task DoWork(int iteration, Split split, CancellationToken cancellationToke totalProverElapsedTime += checker.ProverRunTime; } } + catch (TimeoutException) + { + // The belt-and-suspenders WaitAsync timeout in StartCheck fired, usually + // because the prover subprocess is stuck (e.g. left in a bad state by a + // previous malformed SMT query). Reset the checker and record the split + // as timed out instead of propagating the exception out of verification. + await checker.GoBackToIdle(); + lock (this) + { + vcOutcome = MergeOutcomes(vcOutcome, SolverOutcome.TimeOut); + } + callback.OnTimeout("prover did not respond within timeout"); + } catch { await checker.GoBackToIdle();