early clearing of live variables and incarnation maps

1 files changed, 24 insertions, 2 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 2e279479..2210d357 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1131,6 +1131,7 @@ namespace VC {
           #region Create an assume command equating v_prime with its last incarnation in pred

           #region Create an identifier expression for the last incarnation in pred

           Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(block2Incarnation[pred]);

+

           Expr pred_incarnation_exp;

           Expr o = (Expr)predMap[v];

           if (o == null) {

@@ -1236,17 +1237,38 @@ namespace VC {
       // processed all of a node's predecessors before we process the node.

       Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();

       Block exitBlock = null;

+      Hashtable exitIncarnationMap = null;

       foreach (Block b in sortedNodes) {

         Contract.Assert(b != null);

         Contract.Assert(!block2Incarnation.Contains(b));

         Hashtable /*Variable -> Expr*/ incarnationMap = ComputeIncarnationMap(b, block2Incarnation);

 

+        // b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out.

+        b.liveVarsBefore = null;

+

+        // Decrement the succCount field in each predecessor. Once the field reaches zero in any block, 

+        // all its successors have been passified.  Consequently, its entry in block2Incarnation can be removed.

+        foreach (Block p in b.Predecessors) {

+          p.succCount--;

+          if (p.succCount == 0)

+            block2Incarnation.Remove(p);

+        }

+

         #region Each block's map needs to be available to successor blocks

-        block2Incarnation.Add(b, incarnationMap);

+        GotoCmd gotoCmd = b.TransferCmd as GotoCmd;

+        if (gotoCmd == null) {

+          b.succCount = 0;

+        }

+        else {

+          // incarnationMap needs to be added only if there is some successor of b

+          b.succCount = gotoCmd.labelNames.Length;

+          block2Incarnation.Add(b, incarnationMap);

+        }

         #endregion Each block's map needs to be available to successor blocks

 

         TurnIntoPassiveBlock(b, incarnationMap, mvInfo, oldFrameSubst);

         exitBlock = b;

+        exitIncarnationMap = incarnationMap;

       }

 

       // Verify that exitBlock is indeed the unique exit block

@@ -1254,7 +1276,7 @@ namespace VC {
       Contract.Assert(exitBlock.TransferCmd is ReturnCmd);

       #endregion Convert to Passive Commands

 

-      return (Hashtable)block2Incarnation[exitBlock];

+      return exitIncarnationMap;

     }

 

     /// <summary>