Fixed issue in the verification result caching.

5 files changed, 19 insertions, 13 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index ef2676d0..a53165b6 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -3218,14 +3218,18 @@ namespace Microsoft.Boogie {
       return ErrorChecksumToCachedError.ContainsKey(checksum);

     }

 

-    public void SetErrorChecksumToCachedError(IEnumerable<Tuple<byte[], object>> errors)

+    public void SetErrorChecksumToCachedError(IEnumerable<Tuple<byte[], byte[], object>> errors)

     {

       Contract.Requires(errors != null);

 

       ErrorChecksumToCachedError = new Dictionary<byte[], object>(ChecksumComparer.Default);

       foreach (var kv in errors)

       {

-        ErrorChecksumToCachedError[kv.Item1] = kv.Item2;

+        ErrorChecksumToCachedError[kv.Item1] = kv.Item3;

+        if (kv.Item2 != null)

+        {

+          ErrorChecksumToCachedError[kv.Item2] = null;

+        }

       }

     }

 

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 8f7aa185..066808ae 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -994,9 +994,7 @@ namespace Microsoft.Boogie {
         var assertRequiresCmd = assertCmd as AssertRequiresCmd;

         if (assertRequiresCmd != null)

         {

-          // Add the checksum of the call instead of the assertion itself

-          // because a corresponding counterexample will also have the

-          // checksum of the failing call.

+          impl.AddAssertionChecksum(assertRequiresCmd.Checksum);

           impl.AddAssertionChecksum(assertRequiresCmd.Call.Checksum);

           assertRequiresCmd.SugaredCmdChecksum = assertRequiresCmd.Call.Checksum;

         }

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 5bce360b..e25c9306 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -166,12 +166,12 @@ namespace Microsoft.Boogie
     {

       if (result.Outcome == ConditionGeneration.Outcome.Errors && result.Errors != null && result.Errors.Count < CommandLineOptions.Clo.ProverCCLimit)

       {

-        implementation.SetErrorChecksumToCachedError(result.Errors.Select(cex => new Tuple<byte[], object>(cex.Checksum, cex)));

+        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)

       {

-        implementation.SetErrorChecksumToCachedError(new List<Tuple<byte[], object>>());

+        implementation.SetErrorChecksumToCachedError(new List<Tuple<byte[], byte[], object>>());

         implementation.AssertionChecksumsInCachedSnapshot = result.AssertionChecksums;

       }

     }

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 640b0db2..178f8ddb 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -84,6 +84,7 @@ namespace Microsoft.Boogie {
     public string OriginalRequestId;

     public string RequestId;

     public abstract byte[] Checksum { get; }

+    public byte[] SugaredCmdChecksum;

 

     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;

 

@@ -420,7 +421,7 @@ namespace Microsoft.Boogie {
     }

 

 

-    public CallCounterexample(List<Block> trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public CallCounterexample(List<Block> trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context, byte[] checksum = null)

       : base(trace, model, mvInfo, context) {

       Contract.Requires(!failingRequires.Free);

       Contract.Requires(trace != null);

@@ -429,20 +430,23 @@ namespace Microsoft.Boogie {
       Contract.Requires(failingRequires != null);

       this.FailingCall = failingCall;

       this.FailingRequires = failingRequires;

+      this.checksum = checksum;

+      this.SugaredCmdChecksum = failingCall.Checksum;

     }

 

     public override int GetLocation() {

       return FailingCall.tok.line * 1000 + FailingCall.tok.col;

     }

 

+    byte[] checksum;

     public override byte[] Checksum

     {

-      get { return FailingCall.Checksum; }

+      get { return checksum; }

     }

 

     public override Counterexample Clone()

     {

-        var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context);

+        var ret = new CallCounterexample(Trace, FailingCall, FailingRequires, Model, MvInfo, Context, Checksum);

         ret.calleeCounterexamples = calleeCounterexamples;

         return ret;

     }

@@ -1540,7 +1544,7 @@ namespace VC {
         var dropCmd = false;

         var relevantAssumpVars = currentImplementation != null ? currentImplementation.RelevantInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();

         var relevantDoomedAssumpVars = currentImplementation != null ? currentImplementation.RelevantDoomedInjectedAssumptionVariables(incarnationMap) : new List<LocalVariable>();

-        var checksum = pc.SugaredCmdChecksum != null ? pc.SugaredCmdChecksum : pc.Checksum;

+        var checksum = pc.Checksum;

         if (pc is AssertCmd) {

           var ac = (AssertCmd)pc;

           ac.OrigExpr = ac.Expr;

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index d92f8661..5e83a337 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1626,7 +1626,7 @@ namespace VC {
         outcome = Outcome.Errors;

         foreach (var a in impl.RecycledFailingAssertions)

         {

-          var checksum = a.SugaredCmdChecksum != null ? a.SugaredCmdChecksum : a.Checksum;

+          var checksum = a.Checksum;

           var oldCex = impl.ErrorChecksumToCachedError[checksum] as Counterexample;

           if (oldCex != null)

           {

@@ -2965,7 +2965,7 @@ namespace VC {
       {

         AssertRequiresCmd assertCmd = (AssertRequiresCmd)cmd;

         Contract.Assert(assertCmd != null);

-        CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires, errModel, mvInfo, context);

+        CallCounterexample cc = new CallCounterexample(trace, assertCmd.Call, assertCmd.Requires, errModel, mvInfo, context, assertCmd.Checksum);

         cc.relatedInformation = relatedInformation;

         return cc;

       }