Made it produce more trace output for the verification result caching.

2 files changed, 17 insertions, 38 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 0c027f5c..eb871ac3 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -196,6 +196,7 @@ namespace Microsoft.Boogie
     public int InconclusiveCount;

     public int TimeoutCount;

     public int OutOfMemoryCount;

+    public long[] CachingActionCounts;

   }

 

 

@@ -914,7 +915,7 @@ namespace Microsoft.Boogie
 

       if (1 < CommandLineOptions.Clo.VerifySnapshots)

       {

-        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId, programId);

+        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId, programId, out stats.CachingActionCounts);

       }

 

       #region Verify each implementation

@@ -1035,25 +1036,13 @@ namespace Microsoft.Boogie
         Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(printTimes));

 

         Console.Out.WriteLine("Statistics per request as CSV:");

-        if (printTimes)

-        {

-          Console.Out.WriteLine("Request ID, Time (ms), Error, Inconclusive, Out of Memory, Timeout, Verified");

-        }

-        else

-        {

-          Console.Out.WriteLine("Request ID, Error, Inconclusive, Out of Memory, Timeout, Verified");

-        }

+        Console.Out.WriteLine("Request ID{0}, Error, Inconclusive, Out of Memory, Timeout, Verified, DoNothing, MarkAsPartiallyVerified, MarkAsFullyVerified, RecycleError, AssumeNegationOfAssumptionVariable, Drop", printTimes ? ", Time (ms)" : "");

         foreach (var kv in TimePerRequest.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key)))

         {

           var s = StatisticsPerRequest[kv.Key];

-          if (printTimes)

-          {

-            Console.Out.WriteLine("{0,-19}, {1,8:F0}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}", kv.Key, kv.Value.TotalMilliseconds, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount);

-          }

-          else

-          {

-            Console.Out.WriteLine("{0,-19}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}", kv.Key, kv.Value.TotalMilliseconds, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount);

-          }

+          var cacs = s.CachingActionCounts;

+          var t = printTimes ? string.Format(", {0,8:F0}", kv.Value.TotalMilliseconds) : "";

+          Console.Out.WriteLine("{0,-19}{1}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}, {7,3}, {8,3}, {9,3}, {10,3}, {11,3}, {12,3}", kv.Key, t, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount, cacs[0], cacs[1], cacs[2], cacs[3], cacs[4], cacs[5]);

         }

 

         if (printTimes)

@@ -1138,6 +1127,7 @@ namespace Microsoft.Boogie
 

         using (var vcgen = CreateVCGen(program, checkers))

         {

+          vcgen.CachingActionCounts = stats.CachingActionCounts;

           verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;

           verificationResult.Start = DateTime.UtcNow;

 

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 091ccc25..c75bd52f 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -16,12 +16,13 @@ namespace Microsoft.Boogie
   {

     public DateTime Start { get; internal set; }

     public DateTime End { get; internal set; }

-    public int RewrittenImplementationCount { get; internal set; }

+    public int TransformedImplementationCount { get; internal set; }

     public int ImplementationCount { get; internal set; }

     public int SkippedImplementationCount { get; set; }

     public int LowPriorityImplementationCount { get; set; }

     public int MediumPriorityImplementationCount { get; set; }

     public int HighPriorityImplementationCount { get; set; }

+    public long[] CachingActionCounts { get; set; }

   }

 

 

@@ -40,24 +41,11 @@ namespace Microsoft.Boogie
       if (runs.Any())

       {

         wr.WriteLine("Cached verification result injector statistics as CSV:");

-        if (printTime)

-        {

-          wr.WriteLine("Request ID, Time (ms), Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations");

-        }

-        else

-        {

-          wr.WriteLine("Request ID, Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations");

-        }

+        wr.WriteLine("Request ID, Transformed, Low, Medium, High, Skipped{0}", printTime ? ", Time (ms)" : "");

         foreach (var kv in runs.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key)))

         {

-          if (printTime)

-          {

-            wr.WriteLine("{0,-19}, {1,5:F0}, {2,3}, {3,3}, {4,3}, {5,3}, {6,3}, {7,3}", kv.Key, kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds, kv.Value.RewrittenImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, kv.Value.ImplementationCount);

-          }

-          else

-          {

-            wr.WriteLine("{0,-19}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}, {6,3}", kv.Key, kv.Value.RewrittenImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, kv.Value.ImplementationCount);

-          }

+          var t = printTime ? string.Format(", {0,8:F0}", kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds) : "";

+          wr.WriteLine("{0,-19}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}{6}", kv.Key, kv.Value.TransformedImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, t);

         }

       }

       return wr.ToString();

@@ -114,11 +102,12 @@ namespace Microsoft.Boogie
       return result;

     }

 

-    public static void Inject(Program program, IEnumerable<Implementation> implementations, string requestId, string programId)

+    public static void Inject(Program program, IEnumerable<Implementation> implementations, string requestId, string programId, out long[] cachingActionCounts)

     {

       var eai = new CachedVerificationResultInjector(program, implementations);

 

-      var run = new CachedVerificationResultInjectorRun { Start = DateTime.UtcNow, ImplementationCount = implementations.Count() };

+      cachingActionCounts = new long[Enum.GetNames(typeof(VC.ConditionGeneration.CachingAction)).Length];

+      var run = new CachedVerificationResultInjectorRun { Start = DateTime.UtcNow, ImplementationCount = implementations.Count(), CachingActionCounts = cachingActionCounts };

       foreach (var impl in implementations)

       {

         int priority;

@@ -137,7 +126,7 @@ namespace Microsoft.Boogie
                 if (p != null)

                 {

                   eai.Inject(impl, p);

-                  run.RewrittenImplementationCount++;

+                  run.TransformedImplementationCount++;

                 }

               }

             }

@@ -154,7 +143,7 @@ namespace Microsoft.Boogie
                 if (p != null)

                 {

                   eai.Inject(impl, p);

-                  run.RewrittenImplementationCount++;

+                  run.TransformedImplementationCount++;

                 }

               }

             }