From 2d1dbccf67a424e609501975b6d8602c90ac48cc Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 30 Jun 2014 19:33:11 +0200
Subject: Made it collect some statistics about the more advanced verification
 result caching.

---
 Source/ExecutionEngine/ExecutionEngine.cs         | 23 ++++++++--
 Source/ExecutionEngine/VerificationResultCache.cs | 55 ++++++++++++++++++++++-
 2 files changed, 74 insertions(+), 4 deletions(-)

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 5e1d75ed..2af65733 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -394,6 +394,14 @@ namespace Microsoft.Boogie
 
     public static ErrorInformationFactory errorInformationFactory = new ErrorInformationFactory();
 
+    static int autoRequestIdCount;
+
+    public static string FreshRequestId()
+    {
+      var id = Interlocked.Increment(ref autoRequestIdCount);
+      return string.Format("auto_request_id_{0}", id);
+    }
+
     public readonly static VerificationResultCache Cache = new VerificationResultCache();
 
     static readonly MemoryCache programCache = new MemoryCache("ProgramCache");
@@ -778,13 +786,17 @@ namespace Microsoft.Boogie
     public static PipelineOutcome InferAndVerify(Program program,
                                                  PipelineStatistics stats,
                                                  string programId = null,
-                                                 ErrorReporterDelegate er = null, string requestId = "unknown")
+                                                 ErrorReporterDelegate er = null, string requestId = null)
     {
       Contract.Requires(program != null);
       Contract.Requires(stats != null);
-      Contract.Requires(requestId != null);
       Contract.Ensures(0 <= Contract.ValueAtReturn(out stats.InconclusiveCount) && 0 <= Contract.ValueAtReturn(out stats.TimeoutCount));
 
+      if (requestId == null)
+      {
+        requestId = FreshRequestId();
+      }
+
       RequestIdToCancellationTokenSources[requestId] = new List<CancellationTokenSource>();
 
       #region Do some pre-abstract-interpretation preprocessing on the program
@@ -865,7 +877,7 @@ namespace Microsoft.Boogie
 
       if (1 < CommandLineOptions.Clo.VerifySnapshots)
       {
-        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls);
+        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId);
       }
 
       #region Verify each implementation
@@ -1343,6 +1355,11 @@ namespace Microsoft.Boogie
 
       printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);
 
+      if (1 < CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.Trace)
+      {
+        printer.Inform(CachedVerificationResultInjector.Statistics.Output(CommandLineOptions.Clo.TraceTimes), tw);
+      }
+
       ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit);
     }
 
diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 39d5071d..8eada755 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -2,6 +2,7 @@
 using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.IO;
 using System.Linq;
 using System.Runtime.Caching;
 using System.Text;
@@ -11,6 +12,52 @@ using VC;
 namespace Microsoft.Boogie
 {
 
+  struct CachedVerificationResultInjectorRun
+  {
+    public DateTime Start { get; internal set; }
+    public DateTime End { get; internal set; }
+    public int ImplementationCount { get; internal set; }
+  }
+
+
+  class CachedVerificationResultInjectorStatistics
+  {
+    ConcurrentDictionary<string, CachedVerificationResultInjectorRun> runs = new ConcurrentDictionary<string, CachedVerificationResultInjectorRun>();
+
+    public bool AddRun(string requestId, CachedVerificationResultInjectorRun run)
+    {
+      return runs.TryAdd(requestId, run);
+    }
+
+    public string Output(bool printTime = false)
+    {
+      var wr = new StringWriter();
+      wr.WriteLine("");
+      wr.WriteLine("Cached verification result injector statistics:");
+      if (printTime)
+      {
+        wr.WriteLine("Request ID, Time, Implementations (ms)");
+      }
+      else
+      {
+        wr.WriteLine("Request ID, Implementations (ms)");
+      }
+      foreach (var kv in runs)
+      {
+        if (printTime)
+        {
+          wr.WriteLine("{0}, {1}, {2}", kv.Key, kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds, kv.Value.ImplementationCount);
+        }
+        else
+        {
+          wr.WriteLine("{0}, {1}", kv.Key, kv.Value.ImplementationCount);
+        }
+      }
+      return wr.ToString();
+    }
+  }
+
+
   class CachedVerificationResultInjector : StandardVisitor
   {
     readonly IEnumerable<Implementation> Implementations;
@@ -22,6 +69,8 @@ namespace Microsoft.Boogie
     int assumptionVariableCount;
     int temporaryVariableCount;
 
+    public static readonly CachedVerificationResultInjectorStatistics Statistics = new CachedVerificationResultInjectorStatistics();
+
     int FreshAssumptionVariableName
     {
       get
@@ -58,10 +107,11 @@ namespace Microsoft.Boogie
       return result;
     }
 
-    public static void Inject(Program program, IEnumerable<Implementation> implementations)
+    public static void Inject(Program program, IEnumerable<Implementation> implementations, string requestId)
     {
       var eai = new CachedVerificationResultInjector(program, implementations);
 
+      var run = new CachedVerificationResultInjectorRun { Start = DateTime.UtcNow };
       foreach (var impl in implementations)
       {
         int priority;
@@ -84,11 +134,14 @@ namespace Microsoft.Boogie
               if (p != null)
               {
                 eai.Inject(impl, p);
+                run.ImplementationCount++;
               }
             }
           }
         }
       }
+      run.End = DateTime.UtcNow;
+      Statistics.AddRun(requestId, run);
     }
 
     public override Cmd VisitCallCmd(CallCmd node)
-- 
cgit v1.2.3