Made it produce more trace output for the verification result caching.

2 files changed, 53 insertions, 22 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index e0c3e006..76caa5d3 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1017,11 +1017,8 @@ namespace Microsoft.Boogie
         programCache.Set(programId, program, policy);

       }

 

-      if (0 <= CommandLineOptions.Clo.VerifySnapshots && CommandLineOptions.Clo.TraceCaching)

+      if (0 <= CommandLineOptions.Clo.VerifySnapshots && 2 <= CommandLineOptions.Clo.TraceCaching)

       {

-        Console.Out.WriteLine("");

-        Console.Out.WriteLine("<trace caching>");

-

         var end = DateTime.UtcNow;

         if (TimePerRequest.Count == 0)

         {

@@ -1030,20 +1027,37 @@ namespace Microsoft.Boogie
         TimePerRequest[requestId] = end.Subtract(start);

         StatisticsPerRequest[requestId] = stats;

 

-        Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(true));

+        var printTimes = 3 <= CommandLineOptions.Clo.TraceCaching;

+

+        Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(printTimes));

 

         Console.Out.WriteLine("Statistics per request as CSV:");

-        Console.Out.WriteLine("Request ID, Time (ms), Error, Inconclusive, Out of Memory, Timeout, Verified");

+        if (printTimes)

+        {

+          Console.Out.WriteLine("Request ID, Time (ms), Error, Inconclusive, Out of Memory, Timeout, Verified");

+        }

+        else

+        {

+          Console.Out.WriteLine("Request ID, Error, Inconclusive, Out of Memory, Timeout, Verified");

+        }

         foreach (var kv in TimePerRequest.OrderBy(kv => ExecutionEngine.AutoRequestId(kv.Key)))

         {

           var s = StatisticsPerRequest[kv.Key];

-          Console.Out.WriteLine("{0,-19}, {1,8:F0}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}", kv.Key, kv.Value.TotalMilliseconds, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount);

+          if (printTimes)

+          {

+            Console.Out.WriteLine("{0,-19}, {1,8:F0}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}", kv.Key, kv.Value.TotalMilliseconds, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount);

+          }

+          else

+          {

+            Console.Out.WriteLine("{0,-19}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}", kv.Key, kv.Value.TotalMilliseconds, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount);

+          }

         }

 

-        Console.Out.WriteLine("");

-        Console.Out.WriteLine("Total time (ms) since first request: {0:F0}", end.Subtract(FirstRequestStart).TotalMilliseconds);

-

-        Console.Out.WriteLine("</trace caching>");

+        if (printTimes)

+        {

+          Console.Out.WriteLine("");

+          Console.Out.WriteLine("Total time (ms) since first request: {0:F0}", end.Subtract(FirstRequestStart).TotalMilliseconds);

+        }

       }

 

       #endregion

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index ba995cba..268ab9bd 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Boogie
       var wr = new StringWriter();

       if (runs.Any())

       {

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

+        wr.WriteLine("\nCached verification result injector statistics as CSV:");

         if (printTime)

         {

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

@@ -269,7 +269,30 @@ namespace Microsoft.Boogie
           var assumed = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

           after.Add(assumed);

         }

+

         node.ExtendDesugaring(before, beforePrecondtionCheck, after);

+        if (1 <= CommandLineOptions.Clo.TraceCaching)

+        {

+          using (var tokTxtWr = new TokenTextWriter("<console>", Console.Out, false, false))

+          {

+            Console.Out.WriteLine("\nFor call to {0} in {1}:", node.Proc.Name, currentImplementation.Name);

+            foreach (var b in before)

+            {

+              Console.Out.Write("+ Added before: ");

+              b.Emit(tokTxtWr, 0);

+            }

+            foreach (var b in beforePrecondtionCheck)

+            {

+              Console.Out.Write("+ Added before precondition check: ");

+              b.Emit(tokTxtWr, 0);

+            }

+            foreach (var a in after)

+            {

+              Console.Out.Write("+ Added after: ");

+              a.Emit(tokTxtWr, 0);

+            }

+          }

+        }

       }

 

       return result;

@@ -295,12 +318,9 @@ namespace Microsoft.Boogie
       }

 

       var end = DateTime.UtcNow;

-      if (CommandLineOptions.Clo.TraceCaching)

+      if (3 <= CommandLineOptions.Clo.TraceCaching)

       {

-        Console.Out.WriteLine("");

-        Console.Out.WriteLine("<trace caching>");

-        Console.Out.WriteLine("Collected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

-        Console.Out.WriteLine("</trace caching>");

+        Console.Out.WriteLine("\nCollected other definition axioms within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

       }

     }

 

@@ -346,12 +366,9 @@ namespace Microsoft.Boogie
       dc.VisitProgram(program);

 

       var end = DateTime.UtcNow;

-      if (CommandLineOptions.Clo.TraceCaching)

+      if (3 <= CommandLineOptions.Clo.TraceCaching)

       {

-        Console.Out.WriteLine("");

-        Console.Out.WriteLine("<trace caching>");

-        Console.Out.WriteLine("Collected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

-        Console.Out.WriteLine("</trace caching>");

+        Console.Out.WriteLine("\nCollected dependencies within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

       }

     }