Lazy bingding for region-store manager.

* Now Bind() methods take and return GRState* because binding could
  also alter GDM.
* No variables are initialized except those declared with initial
  values.
* failed C test cases are due to bugs in RemoveDeadBindings(),
which removes constraints that is still alive. This will be fixed in later
patch.
* default value of array and struct regions will be implemented in later patch.


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

14 files changed, 372 insertions, 456 deletions

diff --git a/include/clang/Analysis/PathSensitive/GRState.h b/include/clang/Analysis/PathSensitive/GRState.h
index 483f16ed7d..27df2bbdb6 100644
--- a/include/clang/Analysis/PathSensitive/GRState.h
+++ b/include/clang/Analysis/PathSensitive/GRState.h
@@ -336,15 +336,24 @@ public:
 
   typedef StoreManager::DeadSymbolsTy DeadSymbolsTy;
 
-  const GRState* BindDecl(const GRState* St, const VarDecl* VD, SVal* IVal,
-                          unsigned Count);
+  const GRState* BindDecl(const GRState* St, const VarDecl* VD, SVal IVal) {
+    // Store manager should return a persistent state.
+    return StoreMgr->BindDecl(St, VD, IVal);
+  }
+
+  const GRState* BindDeclWithNoInit(const GRState* St, const VarDecl* VD) {
+    // Store manager should return a persistent state.
+    return StoreMgr->BindDeclWithNoInit(St, VD);
+  }
   
   /// BindCompoundLiteral - Return the state that has the bindings currently
   ///  in 'state' plus the bindings for the CompoundLiteral.  'R' is the region
   ///  for the compound literal and 'BegInit' and 'EndInit' represent an
   ///  array of initializer values.
-  const GRState* BindCompoundLiteral(const GRState* state,
-                                     const CompoundLiteralExpr* CL, SVal V);
+  const GRState* BindCompoundLiteral(const GRState* St,
+                                     const CompoundLiteralExpr* CL, SVal V) {
+    return StoreMgr->BindCompoundLiteral(St, CL, V);
+  }
 
   const GRState* RemoveDeadBindings(const GRState* St, Stmt* Loc, 
                                     const LiveVariables& Liveness,
@@ -468,11 +477,9 @@ public:
     return StoreMgr->GetRegionSVal(state, R);
   }  
   
