From 75542ea0ee9f14ef18eee6e3349747a8f7181b51 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 10 Nov 2014 10:48:12 +0100
Subject: Worked on the verification result caching.

---
 Source/VCGeneration/ConditionGeneration.cs | 70 +++++++++++++++++++++---------
 1 file changed, 50 insertions(+), 20 deletions(-)

(limited to 'Source/VCGeneration')

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 09887f4a..640b0db2 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1484,8 +1484,7 @@ namespace VC {
       MarkAsFullyVerified,
       RecycleError,
       AssumeNegationOfAssumptionVariable,
-      DropAssume,
-      DropAssert
+      DropAssume
     }
 
     public long[] CachingActionCounts;
@@ -1572,26 +1571,54 @@ namespace VC {
               var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);
               if (!isTrue && alwaysUseSubsumption)
               {
-                // Bind the assertion expression to a local variable.
-                var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);
-                var identExpr = new IdentifierExpr(Token.NoToken, incarnation);
-                incarnationMap[incarnation] = identExpr;
-                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)));
                 TraceCachingAction(pc, CachingAction.MarkAsPartiallyVerified);
+                var litExpr = ac.Expr as LiteralExpr;
+                if (litExpr == null || !litExpr.IsTrue)
+                {
+                  // Bind the assertion expression to a local variable.
+                  var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);
+                  var identExpr = new IdentifierExpr(Token.NoToken, incarnation);
+                  incarnationMap[incarnation] = identExpr;
+                  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)));
+                }
+                else
+                {
+                  dropCmd = true;
+                }
               }
               else if (isTrue)
               {
                 if (alwaysUseSubsumption)
                 {
-                  // Turn it into an assume statement.
                   TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);
-                  pc = new AssumeCmd(ac.tok, copy);
-                  pc.Attributes = new QKeyValue(Token.NoToken, "verified_assertion", new List<object>(), pc.Attributes);
+                  var litExpr = ac.Expr as LiteralExpr;
+                  if (litExpr == null || !litExpr.IsTrue)
+                  {
+                    // 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);
+                  }
+                  else
+                  {
+                    dropCmd = true;
+                  }
+                }
+                else if (subsumption == CommandLineOptions.SubsumptionOption.Never)
+                {
+                  TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);
+                  dropCmd = true;
+                }
+                else
+                {
+                  TraceCachingAction(pc, CachingAction.DoNothingToAssert);
                 }
-                dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;
+              }
+              else
+              {
+                TraceCachingAction(pc, CachingAction.DoNothingToAssert);
               }
             }
           }
@@ -1608,12 +1635,18 @@ namespace VC {
               TraceCachingAction(pc, CachingAction.RecycleError);
               pc = new AssumeCmd(ac.tok, copy);
               pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);
+              currentImplementation.AddRecycledFailingAssertion(ac);
             }
-            dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;
-            if (dropCmd || alwaysUseSubsumption)
+            else if (subsumption == CommandLineOptions.SubsumptionOption.Never)
             {
+              TraceCachingAction(pc, CachingAction.RecycleError);
+              dropCmd = true;
               currentImplementation.AddRecycledFailingAssertion(ac);
             }
+            else
+            {
+              TraceCachingAction(pc, CachingAction.DoNothingToAssert);
+            }
           }
           else
           {
@@ -1643,6 +1676,7 @@ namespace VC {
           }
           else
           {
+            TraceCachingAction(pc, CachingAction.DropAssume);
             dropCmd = true;
           }
         }
@@ -1651,10 +1685,6 @@ namespace VC {
         {
           passiveCmds.Add(pc);
         }
-        else
-        {
-          TraceCachingAction(pc, pc is AssumeCmd ? CachingAction.DropAssume : CachingAction.DropAssert);
-        }
       }
       #endregion
       #region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below]
-- 
cgit v1.2.3