Worked on the verification result caching.

1 files changed, 50 insertions, 20 deletions

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]