Made it collect some statistics about the more advanced verification result caching.

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)