Added /verifySnapshots:3, which prints recycled errors messages with the source locations of the new code.

8 files changed, 191 insertions, 62 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index be371fcb..a17ff9c7 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1492,7 +1492,7 @@ namespace Microsoft.Boogie {
           return true;

 

         case "verifySnapshots":

-          ps.GetNumericArgument(ref VerifySnapshots, 3);

+          ps.GetNumericArgument(ref VerifySnapshots, 4);

           return true;

 

         case "traceCaching":

@@ -1944,6 +1944,10 @@ namespace Microsoft.Boogie {
                 0 - do not use any verification result caching (default)

                 1 - use the basic verification result caching

                 2 - use the more advanced verification result caching

+                3 - use the more advanced caching and report errors according

+                    to the new source locations for errors and their

+                    related locations (but not /errorTrace and CaptureState

+                    locations) 

   /verifySeparately

                 verify each input program separately

   /removeEmptyBlocks:<c>

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 67ce49a5..a408642a 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -151,25 +151,18 @@ namespace Microsoft.Boogie
     {

       Contract.Requires(message != null);

 

-      if (category != null)

-      {

+      if (category != null) {

         message = string.Format("{0}: {1}", category, message);

       }

       string s;

-      if (tok != null)

-      {

+      if (tok != null) {

         s = string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(tok.filename), tok.line, tok.col, message);

-      }

-      else

-      {

+      } else {

         s = message;

       }

-      if (error)

-      {

+      if (error) {

         ErrorWriteLine(tw, s);

-      }

-      else

-      {

+      } else {

         tw.WriteLine(s);

       }

     }

@@ -1114,23 +1107,23 @@ namespace Microsoft.Boogie
       printer.Inform(string.Format("Verifying {0} ...", impl.Name), output);

 

       int priority = 0;

-      if (0 < CommandLineOptions.Clo.VerifySnapshots)

-      {

-        verificationResult = Cache.Lookup(impl, out priority);

-      }

-

       var wasCached = false;

-      if (verificationResult != null && priority == Priority.SKIP)

-      {

-        if (CommandLineOptions.Clo.XmlSink != null)

-        {

-          CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, verificationResult.Start);

-        }

+      if (0 < CommandLineOptions.Clo.VerifySnapshots) {

+        var cachedResults = Cache.Lookup(impl, out priority);

+        if (cachedResults != null && priority == Priority.SKIP) {

+          if (CommandLineOptions.Clo.XmlSink != null) {

+            CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, cachedResults.Start);

+          }

 

-        printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);

-        wasCached = true;

+          printer.Inform(string.Format("Retrieving cached verification result for implementation {0}...", impl.Name), output);

+          if (CommandLineOptions.Clo.VerifySnapshots < 3 || cachedResults.Outcome == ConditionGeneration.Outcome.Correct) {

+            verificationResult = cachedResults;

+            wasCached = true;

+          }

+        }

       }

-      else

+

+      if (!wasCached)

       {

         #region Verify the implementation

 

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index a18cee05..f8aca0e9 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -172,48 +172,28 @@ namespace Microsoft.Boogie
         var vr = ExecutionEngine.Cache.Lookup(impl, out priority);

         if (vr != null && vr.ProgramId == programId)

         {

-          if (priority == Priority.LOW)

-          {

+          if (priority == Priority.LOW) {

             run.LowPriorityImplementationCount++;

-            if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)

-            {

-              SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);

-              if (vr.ProgramId != null)

-              {

-                var p = ExecutionEngine.CachedProgram(vr.ProgramId);

-                if (p != null)

-                {

-                  eai.Inject(impl, p);

-                  run.TransformedImplementationCount++;

-                }

-              }

-            }

-          }

-          else if (priority == Priority.MEDIUM)

-          {

+          } else if (priority == Priority.MEDIUM) {

             run.MediumPriorityImplementationCount++;

-            if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)

-            {

+          } else if (priority == Priority.HIGH) {

+            run.HighPriorityImplementationCount++;

+          } else if (priority == Priority.SKIP) {

+            run.SkippedImplementationCount++;

+          }

+

+          if (priority == Priority.LOW || priority == Priority.MEDIUM || 3 <= CommandLineOptions.Clo.VerifySnapshots) {

+            if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds) {

               SetErrorAndAssertionChecksumsInCachedSnapshot(impl, vr);

-              if (vr.ProgramId != null)

-              {

+              if (vr.ProgramId != null) {

                 var p = ExecutionEngine.CachedProgram(vr.ProgramId);

-                if (p != null)

-                {

+                if (p != null) {

                   eai.Inject(impl, p);

                   run.TransformedImplementationCount++;

                 }

               }

             }

           }

-          else if (priority == Priority.HIGH)

-          {

-            run.HighPriorityImplementationCount++;

-          }

-          else if (priority == Priority.SKIP)

-          {

-            run.SkippedImplementationCount++;

-          }

         }

       }

       run.End = DateTime.UtcNow;

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 3a483a58..8e5c853c 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1763,9 +1763,18 @@ namespace VC {
         {

           var checksum = a.Checksum;

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

-          if (oldCex != null)

-          {

-            callback.OnCounterexample(oldCex, null);

+          if (oldCex != null) {

+            if (CommandLineOptions.Clo.VerifySnapshots < 3) {

+              callback.OnCounterexample(oldCex, null);

+            } else {

+              // If possible, we use the old counterexample, but with the location information of "a"

+              var cex = AssertCmdToCloneCounterexample(a, oldCex);

+              callback.OnCounterexample(cex, null);

+              // OnCounterexample may have had side effects on the RequestId and OriginalRequestId fields.  We make

+              // any such updates available in oldCex. (Is this really a good design? --KRML)

+              oldCex.RequestId = cex.RequestId;

+              oldCex.OriginalRequestId = cex.OriginalRequestId;

+            }

           }

         }

       }

@@ -3137,6 +3146,31 @@ namespace VC {
       }

     }

 

+    /// <summary>

+    /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt".

+    /// </summary>

+    public static Counterexample AssertCmdToCloneCounterexample(AssertCmd assrt, Counterexample cex) {

+      Contract.Requires(assrt != null);

+      Contract.Requires(cex != null);

+      Contract.Ensures(Contract.Result<Counterexample>() != null);

+

+      List<string> relatedInformation = new List<string>();

+

+      Counterexample cc;

+      if (assrt is AssertRequiresCmd) {

+        var aa = (AssertRequiresCmd)assrt;

+        cc = new CallCounterexample(cex.Trace, aa.Call, aa.Requires, cex.Model, cex.MvInfo, cex.Context, aa.Checksum);

+      } else if (assrt is AssertEnsuresCmd && cex is ReturnCounterexample) {

+        var aa = (AssertEnsuresCmd)assrt;

+        var oldCex = (ReturnCounterexample)cex;

+        cc = new ReturnCounterexample(cex.Trace, oldCex.FailingReturn, aa.Ensures, cex.Model, cex.MvInfo, cex.Context, aa.Checksum);

+      } else {

+        cc = new AssertCounterexample(cex.Trace, assrt, cex.Model, cex.MvInfo, cex.Context);

+      }

+      cc.relatedInformation = relatedInformation;

+      return cc;

+    }

+

     static VCExpr LetVC(Block startBlock,

                         VCExpr controlFlowVariableExpr,

                         Dictionary<int, Absy> label2absy,

diff --git a/Test/snapshots/Snapshots41.v0.bpl b/Test/snapshots/Snapshots41.v0.bpl
new file mode 100644
index 00000000..631fe544
--- /dev/null
+++ b/Test/snapshots/Snapshots41.v0.bpl
@@ -0,0 +1,35 @@
+procedure {:checksum "0"} M(x: int);

+implementation {:id "M"} {:checksum "1"} M(x: int)

+{                     assert x < 20 || 10 <= x;  // always true

+  assert x < 10;  // error

+  call Other(x);  // error: precondition violation

+}

+

+procedure {:checksum "10"} Other(y: int);

+  requires 0 <= y;

+implementation {:id "Other"} {:checksum "11"} Other(y: int)

+{

+}

+

+procedure {:checksum "20"} Posty() returns (z: int);

+  ensures 2 <= z;  // error: postcondition violation

+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)

+{

+  var t: int;

+  t := 20;

+  if (t < z) {

+  } else {  // the postcondition violation occurs on this 'else' branch

+  }

+}

+

+procedure {:checksum "30"} NoChangeWhazzoeva(u: int);

+implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)

+{

+  assert u != 53;  // error

+}

+

+procedure {:checksum "40"} NoChangeAndCorrect();

+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect()

+{

+  assert true;

+}

diff --git a/Test/snapshots/Snapshots41.v1.bpl b/Test/snapshots/Snapshots41.v1.bpl
new file mode 100644
index 00000000..0cd9fbf9
--- /dev/null
+++ b/Test/snapshots/Snapshots41.v1.bpl
@@ -0,0 +1,39 @@
+procedure {:checksum "0"} M(x: int);

+implementation {:id "M"} {:checksum "1"} M(x: int)

+{

+assert x < 20 || 10 <= x;  // always true

+  

+       assert x < 10;  // error

+  call Other(x);  // error: precondition violation

+  assert x == 7;  // error: this is a new error in v1

+}

+

+

+       procedure {:checksum "10"} Other(y: int);

+         requires 0 <= y;

+       implementation {:id "Other"} {:checksum "11"} Other(y: int)

+       {

+       }

+

+

+

+procedure {:checksum "20"} Posty() returns (z: int);

+  ensures 2 <= z;  // error: postcondition violation

+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)

