early clearing of live variables and incarnation maps

3 files changed, 27 insertions, 10 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 87b48740..825efa21 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -813,6 +813,9 @@ namespace Microsoft.Boogie {
     // VC generation and SCC computation

     public BlockSeq/*!*/ Predecessors;

 

+    // This field is used during passification to null-out entries in block2Incartion hashtable early

+    public int succCount;

+

     public HashSet<Variable/*!*/> liveVarsBefore;

     [ContractInvariantMethod]

     void ObjectInvariant() {

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>

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 4e7dbef0..19418b46 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2320,14 +2320,6 @@ namespace VC {
       storeIncarnationMaps(impl.Name, exitIncarnationMap);

       #endregion

             

-      if (CommandLineOptions.Clo.LiveVariableAnalysis == 1) {

-        Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);

-      } 

-      // TODO: fix

-      //else if (CommandLineOptions.Clo.LiveVariableAnalysis == 2) {

-      //  Microsoft.Boogie.InterProcGenKill.ClearLiveVariables(impl, program);

-      //}

-      

       #region Peep-hole optimizations

       if (CommandLineOptions.Clo.RemoveEmptyBlocks){

         #region Get rid of empty blocks