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 ++++++++++++++++++++---
 1 file changed, 20 insertions(+), 3 deletions(-)

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

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);
     }
 
-- 
cgit v1.2.3