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

4 files changed, 73 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,