[llvm-commits] CVS: llvm/lib/Transforms/Scalar/PredicateSimplifier.cpp

Nick Lewycky nicholas at mxc.ca
Wed Nov 22 15:49:33 PST 2006



Changes in directory llvm/lib/Transforms/Scalar:

PredicateSimplifier.cpp updated: 1.33 -> 1.34
---
Log message:

Update to new predicate simplifier VRP design. Fixes PR966: http://llvm.org/PR966  and PR967: http://llvm.org/PR967 .
Remove predicate simplifier from default gcc3 pipeline. New design is too
slow to enable by default.
Add new testcases for problems encountered in development.


---
Diffs of the changes:  (+1117 -586)

 PredicateSimplifier.cpp | 1703 +++++++++++++++++++++++++++++++-----------------
 1 files changed, 1117 insertions(+), 586 deletions(-)


Index: llvm/lib/Transforms/Scalar/PredicateSimplifier.cpp
diff -u llvm/lib/Transforms/Scalar/PredicateSimplifier.cpp:1.33 llvm/lib/Transforms/Scalar/PredicateSimplifier.cpp:1.34
--- llvm/lib/Transforms/Scalar/PredicateSimplifier.cpp:1.33	Sun Nov  5 13:31:28 2006
+++ llvm/lib/Transforms/Scalar/PredicateSimplifier.cpp	Wed Nov 22 17:49:15 2006
@@ -1,11 +1,11 @@
-//===-- PredicateSimplifier.cpp - Path Sensitive Simplifier -----------===//
+//===-- PredicateSimplifier.cpp - Path Sensitive Simplifier ---------------===//
 //
 //                     The LLVM Compiler Infrastructure
 //
 // This file was developed by Nick Lewycky and is distributed under the
 // University of Illinois Open Source License. See LICENSE.TXT for details.
 //
-//===------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===//
 //
 // Path-sensitive optimizer. In a branch where x == y, replace uses of
 // x with y. Permits further optimization, such as the elimination of
@@ -20,13 +20,53 @@
 //     foo(); // unreachable
 // }
 //
-//===------------------------------------------------------------------===//
+//===----------------------------------------------------------------------===//
 //
-// This optimization works by substituting %q for %p when protected by a
-// conditional that assures us of that fact. Properties are stored as
-// relationships between two values.
+// This pass focusses on four properties; equals, not equals, less-than
+// and less-than-or-equals-to. The greater-than forms are also held just
+// to allow walking from a lesser node to a greater one. These properties
+// are stored in a lattice; LE can become LT or EQ, NE can become LT or GT.
 //
-//===------------------------------------------------------------------===//
+// These relationships define a graph between values of the same type. Each
+// Value is stored in a map table that retrieves the associated Node. This
+// is how EQ relationships are stored; the map contains pointers to the
+// same node. The node contains a most canonical Value* form and the list of
+// known relationships.
+//
+// If two nodes are known to be inequal, then they will contain pointers to
+// each other with an "NE" relationship. If node getNode(%x) is less than
+// getNode(%y), then the %x node will contain <%y, GT> and %y will contain
+// <%x, LT>. This allows us to tie nodes together into a graph like this:
+//
+//   %a < %b < %c < %d
+//
+// with four nodes representing the properties. The InequalityGraph provides
+// queries (such as "isEqual") and mutators (such as "addEqual"). To implement
+// "isLess(%a, %c)", we start with getNode(%c) and walk downwards until
+// we reach %a or the leaf node. Note that the graph is directed and acyclic,
+// but may contain joins, meaning that this walk is not a linear time
+// algorithm.
+//
+// To create these properties, we wait until a branch or switch instruction
+// implies that a particular value is true (or false). The VRPSolver is
+// responsible for analyzing the variable and seeing what new inferences
+// can be made from each property. For example:
+//
+//   %P = seteq int* %ptr, null
+//   %a = or bool %P, %Q
+//   br bool %a label %cond_true, label %cond_false
+//
+// For the true branch, the VRPSolver will start with %a EQ true and look at
+// the definition of %a and find that it can infer that %P and %Q are both
+// true. From %P being true, it can infer that %ptr NE null. For the false
+// branch it can't infer anything from the "or" instruction.
+//
+// Besides branches, we can also infer properties from instruction that may
+// have undefined behaviour in certain cases. For example, the dividend of
+// a division may never be zero. After the division instruction, we may assume
+// that the dividend is not equal to zero.
+//
+//===----------------------------------------------------------------------===//
 
 #define DEBUG_TYPE "predsimplify"
 #include "llvm/Transforms/Scalar.h"
@@ -34,513 +74,1018 @@
 #include "llvm/DerivedTypes.h"
 #include "llvm/Instructions.h"
 #include "llvm/Pass.h"
+#include "llvm/ADT/SetOperations.h"
+#include "llvm/ADT/SmallVector.h"
 #include "llvm/ADT/Statistic.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/Analysis/Dominators.h"
+#include "llvm/Analysis/ET-Forest.h"
+#include "llvm/Assembly/Writer.h"
 #include "llvm/Support/CFG.h"
 #include "llvm/Support/Debug.h"
 #include "llvm/Support/InstVisitor.h"
+#include "llvm/Transforms/Utils/Local.h"
+#include <algorithm>
+#include <deque>
 #include <iostream>
-#include <list>
+#include <sstream>
+#include <map>
 using namespace llvm;
 
