Worked on the verification result caching (use native support for partially verified assertions).

2 files changed, 25 insertions, 118 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 454a2f30..bc535404 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -608,19 +608,6 @@ namespace VC {
 

     protected Implementation currentImplementation;

 

-    private LocalVariable currentTemporaryVariableForAssertions;

-    protected LocalVariable CurrentTemporaryVariableForAssertions

-    {

-      get

-      {

-        if (currentTemporaryVariableForAssertions == null)

-        {

-          currentTemporaryVariableForAssertions = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "##assertion", Microsoft.Boogie.Type.Bool));

-        }

-        return currentTemporaryVariableForAssertions;

-      }

-    }

-

     protected List<Variable> CurrentLocalVariables = null;

 

     // shared across each implementation; created anew for each implementation

@@ -1334,7 +1321,6 @@ namespace VC {
       Contract.Requires(mvInfo != null);

 

       currentImplementation = impl;

-      currentTemporaryVariableForAssertions = null;

 

       var start = DateTime.UtcNow;

 

@@ -1361,7 +1347,6 @@ namespace VC {
         }

       }

 

-      currentTemporaryVariableForAssertions = null;

       currentImplementation = null;

 

       RestoreParamWhereClauses(impl);

@@ -1552,7 +1537,6 @@ namespace VC {
           ac.IncarnationMap = (Dictionary<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(incarnationMap));

 

           var subsumption = Wlp.Subsumption(ac);

-          var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always;

           if (relevantDoomedAssumpVars.Any())

           {

             TraceCachingAction(pc, CachingAction.DoNothingToAssert);

@@ -1573,59 +1557,15 @@ namespace VC {
             {

               bool isTrue;

               var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap, out isTrue);

-              if (!isTrue && alwaysUseSubsumption)

+              TraceCachingAction(pc, !isTrue ? CachingAction.MarkAsPartiallyVerified : CachingAction.MarkAsFullyVerified);

+              var litExpr = ac.Expr as LiteralExpr;

+              if (litExpr == null || !litExpr.IsTrue)

               {

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

-

-                  // TODO(wuestholz): Try to use this instead:

-                  // ac.MarkAsVerifiedUnder(assmVars);

-                }

-                else

-                {

-                  dropCmd = true;

-                }

-              }

-              else if (isTrue)

-              {

-                if (alwaysUseSubsumption)

-                {

-                  TraceCachingAction(pc, CachingAction.MarkAsFullyVerified);

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

-                }

+                ac.MarkAsVerifiedUnder(assmVars);

               }

               else

               {

-                TraceCachingAction(pc, CachingAction.DoNothingToAssert);

+                dropCmd = true;

               }

             }

           }

@@ -1636,24 +1576,10 @@ namespace VC {
                    && currentImplementation.IsAssertionChecksumInCachedSnapshot(checksum)

                    && currentImplementation.IsErrorChecksumInCachedSnapshot(checksum))

           {

-            if (alwaysUseSubsumption)

-            {

-              // Turn it into an assume statement.

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

-            }

-            else if (subsumption == CommandLineOptions.SubsumptionOption.Never)

-            {

-              TraceCachingAction(pc, CachingAction.RecycleError);

-              dropCmd = true;

-              currentImplementation.AddRecycledFailingAssertion(ac);

-            }

-            else

-            {

-              TraceCachingAction(pc, CachingAction.DoNothingToAssert);

-            }

+            TraceCachingAction(pc, CachingAction.RecycleError);

+            ac.MarkAsVerifiedUnder(Expr.True);

+            currentImplementation.AddRecycledFailingAssertion(ac);

+            pc.Attributes = new QKeyValue(Token.NoToken, "recycled_failing_assertion", new List<object>(), pc.Attributes);

           }

           else

           {

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 6f6326d1..cd735501 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -106,17 +106,12 @@ namespace VC {
         AssertCmd ac = (AssertCmd)cmd;

         ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;

         VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);

-        ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext; 

-

-        VCExprLetBinding LB = null;

         VCExpr VU = null;

         if (ac.VerifiedUnder != null)

         {

-          var V = gen.Variable(ctxt.FreshLetBindingName(), Microsoft.Boogie.Type.Bool);

-          LB = gen.LetBinding(V, C);

-          C = V;

           VU = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.VerifiedUnder);

         }

+        ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext; 

 

         VCExpr R = null;

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

@@ -127,28 +122,24 @@ namespace VC {
             ctxt.Label2absy[id] = ac;

           }

 

-          switch (Subsumption(ac)) {

-            case CommandLineOptions.SubsumptionOption.Never:

-              break;

-            case CommandLineOptions.SubsumptionOption.Always:

-              N = gen.Implies(C, N);

-              break;

-            case CommandLineOptions.SubsumptionOption.NotForQuantifiers:

-              if (!(C is VCExprQuantifier)) {

-                N = gen.Implies(C, N);

-              }

-              break;

-            default:

-              Contract.Assert(false); throw new cce.UnreachableException();  // unexpected case

+          var subsumption = Subsumption(ac);

+          if (subsumption == CommandLineOptions.SubsumptionOption.Always

+              || (subsumption == CommandLineOptions.SubsumptionOption.NotForQuantifiers && !(C is VCExprQuantifier)))

+          {

+            N = gen.ImpliesSimp(C, N);

           }

 

-          ctxt.AssertionCount++;

+          if (VU != null)

+          {

+            var litExpr = ac.VerifiedUnder as LiteralExpr;

+            if (litExpr != null && litExpr.IsTrue)

+            {

+              return N;

+            }

+            C = gen.OrSimp(VU, C);

+          }

 

-          // TODO(wuestholz): Try to weaken the assertion instead of assuming the property that has already been verified:

-          // if (VU != null)

-          // {

-          //   C = gen.OrSimp(VU, C);

-          // }

+          ctxt.AssertionCount++;

 

           if (ctxt.ControlFlowVariableExpr == null) {

             Contract.Assert(ctxt.Label2absy != null);

@@ -164,16 +155,6 @@ namespace VC {
             }

           }

         }

-

-        if (VU != null)

-        {

-          R = gen.ImpliesSimp(gen.ImpliesSimp(VU, C), R);

-        }

-

-        if (LB != null)

-        {

-          R = gen.Let(R, LB);

-        }

         return R;

       } else if (cmd is AssumeCmd) {

         AssumeCmd ac = (AssumeCmd)cmd;