analyzer infrastructure: make a bunch of changes to symbolic expressions that

Zhongxing and I discussed by email.

Main changes:
- Removed SymIntConstraintVal and SymIntConstraint
- Added SymExpr as a parent class to SymbolData, SymSymExpr, SymIntExpr
- Added nonloc::SymExprVal to wrap SymExpr
- SymbolRef is now just a typedef of 'const SymbolData*'
- Bunch of minor code cleanups in how some methods were invoked (no functionality change)

This changes are part of a long-term plan to have full symbolic expression
trees. This will be useful for lazily evaluating complicated expressions.


git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@67731 91177308-0d34-0410-b5e6-96231b3b80d8

22 files changed, 571 insertions, 579 deletions

diff --git a/include/clang/Analysis/PathSensitive/BasicValueFactory.h b/include/clang/Analysis/PathSensitive/BasicValueFactory.h
index 3a401d69df..553f8a31bc 100644
--- a/include/clang/Analysis/PathSensitive/BasicValueFactory.h
+++ b/include/clang/Analysis/PathSensitive/BasicValueFactory.h
@@ -47,15 +47,10 @@ class BasicValueFactory {
   typedef llvm::FoldingSet<llvm::FoldingSetNodeWrapper<llvm::APSInt> >
           APSIntSetTy;
 
-  typedef llvm::FoldingSet<SymIntConstraint>
-          SymIntCSetTy;
-  
-
   ASTContext& Ctx;
   llvm::BumpPtrAllocator& BPAlloc;
 
   APSIntSetTy   APSIntSet;
-  SymIntCSetTy  SymIntCSet;
   void*         PersistentSVals;
   void*         PersistentSValPairs;
 
@@ -135,9 +130,6 @@ public:
     return getValue(b ? 1 : 0, Ctx.getTypeSize(Ctx.IntTy), false);
   }
   
-  const SymIntConstraint& getConstraint(SymbolRef sym, BinaryOperator::Opcode Op,
-                                        const llvm::APSInt& V);
-
   const CompoundValData* getCompoundValData(QualType T, 
                                             llvm::ImmutableList<SVal> Vals);
   
diff --git a/include/clang/Analysis/PathSensitive/ConstraintManager.h b/include/clang/Analysis/PathSensitive/ConstraintManager.h
index 32e5bb0cb3..c8e5e85c8a 100644
--- a/include/clang/Analysis/PathSensitive/ConstraintManager.h
+++ b/include/clang/Analysis/PathSensitive/ConstraintManager.h
@@ -26,7 +26,6 @@ namespace clang {
 class GRState;
 class GRStateManager;
 class SVal;
-class SymbolRef;
 
 class ConstraintManager {
 public:
diff --git a/include/clang/Analysis/PathSensitive/GRExprEngine.h b/include/clang/Analysis/PathSensitive/GRExprEngine.h
index dc9767312c..4c0abdcb09 100644
--- a/include/clang/Analysis/PathSensitive/GRExprEngine.h
+++ b/include/clang/Analysis/PathSensitive/GRExprEngine.h
@@ -642,24 +642,24 @@ protected:
     return X.isValid() ? getTF().EvalComplement(*this, cast<NonLoc>(X)) : X;
   }
   
-  SVal EvalBinOp(BinaryOperator::Opcode Op, NonLoc L, NonLoc R) {
-    return R.isValid() ? getTF().DetermEvalBinOpNN(*this, Op, L, R)
+  SVal EvalBinOp(BinaryOperator::Opcode Op, NonLoc L, NonLoc R, QualType T) {
+    return R.isValid() ? getTF().DetermEvalBinOpNN(*this, Op, L, R, T)
                        : R;
   }
 
-  SVal EvalBinOp(BinaryOperator::Opcode Op, NonLoc L, SVal R) {
+  SVal EvalBinOp(BinaryOperator::Opcode Op, NonLoc L, SVal R, QualType T) {
     return R.isValid() ? getTF().DetermEvalBinOpNN(*this, Op, L,
-                                                   cast<NonLoc>(R)) : R;
+                                                   cast<NonLoc>(R), T) : R;
   }
   
   void EvalBinOp(ExplodedNodeSet<GRState>& Dst, Expr* Ex,
                  BinaryOperator::Opcode Op, NonLoc L, NonLoc R,
-                 ExplodedNode<GRState>* Pred);
+                 ExplodedNode<GRState>* Pred, QualType T);
   
   void EvalBinOp(GRStateSet& OStates, const GRState* St, Expr* Ex,
-                 BinaryOperator::Opcode Op, NonLoc L, NonLoc R);  
+                 BinaryOperator::Opcode Op, NonLoc L, NonLoc R, QualType T);  
   
