Changed CallRetValSymbol to SymbolConjured to allow "conjured" symbols to be created for any expression, not just CallExprs.
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 6c5493c..c87ca67 100644
--- a/Analysis/CFRefCount.cpp
+++ b/Analysis/CFRefCount.cpp
@@ -588,7 +588,7 @@
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 @@
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 @@
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 61643a4..b8892e3 100644
--- a/Analysis/GRExprEngine.cpp
+++ b/Analysis/GRExprEngine.cpp
@@ -177,7 +177,7 @@
// Process the true branch.
- bool isFeasible = true;
+ bool isFeasible = false;
ValueState* St = Assume(PrevState, V, true, isFeasible);
if (isFeasible)
@@ -300,8 +300,8 @@
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 @@
// 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 @@
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 @@
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 b4abc3a..a03303c 100644
--- a/Analysis/GRSimpleVals.cpp
+++ b/Analysis/GRSimpleVals.cpp
@@ -432,7 +432,7 @@
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 5454649..f243fa66 100644
--- a/Analysis/SymbolManager.cpp
+++ b/Analysis/SymbolManager.cpp
@@ -72,10 +72,10 @@
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 @@
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 @@
return T->getAsPointerType()->getPointeeType();
}
- case CallRetValKind:
- return cast<SymbolDataCallRetVal>(this)->getCallExpr()->getType();
+ case ConjuredKind:
+ return cast<SymbolConjured>(this)->getExpr()->getType();
}
}