Add '/traceCaching' flag.

2 files changed, 35 insertions, 8 deletions

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);

     }

 

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 67d6dde5..215731b0 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -37,7 +37,6 @@ namespace Microsoft.Boogie
     public string Output(bool printTime = false)

     {

       var wr = new StringWriter();

-      wr.WriteLine("");

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

       if (printTime)

       {

@@ -47,11 +46,11 @@ namespace Microsoft.Boogie
       {

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

       }

-      foreach (var kv in runs)

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

       {

         if (printTime)

         {

-          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);

+          wr.WriteLine("{0}, {1:F0}, {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

         {