Worked on the verification result caching.

4 files changed, 60 insertions, 25 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index ab99102a..8f7aa185 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1293,7 +1293,10 @@ namespace Microsoft.Boogie {
       if (stream.UseForComputingChecksums)

       {

         var lhs = Lhss.FirstOrDefault() as SimpleAssignLhs;

-        if (lhs != null && lhs.AssignedVariable.Decl != null && QKeyValue.FindBoolAttribute(lhs.AssignedVariable.Decl.Attributes, "assumption"))

+        if (lhs != null

+            && lhs.AssignedVariable.Decl != null

+            && (QKeyValue.FindBoolAttribute(lhs.AssignedVariable.Decl.Attributes, "assumption")

+                || lhs.AssignedVariable.Decl.Name.Contains("##old##")))

         {

           return;

         }

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index c75bd52f..5bce360b 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -208,9 +208,9 @@ namespace Microsoft.Boogie
           {

             var oldUnmod = new LocalVariable(Token.NoToken,

               new TypedIdent(Token.NoToken, string.Format("{0}##old##{1}", unmod.Name, FreshTemporaryVariableName), unmod.Type));

-            before.Add(new AssignCmd(Token.NoToken,

-                         new List<AssignLhs> { new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod)) },

-                         new List<Expr> { new IdentifierExpr(Token.NoToken, unmod.Decl) }));

+            var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, oldUnmod));

+            var rhs = new IdentifierExpr(Token.NoToken, unmod.Decl);

+            before.Add(new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs }));

             var eq = LiteralExpr.Eq(new IdentifierExpr(Token.NoToken, oldUnmod), new IdentifierExpr(Token.NoToken, unmod.Decl));

             if (assumedExpr == null)

             {

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]

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index cf588e65..f34fefbe 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -203,7 +203,7 @@ Boogie program verifier finished with 0 verified, 1 error
 Processing call to procedure N in implementation M (at Snapshots11.v1.bpl(7,5)):

   >>> added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;

   >>> added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r;

-Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} 0 < n;

+Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;

   >>> DropAssume

 Processing command (at Snapshots11.v1.bpl(7,5)) assert 0 < call0formal#AT#n;

   >>> RecycleError

@@ -450,6 +450,8 @@ Processing command (at Snapshots24.v1.bpl(11,9)) assert {:subsumption 1} 5 == 5;
   >>> DoNothingToAssert

 Processing command (at Snapshots24.v1.bpl(15,9)) assert {:subsumption 2} 6 != 6;

   >>> RecycleError

+Processing command (at Snapshots24.v1.bpl(19,9)) assert {:subsumption 1} 2 == 2;

+  >>> DoNothingToAssert

 Processing command (at Snapshots24.v1.bpl(20,9)) assert {:subsumption 2} 4 == 4;

   >>> MarkAsFullyVerified

 Processing command (at Snapshots24.v1.bpl(21,9)) assert 5 == 5;