From 4300ab730a6bbc4471e632a1abb1418996d3585b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jan 2024 15:34:40 +0100 Subject: [PATCH 1/2] 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; From 97098d6c4bb8958c0f89edb059010c0e3e195bf1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jan 2024 15:36:38 +0100 Subject: [PATCH 2/2] Rename VCGen --- Source/ExecutionEngine/ExecutionEngine.cs | 4 ++-- Source/Houdini/Houdini.cs | 4 ++-- Source/Houdini/HoudiniSession.cs | 4 ++-- Source/VCGeneration/CommandTransformations.cs | 2 +- Source/VCGeneration/Counterexample.cs | 2 +- Source/VCGeneration/FocusAttribute.cs | 2 +- Source/VCGeneration/ManualSplitFinder.cs | 2 +- Source/VCGeneration/SmokeTester.cs | 6 +++--- Source/VCGeneration/Split.cs | 14 +++++++------- Source/VCGeneration/SplitAndVerifyWorker.cs | 14 +++++++------- Source/VCGeneration/StratifiedVC.cs | 12 ++++++------ ...{VCGen.cs => VerificationConditionGenerator.cs} | 6 +++--- 12 files changed, 36 insertions(+), 36 deletions(-) rename Source/VCGeneration/{VCGen.cs => VerificationConditionGenerator.cs} (99%) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 467cca178..127763000 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -19,7 +19,7 @@ namespace Microsoft.Boogie { - public record ProcessedProgram(Program Program, Action PostProcessResult) { + public record ProcessedProgram(Program Program, Action PostProcessResult) { public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) { } } @@ -880,7 +880,7 @@ private IObservable VerifyImplementationWithoutCaching(Proc var batchCompleted = new Subject<(Split split, VerificationRunResult vcResult)>(); var completeVerification = largeThreadTaskFactory.StartNew(async () => { - var vcgen = new VCGen(processedProgram.Program, checkerPool); + var vcgen = new VerificationConditionGenerator(processedProgram.Program, checkerPool); vcgen.CachingActionCounts = stats.CachingActionCounts; verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount; verificationResult.Start = DateTime.UtcNow; diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 81b82c0cb..11a51b434 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -393,7 +393,7 @@ public class Houdini : ObservableHoudini { protected Program program; protected HashSet houdiniConstants; - protected VCGen vcgen; + protected VerificationConditionGenerator vcgen; protected ProverInterface proverInterface; protected Graph callGraph; protected HashSet vcgenFailures; @@ -470,7 +470,7 @@ protected void Initialize(TextWriter traceWriter, Program program, HoudiniSessio */ var checkerPool = new CheckerPool(Options); - this.vcgen = new VCGen(program, checkerPool); + this.vcgen = new VerificationConditionGenerator(program, checkerPool); this.proverInterface = ProverInterface.CreateProver(Options, program, Options.ProverLogFilePath, Options.ProverLogFileAppend, Options.TimeLimit, taskID: GetTaskID()); diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 2d14561af..5c1032115 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -156,7 +156,7 @@ public bool InUnsatCore(Variable constant) return false; } - public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, + public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, ProverInterface proverInterface, Program program, ImplementationRun run, HoudiniStatistics stats, int taskID = -1) { var impl = run.Implementation; @@ -195,7 +195,7 @@ public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterf new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false)); proverInterface.DefineMacro(macro, conjecture); conjecture = exprGen.Function(macro); - handler = new VCGen.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, impl.debugInfos, collector, + handler = new VerificationConditionGenerator.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, impl.debugInfos, collector, mvInfo, proverInterface.Context, program, this); } diff --git a/Source/VCGeneration/CommandTransformations.cs b/Source/VCGeneration/CommandTransformations.cs index a39bac235..74daf7195 100644 --- a/Source/VCGeneration/CommandTransformations.cs +++ b/Source/VCGeneration/CommandTransformations.cs @@ -9,7 +9,7 @@ public static Cmd AssertIntoAssume(VCGenOptions options, Cmd c) { if (c is AssertCmd assrt) { - return VCGen.AssertTurnedIntoAssume(options, assrt); + return VerificationConditionGenerator.AssertTurnedIntoAssume(options, assrt); } return c; diff --git a/Source/VCGeneration/Counterexample.cs b/Source/VCGeneration/Counterexample.cs index 457568fdd..11e5ff3d9 100644 --- a/Source/VCGeneration/Counterexample.cs +++ b/Source/VCGeneration/Counterexample.cs @@ -196,7 +196,7 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) { var cmd = GetTraceCmd(loc); var calleeName = GetCalledProcName(cmd); - if (calleeName.StartsWith(VC.StratifiedVCGenBase.recordProcName) && + if (calleeName.StartsWith(VC.StratifiedVerificationConditionGeneratorBase.recordProcName) && options.StratifiedInlining > 0) { Contract.Assert(calleeCounterexamples[loc].args.Count == 1); diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs index e08874579..72c3c76c8 100644 --- a/Source/VCGeneration/FocusAttribute.cs +++ b/Source/VCGeneration/FocusAttribute.cs @@ -15,7 +15,7 @@ namespace VCGeneration; public static class FocusAttribute { - public static List FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VCGen par) + public static List FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par) { bool IsFocusCmd(Cmd c) { return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs index 76c3922d6..5646d71fa 100644 --- a/Source/VCGeneration/ManualSplitFinder.cs +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -9,7 +9,7 @@ namespace VCGeneration; public static class ManualSplitFinder { - public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VCGen par, bool splitOnEveryAssert) + public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par, bool splitOnEveryAssert) { List focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par); var splits = focussedImpl.Select(s => FindManualSplits(s, splitOnEveryAssert)).SelectMany(x => x).ToList(); diff --git a/Source/VCGeneration/SmokeTester.cs b/Source/VCGeneration/SmokeTester.cs index 7d46790d9..a56cd5ff6 100644 --- a/Source/VCGeneration/SmokeTester.cs +++ b/Source/VCGeneration/SmokeTester.cs @@ -24,7 +24,7 @@ void ObjectInvariant() Contract.Invariant(callback != null); } - VCGen parent; + VerificationConditionGenerator parent; ImplementationRun run; Block initial; int id; @@ -32,7 +32,7 @@ void ObjectInvariant() HashSet visited = new HashSet(); VerifierCallback callback; - internal SmokeTester(VCGen par, ImplementationRun run, VerifierCallback callback) + internal SmokeTester(VerificationConditionGenerator par, ImplementationRun run, VerifierCallback callback) { Contract.Requires(par != null); Contract.Requires(run != null); @@ -130,7 +130,7 @@ Block CopyBlock(Block b) } else { - seq.Add(VCGen.AssertTurnedIntoAssume(Options, turn)); + seq.Add(VerificationConditionGenerator.AssertTurnedIntoAssume(Options, turn)); } } diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 2a78cd4dd..fdcf1e80f 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -64,7 +64,7 @@ void ObjectInvariant() public Dictionary GotoCmdOrigins { get; } - public readonly VCGen /*!*/ parent; + public readonly VerificationConditionGenerator /*!*/ parent; public Implementation /*!*/ Implementation => Run.Implementation; @@ -84,11 +84,11 @@ void ObjectInvariant() // async interface public int SplitIndex { get; set; } - internal VCGen.ErrorReporter reporter; + internal VerificationConditionGenerator.ErrorReporter reporter; public Split(VCGenOptions options, List /*!*/ blocks, Dictionary /*!*/ gotoCmdOrigins, - VCGen /*!*/ par, ImplementationRun run) + VerificationConditionGenerator /*!*/ par, ImplementationRun run) { Contract.Requires(cce.NonNullElements(blocks)); Contract.Requires(gotoCmdOrigins != null); @@ -616,7 +616,7 @@ List SliceCmds(Block b) if (swap) { - theNewCmd = VCGen.AssertTurnedIntoAssume(Options, a); + theNewCmd = VerificationConditionGenerator.AssertTurnedIntoAssume(Options, a); } } @@ -756,7 +756,7 @@ public Counterexample ToCounterexample(ProverContext context) Contract.Assert(c != null); if (c is AssertCmd) { - var counterexample = VCGen.AssertCmdToCounterexample(Options, (AssertCmd) c, cce.NonNull(b.TransferCmd), trace, null, null, null, context, this); + var counterexample = VerificationConditionGenerator.AssertCmdToCounterexample(Options, (AssertCmd) c, cce.NonNull(b.TransferCmd), trace, null, null, null, context, this); Counterexamples.Add(counterexample); return counterexample; } @@ -943,7 +943,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa ProverContext ctx = checker.TheoremProver.Context; Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator; - var cc = new VCGen.CodeExprConversionClosure(traceWriter, checker.Pool.Options, absyIds, ctx); + var cc = new VerificationConditionGenerator.CodeExprConversionClosure(traceWriter, checker.Pool.Options, absyIds, ctx); bet.SetCodeExprConverter(cc.CodeExprToVerificationCondition); var exprGen = ctx.ExprGen; @@ -957,7 +957,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(absyIds.GetId(Implementation.Blocks[0])))); vc = exprGen.Implies(eqExpr, vc); - reporter = new VCGen.ErrorReporter(Options, GotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback, + reporter = new VerificationConditionGenerator.ErrorReporter(Options, GotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback, mvInfo, checker.TheoremProver.Context, parent.program, this); } diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index a74eefaac..7409ca17e 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -31,7 +31,7 @@ class SplitAndVerifyWorker private bool TrackingProgress => DoSplitting && (callback.OnProgress != null || options.Trace); private bool KeepGoing => maxKeepGoingSplits > 1; - private VCGen vcGen; + private VerificationConditionGenerator verificationConditionGenerator; private VcOutcome vcOutcome; private double remainingCost; private double provenCost; @@ -40,7 +40,7 @@ class SplitAndVerifyWorker private int totalResourceCount; - public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun run, + public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, ImplementationRun run, Dictionary gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo, VcOutcome vcOutcome) { @@ -49,16 +49,16 @@ public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun this.mvInfo = mvInfo; this.run = run; this.vcOutcome = vcOutcome; - this.vcGen = vcGen; + this.verificationConditionGenerator = verificationConditionGenerator; var maxSplits = options.VcsMaxSplits; - VCGen.CheckIntAttributeOnImpl(run, "vcs_max_splits", ref maxSplits); + VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_splits", ref maxSplits); maxKeepGoingSplits = options.VcsMaxKeepGoingSplits; - VCGen.CheckIntAttributeOnImpl(run, "vcs_max_keep_going_splits", ref maxKeepGoingSplits); + VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_keep_going_splits", ref maxKeepGoingSplits); maxVcCost = options.VcsMaxCost; var tmpMaxVcCost = -1; - VCGen.CheckIntAttributeOnImpl(run, "vcs_max_cost", ref tmpMaxVcCost); + VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_cost", ref tmpMaxVcCost); if (tmpMaxVcCost >= 0) { maxVcCost = tmpMaxVcCost; @@ -68,7 +68,7 @@ public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); ResetPredecessors(Implementation.Blocks); - manualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, vcGen, splitOnEveryAssert); + manualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator, splitOnEveryAssert); if (manualSplits.Count == 1 && maxSplits > 1) { manualSplits = Split.DoSplit(manualSplits[0], maxVcCost, maxSplits); diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index beb082cb5..5a296ffc4 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -348,7 +348,7 @@ public override string ToString() public class StratifiedInliningInfo { private VCGenOptions options; - public StratifiedVCGenBase vcgen; + public StratifiedVerificationConditionGeneratorBase vcgen; public ImplementationRun run; public Function function; public Variable controlFlowVariable; @@ -370,10 +370,10 @@ public class StratifiedInliningInfo public Implementation Implementation => run.Implementation; - public StratifiedInliningInfo(VCGenOptions options, ImplementationRun run, StratifiedVCGenBase stratifiedVcGen, + public StratifiedInliningInfo(VCGenOptions options, ImplementationRun run, StratifiedVerificationConditionGeneratorBase stratifiedVerificationConditionGenerator, Action PassiveImplInstrumentation) { - vcgen = stratifiedVcGen; + vcgen = stratifiedVerificationConditionGenerator; this.PassiveImplInstrumentation = PassiveImplInstrumentation; this.run = run; this.options = options; @@ -655,7 +655,7 @@ public void GenerateVC() var absyIds = new ControlFlowIdMap(); - VCGen.CodeExprConversionClosure cc = new VCGen.CodeExprConversionClosure(run.OutputWriter, options, absyIds, proverInterface.Context); + VerificationConditionGenerator.CodeExprConversionClosure cc = new VerificationConditionGenerator.CodeExprConversionClosure(run.OutputWriter, options, absyIds, proverInterface.Context); translator.SetCodeExprConverter(cc.CodeExprToVerificationCondition); vcexpr = gen.Not(vcgen.GenerateVCAux(Implementation, controlFlowVariableExpr, absyIds, proverInterface.Context)); @@ -702,14 +702,14 @@ public void GenerateVC() } // This class is derived and used by Corral to create VCs for Stratified Inlining. - public abstract class StratifiedVCGenBase : VCGen + public abstract class StratifiedVerificationConditionGeneratorBase : VerificationConditionGenerator { public readonly static string recordProcName = "boogie_si_record"; public readonly static string callSiteVarAttr = "callSiteVar"; public Dictionary implName2StratifiedInliningInfo; public ProverInterface prover; - public StratifiedVCGenBase(TextWriter traceWriter, VCGenOptions options, Program program, string logFilePath /*?*/, bool appendLogFile, CheckerPool checkerPool, + public StratifiedVerificationConditionGeneratorBase(TextWriter traceWriter, VCGenOptions options, Program program, string logFilePath /*?*/, bool appendLogFile, CheckerPool checkerPool, Action PassiveImplInstrumentation) : base(program, checkerPool) { diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VerificationConditionGenerator.cs similarity index 99% rename from Source/VCGeneration/VCGen.cs rename to Source/VCGeneration/VerificationConditionGenerator.cs index bbf7dc0ce..a74738744 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VerificationConditionGenerator.cs @@ -18,14 +18,14 @@ namespace VC using Bpl = Microsoft.Boogie; using System.Threading.Tasks; - public class VCGen : ConditionGeneration + public class VerificationConditionGenerator : ConditionGeneration { /// /// Constructor. Initializes the theorem prover. /// [NotDelayed] - public VCGen(Program program, CheckerPool checkerPool) + public VerificationConditionGenerator(Program program, CheckerPool checkerPool) : base(program, checkerPool) { Contract.Requires(program != null); @@ -89,7 +89,7 @@ public CodeExprConversionClosure(TextWriter traceWriter, VCGenOptions options, C public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List bindings, bool isPositiveContext, Dictionary> debugInfos) { - VCGen vcgen = new VCGen(new Program(), new CheckerPool(options)); + VerificationConditionGenerator vcgen = new VerificationConditionGenerator(new Program(), new CheckerPool(options)); vcgen.variable2SequenceNumber = new Dictionary(); vcgen.incarnationOriginMap = new Dictionary(); vcgen.CurrentLocalVariables = codeExpr.LocVars;