forked from OSchip/llvm-project
This patch adds two more SymbolData subclasses: SymIntExpr and SymSymExpr, for
representing symbolic expressions like 'x'+3 and 'x'+'y'. The design is subjected to change later when we fix the class hierarchy of symbolic expressions. llvm-svn: 67678
This commit is contained in:
parent
b2304ee0d1
commit
24e7eade19
|
@ -181,6 +181,12 @@ public:
|
|||
|
||||
static NonLoc MakeVal(SymbolRef sym);
|
||||
|
||||
static NonLoc MakeVal(SymbolManager& SymMgr, SymbolRef lhs,
|
||||
BinaryOperator::Opcode op, const llvm::APSInt& v);
|
||||
|
||||
static NonLoc MakeVal(SymbolManager& SymMgr, SymbolRef lhs,
|
||||
BinaryOperator::Opcode op, SymbolRef rhs);
|
||||
|
||||
static NonLoc MakeIntVal(BasicValueFactory& BasicVals, uint64_t X,
|
||||
bool isUnsigned);
|
||||
|
||||
|
|
|
@ -85,7 +85,7 @@ namespace clang {
|
|||
|
||||
class SymbolData : public llvm::FoldingSetNode {
|
||||
public:
|
||||
enum Kind { RegionRValue, ConjuredKind };
|
||||
enum Kind { RegionRValue, ConjuredKind, SymIntKind, SymSymKind };
|
||||
|
||||
private:
|
||||
Kind K;
|
||||
|
@ -171,6 +171,65 @@ public:
|
|||
}
|
||||
};
|
||||
|
||||
// SymIntExpr - Represents symbolic expression like 'x' + 3.
|
||||
class SymIntExpr : public SymbolData {
|
||||
SymbolRef LHS;
|
||||
BinaryOperator::Opcode Op;
|
||||
const llvm::APSInt& Val;
|
||||
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) {}
|
||||
|
||||
QualType getType(ASTContext& C) const {
|
||||
return T;
|
||||
}
|
||||
|
||||
static void Profile(llvm::FoldingSetNodeID& ID, SymbolRef lhs,
|
||||
BinaryOperator::Opcode op, const llvm::APSInt& V,
|
||||
QualType t) {
|
||||
lhs.Profile(ID);
|
||||
ID.AddInteger(op);
|
||||
ID.AddPointer(&V);
|
||||
ID.Add(t);
|
||||
}
|
||||
|
||||
void Profile(llvm::FoldingSetNodeID& ID) {
|
||||
Profile(ID, LHS, Op, Val, T);
|
||||
}
|
||||
};
|
||||
|
||||
// SymSymExpr - Represents symbolic expression like 'x' + 'y'.
|
||||
class SymSymExpr : public SymbolData {
|
||||
SymbolRef LHS;
|
||||
BinaryOperator::Opcode Op;
|
||||
SymbolRef 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) {}
|
||||
|
||||
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);
|
||||
ID.AddInteger(op);
|
||||
rhs.Profile(ID);
|
||||
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 {
|
||||
|
@ -231,6 +290,12 @@ public:
|
|||
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 SymbolData& getSymbolData(SymbolRef ID) const;
|
||||
|
||||
QualType getType(SymbolRef ID) const {
|
||||
|
|
|
@ -230,11 +230,16 @@ 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());
|
||||
|
||||
BasicVals.getConstraint(cast<nonloc::SymbolVal>(L).getSymbol(),
|
||||
Op, cast<nonloc::ConcreteInt>(R).getValue());
|
||||
return nonloc::SymIntConstraintVal(C);
|
||||
} else {
|
||||
return NonLoc::MakeVal(Eng.getSymbolManager(),
|
||||
cast<nonloc::SymbolVal>(L).getSymbol(),
|
||||
Op, cast<nonloc::ConcreteInt>(R).getValue());
|
||||
}
|
||||
}
|
||||
else
|
||||
return UnknownVal();
|
||||
|
|
|
@ -283,6 +283,23 @@ NonLoc NonLoc::MakeVal(SymbolRef sym) {
|
|||
return nonloc::SymbolVal(sym);
|
||||
}
|
||||
|
||||
NonLoc NonLoc::MakeVal(SymbolManager& SymMgr, SymbolRef lhs,
|
||||
BinaryOperator::Opcode op, const APSInt& v) {
|
||||
// The Environment ensures we always get a persistent APSInt in
|
||||
// BasicValueFactory, so we don't need to get the APSInt from
|
||||
// BasicValueFactory again.
|
||||
|
||||
SymbolRef sym = SymMgr.getSymIntExpr(lhs, op, v, SymMgr.getType(lhs));
|
||||
return nonloc::SymbolVal(sym);
|
||||
}
|
||||
|
||||
NonLoc NonLoc::MakeVal(SymbolManager& SymMgr, SymbolRef lhs,
|
||||
BinaryOperator::Opcode op, SymbolRef rhs) {
|
||||
assert(SymMgr.getType(lhs) == SymMgr.getType(rhs));
|
||||
SymbolRef sym = SymMgr.getSymSymExpr(lhs, op, rhs, SymMgr.getType(lhs));
|
||||
return nonloc::SymbolVal(sym);
|
||||
}
|
||||
|
||||
NonLoc NonLoc::MakeIntVal(BasicValueFactory& BasicVals, uint64_t X,
|
||||
bool isUnsigned) {
|
||||
return nonloc::ConcreteInt(BasicVals.getIntValue(X, isUnsigned));
|
||||
|
|
|
@ -21,28 +21,11 @@ namespace clang {
|
|||
SimpleConstraintManager::~SimpleConstraintManager() {}
|
||||
|
||||
bool SimpleConstraintManager::canReasonAbout(SVal X) const {
|
||||
if (nonloc::SymIntConstraintVal *Y = dyn_cast<nonloc::SymIntConstraintVal>(&X)) {
|
||||
const SymIntConstraint& C = Y->getConstraint();
|
||||
switch (C.getOpcode()) {
|
||||
// We don't reason yet about bitwise-constraints on symbolic values.
|
||||
case BinaryOperator::And:
|
||||
case BinaryOperator::Or:
|
||||
case BinaryOperator::Xor:
|
||||
return false;
|
||||
// We don't reason yet about arithmetic constraints on symbolic values.
|
||||
case BinaryOperator::Mul:
|
||||
case BinaryOperator::Div:
|
||||
case BinaryOperator::Rem:
|
||||
case BinaryOperator::Add:
|
||||
case BinaryOperator::Sub:
|
||||
case BinaryOperator::Shl:
|
||||
case BinaryOperator::Shr:
|
||||
return false;
|
||||
|
||||
// All other cases.
|
||||
default:
|
||||
return true;
|
||||
}
|
||||
if (nonloc::SymbolVal* SymVal = dyn_cast<nonloc::SymbolVal>(&X)) {
|
||||
const SymbolData& data
|
||||
= getSymbolManager().getSymbolData(SymVal->getSymbol());
|
||||
return !(data.getKind() == SymbolData::SymIntKind ||
|
||||
data.getKind() == SymbolData::SymSymKind );
|
||||
}
|
||||
|
||||
return true;
|
||||
|
@ -143,6 +126,12 @@ SimpleConstraintManager::Assume(const GRState* St, NonLoc Cond, bool Assumption,
|
|||
const GRState*
|
||||
SimpleConstraintManager::AssumeAux(const GRState* St,NonLoc Cond,
|
||||
bool Assumption, bool& isFeasible) {
|
||||
// We cannot reason about SymIntExpr and SymSymExpr.
|
||||
if (!canReasonAbout(Cond)) {
|
||||
isFeasible = true;
|
||||
return St;
|
||||
}
|
||||
|
||||
BasicValueFactory& BasicVals = StateMgr.getBasicVals();
|
||||
SymbolManager& SymMgr = StateMgr.getSymbolManager();
|
||||
|
||||
|
|
|
@ -76,6 +76,7 @@ public:
|
|||
|
||||
private:
|
||||
BasicValueFactory& getBasicVals() { return StateMgr.getBasicVals(); }
|
||||
SymbolManager& getSymbolManager() const { return StateMgr.getSymbolManager(); }
|
||||
};
|
||||
|
||||
} // end clang namespace
|
||||
|
|
|
@ -74,6 +74,47 @@ SymbolRef SymbolManager::getConjuredSymbol(const Stmt* E, QualType T,
|
|||
return SymbolCounter++;
|
||||
}
|
||||
|
||||
SymbolRef SymbolManager::getSymIntExpr(SymbolRef lhs,BinaryOperator::Opcode op,
|
||||
const llvm::APSInt& v, QualType t) {
|
||||
llvm::FoldingSetNodeID ID;
|
||||
SymIntExpr::Profile(ID, lhs, op, v, t);
|
||||
void* InsertPos;
|
||||
|
||||
SymbolData* data = DataSet.FindNodeOrInsertPos(ID, InsertPos);
|
||||
|
||||
if (data)
|
||||
return data->getSymbol();
|
||||
|
||||
data = (SymIntExpr*) BPAlloc.Allocate<SymIntExpr>();
|
||||
new (data) SymIntExpr(SymbolCounter, lhs, op, v, t);
|
||||
|
||||
DataSet.InsertNode(data, InsertPos);
|
||||
DataMap[SymbolCounter] = data;
|
||||
|
||||
return SymbolCounter++;
|
||||
}
|
||||
|
||||
SymbolRef SymbolManager::getSymSymExpr(SymbolRef lhs, BinaryOperator::Opcode op,
|
||||
SymbolRef rhs, QualType t) {
|
||||
llvm::FoldingSetNodeID ID;
|
||||
SymSymExpr::Profile(ID, lhs, op, rhs, t);
|
||||
void* InsertPos;
|
||||
|
||||
SymbolData* data = DataSet.FindNodeOrInsertPos(ID, InsertPos);
|
||||
|
||||
if (data)
|
||||
return data->getSymbol();
|
||||
|
||||
data = (SymSymExpr*) BPAlloc.Allocate<SymSymExpr>();
|
||||
new (data) SymSymExpr(SymbolCounter, lhs, op, rhs, t);
|
||||
|
||||
DataSet.InsertNode(data, InsertPos);
|
||||
DataMap[SymbolCounter] = data;
|
||||
|
||||
return SymbolCounter++;
|
||||
}
|
||||
|
||||
|
||||
const SymbolData& SymbolManager::getSymbolData(SymbolRef Sym) const {
|
||||
DataMapTy::const_iterator I = DataMap.find(Sym);
|
||||
assert (I != DataMap.end());
|
||||
|
|
Loading…
Reference in New Issue