Extract classes out of DeadVarElim (#935)

Extract classes out of DeadVarElim

Source/Core/Analysis/BlockCoalescer.cs

@@ -0,0 +1,165 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie;
+
+public class BlockCoalescer : ReadOnlyVisitor
+{
+  public static void CoalesceBlocks(Program program)
+  {
+    Contract.Requires(program != null);
+    BlockCoalescer blockCoalescer = new BlockCoalescer();
+    blockCoalescer.Visit(program);
+  }
+
+  private static HashSet<Block /*!*/> /*!*/ ComputeMultiPredecessorBlocks(Implementation /*!*/ impl)
+  {
+    Contract.Requires(impl != null);
+    Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Block>>()));
+    HashSet<Block /*!*/> visitedBlocks = new HashSet<Block /*!*/>();
+    HashSet<Block /*!*/> multiPredBlocks = new HashSet<Block /*!*/>();
+    Stack<Block /*!*/> dfsStack = new Stack<Block /*!*/>();
+    dfsStack.Push(impl.Blocks[0]);
+    while (dfsStack.Count > 0)
+    {
+      Block /*!*/
+        b = dfsStack.Pop();
+      Contract.Assert(b != null);
+      if (visitedBlocks.Contains(b))
+      {
+        multiPredBlocks.Add(b);
+        continue;
+      }
+
+      visitedBlocks.Add(b);
+      if (b.TransferCmd == null)
+      {
+        continue;
+      }
+
+      if (b.TransferCmd is ReturnCmd)
+      {
+        continue;
+      }
+
+      Contract.Assert(b.TransferCmd is GotoCmd);
+      GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
+      if (gotoCmd.labelTargets == null)
+      {
+        continue;
+      }
+
+      foreach (Block /*!*/ succ in gotoCmd.labelTargets)
+      {
+        Contract.Assert(succ != null);
+        dfsStack.Push(succ);
+      }
+    }
+
+    return multiPredBlocks;
+  }
+
+  public override Implementation VisitImplementation(Implementation impl)
+  {
+    //Contract.Requires(impl != null);
+    Contract.Ensures(Contract.Result<Implementation>() != null);
+    //Console.WriteLine("Procedure {0}", impl.Name);
+    //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count);
+
+    HashSet<Block /*!*/> multiPredBlocks = ComputeMultiPredecessorBlocks(impl);
+    Contract.Assert(cce.NonNullElements(multiPredBlocks));
+    HashSet<Block /*!*/> visitedBlocks = new HashSet<Block /*!*/>();
+    HashSet<Block /*!*/> removedBlocks = new HashSet<Block /*!*/>();
+    Stack<Block /*!*/> dfsStack = new Stack<Block /*!*/>();
+    dfsStack.Push(impl.Blocks[0]);
+    while (dfsStack.Count > 0)
+    {
+      Block /*!*/
+        b = dfsStack.Pop();
+      Contract.Assert(b != null);
+      if (visitedBlocks.Contains(b))
+      {
+        continue;
+      }
+
+      visitedBlocks.Add(b);
+      if (b.TransferCmd == null)
+      {
+        continue;
+      }
+
+      if (b.TransferCmd is ReturnCmd)
+      {
+        continue;
+      }
+
+      Contract.Assert(b.TransferCmd is GotoCmd);
+      GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
+      if (gotoCmd.labelTargets == null)
+      {
+        continue;
+      }
+
+      if (gotoCmd.labelTargets.Count == 1)
+      {
+        Block /*!*/
+          succ = cce.NonNull(gotoCmd.labelTargets[0]);
+        if (!multiPredBlocks.Contains(succ))
+        {
+          foreach (Cmd /*!*/ cmd in succ.Cmds)
+          {
+            Contract.Assert(cmd != null);
+            b.Cmds.Add(cmd);
+          }
+
+          b.TransferCmd = succ.TransferCmd;
+          if (!b.tok.IsValid && succ.tok.IsValid)
+          {
+            b.tok = succ.tok;
+            b.Label = succ.Label;
+          }
+
+          removedBlocks.Add(succ);
+          dfsStack.Push(b);
+          visitedBlocks.Remove(b);
+          continue;
+        }
+      }
+
+      foreach (Block /*!*/ succ in gotoCmd.labelTargets)
+      {
+        Contract.Assert(succ != null);
+        dfsStack.Push(succ);
+      }
+    }
+
+    List<Block /*!*/> newBlocks = new List<Block /*!*/>();
+    foreach (Block /*!*/ b in impl.Blocks)
+    {
+      Contract.Assert(b != null);
+      if (visitedBlocks.Contains(b) && !removedBlocks.Contains(b))
+      {
+        newBlocks.Add(b);
+      }
+    }
+
+    impl.Blocks = newBlocks;
+    foreach (Block b in impl.Blocks)
+    {
+      if (b.TransferCmd is ReturnCmd)
+      {
+        continue;
+      }
+
+      GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
+      gotoCmd.labelNames = new List<string>();
+      foreach (Block succ in gotoCmd.labelTargets)
+      {
+        gotoCmd.labelNames.Add(succ.Label);
+      }
+    }
+
+    // Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count);
+    return impl;
+  }
+}

Source/Core/Analysis/LiveVariableAnalysis/GenKillWeight.cs