+{

+  var t: int;

+  t := 20;

+  if (t < z) {

+    assert true;  // this is a new assert

+  } else {  // the postcondition violation occurs on this 'else' branch

+  }

+}

+

+  procedure   {:checksum "30"} NoChangeWhazzoeva(u: int);

+  implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)

+  {

+       assert u != 53;  // error

+  }

+

+procedure {:checksum "40"} NoChangeAndCorrect();

+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; }

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index 01a231fe..908fc2fd 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,3 @@
 // 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 Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl > "%t"

+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:3 -verifySeparately -noinfer Snapshots41.bpl >> "%t"

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

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 637dd088..9dd3d0ec 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -648,3 +648,46 @@ Processing command (at Snapshots35.v1.bpl(5,5)) assert p;
 Snapshots35.v1.bpl(5,5): Error BP5001: This assertion might not hold.

 

 Boogie program verifier finished with 0 verified, 1 error

+Processing command (at Snapshots41.v0.bpl(3,23)) assert x < 20 || 10 <= x;

+  >>> DoNothingToAssert

+Processing command (at Snapshots41.v0.bpl(4,3)) assert x < 10;

+  >>> DoNothingToAssert

+Processing command (at Snapshots41.v0.bpl(5,3)) assert 0 <= call0formal#AT#y;

