Skip to content

Commit

Permalink
Merge branch 'master' into shazqadeer-patch-1
Browse files Browse the repository at this point in the history
  • Loading branch information
@shazqadeer
shazqadeer authored Jan 26, 2024
2 parents 98b3aa2 + a09ff24 commit f920ad6
Show file tree
Hide file tree
Showing 39 changed files with 1,046 additions and 1,182 deletions.
4 changes: 2 additions & 2 deletions Source/ExecutionEngine/ConsolePrinter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -206,11 +206,11 @@ public virtual void ReportStartVerifyImplementation(Implementation implementatio
// Do not print anything to console
}

public virtual void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result) {
public virtual void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result) {
// Do not print anything to console
}

public virtual void ReportSplitResult(Split split, VCResult splitResult) {
public virtual void ReportSplitResult(Split split, VerificationRunResult splitResult) {
// Do not print anything to console
}
}
134 changes: 67 additions & 67 deletions Source/ExecutionEngine/ExecutionEngine.cs
View file

Large diffs are not rendered by default.

22 changes: 11 additions & 11 deletions Source/ExecutionEngine/VerificationResult.cs → ...xecutionEngine/ImplementationRunResult.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@

namespace Microsoft.Boogie;

public sealed class VerificationResult
public sealed class ImplementationRunResult
{
private readonly Implementation implementation;
public readonly string ProgramId;
Expand Down Expand Up @@ -37,20 +37,20 @@ public int ProofObligationCount
public int ProofObligationCountBefore { get; set; }
public int ProofObligationCountAfter { get; set; }

public ConditionGeneration.Outcome Outcome { get; set; }
public VcOutcome VcOutcome { get; set; }
public List<Counterexample> Errors = new();
public List<VCResult> VCResults;
public List<VerificationRunResult> VCResults;

public ErrorInformation ErrorBeforeVerification { get; set; }

public VerificationResult(Implementation implementation, string programId = null)
public ImplementationRunResult(Implementation implementation, string programId = null)
{
this.implementation = implementation;
ProgramId = programId;
}

public ErrorInformation GetOutcomeError(ExecutionEngineOptions options) {
return ExecutionEngine.GetOutcomeError(options, Outcome, implementation.VerboseName, implementation.tok, MessageIfVerifies,
return ExecutionEngine.GetOutcomeError(options, VcOutcome, implementation.VerboseName, implementation.tok, MessageIfVerifies,
TextWriter.Null, implementation.GetTimeLimit(options), Errors);
}

Expand All @@ -62,11 +62,11 @@ public String GetOutput(OutputPrinter printer,
printer.WriteErrorInformation(ErrorBeforeVerification, result);
}

engine.ProcessOutcome(printer, Outcome, Errors, TimeIndication(engine.Options), stats,
engine.ProcessOutcome(printer, VcOutcome, Errors, TimeIndication(engine.Options), stats,
result, implementation.GetTimeLimit(engine.Options), er, implementation.VerboseName, implementation.tok,
MessageIfVerifies);

engine.ProcessErrors(printer, Errors, Outcome, result, er, implementation);
engine.ProcessErrors(printer, Errors, VcOutcome, result, er, implementation);

return result.ToString();
}
Expand All @@ -79,12 +79,12 @@ public void ProcessXml(ExecutionEngine engine) {
lock (engine.Options.XmlSink) {
engine.Options.XmlSink.WriteStartMethod(implementation.VerboseName, Start);

foreach (var vcResult in VCResults.OrderBy(s => (s.vcNum, s.iteration))) {
engine.Options.XmlSink.WriteSplit(vcResult.vcNum, vcResult.iteration, vcResult.asserts, vcResult.startTime,
vcResult.outcome.ToString().ToLowerInvariant(), vcResult.runTime, vcResult.resourceCount);
foreach (var vcResult in VCResults.OrderBy(s => (vcNum: s.VcNum, iteration: s.Iteration))) {
engine.Options.XmlSink.WriteSplit(vcResult.VcNum, vcResult.Iteration, vcResult.Asserts, vcResult.StartTime,
vcResult.Outcome.ToString().ToLowerInvariant(), vcResult.RunTime, vcResult.ResourceCount);
}

engine.Options.XmlSink.WriteEndMethod(Outcome.ToString().ToLowerInvariant(),
engine.Options.XmlSink.WriteEndMethod(VcOutcome.ToString().ToLowerInvariant(),
End, Elapsed,
ResourceCount);
}
Expand Down
4 changes: 2 additions & 2 deletions Source/ExecutionEngine/ImplementationTask.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ public interface IVerificationStatus {}
/// <summary>
/// Results are available
/// </summary>
public record Completed(VerificationResult Result) : IVerificationStatus;
public record Completed(ImplementationRunResult Result) : IVerificationStatus;

/// <summary>
/// Scheduled to be run but waiting for resources
Expand All @@ -32,7 +32,7 @@ public record Stale : IVerificationStatus;
/// </summary>
public record Running : IVerificationStatus;

public record BatchCompleted(Split Split, VCResult VcResult) : IVerificationStatus;
public record BatchCompleted(Split Split, VerificationRunResult VerificationRunResult) : IVerificationStatus;

public interface IImplementationTask {
IVerificationStatus CacheStatus { get; }
Expand Down
2 changes: 1 addition & 1 deletion Source/ExecutionEngine/OutputPrinter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,5 +14,5 @@ public interface OutputPrinter
void WriteTrailer(TextWriter textWriter, PipelineStatistics stats);
void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true);
void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null);
void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result);
void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result);
}
14 changes: 7 additions & 7 deletions Source/ExecutionEngine/VerificationResultCache.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -229,16 +229,16 @@ public static void Inject(ExecutionEngine engine, Program program,
}

private void SetErrorAndAssertionChecksumsInCachedSnapshot(Implementation implementation,
VerificationResult result)
ImplementationRunResult result)
{
if (result.Outcome == ConditionGeneration.Outcome.Errors && result.Errors != null &&
if (result.VcOutcome == VcOutcome.Errors && result.Errors != null &&
result.Errors.Count < options.ErrorLimit)
{
implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex =>
new Tuple<byte[], byte[], object>(cex.Checksum, cex.SugaredCmdChecksum, cex)));
implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;
}
else if (result.Outcome == ConditionGeneration.Outcome.Correct)
else if (result.VcOutcome == VcOutcome.Correct)
{
implementation.SetErrorChecksumToCachedError(new List<Tuple<byte[], byte[], object>>());
implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;
Expand Down Expand Up @@ -690,7 +690,7 @@ public Program CachedProgram(string programId) {
private readonly CacheItemPolicy Policy = new CacheItemPolicy
{SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default};

public void Insert(Implementation impl, VerificationResult result)
public void Insert(Implementation impl, ImplementationRunResult result)
{
Contract.Requires(impl != null);
Contract.Requires(result != null);
Expand All @@ -699,11 +699,11 @@ public void Insert(Implementation impl, VerificationResult result)
}


public VerificationResult Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)
public ImplementationRunResult Lookup(Implementation impl, bool runDiagnosticsOnTimeout, out int priority)
{
Contract.Requires(impl != null);

var result = Cache.Get(impl.Id) as VerificationResult;
var result = Cache.Get(impl.Id) as ImplementationRunResult;
if (result == null)
{
priority = Priority.HIGH;
Expand All @@ -716,7 +716,7 @@ public VerificationResult Lookup(Implementation impl, bool runDiagnosticsOnTimeo
{
priority = Priority.LOW;
}
else if (result.Outcome == ConditionGeneration.Outcome.TimedOut && runDiagnosticsOnTimeout)
else if (result.VcOutcome == VcOutcome.TimedOut && runDiagnosticsOnTimeout)
{
priority = Priority.MEDIUM;
}
Expand Down
64 changes: 32 additions & 32 deletions Source/Houdini/Houdini.cs
View file
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(ProverInterface.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(ProverInterface.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(ProverInterface.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(ProverInterface.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(ProverInterface.Outcome outcome, List<Counterexample> errors)
private bool IsOutcomeNotHoudini(SolverOutcome outcome, List<Counterexample> errors)
{
switch (outcome)
{
case ProverInterface.Outcome.Valid:
case SolverOutcome.Valid:
return false;
case ProverInterface.Outcome.Invalid:
case SolverOutcome.Invalid:
Contract.Assume(errors != null);
foreach (Counterexample error in errors)
{
Expand All @@ -863,14 +863,14 @@ private bool IsOutcomeNotHoudini(ProverInterface.Outcome outcome, List<Counterex
// Return true if there was at least one non-candidate error
protected bool UpdateHoudiniOutcome(HoudiniOutcome houdiniOutcome,
Implementation implementation,
ProverInterface.Outcome outcome,
SolverOutcome outcome,
List<Counterexample> errors)
{
string implName = implementation.Name;
houdiniOutcome.implementationOutcomes.Remove(implName);
List<Counterexample> nonCandidateErrors = new List<Counterexample>();

if (outcome == ProverInterface.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(ProverInterface.Outcome outcome,
protected bool UpdateAssignmentWorkList(SolverOutcome outcome,
List<Counterexample> errors)
{
Contract.Assume(currentHoudiniState.Implementation != null);
bool dequeue = true;

switch (outcome)
{
case ProverInterface.Outcome.Valid:
case SolverOutcome.Valid:
//yeah, dequeue
break;

case ProverInterface.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<(ProverInterface.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 (ProverInterface.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 == ProverInterface.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 == ProverInterface.Outcome.Valid)
if (Options.UseUnsatCoreForContractInfer && outcome == SolverOutcome.Valid)
{
await session.UpdateUnsatCore(proverInterface, currentHoudiniState.Assignment);
}
Expand Down Expand Up @@ -1704,12 +1704,12 @@ public static void ApplyAssignment(Program prog, HoudiniOutcome outcome)

public class VCGenOutcome
{
public VCGen.Outcome outcome;
public VcOutcome VcOutcome;
public List<Counterexample> errors;

public VCGenOutcome(ProverInterface.Outcome outcome, List<Counterexample> errors)
public VCGenOutcome(SolverOutcome outcome, List<Counterexample> errors)
{
this.outcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
this.VcOutcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
this.errors = errors;
}
}
Expand All @@ -1724,12 +1724,12 @@ public class HoudiniOutcome

// statistics

private int CountResults(VCGen.Outcome outcome)
private int CountResults(VcOutcome vcOutcome)
{
int outcomeCount = 0;
foreach (VCGenOutcome verifyOutcome in implementationOutcomes.Values)
{
if (verifyOutcome.outcome == outcome)
if (verifyOutcome.VcOutcome == vcOutcome)
{
outcomeCount++;
}
Expand All @@ -1738,12 +1738,12 @@ private int CountResults(VCGen.Outcome outcome)
return outcomeCount;
}

private List<string> ListOutcomeMatches(VCGen.Outcome outcome)
private List<string> ListOutcomeMatches(VcOutcome vcOutcome)
{
List<string> result = new List<string>();
foreach (KeyValuePair<string, VCGenOutcome> kvpair in implementationOutcomes)
{
if (kvpair.Value.outcome == outcome)
if (kvpair.Value.VcOutcome == vcOutcome)
{
result.Add(kvpair.Key);
}
Expand All @@ -1754,37 +1754,37 @@ private List<string> ListOutcomeMatches(VCGen.Outcome outcome)

public int ErrorCount
{
get { return CountResults(VCGen.Outcome.Errors); }
get { return CountResults(VcOutcome.Errors); }
}

public int Verified
{
get { return CountResults(VCGen.Outcome.Correct); }
get { return CountResults(VcOutcome.Correct); }
}

public int Inconclusives
{
get { return CountResults(VCGen.Outcome.Inconclusive); }
get { return CountResults(VcOutcome.Inconclusive); }
}

public int TimeOuts
{
get { return CountResults(VCGen.Outcome.TimedOut); }
get { return CountResults(VcOutcome.TimedOut); }
}

public List<string> ListOfTimeouts
{
get { return ListOutcomeMatches(VCGen.Outcome.TimedOut); }
get { return ListOutcomeMatches(VcOutcome.TimedOut); }
}

public List<string> ListOfInconclusives
{
get { return ListOutcomeMatches(VCGen.Outcome.Inconclusive); }
get { return ListOutcomeMatches(VcOutcome.Inconclusive); }
}

public List<string> ListOfErrors
{
get { return ListOutcomeMatches(VCGen.Outcome.Errors); }
get { return ListOutcomeMatches(VcOutcome.Errors); }
}
}
}
Loading

0 comments on commit f920ad6

Please sign in to comment.