From ee75fd2e508d3da48923888833f63ae96ad9b408 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 13 Oct 2014 16:04:14 +0200
Subject: Add '/traceCaching' flag.

---
 Source/ExecutionEngine/ExecutionEngine.cs | 38 +++++++++++++++++++++++++++----
 1 file changed, 33 insertions(+), 5 deletions(-)

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

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index b5f4f87b..44b8719a 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -417,6 +417,10 @@ namespace Microsoft.Boogie
     
     static List<Checker> Checkers = new List<Checker>();
 
+    static DateTime FirstRequestStart;
+
+    static readonly ConcurrentDictionary<string, TimeSpan> TimePerRequest = new ConcurrentDictionary<string, TimeSpan>();
+
     static readonly ConcurrentDictionary<string, CancellationTokenSource> ImplIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
 
     static readonly ConcurrentDictionary<string, CancellationTokenSource> RequestIdToCancellationTokenSource = new ConcurrentDictionary<string, CancellationTokenSource>();
@@ -810,6 +814,8 @@ namespace Microsoft.Boogie
         requestId = FreshRequestId();
       }
 
+      var start = DateTime.UtcNow;
+
       #region Do some pre-abstract-interpretation preprocessing on the program
       // Doing lambda expansion before abstract interpretation means that the abstract interpreter
       // never needs to see any lambda expressions.  (On the other hand, if it were useful for it
@@ -993,6 +999,33 @@ namespace Microsoft.Boogie
       {
         program.FreezeTopLevelDeclarations();
         programCache.Set(programId, program, policy);
+
+        if (CommandLineOptions.Clo.TraceCaching)
+        {
+          Console.Out.WriteLine("");
+          Console.Out.WriteLine("<trace caching>");
+
+          var end = DateTime.UtcNow;
+          if (TimePerRequest.Count == 0)
+          {
+            FirstRequestStart = start;
+          }
+          TimePerRequest[requestId] = end.Subtract(start);
+
+          Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(true));
+
+          Console.Out.WriteLine("Times per request as CSV:");
+          Console.Out.WriteLine("Request ID, Time (ms)");
+          foreach (var kv in TimePerRequest.OrderBy(kv => kv.Key))
+          {
+            Console.Out.WriteLine("{0}, {1:F0}", kv.Key, kv.Value.TotalMilliseconds);
+          }
+
+          Console.Out.WriteLine("");
+          Console.Out.WriteLine("Total time (ms) since first request: {0:F0}", end.Subtract(FirstRequestStart).TotalMilliseconds);
+
+          Console.Out.WriteLine("</trace caching>");
+        }
       }
 
       #endregion
@@ -1394,11 +1427,6 @@ 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);
     }
 
-- 
cgit v1.2.3