+  >>> DoNothingToAssert

+Snapshots41.v0.bpl(4,3): Error BP5001: This assertion might not hold.

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

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

+Processing command (at Snapshots41.v0.bpl(15,3)) assert 2 <= z;

+  >>> DoNothingToAssert

+Snapshots41.v0.bpl(22,3): Error BP5003: A postcondition might not hold on this return path.

+Snapshots41.v0.bpl(15,3): Related location: This is the postcondition that might not hold.

+Processing command (at Snapshots41.v0.bpl(28,3)) assert u != 53;

+  >>> DoNothingToAssert

+Snapshots41.v0.bpl(28,3): Error BP5001: This assertion might not hold.

+Processing command (at Snapshots41.v0.bpl(34,3)) assert true;

+  >>> DoNothingToAssert

+

+Boogie program verifier finished with 2 verified, 4 errors

+Processing command (at Snapshots41.v1.bpl(4,1)) assert x < 20 || 10 <= x;

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots41.v1.bpl(6,8)) assert x < 10;

+  >>> RecycleError

+Processing command (at Snapshots41.v1.bpl(7,3)) assert 0 <= call0formal#AT#y;

+  >>> RecycleError

+Processing command (at Snapshots41.v1.bpl(8,3)) assert x == 7;

+  >>> DoNothingToAssert

+Snapshots41.v1.bpl(6,8): Error BP5001: This assertion might not hold.

+Snapshots41.v1.bpl(7,3): Error BP5002: A precondition for this call might not hold.

+Snapshots41.v1.bpl(13,10): Related location: This is the precondition that might not hold.

+Snapshots41.v1.bpl(8,3): Error BP5001: This assertion might not hold.

+Processing command (at Snapshots41.v1.bpl(27,5)) assert true;

+  >>> DoNothingToAssert

+Processing command (at Snapshots41.v1.bpl(21,3)) assert 2 <= z;

+  >>> DoNothingToAssert

+Snapshots41.v1.bpl(29,3): Error BP5003: A postcondition might not hold on this return path.

+Snapshots41.v1.bpl(21,3): Related location: This is the postcondition that might not hold.

+Processing command (at Snapshots41.v1.bpl(35,8)) assert u != 53;

+  >>> RecycleError

+Snapshots41.v1.bpl(35,8): Error BP5001: This assertion might not hold.

+

+Boogie program verifier finished with 2 verified, 5 errors