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

14 files changed, 390 insertions, 349 deletions

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/lib/Analysis/CFRefCount.cpp
+++ b/lib/Analysis/CFRefCount.cpp
@@ -1591,8 +1591,8 @@ public:
 
 static void PrintPool(std::ostream &Out, SymbolRef Sym, const GRState *state) {
   Out << ' ';
-  if (Sym.isValid())
-    Out << Sym;
+  if (Sym)
+    Out << Sym->getSymbolID();
   else
     Out << "<pool>";
   Out << ":{";
@@ -1705,7 +1705,7 @@ void CFRefCount::EvalSummary(ExplodedNodeSet<GRState>& Dst,
     SVal V = state.GetSValAsScalarOrLoc(*I);    
     SymbolRef Sym = V.getAsLocSymbol();
 
-    if (Sym.isValid())
+    if (Sym)
       if (RefBindings::data_type* T = state.get<RefBindings>(Sym)) {
         state = Update(state, Sym, *T, GetArgE(Summ, idx), hasErr);
         if (hasErr) {
@@ -1746,7 +1746,7 @@ void CFRefCount::EvalSummary(ExplodedNodeSet<GRState>& Dst,
           SymbolRef Sym = state.GetSValAsScalarOrLoc(R).getAsLocSymbol();
           
           // Remove any existing reference-count binding.
-          if (Sym.isValid()) state = state.remove<RefBindings>(Sym);
+          if (Sym) state = state.remove<RefBindings>(Sym);
           
           if (R->isBoundable(Ctx)) {
             // Set the value of the variable to be a conjured symbol.
@@ -1833,7 +1833,7 @@ void CFRefCount::EvalSummary(ExplodedNodeSet<GRState>& Dst,
   // Evaluate the effect on the message receiver.  
   if (!ErrorExpr && Receiver) {
     SymbolRef Sym = state.GetSValAsScalarOrLoc(Receiver).getAsLocSymbol();
-    if (Sym.isValid()) {
+    if (Sym) {
       if (const RefVal* T = state.get<RefBindings>(Sym)) {
         state = Update(state, Sym, *T, GetReceiverE(Summ), hasErr);
         if (hasErr) {
@@ -1977,7 +1977,7 @@ void CFRefCount::EvalObjCMessageExpr(ExplodedNodeSet<GRState>& Dst,
     SVal V = Eng.getStateManager().GetSValAsScalarOrLoc(St, Receiver);
 
     SymbolRef Sym = V.getAsLocSymbol();
-    if (Sym.isValid()) {
+    if (Sym) {
       if (const RefVal* T  = St->get<RefBindings>(Sym)) {
         QualType Ty = T->getType();
         
@@ -2127,7 +2127,7 @@ void CFRefCount::EvalReturn(ExplodedNodeSet<GRState>& Dst,
   GRStateRef state(Builder.GetState(Pred), Eng.getStateManager());
   SymbolRef Sym = state.GetSValAsScalarOrLoc(RetE).getAsLocSymbol();
   
-  if (!Sym.isValid())
+  if (!Sym)
     return;
 
   // Get the reference count binding (if any).
@@ -2824,9 +2824,9 @@ class VISIBILITY_HIDDEN FindUniqueBinding :
     
   bool HandleBinding(StoreManager& SMgr, Store store, const MemRegion* R,
                      SVal val) {
-    SymbolRef SymV = val.getAsSymbol();
-    
-    if (!SymV.isValid() || SymV != Sym)
+
+    SymbolRef SymV = val.getAsSymbol();    
+    if (!SymV || SymV != Sym)
       return true;
     
     if (Binding) {
diff --git a/lib/Analysis/GRExprEngine.cpp b/lib/Analysis/GRExprEngine.cpp
index 80467ebb27..2f3f0bf5cc 100644
--- a/lib/Analysis/GRExprEngine.cpp
+++ b/lib/Analysis/GRExprEngine.cpp
@@ -782,7 +782,8 @@ void GRExprEngine::ProcessSwitch(SwitchNodeBuilder& builder) {
         
     do {
       nonloc::ConcreteInt CaseVal(getBasicVals().getValue(V1.Val.getInt()));      
-      SVal Res = EvalBinOp(BinaryOperator::EQ, CondV, CaseVal);
+      SVal Res = EvalBinOp(BinaryOperator::EQ, CondV, CaseVal,
+                           getContext().IntTy);
       
       // Now "assume" that the case matches.      
       bool isFeasible = false;      
@@ -1449,7 +1450,7 @@ void GRExprEngine::EvalEagerlyAssume(NodeSet &Dst, NodeSet &Src, Expr *Ex) {
 
     const GRState* state = Pred->getState();    
     SVal V = GetSVal(state, Ex);    
-    if (isa<nonloc::SymIntConstraintVal>(V)) {
+    if (isa<nonloc::SymExprVal>(V)) {
       // First assume that the condition is true.
       bool isFeasible = false;
       const GRState *stateTrue = Assume(state, V, true, isFeasible);
@@ -1940,8 +1941,7 @@ void GRExprEngine::VisitCast(Expr* CastE, Expr* Ex, NodeTy* Pred, NodeSet& Dst){
       }
 
       StoreManager& StoreMgr = getStoreManager();
-      const MemRegion* R =
-        StoreMgr.getRegionManager().getSymbolicRegion(Sym, getSymbolManager());
+      const MemRegion* R = StoreMgr.getRegionManager().getSymbolicRegion(Sym);
       
       // Delegate to store manager to get the result of casting a region
       // to a different type.
@@ -2394,7 +2394,8 @@ void GRExprEngine::VisitUnaryOperator(UnaryOperator* U, NodeTy* Pred,
             
             if (isa<Loc>(V)) {
               loc::ConcreteInt X(getBasicVals().getZeroWithPtrWidth());
-              SVal Result = EvalBinOp(BinaryOperator::EQ, cast<Loc>(V), X);
+              SVal Result = EvalBinOp(BinaryOperator::EQ, cast<Loc>(V), X,
+                                      U->getType());
               state = BindExpr(state, U, Result);
             }
             else {
@@ -2403,7 +2404,8 @@ void GRExprEngine::VisitUnaryOperator(UnaryOperator* U, NodeTy* Pred,
               SVal Result = EvalBinOp(BinaryOperator::EQ, cast<NonLoc>(V), X);
               state = SetSVal(state, U, Result);
 #else
-              EvalBinOp(Dst, U, BinaryOperator::EQ, cast<NonLoc>(V), X, *I);
+              EvalBinOp(Dst, U, BinaryOperator::EQ, cast<NonLoc>(V), X, *I,
+                        U->getType());
               continue;
 #endif
             }
@@ -2449,7 +2451,7 @@ void GRExprEngine::VisitUnaryOperator(UnaryOperator* U, NodeTy* Pred,
       BinaryOperator::Opcode Op = U->isIncrementOp() ? BinaryOperator::Add
                                                      : BinaryOperator::Sub;
 
-      SVal Result = EvalBinOp(Op, V2, MakeConstantVal(1U, U));    
+      SVal Result = EvalBinOp(Op, V2, MakeConstantVal(1U, U), U->getType());    
       
       // Conjure a new symbol if necessary to recover precision.
       if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result))
@@ -2643,7 +2645,6 @@ void GRExprEngine::VisitBinaryOperator(BinaryOperator* B,
     return;
   }
   
-  
   if (B->isAssignmentOp())
     VisitLValue(LHS, Pred, Tmp1);
   else
@@ -2716,7 +2717,7 @@ void GRExprEngine::VisitBinaryOperator(BinaryOperator* B,
           // Process non-assignements except commas or short-circuited
           // logical expressions (LAnd and LOr).
           
-          SVal Result = EvalBinOp(Op, LeftV, RightV);
+          SVal Result = EvalBinOp(Op, LeftV, RightV, B->getType());
           
           if (Result.isUnknown()) {
             if (OldSt != state) {
@@ -2828,7 +2829,7 @@ void GRExprEngine::VisitBinaryOperator(BinaryOperator* B,
         }
       
         // Compute the result of the operation.      
-        SVal Result = EvalCast(EvalBinOp(Op, V, RightV), B->getType());
+        SVal Result = EvalCast(EvalBinOp(Op, V, RightV, CTy), B->getType());
           
         if (Result.isUndef()) {
           // The operands were not undefined, but the result is undefined.
@@ -2882,10 +2883,10 @@ void GRExprEngine::VisitBinaryOperator(BinaryOperator* B,
 void GRExprEngine::EvalBinOp(ExplodedNodeSet<GRState>& Dst, Expr* Ex,
                              BinaryOperator::Opcode Op,
                              NonLoc L, NonLoc R,
-                             ExplodedNode<GRState>* Pred) {
+                             ExplodedNode<GRState>* Pred, QualType T) {
 
   GRStateSet OStates;
-  EvalBinOp(OStates, GetState(Pred), Ex, Op, L, R);
+  EvalBinOp(OStates, GetState(Pred), Ex, Op, L, R, T);
 
   for (GRStateSet::iterator I=OStates.begin(), E=OStates.end(); I!=E; ++I)
     MakeNode(Dst, Ex, Pred, *I);
@@ -2893,13 +2894,14 @@ void GRExprEngine::EvalBinOp(ExplodedNodeSet<GRState>& Dst, Expr* Ex,
 
 void GRExprEngine::EvalBinOp(GRStateSet& OStates, const GRState* state,
                              Expr* Ex, BinaryOperator::Opcode Op,
-                             NonLoc L, NonLoc R) {
+                             NonLoc L, NonLoc R, QualType T) {
   
   GRStateSet::AutoPopulate AP(OStates, state);
-  if (R.isValid()) getTF().EvalBinOpNN(OStates, *this, state, Ex, Op, L, R);
+  if (R.isValid()) getTF().EvalBinOpNN(OStates, *this, state, Ex, Op, L, R, T);
 }
 
-SVal GRExprEngine::EvalBinOp(BinaryOperator::Opcode Op, SVal L, SVal R) {
+SVal GRExprEngine::EvalBinOp(BinaryOperator::Opcode Op, SVal L, SVal R,
+                             QualType T) {
   
   if (L.isUndef() || R.isUndef())
     return UndefinedVal();
@@ -2926,7 +2928,7 @@ SVal GRExprEngine::EvalBinOp(BinaryOperator::Opcode Op, SVal L, SVal R) {
   }
   else
     return getTF().DetermEvalBinOpNN(*this, Op, cast<NonLoc>(L),
-                                     cast<NonLoc>(R));
+                                     cast<NonLoc>(R), T);
 }
 
 //===----------------------------------------------------------------------===//
diff --git a/lib/Analysis/GRSimpleVals.cpp b/lib/Analysis/GRSimpleVals.cpp
index 22ccd7b8aa..3bd51ecd72 100644
--- a/lib/Analysis/GRSimpleVals.cpp
+++ b/lib/Analysis/GRSimpleVals.cpp
@@ -131,7 +131,8 @@ static unsigned char LNotOpMap[] = {
 
 SVal GRSimpleVals::DetermEvalBinOpNN(GRExprEngine& Eng,
                                      BinaryOperator::Opcode Op,
-                                     NonLoc L, NonLoc R)  {
+                                     NonLoc L, NonLoc R,
+                                     QualType T)  {
 
   BasicValueFactory& BasicVals = Eng.getBasicVals();
   unsigned subkind = L.getSubKind();
@@ -173,34 +174,35 @@ SVal GRSimpleVals::DetermEvalBinOpNN(GRExprEngine& Eng,
         }
       }
         
-      case nonloc::SymIntConstraintValKind: {
-        
+      case nonloc::SymExprValKind: {
         // Logical not?        
         if (!(Op == BinaryOperator::EQ && R.isZeroConstant()))
           return UnknownVal();
-        
-        const SymIntConstraint& C =
-          cast<nonloc::SymIntConstraintVal>(L).getConstraint();
-        
-        BinaryOperator::Opcode Opc = C.getOpcode();
-        
-        if (Opc < BinaryOperator::LT || Opc > BinaryOperator::NE)
-          return UnknownVal();
 
-        // For comparison operators, translate the constraint by
-        // changing the opcode.
+        const SymExpr &SE=*cast<nonloc::SymExprVal>(L).getSymbolicExpression();
         
-        int idx = (unsigned) Opc - (unsigned) BinaryOperator::LT;
+        // Only handle ($sym op constant) for now.
+        if (const SymIntExpr *E = dyn_cast<SymIntExpr>(&SE)) {
+          BinaryOperator::Opcode Opc = E->getOpcode();
         
-        assert (idx >= 0 && 
-                (unsigned) idx < sizeof(LNotOpMap)/sizeof(unsigned char));
+          if (Opc < BinaryOperator::LT || Opc > BinaryOperator::NE)
+            return UnknownVal();
+
+          // For comparison operators, translate the constraint by
+          // changing the opcode.        
+          int idx = (unsigned) Opc - (unsigned) BinaryOperator::LT;
         
-        Opc = (BinaryOperator::Opcode) LNotOpMap[idx];
+          assert (idx >= 0 && 
+                  (unsigned) idx < sizeof(LNotOpMap)/sizeof(unsigned char));
         
-        const SymIntConstraint& CNew =
-          BasicVals.getConstraint(C.getSymbol(), Opc, C.getInt());
+          Opc = (BinaryOperator::Opcode) LNotOpMap[idx];          
+          assert(E->getType(Eng.getContext()) == T);
+          E = Eng.getSymbolManager().getSymIntExpr(E->getLHS(), Opc,
+                                                   E->getRHS(), T);
+          return nonloc::SymExprVal(E);
+        }
         
-        return nonloc::SymIntConstraintVal(CNew);
+        return UnknownVal();
       }
         
       case nonloc::ConcreteIntKind:
@@ -231,14 +233,18 @@ SVal GRSimpleVals::DetermEvalBinOpNN(GRExprEngine& Eng,
       case nonloc::SymbolValKind:
         if (isa<nonloc::ConcreteInt>(R)) {
           if (Op >= BinaryOperator::LT && Op <= BinaryOperator::NE) {
-            const SymIntConstraint& C =
-              BasicVals.getConstraint(cast<nonloc::SymbolVal>(L).getSymbol(), 
-                                   Op, cast<nonloc::ConcreteInt>(R).getValue());
-            return nonloc::SymIntConstraintVal(C);
+            const SymIntExpr *SE =
+              Eng.getSymbolManager().getSymIntExpr(
+                                     cast<nonloc::SymbolVal>(L).getSymbol(), Op,
+                                     cast<nonloc::ConcreteInt>(R).getValue(),T);
+
+            
+            return nonloc::SymExprVal(SE);
           } else {
             return NonLoc::MakeVal(Eng.getSymbolManager(),
                                    cast<nonloc::SymbolVal>(L).getSymbol(),
-                                   Op, cast<nonloc::ConcreteInt>(R).getValue());
+                                   Op, cast<nonloc::ConcreteInt>(R).getValue(),
+                                   T);
           }
         }
         else
@@ -308,25 +314,28 @@ TryAgain:
       }
       else if (isa<loc::SymbolVal>(R)) {
         
-        const SymIntConstraint& C =
-          BasicVals.getConstraint(cast<loc::SymbolVal>(R).getSymbol(),
-                               BinaryOperator::EQ,
-                               cast<loc::ConcreteInt>(L).getValue());
+        const SymIntExpr *SE =
+          Eng.getSymbolManager().getSymIntExpr(cast<loc::SymbolVal>(R).getSymbol(),
+                                               BinaryOperator::EQ,
+                                               cast<loc::ConcreteInt>(L).getValue(),
+                                               Eng.getContext().IntTy);
         
-        return nonloc::SymIntConstraintVal(C);
+        return nonloc::SymExprVal(SE);
       }
       
       break;
       
     case loc::SymbolValKind: {
 
-      if (isa<loc::ConcreteInt>(R)) {          
-        const SymIntConstraint& C =
-          BasicVals.getConstraint(cast<loc::SymbolVal>(L).getSymbol(),
-                               BinaryOperator::EQ,
-                               cast<loc::ConcreteInt>(R).getValue());
+      if (isa<loc::ConcreteInt>(R)) {
+        const SymIntExpr *SE =
+          Eng.getSymbolManager().getSymIntExpr(
+                                            cast<loc::SymbolVal>(L).getSymbol(),
+                                            BinaryOperator::EQ,
+                                            cast<loc::ConcreteInt>(R).getValue(),
+                                            Eng.getContext().IntTy);
         
-        return nonloc::SymIntConstraintVal(C);
+        return nonloc::SymExprVal(SE);
       }
       
       // FIXME: Implement == for lval Symbols.  This is mainly useful
@@ -378,25 +387,27 @@ TryAgain:
         
         return NonLoc::MakeIntTruthVal(BasicVals, b);
       }
-      else if (isa<loc::SymbolVal>(R)) {        
-        const SymIntConstraint& C =
-          BasicVals.getConstraint(cast<loc::SymbolVal>(R).getSymbol(),
-                                  BinaryOperator::NE,
-                                  cast<loc::ConcreteInt>(L).getValue());
-        
-        return nonloc::SymIntConstraintVal(C);
+      else if (isa<loc::SymbolVal>(R)) {
+        const SymIntExpr * SE =
+        Eng.getSymbolManager().getSymIntExpr(
+                                    cast<loc::SymbolVal>(R).getSymbol(),
+                                    BinaryOperator::NE,
+                                    cast<loc::ConcreteInt>(L).getValue(),
+                                    Eng.getContext().IntTy);
+        return nonloc::SymExprVal(SE);
       }
       
       break;
 
     case loc::SymbolValKind: {
-      if (isa<loc::ConcreteInt>(R)) {          
-        const SymIntConstraint& C =
-          BasicVals.getConstraint(cast<loc::SymbolVal>(L).getSymbol(),
-                                  BinaryOperator::NE,
-                                  cast<loc::ConcreteInt>(R).getValue());
-        
-        return nonloc::SymIntConstraintVal(C);
+      if (isa<loc::ConcreteInt>(R)) {
+        const SymIntExpr *SE = 
+          Eng.getSymbolManager().getSymIntExpr(
+                                          cast<loc::SymbolVal>(L).getSymbol(),
+                                          BinaryOperator::NE,
+                                          cast<loc::ConcreteInt>(R).getValue(),
+                                          Eng.getContext().IntTy);
+        return nonloc::SymExprVal(SE);
       }
       
       // FIXME: Implement != for lval Symbols.  This is mainly useful
diff --git a/lib/Analysis/GRSimpleVals.h b/lib/Analysis/GRSimpleVals.h
index 6848ced2be..efe7c631ab 100644
--- a/lib/Analysis/GRSimpleVals.h
+++ b/lib/Analysis/GRSimpleVals.h
@@ -29,7 +29,7 @@ protected:
   
   virtual SVal DetermEvalBinOpNN(GRExprEngine& Eng,
                                  BinaryOperator::Opcode Op,
-                                 NonLoc L, NonLoc R);
+                                 NonLoc L, NonLoc R, QualType T);
   
 public:
   GRSimpleVals() {}
diff --git a/lib/Analysis/GRTransferFuncs.cpp b/lib/Analysis/GRTransferFuncs.cpp
index c08bd8f0b1..69c09d9a2e 100644
--- a/lib/Analysis/GRTransferFuncs.cpp
+++ b/lib/Analysis/GRTransferFuncs.cpp
@@ -21,7 +21,8 @@ void GRTransferFuncs::EvalBinOpNN(GRStateSet& OStates,
                                   GRExprEngine& Eng,
                                   const GRState *St, Expr* Ex,
                                   BinaryOperator::Opcode Op,
-                                  NonLoc L, NonLoc R) {
+                                  NonLoc L, NonLoc R, QualType T) {
   
-  OStates.Add(Eng.getStateManager().BindExpr(St, Ex, DetermEvalBinOpNN(Eng, Op, L, R)));
+  OStates.Add(Eng.getStateManager().BindExpr(St, Ex,
+                                          DetermEvalBinOpNN(Eng, Op, L, R, T)));
 }
diff --git a/lib/Analysis/MemRegion.cpp b/lib/Analysis/MemRegion.cpp
index 5bfc989eb8..738e8c67d6 100644
--- a/lib/Analysis/MemRegion.cpp
+++ b/lib/Analysis/MemRegion.cpp
@@ -112,10 +112,8 @@ void ElementRegion::Profile(llvm::FoldingSetNodeID& ID) const {
 //===----------------------------------------------------------------------===//
 
 QualType SymbolicRegion::getRValueType(ASTContext& C) const {
-  const SymbolData& data = SymMgr.getSymbolData(sym);
-
   // Get the type of the symbol.
-  QualType T = data.getType(C);
+  QualType T = sym->getType(C);
 
   if (const PointerType* PTy = T->getAsPointerType())
     return PTy->getPointeeType();
@@ -132,8 +130,7 @@ QualType SymbolicRegion::getRValueType(ASTContext& C) const {
 }
 
 QualType SymbolicRegion::getLValueType(ASTContext& C) const {
-  const SymbolData& data = SymMgr.getSymbolData(sym);
-  return data.getType(C);
+  return sym->getType(C);
 }
 
 QualType ElementRegion::getRValueType(ASTContext& C) const {
@@ -332,12 +329,9 @@ MemRegionManager::getElementRegion(SVal Idx, const TypedRegion* superRegion){
 }
 
 /// getSymbolicRegion - Retrieve or create a "symbolic" memory region.
-SymbolicRegion* MemRegionManager::getSymbolicRegion(const SymbolRef sym,
-                                                    const SymbolManager& mgr) {
-  
+SymbolicRegion* MemRegionManager::getSymbolicRegion(SymbolRef sym) {
   llvm::FoldingSetNodeID ID;
   SymbolicRegion::ProfileRegion(ID, sym);
-  
   void* InsertPos;
   MemRegion* data = Regions.FindNodeOrInsertPos(ID, InsertPos);
   SymbolicRegion* R = cast_or_null<SymbolicRegion>(data);
@@ -345,7 +339,7 @@ SymbolicRegion* MemRegionManager::getSymbolicRegion(const SymbolRef sym,
   if (!R) {
     R = (SymbolicRegion*) A.Allocate<SymbolicRegion>();
     // SymbolicRegion's storage class is usually unknown.
-    new (R) SymbolicRegion(sym, mgr, getUnknownRegion());
+    new (R) SymbolicRegion(sym, getUnknownRegion());
     Regions.InsertNode(R, InsertPos);
   }
   
diff --git a/lib/Analysis/RegionStore.cpp b/lib/Analysis/RegionStore.cpp
index 78dda87392..f23369c8e1 100644
--- a/lib/Analysis/RegionStore.cpp
+++ b/lib/Analysis/RegionStore.cpp
@@ -367,8 +367,7 @@ SVal RegionStoreManager::getLValueFieldOrIvar(const GRState* St, SVal Base,
     break;
 
   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:
@@ -412,11 +411,9 @@ SVal RegionStoreManager::getLValueElement(const GRState* St,
 
   const TypedRegion* BaseRegion = 0;
 
-  if (isa<loc::SymbolVal>(Base))
-    BaseRegion = MRMgr.getSymbolicRegion(cast<loc::SymbolVal>(Base).getSymbol(),
-                                         StateMgr.getSymbolManager());
-  else
-    BaseRegion = cast<TypedRegion>(cast<loc::MemRegionVal>(Base).getRegion());
+  BaseRegion = isa<loc::SymbolVal>(Base)
+               ? MRMgr.getSymbolicRegion(cast<loc::SymbolVal>(Base).getSymbol())
+               : cast<TypedRegion>(cast<loc::MemRegionVal>(Base).getRegion());
 
   // Pointer of any type can be cast and used as array base.
   const ElementRegion *ElemR = dyn_cast<ElementRegion>(BaseRegion);
@@ -862,8 +859,7 @@ Store RegionStoreManager::Remove(Store store, Loc L) {
   if (isa<loc::MemRegionVal>(L))
     R = cast<loc::MemRegionVal>(L).getRegion();
   else if (isa<loc::SymbolVal>(L))
-    R = MRMgr.getSymbolicRegion(cast<loc::SymbolVal>(L).getSymbol(),
-                                StateMgr.getSymbolManager());
+    R = MRMgr.getSymbolicRegion(cast<loc::SymbolVal>(L).getSymbol());
   
   if (R) {
     RegionBindingsTy B = GetRegionBindings(store);  
diff --git a/lib/Analysis/SVals.cpp b/lib/Analysis/SVals.cpp
index 0f345602a2..9225f994d3 100644
--- a/lib/Analysis/SVals.cpp
+++ b/lib/Analysis/SVals.cpp
@@ -22,37 +22,13 @@ using llvm::cast;
 using llvm::APSInt;
 
 //===----------------------------------------------------------------------===//
-// Symbol Iteration.
+// Symbol iteration within an SVal.
 //===----------------------------------------------------------------------===//
 
-SVal::symbol_iterator SVal::symbol_begin() const {
-  // FIXME: This is a rat's nest.  Cleanup.
-
-  if (isa<loc::SymbolVal>(this))
-    return symbol_iterator(SymbolRef((uintptr_t)Data));
-  else if (isa<nonloc::SymbolVal>(this))
-    return symbol_iterator(SymbolRef((uintptr_t)Data));
-  else if (isa<nonloc::SymIntConstraintVal>(this)) {
-    const SymIntConstraint& C =
-      cast<nonloc::SymIntConstraintVal>(this)->getConstraint();    
-    return symbol_iterator(C.getSymbol());
-  }
-  else if (isa<nonloc::LocAsInteger>(this)) {
-    const nonloc::LocAsInteger& V = cast<nonloc::LocAsInteger>(*this);
-    return V.getPersistentLoc().symbol_begin();
-  }
-  else if (isa<loc::MemRegionVal>(this)) {
-    const MemRegion* R = cast<loc::MemRegionVal>(this)->getRegion();
-    if (const SymbolicRegion* S = dyn_cast<SymbolicRegion>(R))
-      return symbol_iterator(S->getSymbol());
-  }
-  
-  return symbol_iterator();
-}
 
-SVal::symbol_iterator SVal::symbol_end() const {
-  return symbol_iterator();
-}
+//===----------------------------------------------------------------------===//
+// Utility methods.
+//===----------------------------------------------------------------------===//
 
 /// getAsLocSymbol - If this SVal is a location (subclasses Loc) and 
 ///  wraps a symbol, return that SymbolRef.  Otherwise return a SymbolRef
@@ -78,7 +54,7 @@ SymbolRef SVal::getAsLocSymbol() const {
     }
   }
   
-  return SymbolRef();
+  return 0;
 }
 
 /// getAsSymbol - If this Sval wraps a symbol return that SymbolRef.
@@ -87,9 +63,66 @@ SymbolRef SVal::getAsSymbol() const {
   if (const nonloc::SymbolVal *X = dyn_cast<nonloc::SymbolVal>(this))
     return X->getSymbol();
   
+  if (const nonloc::SymExprVal *X = dyn_cast<nonloc::SymExprVal>(this))
+    if (SymbolRef Y = dyn_cast<SymbolData>(X->getSymbolicExpression()))
+      return Y;
+  
   return getAsLocSymbol();
 }
 
+/// getAsSymbolicExpression - If this Sval wraps a symbolic expression then
+///  return that expression.  Otherwise return NULL.
+const SymExpr *SVal::getAsSymbolicExpression() const {
+  if (const nonloc::SymExprVal *X = dyn_cast<nonloc::SymExprVal>(this))
+    return X->getSymbolicExpression();
+  
+  return getAsSymbol();
+}
+
+bool SVal::symbol_iterator::operator==(const symbol_iterator &X) const {
+  return itr == X.itr;
+}
+
+bool SVal::symbol_iterator::operator!=(const symbol_iterator &X) const {
+  return itr != X.itr;
+}
+
+SVal::symbol_iterator::symbol_iterator(const SymExpr *SE) {
+  itr.push_back(SE);
+  while (!isa<SymbolData>(itr.back())) expand();  
+}
+
+SVal::symbol_iterator& SVal::symbol_iterator::operator++() {
+  assert(!itr.empty() && "attempting to iterate on an 'end' iterator");
+  assert(isa<SymbolData>(itr.back()));
+  itr.pop_back();         
+  if (!itr.empty())
+    while (!isa<SymbolData>(itr.back())) expand();
+  return *this;
+}
+
+SymbolRef SVal::symbol_iterator::operator*() {
+  assert(!itr.empty() && "attempting to dereference an 'end' iterator");
+  return cast<SymbolData>(itr.back());
+}
+
+void SVal::symbol_iterator::expand() {
+  const SymExpr *SE = itr.back();
+  itr.pop_back();
+    
+  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
+    itr.push_back(SIE->getLHS());
+    return;
+  }  
+  else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
+    itr.push_back(SSE->getLHS());
+    itr.push_back(SSE->getRHS());
+    return;
+  }
+  
+  assert(false && "unhandled expansion case");
+}
+
 //===----------------------------------------------------------------------===//
 // Other Iterators.
 //===----------------------------------------------------------------------===//
@@ -168,7 +201,7 @@ SVal loc::ConcreteInt::EvalBinOp(BasicValueFactory& BasicVals,
     return UndefinedVal();
 }
 
-NonLoc Loc::EQ(BasicValueFactory& BasicVals, const Loc& R) const {
+NonLoc Loc::EQ(SymbolManager& SymMgr, const Loc& R) const {
   
   switch (getSubKind()) {
     default:
@@ -180,49 +213,48 @@ NonLoc Loc::EQ(BasicValueFactory& BasicVals, const Loc& R) const {
         bool b = cast<loc::ConcreteInt>(this)->getValue() ==
                  cast<loc::ConcreteInt>(R).getValue();
         
-        return NonLoc::MakeIntTruthVal(BasicVals, b);
+        return NonLoc::MakeIntTruthVal(SymMgr.getBasicVals(), b);
       }
       else if (isa<loc::SymbolVal>(R)) {
-        
-        const SymIntConstraint& C =
-          BasicVals.getConstraint(cast<loc::SymbolVal>(R).getSymbol(),
+        const SymIntExpr *SE =
+          SymMgr.getSymIntExpr(cast<loc::SymbolVal>(R).getSymbol(),
                                BinaryOperator::EQ,
-                               cast<loc::ConcreteInt>(this)->getValue());
+                               cast<loc::ConcreteInt>(this)->getValue(),
+                               SymMgr.getContext().IntTy);
         
-        return nonloc::SymIntConstraintVal(C);        
+        return nonloc::SymExprVal(SE);        
       }
       
       break;
       
       case loc::SymbolValKind: {
         if (isa<loc::ConcreteInt>(R)) {
-          
-          const SymIntConstraint& C =
-            BasicVals.getConstraint(cast<loc::SymbolVal>(this)->getSymbol(),
+          const SymIntExpr *SE =
+            SymMgr.getSymIntExpr(cast<loc::SymbolVal>(this)->getSymbol(),
                                  BinaryOperator::EQ,
-                                 cast<loc::ConcreteInt>(R).getValue());
+                                 cast<loc::ConcreteInt>(R).getValue(),
+                                 SymMgr.getContext().IntTy);
           
-          return nonloc::SymIntConstraintVal(C);
+          return nonloc::SymExprVal(SE);
         }
-        
-        assert (!isa<loc::SymbolVal>(R) && "FIXME: Implement unification.");
-        
+                                 
+        assert (!isa<loc::SymbolVal>(R) && "FIXME: Implement unification.");        
         break;
       }
       
       case loc::MemRegionKind:
       if (isa<loc::MemRegionVal>(R)) {        
         bool b = cast<loc::MemRegionVal>(*this) == cast<loc::MemRegionVal>(R);
-        return NonLoc::MakeIntTruthVal(BasicVals, b);
+        return NonLoc::MakeIntTruthVal(SymMgr.getBasicVals(), b);
       }
       
       break;
   }
   
-  return NonLoc::MakeIntTruthVal(BasicVals, false);
+  return NonLoc::MakeIntTruthVal(SymMgr.getBasicVals(), false);
 }
 
-NonLoc Loc::NE(BasicValueFactory& BasicVals, const Loc& R) const {
+NonLoc Loc::NE(SymbolManager& SymMgr, const Loc& R) const {
   switch (getSubKind()) {
     default:
       assert(false && "NE not implemented for this Loc.");
@@ -233,46 +265,43 @@ NonLoc Loc::NE(BasicVa