Changed CallRetValSymbol to SymbolConjured to allow "conjured" symbols to be created...

Added experimental support for conjuring symbols during assingments where the RHS is "unknown".  This allows more value tracking for path-sensitivity.
Fixed bug in "assumption" logic when processing symbolic constraints; we would improperly mark constraints we didn't support as infeasible.

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

diff --git a/Analysis/CFRefCount.cpp b/Analysis/CFRefCount.cpp
index 6c5493c2061d24480ee715b80b01a9f756e8cfd6..c87ca673b9dabc7df7c637a6bb0a8cad09f5a77e 100644 (file)
--- a/Analysis/CFRefCount.cpp
+++ b/Analysis/CFRefCount.cpp
@@ -588,7 +588,7 @@ void CFRefCount::EvalCall(ExplodedNodeSet<ValueState>& Dst,
     
     if (CE->getType() != Eng.getContext().VoidTy) {    
       unsigned Count = Builder.getCurrentBlockCount();
-      SymbolID Sym = Eng.getSymbolManager().getCallRetValSymbol(CE, Count);
+      SymbolID Sym = Eng.getSymbolManager().getConjuredSymbol(CE, Count);
       
       RVal X = CE->getType()->isPointerType() 
       ? cast<RVal>(lval::SymbolVal(Sym)) 
@@ -664,7 +664,7 @@ void CFRefCount::EvalCall(ExplodedNodeSet<ValueState>& Dst,
       
     case RetEffect::OwnedSymbol: {
       unsigned Count = Builder.getCurrentBlockCount();
-      SymbolID Sym = Eng.getSymbolManager().getCallRetValSymbol(CE, Count);
+      SymbolID Sym = Eng.getSymbolManager().getConjuredSymbol(CE, Count);
 
       ValueState StImpl = *St;
       RefBindings B = GetRefBindings(StImpl);
@@ -679,7 +679,7 @@ void CFRefCount::EvalCall(ExplodedNodeSet<ValueState>& Dst,
       
     case RetEffect::NotOwnedSymbol: {
       unsigned Count = Builder.getCurrentBlockCount();
-      SymbolID Sym = Eng.getSymbolManager().getCallRetValSymbol(CE, Count);
+      SymbolID Sym = Eng.getSymbolManager().getConjuredSymbol(CE, Count);
       
       ValueState StImpl = *St;
       RefBindings B = GetRefBindings(StImpl);

diff --git a/Analysis/GRExprEngine.cpp b/Analysis/GRExprEngine.cpp
index 61643a440ef4d6423cd6e95c50e125874184433f..b8892e3ee546d81091bb431d531b0269ca44aae0 100644 (file)
--- a/Analysis/GRExprEngine.cpp
+++ b/Analysis/GRExprEngine.cpp
@@ -177,7 +177,7 @@ void GRExprEngine::ProcessBranch(Expr* Condition, Stmt* Term,
 
   // Process the true branch.
 
-  bool isFeasible = true;  
+  bool isFeasible = false;  
   ValueState* St = Assume(PrevState, V, true, isFeasible);
 
   if (isFeasible)
@@ -300,8 +300,8 @@ void GRExprEngine::ProcessSwitch(SwitchNodeBuilder& builder) {
       RVal Res = EvalBinOp(BinaryOperator::EQ, CondV, CaseVal);
       
       // Now "assume" that the case matches.
-      bool isFeasible = false;
       
+      bool isFeasible = false;      
       ValueState* StNew = Assume(St, Res, true, isFeasible);
       
       if (isFeasible) {
@@ -317,6 +317,7 @@ void GRExprEngine::ProcessSwitch(SwitchNodeBuilder& builder) {
       // Now "assume" that the case doesn't match.  Add this state
       // to the default state (if it is feasible).
       
+      isFeasible = false;
       StNew = Assume(DefaultSt, Res, false, isFeasible);
       
       if (isFeasible)
@@ -1114,10 +1115,27 @@ void GRExprEngine::VisitBinaryOperator(BinaryOperator* B,
             continue;
           }
           
+          // EXPERIMENTAL: "Conjured" symbols.
+          
+          if (RightV.isUnknown()) {            
+            unsigned Count = Builder->getCurrentBlockCount();
+            SymbolID Sym = SymMgr.getConjuredSymbol(B->getRHS(), Count);
+            
+            RightV = B->getRHS()->getType()->isPointerType() 
+                     ? cast<RVal>(lval::SymbolVal(Sym)) 
+                     : cast<RVal>(nonlval::SymbolVal(Sym));            
+          }
+          
+          // Even if the LHS evaluates to an unknown L-Value, the entire
+          // expression still evaluates to the RHS.
+          
           if (LeftV.isUnknown()) {
             St = SetRVal(St, B, RightV);
             break;
           }
+          
+          // Simulate the effects of a "store":  bind the value of the RHS
+          // to the L-Value represented by the LHS.
 
           St = SetRVal(SetRVal(St, B, RightV), cast<LVal>(LeftV), RightV);
           break;
@@ -1531,6 +1549,7 @@ GRExprEngine::AssumeSymInt(ValueState* St, bool Assumption,
   switch (C.getOpcode()) {
     default:
       // No logic yet for other operators.
+      isFeasible = true;
       return St;
       
     case BinaryOperator::EQ:

diff --git a/Analysis/GRSimpleVals.cpp b/Analysis/GRSimpleVals.cpp
index b4abc3afddbbbb4834185c82f4e6d100e0f2b4be..a03303c079e6b802e3a4a434feeeb0e1d1fc0aa8 100644 (file)
--- a/Analysis/GRSimpleVals.cpp
+++ b/Analysis/GRSimpleVals.cpp
@@ -432,7 +432,7 @@ void GRSimpleVals::EvalCall(ExplodedNodeSet<ValueState>& Dst,
   
   if (CE->getType() != Eng.getContext().VoidTy) {    
     unsigned Count = Builder.getCurrentBlockCount();
-    SymbolID Sym = Eng.getSymbolManager().getCallRetValSymbol(CE, Count);
+    SymbolID Sym = Eng.getSymbolManager().getConjuredSymbol(CE, Count);
         
     RVal X = CE->getType()->isPointerType() 
              ? cast<RVal>(lval::SymbolVal(Sym)) 

diff --git a/Analysis/SymbolManager.cpp b/Analysis/SymbolManager.cpp
index 54546494435d67c38505aeb80a9c6f99f714177d..f243fa667b33bbe0dbb477785d6b852b6d0252e5 100644 (file)
--- a/Analysis/SymbolManager.cpp
+++ b/Analysis/SymbolManager.cpp
@@ -72,10 +72,10 @@ SymbolID SymbolManager::getContentsOfSymbol(SymbolID sym) {
   return SymbolCounter++;
 }
   
-SymbolID SymbolManager::getCallRetValSymbol(CallExpr* CE, unsigned Count) {
+SymbolID SymbolManager::getConjuredSymbol(Expr* E, unsigned Count) {
   
   llvm::FoldingSetNodeID profile;
-  SymbolDataCallRetVal::Profile(profile, CE, Count);
+  SymbolConjured::Profile(profile, E, Count);
   void* InsertPos;
   
   SymbolData* SD = DataSet.FindNodeOrInsertPos(profile, InsertPos);
@@ -83,8 +83,8 @@ SymbolID SymbolManager::getCallRetValSymbol(CallExpr* CE, unsigned Count) {
   if (SD)
     return SD->getSymbol();
   
-  SD = (SymbolData*) BPAlloc.Allocate<SymbolDataCallRetVal>();
-  new (SD) SymbolDataCallRetVal(SymbolCounter, CE, Count);
+  SD = (SymbolData*) BPAlloc.Allocate<SymbolConjured>();
+  new (SD) SymbolConjured(SymbolCounter, E, Count);
   
   DataSet.InsertNode(SD, InsertPos);  
   DataMap[SymbolCounter] = SD;
@@ -116,8 +116,8 @@ QualType SymbolData::getType(const SymbolManager& SymMgr) const {
       return T->getAsPointerType()->getPointeeType();
     }
       
-    case CallRetValKind:
-      return cast<SymbolDataCallRetVal>(this)->getCallExpr()->getType();
+    case ConjuredKind:
+      return cast<SymbolConjured>(this)->getExpr()->getType();
   }
 }
 

diff --git a/include/clang/Analysis/PathSensitive/SymbolManager.h b/include/clang/Analysis/PathSensitive/SymbolManager.h
index a740302c8dd6b0a33434fa329dc3b5f48f062bf6..d0473c6a8eeb196a092821f998b0d7dae334f96c 100644 (file)
--- a/include/clang/Analysis/PathSensitive/SymbolManager.h
+++ b/include/clang/Analysis/PathSensitive/SymbolManager.h
@@ -69,7 +69,7 @@ namespace clang {
   
 class SymbolData : public llvm::FoldingSetNode {
 public:
-  enum Kind { UndefKind, ParmKind, GlobalKind, ContentsOfKind, CallRetValKind };
+  enum Kind { UndefKind, ParmKind, GlobalKind, ContentsOfKind, ConjuredKind };
   
 private:
   Kind K;
@@ -165,32 +165,32 @@ public:
   }  
 };
   
-class SymbolDataCallRetVal : public SymbolData {
-  CallExpr* CE;
+class SymbolConjured : public SymbolData {
+  Expr* E;
   unsigned Count;
 
 public:
-  SymbolDataCallRetVal(SymbolID Sym, CallExpr* ce, unsigned count)
-    : SymbolData(CallRetValKind, Sym), CE(ce), Count(count) {}
+  SymbolConjured(SymbolID Sym, Expr* exp, unsigned count)
+    : SymbolData(ConjuredKind, Sym), E(exp), Count(count) {}
   
-  CallExpr* getCallExpr() const { return CE; }
+  Expr* getExpr() const { return E; }
   unsigned getCount() const { return Count; }  
   
   static void Profile(llvm::FoldingSetNodeID& profile,
-                      CallExpr* CE, unsigned Count) {
+                      Expr* E, unsigned Count) {
     
-    profile.AddInteger((unsigned) CallRetValKind);
-    profile.AddPointer(CE);
+    profile.AddInteger((unsigned) ConjuredKind);
+    profile.AddPointer(E);
     profile.AddInteger(Count);
   }
   
   virtual void Profile(llvm::FoldingSetNodeID& profile) {
-    Profile(profile, CE, Count);
+    Profile(profile, E, Count);
   }
   
   // Implement isa<T> support.
   static inline bool classof(const SymbolData* D) {
-    return D->getKind() == CallRetValKind;
+    return D->getKind() == ConjuredKind;
   }  
 };
 
@@ -243,7 +243,7 @@ public:
   
   SymbolID getSymbol(VarDecl* D);
   SymbolID getContentsOfSymbol(SymbolID sym);
-  SymbolID getCallRetValSymbol(CallExpr* CE, unsigned VisitCount);
+  SymbolID getConjuredSymbol(Expr* E, unsigned VisitCount);
   
   const SymbolData& getSymbolData(SymbolID ID) const;