-  void BindLoc(GRState& St, Loc LV, SVal V) {
-    St.St = StoreMgr->Bind(St.St, LV, V);
+  const GRState* BindLoc(const GRState* St, Loc LV, SVal V) {
+    return StoreMgr->Bind(St, LV, V);
   }
-  
-  const GRState* BindLoc(const GRState* St, Loc LV, SVal V);  
 
   void Unbind(GRState& St, Loc LV) {
     St.St = StoreMgr->Remove(St.St, LV);
@@ -481,6 +488,9 @@ public:
   const GRState* Unbind(const GRState* St, Loc LV);
   
   const GRState* getPersistentState(GRState& Impl);
+
+  // MakeStateWithStore - get a persistent state with the new store.
+  const GRState* MakeStateWithStore(const GRState* St, Store store);
   
   bool isEqual(const GRState* state, Expr* Ex, const llvm::APSInt& V);
   bool isEqual(const GRState* state, Expr* Ex, uint64_t);
@@ -501,7 +511,15 @@ public:
     return addGDM(st, GRStateTrait<T>::GDMIndex(), 
      GRStateTrait<T>::MakeVoidPtr(GRStateTrait<T>::Set(st->get<T>(), K, V, C)));
   }
-  
+
+  template <typename T>
+  const GRState* add(const GRState* st,
+                     typename GRStateTrait<T>::key_type K,
+                     typename GRStateTrait<T>::context_type C) {
+    return addGDM(st, GRStateTrait<T>::GDMIndex(),
+        GRStateTrait<T>::MakeVoidPtr(GRStateTrait<T>::Add(st->get<T>(), K, C)));
+  }
+
   template <typename T>
   const GRState* remove(const GRState* st,
                         typename GRStateTrait<T>::key_type K,
@@ -587,14 +605,12 @@ public:
     return GRStateRef(Mgr->BindExpr(St, Ex, V, Invalidate), *Mgr);
   }
     
-  GRStateRef BindDecl(const VarDecl* VD, SVal* InitVal, unsigned Count) {
-    return GRStateRef(Mgr->BindDecl(St, VD, InitVal, Count), *Mgr);
+  GRStateRef BindDecl(const VarDecl* VD, SVal InitVal) {
+    return GRStateRef(Mgr->BindDecl(St, VD, InitVal), *Mgr);
   }
   
   GRStateRef BindLoc(Loc LV, SVal V) {
-    GRState StImpl = *St;
-    Mgr->BindLoc(StImpl, LV, V);    
-    return GRStateRef(Mgr->getPersistentState(StImpl), *Mgr);
+    return GRStateRef(Mgr->BindLoc(St, LV, V), *Mgr);
   }
   
   GRStateRef BindLoc(SVal LV, SVal V) {
@@ -644,7 +660,12 @@ public:
                  typename GRStateTrait<T>::value_type E) {
     return GRStateRef(Mgr->set<T>(St, K, E, get_context<T>()), *Mgr);
   }  
-  
+
+  template<typename T>
+  GRStateRef add(typename GRStateTrait<T>::key_type K) {
+    return GRStateRef(Mgr->add<T>(St, K, get_context<T>()), *Mgr);
+  }
+
   template<typename T>
   GRStateRef remove(typename GRStateTrait<T>::key_type K,
                     typename GRStateTrait<T>::context_type C) {
@@ -658,7 +679,7 @@ public:
   
   template<typename T>
   bool contains(typename GRStateTrait<T>::key_type key) const {
-    return St->contains(key);
+    return St->contains<T>(key);
   }
   
   // Lvalue methods.
diff --git a/include/clang/Analysis/PathSensitive/MemRegion.h b/include/clang/Analysis/PathSensitive/MemRegion.h
index efe0b9a19c..40c6fde51e 100644
--- a/include/clang/Analysis/PathSensitive/MemRegion.h
+++ b/include/clang/Analysis/PathSensitive/MemRegion.h
@@ -99,7 +99,7 @@ public:
   const MemRegion* getSuperRegion() const {
     return superRegion;
   }
-  
+
   static bool classof(const MemRegion* R) {
     return R->getKind() > SymbolicRegionKind;
   }
@@ -466,6 +466,12 @@ public:
     assert(R);
     return R == globals; 
   }
+
+  /// onStack - check if the region is allocated on the stack.
+  bool onStack(const MemRegion* R);
+
+  /// onHeap - check if the region is allocated on the heap, usually by malloc.
+  bool onHeap(const MemRegion* R);
   
   /// getAllocaRegion - Retrieve a region associated with a call to alloca().
   AllocaRegion* getAllocaRegion(const Expr* Ex, unsigned Cnt);
diff --git a/include/clang/Analysis/PathSensitive/SVals.h b/include/clang/Analysis/PathSensitive/SVals.h
index 361e321823..ca36187530 100644
--- a/include/clang/Analysis/PathSensitive/SVals.h
+++ b/include/clang/Analysis/PathSensitive/SVals.h
@@ -71,7 +71,13 @@ public:
   inline bool operator!=(const SVal& R) const {
     return !(*this == R);
   }
-  
+
+  /// MakeSymbolValue - make a unique symbol value for the region R according to
+  /// its kind. R should be a scalar region. The symbol value T has the same
+  /// type as R's rvalue type.
+  static SVal MakeSymbolValue(SymbolManager& SymMgr, const MemRegion* R, 
+                              QualType T);
+
   static SVal GetSymbolValue(SymbolManager& SymMgr, VarDecl *D);
   static SVal getSymbolValue(SymbolManager& SymMgr, const MemRegion* R,
                              const llvm::APSInt* Idx, QualType T);
@@ -171,6 +177,8 @@ public:
   
   // Utility methods to create NonLocs.
 
+  static NonLoc MakeVal(SymbolRef sym);
+
   static NonLoc MakeVal(BasicValueFactory& BasicVals, unsigned X, 
                         bool isUnsigned);
 
@@ -212,6 +220,8 @@ public:
   static Loc MakeVal(const MemRegion* R);
     
   static Loc MakeVal(AddrLabelExpr* E);
+
+  static Loc MakeVal(SymbolRef sym);
   
   // Implement isa<T> support.
   static inline bool classof(const SVal* V) {
diff --git a/include/clang/Analysis/PathSensitive/Store.h b/include/clang/Analysis/PathSensitive/Store.h
index ca21e20244..5425b6976b 100644
--- a/include/clang/Analysis/PathSensitive/Store.h
+++ b/include/clang/Analysis/PathSensitive/Store.h
@@ -49,16 +49,19 @@ public:
   SVal GetRegionSVal(const GRState* state, const MemRegion* R) {
     return Retrieve(state, loc::MemRegionVal(R));
   }
-  
-  virtual Store Bind(Store St, Loc LV, SVal V) = 0;
-  virtual Store Remove(Store St, Loc LV) = 0;
+
+  /// Bind value V to location L.
+  virtual const GRState* Bind(const GRState* St, Loc L, SVal V) = 0;
+
+  virtual Store Remove(Store St, Loc L) = 0;
   
   /// BindCompoundLiteral - Return the store that has the bindings currently
   ///  in 'store' plus the bindings for the CompoundLiteral.  'R' is the region
   ///  for the compound literal and 'BegInit' and 'EndInit' represent an
   ///  array of initializer values.
-  virtual Store BindCompoundLiteral(Store store, const CompoundLiteralExpr* CL,
-                                    SVal V) = 0;
+  virtual const GRState* BindCompoundLiteral(const GRState* St, 
+                                             const CompoundLiteralExpr* CL,
+                                             SVal V) = 0;
   
   virtual Store getInitialStore() = 0;
   virtual MemRegionManager& getRegionManager() = 0;
@@ -112,8 +115,11 @@ public:
                      llvm::SmallVectorImpl<const MemRegion*>& RegionRoots,
                      LiveSymbolsTy& LSymbols, DeadSymbolsTy& DSymbols) = 0;
 
-  virtual Store BindDecl(Store store, const VarDecl* VD, SVal* InitVal,
-                         unsigned Count) = 0;
+  virtual const GRState* BindDecl(const GRState* St, const VarDecl* VD, 
+                                  SVal InitVal) = 0;
+
+  virtual const GRState* BindDeclWithNoInit(const GRState* St, 
+                                            const VarDecl* VD) = 0;
 
   virtual const GRState* setExtent(const GRState* St,
                                    const MemRegion* R, SVal Extent) {
diff --git a/include/clang/Analysis/PathSensitive/SymbolManager.h b/include/clang/Analysis/PathSensitive/SymbolManager.h
index 1adc7c6eaf..8785293494 100644
--- a/include/clang/Analysis/PathSensitive/SymbolManager.h
+++ b/include/clang/Analysis/PathSensitive/SymbolManager.h
@@ -104,15 +104,15 @@ public:
 };
 
 class SymbolDataParmVar : public SymbolData {
-  ParmVarDecl *VD;
+  const ParmVarDecl *VD;
 
 public:  
-  SymbolDataParmVar(SymbolRef MySym, ParmVarDecl* vd)
+  SymbolDataParmVar(SymbolRef MySym, const ParmVarDecl* vd)
     : SymbolData(ParmKind, MySym), VD(vd) {}
   
-  ParmVarDecl* getDecl() const { return VD; }  
+  const ParmVarDecl* getDecl() const { return VD; }  
   
-  static void Profile(llvm::FoldingSetNodeID& profile, ParmVarDecl* VD) {
+  static void Profile(llvm::FoldingSetNodeID& profile, const ParmVarDecl* VD) {
     profile.AddInteger((unsigned) ParmKind);
     profile.AddPointer(VD);
   }
@@ -128,15 +128,15 @@ public:
 };
   
 class SymbolDataGlobalVar : public SymbolData {
-  VarDecl *VD;
+  const VarDecl *VD;
 
 public:
-  SymbolDataGlobalVar(SymbolRef MySym, VarDecl* vd) :
+  SymbolDataGlobalVar(SymbolRef MySym, const VarDecl* vd) :
     SymbolData(GlobalKind, MySym), VD(vd) {}
   
-  VarDecl* getDecl() const { return VD; }
+  const VarDecl* getDecl() const { return VD; }
   
-  static void Profile(llvm::FoldingSetNodeID& profile, VarDecl* VD) {
+  static void Profile(llvm::FoldingSetNodeID& profile, const VarDecl* VD) {
     profile.AddInteger((unsigned) GlobalKind);
     profile.AddPointer(VD);
   }
@@ -275,8 +275,10 @@ public:
     : SymbolCounter(0), BPAlloc(bpalloc) {}
   
   ~SymbolManager();
-  
-  SymbolRef getSymbol(VarDecl* D);
+
+  /// Make a unique symbol for MemRegion R according to its kind.
+  SymbolRef getSymbol(const MemRegion* R);
+  SymbolRef getSymbol(const VarDecl* D);
   SymbolRef getElementSymbol(const MemRegion* R, const llvm::APSInt* Idx);
   SymbolRef getFieldSymbol(const MemRegion* R, const FieldDecl* D);
   SymbolRef getConjuredSymbol(Stmt* E, QualType T, unsigned VisitCount);
diff --git a/lib/Analysis/BasicStore.cpp b/lib/Analysis/BasicStore.cpp
index 1febba675d..07163d51e3 100644
--- a/lib/Analysis/BasicStore.cpp
+++ b/lib/Analysis/BasicStore.cpp
@@ -39,7 +39,14 @@ public:
   ~BasicStoreManager() {}
 
   SVal Retrieve(const GRState *state, Loc LV, QualType T);  
-  Store Bind(Store St, Loc LV, SVal V);  
+
+  const GRState* Bind(const GRState* St, Loc L, SVal V) {
+    Store store = St->getStore();
+    store = BindInternal(store, L, V);
+    return StateMgr.MakeStateWithStore(St, store);
+  }
+
+  Store BindInternal(Store St, Loc LV, SVal V);  
   Store Remove(Store St, Loc LV);
   Store getInitialStore();
   MemRegionManager& getRegionManager() { return MRMgr; }
@@ -49,9 +56,10 @@ public:
     return loc::MemRegionVal(MRMgr.getVarRegion(VD));
   }
   
-  Store BindCompoundLiteral(Store store, const CompoundLiteralExpr* CL,
-                            SVal V) {
-    return store;
+  const GRState* BindCompoundLiteral(const GRState* St, 
+                                     const CompoundLiteralExpr* CL,
+                                     SVal V) {
+    return St;
   }
   
   SVal getLValueVar(const GRState* St, const VarDecl* VD);
@@ -89,7 +97,25 @@ public:
 
   void iterBindings(Store store, BindingsHandler& f);
 
-  Store BindDecl(Store store, const VarDecl* VD, SVal* InitVal, unsigned Count);
+  const GRState* BindDecl(const GRState* St, const VarDecl* VD, SVal InitVal) {
+    Store store = St->getStore();
+    store = BindDeclInternal(store, VD, &InitVal);
+    return StateMgr.MakeStateWithStore(St, store);
+  }
+
+  const GRState* BindDeclWithNoInit(const GRState* St, const VarDecl* VD) {
+    Store store = St->getStore();
+    store = BindDeclInternal(store, VD, 0);
+    return StateMgr.MakeStateWithStore(St, store);
+  }
+
+  const GRState* BindDecl(const GRState* St, const VarDecl* VD) {
+    Store store = St->getStore();
+    store = BindDeclInternal(store, VD, 0);
+    return StateMgr.MakeStateWithStore(St, store);
+  }
+
+  Store BindDeclInternal(Store store, const VarDecl* VD, SVal* InitVal);
 
   static inline VarBindingsTy GetVarBindings(Store store) {
     return VarBindingsTy(static_cast<const VarBindingsTy::TreeTy*>(store));
@@ -286,7 +312,7 @@ SVal BasicStoreManager::Retrieve(const GRState* state, Loc LV, QualType T) {
   return UnknownVal();
 }
   
-Store BasicStoreManager::Bind(Store store, Loc LV, SVal V) {    
+Store BasicStoreManager::BindInternal(Store store, Loc LV, SVal V) {    
   switch (LV.getSubKind()) {      
     case loc::MemRegionKind: {
       const VarRegion* R =
@@ -421,8 +447,8 @@ Store BasicStoreManager::getInitialStore() {
           SelfRegion = MRMgr.getObjCObjectRegion(MD->getClassInterface(),
                                                  MRMgr.getHeapRegion());
           
-          St = Bind(St, loc::MemRegionVal(MRMgr.getVarRegion(PD)),
-                        loc::MemRegionVal(SelfRegion));
+          St = BindInternal(St, loc::MemRegionVal(MRMgr.getVarRegion(PD)),
+                            loc::MemRegionVal(SelfRegion));
         }
       }
     }
@@ -441,15 +467,15 @@ Store BasicStoreManager::getInitialStore() {
                  ? SVal::GetSymbolValue(StateMgr.getSymbolManager(), VD)
                  : UndefinedVal();
 
-        St = Bind(St, loc::MemRegionVal(MRMgr.getVarRegion(VD)), X);
+        St = BindInternal(St, loc::MemRegionVal(MRMgr.getVarRegion(VD)), X);
       }
     }
   }
   return St;
 }
 
-Store BasicStoreManager::BindDecl(Store store, const VarDecl* VD,
-                                  SVal* InitVal, unsigned Count) {
+Store BasicStoreManager::BindDeclInternal(Store store, const VarDecl* VD,
+                                          SVal* InitVal) {
                  
   BasicValueFactory& BasicVals = StateMgr.getBasicVals();
                  
@@ -479,16 +505,16 @@ Store BasicStoreManager::BindDecl(Store store, const VarDecl* VD,
       if (!InitVal) {
         QualType T = VD->getType();
         if (Loc::IsLocType(T))
-          store = Bind(store, getLoc(VD),
+          store = BindInternal(store, getLoc(VD),
                        loc::ConcreteInt(BasicVals.getValue(0, T)));
         else if (T->isIntegerType())
-          store = Bind(store, getLoc(VD),
+          store = BindInternal(store, getLoc(VD),
                        nonloc::ConcreteInt(BasicVals.getValue(0, T)));
         else {
           // assert(0 && "ignore other types of variables");
         }
       } else {
-        store = Bind(store, getLoc(VD), *InitVal);
+        store = BindInternal(store, getLoc(VD), *InitVal);
       }
     }
   } else {
@@ -496,7 +522,7 @@ Store BasicStoreManager::BindDecl(Store store, const VarDecl* VD,
     QualType T = VD->getType();
     if (Loc::IsLocType(T) || T->isIntegerType()) {
       SVal V = InitVal ? *InitVal : UndefinedVal();
-      store = Bind(store, getLoc(VD), V);
+      store = BindInternal(store, getLoc(VD), V);
     }
   }
 
diff --git a/lib/Analysis/GRExprEngine.cpp b/lib/Analysis/GRExprEngine.cpp
index e6c12ead89..0dd6b5fa68 100644
--- a/lib/Analysis/GRExprEngine.cpp
+++ b/lib/Analysis/GRExprEngine.cpp
@@ -1811,7 +1811,8 @@ void GRExprEngine::VisitDeclStmt(DeclStmt* DS, NodeTy* Pred, NodeSet& Dst) {
   for (NodeSet::iterator I=Tmp.begin(), E=Tmp.end(); I!=E; ++I) {
     const GRState* St = GetState(*I);
     unsigned Count = Builder->getCurrentBlockCount();
-        
+
+    // Decls without InitExpr are not initialized explicitly.
     if (InitEx) {
       SVal InitVal = GetSVal(St, InitEx);
       QualType T = VD->getType();
@@ -1829,11 +1830,9 @@ void GRExprEngine::VisitDeclStmt(DeclStmt* DS, NodeTy* Pred, NodeSet& Dst) {
         }
       }        
       
-      St = StateMgr.BindDecl(St, VD, &InitVal, Count);
-    }
-    else
-      St = StateMgr.BindDecl(St, VD, 0, Count);
-    
+      St = StateMgr.BindDecl(St, VD, InitVal);
+    } else
+      St = StateMgr.BindDeclWithNoInit(St, VD);
     
     // Check if 'VD' is a VLA and if so check if has a non-zero size.
     QualType T = getContext().getCanonicalType(VD->getType());
diff --git a/lib/Analysis/GRState.cpp b/lib/Analysis/GRState.cpp
index 221ab064d3..8e49ebb63d 100644
--- a/lib/Analysis/GRState.cpp
+++ b/lib/Analysis/GRState.cpp
@@ -59,51 +59,6 @@ GRStateManager::RemoveDeadBindings(const GRState* state, Stmt* Loc,
                                            LSymbols, DSymbols);
 }
 
-const GRState* GRStateManager::BindLoc(const GRState* St, Loc LV, SVal V) {
-  
-  Store OldStore = St->getStore();
-  Store NewStore = StoreMgr->Bind(OldStore, LV, V);
-  
-  if (NewStore == OldStore)
-    return St;
-  
-  GRState NewSt = *St;
-  NewSt.St = NewStore;
-  return getPersistentState(NewSt);    
-}
-
-const GRState* GRStateManager::BindDecl(const GRState* St, const VarDecl* VD, 
-                                        SVal* InitVal, unsigned Count) {
-  Store OldStore = St->getStore();
-  Store NewStore = StoreMgr->BindDecl(OldStore, VD, InitVal, Count);
-
-  if (NewStore == OldStore)
-    return St;
-  
-  GRState NewSt = *St;
-  NewSt.St = NewStore;
-  return getPersistentState(NewSt);
-}
-
-/// BindCompoundLiteral - Return the store that has the bindings currently
-///  in 'store' plus the bindings for the CompoundLiteral.  'R' is the region
-///  for the compound literal and 'BegInit' and 'EndInit' represent an
-///  array of initializer values.
-const GRState*
-GRStateManager::BindCompoundLiteral(const GRState* state,
-                                    const CompoundLiteralExpr* CL, SVal ILV) {
-
-  Store oldStore = state->getStore();
-  Store newStore = StoreMgr->BindCompoundLiteral(oldStore, CL, ILV);
-  
-  if (newStore == oldStore)
-    return state;
-  
-  GRState newState = *state;
-  newState.St = newStore;
-  return getPersistentState(newState);
-}
-
 const GRState* GRStateManager::Unbind(const GRState* St, Loc LV) {
   Store OldStore = St->getStore();
   Store NewStore = StoreMgr->Remove(OldStore, LV);
@@ -140,6 +95,13 @@ const GRState* GRStateManager::getPersistentState(GRState& State) {
   return I;
 }
 
+const GRState* GRStateManager::MakeStateWithStore(const GRState* St, 
+                                                  Store store) {
+  GRState NewSt = *St;
+  NewSt.St = store;
+  return getPersistentState(NewSt);
+}
+
 
 //===----------------------------------------------------------------------===//
 //  State pretty-printing.
diff --git a/lib/Analysis/MemRegion.cpp b/lib/Analysis/MemRegion.cpp
index eafeee66d5..8767781354 100644
--- a/lib/Analysis/MemRegion.cpp
+++ b/lib/Analysis/MemRegion.cpp
@@ -215,6 +215,20 @@ MemSpaceRegion* MemRegionManager::getUnknownRegion() {
   return LazyAllocate(unknown);
 }
 
+bool MemRegionManager::onStack(const MemRegion* R) {
+  while (const SubRegion* SR = dyn_cast<SubRegion>(R))
+    R = SR->getSuperRegion();
+
+  return (R != 0) && (R == stack);
+}
+
+bool MemRegionManager::onHeap(const MemRegion* R) {
+  while (const SubRegion* SR = dyn_cast<SubRegion>(R))
+    R = SR->getSuperRegion();
+
+  return (R != 0) && (R == heap); 
+}
+
 StringRegion* MemRegionManager::getStringRegion(const StringLiteral* Str) {
   llvm::FoldingSetNodeID ID;
   MemSpaceRegion* GlobalsR = getGlobalsRegion();
diff --git a/lib/Analysis/RegionStore.cpp b/lib/Analysis/RegionStore.cpp
index 98b408156f..06292d20d8 100644
--- a/lib/Analysis/RegionStore.cpp
+++ b/lib/Analysis/RegionStore.cpp
@@ -62,6 +62,16 @@ namespace clang {
   };
 }
 
+// Regions that have default value zero.
+// FIXME: redefinition!
+// typedef llvm::ImmutableMap<const MemRegion*, SVal> RegionDefaultValue;
+// static int RegionDefaultValueIndex = 0;
+// namespace clang {
+//   template<> struct GRStateTrait<RegionDefaultValue>
+//     : public GRStatePartialTrait<RegionDefaultValue> {
+//     static void* GDMIndex() { return &RegionDefaultValueIndex; }
+//   };
+// }
 
 namespace {
 
@@ -83,7 +93,8 @@ public:
 
   MemRegionManager& getRegionManager() { return MRMgr; }
   
-  Store BindCompoundLiteral(Store store, const CompoundLiteralExpr* CL, SVal V);
+  const GRState* BindCompoundLiteral(const GRState* St, 
+                                     const CompoundLiteralExpr* CL, SVal V);
 
   SVal getLValueString(const GRState* St, const StringLiteral* S);
 
@@ -107,13 +118,24 @@ public:
   CastResult CastRegion(const GRState* state, const MemRegion* R,
                         QualType CastToTy);
 
+  /// The high level logic for this method is this:
+  /// Retrieve (L)
+  ///   if L has binding
+  ///     return L's binding
+  ///   else if L is in killset
+  ///     return unknown
+  ///   else
+  ///     if L is on stack or heap
+  ///       return undefined
+  ///     else
+  ///       return symbolic
   SVal Retrieve(const GRState* state, Loc L, QualType T = QualType());
 
-  Store Bind(Store St, Loc LV, SVal V);
+  const GRState* Bind(const GRState* St, Loc LV, SVal V);
 
   Store Remove(Store store, Loc LV);
 
-  Store getInitialStore();
+  Store getInitialStore() { return RBFactory.GetEmptyMap().getRoot(); }
   
   /// getSelfRegion - Returns the region for the 'self' (Objective-C) or
   ///  'this' object (C++).  When used when analyzing a normal function this
@@ -133,7 +155,11 @@ public:
 
   void UpdateLiveSymbols(SVal X, LiveSymbolsTy& LSymbols);
 
-  Store BindDecl(Store store, const VarDecl* VD, SVal* InitVal, unsigned Count);
+  const GRState* BindDecl(const GRState* St, const VarDecl* VD, SVal InitVal);
+
+  const GRState* BindDeclWithNoInit(const GRState* St, const VarDecl* VD) {
+    return St;
+  }
 
   const GRState* setExtent(const GRState* St, const MemRegion* R, SVal Extent);
 
@@ -152,22 +178,16 @@ private:
     return loc::MemRegionVal(MRMgr.getVarRegion(VD));
   }
 
-  Store InitializeArray(Store store, const TypedRegion* R, SVal Init);
-  Store BindArrayToVal(Store store, const TypedRegion* BaseR, SVal V);
-  Store BindArrayToSymVal(Store store, const TypedRegion* BaseR);
-
-  Store InitializeStruct(Store store, const TypedRegion* R, SVal Init);
-  Store BindStructToVal(Store store, const TypedRegion* BaseR, SVal V);
-  Store BindStructToSymVal(Store store, const TypedRegion* BaseR);
+  const GRState* BindArray(const GRState* St, const TypedRegion* R, SVal V);
 
   /// Retrieve the values in a struct and return a CompoundVal, used when doing
   /// struct copy: 
   /// struct s x, y; 
   /// x = y;
   /// y's value is retrieved by this method.
-  SVal RetrieveStruct(Store store, const TypedRegion* R);
+  SVal RetrieveStruct(const GRState* St, const TypedRegion* R);
 
-  Store BindStruct(Store store, const TypedRegion* R, SVal V);
+  const GRState* BindStruct(const GRState* St, const TypedRegion* R, SVal V);
 
   // Utility methods.
   BasicValueFactory& getBasicVals() { return StateMgr.getBasicVals(); }
@@ -396,41 +416,60 @@ RegionStoreManager::CastRegion(const GRState* state, const MemRegion* R,
   return CastResult(AddRegionView(state, ViewR, R), ViewR);
 }
 
-SVal RegionStoreManager::Retrieve(const GRState* state, Loc L, QualType T) {
+SVal RegionStoreManager::Retrieve(const GRState* St, Loc L, QualType T) {
   assert(!isa<UnknownVal>(L) && "location unknown");
   assert(!isa<UndefinedVal>(L) && "location undefined");
-  Store S = state->getStore();
 
-  switch (L.getSubKind()) {
-  case loc::MemRegionKind: {
-    const MemRegion* R = cast<loc::MemRegionVal>(L).getRegion();
-    assert(R && "bad region");
+  if (isa<loc::SymbolVal>(L))
+    return UnknownVal();
 
-    if (const TypedRegion* TR = dyn_cast<TypedRegion>(R))
-      if (TR->getRValueType(getContext())->isStructureType())
-        return RetrieveStruct(S, TR);
+  if (isa<loc::ConcreteInt>(L))
+    return UndefinedVal();
 
-    RegionBindingsTy B(static_cast<const RegionBindingsTy::TreeTy*>(S));
-    RegionBindingsTy::data_type* V = B.lookup(R);
-    return V ? *V : UnknownVal();
-  }
+  if (isa<loc::FuncVal>(L))
+    return L;
 
-  case loc::SymbolValKind:
-    return UnknownVal();
+  const MemRegion* R = cast<loc::MemRegionVal>(L).getRegion();
+  assert(R && "bad region");
 
-  case loc::ConcreteIntKind:
-    return UndefinedVal(); // As in BasicStoreManager.
+  if (const TypedRegion* TR = dyn_cast<TypedRegion>(R))
+    if (TR->getRValueType(getContext())->isStructureType())
+      return RetrieveStruct(St, TR);
+  
+  RegionBindingsTy B = GetRegionBindings(St->getStore());
+  RegionBindingsTy::data_type* V = B.lookup(R);
 
-  case loc::FuncValKind:
-    return L;
+  // Check if the region has a binding.
+  if (V)
+    return *V;
+  
+  // Check if the region is in killset.
+  GRStateRef state(St, StateMgr);
+  if (state.contains<RegionKills>(R))
+    return UnknownVal();
 
-  default:
-    assert(false && "Invalid Location");
-    return L;
-  }
+  // The location is not initialized.
+  
+  // We treat parameters as symbolic values.
+  if (const VarRegion* VR = dyn_cast<VarRegion>(R))
+    if (isa<ParmVarDecl>(VR->getDecl()))
+      return SVal::MakeSymbolValue(getSymbolManager(), VR,
+                                   VR->getRValueType(getContext()));
+  
+  if (MRMgr.onStack(R) || MRMgr.onHeap(R))
+    return UndefinedVal();
+  else
+    return SVal::MakeSymbolValue(getSymbolManager(), R, 
+                             cast<TypedRegion>(R)->getRValueType(getContext()));
+
+  // FIXME: consider default values for elements and fields.
 }
 
-SVal RegionStoreManager::RetrieveStruct(Store store, const TypedRegion* R) {
+SVal RegionStoreManager::RetrieveStruct(const GRState* St,const TypedRegion* R){
+
+  Store store = St->getStore();
+  GRStateRef state(St, StateMgr);
+
   // FIXME: Verify we want getRValueType instead of getLValueType.
   QualType T = R->getRValueType(getContext());
   assert(T->isStructureType());
@@ -447,10 +486,21 @@ SVal RegionStoreManager::RetrieveStruct(Store store, const TypedRegion* R) {
                                                FieldEnd = Fields.rend();
        Field != FieldEnd; ++Field) {
     FieldRegion* FR = MRMgr.getFieldRegion(*Field, R);
-    RegionBindingsTy B(static_cast<const RegionBindingsTy::TreeTy*>(store));
+    RegionBindingsTy B = GetRegionBindings(store);
     RegionBindingsTy::data_type* data = B.lookup(FR);
 
-    SVal FieldValue = data ? *data : UnknownVal();
+    SVal FieldValue;
+    if (data)
+      FieldValue = *data;
+    else if (state.contains<RegionKills>(FR))
+      FieldValue = UnknownVal();
+    else {
+      if (MRMgr.onStack(FR) || MRMgr.onHeap(FR))
+        FieldValue = UndefinedVal();
+      else
+        FieldValue = SVal::MakeSymbolValue(getSymbolManager(), FR,
+                                           FR->getRValueType(getContext()));
+    }
 
     StructVal = getBasicVals().consVals(FieldValue, StructVal);
   }
@@ -458,25 +508,37 @@ SVal RegionStoreManager::RetrieveStruct(Store store, const TypedRegion* R) {
   return NonLoc::MakeCompoundVal(T, StructVal, getBasicVals());
 }
 
-Store RegionStoreManager::Bind(Store store, Loc LV, SVal V) {
-  if (LV.getSubKind() == loc::SymbolValKind)
-    return store;
-
-  assert(LV.getSubKind() == loc::MemRegionKind);
+const GRState* RegionStoreManager::Bind(const GRState* St, Loc L, SVal V) {
+  // Currently we don't bind value to symbolic location. But if the logic is
+  // made clear, we might change this decision.
+  if (isa<loc::SymbolVal>(L))
+    return St;
 
-  const MemRegion* R = cast<loc::MemRegionVal>(LV).getRegion();
-  
+  // If we get here, the location should be a region.
+  const MemRegion* R = cast<loc::MemRegionVal>(L).getRegion();
   assert(R);
 
+  // Check if the region is a struct region.
   if (const TypedRegion* TR = dyn_cast<TypedRegion>(R))
     // FIXME: Verify we want getRValueType().
     if (TR->getRValueType(getContext())->isStructureType())
-      return BindStruct(store, TR, V);
+      return BindStruct(St, TR, V);
 
+  Store store = St->getStore();
   RegionBindingsTy B = GetRegionBindings(store);
-  return V.isUnknown()
-         ? RBFactory.Remove(B, R).getRoot()
-         : RBFactory.Add(B, R, V).getRoot();
+
+  if (V.isUnknown()) {
+    // Remove the binding.
+    store = RBFactory.Remove(B, R).getRoot();
+
+    // Add the region to the killset.
+    GRStateRef state(St, StateMgr);
+    St = state.add<RegionKills>(R);
+  } 
+  else
+    store = RBFactory.Add(B, R, V).getRoot();
+
+  return StateMgr.MakeStateWithStore(St, store);
 }
 
 Store RegionStoreManager::Remove(Store store, Loc L) {
@@ -488,150 +550,37 @@ Store RegionStoreManager::Remove(Store store, Loc L) {
   return RBFactory.Remove(B, R).getRoot();
 }
 
-Store RegionStoreManager::BindStruct(Store store, const TypedRegion* R, SVal V){
-  // Verify we want getRValueType.
-  QualType T = R->getRValueType(getContext());
-  assert(T->isStructureType());
-
-  const RecordType* RT = cast<RecordType>(T.getTypePtr());
-  RecordDecl* RD = RT->getDecl();
-
-  if (!RD->isDefinition()) {
-    // This can only occur when a pointer of incomplete struct type is used as a
-    // function argument.
-    assert(V.isUnknown());
-    return store;
-  }
-
-  RegionBindingsTy B = GetRegionBindings(store);
-
-  if (isa<UnknownVal>(V))
-    return BindStructToVal(store, R, UnknownVal());
-
-  nonloc::CompoundVal& CV = cast<nonloc::CompoundVal>(V);
-
-  nonloc::CompoundVal::iterator VI = CV.begin(), VE = CV.end();
-  RecordDecl::field_iterator FI = RD->field_begin(), FE = RD->field_end();
-
-  for (; FI != FE; ++FI, ++VI) {
-    assert(VI != VE);
-
-    FieldRegion* FR = MRMgr.getFieldRegion(*FI, R);
-
-    B = RBFactory.Add(B, FR, *VI);
-  }
-
-  return B.getRoot();
-}
+const GRState* RegionStoreManager::BindDecl(const GRState* St, 
+                                            const VarDecl* VD, SVal InitVal) {
+  // All static variables are treated as symbolic values.
+  if (VD->hasGlobalStorage())
+    return St;
 
-Store RegionStoreManager::getInitialStore() {
-  typedef LiveVariables::AnalysisDataTy LVDataTy;
-  LVDataTy& D = StateMgr.getLiveVariables().getAnalysisData();
-
-  Store St = RBFactory.GetEmptyMap().getRoot();
-
-  for (LVDataTy::decl_iterator I=D.begin_decl(), E=D.end_decl(); I != E; ++I) {
-    NamedDecl* ND = const_cast<NamedDecl*>(I->first);
-
-    if (VarDecl* VD = dyn_cast<VarDecl>(ND)) {
-      // Punt on static variables for now.
-      if (VD->getStorageClass() == VarDecl::Static)
-        continue;
-
-      VarRegion* VR = MRMgr.getVarRegion(VD);
-
-      QualType T = VD->getType();
-      // Only handle pointers and integers for now.
-      if (Loc::IsLocType(T) || T->isIntegerType()) {
-        // Initialize globals and parameters to symbolic values.
-        // Initialize local variables to undefined.
-        SVal X = (VD->hasGlobalStorage() || isa<ParmVarDecl>(VD) ||
-                  isa<ImplicitParamDecl>(VD))
-                 ? SVal::GetSymbolValue(getSymbolManager(), VD)
-                 : UndefinedVal();
-
-        St = Bind(St, getVarLoc(VD), X);
-      } 
-      else if (T->is