-typedef DominatorTree::Node DTNodeType;
-
 namespace {
   Statistic<>
   NumVarsReplaced("predsimplify", "Number of argument substitutions");
   Statistic<>
   NumInstruction("predsimplify", "Number of instructions removed");
+  Statistic<>
+  NumSimple("predsimplify", "Number of simple replacements");
+
+  /// The InequalityGraph stores the relationships between values.
+  /// Each Value in the graph is assigned to a Node. Nodes are pointer
+  /// comparable for equality. The caller is expected to maintain the logical
+  /// consistency of the system.
+  ///
+  /// The InequalityGraph class may invalidate Node*s after any mutator call.
+  /// @brief The InequalityGraph stores the relationships between values.
+  class VISIBILITY_HIDDEN InequalityGraph {
+  public:
+    class Node;
+
+    // LT GT EQ
+    //  0  0  0 -- invalid (false)
+    //  0  0  1 -- invalid (EQ)
+    //  0  1  0 -- GT
+    //  0  1  1 -- GE
+    //  1  0  0 -- LT
+    //  1  0  1 -- LE
+    //  1  1  0 -- NE
+    //  1  1  1 -- invalid (true)
+    enum LatticeBits {
+      EQ_BIT = 1, GT_BIT = 2, LT_BIT = 4
+    };
+    enum LatticeVal {
+      GT = GT_BIT, GE = GT_BIT | EQ_BIT,
+      LT = LT_BIT, LE = LT_BIT | EQ_BIT,
+      NE = GT_BIT | LT_BIT
+    };
+
+    static bool validPredicate(LatticeVal LV) {
+      return LV > 1 && LV < 7;
+    }
 
-  class PropertySet;
+  private:
+    typedef std::map<Value *, Node *> NodeMapType;
+    NodeMapType Nodes;
 
-  /// Similar to EquivalenceClasses, this stores the set of equivalent
-  /// types. Beyond EquivalenceClasses, it allows us to specify which
-  /// element will act as leader.
-  template<typename ElemTy>
-  class VISIBILITY_HIDDEN Synonyms {
-    std::map<ElemTy, unsigned> mapping;
-    std::vector<ElemTy> leaders;
-    PropertySet *PS;
+    const InequalityGraph *ConcreteIG;
 
   public:
-    typedef unsigned iterator;
-    typedef const unsigned const_iterator;
+    /// A single node in the InequalityGraph. This stores the canonical Value
+    /// for the node, as well as the relationships with the neighbours.
+    ///
+    /// Because the lists are intended to be used for traversal, it is invalid
+    /// for the node to list itself in LessEqual or GreaterEqual lists. The
+    /// fact that a node is equal to itself is implied, and may be checked
+    /// with pointer comparison.
+    /// @brief A single node in the InequalityGraph.
+    class VISIBILITY_HIDDEN Node {
+      friend class InequalityGraph;
+
+      Value *Canonical;
+
+      typedef SmallVector<std::pair<Node *, LatticeVal>, 4> RelationsType;
+      RelationsType Relations;
+    public:
+      typedef RelationsType::iterator       iterator;
+      typedef RelationsType::const_iterator const_iterator;
+
+    private:
+      /// Updates the lattice value for a given node. Create a new entry if
+      /// one doesn't exist, otherwise it merges the values. The new lattice
+      /// value must not be inconsistent with any previously existing value.
+      void update(Node *N, LatticeVal R) {
+        iterator I = find(N);
+        if (I == end()) {
+          Relations.push_back(std::make_pair(N, R));
+        } else {
+          I->second = static_cast<LatticeVal>(I->second & R);
+          assert(validPredicate(I->second) &&
+                 "Invalid union of lattice values.");
+        }
+      }
+
+      void assign(Node *N, LatticeVal R) {
+        iterator I = find(N);
+        if (I != end()) I->second = R;
+
+        Relations.push_back(std::make_pair(N, R));
+      }
+
+    public:
+      iterator begin()       { return Relations.begin(); }
+      iterator end()         { return Relations.end();   }
+      iterator find(Node *N) {
+        iterator I = begin();
+        for (iterator E = end(); I != E; ++I)
+          if (I->first == N) break;
+        return I;
+      }
+
+      const_iterator begin()       const { return Relations.begin(); }
+      const_iterator end()         const { return Relations.end();   }
+      const_iterator find(Node *N) const {
+        const_iterator I = begin();
+        for (const_iterator E = end(); I != E; ++I)
+          if (I->first == N) break;
+        return I;
+      }
+
+      unsigned findIndex(Node *N) {
+        unsigned i = 0;
+        iterator I = begin();
+        for (iterator E = end(); I != E; ++I, ++i)
+          if (I->first == N) return i;
+        return (unsigned)-1;
+      }
 
-    Synonyms(PropertySet *PS) : PS(PS) {}
+      void erase(iterator i) { Relations.erase(i); }
 
-    // Inspection
+      Value *getValue() const { return Canonical; }
+      void setValue(Value *V) { Canonical = V; }
 
-    bool empty() const {
-      return leaders.empty();
+      void addNotEqual(Node *N)     { update(N, NE); }
+      void addLess(Node *N)         { update(N, LT); }
+      void addLessEqual(Node *N)    { update(N, LE); }
+      void addGreater(Node *N)      { update(N, GT); }
+      void addGreaterEqual(Node *N) { update(N, GE); }
+    };
+
+    InequalityGraph() : ConcreteIG(NULL) {}
+
+    InequalityGraph(const InequalityGraph &_IG) {
+#if 0 // disable COW
+      if (_IG.ConcreteIG) ConcreteIG = _IG.ConcreteIG;
+      else ConcreteIG = &_IG;
+#else
+      ConcreteIG = &_IG;
+      materialize();
+#endif
     }
 
-    iterator findLeader(ElemTy &e) {
-      typename std::map<ElemTy, unsigned>::iterator MI = mapping.find(e);
-      if (MI == mapping.end()) return 0;
+    ~InequalityGraph();
 
-      return MI->second;
+  private:
+    void materialize();
+
+  public:
+    /// If the Value is in the graph, return the canonical form. Otherwise,
+    /// return the original Value.
+    Value *canonicalize(Value *V) const {  
+      if (const Node *N = getNode(V))
+        return N->getValue();
+      else 
+        return V;
+    }
+
+    /// Returns the node currently representing Value V, or null if no such
+    /// node exists.
+    Node *getNode(Value *V) {
+      materialize();
+
+      NodeMapType::const_iterator I = Nodes.find(V);
+      return (I != Nodes.end()) ? I->second : 0;
+    }
+
+    const Node *getNode(Value *V) const {
+      if (ConcreteIG) return ConcreteIG->getNode(V);
+
+      NodeMapType::const_iterator I = Nodes.find(V);
+      return (I != Nodes.end()) ? I->second : 0;
+    }
+
+    Node *getOrInsertNode(Value *V) {
+      if (Node *N = getNode(V))
+        return N;
+      else
+        return newNode(V);
+    }
+
+    Node *newNode(Value *V) {
+      //DEBUG(std::cerr << "new node: " << *V << "\n");
+      materialize();
+      Node *&N = Nodes[V];
+      assert(N == 0 && "Node already exists for value.");
+      N = new Node();
+      N->setValue(V);
+      return N;
+    }
+
+    /// Returns true iff the nodes are provably inequal.
+    bool isNotEqual(const Node *N1, const Node *N2) const {
+      if (N1 == N2) return false;
+      for (Node::const_iterator I = N1->begin(), E = N1->end(); I != E; ++I) {
+        if (I->first == N2)
+          return (I->second & EQ_BIT) == 0;
+      }
+      return isLess(N1, N2) || isGreater(N1, N2);
     }
 
-    const_iterator findLeader(ElemTy &e) const {
-      typename std::map<ElemTy, unsigned>::const_iterator MI =
-          mapping.find(e);
-      if (MI == mapping.end()) return 0;
+    /// Returns true iff N1 is provably less than N2.
+    bool isLess(const Node *N1, const Node *N2) const {
+      if (N1 == N2) return false;
+      for (Node::const_iterator I = N2->begin(), E = N2->end(); I != E; ++I) {
+        if (I->first == N1)
+          return I->second == LT;
+      }
+      for (Node::const_iterator I = N2->begin(), E = N2->end(); I != E; ++I) {
+        if ((I->second & (LT_BIT | GT_BIT)) == LT_BIT)
+          if (isLess(N1, I->first)) return true;
+      }
+      return false;
+    }
+
+    /// Returns true iff N1 is provably less than or equal to N2.
+    bool isLessEqual(const Node *N1, const Node *N2) const {
+      if (N1 == N2) return true;
+      for (Node::const_iterator I = N2->begin(), E = N2->end(); I != E; ++I) {
+        if (I->first == N1)
+          return (I->second & (LT_BIT | GT_BIT)) == LT_BIT;
+      }
+      for (Node::const_iterator I = N2->begin(), E = N2->end(); I != E; ++I) {
+        if ((I->second & (LT_BIT | GT_BIT)) == LT_BIT)
+          if (isLessEqual(N1, I->first)) return true;
+      }
+      return false;
+    }
 
-      return MI->second;
+    /// Returns true iff N1 is provably greater than N2.
+    bool isGreater(const Node *N1, const Node *N2) const {
+      return isLess(N2, N1);
     }
 
-    ElemTy &getLeader(iterator I) {
-      assert(I && I <= leaders.size() && "Illegal leader to get.");
-      return leaders[I-1];
+    /// Returns true iff N1 is provably greater than or equal to N2.
+    bool isGreaterEqual(const Node *N1, const Node *N2) const {
+      return isLessEqual(N2, N1);
     }
 
-    const ElemTy &getLeader(const_iterator I) const {
-      assert(I && I <= leaders.size() && "Illegal leaders to get.");
-      return leaders[I-1];
+    // The add* methods assume that your input is logically valid and may 
+    // assertion-fail or infinitely loop if you attempt a contradiction.
+
+    void addEqual(Node *N, Value *V) {
+      materialize();
+      Nodes[V] = N;
+    }
+
+    void addNotEqual(Node *N1, Node *N2) {
+      assert(N1 != N2 && "A node can't be inequal to itself.");
+      materialize();
+      N1->addNotEqual(N2);
+      N2->addNotEqual(N1);
+    }
+
+    /// N1 is less than N2.
+    void addLess(Node *N1, Node *N2) {
+      assert(N1 != N2 && !isLess(N2, N1) && "Attempt to create < cycle.");
+      materialize();
+      N2->addLess(N1);
+      N1->addGreater(N2);
+    }
+
+    /// N1 is less than or equal to N2.
+    void addLessEqual(Node *N1, Node *N2) {
+      assert(N1 != N2 && "Nodes are equal. Use mergeNodes instead.");
+      assert(!isGreater(N1, N2) && "Impossible: Adding x <= y when x > y.");
+      materialize();
+      N2->addLessEqual(N1);
+      N1->addGreaterEqual(N2);
+    }
+
+    /// Find the transitive closure starting at a node walking down the edges
+    /// of type Val. Type Inserter must be an inserter that accepts Node *.
+    template <typename Inserter>
+    void transitiveClosure(Node *N, LatticeVal Val, Inserter insert) {
+      for (Node::iterator I = N->begin(), E = N->end(); I != E; ++I) {
+        if (I->second == Val) {
+          *insert = I->first;
+          transitiveClosure(I->first, Val, insert);
+        }
+      }
+    }
+
+    /// Kills off all the nodes in Kill by replicating their properties into
+    /// node N. The elements of Kill must be unique. After merging, N's new
+    /// canonical value is NewCanonical. Type C must be a container of Node *.
+    template <typename C>
+    void mergeNodes(Node *N, C &Kill, Value *NewCanonical);
+
+    /// Removes a Value from the graph, but does not delete any nodes. As this
+    /// method does not delete Nodes, V may not be the canonical choice for
+    /// any node.
+    void remove(Value *V) {
+      materialize();
+
+      for (NodeMapType::iterator I = Nodes.begin(), E = Nodes.end(); I != E;) {
+        NodeMapType::iterator J = I++;
+        assert(J->second->getValue() != V && "Can't delete canonical choice.");
+        if (J->first == V) Nodes.erase(J);
+      }
     }
 
-#ifdef DEBUG
+#ifndef NDEBUG
     void debug(std::ostream &os) const {
-      for (unsigned i = 1, e = leaders.size()+1; i != e; ++i) {
-        os << i << ". " << *getLeader(i) << ": [";
-        for (std::map<Value *, unsigned>::const_iterator
-             I = mapping.begin(), E = mapping.end(); I != E; ++I) {
-          if ((*I).second == i && (*I).first != leaders[i-1]) {
-            os << *(*I).first << "  ";
-          }
+    std::set<Node *> VisitedNodes;
+    for (NodeMapType::const_iterator I = Nodes.begin(), E = Nodes.end();
+         I != E; ++I) {
+      Node *N = I->second;
+      os << *I->first << " == " << *N->getValue() << "\n";
+      if (VisitedNodes.insert(N).second) {
+        os << *N->getValue() << ":\n";
+        for (Node::const_iterator NI = N->begin(), NE = N->end();
+             NI != NE; ++NI) {
+          static const std::string names[8] =
+              { "00", "01", " <", "<=", " >", ">=", "!=", "07" };
+          os << "  " << names[NI->second] << " "
+             << *NI->first->getValue() << "\n";
         }
-        os << "]\n";
       }
     }
+  }
 #endif
+  };
 
-    // Mutators
+  InequalityGraph::~InequalityGraph() {
+    if (ConcreteIG) return;
 
-    void remove(ElemTy &e) {
-      ElemTy E = e;      // The parameter to erase must not be a reference to
-      mapping.erase(E);  // an element contained in the map.
-    }
-
-    /// Combine two sets referring to the same element, inserting the
-    /// elements as needed. Returns a valid iterator iff two already
-    /// existing disjoint synonym sets were combined. The iterator
-    /// points to the no longer existing element.
-    iterator unionSets(ElemTy E1, ElemTy E2);
-
-    /// Returns an iterator pointing to the synonym set containing
-    /// element e. If none exists, a new one is created and returned.
-    iterator findOrInsert(ElemTy &e) {
-      iterator I = findLeader(e);
-      if (I) return I;
-
-      leaders.push_back(e);
-      I = leaders.size();
-      mapping[e] = I;
-      return I;
+    std::vector<Node *> Remove;
+    for (NodeMapType::iterator I = Nodes.begin(), E = Nodes.end();
+         I != E; ++I) {
+      if (I->first == I->second->getValue())
+        Remove.push_back(I->second);
+    }
+    for (std::vector<Node *>::iterator I = Remove.begin(), E = Remove.end();
+         I != E; ++I) {
+      delete *I;
     }
-  };
+  }
 
-  /// Represents the set of equivalent Value*s and provides insertion
-  /// and fast lookup. Also stores the set of inequality relationships.
-  class PropertySet {
-    /// Returns true if V1 is a better choice than V2.
-    bool compare(Value *V1, Value *V2) const {
-      if (isa<Constant>(V1)) {
-        if (!isa<Constant>(V2)) {
-          return true;
+  template <typename C>
+  void InequalityGraph::mergeNodes(Node *N, C &Kill, Value *NewCanonical) {
+    materialize();
+
+    // Merge the relationships from the members of Kill into N.
+    for (typename C::iterator KI = Kill.begin(), KE = Kill.end();
+         KI != KE; ++KI) {
+
+     for (Node::iterator I = (*KI)->begin(), E = (*KI)->end(); I != E; ++I) {
+       if (I->first == N) continue;
+
+        Node::iterator NI = N->find(I->first);
+        if (NI == N->end()) {
+          N->Relations.push_back(std::make_pair(I->first, I->second));
+        } else {
+          unsigned char LV = NI->second & I->second;
+          if (LV == EQ_BIT) {
+
+           assert(std::find(Kill.begin(), Kill.end(), I->first) != Kill.end()
+                   && "Lost EQ property.");
+            N->erase(NI);
+          } else {
+            NI->second = static_cast<LatticeVal>(LV);
+            assert(InequalityGraph::validPredicate(NI->second) &&
+                   "Invalid union of lattice values.");
+          }
         }
-      } else if (isa<Argument>(V1)) {
-        if (!isa<Constant>(V2) && !isa<Argument>(V2)) {
-          return true;
+
+        // All edges are reciprocal; every Node that Kill points to also
+        // contains a pointer to Kill. Replace those with pointers with N.
+        unsigned iter = I->first->findIndex(*KI);
+        assert(iter != (unsigned)-1 && "Edge not reciprocal.");
+        I->first->assign(N, (I->first->begin()+iter)->second);
+        I->first->erase(I->first->begin()+iter);
+      }
+
+      // Removing references from N to Kill.
+      Node::iterator I = N->find(*KI);
+      if (I != N->end()) {
+        N->erase(I); // breaks reciprocity until Kill is deleted.
+      }
+    }
+
+    N->setValue(NewCanonical);
+
+    // Update value mapping to point to the merged node.
+    for (NodeMapType::iterator I = Nodes.begin(), E = Nodes.end();
+         I != E; ++I) {
+      if (std::find(Kill.begin(), Kill.end(), I->second) != Kill.end())
+        I->second = N;
+    }
+
+    for (typename C::iterator KI = Kill.begin(), KE = Kill.end();
+         KI != KE; ++KI) {
+      delete *KI;
+    }
+  }
+
+  void InequalityGraph::materialize() {
+    if (!ConcreteIG) return;
+    const InequalityGraph *IG = ConcreteIG;
+    ConcreteIG = NULL;
+
+    for (NodeMapType::const_iterator I = IG->Nodes.begin(),
+         E = IG->Nodes.end(); I != E; ++I) {
+      if (I->first == I->second->getValue()) {
+        Node *N = newNode(I->first);
+        N->Relations.reserve(N->Relations.size());
+      }
+    }
+    for (NodeMapType::const_iterator I = IG->Nodes.begin(),
+         E = IG->Nodes.end(); I != E; ++I) {
+      if (I->first != I->second->getValue()) {
+        Nodes[I->first] = getNode(I->second->getValue());
+      } else {
+        Node *Old = I->second;
+        Node *N = getNode(I->first);
+        for (Node::const_iterator NI = Old->begin(), NE = Old->end();
+             NI != NE; ++NI) {
+          N->assign(getNode(NI->first->getValue()), NI->second);
         }
       }
-      if (Instruction *I1 = dyn_cast<Instruction>(V1)) {
-        if (Instruction *I2 = dyn_cast<Instruction>(V2)) {
-          BasicBlock *BB1 = I1->getParent(),
-                     *BB2 = I2->getParent();
-          if (BB1 == BB2) {
-            for (BasicBlock::const_iterator I = BB1->begin(), E = BB1->end();
-                 I != E; ++I) {
-              if (&*I == I1) return true;
-              if (&*I == I2) return false;
-            }
-            assert(0 && "Instructions not found in parent BasicBlock?");
-          } else
-            return DT->getNode(BB1)->properlyDominates(DT->getNode(BB2));
+    }
+  }
+
+  /// VRPSolver keeps track of how changes to one variable affect other
+  /// variables, and forwards changes along to the InequalityGraph. It
+  /// also maintains the correct choice for "canonical" in the IG.
+  /// @brief VRPSolver calculates inferences from a new relationship.
+  class VISIBILITY_HIDDEN VRPSolver {
+  private:
+    std::deque<Instruction *> WorkList;
+
+    InequalityGraph &IG;
+    const InequalityGraph &cIG;
+    ETForest *Forest;
+    ETNode *Top;
+
+    typedef InequalityGraph::Node Node;
+
+    /// Returns true if V1 is a better canonical value than V2.
+    bool compare(Value *V1, Value *V2) const {
+      if (isa<Constant>(V1))
+        return !isa<Constant>(V2);
+      else if (isa<Constant>(V2))
+        return false;
+      else if (isa<Argument>(V1))
+        return !isa<Argument>(V2);
+      else if (isa<Argument>(V2))
+        return false;
+
+      Instruction *I1 = dyn_cast<Instruction>(V1);
+      Instruction *I2 = dyn_cast<Instruction>(V2);
+
+      if (!I1 || !I2) return false;
+
+      BasicBlock *BB1 = I1->getParent(),
+                 *BB2 = I2->getParent();
+      if (BB1 == BB2) {
+        for (BasicBlock::const_iterator I = BB1->begin(), E = BB1->end();
+             I != E; ++I) {
+          if (&*I == I1) return true;
+          if (&*I == I2) return false;
         }
+        assert(!"Instructions not found in parent BasicBlock?");
+      } else {
+        return Forest->properlyDominates(BB1, BB2);
       }
       return false;
     }
 
-    struct Property;
-  public:
-    /// Choose the canonical Value in a synonym set.
-    /// Leaves the more canonical choice in V1.
-    void order(Value *&V1, Value *&V2) const {
-      if (compare(V2, V1)) std::swap(V1, V2);
+    void addToWorklist(Instruction *I) {
+      //DEBUG(std::cerr << "addToWorklist: " << *I << "\n");
+
+      if (!isa<BinaryOperator>(I) && !isa<SelectInst>(I)) return;
+
+      const Type *Ty = I->getType();
+      if (Ty == Type::VoidTy || Ty->isFPOrFPVector()) return;
+
+      if (isInstructionTriviallyDead(I)) return;
+
+      WorkList.push_back(I);
     }
 
-    PropertySet(DominatorTree *DT) : union_find(this), DT(DT) {}
+    void addRecursive(Value *V) {
+      //DEBUG(std::cerr << "addRecursive: " << *V << "\n");
 
-    Synonyms<Value *> union_find;
+      Instruction *I = dyn_cast<Instruction>(V);
+      if (I)
+        addToWorklist(I);
+      else if (!isa<Argument>(V))
+        return;
+
+      //DEBUG(std::cerr << "addRecursive uses...\n");
+      for (Value::use_iterator UI = V->use_begin(), UE = V->use_end();
+           UI != UE; ++UI) {
+        // Use must be either be dominated by Top, or dominate Top.
+        if (Instruction *Inst = dyn_cast<Instruction>(*UI)) {
+          ETNode *INode = Forest->getNodeForBlock(Inst->getParent());
+          if (INode->DominatedBy(Top) || Top->DominatedBy(INode))
+            addToWorklist(Inst);
+        }
+      }
 
-    typedef std::vector<Property>::iterator       PropertyIterator;
-    typedef std::vector<Property>::const_iterator ConstPropertyIterator;
-    typedef Synonyms<Value *>::iterator  SynonymIterator;
+      if (I) {
+        //DEBUG(std::cerr << "addRecursive ops...\n");
+        for (User::op_iterator OI = I->op_begin(), OE = I->op_end();
+             OI != OE; ++OI) {
+          if (Instruction *Inst = dyn_cast<Instruction>(*OI))
+            addToWorklist(Inst);
+        }
+      }
+      //DEBUG(std::cerr << "exit addRecursive (" << *V << ").\n");
+    }
 
-    enum Ops {
-      EQ,
-      NE
-    };
+  public:
+    VRPSolver(InequalityGraph &IG, ETForest *Forest, BasicBlock *TopBB)
+      : IG(IG), cIG(IG), Forest(Forest), Top(Forest->getNodeForBlock(TopBB)) {}
 
-    Value *canonicalize(Value *V) const {
-      Value *C = lookup(V);
-      return C ? C : V;
+    bool isEqual(Value *V1, Value *V2) const {
+      if (V1 == V2) return true;
+      if (const Node *N1 = cIG.getNode(V1))
+        return N1 == cIG.getNode(V2);
+      return false;
     }
 
-    Value *lookup(Value *V) const {
-      SynonymIterator SI = union_find.findLeader(V);
-      if (!SI) return NULL;
-      return union_find.getLeader(SI);
+    bool isNotEqual(Value *V1, Value *V2) const {
+      if (V1 == V2) return false;
+      if (const Node *N1 = cIG.getNode(V1))
+        if (const Node *N2 = cIG.getNode(V2))
+          return cIG.isNotEqual(N1, N2);
+      return false;
     }
 
-    bool empty() const {
-      return union_find.empty();
+    bool isLess(Value *V1, Value *V2) const {
+      if (V1 == V2) return false;
+      if (const Node *N1 = cIG.getNode(V1))
+        if (const Node *N2 = cIG.getNode(V2))
+          return cIG.isLess(N1, N2);
+      return false;
     }
 
-    void remove(Value *V) {
-      SynonymIterator I = union_find.findLeader(V);
-      if (!I) return;
+    bool isLessEqual(Value *V1, Value *V2) const {
+      if (V1 == V2) return true;
+      if (const Node *N1 = cIG.getNode(V1))
+        if (const Node *N2 = cIG.getNode(V2))
+          return cIG.isLessEqual(N1, N2);
+      return false;
+    }
 
-      union_find.remove(V);
+    bool isGreater(Value *V1, Value *V2) const {
+      if (V1 == V2) return false;
+      if (const Node *N1 = cIG.getNode(V1))
+        if (const Node *N2 = cIG.getNode(V2))
+          return cIG.isGreater(N1, N2);
+      return false;
+    }
 
-      for (PropertyIterator PI = Properties.begin(), PE = Properties.end();
-           PI != PE;) {
-        Property &P = *PI++;
-        if (P.I1 == I || P.I2 == I) Properties.erase(PI);
-      }
+    bool isGreaterEqual(Value *V1, Value *V2) const {
+      if (V1 == V2) return true;
+      if (const Node *N1 = IG.getNode(V1))
+        if (const Node *N2 = IG.getNode(V2))
+          return cIG.isGreaterEqual(N1, N2);
+      return false;
     }
 
-    void addEqual(Value *V1, Value *V2) {
-      // If %x = 0. and %y = -0., seteq %x, %y is true, but
-      // copysign(%x) is not the same as copysign(%y).
-      if (V1->getType()->isFloatingPoint()) return;
+    // All of the add* functions return true if the InequalityGraph represents
+    // the property, and false if there is a logical contradiction. On false,
+    // you may no longer perform any queries on the InequalityGraph.
+
+    bool addEqual(Value *V1, Value *V2) {
+      //DEBUG(std::cerr << "addEqual(" << *V1 << ", "
+      //                               << *V2 << ")\n");
+      if (isEqual(V1, V2)) return true;
+
+      const Node *cN1 = cIG.getNode(V1), *cN2 = cIG.getNode(V2);
+
+      if (cN1 && cN2 && cIG.isNotEqual(cN1, cN2))
+          return false;
+
+      if (compare(V2, V1)) { std::swap(V1, V2); std::swap(cN1, cN2); }
+
+      if (cN1) {
+        if (ConstantBool *CB = dyn_cast<ConstantBool>(V1)) {
+          Node *N1 = IG.getNode(V1);
+           
+          // When "addEqual" is performed and the new value is a ConstantBool,
+          // iterate through the NE set and fix them up to be EQ of the
+          // opposite bool.
+
+          for (Node::iterator I = N1->begin(), E = N1->end(); I != E; ++I)
+            if ((I->second & 1) == 0) {
+              assert(N1 != I->first && "Node related to itself?");
+              addEqual(I->first->getValue(),
+                       ConstantBool::get(!CB->getValue()));
+            }
+        }
+      }
+
+      if (!cN2) {
+        if (Instruction *I2 = dyn_cast<Instruction>(V2)) {
+          ETNode *Node_I2 = Forest->getNodeForBlock(I2->getParent());
+          if (Top != Node_I2 && Node_I2->DominatedBy(Top)) {
+            Value *V = V1;
+            if (cN1 && compare(V1, cN1->getValue())) V = cN1->getValue();
+            //DEBUG(std::cerr << "Simply removing " << *I2
+            //                << ", replacing with " << *V << "\n");
+            I2->replaceAllUsesWith(V);
+            // leave it dead; it'll get erased later.
+            ++NumSimple;
+            addRecursive(V1);
+            return true;
+          }
+        }
+      }
 
-      order(V1, V2);
-      if (isa<Constant>(V2)) return; // refuse to set false == true.
+      Node *N1 = IG.getNode(V1), *N2 = IG.getNode(V2);
 
-      if (union_find.findLeader(V1) &&
-          union_find.findLeader(V1) == union_find.findLeader(V2))
-        return; // no-op
+      if ( N1 && !N2) {
+        IG.addEqual(N1, V2);
+        if (compare(V1, N1->getValue())) N1->setValue(V1);
+      }
+      if (!N1 &&  N2) {
+        IG.addEqual(N2, V1);
+        if (compare(V1, N2->getValue())) N2->setValue(V1);
+      }
+      if ( N1 &&  N2) {
+        // Suppose we're being told that %x == %y, and %x <= %z and %y >= %z.
+        // We can't just merge %x and %y because the relationship with %z would
+        // be EQ and that's invalid; they need to be the same Node.
+        //
+        // What we're doing is looking for any chain of nodes reaching %z such
+        // that %x <= %z and %y >= %z, and vice versa. The cool part is that
+        // every node in between is also equal because of the squeeze principle.
+
+        std::vector<Node *> N1_GE, N2_LE, N1_LE, N2_GE;
+        IG.transitiveClosure(N1, InequalityGraph::GE, back_inserter(N1_GE));
+        std::sort(N1_GE.begin(), N1_GE.end());
+        N1_GE.erase(std::unique(N1_GE.begin(), N1_GE.end()), N1_GE.end());
+        IG.transitiveClosure(N2, InequalityGraph::LE, back_inserter(N2_LE));
+        std::sort(N1_LE.begin(), N1_LE.end());
+        N1_LE.erase(std::unique(N1_LE.begin(), N1_LE.end()), N1_LE.end());
+        IG.transitiveClosure(N1, InequalityGraph::LE, back_inserter(N1_LE));
+        std::sort(N2_GE.begin(), N2_GE.end());
+        N2_GE.erase(std::unique(N2_GE.begin(), N2_GE.end()), N2_GE.end());
+        std::unique(N2_GE.begin(), N2_GE.end());
+        IG.transitiveClosure(N2, InequalityGraph::GE, back_inserter(N2_GE));
+        std::sort(N2_LE.begin(), N2_LE.end());
+        N2_LE.erase(std::unique(N2_LE.begin(), N2_LE.end()), N2_LE.end());
+
+        std::vector<Node *> Set1, Set2;
+        std::set_intersection(N1_GE.begin(), N1_GE.end(),
+                              N2_LE.begin(), N2_LE.end(),
+                              back_inserter(Set1));
+        std::set_intersection(N1_LE.begin(), N1_LE.end(),
+                              N2_GE.begin(), N2_GE.end(),
+                              back_inserter(Set2));
+
+        std::vector<Node *> Equal;
+        std::set_union(Set1.begin(), Set1.end(), Set2.begin(), Set2.end(),
+                       back_inserter(Equal));
 
-      SynonymIterator deleted = union_find.unionSets(V1, V2);
-      if (deleted) {
-        SynonymIterator replacement = union_find.findLeader(V1);
-        // Move Properties
-        for (PropertyIterator I = Properties.begin(), E = Properties.end();
+        Value *Best = N1->getValue();
+        if (compare(N2->getValue(), Best)) Best = N2->getValue();
+
+        for (std::vector<Node *>::iterator I = Equal.begin(), E = Equal.end();
              I != E; ++I) {
-          if (I->I1 == deleted) I->I1 = replacement;
-          else if (I->I1 > deleted) --I->I1;
-          if (I->I2 == deleted) I->I2 = replacement;
-          else if (I->I2 > deleted) --I->I2;
+          Value *V = (*I)->getValue();
+          if (compare(V, Best)) Best = V;
         }
+
+        Equal.push_back(N2);
+        IG.mergeNodes(N1, Equal, Best);
       }
-      addImpliedProperties(EQ, V1, V2);
+      if (!N1 && !N2) IG.addEqual(IG.newNode(V1), V2);
+
+      addRecursive(V1);
+      addRecursive(V2);
+
+      return true;
     }
 
-    void addNotEqual(Value *V1, Value *V2) {
-      // If %x = NAN then seteq %x, %x is false.
-      if (V1->getType()->isFloatingPoint()) return;
+    bool addNotEqual(Value *V1, Value *V2) {
+      //DEBUG(std::cerr << "addNotEqual(" << *V1 << ", "
+      //                                  << *V2 << ")\n");
+      if (isNotEqual(V1, V2)) return true;
 
-      // For example, %x = setne int 0, 0 causes "0 != 0".
-      if (isa<Constant>(V1) && isa<Constant>(V2)) return;
+      // Never permit %x NE true/false.
+      if (ConstantBool *B1 = dyn_cast<ConstantBool>(V1)) {
+        return addEqual(ConstantBool::get(!B1->getValue()), V2);
+      } else if (ConstantBool *B2 = dyn_cast<ConstantBool>(V2)) {
+        return addEqual(V1, ConstantBool::get(!B2->getValue()));
+      }
 
-      if (findProperty(NE, V1, V2) != Properties.end())
-        return; // no-op.
+      Node *N1 = IG.getOrInsertNode(V1),
+           *N2 = IG.getOrInsertNode(V2);
 
-      // Add the property.
-      SynonymIterator I1 = union_find.findOrInsert(V1),
-                      I2 = union_find.findOrInsert(V2);
+      if (N1 == N2) return false;
 
-      // Technically this means that the block is unreachable.
-      if (I1 == I2) return;
+      IG.addNotEqual(N1, N2);
 
-      Properties.push_back(Property(NE, I1, I2));
-      addImpliedProperties(NE, V1, V2);
+      addRecursive(V1);
+      addRecursive(V2);
+
+      return true;
     }
 
-    PropertyIterator findProperty(Ops Opcode, Value *V1, Value *V2) {
-      assert(Opcode != EQ && "Can't findProperty on EQ."
-             "Use the lookup method instead.");
+    /// Set V1 less than V2.
+    bool addLess(Value *V1, Value *V2) {
+      if (isLess(V1, V2)) return true;
+      if (isGreaterEqual(V1, V2)) return false;
 
-      SynonymIterator I1 = union_find.findLeader(V1),
-                      I2 = union_find.findLeader(V2);
-      if (!I1 || !I2) return Properties.end();
+      Node *N1 = IG.getOrInsertNode(V1), *N2 = IG.getOrInsertNode(V2);
 
-      return
-      find(Properties.begin(), Properties.end(), Property(Opcode, I1, I2));
-    }
+      if (N1 == N2) return false;
 
-    ConstPropertyIterator
-    findProperty(Ops Opcode, Value *V1, Value *V2) const {
-      assert(Opcode != EQ && "Can't findProperty on EQ."
-             "Use the lookup method instead.");
+      IG.addLess(N1, N2);
 
-      SynonymIterator I1 = union_find.findLeader(V1),
-                      I2 = union_find.findLeader(V2);
-      if (!I1 || !I2) return Properties.end();
+      addRecursive(V1);
+      addRecursive(V2);
 
-      return
-      find(Properties.begin(), Properties.end(), Property(Opcode, I1, I2));
+      return true;
     }
 
-  private:
-    // Represents Head OP [Tail1, Tail2, ...]
-    // For example: %x != %a, %x != %b.
-    struct VISIBILITY_HIDDEN Property {
-      typedef SynonymIterator Iter;
-
-      Property(Ops opcode, Iter i1, Iter i2)
-        : Opcode(opcode), I1(i1), I2(i2)
-      { assert(opcode != EQ && "Equality belongs in the synonym set, "
-                               "not a property."); }
-
-      bool operator==(const Property &P) const {
-        return (Opcode == P.Opcode) &&
-               ((I1 == P.I1 && I2 == P.I2) ||
-                (I1 == P.I2 && I2 == P.I1));
-      }
+    /// Set V1 less than or equal to V2.
+    bool addLessEqual(Value *V1, Value *V2) {
+      if (isLessEqual(V1, V2)) return true;
+      if (V1 == V2) return true;
 
-      Ops Opcode;
-      Iter I1, I2;
-    };
+      if (isLessEqual(V2, V1))
+        return addEqual(V1, V2);
 
-    void addToResolve(Value *V, std::list<Value *> &WorkList) {
-      if (!isa<Constant>(V) && !isa<BasicBlock>(V)) {
-        for (Value::use_iterator UI = V->use_begin(), UE = V->use_end();
-             UI != UE; ++UI) {
-          if (!isa<Constant>(*UI) && !isa<BasicBlock>(*UI)) {
-            WorkList.push_back(*UI);
-          }
-        }
-      }
+      if (isGreater(V1, V2)) return false;
+
+      Node *N1 = IG.getOrInsertNode(V1),
+           *N2 = IG.getOrInsertNode(V2);
+
+      if (N1 == N2) return true;
+
+      IG.addLessEqual(N1, N2);
+
+      addRecursive(V1);
+      addRecursive(V2);
+
+      return true;
     }
 
-    void resolve(std::list<Value *> &WorkList) {
-      if (WorkList.empty()) return;
+    void solve() {
+      DEBUG(std::cerr << "WorkList entry, size: " << WorkList.size() << "\n");
+      while (!WorkList.empty()) {
+        DEBUG(std::cerr << "WorkList size: " << WorkList.size() << "\n");
 
-      Value *V = WorkList.front();
-      WorkList.pop_front();
+        Instruction *I = WorkList.front();
+        WorkList.pop_front();
 
-      if (empty()) return;
+        Value *Canonical = cIG.canonicalize(I);
+        const Type *Ty = I->getType();
 
-      Instruction *I = dyn_cast<Instruction>(V);
-      if (!I) return;
+        //DEBUG(std::cerr << "solving: " << *I << "\n");
+        //DEBUG(IG.debug(std::cerr));
 
-      if (BinaryOperator *BO = dyn_cast<BinaryOperator>(I)) {
-        Value *lhs = canonicalize(BO->getOperand(0)),
-              *rhs = canonicalize(BO->getOperand(1));
-
-        ConstantIntegral *CI1 = dyn_cast<ConstantIntegral>(lhs),
-                         *CI2 = dyn_cast<ConstantIntegral>(rhs);
-
-        if (CI1 && CI2) {
-          addToResolve(BO, WorkList);
-          addEqual(BO, ConstantExpr::get(BO->getOpcode(), CI1, CI2));
-        } else if (SetCondInst *SCI = dyn_cast<SetCondInst>(BO)) {
-          PropertySet::ConstPropertyIterator NE =
-             findProperty(PropertySet::NE, lhs, rhs);
+        if (BinaryOperator *BO = dyn_cast<BinaryOperator>(I)) {
+          Value *Op0 = cIG.canonicalize(BO->getOperand(0)),
+                *Op1 = cIG.canonicalize(BO->getOperand(1));
 
-          if (NE != Properties.end()) {
-            switch (SCI->getOpcode()) {
+          ConstantIntegral *CI1 = dyn_cast<ConstantIntegral>(Op0),
+                           *CI2 = dyn_cast<ConstantIntegral>(Op1);
+
+          if (CI1 && CI2)
+            addEqual(BO, ConstantExpr::get(BO->getOpcode(), CI1, CI2));
+
+          switch (BO->getOpcode()) {
             case Instruction::SetEQ:
-              addToResolve(SCI, WorkList);
-              addEqual(SCI, ConstantBool::getFalse());
+              // "seteq int %a, %b" EQ true  then %a EQ %b
+              // "seteq int %a, %b" EQ false then %a NE %b
+              if (Canonical == ConstantBool::getTrue())
+                addEqual(Op0, Op1);
+              else if (Canonical == ConstantBool::getFalse())
+                addNotEqual(Op0, Op1);
+
+              // %a EQ %b then "seteq int %a, %b" EQ true
+              // %a NE %b then "seteq int %a, %b" EQ false
+              if (isEqual(Op0, Op1))
+                addEqual(BO, ConstantBool::getTrue());
+              else if (isNotEqual(Op0, Op1))
+                addEqual(BO, ConstantBool::getFalse());
+
               break;
             case Instruction::SetNE:
-              addToResolve(SCI, WorkList);
-              addEqual(SCI, ConstantBool::getTrue());
+              // "setne int %a, %b" EQ true  then %a NE %b
+              // "setne int %a, %b" EQ false then %a EQ %b
+              if (Canonical == ConstantBool::getTrue())
+                addNotEqual(Op0, Op1);
+              else if (Canonical == ConstantBool::getFalse())
+                addEqual(Op0, Op1);
+
+              // %a EQ %b then "setne int %a, %b" EQ false
+              // %a NE %b then "setne int %a, %b" EQ true
+              if (isEqual(Op0, Op1))
+                addEqual(BO, ConstantBool::getFalse());
+              else if (isNotEqual(Op0, Op1))
+                addEqual(BO, ConstantBool::getTrue());
+
               break;
-            case Instruction::SetLE:
-            case Instruction::SetGE:
             case Instruction::SetLT:
+              // "setlt int %a, %b" EQ true  then %a LT %b
+              // "setlt int %a, %b" EQ false then %b LE %a
+              if (Canonical == ConstantBool::getTrue())
+                addLess(Op0, Op1);
+              else if (Canonical == ConstantBool::getFalse())
+                addLessEqual(Op1, Op0);
+
+              // %a LT %b then "setlt int %a, %b" EQ true
+              // %a GE %b then "setlt int %a, %b" EQ false
+              if (isLess(Op0, Op1))
+                addEqual(BO, ConstantBool::getTrue());
+              else if (isGreaterEqual(Op0, Op1))
+                addEqual(BO, ConstantBool::getFalse());
+
+              break;
+            case Instruction::SetLE:
+              // "setle int %a, %b" EQ true  then %a LE %b
+              // "setle int %a, %b" EQ false then %b LT %a
+              if (Canonical == ConstantBool::getTrue())
+                addLessEqual(Op0, Op1);
+              else if (Canonical == ConstantBool::getFalse())
+                addLess(Op1, Op0);
+
+              // %a LE %b then "setle int %a, %b" EQ true
+              // %a GT %b then "setle int %a, %b" EQ false
+              if (isLessEqual(Op0, Op1))
+                addEqual(BO, ConstantBool::getTrue());
+              else if (isGreater(Op0, Op1))
+                addEqual(BO, ConstantBool::getFalse());
+
+              break;
             case Instruction::SetGT:
+              // "setgt int %a, %b" EQ true  then %b LT %a
+              // "setgt int %a, %b" EQ false then %a LE %b
+              if (Canonical == ConstantBool::getTrue())
+                addLess(Op1, Op0);
+              else if (Canonical == ConstantBool::getFalse())
+                addLessEqual(Op0, Op1);
+
+              // %a GT %b then "setgt int %a, %b" EQ true
+              // %a LE %b then "setgt int %a, %b" EQ false
+              if (isGreater(Op0, Op1))
+                addEqual(BO, ConstantBool::getTrue());
+              else if (isLessEqual(Op0, Op1))
+                addEqual(BO, ConstantBool::getFalse());
+
+              break;
+            case Instruction::SetGE:
+              // "setge int %a, %b" EQ true  then %b LE %a
+              // "setge int %a, %b" EQ false then %a LT %b
+              if (Canonical == ConstantBool::getTrue())
+                addLessEqual(Op1, Op0);
+              else if (Canonical == ConstantBool::getFalse())
+                addLess(Op0, Op1);
+
+              // %a GE %b then "setge int %a, %b" EQ true
+              // %a LT %b then "setlt int %a, %b" EQ false
+              if (isGreaterEqual(Op0, Op1))
+                addEqual(BO, ConstantBool::getTrue());
+              else if (isLess(Op0, Op1))
+                addEqual(BO, ConstantBool::getFalse());
+
               break;
+            case Instruction::And: {
+              // "and int %a, %b"  EQ -1   then %a EQ -1   and %b EQ -1
+              // "and bool %a, %b" EQ true then %a EQ true and %b EQ true
+              ConstantIntegral *CI = ConstantIntegral::getAllOnesValue(Ty);
+              if (Canonical == CI) {
+                addEqual(CI, Op0);
+                addEqual(CI, Op1);
+              }
+            } break;
+            case Instruction::Or: {
+              // "or int %a, %b"  EQ 0     then %a EQ 0     and %b EQ 0
+              // "or bool %a, %b" EQ false then %a EQ false and %b EQ false
+              Constant *Zero = Constant::getNullValue(Ty);
+              if (Canonical == Zero) {
+                addEqual(Zero, Op0);
+                addEqual(Zero, Op1);
+              }
+            } break;
+            case Instruction::Xor: {
+              // "xor bool true,  %a" EQ true  then %a EQ false
+              // "xor bool true,  %a" EQ false then %a EQ true
+              // "xor bool false, %a" EQ true  then %a EQ true
+              // "xor bool false, %a" EQ false then %a EQ false
+              // "xor int %c, %a" EQ %c then %a EQ 0
+              // "xor int %c, %a" NE %c then %a NE 0
+              // 1. Repeat all of the above, with order of operands reversed.
+              Value *LHS = Op0, *RHS = Op1;
+              if (!isa<Constant>(LHS)) std::swap(LHS, RHS);
+
+              if (ConstantBool *CB = dyn_cast<ConstantBool>(Canonical)) {
+                if (ConstantBool *A = dyn_cast<ConstantBool>(LHS))
+                  addEqual(RHS, ConstantBool::get(A->getValue() ^
+                                                  CB->getValue()));
+              }
+              if (Canonical == LHS) {
+                if (isa<ConstantIntegral>(Canonical))
+                  addEqual(RHS, Constant::getNullValue(Ty));
+              } else if (isNotEqual(LHS, Canonical)) {
+                addNotEqual(RHS, Constant::getNullValue(Ty));
+              }
+            } break;
             default:
-              assert(0 && "Unknown opcode in SetCondInst.");
               break;
-            }
           }
-        }
-      } else if (SelectInst *SI = dyn_cast<SelectInst>(I)) {
-        Value *Condition = canonicalize(SI->getCondition());
-        if (ConstantBool *CB = dyn_cast<ConstantBool>(Condition)) {
-          addToResolve(SI, WorkList);
-          addEqual(SI, CB->getValue() ? SI->getTrueValue() : SI->getFalseValue());
-        }
-      }
-      if (!WorkList.empty()) resolve(WorkList);
-    }
-
-    void add(Ops Opcode, Value *V1, Value *V2, bool invert) {
-      switch (Opcode) {
-        case EQ:
-          if (invert) addNotEqual(V1, V2);
-          else        addEqual(V1, V2);
-          break;
-        case NE:
-          if (invert) addEqual(V1, V2);
-          else        addNotEqual(V1, V2);
-          break;
-        default:
-          assert(0 && "Unknown property opcode.");
-      }
-    }
-
-    /// Finds the properties implied by an equivalence and adds them too.
-    /// Example: ("seteq %a, %b", true,  EQ) --> (%a, %b, EQ)
-    ///          ("seteq %a, %b", false, EQ) --> (%a, %b, NE)
-    void addImpliedProperties(Ops Opcode, Value *V1, Value *V2) {
-      order(V1, V2);
-
-      if (BinaryOperator *BO = dyn_cast<BinaryOperator>(V2)) {
-        switch (BO->getOpcode()) {
-        case Instruction::SetEQ:
-          // "seteq int %a, %b" EQ true  then %a EQ %b
-          // "seteq int %a, %b" EQ false then %a NE %b
-          // "seteq int %a, %b" NE true  then %a NE %b
-          // "seteq int %a, %b" NE false then %a EQ %b
-          if (ConstantBool *V1CB = dyn_cast<ConstantBool>(V1))
-            add(Opcode, BO->getOperand(0), BO->getOperand(1),!V1CB->getValue());
-          break;
-        case Instruction::SetNE:
-          // "setne int %a, %b" EQ true  then %a NE %b
-          // "setne int %a, %b" EQ false then %a EQ %b
-          // "setne int %a, %b" NE true  then %a EQ %b
-          // "setne int %a, %b" NE false then %a NE %b
-          if (ConstantBool *V1CB = dyn_cast<ConstantBool>(V1))
-            add(Opcode, BO->getOperand(0), BO->getOperand(1), V1CB->getValue());
-          break;
-        case Instruction::SetLT:
-        case Instruction::SetGT:
-          // "setlt/gt int %a, %b" EQ true  then %a NE %b
-          // "setlt/gt int %a, %b" NE false then %a NE %b
-
-          if (ConstantBool *CB = dyn_cast<ConstantBool>(V1)) {
-            if (CB->getValue() ^ (Opcode==NE))
-              addNotEqual(BO->getOperand(0), BO->getOperand(1));
-	  }
-          break;
-        case Instruction::SetLE:
-        case Instruction::SetGE:
-          // "setle/ge int %a, %b" EQ false then %a NE %b
-          // "setle/ge int %a, %b" NE true  then %a NE %b
-          if (ConstantBool *CB = dyn_cast<ConstantBool>(V1)) {
-            if (CB->getValue() ^ (Opcode==EQ))
-              addNotEqual(BO->getOperand(0), BO->getOperand(1));
-	  }
-          break;
-        case Instruction::And: {
-          // "and int %a, %b"  EQ 0xff  then %a EQ 0xff and %b EQ 0xff
-          // "and bool %a, %b" EQ true  then %a EQ true and %b EQ true
-          // "and bool %a, %b" NE false then %a EQ true and %b EQ true
-          if (ConstantIntegral *CI = dyn_cast<ConstantIntegral>(V1)) {
-            if (Opcode == EQ && CI->isAllOnesValue()) {
-              addEqual(CI, BO->getOperand(0));
-              addEqual(CI, BO->getOperand(1));
-            } else if (Opcode == NE && CI == ConstantBool::getFalse()) {
-              addEqual(ConstantBool::getTrue(), BO->getOperand(0));
-              addEqual(ConstantBool::getTrue(), BO->getOperand(1));
-            }
-          }
-        } break;
-        case Instruction::Or: {
-          // "or int %a, %b"  EQ 0     then %a EQ 0     and %b EQ 0
-          // "or bool %a, %b" EQ false then %a EQ false and %b EQ false
-          // "or bool %a, %b" NE true  then %a EQ false and %b EQ false
-          if (ConstantIntegral *CI = dyn_cast<ConstantIntegral>(V1)) {
-            if (Opcode == EQ && CI->isNullValue()) {
-              addEqual(CI, BO->getOperand(0));
-              addEqual(CI, BO->getOperand(1));
-            } else if (Opcode == NE && CI == ConstantBool::getTrue()) {
-              addEqual(ConstantBool::getFalse(), BO->getOperand(0));
-              addEqual(ConstantBool::getFalse(), BO->getOperand(1));
-            }
-          }
-        } break;
-        case Instruction::Xor: {
-          // "xor bool true,  %a" EQ true  then %a = false
-          // "xor bool true,  %a" EQ false then %a = true
-          // "xor bool false, %a" EQ true  then %a = true
-          // "xor bool false, %a" EQ false then %a = false
-          // 1. Repeat all of the above, with "NE false" in place of
-          //    "EQ true" and "NE true" in place of "EQ false".
-          // "xor int %c, %a" EQ %c then %a = 0
-          // "xor int %c, %a" NE %c then %a != 0
-          // 2. Repeat all of the above, with order of operands reversed.
-
-          Value *LHS = BO->getOperand(0), *RHS = BO->getOperand(1);
-          if (!isa<Constant>(LHS)) std::swap(LHS, RHS);
-
-          if (ConstantBool *CB = dyn_cast<ConstantBool>(V1)) {
-            if (ConstantBool *A = dyn_cast<ConstantBool>(LHS)) {
-              addEqual(RHS, ConstantBool::get(A->getValue() ^ CB->getValue()
-                                              ^ (Opcode==NE)));
-            }
-          }
-          else if (ConstantIntegral *CI = dyn_cast<ConstantIntegral>(V1)) {
-            if (ConstantIntegral *A = dyn_cast<ConstantIntegral>(LHS)) {
-              if (A == CI)
-                add(Opcode, RHS, Constant::getNullValue(A->getType()), false);
-            }
-          }
-        } break;
-        default:
-          break;
-        }
-      } else if (SelectInst *SI = dyn_cast<SelectInst>(V2)) {
-        ConstantBool *True  = ConstantBool::get(Opcode==EQ),
-                     *False = ConstantBool::get(Opcode!=EQ);
-
-        if (V1 == canonicalize(SI->getTrueValue()))
-          addEqual(SI->getCondition(), True);
-        else if (V1 == canonicalize(SI->getFalseValue()))
-          addEqual(SI->getCondition(), False);
-      }
-
-      std::list<Value *> WorkList;
-      addToResolve(V1, WorkList);
-      addToResolve(V2, WorkList);
-      resolve(WorkList);
-    }
 
-    DominatorTree *DT;
-  public:
-#ifdef DEBUG
-    void debug(std::ostream &os) const {
-      static const char *OpcodeTable[] = { "EQ", "NE" };
+          // "%x = add int %y, %z" and %x EQ %y then %z EQ 0
+          // "%x = mul int %y, %z" and %x EQ %y then %z EQ 1
+          // 1. Repeat all of the above, with order of operands reversed.
+          // "%x = fdiv float %y, %z" and %x EQ %y then %z EQ 1
+          Value *Known = Op0, *Unknown = Op1;
+          if (Known != BO) std::swap(Known, Unknown);
+          if (Known == BO) {
+            switch (BO->getOpcode()) {
+              default: break;
+              case Instruction::Xor:
+              case Instruction::Or:
+              case Instruction::Add:
+              case Instruction::Sub:
+                if (!Ty->isFloatingPoint())
+                  addEqual(Unknown, Constant::getNullValue(Ty));
+                break;
+              case Instruction::UDiv:
+              case Instruction::SDiv:
+              case Instruction::FDiv:
+                if (Unknown == Op0) break; // otherwise, fallthrough
+              case Instruction::And:
+              case Instruction::Mul:
+                Constant *One = NULL;
+                if (isa<ConstantInt>(Unknown))
+                  One = ConstantInt::get(Ty, 1);
+                else if (isa<ConstantFP>(Unknown))
+                  One = ConstantFP::get(Ty, 1);
+                else if (isa<ConstantBool>(Unknown))
+                  One = ConstantBool::getTrue();
 
-      union_find.debug(os);
-      for (std::vector<Property>::const_iterator I = Properties.begin(),
-           E = Properties.end(); I != E; ++I) {
-        os << (*I).I1 << " " << OpcodeTable[(*I).Opcode] << " "
-           << (*I).I2 << "\n";
+                if (One) addEqual(Unknown, One);
+                break;
+            }
+          }
+        } else if (SelectInst *SI = dyn_cast<SelectInst>(I)) {
+          // Given: "%a = select bool %x, int %b, int %c"
+          // %a EQ %b then %x EQ true
+          // %a EQ %c then %x EQ false
+          if (isEqual(I, SI->getTrueValue()) ||
+              isNotEqual(I, SI->getFalseValue()))
+            addEqual(SI->getCondition(), ConstantBool::getTrue());
+          else if (isEqual(I, SI->getFalseValue()) ||
+                   isNotEqual(I, SI->getTrueValue()))
+            addEqual(SI->getCondition(), ConstantBool::getFalse());
+
+          // %x EQ true  then %a EQ %b
+          // %x EQ false then %a NE %b
+          if (isEqual(SI->getCondition(), ConstantBool::getTrue()))
+            addEqual(SI, SI->getTrueValue());
+          else if (isEqual(SI->getCondition(), ConstantBool::getFalse()))
+            addEqual(SI, SI->getFalseValue());
+        }
       }
-      os << "\n";
     }
-#endif
-
-    std::vector<Property> Properties;
   };
 
   /// PredicateSimplifier - This class is a simplifier that replaces
   /// one equivalent variable with another. It also tracks what
   /// can't be equal and will solve setcc instructions when possible.
-  class PredicateSimplifier : public FunctionPass {
+  /// @brief Root of the predicate simplifier optimization.
+  class VISIBILITY_HIDDEN PredicateSimplifier : public FunctionPass {
+    DominatorTree *DT;
+    ETForest *Forest;
+    bool modified;
+
+    class State {
+    public:
+      BasicBlock *ToVisit;
+      InequalityGraph *IG;
+
+      State(BasicBlock *BB, InequalityGraph *IG) : ToVisit(BB), IG(IG) {}
+    };
+
+    std::vector<State> WorkList;
+
   public:
     bool runOnFunction(Function &F);
-    virtual void getAnalysisUsage(AnalysisUsage &AU) const;
+
+    virtual void getAnalysisUsage(AnalysisUsage &AU) const {
+      AU.addRequiredID(BreakCriticalEdgesID);
+      AU.addRequired<DominatorTree>();
+      AU.addRequired<ETForest>();
+      AU.setPreservesCFG();
+      AU.addPreservedID(BreakCriticalEdgesID);
+    }
 
   private:
     /// Forwards - Adds new properties into PropertySet and uses them to
@@ -548,17 +1093,16 @@
     /// a transition from one BasicBlock to another, this will use the
     /// PredicateSimplifier::proceedToSuccessor(s) interface to enter the
     /// basic block with the new PropertySet.
-    class Forwards : public InstVisitor<Forwards> {
+    /// @brief Performs abstract execution of the program.
+    class VISIBILITY_HIDDEN Forwards : public InstVisitor<Forwards> {
       friend class InstVisitor<Forwards>;
       PredicateSimplifier *PS;
-    public:
-      PropertySet &KP;
 
-      Forwards(PredicateSimplifier *PS, PropertySet &KP) : PS(PS), KP(KP) {}
+    public:
+      InequalityGraph &IG;
 
-      // Tries to simplify each Instruction and add new properties to
-      // the PropertySet. Returns true if it erase the instruction.
-      //void visitInstruction(Instruction *I);
+      Forwards(PredicateSimplifier *PS, InequalityGraph &IG)
+        : PS(PS), IG(IG) {}
 
       void visitTerminatorInst(TerminatorInst &TI);
       void visitBranchInst(BranchInst &BI);
@@ -567,236 +1111,223 @@
       void visitAllocaInst(AllocaInst &AI);
       void visitLoadInst(LoadInst &LI);
       void visitStoreInst(StoreInst &SI);
+
       void visitBinaryOperator(BinaryOperator &BO);
     };
 
     // Used by terminator instructions to proceed from the current basic
     // block to the next. Verifies that "current" dominates "next",
     // then calls visitBasicBlock.
-    void proceedToSuccessors(PropertySet &CurrentPS, BasicBlock *Current);
-    void proceedToSuccessor(PropertySet &Properties, BasicBlock *Next);
-
-    // Visits each instruction in the basic block.
-    void visitBasicBlock(BasicBlock *Block, PropertySet &KnownProperties);
-
-    // Tries to simplify each Instruction and add new properties to
-    // the PropertySet.
-    void visitInstruction(Instruction *I, PropertySet &);
-
-    DominatorTree *DT;
-    bool modified;
-  };
-
-  RegisterPass<PredicateSimplifier> X("predsimplify",
-                                      "Predicate Simplifier");
-
-  template <typename ElemTy>
-  typename Synonyms<ElemTy>::iterator
-  Synonyms<ElemTy>::unionSets(ElemTy E1, ElemTy E2) {
-    PS->order(E1, E2);
-
-    iterator I1 = findLeader(E1),
-             I2 = findLeader(E2);
-
-    if (!I1 && !I2) { // neither entry is in yet
-      leaders.push_back(E1);
-      I1 = leaders.size();
-      mapping[E1] = I1;
-      mapping[E2] = I1;
-      return 0;
+    void proceedToSuccessors(const InequalityGraph &IG, BasicBlock *BBCurrent) {
+      DominatorTree::Node *Current = DT->getNode(BBCurrent);
+      for (DominatorTree::Node::iterator I = Current->begin(),
+           E = Current->end(); I != E; ++I) {
+        //visitBasicBlock((*I)->getBlock(), IG);
+        WorkList.push_back(State((*I)->getBlock(), new InequalityGraph(IG)));
+      }
     }
 
-    if (!I1 && I2) {
-      mapping[E1] = I2;
-      std::swap(getLeader(I2), E1);
-      return 0;
+    void proceedToSuccessor(InequalityGraph *NextIG, BasicBlock *Next) {
+      //visitBasicBlock(Next, NextIG);
+      WorkList.push_back(State(Next, NextIG));
     }
 
-    if (I1 && !I2) {
-      mapping[E2] = I1;
-      return 0;
+    // Visits each instruction in the basic block.
+    void visitBasicBlock(BasicBlock *BB, InequalityGraph &IG) {
+     DEBUG(std::cerr << "Entering Basic Block: " << BB->getName() << "\n");
+     for (BasicBlock::iterator I = BB->begin(), E = BB->end(); I != E;) {
+       visitInstruction(I++, IG);
+      }
     }
 
-    if (I1 == I2) return 0;
+    // Tries to simplify each Instruction and add new properties to
+    // the PropertySet.
+    void visitInstruction(Instruction *I, InequalityGraph &IG) {
+      DEBUG(std::cerr << "Considering instruction " << *I << "\n");
+      DEBUG(IG.debug(std::cerr));
+
+      // Sometimes instructions are made dead due to earlier analysis.
+      if (isInstructionTriviallyDead(I)) {
+        I->eraseFromParent();
+        return;
+      }
 
-    // This is the case where we have two sets, [%a1, %a2, %a3] and
-    // [%p1, %p2, %p3] and someone says that %a2 == %p3. We need to
-    // combine the two synsets.
+      // Try to replace the whole instruction.
+      Value *V = IG.canonicalize(I);
+      if (V != I) {
+        modified = true;
+        ++NumInstruction;
+        DEBUG(std::cerr << "Removing " << *I << ", replacing with "
+                        << *V << "\n");
+        IG.remove(I);
+        I->replaceAllUsesWith(V);
+        I->eraseFromParent();
+        return;
+      }
 
-    if (I1 > I2) --I1;
+      // Try to substitute operands.
+      for (unsigned i = 0, e = I->getNumOperands(); i != e; ++i) {
+        Value *Oper = I->getOperand(i);
+        Value *V = IG.canonicalize(Oper);
+        if (V != Oper) {
+          modified = true;
+          ++NumVarsReplaced;
+          DEBUG(std::cerr << "Resolving " << *I);
+          I->setOperand(i, V);
+          DEBUG(std::cerr << " into " << *I);
+        }
+      }
 
-    for (std::map<Value *, unsigned>::iterator I = mapping.begin(),
-         E = mapping.end(); I != E; ++I) {
-      if (I->second == I2) I->second = I1;
-      else if (I->second > I2) --I->second;
+      //DEBUG(std::cerr << "push (%" << I->getParent()->getName() << ")\n");
+      Forwards visit(this, IG);
+      visit.visit(*I);
+      //DEBUG(std::cerr << "pop (%" << I->getParent()->getName() << ")\n");
     }
+  };
 
-    leaders.erase(leaders.begin() + I2 - 1);
-
-    return I2;
-  }
-}
-
-FunctionPass *llvm::createPredicateSimplifierPass() {
-  return new PredicateSimplifier();
-}
+  bool PredicateSimplifier::runOnFunction(Function &F) {
+    DT = &getAnalysis<DominatorTree>();
+    Forest = &getAnalysis<ETForest>();
 
-bool PredicateSimplifier::runOnFunction(Function &F) {
-  DT = &getAnalysis<DominatorTree>();
+    DEBUG(std::cerr << "Entering Function: " << F.getName() << "\n");
 
-  modified = false;
-  PropertySet KnownProperties(DT);
-  visitBasicBlock(DT->getRootNode()->getBlock(), KnownProperties);
-  return modified;
-}
+    modified = false;
+    WorkList.push_back(State(DT->getRoot(), new InequalityGraph()));
 
-void PredicateSimplifier::getAnalysisUsage(AnalysisUsage &AU) const {
-  AU.addRequiredID(BreakCriticalEdgesID);
-  AU.addRequired<DominatorTree>();
-  AU.setPreservesCFG();
-  AU.addPreservedID(BreakCriticalEdgesID);
-}
+    do {
+      State S = WorkList.back();
+      WorkList.pop_back();
+      visitBasicBlock(S.ToVisit, *S.IG);
+      delete S.IG;
+    } while (!WorkList.empty());
 
-void PredicateSimplifier::visitBasicBlock(BasicBlock *BB,
-                                          PropertySet &KnownProperties) {
-  for (BasicBlock::iterator I = BB->begin(), E = BB->end(); I != E;) {
-    visitInstruction(I++, KnownProperties);
-  }
-}
+    //DEBUG(F.viewCFG());
 
-void PredicateSimplifier::visitInstruction(Instruction *I,
-                                           PropertySet &KnownProperties) {
-  // Try to replace the whole instruction.
-  Value *V = KnownProperties.canonicalize(I);
-  if (V != I) {
-    modified = true;
-    ++NumInstruction;
-    DEBUG(std::cerr << "Removing " << *I);
-    KnownProperties.remove(I);
-    I->replaceAllUsesWith(V);
-    I->eraseFromParent();
-    return;
-  }
-
-  // Try to substitute operands.
-  for (unsigned i = 0, e = I->getNumOperands(); i != e; ++i) {
-    Value *Oper = I->getOperand(i);
-    Value *V = KnownProperties.canonicalize(Oper);
-    if (V != Oper) {
-      modified = true;
-      ++NumVarsReplaced;
-      DEBUG(std::cerr << "Resolving " << *I);
-      I->setOperand(i, V);
-      DEBUG(std::cerr << "into " << *I);
-    }
+    return modified;
   }
 
-  Forwards visit(this, KnownProperties);
-  visit.visit(*I);
-}
-
-void PredicateSimplifier::proceedToSuccessors(PropertySet &KP,
-                                              BasicBlock *BBCurrent) {
-  DTNodeType *Current = DT->getNode(BBCurrent);
-  for (DTNodeType::iterator I = Current->begin(), E = Current->end();
-       I != E; ++I) {
-    PropertySet Copy(KP);
-    visitBasicBlock((*I)->getBlock(), Copy);
+  void PredicateSimplifier::Forwards::visitTerminatorInst(TerminatorInst &TI) {
+    PS->proceedToSuccessors(IG, TI.getParent());
   }
-}
 
-void PredicateSimplifier::proceedToSuccessor(PropertySet &KP, BasicBlock *BB) {
-  visitBasicBlock(BB, KP);
-}
+  void PredicateSimplifier::Forwards::visitBranchInst(BranchInst &BI) {
+    BasicBlock *BB = BI.getParent();
 
-void PredicateSimplifier::Forwards::visitTerminatorInst(TerminatorInst &TI) {
-  PS->proceedToSuccessors(KP, TI.getParent());
-}
-
-void PredicateSimplifier::Forwards::visitBranchInst(BranchInst &BI) {
-  BasicBlock *BB = BI.getParent();
+    if (BI.isUnconditional()) {
+      PS->proceedToSuccessors(IG, BB);
+      return;
+    }
+
+    Value *Condition = BI.getCondition();
+    BasicBlock *TrueDest  = BI.getSuccessor(0),
+               *FalseDest = BI.getSuccessor(1);
+
+    if (isa<ConstantBool>(Condition) || TrueDest == FalseDest) {
+      PS->proceedToSuccessors(IG, BB);
+      return;
+    }
+
+    DominatorTree::Node *Node = PS->DT->getNode(BB);
+    for (DominatorTree::Node::iterator I = Node->begin(), E = Node->end();
+         I != E; ++I) {
+      BasicBlock *Dest = (*I)->getBlock();
+      InequalityGraph *DestProperties = new InequalityGraph(IG);
+      VRPSolver Solver(*DestProperties, PS->Forest, Dest);
+
+      if (Dest == TrueDest) {
+        DEBUG(std::cerr << "(" << BB->getName() << ") true set:\n");
+        if (!Solver.addEqual(ConstantBool::getTrue(), Condition)) continue;
+        Solver.solve();
+        DEBUG(DestProperties->debug(std::cerr));
+      } else if (Dest == FalseDest) {
+        DEBUG(std::cerr << "(" << BB->getName() << ") false set:\n");
+        if (!Solver.addEqual(ConstantBool::getFalse(), Condition)) continue;
+        Solver.solve();
+        DEBUG(DestProperties->debug(std::cerr));
+      }
 
-  if (BI.isUnconditional()) {
-    PS->proceedToSuccessors(KP, BB);
-    return;
+      PS->proceedToSuccessor(DestProperties, Dest);
+    }
   }
 
-  Value *Condition = BI.getCondition();
+  void PredicateSimplifier::Forwards::visitSwitchInst(SwitchInst &SI) {
+    Value *Condition = SI.getCondition();
 
-  BasicBlock *TrueDest  = BI.getSuccessor(0),
-             *FalseDest = BI.getSuccessor(1);
-
-  if (isa<ConstantBool>(Condition) || TrueDest == FalseDest) {
-    PS->proceedToSuccessors(KP, BB);
-    return;
+    // Set the EQProperty in each of the cases BBs, and the NEProperties
+    // in the default BB.
+    // InequalityGraph DefaultProperties(IG);
+
+    DominatorTree::Node *Node = PS->DT->getNode(SI.getParent());
+    for (DominatorTree::Node::iterator I = Node->begin(), E = Node->end();
+         I != E; ++I) {
+      BasicBlock *BB = (*I)->getBlock();
+
+      InequalityGraph *BBProperties = new InequalityGraph(IG);
+      VRPSolver Solver(*BBProperties, PS->Forest, BB);
+      if (BB == SI.getDefaultDest()) {
+        for (unsigned i = 1, e = SI.getNumCases(); i < e; ++i)
+          if (SI.getSuccessor(i) != BB)
+            if (!Solver.addNotEqual(Condition, SI.getCaseValue(i))) continue;
+        Solver.solve();
+      } else if (ConstantInt *CI = SI.findCaseDest(BB)) {
+        if (!Solver.addEqual(Condition, CI)) continue;
+        Solver.solve();
+      }
+      PS->proceedToSuccessor(BBProperties, BB);
+    }
   }
 
-  DTNodeType *Node = PS->DT->getNode(BB);
-  for (DTNodeType::iterator I = Node->begin(), E = Node->end(); I != E; ++I) {
-    BasicBlock *Dest = (*I)->getBlock();
-    PropertySet DestProperties(KP);
-
-    if (Dest == TrueDest)
-      DestProperties.addEqual(ConstantBool::getTrue(), Condition);
-    else if (Dest == FalseDest)
-      DestProperties.addEqual(ConstantBool::getFalse(), Condition);
-
-    PS->proceedToSuccessor(DestProperties, Dest);
+  void PredicateSimplifier::Forwards::visitAllocaInst(AllocaInst &AI) {
+    VRPSolver VRP(IG, PS->Forest, AI.getParent());
+    VRP.addNotEqual(Constant::getNullValue(AI.getType()), &AI);
+    VRP.solve();
   }
-}
 
-void PredicateSimplifier::Forwards::visitSwitchInst(SwitchInst &SI) {
-  Value *Condition = SI.getCondition();
-
-  // Set the EQProperty in each of the cases BBs,
-  // and the NEProperties in the default BB.
-  PropertySet DefaultProperties(KP);
-
-  DTNodeType *Node = PS->DT->getNode(SI.getParent());
-  for (DTNodeType::iterator I = Node->begin(), E = Node->end(); I != E; ++I) {
-    BasicBlock *BB = (*I)->getBlock();
-
-    PropertySet BBProperties(KP);
-    if (BB == SI.getDefaultDest()) {
-      for (unsigned i = 1, e = SI.getNumCases(); i < e; ++i)
-        if (SI.getSuccessor(i) != BB)
-          BBProperties.addNotEqual(Condition, SI.getCaseValue(i));
-    } else if (ConstantInt *CI = SI.findCaseDest(BB)) {
-      BBProperties.addEqual(Condition, CI);
-    }
-    PS->proceedToSuccessor(BBProperties, BB);
+  void PredicateSimplifier::Forwards::visitLoadInst(LoadInst &LI) {
+    Value *Ptr = LI.getPointerOperand();
+    // avoid "load uint* null" -> null NE null.
+    if (isa<Constant>(Ptr)) return;
+
+    VRPSolver VRP(IG, PS->Forest, LI.getParent());
+    VRP.addNotEqual(Constant::getNullValue(Ptr->getType()), Ptr);
+    VRP.solve();
   }
-}
-
-void PredicateSimplifier::Forwards::visitAllocaInst(AllocaInst &AI) {
-  KP.addNotEqual(Constant::getNullValue(AI.getType()), &AI);
-}
-
-void PredicateSimplifier::Forwards::visitLoadInst(LoadInst &LI) {
-  Value *Ptr = LI.getPointerOperand();
-  KP.addNotEqual(Constant::getNullValue(Ptr->getType()), Ptr);
-}
 
-void PredicateSimplifier::Forwards::visitStoreInst(StoreInst &SI) {
-  Value *Ptr = SI.getPointerOperand();
-  KP.addNotEqual(Constant::getNullValue(Ptr->getType()), Ptr);
-}
+  void PredicateSimplifier::Forwards::visitStoreInst(StoreInst &SI) {
+    Value *Ptr = SI.getPointerOperand();
+    if (isa<Constant>(Ptr)) return;
+
+    VRPSolver VRP(IG, PS->Forest, SI.getParent());
+    VRP.addNotEqual(Constant::getNullValue(Ptr->getType()), Ptr);
+    VRP.solve();
+  }
 
-void PredicateSimplifier::Forwards::visitBinaryOperator(BinaryOperator &BO) {
-  Instruction::BinaryOps ops = BO.getOpcode();
+  void PredicateSimplifier::Forwards::visitBinaryOperator(BinaryOperator &BO) {
+    Instruction::BinaryOps ops = BO.getOpcode();
 
-  switch (ops) {
+    switch (ops) {
     case Instruction::URem:
     case Instruction::SRem:
+    case Instruction::FRem:
     case Instruction::UDiv:
     case Instruction::SDiv:
-    case Instruction::FDiv:
-    case Instruction::FRem: {
+    case Instruction::FDiv: {
       Value *Divisor = BO.getOperand(1);
-      KP.addNotEqual(Constant::getNullValue(Divisor->getType()), Divisor);
+      VRPSolver VRP(IG, PS->Forest, BO.getParent());
+      VRP.addNotEqual(Constant::getNullValue(Divisor->getType()), Divisor);
+      VRP.solve();
       break;
     }
     default:
       break;
+    }
   }
+
+
+  RegisterPass<PredicateSimplifier> X("predsimplify",
+                                      "Predicate Simplifier");
+}
+
+FunctionPass *llvm::createPredicateSimplifierPass() {
+  return new PredicateSimplifier();
 }






More information about the llvm-commits mailing list