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

1 files changed, 71 insertions, 13 deletions

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

           }

         }

       }