-  SVal EvalBinOp(BinaryOperator::Opcode Op, SVal L, SVal R);
+  SVal EvalBinOp(BinaryOperator::Opcode Op, SVal L, SVal R, QualType T);
   
   void EvalCall(NodeSet& Dst, CallExpr* CE, SVal L, NodeTy* Pred) {
     assert (Builder && "GRStmtNodeBuilder must be defined.");
diff --git a/include/clang/Analysis/PathSensitive/GRState.h b/include/clang/Analysis/PathSensitive/GRState.h
index 72418583ae..7110c7bc2d 100644
--- a/include/clang/Analysis/PathSensitive/GRState.h
+++ b/include/clang/Analysis/PathSensitive/GRState.h
@@ -310,7 +310,7 @@ public:
     ISetFactory(alloc),
     GDMFactory(alloc),
     BasicVals(Ctx, alloc),
-    SymMgr(Ctx, alloc),
+    SymMgr(Ctx, BasicVals, alloc),
     Alloc(alloc),
     cfg(c),
     codedecl(cd),
diff --git a/include/clang/Analysis/PathSensitive/GRTransferFuncs.h b/include/clang/Analysis/PathSensitive/GRTransferFuncs.h
index 69a7a12dd2..bee139f968 100644
--- a/include/clang/Analysis/PathSensitive/GRTransferFuncs.h
+++ b/include/clang/Analysis/PathSensitive/GRTransferFuncs.h
@@ -32,7 +32,7 @@ class GRTransferFuncs {
 protected:
   virtual SVal DetermEvalBinOpNN(GRExprEngine& Eng,
                                  BinaryOperator::Opcode Op,
-                                 NonLoc L, NonLoc R) {
+                                 NonLoc L, NonLoc R, QualType T) {
     return UnknownVal();
   }
   
@@ -59,7 +59,8 @@ public:
   // for OStates
   virtual void EvalBinOpNN(GRStateSet& OStates, GRExprEngine& Eng,
                            const GRState* St, Expr* Ex,
-                           BinaryOperator::Opcode Op, NonLoc L, NonLoc R);
+                           BinaryOperator::Opcode Op, NonLoc L, NonLoc R,
+                           QualType T);
   
   virtual SVal EvalBinOp(GRExprEngine& Engine, BinaryOperator::Opcode Op,
                          Loc L, Loc R) = 0;
diff --git a/include/clang/Analysis/PathSensitive/MemRegion.h b/include/clang/Analysis/PathSensitive/MemRegion.h
index 8cf084ad57..b54efadd3a 100644
--- a/include/clang/Analysis/PathSensitive/MemRegion.h
+++ b/include/clang/Analysis/PathSensitive/MemRegion.h
@@ -182,11 +182,10 @@ public:
 class SymbolicRegion : public TypedRegion {
 protected:
   const SymbolRef sym;
-  const SymbolManager& SymMgr;
 
 public:
-  SymbolicRegion(const SymbolRef s, const SymbolManager& mgr, MemRegion* sreg) 
-    : TypedRegion(sreg, SymbolicRegionKind), sym(s), SymMgr(mgr) {}
+  SymbolicRegion(const SymbolRef s, const MemRegion* sreg) 
+    : TypedRegion(sreg, SymbolicRegionKind), sym(s) {}
     
   SymbolRef getSymbol() const {
     return sym;
@@ -539,7 +538,7 @@ public:
   getCompoundLiteralRegion(const CompoundLiteralExpr* CL);  
   
   /// getSymbolicRegion - Retrieve or create a "symbolic" memory region.
-  SymbolicRegion* getSymbolicRegion(const SymbolRef sym, const SymbolManager&);
+  SymbolicRegion* getSymbolicRegion(SymbolRef sym);
 
   StringRegion* getStringRegion(const StringLiteral* Str);
 
diff --git a/include/clang/Analysis/PathSensitive/SVals.h b/include/clang/Analysis/PathSensitive/SVals.h
index 030115387a..a025325590 100644
--- a/include/clang/Analysis/PathSensitive/SVals.h
+++ b/include/clang/Analysis/PathSensitive/SVals.h
@@ -96,54 +96,45 @@ public:
   bool isZeroConstant() const;
   
   /// getAsLocSymbol - If this SVal is a location (subclasses Loc) and 
-  ///  wraps a symbol, return that SymbolRef.  Otherwise return a SymbolRef
-  ///  where 'isValid()' returns false.
+  ///  wraps a symbol, return that SymbolRef.  Otherwise return a SymbolData*
   SymbolRef getAsLocSymbol() const;
   
   /// getAsSymbol - If this Sval wraps a symbol return that SymbolRef.
   ///  Otherwise return a SymbolRef where 'isValid()' returns false.
   SymbolRef getAsSymbol() const;
+
+  /// getAsSymbolicExpression - If this Sval wraps a symbolic expression then
+  ///  return that expression.  Otherwise return NULL.
+  const SymExpr *getAsSymbolicExpression() const;
   
   void print(std::ostream& OS) const;
   void print(llvm::raw_ostream& OS) const;
   void printStdErr() const;
-  
+
+  // Iterators.
   class symbol_iterator {
-    SymbolRef SingleRef;
-    const SymbolRef* sptr;
+    llvm::SmallVector<const SymExpr*, 5> itr;
+    void expand();
   public:
+    symbol_iterator() {}
+    symbol_iterator(const SymExpr* SE);
     
-    bool operator==(const symbol_iterator& X) {
-      return SingleRef == X.SingleRef && sptr == X.sptr;
-    }
-    
-    bool operator!=(const symbol_iterator& X) {
-      return SingleRef != X.SingleRef || sptr != X.sptr;
-    }
-    
-    symbol_iterator& operator++() {
-      if (sptr)
-        ++sptr;
-      else
-        SingleRef = SymbolRef();
+    symbol_iterator& operator++();
+    SymbolRef operator*();
       
-      return *this;
-    }
-    
-    SymbolRef operator*() const {
-      if (sptr)
-        return *sptr;
-      
-      return SingleRef;
-    }
-    
-    symbol_iterator(SymbolRef x) : SingleRef(x), sptr(0) {}
-    symbol_iterator() : sptr(0) {}
-    symbol_iterator(const SymbolRef* x) : sptr(x) {}
+    bool operator==(const symbol_iterator& X) const;
+    bool operator!=(const symbol_iterator& X) const;
   };
   
-  symbol_iterator symbol_begin() const;
-  symbol_iterator symbol_end() const;
+  symbol_iterator symbol_begin() const {
+    const SymExpr *SE = getAsSymbolicExpression();
+    if (SE)
+      return symbol_iterator(SE);
+    else
+      return symbol_iterator();
+  }
+  
+  symbol_iterator symbol_end() const { return symbol_iterator(); }
   
   // Implement isa<T> support.
   static inline bool classof(const SVal*) { return true; }
@@ -178,14 +169,15 @@ public:
   void print(llvm::raw_ostream& Out) const;
   
   // Utility methods to create NonLocs.
-
   static NonLoc MakeVal(SymbolRef sym);
 
-  static NonLoc MakeVal(SymbolManager& SymMgr, SymbolRef lhs, 
-                        BinaryOperator::Opcode op, const llvm::APSInt& v);
+  static NonLoc MakeVal(SymbolManager& SymMgr, const SymExpr *lhs, 
+                        BinaryOperator::Opcode op, const llvm::APSInt& rhs,
+                        QualType T);
   
-  static NonLoc MakeVal(SymbolManager& SymMgr, SymbolRef lhs, 
-                        BinaryOperator::Opcode op, SymbolRef rhs);
+  static NonLoc MakeVal(SymbolManager& SymMgr, const SymExpr *lhs,
+                        BinaryOperator::Opcode op, const SymExpr *rhs,
+                        QualType T);
 
   static NonLoc MakeIntVal(BasicValueFactory& BasicVals, uint64_t X, 
                            bool isUnsigned);
@@ -219,8 +211,8 @@ protected:
     : SVal(const_cast<void*>(D), true, SubKind) {}
   
   // Equality operators.
-  NonLoc EQ(BasicValueFactory& BasicVals, const Loc& R) const;
-  NonLoc NE(BasicValueFactory& BasicVals, const Loc& R) const;
+  NonLoc EQ(SymbolManager& SM, const Loc& R) const;
+  NonLoc NE(SymbolManager& SM, const Loc& R) const;
   
 public:
   void print(llvm::raw_ostream& Out) const;
@@ -248,17 +240,15 @@ public:
 
 namespace nonloc {
   
-enum Kind { ConcreteIntKind, SymbolValKind, SymIntConstraintValKind,
+enum Kind { ConcreteIntKind, SymbolValKind, SymExprValKind,
             LocAsIntegerKind, CompoundValKind };
 
 class SymbolVal : public NonLoc {
 public:
-  SymbolVal(SymbolRef SymID)
-    : NonLoc(SymbolValKind,
-             reinterpret_cast<void*>((uintptr_t) SymID.getNumber())) {}
+  SymbolVal(SymbolRef sym) : NonLoc(SymbolValKind, sym) {}
   
   SymbolRef getSymbol() const {
-    return (SymbolRef) reinterpret_cast<uintptr_t>(Data);
+    return (const SymbolData*) Data;
   }
   
   static inline bool classof(const SVal* V) {
@@ -271,22 +261,22 @@ public:
   }
 };
 
-class SymIntConstraintVal : public NonLoc {    
+class SymExprVal : public NonLoc {    
 public:
-  SymIntConstraintVal(const SymIntConstraint& C)
-    : NonLoc(SymIntConstraintValKind, reinterpret_cast<const void*>(&C)) {}
+  SymExprVal(const SymExpr *SE)
+    : NonLoc(SymExprValKind, reinterpret_cast<const void*>(SE)) {}
 
-  const SymIntConstraint& getConstraint() const {
-    return *reinterpret_cast<SymIntConstraint*>(Data);
+  const SymExpr *getSymbolicExpression() const {
+    return reinterpret_cast<SymExpr*>(Data);
   }
   
   static inline bool classof(const SVal* V) {
     return V->getBaseKind() == NonLocKind &&
-           V->getSubKind() == SymIntConstraintValKind;
+           V->getSubKind() == SymExprValKind;
   }
   
   static inline bool classof(const NonLoc* V) {
-    return V->getSubKind() == SymIntConstraintValKind;
+    return V->getSubKind() == SymExprValKind;
   }
 };
 
@@ -387,12 +377,9 @@ enum Kind { SymbolValKind, GotoLabelKind, MemRegionKind, FuncValKind,
 
 class SymbolVal : public Loc {
 public:
-  SymbolVal(SymbolRef SymID)
-  : Loc(SymbolValKind, reinterpret_cast<void*>((uintptr_t) SymID.getNumber())){}
+  SymbolVal(SymbolRef sym) : Loc(SymbolValKind, sym) {}
   
-  SymbolRef getSymbol() const {
-    return (SymbolRef) reinterpret_cast<uintptr_t>(Data);
-  }
+  SymbolRef getSymbol() const { return (SymbolRef) Data; }
   
   static inline bool classof(const SVal* V) {
     return V->getBaseKind() == LocKind &&
diff --git a/include/clang/Analysis/PathSensitive/SymbolManager.h b/include/clang/Analysis/PathSensitive/SymbolManager.h
index 72a8b7907f..9bdbd88cae 100644
--- a/include/clang/Analysis/PathSensitive/SymbolManager.h
+++ b/include/clang/Analysis/PathSensitive/SymbolManager.h
@@ -28,92 +28,64 @@ namespace llvm {
   class raw_ostream;
 }
 
+namespace clang {  
+  class MemRegion;
+  class ASTContext;
+  class BasicValueFactory;
+}
+
 namespace clang {
   
-class MemRegion;
-class SymbolManager;
-class ASTContext;
-
-class SymbolRef {
-  unsigned Data;
+class SymExpr : public llvm::FoldingSetNode {
 public:
-  SymbolRef() : Data(~0U - 2) {}
-  SymbolRef(unsigned x) : Data(x) {}
-
-  bool isValid() const { return Data != (unsigned) (~0U - 2);  }
-  unsigned getNumber() const { assert (isValid()); return Data; }
-  
-  bool operator<(const SymbolRef& X) const { return Data < X.Data; }
-  bool operator>(const SymbolRef& X) const { return Data > X.Data; }
-  bool operator==(const SymbolRef& X) const { return Data == X.Data; }
-  bool operator!=(const SymbolRef& X) const { return Data != X.Data; }
-      
-  void Profile(llvm::FoldingSetNodeID& ID) const { 
-    ID.AddInteger(Data);
-  }
-};
-} // end clang namespace
-
-namespace llvm {
-  llvm::raw_ostream& operator<<(llvm::raw_ostream& Out, clang::SymbolRef Sym);
-}
-namespace std {
-  std::ostream& operator<<(std::ostream& Out, clang::SymbolRef Sym);
-}
-
-namespace llvm {
-template <> struct DenseMapInfo<clang::SymbolRef> {
-  static inline clang::SymbolRef getEmptyKey() {
-    return clang::SymbolRef(~0U);
-  }
-  static inline clang::SymbolRef getTombstoneKey() {
-    return clang::SymbolRef(~0U - 1);
-  }
-  static unsigned getHashValue(clang::SymbolRef X) {
-    return X.getNumber();
-  }
-  static bool isEqual(clang::SymbolRef X, clang::SymbolRef Y) {
-    return X == Y;
-  }
-  static bool isPod() { return true; }
-};
-}
-
-// SymbolData: Used to record meta data about symbols.
+  enum Kind { BEGIN_SYMBOLS, RegionRValue, ConjuredKind, END_SYMBOLS,
+              SymIntKind, SymSymKind };
+private:
+  Kind K;
 
-namespace clang {
+protected:
+  SymExpr(Kind k) : K(k) {}  
   
-class SymbolData : public llvm::FoldingSetNode {
 public:
-  enum Kind { RegionRValue, ConjuredKind, SymIntKind, SymSymKind };
+  virtual ~SymExpr() {}
+  
+  Kind getKind() const { return K; }  
+  
+  virtual QualType getType(ASTContext&) const = 0;  
+  virtual void Profile(llvm::FoldingSetNodeID& profile) = 0;
+  
+  // Implement isa<T> support.
+  static inline bool classof(const SymExpr*) { return true; }
+};
+  
+typedef unsigned SymbolID;
   
+class SymbolData : public SymExpr {
 private:
-  Kind K;
-  SymbolRef Sym;
+  const SymbolID Sym;
   
 protected:
-  SymbolData(Kind k, SymbolRef sym) : K(k), Sym(sym) {}  
+  SymbolData(Kind k, SymbolID sym) : SymExpr(k), Sym(sym) {}  
 
 public:
   virtual ~SymbolData() {}
   
-  Kind getKind() const { return K; }  
-  
-  SymbolRef getSymbol() const { return Sym; }
+  SymbolID getSymbolID() const { return Sym; }
     
-  virtual QualType getType(ASTContext&) const = 0;
-  
-  virtual void Profile(llvm::FoldingSetNodeID& profile) = 0;
-  
   // Implement isa<T> support.
-  static inline bool classof(const SymbolData*) { return true; }
+  static inline bool classof(const SymExpr* SE) { 
+    Kind k = SE->getKind();
+    return k > BEGIN_SYMBOLS && k < END_SYMBOLS;
+  }
 };
+
+typedef const SymbolData* SymbolRef;
   
 class SymbolRegionRValue : public SymbolData {
   const MemRegion *R;
 public:
-  SymbolRegionRValue(SymbolRef MySym, const MemRegion *r)
-    : SymbolData(RegionRValue, MySym), R(r) {}
+  SymbolRegionRValue(SymbolID sym, const MemRegion *r)
+    : SymbolData(RegionRValue, sym), R(r) {}
   
   const MemRegion* getRegion() const { return R; }
 
@@ -129,8 +101,8 @@ public:
   QualType getType(ASTContext&) const;
 
   // Implement isa<T> support.
-  static inline bool classof(const SymbolData* D) {
-    return D->getKind() == RegionRValue;
+  static inline bool classof(const SymExpr* SE) {
+    return SE->getKind() == RegionRValue;
   }
 };
 
@@ -141,9 +113,9 @@ class SymbolConjured : public SymbolData {
   const void* SymbolTag;
 
 public:
-  SymbolConjured(SymbolRef Sym, const Stmt* s, QualType t, unsigned count,
+  SymbolConjured(SymbolID sym, const Stmt* s, QualType t, unsigned count,
                  const void* symbolTag)
-    : SymbolData(ConjuredKind, Sym), S(s), T(t), Count(count),
+    : SymbolData(ConjuredKind, sym), S(s), T(t), Count(count),
       SymbolTag(symbolTag) {}
   
   const Stmt* getStmt() const { return S; }
@@ -166,143 +138,135 @@ public:
   }
 
   // Implement isa<T> support.
-  static inline bool classof(const SymbolData* D) {
-    return D->getKind() == ConjuredKind;
+  static inline bool classof(const SymExpr* SE) {
+    return SE->getKind() == ConjuredKind;
   }  
 };
 
 // SymIntExpr - Represents symbolic expression like 'x' + 3.
-class SymIntExpr : public SymbolData {
-  SymbolRef LHS;
+class SymIntExpr : public SymExpr {
+  const SymExpr *LHS;
   BinaryOperator::Opcode Op;
-  const llvm::APSInt& Val;
+  const llvm::APSInt& RHS;
   QualType T;
 
 public:
-  SymIntExpr(SymbolRef sym, SymbolRef lhs, BinaryOperator::Opcode op,
-             const llvm::APSInt& V, QualType t)
-    : SymbolData(SymIntKind, sym), LHS(lhs), Op(op), Val(V), T(t) {}
+  SymIntExpr(const SymExpr *lhs, BinaryOperator::Opcode op,
+             const llvm::APSInt& rhs, QualType t)
+    : SymExpr(SymIntKind), LHS(lhs), Op(op), RHS(rhs), T(t) {}
 
-  QualType getType(ASTContext& C) const {
-    return T;
-  }
+  // FIXME: We probably need to make this out-of-line to avoid redundant
+  // generation of virtual functions.
+  QualType getType(ASTContext& C) const { return T; }  
+  
+  BinaryOperator::Opcode getOpcode() const { return Op; }
+  
+  const SymExpr *getLHS() const { return LHS; }
+  const llvm::APSInt &getRHS() const { return RHS; }
 
-  static void Profile(llvm::FoldingSetNodeID& ID, SymbolRef lhs, 
-                      BinaryOperator::Opcode op, const llvm::APSInt& V,
+  static void Profile(llvm::FoldingSetNodeID& ID, const SymExpr *lhs, 
+                      BinaryOperator::Opcode op, const llvm::APSInt& rhs,
                       QualType t) {
-    lhs.Profile(ID);
+    ID.AddInteger((unsigned) SymIntKind);
+    ID.AddPointer(lhs);
     ID.AddInteger(op);
-    ID.AddPointer(&V);
+    ID.AddPointer(&rhs);
     ID.Add(t);
   }
 
   void Profile(llvm::FoldingSetNodeID& ID) {
-    Profile(ID, LHS, Op, Val, T);
+    Profile(ID, LHS, Op, RHS, T);
   }
+  
+  // Implement isa<T> support.
+  static inline bool classof(const SymExpr* SE) {
+    return SE->getKind() == SymIntKind;
+  }  
 };
 
 // SymSymExpr - Represents symbolic expression like 'x' + 'y'.
-class SymSymExpr : public SymbolData {
-  SymbolRef LHS;
+class SymSymExpr : public SymExpr {
+  const SymExpr *LHS;
   BinaryOperator::Opcode Op;
-  SymbolRef RHS;
+  const SymExpr *RHS;
   QualType T;
 
 public:
-  SymSymExpr(SymbolRef sym, SymbolRef lhs, BinaryOperator::Opcode op,
-             SymbolRef rhs, QualType t)
-    : SymbolData(SymSymKind, sym), LHS(lhs), Op(op), RHS(rhs), T(t) {}
+  SymSymExpr(const SymExpr *lhs, BinaryOperator::Opcode op, const SymExpr *rhs,
+             QualType t)
+    : SymExpr(SymSymKind), LHS(lhs), Op(op), RHS(rhs), T(t) {}
 
-  QualType getType(ASTContext& C) const {
-    return T;
-  }
+  const SymExpr *getLHS() const { return LHS; }
+  const SymExpr *getRHS() const { return RHS; }
+  
+  // FIXME: We probably need to make this out-of-line to avoid redundant
+  // generation of virtual functions.
+  QualType getType(ASTContext& C) const { return T; }
 
-  static void Profile(llvm::FoldingSetNodeID& ID, SymbolRef lhs,
-                      BinaryOperator::Opcode op, SymbolRef rhs, QualType t) {
-    lhs.Profile(ID);
+  static void Profile(llvm::FoldingSetNodeID& ID, const SymExpr *lhs,
+                      BinaryOperator::Opcode op, const SymExpr *rhs, QualType t) {
+    ID.AddInteger((unsigned) SymSymKind);
+    ID.AddPointer(lhs);
     ID.AddInteger(op);
-    rhs.Profile(ID);
+    ID.AddPointer(rhs);
     ID.Add(t);
   }
 
   void Profile(llvm::FoldingSetNodeID& ID) {
     Profile(ID, LHS, Op, RHS, T);
   }
-};
-
-// Constraints on symbols.  Usually wrapped by SValues.
-
-class SymIntConstraint : public llvm::FoldingSetNode {
-  SymbolRef Symbol;
-  BinaryOperator::Opcode Op;
-  const llvm::APSInt& Val;
-public:  
-  SymIntConstraint(SymbolRef sym, BinaryOperator::Opcode op, 
-                   const llvm::APSInt& V)
-  : Symbol(sym),
-  Op(op), Val(V) {}
-  
-  BinaryOperator::Opcode getOpcode() const { return Op; }
-  const SymbolRef& getSymbol() const { return Symbol; }
-  const llvm::APSInt& getInt() const { return Val; }
-  
-  static inline void Profile(llvm::FoldingSetNodeID& ID,
-                             SymbolRef Symbol,
-                             BinaryOperator::Opcode Op,
-                             const llvm::APSInt& Val) {
-    Symbol.Profile(ID);
-    ID.AddInteger(Op);
-    ID.AddPointer(&Val);
-  }
   
-  void Profile(llvm::FoldingSetNodeID& ID) {
-    Profile(ID, Symbol, Op, Val);
-  }
+  // Implement isa<T> support.
+  static inline bool classof(const SymExpr* SE) {
+    return SE->getKind() == SymSymKind;
+  }  
 };
 
-
 class SymbolManager {
-  typedef llvm::FoldingSet<SymbolData> DataSetTy;
-  typedef llvm::DenseMap<SymbolRef, SymbolData*> DataMapTy;
-  
-  DataSetTy DataSet;
-  DataMapTy DataMap;
-  
+  typedef llvm::FoldingSet<SymExpr> DataSetTy;
+  DataSetTy DataSet;  
   unsigned SymbolCounter;
   llvm::BumpPtrAllocator& BPAlloc;
+  BasicValueFactory &BV;
   ASTContext& Ctx;
   
 public:
-  SymbolManager(ASTContext& ctx, llvm::BumpPtrAllocator& bpalloc)
-    : SymbolCounter(0), BPAlloc(bpalloc), Ctx(ctx) {}
+  SymbolManager(ASTContext& ctx, BasicValueFactory &bv, 
+                llvm::BumpPtrAllocator& bpalloc)
+    : SymbolCounter(0), BPAlloc(bpalloc), BV(bv), Ctx(ctx) {}
   
   ~SymbolManager();
   
   static bool canSymbolicate(QualType T);
 
   /// Make a unique symbol for MemRegion R according to its kind.
-  SymbolRef getRegionRValueSymbol(const MemRegion* R);
-  SymbolRef getConjuredSymbol(const Stmt* E, QualType T, unsigned VisitCount,
-                              const void* SymbolTag = 0);
+  const SymbolRegionRValue* getRegionRValueSymbol(const MemRegion* R);
+  const SymbolConjured* getConjuredSymbol(const Stmt* E, QualType T,
+                                          unsigned VisitCount,
+                                          const void* SymbolTag = 0);
 
-  SymbolRef getConjuredSymbol(const Expr* E, unsigned VisitCount,
-                              const void* SymbolTag = 0) {    
+  const SymbolConjured* getConjuredSymbol(const Expr* E, unsigned VisitCount,
+                                          const void* SymbolTag = 0) {    
     return getConjuredSymbol(E, E->getType(), VisitCount, SymbolTag);
   }
 
-  SymbolRef getSymIntExpr(SymbolRef lhs, BinaryOperator::Opcode op, 
-                          const llvm::APSInt& v, QualType t);
-
-  SymbolRef getSymSymExpr(SymbolRef lhs, BinaryOperator::Opcode op,
-                          SymbolRef rhs, QualType t);
+  const SymIntExpr *getSymIntExpr(const SymExpr *lhs, BinaryOperator::Opcode op, 
+                                  const llvm::APSInt& rhs, QualType t);
   
-  const SymbolData& getSymbolData(SymbolRef ID) const;
+  const SymIntExpr *getSymIntExpr(const SymExpr &lhs, BinaryOperator::Opcode op,
+                                  const llvm::APSInt& rhs, QualType t) {
+    return getSymIntExpr(&lhs, op, rhs, t);
+  }
+
+  const SymSymExpr *getSymSymExpr(const SymExpr *lhs, BinaryOperator::Opcode op,
+                                  const SymExpr *rhs, QualType t);
   
-  QualType getType(SymbolRef ID) const {
-    return getSymbolData(ID).getType(Ctx);
+  QualType getType(const SymExpr *SE) const {
+    return SE->getType(Ctx);
   }
   
-  ASTContext& getContext() { return Ctx; }
+  ASTContext &getContext() { return Ctx; }
+  BasicValueFactory &getBasicVals() { return BV; }
 };
   
 class SymbolReaper {
@@ -353,4 +317,13 @@ public:
   
 } // end clang namespace
 
+namespace llvm {
+  llvm::raw_ostream& operator<<(llvm::raw_ostream& Out,
+                                const clang::SymExpr *SE);
+}
+namespace std {
+  std::ostream& operator<<(std::ostream& Out,
+                           const clang::SymExpr *SE);
+}
+
 #endif
diff --git a/lib/Analysis/BasicStore.cpp b/lib/Analysis/BasicStore.cpp
index 01260480d1..8c5b71f234 100644
--- a/lib/Analysis/BasicStore.cpp
+++ b/lib/Analysis/BasicStore.cpp
@@ -197,8 +197,8 @@ SVal BasicStoreManager::getLValueField(const GRState* St, SVal Base,
   
   switch(BaseL.getSubKind()) {
     case loc::SymbolValKind:
-      BaseR = MRMgr.getSymbolicRegion(cast<loc::SymbolVal>(&BaseL)->getSymbol(),
-                                      StateMgr.getSymbolManager());
+      BaseR =
+        MRMgr.getSymbolicRegion(cast<loc::SymbolVal>(&BaseL)->getSymbol());
       break;
       
     case loc::GotoLabelKind:
@@ -243,8 +243,7 @@ SVal BasicStoreManager::getLValueElement(const GRState* St, SVal Base,
       // Create a region to represent this symbol.
       // FIXME: In the future we may just use symbolic regions instead of
       //  SymbolVals to reason about symbolic memory chunks.
-      const MemRegion* SymR = MRMgr.getSymbolicRegion(Sym, 
-                                                  StateMgr.getSymbolManager());
+      const MemRegion* SymR = MRMgr.getSymbolicRegion(Sym);
       // Layered a typed region on top of this.
       QualType T = StateMgr.getSymbolManager().getType(Sym);
       BaseR = MRMgr.getTypedViewRegion(T, SymR);
diff --git a/lib/Analysis/BasicValueFactory.cpp b/lib/Analysis/BasicValueFactory.cpp
index 6ceab93b08..72ad0a5ed8 100644
--- a/lib/Analysis/BasicValueFactory.cpp
+++ b/lib/Analysis/BasicValueFactory.cpp
@@ -97,25 +97,6 @@ const llvm::APSInt& BasicValueFactory::getValue(uint64_t X, QualType T) {
   return getValue(V);
 }
 
-const SymIntConstraint&
-BasicValueFactory::getConstraint(SymbolRef sym, BinaryOperator::Opcode Op,
-                            const llvm::APSInt& V) {
-  
-  llvm::FoldingSetNodeID ID;
-  SymIntConstraint::Profile(ID, sym, Op, V);
-  void* InsertPos;
-  
-  SymIntConstraint* C = SymIntCSet.FindNodeOrInsertPos(ID, InsertPos);
-  
-  if (!C) {
-    C = (SymIntConstraint*) BPAlloc.Allocate<SymIntConstraint>();
-    new (C) SymIntConstraint(sym, Op, V);
-    SymIntCSet.InsertNode(C, InsertPos);
-  }
-  
-  return *C;
-}
-
 const CompoundValData* 
 BasicValueFactory::getCompoundValData(QualType T,
                                       llvm::ImmutableList<SVal> Vals) {
diff --git a/lib/Analysis/BugReporter.cpp b/lib/Analysis/BugReporter.cpp
index ffa1593fd5..6807c9f08e 100644
--- a/lib/Analysis/BugReporter.cpp
+++ b/lib/Analysis/BugReporter.cpp
@@ -443,7 +443,7 @@ public:
   bool HandleBinding(StoreManager& SMgr, Store store,
                      const MemRegion* R, SVal V) {
 
-    SymbolRef ScanSym;
+    SymbolRef ScanSym = 0;
     
     if (loc::SymbolVal* SV = dyn_cast<loc::SymbolVal>(&V))
       ScanSym = SV->getSymbol();
@@ -545,7 +545,7 @@ public:
   
   bool HandleBinding(StoreManager& SMgr, Store store,
                      const MemRegion* R, SVal V) {
-    SymbolRef ScanSym;
+    SymbolRef ScanSym = 0;
   
     if (loc::SymbolVal* SV = dyn_cast<loc::SymbolVal>(&V))
       ScanSym = SV->getSymbol();
@@ -554,7 +554,7 @@ public:
     else
       return true;
   
-    assert (ScanSym.isValid());
+    assert (ScanSym);
   
     if (!BR.isNotable(ScanSym))
       return true;
diff --git a/lib/Analysis/CFRefCount.cpp b/lib/Analysis/CFRefCount.cpp
index be1d794252..6e43ec5faf 100644
--- a/