@@ -0,0 +1,189 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie;
+
+/*
+// An idempotent semiring interface
+abstract public class Weight {
+   abstract public Weight! one();
+   abstract public Weight! zero();
+   abstract public Weight! extend(Weight! w1, Weight! w2);
+   abstract public Weight! combine(Weight! w1, Weight! w2);
+   abstract public Weight! isEqual(Weight! w);
+   abstract public Weight! projectLocals()
+}
+*/
+
+// Weight domain for LiveVariableAnalysis (Gen/Kill)
+public class GenKillWeight
+{
+  // lambda S. (S - kill) union gen
+  HashSet<Variable /*!*/> /*!*/
+    gen;
+
+  HashSet<Variable /*!*/> /*!*/
+    kill;
+
+  [ContractInvariantMethod]
+  void ObjectInvariant()
+  {
+    Contract.Invariant(cce.NonNullElements(gen));
+    Contract.Invariant(cce.NonNullElements(kill));
+    Contract.Invariant(oneWeight != null);
+    Contract.Invariant(zeroWeight != null);
+  }
+
+  bool isZero;
+
+  public static GenKillWeight /*!*/
+    oneWeight = new GenKillWeight(new HashSet<Variable /*!*/>(), new HashSet<Variable /*!*/>());
+
+  public static GenKillWeight /*!*/
+    zeroWeight = new GenKillWeight();
+
+  // initializes to zero
+  public GenKillWeight()
+  {
+    this.isZero = true;
+    this.gen = new HashSet<Variable /*!*/>();
+    this.kill = new HashSet<Variable /*!*/>();
+  }
+
+  public GenKillWeight(HashSet<Variable /*!*/> gen, HashSet<Variable /*!*/> kill)
+  {
+    Contract.Requires(cce.NonNullElements(gen));
+    Contract.Requires(cce.NonNullElements(kill));
+    Contract.Assert(gen != null);
+    Contract.Assert(kill != null);
+    this.gen = gen;
+    this.kill = kill;
+    this.isZero = false;
+  }
+
+  public static GenKillWeight one()
+  {
+    Contract.Ensures(Contract.Result<GenKillWeight>() != null);
+    return oneWeight;
+  }
+
+  public static GenKillWeight zero()
+  {
+    Contract.Ensures(Contract.Result<GenKillWeight>() != null);
+    return zeroWeight;
+  }
+
+  public static GenKillWeight extend(GenKillWeight w1, GenKillWeight w2)
+  {
+    Contract.Requires(w2 != null);
+    Contract.Requires(w1 != null);
+    Contract.Ensures(Contract.Result<GenKillWeight>() != null);
+    if (w1.isZero || w2.isZero)
+    {
+      return zero();
+    }
+
+    HashSet<Variable> t = new HashSet<Variable>(w2.gen);
+    t.ExceptWith(w1.kill);
+    HashSet<Variable> g = new HashSet<Variable>(w1.gen);
+    g.UnionWith(t);
+    HashSet<Variable> k = new HashSet<Variable>(w1.kill);
+    k.UnionWith(w2.kill);
+    return new GenKillWeight(g, k);
+    //return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill));
+  }
+
+  public static GenKillWeight combine(GenKillWeight w1, GenKillWeight w2)
+  {
+    Contract.Requires(w2 != null);
+    Contract.Requires(w1 != null);
+    Contract.Ensures(Contract.Result<GenKillWeight>() != null);
+    if (w1.isZero)
+    {
+      return w2;
+    }
+
+    if (w2.isZero)
+    {
+      return w1;
+    }
+
+    HashSet<Variable> g = new HashSet<Variable>(w1.gen);
+    g.UnionWith(w2.gen);
+    HashSet<Variable> k = new HashSet<Variable>(w1.kill);
+    k.IntersectWith(w2.kill);
+    return new GenKillWeight(g, k);
+    //return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill));
+  }
+
+  public static GenKillWeight projectLocals(GenKillWeight w)
+  {
+    Contract.Requires(w != null);
+    Contract.Ensures(Contract.Result<GenKillWeight>() != null);
+    HashSet<Variable /*!*/> gen = new HashSet<Variable>();
+    foreach (Variable v in w.gen)
+    {
+      if (isGlobal(v))
+      {
+        gen.Add(v);
+      }
+    }
+
+    HashSet<Variable /*!*/> kill = new HashSet<Variable>();
+    foreach (Variable v in w.kill)
+    {
+      if (isGlobal(v))
+      {
+        kill.Add(v);
+      }
+    }
+
+    return new GenKillWeight(gen, kill);
+  }
+
+  public static bool isEqual(GenKillWeight w1, GenKillWeight w2)
+  {
+    Contract.Requires(w2 != null);
+    Contract.Requires(w1 != null);
+    if (w1.isZero)
+    {
+      return w2.isZero;
+    }
+
+    if (w2.isZero)
+    {
+      return w1.isZero;
+    }
+
+    return (w1.gen.Equals(w2.gen) && w1.kill.Equals(w2.kill));
+  }
+
+  private static bool isGlobal(Variable v)
+  {
+    Contract.Requires(v != null);
+    return (v is GlobalVariable);
+  }
+
+  [Pure]
+  public override string ToString()
+  {
+    Contract.Ensures(Contract.Result<string>() != null);
+    return string.Format("({0},{1})", gen.ToString(), kill.ToString());
+  }
+
+  public HashSet<Variable /*!*/> /*!*/ getLiveVars()
+  {
+    Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));
+    return gen;
+  }
+
+  public HashSet<Variable /*!*/> /*!*/ getLiveVars(HashSet<Variable /*!*/> /*!*/ lv)
+  {
+    Contract.Requires(cce.NonNullElements(lv));
+    Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Variable>>()));
+    HashSet<Variable> temp = new HashSet<Variable>(lv);
+    temp.ExceptWith(kill);
+    temp.UnionWith(gen);
+    return temp;
+  }
+}