Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Renames #842

Merged
merged 2 commits into from
Jan 26, 2024
Merged

Renames #842

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4300ab7
Rename Outcome to SolverOutcome
keyboardDrummer Jan 26, 2024
97098d6
Rename VCGen
keyboardDrummer Jan 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Source/ExecutionEngine/ExecutionEngine.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@

namespace Microsoft.Boogie
{
public record ProcessedProgram(Program Program, Action<VCGen, Implementation, ImplementationRunResult> PostProcessResult) {
public record ProcessedProgram(Program Program, Action<VerificationConditionGenerator, Implementation, ImplementationRunResult> PostProcessResult) {
public ProcessedProgram(Program program) : this(program, (_, _, _) => { }) {
}
}
Expand Down Expand Up @@ -880,7 +880,7 @@ private IObservable<IVerificationStatus> 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;
Expand Down
38 changes: 19 additions & 19 deletions Source/Houdini/Houdini.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ public virtual void UpdateAssignment(Dictionary<Variable, bool> assignment)
{
}

public virtual void UpdateOutcome(Outcome outcome)
public virtual void UpdateOutcome(SolverOutcome outcome)
{
}

Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -237,7 +237,7 @@ public override void UpdateAssignment(Dictionary<Variable, bool> assignment)
wr.Flush();
}

public override void UpdateOutcome(Outcome outcome)
public override void UpdateOutcome(SolverOutcome outcome)
{
wr.WriteLine("analysis outcome :" + outcome);
wr.Flush();
Expand Down Expand Up @@ -335,7 +335,7 @@ protected void NotifyAssignment(Dictionary<Variable, bool> 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); });
}
Expand Down Expand Up @@ -393,7 +393,7 @@ public class Houdini : ObservableHoudini
{
protected Program program;
protected HashSet<Variable> houdiniConstants;
protected VCGen vcgen;
protected VerificationConditionGenerator vcgen;
protected ProverInterface proverInterface;
protected Graph<Implementation> callGraph;
protected HashSet<Implementation> vcgenFailures;
Expand Down Expand Up @@ -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());

Expand Down Expand Up @@ -837,13 +837,13 @@ protected Dictionary<Variable, bool> BuildAssignment(HashSet<Variable> constants
return initial;
}

private bool IsOutcomeNotHoudini(Outcome outcome, List<Counterexample> errors)
private bool IsOutcomeNotHoudini(SolverOutcome outcome, List<Counterexample> 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)
{
Expand All @@ -863,14 +863,14 @@ private bool IsOutcomeNotHoudini(Outcome outcome, List<Counterexample> errors)
// Return true if there was at least one non-candidate error
protected bool UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,
Implementation implementation,
Outcome outcome,
SolverOutcome outcome,
List<Counterexample> errors)
{
string implName = implementation.Name;
houdiniOutcome.implementationOutcomes.Remove(implName);
List<Counterexample> nonCandidateErrors = new List<Counterexample>();

if (outcome == Outcome.Invalid)
if (outcome == SolverOutcome.Invalid)
{
foreach (Counterexample error in errors)
{
Expand Down Expand Up @@ -937,19 +937,19 @@ 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<Counterexample> errors)
{
Contract.Assume(currentHoudiniState.Implementation != null);
bool dequeue = true;

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)
Expand Down Expand Up @@ -1489,15 +1489,15 @@ private RefutedAnnotation ExtractRefutedAnnotation(Counterexample error)
return null;
}

private async Task<(Outcome, List<Counterexample> errors)> TryCatchVerify(HoudiniSession session, int stage, IReadOnlyList<int> completedStages)
private async Task<(SolverOutcome, List<Counterexample> errors)> TryCatchVerify(HoudiniSession session, int stage, IReadOnlyList<int> completedStages)
{
try {
return await session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), GetErrorLimit());
}
catch (UnexpectedProverOutputException upo)
{
Contract.Assume(upo != null);
return (Outcome.Undetermined, null);
return (SolverOutcome.Undetermined, null);
}

}
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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);
}
Expand Down Expand Up @@ -1707,7 +1707,7 @@ public class VCGenOutcome
public VcOutcome VcOutcome;
public List<Counterexample> errors;

public VCGenOutcome(Outcome outcome, List<Counterexample> errors)
public VCGenOutcome(SolverOutcome outcome, List<Counterexample> errors)
{
this.VcOutcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
this.errors = errors;
Expand Down
24 changes: 12 additions & 12 deletions Source/Houdini/HoudiniSession.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
}

