[cfe-commits] r145832 - in /cfe/trunk: include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h lib/StaticAnalyzer/Core/ExprEngineC.cpp lib/StaticAnalyzer/Core/ProgramState.cpp lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp test/Analysis/out-of-bounds.c
Anna Zaks
ganna at apple.com
Mon Dec 5 10:58:25 PST 2011
Author: zaks
Date: Mon Dec 5 12:58:25 2011
New Revision: 145832
URL: http://llvm.org/viewvc/llvm-project?rev=145832&view=rev
Log:
[analyzer] Remove all uses of ConstraintManager::canResonAbout() from
ExprEngine.
Teach SimpleConstraintManager::assumeSymRel() to propagate constraints
to symbolic expressions.
+ One extra warning (real bug) is now generated due to enhanced
assumeSymRel().
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp
cfe/trunk/lib/StaticAnalyzer/Core/ProgramState.cpp
cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
cfe/trunk/test/Analysis/out-of-bounds.c
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h?rev=145832&r1=145831&r2=145832&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h Mon Dec 5 12:58:25 2011
@@ -276,6 +276,7 @@
enum Kind { ConcreteIntKind, SymbolValKind, SymExprValKind,
LocAsIntegerKind, CompoundValKind, LazyCompoundValKind };
+// TODO: Change to contain symbol data.
class SymbolVal : public NonLoc {
public:
SymbolVal(SymbolRef sym) : NonLoc(SymbolValKind, sym) {}
Modified: cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp?rev=145832&r1=145831&r2=145832&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/ExprEngineC.cpp Mon Dec 5 12:58:25 2011
@@ -121,8 +121,7 @@
SVal LHSVal;
- if (Result.isUnknown() ||
- !getConstraintManager().canReasonAbout(Result)) {
+ if (Result.isUnknown()) {
unsigned Count = currentBuilderContext->getCurrentBlockCount();
@@ -358,8 +357,7 @@
// Recover some path-sensitivity if a scalar value evaluated to
// UnknownVal.
- if ((InitVal.isUnknown() ||
- !getConstraintManager().canReasonAbout(InitVal)) &&
+ if ((InitVal.isUnknown()) &&
!VD->getType()->isReferenceType() &&
!Pred->getState()->isTainted(InitVal)) {
InitVal = svalBuilder.getConjuredSymbolVal(NULL, InitEx,
@@ -726,7 +724,7 @@
SVal Result = evalBinOp(state, Op, V2, RHS, U->getType());
// Conjure a new symbol if necessary to recover precision.
- if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result)){
+ if (Result.isUnknown()){
DefinedOrUnknownSVal SymVal =
svalBuilder.getConjuredSymbolVal(NULL, Ex,
currentBuilderContext->getCurrentBlockCount());
Modified: cfe/trunk/lib/StaticAnalyzer/Core/ProgramState.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/ProgramState.cpp?rev=145832&r1=145831&r2=145832&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/ProgramState.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/ProgramState.cpp Mon Dec 5 12:58:25 2011
@@ -550,9 +550,8 @@
return true;
isVisited = 1;
- if (const SymbolData *sData = dyn_cast<SymbolData>(sym))
- if (!visitor.VisitSymbol(sData))
- return false;
+ if (!visitor.VisitSymbol(sym))
+ return false;
switch (sym->getKind()) {
case SymExpr::RegionValueKind:
Modified: cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp?rev=145832&r1=145831&r2=145832&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp Mon Dec 5 12:58:25 2011
@@ -212,6 +212,40 @@
} // end switch
}
+static llvm::APSInt computeAdjustment(const SymExpr *LHS,
+ SymbolRef &Sym) {
+ llvm::APSInt DefaultAdjustment;
+ DefaultAdjustment = 0;
+
+ // First check if the LHS is a simple symbol reference.
+ if (isa<SymbolData>(LHS))
+ return DefaultAdjustment;
+
+ // Next, see if it's a "($sym+constant1)" expression.
+ const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
+
+ // We cannot simplify "($sym1+$sym2)".
+ if (!SE)
+ return DefaultAdjustment;
+
+ // Get the constant out of the expression "($sym+constant1)" or
+ // "<expr>+constant1".
+ Sym = SE->getLHS();
+ switch (SE->getOpcode()) {
+ case BO_Add:
+ return SE->getRHS();
+ break;
+ case BO_Sub:
+ return -SE->getRHS();
+ break;
+ default:
+ // We cannot simplify non-additive operators.
+ return DefaultAdjustment;
+ }
+
+ return DefaultAdjustment;
+}
+
const ProgramState *SimpleConstraintManager::assumeSymRel(const ProgramState *state,
const SymExpr *LHS,
BinaryOperator::Opcode op,
@@ -219,48 +253,15 @@
assert(BinaryOperator::isComparisonOp(op) &&
"Non-comparison ops should be rewritten as comparisons to zero.");
- // We only handle simple comparisons of the form "$sym == constant"
- // or "($sym+constant1) == constant2".
- // The adjustment is "constant1" in the above expression. It's used to
- // "slide" the solution range around for modular arithmetic. For example,
- // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
- // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
- // the subclasses of SimpleConstraintManager to handle the adjustment.
- llvm::APSInt Adjustment;
-
- // First check if the LHS is a simple symbol reference.
- SymbolRef Sym = dyn_cast<SymbolData>(LHS);
- if (Sym) {
- Adjustment = 0;
- } else {
- // Next, see if it's a "($sym+constant1)" expression.
- const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
-
- // We don't handle "($sym1+$sym2)".
- // Give up and assume the constraint is feasible.
- if (!SE)
- return state;
-
- // We don't handle "(<expr>+constant1)".
- // Give up and assume the constraint is feasible.
- Sym = dyn_cast<SymbolData>(SE->getLHS());
- if (!Sym)
- return state;
-
- // Get the constant out of the expression "($sym+constant1)".
- switch (SE->getOpcode()) {
- case BO_Add:
- Adjustment = SE->getRHS();
- break;
- case BO_Sub:
- Adjustment = -SE->getRHS();
- break;
- default:
- // We don't handle non-additive operators.
- // Give up and assume the constraint is feasible.
- return state;
- }
- }
+ // We only handle simple comparisons of the form "$sym == constant"
+ // or "($sym+constant1) == constant2".
+ // The adjustment is "constant1" in the above expression. It's used to
+ // "slide" the solution range around for modular arithmetic. For example,
+ // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
+ // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
+ // the subclasses of SimpleConstraintManager to handle the adjustment.
+ SymbolRef Sym = LHS;
+ llvm::APSInt Adjustment = computeAdjustment(LHS, Sym);
// FIXME: This next section is a hack. It silently converts the integers to
// be of the same type as the symbol, which is not always correct. Really the
Modified: cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp?rev=145832&r1=145831&r2=145832&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp Mon Dec 5 12:58:25 2011
@@ -260,9 +260,10 @@
// Wrap the LHS up in a NonLoc again and let evalCastFromNonLoc do the
// dirty work.
if (isIdempotent) {
- if (SymbolRef LHSSym = dyn_cast<SymbolData>(LHS))
- return evalCastFromNonLoc(nonloc::SymbolVal(LHSSym), resultTy);
- return evalCastFromNonLoc(nonloc::SymExprVal(LHS), resultTy);
+ if (isa<SymbolData>(LHS))
+ return evalCastFromNonLoc(nonloc::SymbolVal(LHS), resultTy);
+ else
+ return evalCastFromNonLoc(nonloc::SymExprVal(LHS), resultTy);
}
// If we reach this point, the expression cannot be simplified.
Modified: cfe/trunk/test/Analysis/out-of-bounds.c
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/out-of-bounds.c?rev=145832&r1=145831&r2=145832&view=diff
==============================================================================
--- cfe/trunk/test/Analysis/out-of-bounds.c (original)
+++ cfe/trunk/test/Analysis/out-of-bounds.c Mon Dec 5 12:58:25 2011
@@ -128,13 +128,11 @@
buf[0][0] = 1; // no-warning
}
-// *** FIXME ***
-// We don't get a warning here yet because our symbolic constraint solving
-// doesn't handle: (symbol * constant) < constant
+// Testing if solver handles (symbol * constant) < constant
void test3(int x) {
int buf[100];
if (x < 0)
- buf[x] = 1;
+ buf[x] = 1; // expected-warning {{Out of bound memory access (accessed memory precedes memory block)}}
}
// *** FIXME ***
More information about the cfe-commits
mailing list