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

4 files changed, 35 insertions, 53 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 2bacc19f..a78cb71b 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -965,7 +965,6 @@ namespace Microsoft.Boogie {
         var havocCmd = cmd as HavocCmd;

         if (havocCmd != null)

         {

-          // TODO(wuestholz): Check with Rustan if this makes sense.

           tokTxtWr.Write("havoc ");

           var relevantVars = havocCmd.Vars.Where(v => usedVariables.Contains(v.Decl) && !v.Decl.Name.StartsWith("a##post##")).ToList();

           relevantVars.Emit(tokTxtWr, true);

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 0c027f5c..eb871ac3 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -196,6 +196,7 @@ namespace Microsoft.Boogie
     public int InconclusiveCount;

     public int TimeoutCount;

     public int OutOfMemoryCount;

+    public long[] CachingActionCounts;

   }

 

 

@@ -914,7 +915,7 @@ namespace Microsoft.Boogie
 

       if (1 < CommandLineOptions.Clo.VerifySnapshots)

       {

-        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId, programId);

+        CachedVerificationResultInjector.Inject(program, stablePrioritizedImpls, requestId, programId, out stats.CachingActionCounts);

       }

 

       #region Verify each implementation

@@ -1035,25 +1036,13 @@ namespace Microsoft.Boogie
         Console.Out.WriteLine(CachedVerificationResultInjector.Statistics.Output(printTimes));

 

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

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

-        }

+        Console.Out.WriteLine("Request ID{0}, Error, Inconclusive, Out of Memory, Timeout, Verified, DoNothing, MarkAsPartiallyVerified, MarkAsFullyVerified, RecycleError, AssumeNegationOfAssumptionVariable, Drop", printTimes ? ", Time (ms)" : "");

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

         {

           var s = StatisticsPerRequest[kv.Key];

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

-          }

+          var cacs = s.CachingActionCounts;

+          var t = printTimes ? string.Format(", {0,8:F0}", kv.Value.TotalMilliseconds) : "";

+          Console.Out.WriteLine("{0,-19}{1}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}, {7,3}, {8,3}, {9,3}, {10,3}, {11,3}, {12,3}", kv.Key, t, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount, cacs[0], cacs[1], cacs[2], cacs[3], cacs[4], cacs[5]);

         }

 

         if (printTimes)