Expand Down Expand Up @@ -252,7 +252,7 @@ private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary<Variable,

public HoudiniOptions Options => houdini.Options;

public async Task<(Outcome, List<Counterexample> errors)> Verify(
public async Task<(SolverOutcome, List<Counterexample> errors)> Verify(
ProverInterface proverInterface,
Dictionary<Variable, bool> assignment,
int errorLimit)
Expand Down Expand Up @@ -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
{
Expand All @@ -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;
}
Expand Down Expand Up @@ -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;
}
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -515,8 +515,8 @@ public async Task UpdateUnsatCore(ProverInterface proverInterface, Dictionary<Va
assumptionExprs.Add(exprTranslator.LookupVariable(v));
}

(Outcome tmp, var unsatCore) = await proverInterface.CheckAssumptions(assumptionExprs, handler, CancellationToken.None);
System.Diagnostics.Debug.Assert(tmp == Outcome.Valid);
(SolverOutcome tmp, var unsatCore) = await proverInterface.CheckAssumptions(assumptionExprs, handler, CancellationToken.None);
System.Diagnostics.Debug.Assert(tmp == SolverOutcome.Valid);
unsatCoreSet = new HashSet<Variable>();
foreach (int i in unsatCore)
{
Expand Down
10 changes: 5 additions & 5 deletions Source/Provers/SMTLib/ProverInterface.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ public virtual int StartingProcId()
return 0;
}

public virtual void OnModel(IList<string> labels, Model model, Outcome proverOutcome)
public virtual void OnModel(IList<string> labels, Model model, SolverOutcome proverOutcome)
{
Contract.Requires(cce.NonNullElements(labels));
}
Expand Down Expand Up @@ -157,7 +157,7 @@ public virtual Absy Label2Absy(string label)
}
}

public abstract Task<Outcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken);
public abstract Task<SolverOutcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken);

public virtual void LogComment(string comment)
{
Expand Down Expand Up @@ -232,13 +232,13 @@ public virtual void Check()
}

// (check-sat + get-unsat-core + checkOutcome)
public virtual Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions, ErrorHandler handler,
public virtual Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions, ErrorHandler handler,
CancellationToken cancellationToken)
{
throw new NotImplementedException();
}

public virtual Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
public virtual Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
ErrorHandler handler, CancellationToken cancellationToken)
{
throw new NotImplementedException();
Expand Down Expand Up @@ -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,
Expand Down
22 changes: 11 additions & 11 deletions Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ public override int FlushAxiomsToTheoremProver()
return 0;
}

public override async Task<Outcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit,
public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit,
CancellationToken cancellationToken)
{
currentErrorHandler = handler;
Expand Down Expand Up @@ -134,7 +134,7 @@ private Task<IReadOnlyList<SExpr>> SendRequestsAndClose(IReadOnlyList<string> re
return Process.SendRequestsAndCloseInput(sanitizedRequests, cancellationToken);
}

private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
private async Task<SolverOutcome> CheckSat(CancellationToken cancellationToken)
{
var requests = new List<string>();
requests.Add("(check-sat)");
Expand All @@ -148,7 +148,7 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
}

if (Process == null || HadErrors) {
return Outcome.Undetermined;
return SolverOutcome.Undetermined;
}

try {
Expand All @@ -159,7 +159,7 @@ private async Task<Outcome> CheckSat(CancellationToken cancellationToken)
catch (TimeoutException) {
currentErrorHandler.OnResourceExceeded("hard solver timeout");
resourceCount = -1;
return Outcome.TimeOut;
return SolverOutcome.TimeOut;
}
var responseStack = new Stack<SExpr>(responses.Reverse());

Expand All @@ -176,8 +176,8 @@ private async Task<Outcome> 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;
}
}

Expand All @@ -186,16 +186,16 @@ private async Task<Outcome> 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);
}
Expand Down Expand Up @@ -294,13 +294,13 @@ public override Task<List<string>> UnsatCore()
throw new NotSupportedException("Batch mode solver interface does not support unsat cores.");
}

public override Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions,
public override Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> assumptions,
ErrorHandler handler, CancellationToken cancellationToken)
{
throw new NotSupportedException("Batch mode solver interface does not support checking assumptions.");
}

public override Task<(Outcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
public override Task<(SolverOutcome, List<int>)> CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions,
ErrorHandler handler, CancellationToken cancellationToken)
{
throw new NotSupportedException("Batch mode solver interface does not support checking assumptions.");
Expand Down
Loading
Loading