From cb4d41266301c26b9c863561df57ffd30ae0ec6f Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Sat, 18 Oct 2014 00:10:25 +0200
Subject: Made it produce more trace output for the verification result
 caching.

---
 Source/VCGeneration/ConditionGeneration.cs | 84 +++++++++++++++++++++++++-----
 1 file changed, 71 insertions(+), 13 deletions(-)

(limited to 'Source/VCGeneration')

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