6 files changed, 179 insertions, 16 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc
index 423b436f..035879ec 100644
--- a/Source/BoogieDriver/BoogieDriver.ssc
+++ b/Source/BoogieDriver/BoogieDriver.ssc
@@ -70,7 +70,7 @@ namespace Microsoft.Boogie
 

       SelectPlatform(CommandLineOptions.Clo);

 

-      Helpers.ExtraTraceInformation("Becoming sentinent");

+      Helpers.ExtraTraceInformation("Becoming sentient");

 

       // Make sure the Spec# runtime is initialized.

       // This happens when the static constructor for the Runtime type is executed.

@@ -418,7 +418,7 @@ namespace Microsoft.Boogie
     

     static PipelineOutcome EliminateDeadVariablesAndInline(Program! program) {

       // Eliminate dead variables

-      Microsoft.Boogie.DeadVarEliminator.Eliminate(program);

+      Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);

       

       // Inline

       List<Declaration!>! TopLevelDeclarations = program.TopLevelDeclarations;

diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc
index 723b40e3..d0c65c96 100644
--- a/Source/Core/AbsyCmd.ssc
+++ b/Source/Core/AbsyCmd.ssc
@@ -696,6 +696,12 @@ namespace Microsoft.Boogie
     // VC generation and SCC computation

     public BlockSeq! Predecessors;

 

+    public Set liveVarsBefore;

+    public bool IsLive(Variable! v) {

+      if (liveVarsBefore == null) return true;

+      return liveVarsBefore.Contains(v);

+    }

+    

     public Block() { this(Token.NoToken, "", new CmdSeq(), new ReturnCmd(Token.NoToken));}

 

     public Block (IToken! tok, string! label, CmdSeq! cmds, TransferCmd transferCmd)

@@ -707,6 +713,7 @@ namespace Microsoft.Boogie
       this.PreInvariant = null;

       this.PostInvariant = null;

       this.Predecessors = new BlockSeq();

+      this.liveVarsBefore = null;

       this.TraversingStatus = VisitState.ToVisit;

       this.iterations = 0;

       // base(tok);

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 6a9eac04..bd54d624 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -228,6 +228,8 @@ namespace Microsoft.Boogie
     

     public bool ReflectAdd = false;

 

+    public bool LiveVariableAnalysis = true;

+    

     // Static constructor

     static CommandLineOptions()

     {

@@ -821,6 +823,25 @@ namespace Microsoft.Boogie
             }

             break;

           

+          case "-liveVariableAnalysis":

+          case "/liveVariableAnalysis":

+            if (ps.ConfirmArgumentCount(1))

+            {

+              switch (args[ps.i])

+              {

+                case "0": 

+                  LiveVariableAnalysis = false;

+                  break;

+                case "1":

+                  LiveVariableAnalysis = true;

+                  break;

+                default:

+                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                  break;

+              }

+            }

+            break;

+            

           case "/DoomDebug":

             vcVariety = VCVariety.Doomed;

             useDoomDebug = true;

@@ -1141,7 +1162,7 @@ namespace Microsoft.Boogie
               ps.CheckBooleanFlag("z3types", ref Z3types) ||

               ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||

               ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||

-              ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory)

