Worked on the more advanced verification result caching.

2 files changed, 15 insertions, 21 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 33f36a31..cdeb6c2c 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -81,6 +81,7 @@ namespace Microsoft.Boogie {
     public ProverContext Context;

     [Peer]

     public List<string>/*!>!*/ relatedInformation;

+    public string OriginalRequestId;

     public string RequestId;

     public abstract byte[] Checksum { get; }

 

@@ -1103,6 +1104,10 @@ namespace VC {
         {

           ce.RequestId = RequestId;

         }

+        if (ce.OriginalRequestId == null)

+        {

+          ce.OriginalRequestId = RequestId;

+        }

         examples.Add(ce);

       }

 

@@ -1420,10 +1425,10 @@ namespace VC {
         byte[] currentChecksum = null;

         foreach (Block p in b.Predecessors) {

           p.succCount--;

-          if (b.Checksum != null)

+          if (p.Checksum != null)

           {

             // Compute the checksum based on the checksums of the predecessor. The order should not matter.

-            currentChecksum = ChecksumHelper.CombineChecksums(b.Checksum, currentChecksum, true);

+            currentChecksum = ChecksumHelper.CombineChecksums(p.Checksum, currentChecksum, true);

           }

           if (p.succCount == 0)

             block2Incarnation.Remove(p);

@@ -1532,11 +1537,13 @@ namespace VC {
                    && currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)

                    && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))

           {

+            // TODO(wuestholz): Do the same for assertions if they have been proved in the previous snapshot.

+

             // Turn it into an assume statement.

-            // TODO(wuestholz): Uncomment this once the canned errors are reported.            

+            // TODO(wuestholz): Uncomment this.

             // pc = new AssumeCmd(ac.tok, copy);

-            pc.Attributes = new QKeyValue(Token.NoToken, "canned_failing_assertion", new List<object>(), pc.Attributes);

-            currentImplementation.AddCannedFailingAssertion(ac);

+            pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);

+            currentImplementation.AddRecycledFailingAssertion(ac);

           }

         }

         else if (pc is AssumeCmd

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 3e601511..239cecdb 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1620,30 +1620,18 @@ namespace VC {
 

       Outcome outcome = Outcome.Correct;

 

-      // Report all canned failing assertions for this implementation.

-      if (impl.CannedFailingAssertions != null && impl.CannedFailingAssertions.Any())

+      // Report all recycled failing assertions for this implementation.

+      if (impl.RecycledFailingAssertions != null && impl.RecycledFailingAssertions.Any())

       {

         // TODO(wuestholz): Uncomment this.

         // outcome = Outcome.Errors;

-        foreach (var a in impl.CannedFailingAssertions)

+        foreach (var a in impl.RecycledFailingAssertions)

         {

           var oldCex = impl.ErrorChecksumToCachedError[a.Checksum] as Counterexample;

           if (oldCex != null)

           {

-            // TODO(wuestholz): Maybe we could create a "fresh" counterexample instead.

-            // TransferCmd trCmd = null;

-            // var oldRetCex = oldCex as ReturnCounterexample;

-            // if (oldRetCex != null)

-            // {

-            //   trCmd = oldRetCex.FailingReturn;

-            // }

-            // var cex = AssertCmdToCounterexample(a, trCmd, oldCex.Trace, oldCex.Model, oldCex.MvInfo, oldCex.Context);

-            // cex.RequestId = oldCex.RequestId;

-

             // TODO(wuestholz): Uncomment this.

-            // var oldReqId = oldCex.RequestId;

             // callback.OnCounterexample(oldCex, null);

-            // oldCex.RequestId = oldReqId;

           }

         }

       }

@@ -2677,7 +2665,6 @@ namespace VC {
         #region Get rid of empty blocks

         {

           RemoveEmptyBlocksIterative(impl.Blocks);

-          // TODO(wuestholz): Update impl.AssertionChecksums and maybe impl.CannedFailingAssertions.

           impl.PruneUnreachableBlocks();

         }

         #endregion Get rid of empty blocks