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

4 files changed, 129 insertions, 37 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index c49b3b3c..eca410b2 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -389,7 +389,7 @@ namespace Microsoft.Boogie {
     public bool Trace = false;

     public bool TraceTimes = false;

     public bool TraceProofObligations = false;

-    public bool TraceCaching = false;

+    public int TraceCaching = 0;

     public bool NoResolve = false;

     public bool NoTypecheck = false;

     public bool OverlookBoogieTypeErrors = false;

@@ -1325,6 +1325,10 @@ namespace Microsoft.Boogie {
         case "verifySnapshots":

           ps.GetNumericArgument(ref VerifySnapshots, 3);

           return true;

+

+        case "traceCaching":

+          ps.GetNumericArgument(ref TraceCaching, 4);

+          return true;

 		

 		case "useSmtOutputFormat": {

 		  if (ps.ConfirmArgumentCount(0)) {

@@ -1393,7 +1397,6 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("wait", ref Wait) ||

               ps.CheckBooleanFlag("trace", ref Trace) ||

               ps.CheckBooleanFlag("traceTimes", ref TraceTimes) ||

-              ps.CheckBooleanFlag("traceCaching", ref TraceCaching) ||

               ps.CheckBooleanFlag("tracePOs", ref TraceProofObligations) ||

               ps.CheckBooleanFlag("noResolve", ref NoResolve) ||

               ps.CheckBooleanFlag("noTypecheck", ref NoTypecheck) ||

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

       }

     }

 

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 7fb12589..6fa26967 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1336,12 +1336,24 @@ namespace VC {
       Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);

       

       var end = DateTime.UtcNow;

-      if (CommandLineOptions.Clo.TraceCaching)

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

       {

-        Console.Out.WriteLine("");

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

-        Console.Out.WriteLine("Turned implementation into passive commands within {0:F0} ms.", end.Subtract(start).TotalMilliseconds);

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

+        Console.Out.WriteLine("\nTurned implementation into passive commands within {0:F0} ms.\n", end.Subtract(start).TotalMilliseconds);

+

+      }

+

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

+      {

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

+        {

+          var pd = CommandLineOptions.Clo.PrintDesugarings;

+          var pu = CommandLineOptions.Clo.PrintUnstructured;

+          CommandLineOptions.Clo.PrintDesugarings = true;

+          CommandLineOptions.Clo.PrintUnstructured = 1;

+          impl.Emit(tokTxtWr, 0);

+          CommandLineOptions.Clo.PrintDesugarings = pd;

+          CommandLineOptions.Clo.PrintUnstructured = pu;

+        }

       }

 

       currentTemporaryVariableForAssertions = null;

@@ -1458,6 +1470,27 @@ namespace VC {
       return Substituter.SubstitutionFromHashtable(oldFrameMap);

     }

 

+    void TraceCachingTransformation(Cmd from, string message, Cmd to = null)

+    {

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

+      {

+        Console.WriteLine("");

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

+        {

+          from.Emit(tokTxtWr, 0);

+          Console.Write(message);

+          if (to != null)

+          {

+            to.Emit(tokTxtWr, 0);

+          }

+          else

+          {

+            Console.WriteLine("");

+          }

+        }

+      }

+    }

+

     /// <summary>

     /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc

     /// Meanwhile, record any information needed to later reconstruct a model view.

@@ -1504,9 +1537,13 @@ namespace VC {
               && currentImplementation.HasCachedSnapshot

               && !currentImplementation.AnyErrorsInCachedSnapshot

               && currentImplementation.InjectedAssumptionVariables.Count == 1)

-          { }

+          {

+            TraceCachingTransformation(pc, "==> did nothing\n");

+          }

           else if (relevantDoomedAssumpVars.Any())

-          { }

+          {

+            TraceCachingTransformation(pc, "==> did nothing\n");

+          }

           else if (currentImplementation != null

                    && currentImplementation.HasCachedSnapshot

                    && checksum != null

@@ -1524,15 +1561,19 @@ namespace VC {
               ac.IncarnationMap[incarnation] = identExpr;

               passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));

               copy = identExpr;

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

+              var a = new AssumeCmd(Token.NoToken, LiteralExpr.Imp(assmVars, identExpr));

+              passiveCmds.Add(a);

+              TraceCachingTransformation(pc, "== marked as partially verified ==> ", a);

             }

             else if (isTrue)

             {

               if (alwaysUseSubsumption)

               {

                 // Turn it into an assume statement.

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

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

+                var a = new AssumeCmd(ac.tok, copy);

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

+                TraceCachingTransformation(pc, "== marked as fully verified ==> ", a);

+                pc = a;

               }

               dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;

             }

@@ -1547,8 +1588,10 @@ namespace VC {
             if (alwaysUseSubsumption)

             {

               // Turn it into an assume statement.

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

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

+              var a = new AssumeCmd(ac.tok, copy);

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

+              TraceCachingTransformation(pc, "== recycled error ==> ", a);

+              pc = a;

             }

             dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;

             if (dropCmd || alwaysUseSubsumption)

@@ -1556,6 +1599,10 @@ namespace VC {
               currentImplementation.AddRecycledFailingAssertion(ac);

             }

           }

+          else

+          {

+            TraceCachingTransformation(pc, "==> did nothing\n");

+          }

         }

         else if (pc is AssumeCmd

                  && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot")

@@ -1571,6 +1618,11 @@ namespace VC {
             if (!isTrue)

             {

               copy = LiteralExpr.Imp(assmVars, copy);

+              TraceCachingTransformation(pc, "==> marked as partially verified\n");

+            }

+            else

+            {

+              TraceCachingTransformation(pc, "==> marked as full verified\n");

             }

           }

           else

@@ -1583,6 +1635,10 @@ namespace VC {
         {

           passiveCmds.Add(pc);

         }

+        else

+        {

+          TraceCachingTransformation(pc, "==> dropped\n");

+        }

       }

       #endregion

       #region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below]

@@ -1664,7 +1720,9 @@ namespace VC {
           Expr incarnation;

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

           {

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

+            var a = new AssumeCmd(c.tok, Expr.Not(incarnation));

+            TraceCachingTransformation(assign, "== assumed negation of single assumption variable ==> ", a);

+            passiveCmds.Add(a);

           }

         }

       }