Fixed issue in the verification result caching.

9 files changed, 78 insertions, 15 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;

       }

diff --git a/Test/snapshots/Snapshots30.v0.bpl b/Test/snapshots/Snapshots30.v0.bpl
new file mode 100644
index 00000000..459c4007
--- /dev/null
+++ b/Test/snapshots/Snapshots30.v0.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "0"} P();

+

+implementation {:id "P"} {:checksum "1"} P()

+{

+    call Q();

+}

+

+procedure {:checksum "2"} Q();

+  requires 0 == 0;

+  requires 1 == 1;

+  requires 2 != 2;

+  requires 3 == 3;

+  requires 4 == 4;

diff --git a/Test/snapshots/Snapshots30.v1.bpl b/Test/snapshots/Snapshots30.v1.bpl
new file mode 100644
index 00000000..089a1939
--- /dev/null
+++ b/Test/snapshots/Snapshots30.v1.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "0"} P();

+

+implementation {:id "P"} {:checksum "2"} P()

+{

+    call Q();

+    assert 5 == 5;

+}

+

+procedure {:checksum "2"} Q();

+  requires 0 == 0;

+  requires 1 == 1;

+  requires 2 != 2;

+  requires 3 == 3;

+  requires 4 == 4;

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index 484fa8e2..fb476128 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl > "%t"

+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl > "%t"

 // RUN: %diff "%s.expect" "%t"

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index f34fefbe..d8642441 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -72,7 +72,7 @@ Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_sn
 Processing command (at Snapshots2.v5.bpl(7,5)) assert F0();

   >>> MarkAsFullyVerified

 Processing command (at Snapshots2.v5.bpl(3,1)) assert F0();

-  >>> DoNothingToAssert

+  >>> MarkAsFullyVerified

 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing command (at Snapshots3.v0.bpl(2,1)) assert G();

@@ -516,3 +516,33 @@ Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0;
 Snapshots28.v1.bpl(15,5): Error BP5001: This assertion might not hold.

 

 Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots30.v0.bpl(5,5)) assert 0 == 0;

+  >>> DoNothingToAssert

+Processing command (at Snapshots30.v0.bpl(5,5)) assert 1 == 1;

+  >>> DoNothingToAssert

+Processing command (at Snapshots30.v0.bpl(5,5)) assert 2 != 2;

+  >>> DoNothingToAssert

+Processing command (at Snapshots30.v0.bpl(5,5)) assert 3 == 3;

+  >>> DoNothingToAssert

+Processing command (at Snapshots30.v0.bpl(5,5)) assert 4 == 4;

+  >>> DoNothingToAssert

+Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.

+Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.

+

+Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots30.v1.bpl(5,5)) assert 0 == 0;

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots30.v1.bpl(5,5)) assert 1 == 1;

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots30.v1.bpl(5,5)) assert 2 != 2;

+  >>> RecycleError

+Processing command (at Snapshots30.v1.bpl(5,5)) assert 3 == 3;

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots30.v1.bpl(5,5)) assert 4 == 4;

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots30.v1.bpl(6,5)) assert 5 == 5;

+  >>> DoNothingToAssert

+Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.

+Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.

+

+Boogie program verifier finished with 0 verified, 1 error