@@ -1138,6 +1127,7 @@ namespace Microsoft.Boogie
 

         using (var vcgen = CreateVCGen(program, checkers))

         {

+          vcgen.CachingActionCounts = stats.CachingActionCounts;

           verificationResult.ProofObligationCountBefore = vcgen.CumulativeAssertionCount;

           verificationResult.Start = DateTime.UtcNow;

 

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index 091ccc25..c75bd52f 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -16,12 +16,13 @@ namespace Microsoft.Boogie
   {

     public DateTime Start { get; internal set; }

     public DateTime End { get; internal set; }

-    public int RewrittenImplementationCount { get; internal set; }

+    public int TransformedImplementationCount { get; internal set; }

     public int ImplementationCount { get; internal set; }

     public int SkippedImplementationCount { get; set; }

     public int LowPriorityImplementationCount { get; set; }

     public int MediumPriorityImplementationCount { get; set; }

     public int HighPriorityImplementationCount { get; set; }

+    public long[] CachingActionCounts { get; set; }

   }

 

 

@@ -40,24 +41,11 @@ namespace Microsoft.Boogie
       if (runs.Any())

       {

         wr.WriteLine("Cached 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");

-        }

-        else

-        {

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

-        }

+        wr.WriteLine("Request ID, Transformed, Low, Medium, High, Skipped{0}", printTime ? ", Time (ms)" : "");

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

         {

-          if (printTime)

-          {

-            wr.WriteLine("{0,-19}, {1,5:F0}, {2,3}, {3,3}, {4,3}, {5,3}, {6,3}, {7,3}", 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

-          {

-            wr.WriteLine("{0,-19}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}, {6,3}", kv.Key, kv.Value.RewrittenImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, kv.Value.ImplementationCount);

-          }

+          var t = printTime ? string.Format(", {0,8:F0}", kv.Value.End.Subtract(kv.Value.Start).TotalMilliseconds) : "";

+          wr.WriteLine("{0,-19}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}{6}", kv.Key, kv.Value.TransformedImplementationCount, kv.Value.LowPriorityImplementationCount, kv.Value.MediumPriorityImplementationCount, kv.Value.HighPriorityImplementationCount, kv.Value.SkippedImplementationCount, t);

         }

       }

       return wr.ToString();

@@ -114,11 +102,12 @@ namespace Microsoft.Boogie
       return result;

     }

 

-    public static void Inject(Program program, IEnumerable<Implementation> implementations, string requestId, string programId)

+    public static void Inject(Program program, IEnumerable<Implementation> implementations, string requestId, string programId, out long[] cachingActionCounts)

     {

       var eai = new CachedVerificationResultInjector(program, implementations);

 

-      var run = new CachedVerificationResultInjectorRun { Start = DateTime.UtcNow, ImplementationCount = implementations.Count() };

+      cachingActionCounts = new long[Enum.GetNames(typeof(VC.ConditionGeneration.CachingAction)).Length];

+      var run = new CachedVerificationResultInjectorRun { Start = DateTime.UtcNow, ImplementationCount = implementations.Count(), CachingActionCounts = cachingActionCounts };

       foreach (var impl in implementations)

       {

         int priority;

@@ -137,7 +126,7 @@ namespace Microsoft.Boogie
                 if (p != null)

                 {

                   eai.Inject(impl, p);

-                  run.RewrittenImplementationCount++;

+                  run.TransformedImplementationCount++;

                 }

               }

             }

@@ -154,7 +143,7 @@ namespace Microsoft.Boogie
                 if (p != null)

                 {

                   eai.Inject(impl, p);

-                  run.RewrittenImplementationCount++;

+                  run.TransformedImplementationCount++;

                 }

               }

             }

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 78c36fbe..4a85005e 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1308,6 +1308,7 @@ namespace VC {
       List<Cmd> passiveCmds = new List<Cmd>();

       foreach (Cmd c in b.Cmds) {

         Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction

+        // TODO(wuestholz): Maybe we should use multiple variable collectors.

         ChecksumHelper.ComputeChecksums(c, currentImplementation, variableCollector.usedVars, currentChecksum);

         variableCollector.Visit(c);

         currentChecksum = c.Checksum;

@@ -1472,17 +1473,19 @@ namespace VC {
       return Substituter.SubstitutionFromHashtable(oldFrameMap);

     }

 

-    enum CachingAction

+    public enum CachingAction : byte

     {

       DoNothing,

       MarkAsPartiallyVerified,

       MarkAsFullyVerified,

-      Drop,

       RecycleError,

-      AssumeNegationOfAssumptionVariable

+      AssumeNegationOfAssumptionVariable,

+      Drop,

     }

 

-    void TraceCaching(Cmd cmd, CachingAction action)

+    public long[] CachingActionCounts;

+

+    void TraceCachingAction(Cmd cmd, CachingAction action)

     {

       if (1 <= CommandLineOptions.Clo.TraceCaching)

       {

@@ -1493,6 +1496,7 @@ namespace VC {
           cmd.Emit(tokTxtWr, 0);

           Console.Out.WriteLine("  >>> {0}", action);

         }

+        Interlocked.Increment(ref CachingActionCounts[(int)action]);

       }

     }

 

@@ -1543,11 +1547,11 @@ namespace VC {
               && !currentImplementation.AnyErrorsInCachedSnapshot

               && currentImplementation.InjectedAssumptionVariables.Count == 1)

           {

-            TraceCaching(pc, CachingAction.DoNothing);

+            TraceCachingAction(pc, CachingAction.DoNothing);

           }

           else if (relevantDoomedAssumpVars.Any())

           {

-            TraceCaching(pc, CachingAction.DoNothing);

+            TraceCachingAction(pc, CachingAction.DoNothing);

           }

           else if (currentImplementation != null

                    && currentImplementation.HasCachedSnapshot

@@ -1567,14 +1571,14 @@ namespace VC {
               passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));

               copy = identExpr;

               passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr)));

-              TraceCaching(pc, CachingAction.MarkAsPartiallyVerified);

+              TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);

             }

             else if (isTrue)

             {

               if (alwaysUseSubsumption)

               {

                 // Turn it into an assume statement.

-                TraceCaching(pc, CachingAction.MarkAsFullyVerified);

+                TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);

                 pc = new AssumeCmd(ac.tok, copy);

                 pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);

               }

@@ -1591,7 +1595,7 @@ namespace VC {
             if (alwaysUseSubsumption)

             {

               // Turn it into an assume statement.

-              TraceCaching(pc, CachingAction.RecycleError);

+              TraceCachingAction(pc, CachingAction.RecycleError);

               pc = new AssumeCmd(ac.tok, copy);

               pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);

             }

@@ -1603,7 +1607,7 @@ namespace VC {
           }

           else

           {

-            TraceCaching(pc, CachingAction.DoNothing);

+            TraceCachingAction(pc, CachingAction.DoNothing);

           }

         }

         else if (pc is AssumeCmd

@@ -1620,11 +1624,11 @@ namespace VC {
             if (!isTrue)

             {

               copy = LiteralExpr.Imp(assmVars, copy);

-              TraceCaching(pc, CachingAction.MarkAsPartiallyVerified);

+              TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);

             }

             else

             {

-              TraceCaching(pc, CachingAction.MarkAsFullyVerified);

+              TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);

             }

           }

           else

@@ -1639,7 +1643,7 @@ namespace VC {
         }

         else

         {

-          TraceCaching(pc, CachingAction.Drop);

+          TraceCachingAction(pc, CachingAction.Drop);

         }

       }

       #endregion

@@ -1722,7 +1726,7 @@ namespace VC {
           Expr incarnation;

           if (identExpr != null && identExpr.Decl != null && QKeyValue.FindBoolAttribute(identExpr.Decl.Attributes, "assumption") && incarnationMap.TryGetValue(identExpr.Decl, out incarnation))

           {

-            TraceCaching(assign, CachingAction.AssumeNegationOfAssumptionVariable);

+            TraceCachingAction(assign, CachingAction.AssumeNegationOfAssumptionVariable);

             passiveCmds.Add(new AssumeCmd(c.tok, Expr.Not(incarnation)));

           }

         }