Did some refactoring.

4 files changed, 72 insertions, 48 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index a419fead..a9466f8d 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -3128,7 +3128,14 @@ namespace Microsoft.Boogie {
       assertionChecksums.Add(checksum);

     }

 

-    public ISet<byte[]> AssertionChecksumsInPreviousSnapshot { get; set; }

+    public ISet<byte[]> AssertionChecksumsInCachedSnapshot { get; set; }

+

+    public bool IsAssertionChecksumInCachedSnapshot(byte[] checksum)

+    {

+      Contract.Requires(AssertionChecksumsInCachedSnapshot != null);

+

+      return AssertionChecksumsInCachedSnapshot.Contains(checksum);

+    }

 

     public IList<AssertCmd> RecycledFailingAssertions { get; protected set; }

 

@@ -3214,6 +3221,13 @@ namespace Microsoft.Boogie {
 

     public IDictionary<byte[], object> ErrorChecksumToCachedError { get; private set; }

 

+    public bool IsErrorChecksumInCachedSnapshot(byte[] checksum)

+    {

+      Contract.Requires(ErrorChecksumToCachedError != null);

+

+      return ErrorChecksumToCachedError.ContainsKey(checksum);

+    }

+

     public void SetErrorChecksumToCachedError(IEnumerable<Tuple<byte[], object>> errors)

     {

       Contract.Requires(errors != null);

@@ -3225,11 +3239,11 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public bool NoErrorsInCachedSnapshot

+    public bool HasCachedSnapshot

     {

       get

       {

-        return ErrorChecksumToCachedError != null && !ErrorChecksumToCachedError.Any();

+        return ErrorChecksumToCachedError != null && AssertionChecksumsInCachedSnapshot != null;

       }

     }

 

@@ -3237,7 +3251,9 @@ namespace Microsoft.Boogie {
     {

       get

       {

-        return ErrorChecksumToCachedError != null && ErrorChecksumToCachedError.Any();

+        Contract.Requires(ErrorChecksumToCachedError != null);

+

+        return ErrorChecksumToCachedError.Any();

       }

     }

 

@@ -3246,15 +3262,22 @@ namespace Microsoft.Boogie {
     {

       get

       {

-        return injectedAssumptionVariables;

+        return injectedAssumptionVariables != null ? injectedAssumptionVariables : new List<LocalVariable>();

       }

     }

 

-    public Expr ConjunctionOfInjectedAssumptionVariables(Dictionary<Variable, Expr> incarnationMap)

+    public List<LocalVariable> PossiblyFalseAssumptionVariables(Dictionary<Variable, Expr> incarnationMap)

+    {

+      return InjectedAssumptionVariables.Where(v => incarnationMap.ContainsKey(v)).ToList();

+    }

+

+    public Expr ConjunctionOfInjectedAssumptionVariables(Dictionary<Variable, Expr> incarnationMap, out bool isTrue)

     {

-      Contract.Requires(InjectedAssumptionVariables != null && InjectedAssumptionVariables.Any() && incarnationMap != null);

+      Contract.Requires(incarnationMap != null);

 

-      return LiteralExpr.BinaryTreeAnd(injectedAssumptionVariables.Where(v => incarnationMap.ContainsKey(v)).Select(v => incarnationMap[v]).ToList());

+      var vars = PossiblyFalseAssumptionVariables(incarnationMap).Select(v => incarnationMap[v]).ToList();

+      isTrue = vars.Count == 0;

+      return LiteralExpr.BinaryTreeAnd(vars);

     }

 

     public void InjectAssumptionVariable(LocalVariable variable)

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index e9975fe5..2993feb7 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -421,14 +421,13 @@ namespace Microsoft.Boogie {
       foreach (Block/*!*/ block in sortedNodes) {

         Contract.Assert(block != null);

         HashSet<Variable/*!*/>/*!*/ liveVarsAfter = new HashSet<Variable/*!*/>();

-        if (impl.InjectedAssumptionVariables != null)

+

+        // The injected assumption variables should always be considered to be live.

+        foreach (var v in impl.InjectedAssumptionVariables)

         {

-          // The injected assumption variables should always be considered to be live.

-          foreach (var v in impl.InjectedAssumptionVariables)

-          {

-            liveVarsAfter.Add(v);

-          }

+          liveVarsAfter.Add(v);

         }

+

         if (block.TransferCmd is GotoCmd) {

           GotoCmd gotoCmd = (GotoCmd)block.TransferCmd;

           if (gotoCmd.labelTargets != null) {

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index eed92d31..e647ea3b 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -136,7 +136,7 @@ namespace Microsoft.Boogie
                 var p = ExecutionEngine.CachedProgram(vr.ProgramId);

                 if (p != null)

                 {

-                  SetAssertionChecksumsInPreviousSnapshot(impl, p);

+                  SetAssertionChecksumsInCachedSnapshot(impl, p);

                   eai.Inject(impl, p);

                   run.RewrittenImplementationCount++;

                 }

@@ -154,7 +154,7 @@ namespace Microsoft.Boogie
                 var p = ExecutionEngine.CachedProgram(vr.ProgramId);

                 if (p != null)

                 {

-                  SetAssertionChecksumsInPreviousSnapshot(impl, p);

+                  SetAssertionChecksumsInCachedSnapshot(impl, p);

                 }

               }

             }

@@ -202,12 +202,12 @@ namespace Microsoft.Boogie
       }

     }

 

-    private static void SetAssertionChecksumsInPreviousSnapshot(Implementation implementation, Program program)

+    private static void SetAssertionChecksumsInCachedSnapshot(Implementation implementation, Program program)

     {

-      var implPrevSnap = program.FindImplementation(implementation.Id);

-      if (implPrevSnap != null)

+      var cachedImpl = program.FindImplementation(implementation.Id);

+      if (cachedImpl != null)

       {

-        implementation.AssertionChecksumsInPreviousSnapshot = implPrevSnap.AssertionChecksums;

+        implementation.AssertionChecksumsInCachedSnapshot = cachedImpl.AssertionChecksums;

       }

     }

 

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 36f38ab8..8295a873 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1489,6 +1489,7 @@ namespace VC {
         }

         Contract.Assert(copy != null);

         var dropCmd = false;

+        var possiblyFalseAssumpVars = currentImplementation != null ? currentImplementation.PossiblyFalseAssumptionVariables(incarnationMap) : null;

         if (pc is AssertCmd) {

           var ac = (AssertCmd)pc;

           ac.OrigExpr = ac.Expr;

@@ -1499,15 +1500,14 @@ namespace VC {
           var alwaysUseSubsumption = subsumption == CommandLineOptions.SubsumptionOption.Always;

           if (alwaysUseSubsumption

               && currentImplementation != null

-              && ((currentImplementation.NoErrorsInCachedSnapshot

-                   && currentImplementation.InjectedAssumptionVariables != null

-                   && 2 <= currentImplementation.InjectedAssumptionVariables.Count)

-                  || (currentImplementation.AnyErrorsInCachedSnapshot

-                      && currentImplementation.InjectedAssumptionVariables != null

-                      && currentImplementation.InjectedAssumptionVariables.Any()

-                      && ac.Checksum != null

-                      && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))

-                      && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum))))

+              && currentImplementation.HasCachedSnapshot

+              && ((!currentImplementation.AnyErrorsInCachedSnapshot

+                   && 2 <= possiblyFalseAssumpVars.Count)

+                   || (currentImplementation.AnyErrorsInCachedSnapshot

+                       && possiblyFalseAssumpVars.Any()

+                       && ac.Checksum != null

+                       && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum)

+                       && !currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum))))

           {

             // Bind the assertion expression to a local variable.

             var incarnation = CreateIncarnation(CurrentTemporaryVariableForAssertions, containingBlock);

@@ -1516,9 +1516,10 @@ namespace VC {
             ac.IncarnationMap[incarnation] = identExpr;

             passiveCmds.Add(new AssumeCmd(Token.NoToken, LiteralExpr.Eq(identExpr, copy)));

             copy = identExpr;

-            var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap);

+            bool isTrue;

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

             Expr expr = identExpr;

-            if (assmVars != Expr.True)

+            if (!isTrue)

             {

               expr = LiteralExpr.Imp(assmVars, expr);

             }

@@ -1530,10 +1531,10 @@ namespace VC {
           }

           else if (currentImplementation != null

                    && ac.Checksum != null

-                   && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))

