Code review

boogie-org · Feb 2, 2024 · beef94a · beef94a
1 parent 83888e8
commit beef94a
Show file tree

Hide file tree

Showing 7 changed files with 25 additions and 22 deletions.
diff --git a/Source/ExecutionEngine/ImplementationRunResult.cs b/Source/ExecutionEngine/ImplementationRunResult.cs
@@ -76,8 +76,8 @@ public void ProcessXml(ExecutionEngine engine) {
     lock (engine.Options.XmlSink) {
       engine.Options.XmlSink.WriteStartMethod(implementation.VerboseName, Start);
 
-      foreach (var vcResult in RunResults.OrderBy(s => (s.vcNum, iteration: s.Iteration))) {
-        engine.Options.XmlSink.WriteSplit(vcResult.vcNum, vcResult.Iteration, vcResult.Asserts, vcResult.StartTime,
+      foreach (var vcResult in RunResults.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);
       }
 

diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs
@@ -21,7 +21,7 @@ public class VerificationTask : IVerificationTask {
   public ProcessedProgram ProcessedProgram { get; }
 
   public IToken ScopeToken => Split.Implementation.tok;
-  public string ScopeId => Split.Implementation.VerboseName; // TODO this verbose name threw me off. Why do we need it besides the regular name?
+  public string ScopeId => Split.Implementation.VerboseName;
 
   public IToken Token => Split.Token;
   public ManualSplit Split { get; }
@@ -122,14 +122,6 @@ await Split.BeginCheck(Split.Run.OutputWriter, checker, collector,
       await checker.ProverTask;
       var result = Split.ReadOutcome(0, checker, collector);
 
-      // if (SplitAndVerifyWorker.IsProverFailed(result.Outcome)) {
-      //   // Update one last time the result with the dummy counter-example to indicate the position of the failure
-      //   var cex = Split.ToCounterexample(checker.TheoremProver.Context);
-      //   Split.Counterexamples.Add(cex);
-      //   result = result with {
-      //     CounterExamples = Split.Counterexamples
-      //   };
-      // }
       CacheStatus = new Completed(result);
       yield return CacheStatus;
     }

diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs
@@ -365,13 +365,19 @@ public async Task StatusTest() {
     Assert.AreEqual(secondName, statusList[4].Item1);
     Assert.IsTrue(statusList[4].Item2 is Completed);
 
+    Assert.True(tasks[0].CacheStatus is Completed);
+    Assert.AreEqual(SolverOutcome.Invalid, ((Completed)tasks[0].CacheStatus).Result.Outcome);
+
+    Assert.True(tasks[1].CacheStatus is Completed);
+    Assert.AreEqual(SolverOutcome.Valid, ((Completed)tasks[1].CacheStatus).Result.Outcome);
+
     // Caching is currently not working
-    // var tasks2 = engine.GetVerificationTasks(program);
-    // Assert.True(tasks2[0].CacheStatus is Completed);
-    // Assert.AreEqual(VcOutcome.Errors, ((Completed)tasks2[0].CacheStatus).Result.Outcome);
-    //
-    // Assert.True(tasks2[1].CacheStatus is Completed);
-    // Assert.AreEqual(VcOutcome.Correct, ((Completed)tasks2[1].CacheStatus).Result.Outcome);
+    var tasks2 = engine.GetVerificationTasks(program);
+    Assert.True(tasks2[0].CacheStatus is Completed);
+    Assert.AreEqual(SolverOutcome.Invalid, ((Completed)tasks2[0].CacheStatus).Result.Outcome);
+
+    Assert.True(tasks2[1].CacheStatus is Completed);
+    Assert.AreEqual(SolverOutcome.Valid, ((Completed)tasks2[1].CacheStatus).Result.Outcome);
 
     var batchResult = (Completed) statusList[2].Item2;
 

diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs
@@ -43,7 +43,8 @@ public static IEnumerable<ManualSplit> FocusAndSplit(VCGenOptions options, Imple
           var token = pair.Value[i];
           bool lastSplitInBlock = i == pair.Value.Count - 1;
           var newBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, i, pair.Key, lastSplitInBlock, splitOnEveryAssert);
-          splits.Add(new ManualSplit(initialSplit.Options, BlockTransformations.PostProcess(newBlocks), initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, token)); // REVIEW: Does gotoCmdOrigins need to be changed at all?
+          splits.Add(new ManualSplit(initialSplit.Options, 
+            BlockTransformations.PostProcess(newBlocks), initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, token));
         }
       }
     }

diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs
@@ -889,7 +889,7 @@ public VerificationRunResult ReadOutcome(int iteration, Checker checker, Verifie
 
         var resourceCount = checker.GetProverResourceCount();
         var result = new VerificationRunResult(
-          vcNum: SplitIndex + 1,
+          VcNum: SplitIndex + 1,
           Iteration: iteration,
           StartTime: checker.ProverStart,
           Outcome: outcome,

diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs
@@ -34,9 +34,13 @@ public class SplitAndVerifyWorker
 
     private int totalResourceCount;
 
-    public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator,
+    public SplitAndVerifyWorker(
+      VCGenOptions options, 
+      VerificationConditionGenerator verificationConditionGenerator,
       ImplementationRun run,
-      Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo,
+      Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, 
+      VerifierCallback callback, 
+      ModelViewInfo mvInfo,
       VcOutcome vcOutcome)
     {
       this.options = options;

diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs
@@ -8,7 +8,7 @@ namespace VC
 {
   public record VerificationRunResult
   (
-    int vcNum,
+    int VcNum,
     int Iteration,
     DateTime StartTime,
     SolverOutcome Outcome,