+              ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) 

               )

             {

               // one of the boolean flags matched

@@ -1820,7 +1841,9 @@ namespace Microsoft.Boogie
   /break[:method] : break into debugger

 

   ---- Verification-condition generation options -----------------------------

-

+  

+  /liveVariableAnalysis:<c> : 0 = do not perform live variable analysis 

+                              1 = perform live variable analysis (default)

   /noVerify      : skip VC generation and invocation of the theorem prover

   /noRemoveEmptyBlocks : do not remove empty blocks during VC generation

   /vc:<variety>  : n = nested block (default for non-/prover:z3),

diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc
index 897ca9e8..c7b0c7d8 100644
--- a/Source/Core/DeadVarElim.ssc
+++ b/Source/Core/DeadVarElim.ssc
@@ -1,18 +1,17 @@
 using System;

 using System.Collections.Generic;

-  

+using Graphing;

+

 namespace Microsoft.Boogie

 {

-  public class DeadVarEliminator : StandardVisitor {

+  public class UnusedVarEliminator : VariableCollector {

     public static void Eliminate(Program! program) {

-      DeadVarEliminator elim = new DeadVarEliminator();

+      UnusedVarEliminator elim = new UnusedVarEliminator();

       elim.Visit(program);

     }

-    

-    private System.Collections.Generic.Set<Variable!>! usedVars;

   

-    private DeadVarEliminator() {

-      usedVars = new System.Collections.Generic.Set<Variable!>();

+    private UnusedVarEliminator() {

+      base();

     }

       

 	public override Implementation! VisitImplementation(Implementation! node) {

@@ -30,12 +29,141 @@ namespace Microsoft.Boogie
 	  usedVars.Clear();

 	  return impl;

 	}

+  }

+  

+  public class VariableCollector : StandardVisitor {

+	public System.Collections.Generic.Set<Variable!>! usedVars;

+	public VariableCollector() {

+	  usedVars = new System.Collections.Generic.Set<Variable!>();

+	}

 	

-	public override Expr! VisitIdentifierExpr(IdentifierExpr! node)

-    {

-      if (node.Decl != null)

+    public override Expr! VisitIdentifierExpr(IdentifierExpr! node) {

+      if (node.Decl != null) {

         usedVars.Add(node.Decl);

+      }

       return node;

     }

+  } 

+  

+  public class LiveVariableAnalysis {

+	public static void ComputeLiveVariables(Program! program, Implementation! impl) {

+	  Microsoft.Boogie.Helpers.ExtraTraceInformation("Starting live variable analysis");

+	  Graphing.Graph<Block> dag = new Graph<Block>();

+      dag.AddSource((!)impl.Blocks[0]); // there is always at least one node in the graph

+      foreach (Block b in impl.Blocks)

+      {

+        GotoCmd gtc = b.TransferCmd as GotoCmd;

+        if (gtc != null)

+        {

+          assume gtc.labelTargets != null;

+          foreach (Block! dest in gtc.labelTargets)

+          {

+            dag.AddEdge(dest, b);

+          }

+        }

+      }

+      

+      IEnumerable<Block> sortedNodes = dag.TopologicalSort();

+	  foreach (Block! block in sortedNodes) {

+	    Set! liveVarsAfter = new Set();

+	    if (block.TransferCmd is GotoCmd) {

+	      GotoCmd gotoCmd = (GotoCmd) block.TransferCmd;

+	      if (gotoCmd.labelTargets != null) {

+	        foreach (Block! succ in gotoCmd.labelTargets) {

+	          assert succ.liveVarsBefore != null;

+	          liveVarsAfter.AddAll(succ.liveVarsBefore);

+	        }

+	      }

+	    }

+	    

+        CmdSeq cmds = block.Cmds;

+	    int len = cmds.Length;

+	    for (int i = len - 1; i >= 0; i--) {

+	      Propagate(cmds[i], liveVarsAfter);

+	    }

+	    

+	    block.liveVarsBefore = liveVarsAfter;

+	  }

+	}

+	

+	// perform in place update of liveSet

+	private static void Propagate(Cmd! cmd, Set! liveSet) {

+	  if (cmd is AssignCmd) {

+	    AssignCmd! assignCmd = (AssignCmd) cmd;

+	    // I must first iterate over all the targets and remove the live ones.

+	    // After the removals are done, I must add the variables referred on 

+	    // the right side of the removed targets

+	    Set<int> indexSet = new Set<int>();

+	    int index = 0;

+	    foreach (AssignLhs! lhs in assignCmd.Lhss) {

+	      Variable var = lhs.DeepAssignedVariable;

+	      if (var != null && liveSet.Contains(var)) {

+	        indexSet.Add(index);

+	        if (lhs is SimpleAssignLhs) {

+	          // we should only remove non-map target variables because there is an implicit

+	          // read of a map variable in an assignment to it

+			  liveSet.Remove(var);

+			}

+	      }

+	      index++;

+	    }

+	    index = 0;

+	    foreach (Expr! expr in assignCmd.Rhss) {

+	      if (indexSet.Contains(index)) {

+	        VariableCollector! collector = new VariableCollector();

+	        collector.Visit(expr);

+	        liveSet.AddAll(collector.usedVars);

+	        AssignLhs lhs = assignCmd.Lhss[index];

+	        if (lhs is MapAssignLhs) {

+	          // If the target is a map, then all indices are also read

+	          MapAssignLhs malhs = (MapAssignLhs) lhs;

+	          foreach (Expr e in malhs.Indexes) {

+	            VariableCollector! c = new VariableCollector();

+	            c.Visit(e);

+	            liveSet.AddAll(c.usedVars);

+	          }

+	        }

+	      }

+	      index++;

+	    }

+	  } else if (cmd is HavocCmd) {

+	    HavocCmd! havocCmd = (HavocCmd) cmd;

+	    foreach (IdentifierExpr! expr in havocCmd.Vars) {

+	      if (expr.Decl != null) {

+	        liveSet.Remove(expr.Decl);

+	      }

+	    }

+	  } else if (cmd is PredicateCmd) {

+	    assert (cmd is AssertCmd || cmd is AssumeCmd);

+	    PredicateCmd! predicateCmd = (PredicateCmd) cmd;

+	    if (predicateCmd.Expr is LiteralExpr) {

+	      LiteralExpr le = (LiteralExpr) predicateCmd.Expr;

+	      if (le.IsFalse) {

+	        liveSet.Clear();

+	      }

+	    } else {

+	      VariableCollector! collector = new VariableCollector();

+	      collector.Visit(predicateCmd.Expr);

+	      liveSet.AddAll(collector.usedVars);

+	    }

+	  } else if (cmd is CommentCmd) {

+        // comments are just for debugging and don't affect verification

+      } else if (cmd is SugaredCmd) {

+        SugaredCmd! sugCmd = (SugaredCmd) cmd;

+        Propagate(sugCmd.Desugaring, liveSet);

+      } else if (cmd is StateCmd) {

+        StateCmd! stCmd = (StateCmd) cmd;

+        CmdSeq! cmds = stCmd.Cmds;

+        int len = cmds.Length;

+        for (int i = len - 1; i >= 0; i--) {

+          Propagate(cmds[i], liveSet);

+        }

+        foreach (Variable! v in stCmd.Locals) {

+          liveSet.Remove(v);

+        }

+      } else {

+        assert false;

+      }

+	}

   }

 }
\ No newline at end of file
diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc
index e0088bb8..922ee68d 100644
--- a/Source/VCGeneration/ConditionGeneration.ssc
+++ b/Source/VCGeneration/ConditionGeneration.ssc
@@ -718,7 +718,7 @@ namespace VC
         {

           if (!incarnationMap.Contains(v))

           {

-            // v was not in the domain of the precessors seen so far, so it needs to be fixed up

+            // v was not in the domain of the predecessors seen so far, so it needs to be fixed up

             fixUps.Add(v);

           }

           else

@@ -735,8 +735,9 @@ namespace VC
       }

 

       #region Second, for all variables in the fixups list, introduce a new incarnation and push it back into the preds.

-      foreach (Variable! v in fixUps )

+      foreach (Variable! v in fixUps)

       {

+        if (!b.IsLive(v)) continue;

         Variable v_prime = CreateIncarnation(v, b);

         IdentifierExpr ie = new IdentifierExpr(v_prime.tok, v_prime);

         assert incarnationMap != null;

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index 7a3a772c..24104fb4 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -1753,6 +1753,10 @@ namespace VC
       }

       #endregion

     

+      if (CommandLineOptions.Clo.LiveVariableAnalysis) {

+	    Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(program, impl);

+	  }

+	  

       Convert2PassiveCmd(impl);

       

       #region Peep-hole optimizations