From 454f7ff730ca2b17e6b9c705d36f071d66d9ef45 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 4 Jul 2014 05:15:38 +0200
Subject: Made it collect more statistics about the more advanced verification
 result caching.

---
 Source/ExecutionEngine/VerificationResultCache.cs | 60 +++++++++++++++--------
 1 file changed, 40 insertions(+), 20 deletions(-)

(limited to 'Source/ExecutionEngine/VerificationResultCache.cs')

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 5c3324cc..58423f24 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -18,6 +18,10 @@ namespace Microsoft.Boogie
     public DateTime End { get; internal set; }
     public int RewrittenImplementationCount { 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; }
   }
 
 
@@ -37,21 +41,21 @@ namespace Microsoft.Boogie
       wr.WriteLine("Cached verification result injector statistics as CSV:");
       if (printTime)
       {
-        wr.WriteLine("Request ID, Time (ms), Rewritten Implementations, Implementations");
+        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, Implementations");
+        wr.WriteLine("Request ID, Rewritten Implementations, Low Priority Implementations, Medium Priority Implementations, High Priority Implementations, Skipped Implementations, Implementations");
       }
       foreach (var kv in runs)
       {
         if (printTime)
         {
-          wr.WriteLine("{0}, {1}, {2}, {3}", kv.Key, kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds, kv.Value.RewrittenImplementationCount, kv.Value.ImplementationCount);
+          wr.WriteLine("{0}, {1}, {2}, {3}, {4}, {5}, {6}, {7}", 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}, {1}, {2}", kv.Key, kv.Value.RewrittenImplementationCount, kv.Value.ImplementationCount);
+          wr.WriteLine("{0}, {1}, {2}, {3}, {4}, {5}, {6}", kv.Key, kv.Value.RewrittenImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, kv.Value.ImplementationCount);
         }
       }
       return wr.ToString();
@@ -117,28 +121,44 @@ namespace Microsoft.Boogie
       {
         int priority;
         var vr = ExecutionEngine.Cache.Lookup(impl, out priority);
-        if (vr != null && priority == Priority.LOW)
+        if (vr != null)
         {
-          if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
+          if (priority == Priority.LOW)
           {
-            if (vr.Errors != null)
+            run.LowPriorityImplementationCount++;
+            if (TimeThreshold < vr.End.Subtract(vr.Start).TotalMilliseconds)
             {
-              impl.ErrorsInCachedSnapshot = vr.Errors.ToList<object>();
-            }
-            else if (vr.Outcome == ConditionGeneration.Outcome.Correct)
-            {
-              impl.ErrorsInCachedSnapshot = new List<object>();
-            }
-            if (vr.ProgramId != null)
-            {
-              var p = ExecutionEngine.CachedProgram(vr.ProgramId);
-              if (p != null)
+              if (vr.Errors != null)
+              {
+                impl.ErrorsInCachedSnapshot = vr.Errors.ToList<object>();
+              }
+              else if (vr.Outcome == ConditionGeneration.Outcome.Correct)
+              {
+                impl.ErrorsInCachedSnapshot = new List<object>();
+              }
+              if (vr.ProgramId != null)
               {
-                eai.Inject(impl, p);
-                run.RewrittenImplementationCount++;
+                var p = ExecutionEngine.CachedProgram(vr.ProgramId);
+                if (p != null)
+                {
+                  eai.Inject(impl, p);
+                  run.RewrittenImplementationCount++;
+                }
               }
             }
           }
+          else if (priority == Priority.MEDIUM)
+          {
+            run.MediumPriorityImplementationCount++;
+          }
+          else if (priority == Priority.HIGH)
+          {
+            run.HighPriorityImplementationCount++;
+          }
+          else if (priority == Priority.SKIP)
+          {
+            run.SkippedImplementationCount++;
+          }
         }
       }
       run.End = DateTime.UtcNow;
@@ -403,7 +423,7 @@ namespace Microsoft.Boogie
   public class VerificationResultCache
   {
     private readonly MemoryCache Cache = new MemoryCache("VerificationResultCache");
-    private readonly CacheItemPolicy Policy = new CacheItemPolicy { SlidingExpiration = new TimeSpan(0, 10, 0) };
+    private readonly CacheItemPolicy Policy = new CacheItemPolicy { SlidingExpiration = new TimeSpan(0, 10, 0), Priority = CacheItemPriority.Default };
 
 
     public void Insert(Implementation impl, VerificationResult result)
-- 
cgit v1.2.3