[cfe-commits] r65480 - in /cfe/trunk: Driver/AnalysisConsumer.cpp include/clang/Analysis/PathSensitive/GRExprEngine.h lib/Analysis/GRExprEngine.cpp test/Analysis/misc-ps-eager-assume.m
Ted Kremenek
kremenek at apple.com
Wed Feb 25 14:32:03 PST 2009
Author: kremenek
Date: Wed Feb 25 16:32:02 2009
New Revision: 65480
URL: http://llvm.org/viewvc/llvm-project?rev=65480&view=rev
Log:
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.
Added:
cfe/trunk/test/Analysis/misc-ps-eager-assume.m
Modified:
cfe/trunk/Driver/AnalysisConsumer.cpp
cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h
cfe/trunk/lib/Analysis/GRExprEngine.cpp
Modified: cfe/trunk/Driver/AnalysisConsumer.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/Driver/AnalysisConsumer.cpp?rev=65480&r1=65479&r2=65480&view=diff
==============================================================================
--- cfe/trunk/Driver/AnalysisConsumer.cpp (original)
+++ cfe/trunk/Driver/AnalysisConsumer.cpp Wed Feb 25 16:32:02 2009
@@ -152,6 +152,12 @@
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 @@
if (!L) return;
GRExprEngine Eng(*mgr.getCFG(), *mgr.getCodeDecl(), mgr.getContext(), *L, mgr,
- PurgeDead,
+ PurgeDead, EagerlyAssume,
mgr.getStoreManagerCreator(),
mgr.getConstraintManagerCreator());
Modified: cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h?rev=65480&r1=65479&r2=65480&view=diff
==============================================================================
--- cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h (original)
+++ cfe/trunk/include/clang/Analysis/PathSensitive/GRExprEngine.h Wed Feb 25 16:32:02 2009
@@ -90,6 +90,15 @@
// 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:
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 @@
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;
Modified: cfe/trunk/lib/Analysis/GRExprEngine.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/Analysis/GRExprEngine.cpp?rev=65480&r1=65479&r2=65480&view=diff
==============================================================================
--- cfe/trunk/lib/Analysis/GRExprEngine.cpp (original)
+++ cfe/trunk/lib/Analysis/GRExprEngine.cpp Wed Feb 25 16:32:02 2009
@@ -103,7 +103,7 @@
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 @@
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 @@
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 @@
// 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) {
Added: cfe/trunk/test/Analysis/misc-ps-eager-assume.m
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/misc-ps-eager-assume.m?rev=65480&view=auto
==============================================================================
--- cfe/trunk/test/Analysis/misc-ps-eager-assume.m (added)
+++ cfe/trunk/test/Analysis/misc-ps-eager-assume.m Wed Feb 25 16:32:02 2009
@@ -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
+ }
+ }
+}
+
More information about the cfe-commits
mailing list