From 4300ab730a6bbc4471e632a1abb1418996d3585b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jan 2024 15:34:40 +0100 Subject: [PATCH] Rename Outcome to SolverOutcome --- Source/Houdini/Houdini.cs | 34 +++++------ Source/Houdini/HoudiniSession.cs | 20 +++---- Source/Provers/SMTLib/ProverInterface.cs | 10 ++-- .../SMTLib/SMTLibBatchTheoremProver.cs | 22 ++++---- .../SMTLib/SMTLibInteractiveTheoremProver.cs | 56 +++++++++---------- .../SMTLib/SMTLibProcessTheoremProver.cs | 34 +++++------ .../ExecutionEngineTest.cs | 2 +- Source/VCGeneration/Checker.cs | 18 +++--- Source/VCGeneration/ConditionGeneration.cs | 14 ++--- Source/VCGeneration/SmokeTester.cs | 8 +-- Source/VCGeneration/Split.cs | 4 +- Source/VCGeneration/SplitAndVerifyWorker.cs | 29 +++++----- Source/VCGeneration/VCGen.cs | 2 +- Source/VCGeneration/VerificationRunResult.cs | 18 +++--- 14 files changed, 135 insertions(+), 136 deletions(-) diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 5883784f9..81b82c0cb 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -52,7 +52,7 @@ public virtual void UpdateAssignment(Dictionary assignment) { } - public virtual void UpdateOutcome(Outcome outcome) + public virtual void UpdateOutcome(SolverOutcome outcome) { } @@ -158,7 +158,7 @@ public override void UpdateImplementation(Implementation implementation) curImp = implementation; } - public override void UpdateOutcome(Outcome o) + public override void UpdateOutcome(SolverOutcome o) { Contract.Assert(curImp != null); DateTime endT = DateTime.UtcNow; @@ -237,7 +237,7 @@ public override void UpdateAssignment(Dictionary assignment) wr.Flush(); } - public override void UpdateOutcome(Outcome outcome) + public override void UpdateOutcome(SolverOutcome outcome) { wr.WriteLine("analysis outcome :" + outcome); wr.Flush(); @@ -335,7 +335,7 @@ protected void NotifyAssignment(Dictionary assignment) Notify((NotifyDelegate) delegate(HoudiniObserver r) { r.UpdateAssignment(assignment); }); } - protected void NotifyOutcome(Outcome outcome) + protected void NotifyOutcome(SolverOutcome outcome) { Notify((NotifyDelegate) delegate(HoudiniObserver r) { r.UpdateOutcome(outcome); }); } @@ -837,13 +837,13 @@ protected Dictionary BuildAssignment(HashSet constants return initial; } - private bool IsOutcomeNotHoudini(Outcome outcome, List errors) + private bool IsOutcomeNotHoudini(SolverOutcome outcome, List errors) { switch (outcome) { - case Outcome.Valid: + case SolverOutcome.Valid: return false; - case Outcome.Invalid: + case SolverOutcome.Invalid: Contract.Assume(errors != null); foreach (Counterexample error in errors) { @@ -863,14 +863,14 @@ private bool IsOutcomeNotHoudini(Outcome outcome, List errors) // Return true if there was at least one non-candidate error protected bool UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome, Implementation implementation, - Outcome outcome, + SolverOutcome outcome, List errors) { string implName = implementation.Name; houdiniOutcome.implementationOutcomes.Remove(implName); List nonCandidateErrors = new List(); - if (outcome == Outcome.Invalid) + if (outcome == SolverOutcome.Invalid) { foreach (Counterexample error in errors) { @@ -937,7 +937,7 @@ protected void AddRelatedToWorkList(RefutedAnnotation refutedAnnotation) // Updates the worklist and current assignment // @return true if the current function is dequeued - protected bool UpdateAssignmentWorkList(Outcome outcome, + protected bool UpdateAssignmentWorkList(SolverOutcome outcome, List errors) { Contract.Assume(currentHoudiniState.Implementation != null); @@ -945,11 +945,11 @@ protected bool UpdateAssignmentWorkList(Outcome outcome, switch (outcome) { - case Outcome.Valid: + case SolverOutcome.Valid: //yeah, dequeue break; - case Outcome.Invalid: + case SolverOutcome.Invalid: Contract.Assume(errors != null); foreach (Counterexample error in errors) @@ -1489,7 +1489,7 @@ private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) return null; } - private async Task<(Outcome, List errors)> TryCatchVerify(HoudiniSession session, int stage, IReadOnlyList completedStages) + private async Task<(SolverOutcome, List errors)> TryCatchVerify(HoudiniSession session, int stage, IReadOnlyList completedStages) { try { return await session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), GetErrorLimit()); @@ -1497,7 +1497,7 @@ private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error) catch (UnexpectedProverOutputException upo) { Contract.Assume(upo != null); - return (Outcome.Undetermined, null); + return (SolverOutcome.Undetermined, null); } } @@ -1551,7 +1551,7 @@ private async Task HoudiniVerifyCurrent(HoudiniSession session, int stage, IRead #region Explain Houdini - if (Options.ExplainHoudini && outcome == Outcome.Invalid) + if (Options.ExplainHoudini && outcome == SolverOutcome.Invalid) { Contract.Assume(errors != null); // make a copy of this variable @@ -1587,7 +1587,7 @@ private async Task HoudiniVerifyCurrent(HoudiniSession session, int stage, IRead if (UpdateAssignmentWorkList(outcome, errors)) { - if (Options.UseUnsatCoreForContractInfer && outcome == Outcome.Valid) + if (Options.UseUnsatCoreForContractInfer && outcome == SolverOutcome.Valid) { await session.UpdateUnsatCore(proverInterface, currentHoudiniState.Assignment); } @@ -1707,7 +1707,7 @@ public class VCGenOutcome public VcOutcome VcOutcome; public List errors; - public VCGenOutcome(Outcome outcome, List errors) + public VCGenOutcome(SolverOutcome outcome, List errors) { this.VcOutcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome); this.errors = errors; diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index e4d0959c5..2d14561af 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -252,7 +252,7 @@ private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary houdini.Options; - public async Task<(Outcome, List errors)> Verify( + public async Task<(SolverOutcome, List errors)> Verify( ProverInterface proverInterface, Dictionary assignment, int errorLimit) @@ -393,7 +393,7 @@ public async Task Explain(ProverInterface proverInterface, var el = Options.ErrorLimit; Options.ErrorLimit = 1; - var outcome = Outcome.Undetermined; + var outcome = SolverOutcome.Undetermined; do { @@ -402,8 +402,8 @@ public async Task Explain(ProverInterface proverInterface, handler, CancellationToken.None); hardAssumptions.RemoveAt(hardAssumptions.Count - 1); - if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory || - outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined) + if (outcome == SolverOutcome.TimeOut || outcome == SolverOutcome.OutOfMemory || + outcome == SolverOutcome.OutOfResource || outcome == SolverOutcome.Undetermined) { break; } @@ -436,8 +436,8 @@ public async Task Explain(ProverInterface proverInterface, (outcome, var unsatisfiedSoftAssumptions2) = await proverInterface.CheckAssumptions(hardAssumptions, softAssumptions2, handler, CancellationToken.None); - if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory || - outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined) + if (outcome == SolverOutcome.TimeOut || outcome == SolverOutcome.OutOfMemory || + outcome == SolverOutcome.OutOfResource || outcome == SolverOutcome.Undetermined) { break; } @@ -467,8 +467,8 @@ public async Task Explain(ProverInterface proverInterface, } } while (false); - if (outcome == Outcome.TimeOut || outcome == Outcome.OutOfMemory || - outcome == Outcome.OutOfResource || outcome == Outcome.Undetermined) + if (outcome == SolverOutcome.TimeOut || outcome == SolverOutcome.OutOfMemory || + outcome == SolverOutcome.OutOfResource || outcome == SolverOutcome.Undetermined) { Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, "TimeOut", Description); @@ -515,8 +515,8 @@ public async Task UpdateUnsatCore(ProverInterface proverInterface, Dictionary(); foreach (int i in unsatCore) { diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index cad437a24..145010769 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -112,7 +112,7 @@ public virtual int StartingProcId() return 0; } - public virtual void OnModel(IList labels, Model model, Outcome proverOutcome) + public virtual void OnModel(IList labels, Model model, SolverOutcome proverOutcome) { Contract.Requires(cce.NonNullElements(labels)); } @@ -157,7 +157,7 @@ public virtual Absy Label2Absy(string label) } } - public abstract Task Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken); + public abstract Task Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken); public virtual void LogComment(string comment) { @@ -232,13 +232,13 @@ public virtual void Check() } // (check-sat + get-unsat-core + checkOutcome) - public virtual Task<(Outcome, List)> CheckAssumptions(List assumptions, ErrorHandler handler, + public virtual Task<(SolverOutcome, List)> CheckAssumptions(List assumptions, ErrorHandler handler, CancellationToken cancellationToken) { throw new NotImplementedException(); } - public virtual Task<(Outcome, List)> CheckAssumptions(List hardAssumptions, List softAssumptions, + public virtual Task<(SolverOutcome, List)> CheckAssumptions(List hardAssumptions, List softAssumptions, ErrorHandler handler, CancellationToken cancellationToken) { throw new NotImplementedException(); @@ -295,7 +295,7 @@ public virtual void AssertNamed(VCExpr vc, bool polarity, string name) public abstract Task GoBackToIdle(); } -public enum Outcome +public enum SolverOutcome { Valid, Invalid, diff --git a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs b/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs index 9e434d272..8a82a21e9 100644 --- a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs @@ -62,7 +62,7 @@ public override int FlushAxiomsToTheoremProver() return 0; } - public override async Task Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, + public override async Task Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken) { currentErrorHandler = handler; @@ -134,7 +134,7 @@ private Task> SendRequestsAndClose(IReadOnlyList re return Process.SendRequestsAndCloseInput(sanitizedRequests, cancellationToken); } - private async Task CheckSat(CancellationToken cancellationToken) + private async Task CheckSat(CancellationToken cancellationToken) { var requests = new List(); requests.Add("(check-sat)"); @@ -148,7 +148,7 @@ private async Task CheckSat(CancellationToken cancellationToken) } if (Process == null || HadErrors) { - return Outcome.Undetermined; + return SolverOutcome.Undetermined; } try { @@ -159,7 +159,7 @@ private async Task CheckSat(CancellationToken cancellationToken) catch (TimeoutException) { currentErrorHandler.OnResourceExceeded("hard solver timeout"); resourceCount = -1; - return Outcome.TimeOut; + return SolverOutcome.TimeOut; } var responseStack = new Stack(responses.Reverse()); @@ -176,8 +176,8 @@ private async Task CheckSat(CancellationToken cancellationToken) resourceCount = ParseRCount(rlimitSExp); // Sometimes Z3 doesn't tell us that it ran out of resources - if (result != Outcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) { - result = Outcome.OutOfResource; + if (result != SolverOutcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) { + result = SolverOutcome.OutOfResource; } } @@ -186,16 +186,16 @@ private async Task CheckSat(CancellationToken cancellationToken) if (options.LibOptions.ProduceUnsatCores) { var unsatCoreSExp = responseStack.Pop(); - if (result == Outcome.Valid) { + if (result == SolverOutcome.Valid) { ReportCoveredElements(unsatCoreSExp); } } - if (result == Outcome.Invalid) { + if (result == SolverOutcome.Invalid) { var labels = CalculatePath(currentErrorHandler.StartingProcId(), errorModel); if (labels.Length == 0) { // Without a path to an error, we don't know what to report - result = Outcome.Undetermined; + result = SolverOutcome.Undetermined; } else { currentErrorHandler.OnModel(labels, errorModel, result); } @@ -294,13 +294,13 @@ public override Task> UnsatCore() throw new NotSupportedException("Batch mode solver interface does not support unsat cores."); } - public override Task<(Outcome, List)> CheckAssumptions(List assumptions, + public override Task<(SolverOutcome, List)> CheckAssumptions(List assumptions, ErrorHandler handler, CancellationToken cancellationToken) { throw new NotSupportedException("Batch mode solver interface does not support checking assumptions."); } - public override Task<(Outcome, List)> CheckAssumptions(List hardAssumptions, List softAssumptions, + public override Task<(SolverOutcome, List)> CheckAssumptions(List hardAssumptions, List softAssumptions, ErrorHandler handler, CancellationToken cancellationToken) { throw new NotSupportedException("Batch mode solver interface does not support checking assumptions."); diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs index 56736194e..71f5ab872 100644 --- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs @@ -63,7 +63,7 @@ public override int FlushAxiomsToTheoremProver() } private bool hasReset = true; - public override async Task Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken) + public override async Task Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken) { currentErrorHandler = handler; try @@ -185,12 +185,12 @@ public override void FullReset(VCExpressionGenerator generator) } [NoDefaultContract] - public async Task CheckSat(CancellationToken cancellationToken, + public async Task CheckSat(CancellationToken cancellationToken, int errorLimit) { Contract.EnsuresOnThrow(true); - var result = Outcome.Undetermined; + var result = SolverOutcome.Undetermined; if (Process == null || HadErrors) { @@ -198,7 +198,7 @@ public async Task CheckSat(CancellationToken cancellationToken, } var errorsDiscovered = 0; - var globalResult = Outcome.Undetermined; + var globalResult = SolverOutcome.Undetermined; while (true) { @@ -213,7 +213,7 @@ public async Task CheckSat(CancellationToken cancellationToken, var reporter = currentErrorHandler; // TODO(wuestholz): Is the reporter ever null? - if (usingUnsatCore && result == Outcome.Valid && reporter != null && 0 < NamedAssumes.Count) + if (usingUnsatCore && result == SolverOutcome.Valid && reporter != null && 0 < NamedAssumes.Count) { if (usingUnsatCore) { @@ -222,16 +222,16 @@ public async Task CheckSat(CancellationToken cancellationToken, } } - if (libOptions.RunDiagnosticsOnTimeout && result == Outcome.TimeOut) { + if (libOptions.RunDiagnosticsOnTimeout && result == SolverOutcome.TimeOut) { (result, popLater) = await RunTimeoutDiagnostics(currentErrorHandler, result, cancellationToken); } - if (globalResult == Outcome.Undetermined) + if (globalResult == SolverOutcome.Undetermined) { globalResult = result; } - if (result == Outcome.Invalid) + if (result == SolverOutcome.Invalid) { Model model = await GetErrorModel(cancellationToken); if (libOptions.SIBoolControlVC) @@ -244,7 +244,7 @@ public async Task CheckSat(CancellationToken cancellationToken, if (labels.Length == 0) { // Without a path to an error, we don't know what to report - globalResult = Outcome.Undetermined; + globalResult = SolverOutcome.Undetermined; break; } } @@ -309,7 +309,7 @@ private T WrapInPushPop(ref bool popLater, Func action) return result; } - private async Task<(Outcome, bool)> RunTimeoutDiagnostics(ErrorHandler handler, Outcome result, CancellationToken cancellationToken) + private async Task<(SolverOutcome, bool)> RunTimeoutDiagnostics(ErrorHandler handler, SolverOutcome result, CancellationToken cancellationToken) { var popLater = false; if (libOptions.TraceDiagnosticsOnTimeout) { @@ -332,9 +332,9 @@ private T WrapInPushPop(ref bool popLater, Func action) if (0 < timedOut.Count) { result = await WrapInPushPop(ref popLater, () => CheckSplit(timedOut, options.TimeLimit, timeLimitPerAssertion, ref queries, cancellationToken)); - if (result == Outcome.Valid) { + if (result == SolverOutcome.Valid) { timedOut.Clear(); - } else if (result == Outcome.TimeOut) { + } else if (result == SolverOutcome.TimeOut) { // Give up and report which assertions were not verified. var cmds = timedOut.Select(id => ctx.TimeoutDiagnosticIDToAssertion[id]); @@ -343,7 +343,7 @@ private T WrapInPushPop(ref bool popLater, Func action) } } } else { - result = Outcome.Valid; + result = SolverOutcome.Valid; } break; @@ -357,13 +357,13 @@ private T WrapInPushPop(ref bool popLater, Func action) var splitRes = await WrapInPushPop(ref popLater, () => CheckSplit(split, timeLimitPerAssertion, timeLimitPerAssertion, ref queries, cancellationToken)); - if (splitRes == Outcome.Valid) { + if (splitRes == SolverOutcome.Valid) { unverified.ExceptWith(split); frac = 1; - } else if (splitRes == Outcome.Invalid) { + } else if (splitRes == SolverOutcome.Invalid) { result = splitRes; break; - } else if (splitRes == Outcome.TimeOut) { + } else if (splitRes == SolverOutcome.TimeOut) { if (2 <= frac && (4 <= (rem / frac))) { frac *= 4; } else if (2 <= (rem / frac)) { @@ -407,7 +407,7 @@ private T WrapInPushPop(ref bool popLater, Func action) return (result, popLater); } - private Task CheckSplit(SortedSet split, uint timeLimit, uint timeLimitPerAssertion, + private Task CheckSplit(SortedSet split, uint timeLimit, uint timeLimitPerAssertion, ref int queries, CancellationToken cancellationToken) { var tla = (uint)(timeLimitPerAssertion * split.Count); @@ -497,9 +497,9 @@ private async Task GetErrorModel(CancellationToken cancellationToken) return resp != null ? ParseErrorModel(resp) : null; } - private async Task CheckSatAndGetResponse(CancellationToken cancellationToken) + private async Task CheckSatAndGetResponse(CancellationToken cancellationToken) { - var result = Outcome.Undetermined; + var result = SolverOutcome.Undetermined; var wasUnknown = false; var checkSatResponse = await SendVcRequest("(check-sat)").WaitAsync(cancellationToken); @@ -514,7 +514,7 @@ private async Task CheckSatAndGetResponse(CancellationToken cancellatio if (getInfoResponse != null) { result = ParseReasonUnknown(getInfoResponse, result); - if (result == Outcome.OutOfMemory) { + if (result == SolverOutcome.OutOfMemory) { processNeedsRestart = true; } } @@ -523,8 +523,8 @@ private async Task CheckSatAndGetResponse(CancellationToken cancellatio if (options.Solver == SolverKind.Z3) { resourceCount = ParseRCount(await SendVcRequest($"(get-info :{Z3.RlimitOption})")); // Sometimes Z3 doesn't tell us that it ran out of resources - if (result != Outcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) { - result = Outcome.OutOfResource; + if (result != SolverOutcome.Valid && resourceCount > options.ResourceLimit && options.ResourceLimit > 0) { + result = SolverOutcome.OutOfResource; } } @@ -681,7 +681,7 @@ public override int GetRCount() /// static int nameCounter; - public override async Task<(Outcome, List)> CheckAssumptions(List assumptions, + public override async Task<(SolverOutcome, List)> CheckAssumptions(List assumptions, ErrorHandler handler, CancellationToken cancellationToken) { currentErrorHandler = handler; @@ -706,7 +706,7 @@ public override int GetRCount() PrepareCommon(); var outcome = await CheckSat(cancellationToken, libOptions.ErrorLimit); - if (outcome != Outcome.Valid) + if (outcome != SolverOutcome.Valid) { Pop(); return (outcome, new List()); @@ -738,7 +738,7 @@ public override int GetRCount() } } - public override async Task<(Outcome, List)> CheckAssumptions(List hardAssumptions, List softAssumptions, + public override async Task<(SolverOutcome, List)> CheckAssumptions(List hardAssumptions, List softAssumptions, ErrorHandler handler, CancellationToken cancellationToken) { currentErrorHandler = handler; @@ -766,7 +766,7 @@ public override int GetRCount() PrepareCommon(); var outcome = await CheckSatAndGetResponse(cancellationToken); - if (outcome != Outcome.Invalid) + if (outcome != SolverOutcome.Invalid) { Pop(); return (outcome, new List()); @@ -785,7 +785,7 @@ public override int GetRCount() PrepareCommon(); outcome = await CheckSat(cancellationToken, libOptions.ErrorLimit); - if (outcome != Outcome.Valid) + if (outcome != SolverOutcome.Valid) { break; } @@ -805,7 +805,7 @@ public override int GetRCount() k++; } - if (outcome == Outcome.Invalid) + if (outcome == SolverOutcome.Invalid) { foreach (var relaxVar in relaxVars) { diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs index 990d4791e..f037a15ec 100644 --- a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs +++ b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs @@ -1181,9 +1181,9 @@ public override void SetAdditionalSmtOptions(IEnumerable entries) { additionalSmtOptions = entries; } - protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown) + protected SolverOutcome ParseOutcome(SExpr resp, out bool wasUnknown) { - var result = Outcome.Undetermined; + var result = SolverOutcome.Undetermined; wasUnknown = false; if (resp is null) { @@ -1194,13 +1194,13 @@ protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown) switch (resp.Name) { case "unsat": - result = Outcome.Valid; + result = SolverOutcome.Valid; break; case "sat": - result = Outcome.Invalid; + result = SolverOutcome.Invalid; break; case "unknown": - result = Outcome.Invalid; + result = SolverOutcome.Invalid; wasUnknown = true; break; case "objectives": @@ -1212,7 +1212,7 @@ protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown) || resp.Arguments[0].Name.Contains("resource limits reached"))) { currentErrorHandler.OnResourceExceeded("max resource limit"); - result = Outcome.OutOfResource; + result = SolverOutcome.OutOfResource; } else { @@ -1227,9 +1227,9 @@ protected Outcome ParseOutcome(SExpr resp, out bool wasUnknown) return result; } - protected Outcome ParseReasonUnknown(SExpr resp, Outcome initialOutcome) + protected SolverOutcome ParseReasonUnknown(SExpr resp, SolverOutcome initialOutcome) { - Outcome result; + SolverOutcome result; if (resp is null || resp.Name == "") { result = initialOutcome; } @@ -1244,15 +1244,15 @@ protected Outcome ParseReasonUnknown(SExpr resp, Outcome initialOutcome) case "(incomplete quantifiers)": case "(incomplete (theory arithmetic))": case "smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))": - result = Outcome.Invalid; + result = SolverOutcome.Invalid; break; case "memout": currentErrorHandler.OnResourceExceeded("memory"); - result = Outcome.OutOfMemory; + result = SolverOutcome.OutOfMemory; break; case "timeout": currentErrorHandler.OnResourceExceeded("timeout"); - result = Outcome.TimeOut; + result = SolverOutcome.TimeOut; break; case "canceled": // both timeout and max resource limit are reported as @@ -1260,12 +1260,12 @@ protected Outcome ParseReasonUnknown(SExpr resp, Outcome initialOutcome) if (this.options.TimeLimit > 0) { currentErrorHandler.OnResourceExceeded("timeout"); - result = Outcome.TimeOut; + result = SolverOutcome.TimeOut; } else { currentErrorHandler.OnResourceExceeded("max resource limit"); - result = Outcome.OutOfResource; + result = SolverOutcome.OutOfResource; } break; @@ -1273,20 +1273,20 @@ protected Outcome ParseReasonUnknown(SExpr resp, Outcome initialOutcome) case "resource limits reached": case "(resource limits reached)": currentErrorHandler.OnResourceExceeded("max resource limit"); - result = Outcome.OutOfResource; + result = SolverOutcome.OutOfResource; break; case "unknown": - result = Outcome.Undetermined; + result = SolverOutcome.Undetermined; break; default: - result = Outcome.Undetermined; + result = SolverOutcome.Undetermined; HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp); break; } } else { - result = Outcome.Undetermined; + result = SolverOutcome.Undetermined; HandleProverError("Unexpected prover response (getting info about 'unknown' response): " + resp); } diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs index 3ac3068df..7eda7869a 100644 --- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs @@ -353,7 +353,7 @@ public async Task StatusTest() { Assert.Contains(assertion, perAssertCounterExamples.Keys); var outcomeAssertion = perAssertOutcome[assertion]; var counterExampleAssertion = perAssertCounterExamples[assertion]; - Assert.AreEqual(Outcome.Invalid, outcomeAssertion); + Assert.AreEqual(SolverOutcome.Invalid, outcomeAssertion); Assert.AreEqual(true, counterExampleAssertion is AssertCounterexample); var assertCounterexample = (AssertCounterexample)counterExampleAssertion; Assert.AreEqual(assertCounterexample.FailingAssert, assertion); diff --git a/Source/VCGeneration/Checker.cs b/Source/VCGeneration/Checker.cs index 6ce4cc4cc..125552d7d 100644 --- a/Source/VCGeneration/Checker.cs +++ b/Source/VCGeneration/Checker.cs @@ -40,7 +40,7 @@ void ObjectInvariant() private ProverInterface thmProver; // state for the async interface - private volatile Outcome outcome; + private volatile SolverOutcome outcome; private volatile bool hasOutput; private volatile UnexpectedProverOutputException outputExn; public DateTime ProverStart { get; private set; } @@ -292,22 +292,22 @@ private async Task Check(string descriptiveName, VCExpr vc, CancellationToken ca switch (outcome) { - case Outcome.Valid: + case SolverOutcome.Valid: thmProver.LogComment("Valid"); break; - case Outcome.Invalid: + case SolverOutcome.Invalid: thmProver.LogComment("Invalid"); break; - case Outcome.TimeOut: + case SolverOutcome.TimeOut: thmProver.LogComment("Timed out"); break; - case Outcome.OutOfResource: + case SolverOutcome.OutOfResource: thmProver.LogComment("Out of resource"); break; - case Outcome.OutOfMemory: + case SolverOutcome.OutOfMemory: thmProver.LogComment("Out of memory"); break; - case Outcome.Undetermined: + case SolverOutcome.Undetermined: thmProver.LogComment("Undetermined"); break; } @@ -341,7 +341,7 @@ public async Task BeginCheck(string descriptiveName, VCExpr vc, ProverInterface. ProverTask = Check(descriptiveName, vc, cancellationToken); } - public Outcome ReadOutcome() + public SolverOutcome ReadOutcome() { Contract.Requires(IsBusy); Contract.Requires(HasOutput); @@ -389,7 +389,7 @@ public override Task GoBackToIdle() throw new NotImplementedException(); } - public override Task Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, + public override Task Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken) { throw new NotImplementedException(); } diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 418d47198..4a8b93924 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -44,21 +44,21 @@ public ConditionGenerationContracts(Program program, CheckerPool checkerPool) [ContractClass(typeof(ConditionGenerationContracts))] public abstract class ConditionGeneration : IDisposable { - public static VcOutcome ProverInterfaceOutcomeToConditionGenerationOutcome(Microsoft.Boogie.Outcome outcome) + public static VcOutcome ProverInterfaceOutcomeToConditionGenerationOutcome(Microsoft.Boogie.SolverOutcome outcome) { switch (outcome) { - case Microsoft.Boogie.Outcome.Invalid: + case Microsoft.Boogie.SolverOutcome.Invalid: return VcOutcome.Errors; - case Microsoft.Boogie.Outcome.OutOfMemory: + case Microsoft.Boogie.SolverOutcome.OutOfMemory: return VcOutcome.OutOfMemory; - case Microsoft.Boogie.Outcome.TimeOut: + case Microsoft.Boogie.SolverOutcome.TimeOut: return VcOutcome.TimedOut; - case Microsoft.Boogie.Outcome.OutOfResource: + case Microsoft.Boogie.SolverOutcome.OutOfResource: return VcOutcome.OutOfResource; - case Microsoft.Boogie.Outcome.Undetermined: + case Microsoft.Boogie.SolverOutcome.Undetermined: return VcOutcome.Inconclusive; - case Microsoft.Boogie.Outcome.Valid: + case Microsoft.Boogie.SolverOutcome.Valid: return VcOutcome.Correct; } diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs index 432236303..7d46790d9 100644 --- a/Source/VCGeneration/SmokeTester.cs +++ b/Source/VCGeneration/SmokeTester.cs @@ -278,7 +278,7 @@ async Task CheckUnreachable(TextWriter traceWriter, Block cur, List s Checker checker = await parent.CheckerPool.FindCheckerFor(parent, null, CancellationToken.None); Contract.Assert(checker != null); - Outcome outcome = Outcome.Undetermined; + SolverOutcome outcome = SolverOutcome.Undetermined; try { VCExpr vc; @@ -327,12 +327,12 @@ async Task CheckUnreachable(TextWriter traceWriter, Block cur, List s if (Options.Trace) { traceWriter.WriteLine(" [{0} s] {1}", elapsed.TotalSeconds, - outcome == Outcome.Valid + outcome == SolverOutcome.Valid ? "OOPS" - : "OK" + (outcome == Outcome.Invalid ? "" : " (" + outcome + ")")); + : "OK" + (outcome == SolverOutcome.Invalid ? "" : " (" + outcome + ")")); } - if (outcome == Outcome.Valid) + if (outcome == SolverOutcome.Valid) { // copy it again, so we get the version with calls, assignments and such copy = CopyBlock(cur); diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index e6fb880d7..2a78cd4dd 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -883,10 +883,10 @@ public Counterexample ToCounterexample(ProverContext context) return result; } - public (Bpl.Outcome outcome, VerificationRunResult result, int resourceCount) ReadOutcome(int iteration, Checker checker, VerifierCallback callback) + public (Bpl.SolverOutcome outcome, VerificationRunResult result, int resourceCount) ReadOutcome(int iteration, Checker checker, VerifierCallback callback) { Contract.EnsuresOnThrow(true); - Bpl.Outcome outcome = cce.NonNull(checker).ReadOutcome(); + Bpl.SolverOutcome outcome = cce.NonNull(checker).ReadOutcome(); if (Options.Trace && SplitIndex >= 0) { diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index d361ada9a..a74eefaac 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -9,7 +9,6 @@ using Microsoft.Boogie; using VCGeneration; using static VC.ConditionGeneration; -using Outcome = Microsoft.Boogie.Outcome; namespace VC { @@ -197,17 +196,17 @@ private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Ch } } - private static bool IsProverFailed(Outcome outcome) + private static bool IsProverFailed(SolverOutcome outcome) { switch (outcome) { - case Outcome.Valid: - case Outcome.Invalid: - case Outcome.Undetermined: + case SolverOutcome.Valid: + case SolverOutcome.Invalid: + case SolverOutcome.Undetermined: return false; - case Outcome.OutOfMemory: - case Outcome.TimeOut: - case Outcome.OutOfResource: + case SolverOutcome.OutOfMemory: + case SolverOutcome.TimeOut: + case SolverOutcome.OutOfResource: return true; default: Contract.Assert(false); @@ -215,36 +214,36 @@ private static bool IsProverFailed(Outcome outcome) } } - private static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, Outcome newOutcome) + private static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, SolverOutcome newOutcome) { switch (newOutcome) { - case Outcome.Valid: + case SolverOutcome.Valid: return currentVcOutcome; - case Outcome.Invalid: + case SolverOutcome.Invalid: return VcOutcome.Errors; - case Outcome.OutOfMemory: + case SolverOutcome.OutOfMemory: if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) { return VcOutcome.OutOfMemory; } return currentVcOutcome; - case Outcome.TimeOut: + case SolverOutcome.TimeOut: if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) { return VcOutcome.TimedOut; } return currentVcOutcome; - case Outcome.OutOfResource: + case SolverOutcome.OutOfResource: if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) { return VcOutcome.OutOfResource; } return currentVcOutcome; - case Outcome.Undetermined: + case SolverOutcome.Undetermined: if (currentVcOutcome != VcOutcome.Errors) { return VcOutcome.Inconclusive; diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index c0abd717d..bbf7dc0ce 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -501,7 +501,7 @@ public ErrorReporter(VCGenOptions options, } public override void OnModel(IList labels /*!*/ /*!*/, Model model, - Bpl.Outcome proverOutcome) + Bpl.SolverOutcome proverOutcome) { // no counter examples reported. if (labels.Count == 0) diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs index c26e859a5..5704dca80 100644 --- a/Source/VCGeneration/VerificationRunResult.cs +++ b/Source/VCGeneration/VerificationRunResult.cs @@ -20,7 +20,7 @@ public record VerificationRunResult int VcNum, int Iteration, DateTime StartTime, - Bpl.Outcome Outcome, + Bpl.SolverOutcome Outcome, TimeSpan RunTime, int MaxCounterExamples, List CounterExamples, @@ -29,12 +29,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.Outcome.Valid) { - perAssertOutcome = Asserts.ToDictionary(cmd => cmd, assertCmd => Bpl.Outcome.Valid); + if (Outcome == Bpl.SolverOutcome.Valid) { + perAssertOutcome = Asserts.ToDictionary(cmd => cmd, assertCmd => Bpl.SolverOutcome.Valid); } else { foreach (var counterExample in CounterExamples) { AssertCmd underlyingAssert; @@ -53,17 +53,17 @@ public void ComputePerAssertOutcomes(out Dictionary perA continue; } - perAssertOutcome.TryAdd(underlyingAssert, Bpl.Outcome.Invalid); + perAssertOutcome.TryAdd(underlyingAssert, Bpl.SolverOutcome.Invalid); perAssertCounterExamples.TryAdd(underlyingAssert, counterExample); } var remainingOutcome = - Outcome == Bpl.Outcome.Invalid && CounterExamples.Count < MaxCounterExamples + Outcome == Bpl.SolverOutcome.Invalid && CounterExamples.Count < MaxCounterExamples // We could not extract more counterexamples, remaining assertions are thus valid - ? Bpl.Outcome.Valid - : Outcome == Bpl.Outcome.Invalid + ? Bpl.SolverOutcome.Valid + : Outcome == Bpl.SolverOutcome.Invalid // We reached the maximum number of counterexamples, we can't infer anything for the remaining assertions - ? Bpl.Outcome.Undetermined + ? Bpl.SolverOutcome.Undetermined // TimeOut, OutOfMemory, OutOfResource, Undetermined for a single split also applies to assertions : Outcome;