From a3325de0835308c293e999b574a804366f37d936 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 16 Jan 2015 12:21:49 +0100
Subject: Worked on the verification result caching (use native support for
 partially verified assertions).

---
 Source/VCGeneration/ConditionGeneration.cs | 92 +++---------------------------
 1 file changed, 9 insertions(+), 83 deletions(-)

(limited to 'Source/VCGeneration/ConditionGeneration.cs')

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
           {
-- 
cgit v1.2.3