forked from OSchip/llvm-project
Add experimental logic in GRExprEngine::EvalEagerlyAssume() to handle
expressions of the form: 'short x = (y != 10);' While we handle 'int x = (y != 10)' lazily, the cast to another integer type currently loses the symbolic constraint. Eager evaluation of the constraint causes the paths to bifurcate and eagerly evaluate 'y != 10' to a constant of 1 or 0. This should address <rdar://problem/6619921> until we have a better (more lazy approach) for handling promotions/truncations of symbolic integer values. llvm-svn: 65480
This commit is contained in:
parent
1e249f8641
commit
dc3f50fbd9
|
@ -152,6 +152,12 @@ PurgeDead("analyzer-purge-dead",
|
|||
llvm::cl::desc("Remove dead symbols, bindings, and constraints before"
|
||||
" processing a statement."));
|
||||
|
||||
static llvm::cl::opt<bool>
|
||||
EagerlyAssume("analyzer-eagerly-assume",
|
||||
llvm::cl::init(false),
|
||||
llvm::cl::desc("Eagerly assume the truth/falseness of some "
|
||||
"symbolic constraints."));
|
||||
|
||||
static llvm::cl::opt<std::string>
|
||||
AnalyzeSpecificFunction("analyze-function",
|
||||
llvm::cl::desc("Run analysis on specific function"));
|
||||
|
@ -516,7 +522,7 @@ static void ActionGRExprEngine(AnalysisManager& mgr, GRTransferFuncs* tf,
|
|||
if (!L) return;
|
||||
|
||||
GRExprEngine Eng(*mgr.getCFG(), *mgr.getCodeDecl(), mgr.getContext(), *L, mgr,
|
||||
PurgeDead,
|
||||
PurgeDead, EagerlyAssume,
|
||||
mgr.getStoreManagerCreator(),
|
||||
mgr.getConstraintManagerCreator());
|
||||
|
||||
|
|
|
@ -90,6 +90,15 @@ protected:
|
|||
// destructor is called before the rest of the GRExprEngine is destroyed.
|
||||
GRBugReporter BR;
|
||||
|
||||
/// EargerlyAssume - A flag indicating how the engine should handle
|
||||
// expressions such as: 'x = (y != 0)'. When this flag is true then
|
||||
// the subexpression 'y != 0' will be eagerly assumed to be true or false,
|
||||
// thus evaluating it to the integers 0 or 1 respectively. The upside
|
||||
// is that this can increase analysis precision until we have a better way
|
||||
// to lazily evaluate such logic. The downside is that it eagerly
|
||||
// bifurcates paths.
|
||||
const bool EagerlyAssume;
|
||||
|
||||
public:
|
||||
typedef llvm::SmallPtrSet<NodeTy*,2> ErrorNodes;
|
||||
typedef llvm::DenseMap<NodeTy*, Expr*> UndefArgsTy;
|
||||
|
@ -186,7 +195,7 @@ public:
|
|||
public:
|
||||
GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx, LiveVariables& L,
|
||||
BugReporterData& BRD,
|
||||
bool purgeDead,
|
||||
bool purgeDead, bool eagerlyAssume = true,
|
||||
StoreManagerCreator SMC = CreateBasicStoreManager,
|
||||
ConstraintManagerCreator CMC = CreateBasicConstraintManager);
|
||||
|
||||
|
@ -606,6 +615,11 @@ protected:
|
|||
const GRState* CheckDivideZero(Expr* Ex, const GRState* St, NodeTy* Pred,
|
||||
SVal Denom);
|
||||
|
||||
/// EvalEagerlyAssume - Given the nodes in 'Src', eagerly assume symbolic
|
||||
/// expressions of the form 'x != 0' and generate new nodes (stored in Dst)
|
||||
/// with those assumptions.
|
||||
void EvalEagerlyAssume(NodeSet& Dst, NodeSet& Src);
|
||||
|
||||
SVal EvalCast(SVal X, QualType CastT) {
|
||||
if (X.isUnknownOrUndef())
|
||||
return X;
|
||||
|
|
|
@ -103,7 +103,7 @@ static inline Selector GetNullarySelector(const char* name, ASTContext& Ctx) {
|
|||
|
||||
GRExprEngine::GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx,
|
||||
LiveVariables& L, BugReporterData& BRD,
|
||||
bool purgeDead,
|
||||
bool purgeDead, bool eagerlyAssume,
|
||||
StoreManagerCreator SMC,
|
||||
ConstraintManagerCreator CMC)
|
||||
: CoreEngine(cfg, CD, Ctx, *this),
|
||||
|
@ -116,7 +116,8 @@ GRExprEngine::GRExprEngine(CFG& cfg, Decl& CD, ASTContext& Ctx,
|
|||
NSExceptionII(NULL), NSExceptionInstanceRaiseSelectors(NULL),
|
||||
RaiseSel(GetNullarySelector("raise", G.getContext())),
|
||||
PurgeDead(purgeDead),
|
||||
BR(BRD, *this) {}
|
||||
BR(BRD, *this),
|
||||
EagerlyAssume(eagerlyAssume) {}
|
||||
|
||||
GRExprEngine::~GRExprEngine() {
|
||||
BR.FlushReports();
|
||||
|
@ -262,7 +263,14 @@ void GRExprEngine::Visit(Stmt* S, NodeTy* Pred, NodeSet& Dst) {
|
|||
break;
|
||||
}
|
||||
|
||||
VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Dst);
|
||||
if (EagerlyAssume && (B->isRelationalOp() || B->isEqualityOp())) {
|
||||
NodeSet Tmp;
|
||||
VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Tmp);
|
||||
EvalEagerlyAssume(Dst, Tmp);
|
||||
}
|
||||
else
|
||||
VisitBinaryOperator(cast<BinaryOperator>(S), Pred, Dst);
|
||||
|
||||
break;
|
||||
}
|
||||
|
||||
|
@ -1349,6 +1357,44 @@ void GRExprEngine::VisitCallRec(CallExpr* CE, NodeTy* Pred,
|
|||
// Transfer function: Objective-C ivar references.
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
static std::pair<const void*,const void*> EagerlyAssumeTag(&EagerlyAssumeTag,0);
|
||||
|
||||
void GRExprEngine::EvalEagerlyAssume(NodeSet &Dst, NodeSet &Src) {
|
||||
for (NodeSet::iterator I=Src.begin(), E=Src.end(); I!=E; ++I) {
|
||||
NodeTy *Pred = *I;
|
||||
Stmt *S = cast<PostStmt>(Pred->getLocation()).getStmt();
|
||||
const GRState* state = Pred->getState();
|
||||
SVal V = GetSVal(state, S);
|
||||
if (isa<nonloc::SymIntConstraintVal>(V)) {
|
||||
// First assume that the condition is true.
|
||||
bool isFeasible = false;
|
||||
const GRState *stateTrue = Assume(state, V, true, isFeasible);
|
||||
if (isFeasible) {
|
||||
stateTrue = BindExpr(stateTrue, cast<Expr>(S),
|
||||
MakeConstantVal(1U, cast<Expr>(S)));
|
||||
Dst.Add(Builder->generateNode(PostStmtCustom(S, &EagerlyAssumeTag),
|
||||
stateTrue, Pred));
|
||||
}
|
||||
|
||||
// Next, assume that the condition is false.
|
||||
isFeasible = false;
|
||||
const GRState *stateFalse = Assume(state, V, false, isFeasible);
|
||||
if (isFeasible) {
|
||||
stateFalse = BindExpr(stateFalse, cast<Expr>(S),
|
||||
MakeConstantVal(0U, cast<Expr>(S)));
|
||||
Dst.Add(Builder->generateNode(PostStmtCustom(S, &EagerlyAssumeTag),
|
||||
stateFalse, Pred));
|
||||
}
|
||||
}
|
||||
else
|
||||
Dst.Add(Pred);
|
||||
}
|
||||
}
|
||||
|
||||
//===----------------------------------------------------------------------===//
|
||||
// Transfer function: Objective-C ivar references.
|
||||
//===----------------------------------------------------------------------===//
|
||||
|
||||
void GRExprEngine::VisitObjCIvarRefExpr(ObjCIvarRefExpr* Ex,
|
||||
NodeTy* Pred, NodeSet& Dst,
|
||||
bool asLValue) {
|
||||
|
|
|
@ -0,0 +1,14 @@
|
|||
// RUN: clang -analyze -checker-cfref --analyzer-store=region -analyzer-constraints=range --verify -fblocks %s -analyzer-eagerly-assume
|
||||
|
||||
void handle_assign_of_condition(int x) {
|
||||
// The cast to 'short' causes us to lose symbolic constraint.
|
||||
short y = (x != 0);
|
||||
char *p = 0;
|
||||
if (y) {
|
||||
// This should be infeasible.
|
||||
if (!(x != 0)) {
|
||||
*p = 1; // no-warning
|
||||
}
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue