diff --git a/Analysis/GREngine.cpp b/Analysis/GREngine.cpp
new file mode 100644
index 0000000..a10b4b8
--- /dev/null
+++ b/Analysis/GREngine.cpp
@@ -0,0 +1,261 @@
+//==- GREngine.cpp - Path-Sensitive Dataflow Engine ----------------*- C++ -*-//
+//             
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines a generic engine for intraprocedural, path-sensitive,
+//  dataflow analysis via graph reachability engine.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/PathSensitive/GREngine.h"
+#include "clang/AST/Expr.h"
+#include "llvm/Support/Compiler.h"
+#include "llvm/Support/Casting.h"
+#include "llvm/ADT/DenseMap.h"
+#include <vector>
+
+using llvm::cast;
+using llvm::isa;
+using namespace clang;
+
+namespace {
+  class VISIBILITY_HIDDEN DFS : public GRWorkList {
+  llvm::SmallVector<GRWorkListUnit,20> Stack;
+public:
+  virtual bool hasWork() const {
+    return !Stack.empty();
+  }
+
+  virtual void Enqueue(const GRWorkListUnit& U) {
+    Stack.push_back(U);
+  }
+
+  virtual GRWorkListUnit Dequeue() {
+    assert (!Stack.empty());
+    const GRWorkListUnit& U = Stack.back();
+    Stack.pop_back(); // This technically "invalidates" U, but we are fine.
+    return U;
+  }
+};
+} // end anonymous namespace
+
+GRWorkList* GRWorkList::MakeDFS() { return new DFS(); }
+
+/// ExecuteWorkList - Run the worklist algorithm for a maximum number of steps.
+bool GREngineImpl::ExecuteWorkList(unsigned Steps) {
+  
+  if (G->num_roots() == 0) { // Initialize the analysis by constructing
+    // the root if none exists.
+    
+    CFGBlock* Entry = &cfg.getEntry();
+    
+    assert (Entry->empty() && 
+            "Entry block must be empty.");
+    
+    assert (Entry->succ_size() == 1 &&
+            "Entry block must have 1 successor.");
+    
+    // Get the solitary successor.
+    CFGBlock* Succ = *(Entry->succ_begin());   
+    
+    // Construct an edge representing the
+    // starting location in the function.
+    BlockEdge StartLoc(cfg, Entry, Succ);
+    
+    // Generate the root.
+    GenerateNode(StartLoc, getInitialState());
+  }
+  
+  while (Steps && WList->hasWork()) {
+    --Steps;
+    const GRWorkListUnit& WU = WList->Dequeue();
+    ExplodedNodeImpl* Node = WU.getNode();
+    
+    // Dispatch on the location type.
+    switch (Node->getLocation().getKind()) {
+      default:
+        assert (isa<BlockEdge>(Node->getLocation()));
+        HandleBlockEdge(cast<BlockEdge>(Node->getLocation()), Node);
+        break;
+        
+      case ProgramPoint::BlockEntranceKind:
+        HandleBlockEntrance(cast<BlockEntrance>(Node->getLocation()), Node);
+        break;
+        
+      case ProgramPoint::BlockExitKind:
+        HandleBlockExit(cast<BlockExit>(Node->getLocation()), Node);
+        break;
+        
+      case ProgramPoint::PostStmtKind:
+        HandlePostStmt(cast<PostStmt>(Node->getLocation()), WU.getBlock(),
+                       WU.getIndex(), Node);
+        break;        
+    }
+  }
+  
+  return WList->hasWork();
+}
+
+void GREngineImpl::HandleBlockEdge(const BlockEdge& L, ExplodedNodeImpl* Pred) {
+  
+  CFGBlock* Blk = L.getDst();
+  
+  // Check if we are entering the EXIT block. 
+  if (Blk == &cfg.getExit()) {
+    
+    assert (cfg.getExit().size() == 0 && "EXIT block cannot contain Stmts.");
+
+    // Process the final state transition.    
+    void* State = ProcessEOP(Blk, Pred->State);
+
+    bool IsNew;
+    ExplodedNodeImpl* Node = G->getNodeImpl(BlockEntrance(Blk), State, &IsNew);
+    Node->addPredecessor(Pred);
+    
+    // If the node was freshly created, mark it as an "End-Of-Path" node.
+    if (IsNew) G->addEndOfPath(Node); 
+    
+    // This path is done. Don't enqueue any more nodes.
+    return;
+  }
+  
+  // FIXME: we will dispatch to a function that
+  //  manipulates the state at the entrance to a block.
+  
+  if (!Blk->empty())                            
+    GenerateNode(BlockEntrance(Blk), Pred->State, Pred);
+  else
+    GenerateNode(BlockExit(Blk), Pred->State, Pred);
+}
+
+void GREngineImpl::HandleBlockEntrance(const BlockEntrance& L,
+                                       ExplodedNodeImpl* Pred) {
+  
+  if (Stmt* S = L.getFirstStmt()) {
+    GRNodeBuilderImpl Builder(L.getBlock(), 0, Pred, this);
+    ProcessStmt(S, Builder);
+  }
+  else
+    GenerateNode(BlockExit(L.getBlock()), Pred->State, Pred);
+}
+
+
+void GREngineImpl::HandleBlockExit(const BlockExit& L, ExplodedNodeImpl* Pred) {
+  
+  CFGBlock* B = L.getBlock();
+  
+  if (Stmt* Terminator = B->getTerminator())
+    ProcessTerminator(Terminator, B, Pred);
+  else {
+    assert (B->succ_size() == 1 &&
+            "Blocks with no terminator should have at most 1 successor.");
+    
+    GenerateNode(BlockEdge(cfg,B,*(B->succ_begin())), Pred->State, Pred);    
+  }
+}
+
+void GREngineImpl::HandlePostStmt(const PostStmt& L, CFGBlock* B,
+                                  unsigned StmtIdx, ExplodedNodeImpl* Pred) {
+  
+  assert (!B->empty());
+
+  if (StmtIdx == B->size()) {
+    // FIXME: This is essentially an epsilon-transition.  Do we need it?
+    //  It does simplify the logic, and it is also another point
+    //  were we could introduce a dispatch to the client.
+    GenerateNode(BlockExit(B), Pred->State, Pred);
+  }
+  else {
+    GRNodeBuilderImpl Builder(B, StmtIdx, Pred, this);
+    ProcessStmt(L.getStmt(), Builder);
+  }
+}
+
+typedef llvm::DenseMap<Stmt*,Stmt*> ParentMapTy;
+/// PopulateParentMap - Recurse the AST starting at 'Parent' and add the
+///  mappings between child and parent to ParentMap.
+static void PopulateParentMap(Stmt* Parent, ParentMapTy& M) {
+  for (Stmt::child_iterator I=Parent->child_begin(), 
+       E=Parent->child_end(); I!=E; ++I) {
+    
+    assert (M.find(*I) == M.end());
+    M[*I] = Parent;
+    PopulateParentMap(*I, M);
+  }
+}
+
+/// GenerateNode - Utility method to generate nodes, hook up successors,
+///  and add nodes to the worklist.
+void GREngineImpl::GenerateNode(const ProgramPoint& Loc, void* State,
+                                ExplodedNodeImpl* Pred) {
+  
+  bool IsNew;
+  ExplodedNodeImpl* Node = G->getNodeImpl(Loc, State, &IsNew);
+  
+  if (Pred) 
+    Node->addPredecessor(Pred);  // Link 'Node' with its predecessor.
+  else {
+    assert (IsNew);
+    G->addRoot(Node);  // 'Node' has no predecessor.  Make it a root.
+  }
+  
+  // Only add 'Node' to the worklist if it was freshly generated.
+  if (IsNew) WList->Enqueue(GRWorkListUnit(Node));
+}
+
+GRNodeBuilderImpl::GRNodeBuilderImpl(CFGBlock* b, unsigned idx,
+                                     ExplodedNodeImpl* N, GREngineImpl* e)
+  : Eng(*e), B(*b), Idx(idx), LastNode(N), Populated(false) {
+  Deferred.insert(N);
+}
+
+GRNodeBuilderImpl::~GRNodeBuilderImpl() {
+  for (DeferredTy::iterator I=Deferred.begin(), E=Deferred.end(); I!=E; ++I)
+    if (!(*I)->isInfeasible())
+      GenerateAutoTransition(*I);
+}
+
+void GRNodeBuilderImpl::GenerateAutoTransition(ExplodedNodeImpl* N) {
+  assert (!N->isInfeasible());
+  
+  PostStmt Loc(getStmt());
+  
+  if (Loc == N->getLocation()) {
+    // Note: 'N' should be a fresh node because otherwise it shouldn't be
+    // a member of Deferred.
+    Eng.WList->Enqueue(N, B, Idx+1);
+    return;
+  }
+  
+  bool IsNew;
+  ExplodedNodeImpl* Succ = Eng.G->getNodeImpl(Loc, N->State, &IsNew);
+  Succ->addPredecessor(N);
+
+  if (IsNew)
+    Eng.WList->Enqueue(Succ, B, Idx+1);
+}
+
+ExplodedNodeImpl* GRNodeBuilderImpl::generateNodeImpl(Stmt* S, void* State,
+                                                      ExplodedNodeImpl* Pred) {
+  
+  bool IsNew;
+  ExplodedNodeImpl* N = Eng.G->getNodeImpl(PostStmt(S), State, &IsNew);
+  N->addPredecessor(Pred);
+  Deferred.erase(Pred);
+  
+  HasGeneratedNode = true;
+  
+  if (IsNew) {
+    Deferred.insert(N);
+    LastNode = N;
+    return N;
+  }
+  
+  LastNode = NULL;
+  return NULL;  
+}
diff --git a/include/clang/Analysis/PathSensitive/ExplodedGraph.h b/include/clang/Analysis/PathSensitive/ExplodedGraph.h
index d2241dc..1fd2f40 100644
--- a/include/clang/Analysis/PathSensitive/ExplodedGraph.h
+++ b/include/clang/Analysis/PathSensitive/ExplodedGraph.h
@@ -28,13 +28,16 @@
 
 class GREngineImpl;
 class ExplodedNodeImpl;
+class GRNodeBuilderImpl;
 
 class ExplodedNodeImpl : public llvm::FoldingSetNode {
 protected:
   friend class ExplodedGraphImpl;
+  friend class GREngineImpl;
+  friend class GRNodeBuilderImpl;
   
   class NodeGroup {
-    enum { Size1 = 0x0, SizeOther = 0x1, Flags = 0x1 };
+    enum { Size1 = 0x0, SizeOther = 0x1, Infeasible = 0x2, Flags = 0x3 };
     uintptr_t P;
     
     unsigned getKind() const { return P & Flags; }
@@ -55,6 +58,14 @@
     bool empty() const;
     
     void addNode(ExplodedNodeImpl* N);
+    
+    void setInfeasibleFlag() {
+      P |= Infeasible;
+    }
+    
+    bool getInfeasibleFlag() const {
+      return P & Infeasible ? true : false;
+    }
   };
   
   
@@ -78,9 +89,9 @@
   : Location(loc), State(state) {}
   
   /// addPredeccessor - Adds a predecessor to the current node, and 
-  ///  in tandem add this node as a successor of the other node.  This
-  ///  method is intended to be used only by ExplodedGraphImpl.
+  ///  in tandem add this node as a successor of the other node.
   void addPredecessor(ExplodedNodeImpl* V) {
+    assert (!V->isInfeasible());
     Preds.addNode(V);
     V->Succs.addNode(this);
   }
@@ -103,6 +114,9 @@
   unsigned pred_size() const { return Preds.size(); }
   bool succ_empty() const { return Succs.empty(); }
   bool pred_empty() const { return Preds.size(); }
+  
+  bool isInfeasible() const { return Preds.getInfeasibleFlag(); }
+  void setInfeasible() { Preds.setInfeasibleFlag(); }  
 };
 
 
@@ -166,6 +180,7 @@
 class ExplodedGraphImpl {
 protected:
   friend class GREngineImpl;
+  friend class GRNodeBuilderImpl;
   
   // Type definitions.
   typedef llvm::DenseMap<ProgramPoint,void*>        EdgeNodeSetMap;
diff --git a/include/clang/Analysis/PathSensitive/GREngine.h b/include/clang/Analysis/PathSensitive/GREngine.h
new file mode 100644
index 0000000..20f1071
--- /dev/null
+++ b/include/clang/Analysis/PathSensitive/GREngine.h
@@ -0,0 +1,228 @@
+//==- GREngine.h - Path-Sensitive Dataflow Engine ------------------*- C++ -*-//
+//             
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines a generic engine for intraprocedural, path-sensitive,
+//  dataflow analysis via graph reachability engine.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_GRENGINE
+#define LLVM_CLANG_ANALYSIS_GRENGINE
+
+#include "clang/Analysis/PathSensitive/ExplodedGraph.h"
+#include "clang/Analysis/PathSensitive/GRWorkList.h"
+#include "llvm/ADT/OwningPtr.h"
+
+namespace clang {
+  
+class CFG;
+class GRNodeBuilderImpl;
+class GRWorkList;
+  
+class GREngineImpl {
+protected:
+  friend class GRNodeBuilderImpl;
+  
+  typedef llvm::DenseMap<Stmt*,Stmt*> ParentMapTy;
+
+  /// cfg - The control-flow graph of the function being analyzed.
+  CFG& cfg;
+    
+  /// G - The simulation graph.  Each node is a (location,state) pair.
+  llvm::OwningPtr<ExplodedGraphImpl> G;
+  
+  /// ParentMap - A lazily populated map from a Stmt* to its parent Stmt*.
+  void* ParentMap;
+  
+  /// CurrentBlkExpr - The current Block-level expression being processed.
+  ///  This is used when lazily populating ParentMap.
+  Stmt* CurrentBlkExpr;
+  
+  /// WList - A set of queued nodes that need to be processed by the
+  ///  worklist algorithm.  It is up to the implementation of WList to decide
+  ///  the order that nodes are processed.
+  GRWorkList* WList;
+  
+  void GenerateNode(const ProgramPoint& Loc, void* State, 
+                    ExplodedNodeImpl* Pred = NULL);
+  
+  /// getInitialState - Gets the void* representing the initial 'state'
+  ///  of the analysis.  This is simply a wrapper (implemented
+  ///  in GREngine) that performs type erasure on the initial
+  ///  state returned by the checker object.
+  virtual void* getInitialState() = 0;
+  
+  void HandleBlockEdge(const BlockEdge& E, ExplodedNodeImpl* Pred);
+  void HandleBlockEntrance(const BlockEntrance& E, ExplodedNodeImpl* Pred);
+  void HandleBlockExit(const BlockExit& E, ExplodedNodeImpl* Pred);
+  void HandlePostStmt(const PostStmt& S, CFGBlock* B,
+                      unsigned StmtIdx, ExplodedNodeImpl *Pred);
+
+  virtual void* ProcessEOP(CFGBlock* Blk, void* State) = 0;  
+
+  virtual void ProcessStmt(Stmt* S, GRNodeBuilderImpl& Builder) = 0;
+
+  virtual void ProcessTerminator(Stmt* Terminator, CFGBlock* B, 
+                                 ExplodedNodeImpl* Pred) = 0;
+
+private:
+  GREngineImpl(const GREngineImpl&); // Do not implement.
+  GREngineImpl& operator=(const GREngineImpl&);
+  
+protected:  
+  GREngineImpl(CFG& c, ExplodedGraphImpl* g, GRWorkList* wl)
+   : cfg(c), G(g), WList(wl) {}
+  
+public:
+  /// ExecuteWorkList - Run the worklist algorithm for a maximum number of
+  ///  steps.  Returns true if there is still simulation state on the worklist.
+  bool ExecuteWorkList(unsigned Steps = 1000000);
+  
+  virtual ~GREngineImpl() {}
+};
+  
+class GRNodeBuilderImpl {
+  GREngineImpl& Eng;
+  CFGBlock& B;
+  const unsigned Idx;
+  ExplodedNodeImpl* LastNode;  
+  bool HasGeneratedNode;
+  bool Populated;
+  
+  typedef llvm::SmallPtrSet<ExplodedNodeImpl*,5> DeferredTy;
+  DeferredTy Deferred;
+  
+  void GenerateAutoTransition(ExplodedNodeImpl* N);
+  
+public:
+  GRNodeBuilderImpl(CFGBlock* b, unsigned idx,
+                    ExplodedNodeImpl* N, GREngineImpl* e);      
+  
+  ~GRNodeBuilderImpl();
+  
+  const ExplodedGraphImpl& getGraph() const { return *Eng.G; }
+
+  inline ExplodedNodeImpl* getLastNode() {
+    return LastNode ? (LastNode->isInfeasible() ? NULL : LastNode) : NULL;
+  }
+  
+  ExplodedNodeImpl* generateNodeImpl(Stmt* S, void* State,
+                                     ExplodedNodeImpl* Pred);
+
+  inline ExplodedNodeImpl* generateNodeImpl(Stmt* S, void* State) {
+    ExplodedNodeImpl* N = getLastNode();
+    assert (N && "Predecessor of new node is infeasible.");
+    return generateNodeImpl(S, State, N);
+  }
+  
+  Stmt* getStmt() const { return B[Idx]; }
+  
+  CFGBlock* getBlock() const { return &B; }
+};
+
+template<typename CHECKER>
+class GRNodeBuilder  {
+  typedef CHECKER                                CheckerTy; 
+  typedef typename CheckerTy::StateTy            StateTy;
+  typedef ExplodedGraph<CheckerTy>               GraphTy;
+  typedef typename GraphTy::NodeTy               NodeTy;
+  
+  GRNodeBuilderImpl& NB;
+  
+public:
+  const GraphTy& getGraph() const {
+    return static_cast<const GraphTy&>(NB.getGraph());
+  }
+  
+  NodeTy* getLastNode() const {
+    return static_cast<NodeTy*>(NB.getLastNode());
+  }
+  
+  NodeTy* generateNode(Stmt* S, StateTy State, NodeTy* Pred) {
+    void *state = GRTrait<StateTy>::toPtr(State);        
+    return static_cast<NodeTy*>(NB.generateNodeImpl(S, state, Pred));
+  }
+  
+  NodeTy* generateNode(Stmt* S, StateTy State) {
+    void *state = GRTrait<StateTy>::toPtr(State);
+    return static_cast<NodeTy*>(NB.generateNodeImpl(S, state));    
+  }  
+};
+  
+  
+template<typename CHECKER>
+class GREngine : public GREngineImpl {
+public:
+  typedef CHECKER                                CheckerTy; 
+  typedef typename CheckerTy::StateTy            StateTy;
+  typedef ExplodedGraph<CheckerTy>               GraphTy;
+  typedef typename GraphTy::NodeTy               NodeTy;
+
+protected:
+  // A local reference to the checker that avoids an indirect access
+  // via the Graph.
+  CheckerTy* Checker;
+  
+  
+  virtual void* getInitialState() {
+    return GRTrait<StateTy>::toPtr(getCheckerState()->getInitialState());
+  }
+  
+  virtual void* ProcessEOP(CFGBlock* Blk, void* State) {
+    // FIXME: Perform dispatch to adjust state.
+    return State;
+  }
+  
+  virtual void ProcessStmt(Stmt* S, GRNodeBuilderImpl& BuilderImpl) {
+    GRNodeBuilder<CHECKER> Builder(BuilderImpl);
+    Checker->ProcessStmt(S, Builder);
+  }
+
+  virtual void ProcessTerminator(Stmt* Terminator, CFGBlock* B, 
+                                 ExplodedNodeImpl* Pred) {
+    // FIXME: Dispatch.    
+  }
+  
+  
+public:  
+  /// Construct a GREngine object to analyze the provided CFG using
+  ///  a DFS exploration of the exploded graph.
+  GREngine(CFG& Cfg)
+  : GREngineImpl(cfg, new GraphTy(), GRWorkList::MakeDFS()),
+      Checker(static_cast<GraphTy*>(G.get())->getCheckerState()) {}
+  
+  /// Construct a GREngine object to analyze the provided CFG and to
+  ///  use the provided worklist object to execute the worklist algorithm.
+  ///  The GREngine object assumes ownership of 'wlist'.
+  GREngine(CFG& cfg, GRWorkList* wlist) 
+    : GREngineImpl(cfg, new GraphTy(), wlist),
+      Checker(static_cast<GraphTy*>(G.get())->getCheckerState()) {}
+  
+  virtual ~GREngine() {}
+  
+  /// getGraph - Returns the exploded graph.
+  GraphTy& getGraph() {
+    return *static_cast<GraphTy*>(G.get());
+  }
+  
+  /// getCheckerState - Returns the internal checker state.
+  CheckerTy& getCheckerState() {
+    return *Checker;
+  }  
+  
+  /// takeGraph - Returns the exploded graph.  Ownership of the graph is
+  ///  transfered to the caller.
+  GraphTy* takeGraph() { 
+    return static_cast<GraphTy*>(G.take());
+  }
+};
+
+} // end clang namespace
+
+#endif
diff --git a/include/clang/Analysis/PathSensitive/GRWorkList.h b/include/clang/Analysis/PathSensitive/GRWorkList.h
new file mode 100644
index 0000000..4e3ce54
--- /dev/null
+++ b/include/clang/Analysis/PathSensitive/GRWorkList.h
@@ -0,0 +1,54 @@
+//==- GRWorkList.h - Worklist class used by GREngine ---------------*- C++ -*-//
+//             
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines GRWorkList, a pure virtual class that represents an
+//  opaque worklist used by GREngine to explore the reachability state space.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_GRWORKLIST
+#define LLVM_CLANG_ANALYSIS_GRWORKLIST
+
+namespace clang {  
+
+class ExplodedNodeImpl;
+  
+class GRWorkListUnit {
+  ExplodedNodeImpl* Node;
+  CFGBlock* Block;
+  unsigned BlockIdx;
+  
+public:
+  GRWorkListUnit(ExplodedNodeImpl* N, CFGBlock* B, unsigned idx)
+  : Node(N), Block(B), BlockIdx(idx) {}
+  
+  explicit GRWorkListUnit(ExplodedNodeImpl* N)
+  : Node(N), Block(NULL), BlockIdx(0) {}
+  
+  ExplodedNodeImpl* getNode()  const { return Node; }    
+  CFGBlock*         getBlock() const { return Block; }
+  unsigned          getIndex() const { return BlockIdx; }
+};
+
+class GRWorkList {
+public:
+  virtual ~GRWorkList() = 0;
+  virtual bool hasWork() const = 0;
+  virtual void Enqueue(const GRWorkListUnit& U) = 0;
+
+  void Enqueue(ExplodedNodeImpl* N, CFGBlock& B, unsigned idx) {
+    Enqueue(GRWorkListUnit(N,&B,idx));
+  }
+  
+  virtual GRWorkListUnit Dequeue() = 0;
+  
+  static GRWorkList* MakeDFS(); 
+};
+} // end clang namespace  
+#endif