-                   && currentImplementation.ErrorChecksumToCachedError != null

-                   && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)

-                   && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))

+                   && currentImplementation.HasCachedSnapshot

+                   && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum)

+                   && !currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum)

+                   && possiblyFalseAssumpVars.Count == 0)

           {

             if (alwaysUseSubsumption)

             {

@@ -1544,11 +1545,12 @@ namespace VC {
             dropCmd = subsumption == CommandLineOptions.SubsumptionOption.Never;

           }

           else if (currentImplementation != null

+                   && currentImplementation.HasCachedSnapshot

                    && currentImplementation.AnyErrorsInCachedSnapshot

                    && ac.Checksum != null

-                   && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(ac.Checksum))

-                   && currentImplementation.ErrorChecksumToCachedError.ContainsKey(ac.Checksum)

-                   && (currentImplementation.InjectedAssumptionVariables == null || !currentImplementation.InjectedAssumptionVariables.Any(v => incarnationMap.ContainsKey(v))))

+                   && currentImplementation.IsAssertionChecksumInCachedSnapshot(ac.Checksum)

+                   && currentImplementation.IsErrorChecksumInCachedSnapshot(ac.Checksum)

+                   && possiblyFalseAssumpVars.Count == 0)

           {

             if (alwaysUseSubsumption)

             {

@@ -1564,12 +1566,11 @@ namespace VC {
           }

         }

         else if (pc is AssumeCmd

-                 && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot")

-                 && currentImplementation.InjectedAssumptionVariables != null

-                 && currentImplementation.InjectedAssumptionVariables.Any())

+                 && QKeyValue.FindBoolAttribute(pc.Attributes, "precondition_previous_snapshot"))

         {

-          var assmVars = currentImplementation.ConjunctionOfInjectedAssumptionVariables(incarnationMap);

-          if (assmVars != Expr.True)

+          bool isTrue;

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

+          if (!isTrue)

           {

             copy = LiteralExpr.Imp(assmVars, copy);

           }

@@ -1577,11 +1578,12 @@ namespace VC {
         }

         pc.Expr = copy;

         if (!dropCmd

-            || currentImplementation.NoErrorsInCachedSnapshot

+            || !currentImplementation.HasCachedSnapshot

+            || !currentImplementation.AnyErrorsInCachedSnapshot

             || (currentImplementation.AnyErrorsInCachedSnapshot

                 && pc.Checksum != null

-                && (currentImplementation.AssertionChecksumsInPreviousSnapshot != null && currentImplementation.AssertionChecksumsInPreviousSnapshot.Contains(pc.Checksum))

-                && !currentImplementation.ErrorChecksumToCachedError.ContainsKey(pc.Checksum)))

+                && currentImplementation.IsAssertionChecksumInCachedSnapshot(pc.Checksum)

+                && !currentImplementation.IsErrorChecksumInCachedSnapshot(pc.Checksum)))

         {

           passiveCmds.Add(pc);

         }

@@ -1657,8 +1659,8 @@ namespace VC {
         }

 

         if (currentImplementation != null

-            && currentImplementation.NoErrorsInCachedSnapshot

-            && currentImplementation.InjectedAssumptionVariables != null

+            && currentImplementation.HasCachedSnapshot

+            && !currentImplementation.AnyErrorsInCachedSnapshot

             && currentImplementation.InjectedAssumptionVariables.Count == 1

             && assign.Lhss.Count == 1)

         {