Some refactoring in the VCGeneration assembly

Source/ExecutionEngine/ConsolePrinter.cs

@@ -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
   }
 }

Source/ExecutionEngine/VerificationResult.cs → Source/ExecutionEngine/ImplementationRunResult.cs

@@ -7,7 +7,7 @@
 
 namespace Microsoft.Boogie;
 
-public sealed class VerificationResult
+public sealed class ImplementationRunResult
 {
   private readonly Implementation implementation;
   public readonly string ProgramId;
@@ -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);
   }
 
@@ -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();
   }
@@ -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);
     }

Source/ExecutionEngine/ImplementationTask.cs

@@ -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
@@ -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; }

Source/ExecutionEngine/OutputPrinter.cs

@@ -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);
 }

Source/ExecutionEngine/VerificationResultCache.cs

@@ -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;
@@ -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);
@@ -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;
@@ -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;
       }

Source/Houdini/Houdini.cs

@@ -52,7 +52,7 @@ public virtual void UpdateAssignment(Dictionary<Variable, bool> assignment)
     {
     }
 
-    public virtual void UpdateOutcome(ProverInterface.Outcome outcome)
+    public virtual void UpdateOutcome(Outcome outcome)
     {
     }
 
@@ -158,7 +158,7 @@ public override void UpdateImplementation(Implementation implementation)
       curImp = implementation;
     }
 
-    public override void UpdateOutcome(ProverInterface.Outcome o)
+    public override void UpdateOutcome(Outcome o)
     {
       Contract.Assert(curImp != null);
       DateTime endT = DateTime.UtcNow;
@@ -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(Outcome outcome)
     {
       wr.WriteLine("analysis outcome :" + outcome);
       wr.Flush();
@@ -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(Outcome outcome)
     {
       Notify((NotifyDelegate) delegate(HoudiniObserver r) { r.UpdateOutcome(outcome); });
     }
@@ -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(Outcome outcome, List<Counterexample> errors)
     {
       switch (outcome)
       {
-        case ProverInterface.Outcome.Valid:
+        case Outcome.Valid:
           return false;
-        case ProverInterface.Outcome.Invalid:
+        case Outcome.Invalid:
           Contract.Assume(errors != null);
           foreach (Counterexample error in errors)
           {
@@ -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,
+      Outcome 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 == Outcome.Invalid)
       {
         foreach (Counterexample error in errors)
         {
@@ -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(Outcome outcome,
       List<Counterexample> errors)
     {
       Contract.Assume(currentHoudiniState.Implementation != null);
       bool dequeue = true;
 
       switch (outcome)
       {
-        case ProverInterface.Outcome.Valid:
+        case Outcome.Valid:
           //yeah, dequeue
           break;
 
-        case ProverInterface.Outcome.Invalid:
+        case Outcome.Invalid:
           Contract.Assume(errors != null);
 
           foreach (Counterexample error in errors)
@@ -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<(Outcome, 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 (Outcome.Undetermined, null);
       }
 
     }
@@ -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 == Outcome.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 == ProverInterface.Outcome.Valid)
+          if (Options.UseUnsatCoreForContractInfer && outcome == Outcome.Valid)
           {
             await session.UpdateUnsatCore(proverInterface, currentHoudiniState.Assignment);
           }
@@ -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(Outcome outcome, List<Counterexample> errors)
     {
-      this.outcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
+      this.VcOutcome = ConditionGeneration.ProverInterfaceOutcomeToConditionGenerationOutcome(outcome);
       this.errors = errors;
     }
   }
@@ -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++;
         }
@@ -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);
         }
@@ -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); }
     }
   }
 }