[cfe-commits] [patch] Tracking simple arithmetic constraints (PR2695)
Jordy Rose
jediknil at belkadan.com
Mon Jun 14 13:21:11 PDT 2010
Finally revised and with better test cases.
Summary of changes:
- SimpleSValuator folds additive expressions ("$sym + k1 - k2").
- SimpleSValuator does not make UnknownVals everywhere it could. When the
LHS is a symbol or symbolic expression, it should probably only make a
SymExprVal if the constraint manager actually canReasonAbout() it.
- SimpleConstraintManager's subclasses can now handle expressions of the
form "($sym + k1) <> k2", where "<>" is a comparison operator.
- SimpleConstraintManager's AssumeSymREL (pure virtual) methods take an
extra "adjustment" parameter. This corresponds to "k1" in the above
expression.
- RangeSets (an implementation detail of RangeConstraintManager) are now
narrowed down using "intersections", rather than comparison-based
constraints.
- Overflow is modeled for both unsigned and signed types.
- There is no special testing for true tautological expressions (x + k1 <
MAX).
- There is now a static version of BinaryOperator::isAdditiveOp().
-------------- next part --------------
Index: lib/Checker/BasicConstraintManager.cpp
===================================================================
--- lib/Checker/BasicConstraintManager.cpp (revision 105949)
+++ lib/Checker/BasicConstraintManager.cpp (working copy)
@@ -54,22 +54,28 @@
ISetFactory(statemgr.getAllocator()) {}
const GRState* AssumeSymNE(const GRState* state, SymbolRef sym,
- const llvm::APSInt& V);
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment);
const GRState* AssumeSymEQ(const GRState* state, SymbolRef sym,
- const llvm::APSInt& V);
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment);
const GRState* AssumeSymLT(const GRState* state, SymbolRef sym,
- const llvm::APSInt& V);
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment);
const GRState* AssumeSymGT(const GRState* state, SymbolRef sym,
- const llvm::APSInt& V);
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment);
const GRState* AssumeSymGE(const GRState* state, SymbolRef sym,
- const llvm::APSInt& V);
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment);
const GRState* AssumeSymLE(const GRState* state, SymbolRef sym,
- const llvm::APSInt& V);
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment);
const GRState* AddEQ(const GRState* state, SymbolRef sym, const llvm::APSInt& V);
@@ -94,46 +100,52 @@
return new BasicConstraintManager(statemgr, subengine);
}
+
const GRState*
BasicConstraintManager::AssumeSymNE(const GRState *state, SymbolRef sym,
- const llvm::APSInt& V) {
- // First, determine if sym == X, where X != V.
+ const llvm::APSInt &V,
+ const llvm::APSInt &Adjustment) {
+ // First, determine if sym == X, where X+Adjustment != V.
+ llvm::APSInt Adjusted = V-Adjustment;
if (const llvm::APSInt* X = getSymVal(state, sym)) {
- bool isFeasible = (*X != V);
+ bool isFeasible = (*X != Adjusted);
return isFeasible ? state : NULL;
}
- // Second, determine if sym != V.
- if (isNotEqual(state, sym, V))
+ // Second, determine if sym+Adjustment != V.
+ if (isNotEqual(state, sym, Adjusted))
return state;
// If we reach here, sym is not a constant and we don't know if it is != V.
// Make that assumption.
- return AddNE(state, sym, V);
+ return AddNE(state, sym, Adjusted);
}
-const GRState *BasicConstraintManager::AssumeSymEQ(const GRState *state,
- SymbolRef sym,
- const llvm::APSInt &V) {
- // First, determine if sym == X, where X != V.
+const GRState*
+BasicConstraintManager::AssumeSymEQ(const GRState *state, SymbolRef sym,
+ const llvm::APSInt &V,
+ const llvm::APSInt &Adjustment) {
+ // First, determine if sym == X, where X+Adjustment != V.
+ llvm::APSInt Adjusted = V-Adjustment;
if (const llvm::APSInt* X = getSymVal(state, sym)) {
- bool isFeasible = *X == V;
+ bool isFeasible = (*X == Adjusted);
return isFeasible ? state : NULL;
}
- // Second, determine if sym != V.
- if (isNotEqual(state, sym, V))
+ // Second, determine if sym+Adjustment != V.
+ if (isNotEqual(state, sym, Adjusted))
return NULL;
// If we reach here, sym is not a constant and we don't know if it is == V.
// Make that assumption.
- return AddEQ(state, sym, V);
+ return AddEQ(state, sym, Adjusted);
}
-// These logic will be handled in another ConstraintManager.
-const GRState *BasicConstraintManager::AssumeSymLT(const GRState *state,
- SymbolRef sym,
- const llvm::APSInt& V) {
+// The logic for these will be handled in another ConstraintManager.
+const GRState*
+BasicConstraintManager::AssumeSymLT(const GRState *state, SymbolRef sym,
+ const llvm::APSInt &V,
+ const llvm::APSInt &Adjustment) {
// Is 'V' the smallest possible value?
if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
// sym cannot be any value less than 'V'. This path is infeasible.
@@ -141,13 +153,13 @@
}
// FIXME: For now have assuming x < y be the same as assuming sym != V;
- return AssumeSymNE(state, sym, V);
+ return AssumeSymNE(state, sym, V, Adjustment);
}
-const GRState *BasicConstraintManager::AssumeSymGT(const GRState *state,
- SymbolRef sym,
- const llvm::APSInt& V) {
-
+const GRState*
+BasicConstraintManager::AssumeSymGT(const GRState *state, SymbolRef sym,
+ const llvm::APSInt &V,
+ const llvm::APSInt &Adjustment) {
// Is 'V' the largest possible value?
if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
// sym cannot be any value greater than 'V'. This path is infeasible.
@@ -155,56 +167,60 @@
}
// FIXME: For now have assuming x > y be the same as assuming sym != V;
- return AssumeSymNE(state, sym, V);
+ return AssumeSymNE(state, sym, V, Adjustment);
}
-const GRState *BasicConstraintManager::AssumeSymGE(const GRState *state,
- SymbolRef sym,
- const llvm::APSInt &V) {
-
- // Reject a path if the value of sym is a constant X and !(X >= V).
+const GRState*
+BasicConstraintManager::AssumeSymGE(const GRState *state, SymbolRef sym,
+ const llvm::APSInt &V,
+ const llvm::APSInt &Adjustment) {
+ // Reject a path if the value of sym is a constant X and !(X+Adj >= V).
if (const llvm::APSInt *X = getSymVal(state, sym)) {
- bool isFeasible = *X >= V;
+ bool isFeasible = (*X >= V-Adjustment);
return isFeasible ? state : NULL;
}
// Sym is not a constant, but it is worth looking to see if V is the
// maximum integer value.
if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
- // If we know that sym != V, then this condition is infeasible since
- // there is no other value greater than V.
- bool isFeasible = !isNotEqual(state, sym, V);
+ llvm::APSInt Adjusted = V-Adjustment;
+ // If we know that sym != V (after adjustment), then this condition
+ // is infeasible since there is no other value greater than V.
+ bool isFeasible = !isNotEqual(state, sym, Adjusted);
+
// If the path is still feasible then as a consequence we know that
- // 'sym == V' because we cannot have 'sym > V' (no larger values).
+ // 'sym+Adjustment == V' because there are no larger values.
// Add this constraint.
- return isFeasible ? AddEQ(state, sym, V) : NULL;
+ return isFeasible ? AddEQ(state, sym, Adjusted) : NULL;
}
return state;
}
const GRState*
-BasicConstraintManager::AssumeSymLE(const GRState* state, SymbolRef sym,
- const llvm::APSInt& V) {
-
- // Reject a path if the value of sym is a constant X and !(X <= V).
+BasicConstraintManager::AssumeSymLE(const GRState *state, SymbolRef sym,
+ const llvm::APSInt &V,
+ const llvm::APSInt &Adjustment) {
+ // Reject a path if the value of sym is a constant X and !(X+Adj <= V).
if (const llvm::APSInt* X = getSymVal(state, sym)) {
- bool isFeasible = *X <= V;
+ bool isFeasible = (*X <= V-Adjustment);
return isFeasible ? state : NULL;
}
// Sym is not a constant, but it is worth looking to see if V is the
// minimum integer value.
if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
- // If we know that sym != V, then this condition is infeasible since
- // there is no other value less than V.
- bool isFeasible = !isNotEqual(state, sym, V);
+ llvm::APSInt Adjusted = V-Adjustment;
+ // If we know that sym != V (after adjustment), then this condition
+ // is infeasible since there is no other value less than V.
+ bool isFeasible = !isNotEqual(state, sym, Adjusted);
+
// If the path is still feasible then as a consequence we know that
- // 'sym == V' because we cannot have 'sym < V' (no smaller values).
+ // 'sym+Adjustment == V' because there are no smaller values.
// Add this constraint.
- return isFeasible ? AddEQ(state, sym, V) : NULL;
+ return isFeasible ? AddEQ(state, sym, Adjusted) : NULL;
}
return state;
@@ -213,7 +229,7 @@
const GRState* BasicConstraintManager::AddEQ(const GRState* state, SymbolRef sym,
const llvm::APSInt& V) {
// Create a new state with the old binding replaced.
- return state->set<ConstEq>(sym, &V);
+ return state->set<ConstEq>(sym, &state->getBasicVals().getValue(V));
}
const GRState* BasicConstraintManager::AddNE(const GRState* state, SymbolRef sym,
@@ -224,7 +240,7 @@
GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
// Now add V to the NE set.
- S = ISetFactory.Add(S, &V);
+ S = ISetFactory.Add(S, &state->getBasicVals().getValue(V));
// Create a new state with the old binding replaced.
return state->set<ConstNotEq>(sym, S);
@@ -243,7 +259,7 @@
const ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym);
// See if V is present in the NE-set.
- return T ? T->contains(&V) : false;
+ return T ? T->contains(&state->getBasicVals().getValue(V)) : false;
}
bool BasicConstraintManager::isEqual(const GRState* state, SymbolRef sym,
Index: lib/Checker/RangeConstraintManager.cpp
===================================================================
--- lib/Checker/RangeConstraintManager.cpp (revision 105949)
+++ lib/Checker/RangeConstraintManager.cpp (working copy)
@@ -105,97 +105,73 @@
return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0;
}
- /// AddEQ - Create a new RangeSet with the additional constraint that the
- /// value be equal to V.
- RangeSet AddEQ(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
- // Search for a range that includes 'V'. If so, return a new RangeSet
- // representing { [V, V] }.
- for (PrimRangeSet::iterator i = begin(), e = end(); i!=e; ++i)
- if (i->Includes(V))
- return RangeSet(F, V, V);
-
- return RangeSet(F);
- }
-
- /// AddNE - Create a new RangeSet with the additional constraint that the
- /// value be not be equal to V.
- RangeSet AddNE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
- PrimRangeSet newRanges = ranges;
-
- // FIXME: We can perhaps enhance ImmutableSet to do this search for us
- // in log(N) time using the sorted property of the internal AVL tree.
- for (iterator i = begin(), e = end(); i != e; ++i) {
- if (i->Includes(V)) {
- // Remove the old range.
- newRanges = F.Remove(newRanges, *i);
- // Split the old range into possibly one or two ranges.
- if (V != i->From())
- newRanges = F.Add(newRanges, Range(i->From(), BV.Sub1(V)));
- if (V != i->To())
- newRanges = F.Add(newRanges, Range(BV.Add1(V), i->To()));
- // All of the ranges are non-overlapping, so we can stop.
+private:
+ void IntersectInRange(BasicValueFactory &BV, Factory &F,
+ const llvm::APSInt &Lower,
+ const llvm::APSInt &Upper,
+ PrimRangeSet &newRanges,
+ PrimRangeSet::iterator &i,
+ PrimRangeSet::iterator &e) const {
+ // There are six cases for each range R in the set:
+ // 1. R is entirely before the intersection range.
+ // 2. R is entirely after the intersection range.
+ // 3. R contains the entire intersection range.
+ // 4. R starts before the intersection range and ends in the middle.
+ // 5. R starts in the middle of the intersection range and ends after it.
+ // 6. R is entirely contained in the intersection range.
+ // These correspond to each of the conditions below.
+ for (/* i = begin(), e = end() */; i != e; ++i) {
+ if (i->To() < Lower) {
+ continue;
+ }
+ if (i->From() > Upper) {
break;
}
- }
- return newRanges;
- }
-
- /// AddNE - Create a new RangeSet with the additional constraint that the
- /// value be less than V.
- RangeSet AddLT(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
- PrimRangeSet newRanges = F.GetEmptySet();
-
- for (iterator i = begin(), e = end() ; i != e ; ++i) {
- if (i->Includes(V) && i->From() < V)
- newRanges = F.Add(newRanges, Range(i->From(), BV.Sub1(V)));
- else if (i->To() < V)
- newRanges = F.Add(newRanges, *i);
+ if (i->Includes(Lower)) {
+ if (i->Includes(Upper)) {
+ newRanges = F.Add(newRanges, Range(BV.getValue(Lower),
+ BV.getValue(Upper)));
+ break;
+ } else
+ newRanges = F.Add(newRanges, Range(BV.getValue(Lower), i->To()));
+ } else {
+ if (i->Includes(Upper)) {
+ newRanges = F.Add(newRanges, Range(i->From(), BV.getValue(Upper)));
+ break;
+ } else
+ newRanges = F.Add(newRanges, *i);
+ }
}
-
- return newRanges;
}
- RangeSet AddLE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
+public:
+ RangeSet Intersect(BasicValueFactory &BV, Factory &F,
+ const llvm::APSInt &Lower,
+ const llvm::APSInt &Upper) const {
PrimRangeSet newRanges = F.GetEmptySet();
- for (iterator i = begin(), e = end(); i != e; ++i) {
- // Strictly we should test for includes *V + 1, but no harm is
- // done by this formulation
- if (i->Includes(V))
- newRanges = F.Add(newRanges, Range(i->From(), V));
- else if (i->To() <= V)
- newRanges = F.Add(newRanges, *i);
- }
-
+ PrimRangeSet::iterator i = begin(), e = end();
+ IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);
return newRanges;
}
- RangeSet AddGT(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
- PrimRangeSet newRanges = F.GetEmptySet();
+ RangeSet Intersect(BasicValueFactory &BV, Factory &F,
+ const llvm::APSInt &FirstLower,
+ const llvm::APSInt &FirstUpper,
+ const llvm::APSInt &SecondLower,
+ const llvm::APSInt &SecondUpper) const {
+ assert((FirstLower < SecondLower) &&
+ "The first range should be numerically before the second range.");
- for (PrimRangeSet::iterator i = begin(), e = end(); i != e; ++i) {
- if (i->Includes(V) && i->To() > V)
- newRanges = F.Add(newRanges, Range(BV.Add1(V), i->To()));
- else if (i->From() > V)
- newRanges = F.Add(newRanges, *i);
- }
+ // assert(SecondLower > FirstUpper+1)
+ assert(((SecondLower - FirstUpper).ugt(1)) &&
+ "Intersect ranges should not be continuous");
- return newRanges;
- }
-
- RangeSet AddGE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
PrimRangeSet newRanges = F.GetEmptySet();
-
- for (PrimRangeSet::iterator i = begin(), e = end(); i != e; ++i) {
- // Strictly we should test for includes *V - 1, but no harm is
- // done by this formulation
- if (i->Includes(V))
- newRanges = F.Add(newRanges, Range(V, i->To()));
- else if (i->From() >= V)
- newRanges = F.Add(newRanges, *i);
- }
-
+ PrimRangeSet::iterator i = begin(), e = end();
+ IntersectInRange(BV, F, FirstLower, FirstUpper, newRanges, i, e);
+ IntersectInRange(BV, F, SecondLower, SecondUpper, newRanges, i, e);
return newRanges;
}
@@ -237,23 +213,29 @@
RangeConstraintManager(GRSubEngine &subengine)
: SimpleConstraintManager(subengine) {}
- const GRState* AssumeSymNE(const GRState* St, SymbolRef sym,
- const llvm::APSInt& V);
+ const GRState* AssumeSymNE(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
- const GRState* AssumeSymEQ(const GRState* St, SymbolRef sym,
- const llvm::APSInt& V);
+ const GRState* AssumeSymEQ(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
- const GRState* AssumeSymLT(const GRState* St, SymbolRef sym,
- const llvm::APSInt& V);
+ const GRState* AssumeSymLT(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
- const GRState* AssumeSymGT(const GRState* St, SymbolRef sym,
- const llvm::APSInt& V);
+ const GRState* AssumeSymGT(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
- const GRState* AssumeSymGE(const GRState* St, SymbolRef sym,
- const llvm::APSInt& V);
+ const GRState* AssumeSymGE(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
- const GRState* AssumeSymLE(const GRState* St, SymbolRef sym,
- const llvm::APSInt& V);
+ const GRState* AssumeSymLE(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment);
const llvm::APSInt* getSymVal(const GRState* St, SymbolRef sym) const;
@@ -303,10 +285,6 @@
return state->set<ConstraintRange>(CR);
}
-//===------------------------------------------------------------------------===
-// AssumeSymX methods: public interface for RangeConstraintManager.
-//===------------------------------------------------------------------------===/
-
RangeSet
RangeConstraintManager::GetRange(const GRState *state, SymbolRef sym) {
if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
@@ -323,21 +301,179 @@
// AssumeSymX methods: public interface for RangeConstraintManager.
//===------------------------------------------------------------------------===/
-#define AssumeX(OP)\
-const GRState*\
-RangeConstraintManager::AssumeSym ## OP(const GRState* state, SymbolRef sym,\
- const llvm::APSInt& V){\
- const RangeSet& R = GetRange(state, sym).Add##OP(state->getBasicVals(), F, V);\
- return !R.isEmpty() ? state->set<ConstraintRange>(sym, R) : NULL;\
+// The syntax for ranges below is mathematical, using [x, y] for inclusive
+// bounds and (x, y) for exclusive bounds.
+
+const GRState*
+RangeConstraintManager::AssumeSymNE(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ BasicValueFactory &BV = state->getBasicVals();
+
+ QualType T = state->getSymbolManager().getType(sym);
+ const llvm::APSInt &Min = BV.getMinValue(T);
+ const llvm::APSInt &Max = BV.getMaxValue(T);
+ llvm::APSInt AdjInt = Int-Adjustment;
+
+ if (AdjInt == Min) {
+ // (Min, Max]
+ ++AdjInt;
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, AdjInt, Max);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+
+ } else if (AdjInt == Max) {
+ // [Min, Max)
+ --AdjInt;
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Min, AdjInt);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+
+ } else {
+ // [Min, Int-Adjustment) and (Int-Adjustment, Max]
+ llvm::APSInt AdjustedUpwards(AdjInt);
+ --AdjInt;
+ ++AdjustedUpwards;
+
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Min, AdjInt,
+ AdjustedUpwards, Max);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+ }
}
-AssumeX(EQ)
-AssumeX(NE)
-AssumeX(LT)
-AssumeX(GT)
-AssumeX(LE)
-AssumeX(GE)
+const GRState*
+RangeConstraintManager::AssumeSymEQ(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ // [Int-Adjustment, Int-Adjustment]
+ BasicValueFactory &BV = state->getBasicVals();
+ llvm::APSInt AdjInt = Int-Adjustment;
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, AdjInt, AdjInt);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+const GRState*
+RangeConstraintManager::AssumeSymLT(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ BasicValueFactory &BV = state->getBasicVals();
+
+ QualType T = state->getSymbolManager().getType(sym);
+ const llvm::APSInt &Min = BV.getMinValue(T);
+
+ // Special case for Int == Min. This is always false.
+ if (Int == Min)
+ return NULL;
+
+ llvm::APSInt Lower = Min-Adjustment;
+ llvm::APSInt Upper = Int-Adjustment;
+ --Upper;
+
+ if (Adjustment == 0 || Min+Adjustment >= Int) {
+ // [Min-Adjustment, Int-Adjustment)
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+
+ } else {
+ // [Min-Adjustment, Max] and [Min, Int-Adjustment)
+ const llvm::APSInt &Max = BV.getMaxValue(T);
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Min, Upper,
+ Lower, Max);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+ }
+}
+
+const GRState*
+RangeConstraintManager::AssumeSymGT(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ BasicValueFactory &BV = state->getBasicVals();
+
+ QualType T = state->getSymbolManager().getType(sym);
+ const llvm::APSInt &Max = BV.getMaxValue(T);
+
+ // Special case for Int == Max. This is always false.
+ if (Int == Max)
+ return NULL;
+
+ llvm::APSInt Lower = Int-Adjustment;
+ llvm::APSInt Upper = Max-Adjustment;
+ ++Lower;
+
+ if (Adjustment == 0 || Max+Adjustment <= Int) {
+ // (Int-Adjustment, Max-Adjustment]
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+
+ } else {
+ // (Int-Adjustment, Max] and [Min, Max-Adjustment]
+ const llvm::APSInt &Min = BV.getMinValue(T);
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Min, Upper,
+ Lower, Max);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+ }
+}
+
+const GRState*
+RangeConstraintManager::AssumeSymGE(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ BasicValueFactory &BV = state->getBasicVals();
+
+ QualType T = state->getSymbolManager().getType(sym);
+ const llvm::APSInt &Min = BV.getMinValue(T);
+
+ // Special case for Int == Min. This is always feasible.
+ if (Int == Min)
+ return state;
+
+ const llvm::APSInt &Max = BV.getMaxValue(T);
+
+ llvm::APSInt Lower = Int-Adjustment;
+ llvm::APSInt Upper = Max-Adjustment;
+
+ if (Adjustment == 0 || Max+Adjustment < Int) {
+ // [Int-Adjustment, Max-Adjustment]
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+
+ } else {
+ // [Int-Adjustment, Max] and [Min, Max-Adjustment]
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Min, Upper,
+ Lower, Max);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+ }
+}
+
+const GRState*
+RangeConstraintManager::AssumeSymLE(const GRState* state, SymbolRef sym,
+ const llvm::APSInt& Int,
+ const llvm::APSInt& Adjustment) {
+ BasicValueFactory &BV = state->getBasicVals();
+
+ QualType T = state->getSymbolManager().getType(sym);
+ const llvm::APSInt &Max = BV.getMaxValue(T);
+
+ // Special case for Int == Max. This is always feasible.
+ if (Int == Max)
+ return state;
+
+ const llvm::APSInt &Min = BV.getMinValue(T);
+
+ llvm::APSInt Lower = Min-Adjustment;
+ llvm::APSInt Upper = Int-Adjustment;
+
+ if (Adjustment == 0 || Min+Adjustment > Int) {
+ // [Min-Adjustment, Int-Adjustment]
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+
+ } else {
+ // [Min-Adjustment, Max] and [Min, Int-Adjustment]
+ RangeSet New = GetRange(state, sym).Intersect(BV, F, Min, Upper,
+ Lower, Max);
+ return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+ }
+}
+
//===------------------------------------------------------------------------===
// Pretty-printing.
//===------------------------------------------------------------------------===/
Index: lib/Checker/SimpleConstraintManager.cpp
===================================================================
--- lib/Checker/SimpleConstraintManager.cpp (revision 105949)
+++ lib/Checker/SimpleConstraintManager.cpp (working copy)
@@ -35,12 +35,11 @@
case BinaryOperator::Or:
case BinaryOperator::Xor:
return false;
- // We don't reason yet about arithmetic constraints on symbolic values.
+ // We don't reason yet about these 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;
@@ -90,12 +89,11 @@
while (SubR) {
// FIXME: now we only find the first symbolic region.
if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
+ const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth();
if (Assumption)
- return AssumeSymNE(state, SymR->getSymbol(),
- BasicVals.getZeroWithPtrWidth());
+ return AssumeSymNE(state, SymR->getSymbol(), zero, zero);
else
- return AssumeSymEQ(state, SymR->getSymbol(),
- BasicVals.getZeroWithPtrWidth());
+ return AssumeSymEQ(state, SymR->getSymbol(), zero, zero);
}
SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
}
@@ -121,11 +119,27 @@
return SU.ProcessAssume(state, cond, assumption);
}
+static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
+ // FIXME: This should probably be part of BinaryOperator, since this isn't
+ // the only place it's used. (This code was copied from SimpleSValuator.cpp.)
+ switch (op) {
+ default:
+ assert(false && "Invalid opcode.");
+ case BinaryOperator::LT: return BinaryOperator::GE;
+ case BinaryOperator::GT: return BinaryOperator::LE;
+ case BinaryOperator::LE: return BinaryOperator::GT;
+ case BinaryOperator::GE: return BinaryOperator::LT;
+ case BinaryOperator::EQ: return BinaryOperator::NE;
+ case BinaryOperator::NE: return BinaryOperator::EQ;
+ }
+}
+
const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
NonLoc Cond,
bool Assumption) {
- // We cannot reason about SymIntExpr and SymSymExpr.
+ // We cannot reason about SymSymExprs,
+ // and can only reason about some SymIntExprs.
if (!canReasonAbout(Cond)) {
// Just return the current state indicating that the path is feasible.
// This may be an over-approximation of what is possible.
@@ -144,30 +158,42 @@
SymbolRef sym = SV.getSymbol();
QualType T = SymMgr.getType(sym);
const llvm::APSInt &zero = BasicVals.getValue(0, T);
-
- return Assumption ? AssumeSymNE(state, sym, zero)
- : AssumeSymEQ(state, sym, zero);
+ if (Assumption)
+ return AssumeSymNE(state, sym, zero, zero);
+ else
+ return AssumeSymEQ(state, sym, zero, zero);
}
case nonloc::SymExprValKind: {
nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
- if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression())){
- // FIXME: This is a hack. It silently converts the RHS integer to be
- // of the same type as on the left side. This should be removed once
- // we support truncation/extension of symbolic values.
- GRStateManager &StateMgr = state->getStateManager();
- ASTContext &Ctx = StateMgr.getContext();
- QualType LHSType = SE->getLHS()->getType(Ctx);
- BasicValueFactory &BasicVals = StateMgr.getBasicVals();
- const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS());
- SymIntExpr SENew(SE->getLHS(), SE->getOpcode(), RHS, SE->getType(Ctx));
- return AssumeSymInt(state, Assumption, &SENew);
- }
+ // For now, we only handle expressions whose RHS is an integer.
+ // All other expressions are assumed to be feasible.
+ const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression());
+ if (!SE)
+ return state;
- // For all other symbolic expressions, over-approximate and consider
- // the constraint feasible.
- return state;
+ GRStateManager &StateMgr = state->getStateManager();
+ ASTContext &Ctx = StateMgr.getContext();
+ BasicValueFactory &BasicVals = StateMgr.getBasicVals();
+
+ // FIXME: This is a hack. It silently converts the RHS integer to be
+ // of the same type as on the left side. This should be removed once
+ // we support truncation/extension of symbolic values.
+ const SymExpr *LHS = SE->getLHS();
+ QualType LHSType = LHS->getType(Ctx);
+ const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS());
+
+ BinaryOperator::Opcode op = SE->getOpcode();
+ // FIXME: We should implicitly compare non-comparison expressions to 0.
+ if (!BinaryOperator::isComparisonOp(op))
+ return state;
+
+ // From here on out, op is the real comparison we'll be testing.
+ if (!Assumption)
+ op = NegateComparison(op);
+
+ return AssumeSymRel(state, LHS, op, RHS);
}
case nonloc::ConcreteIntKind: {
@@ -182,43 +208,76 @@
} // end switch
}
-const GRState *SimpleConstraintManager::AssumeSymInt(const GRState *state,
- bool Assumption,
- const SymIntExpr *SE) {
+const GRState *SimpleConstraintManager::AssumeSymRel(const GRState *state,
+ const SymExpr *LHS,
+ BinaryOperator::Opcode op,
+ const llvm::APSInt& Int) {
+ 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(Int.getBitWidth(), Int.isUnsigned());
- // Here we assume that LHS is a symbol. This is consistent with the
- // rest of the constraint manager logic.
- SymbolRef Sym = cast<SymbolData>(SE->getLHS());
- const llvm::APSInt &Int = SE->getRHS();
+ // First check if the LHS is a simple symbol reference.
+ SymbolRef Sym = dyn_cast<SymbolData>(LHS);
+ if (!Sym) {
+ // Next, see if it's a "($sym+constant1)" expression.
+ const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
- switch (SE->getOpcode()) {
+ // 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 BinaryOperator::Add:
+ Adjustment = SE->getRHS();
+ break;
+ case BinaryOperator::Sub:
+ Adjustment = -SE->getRHS();
+ break;
+ default:
+ // We don't handle non-additive operators.
+ // Give up and assume the constraint is feasible.
+ return state;
+ }
+ }
+
+ switch (op) {
default:
// No logic yet for other operators. Assume the constraint is feasible.
return state;
case BinaryOperator::EQ:
- return Assumption ? AssumeSymEQ(state, Sym, Int)
- : AssumeSymNE(state, Sym, Int);
+ return AssumeSymEQ(state, Sym, Int, Adjustment);
case BinaryOperator::NE:
- return Assumption ? AssumeSymNE(state, Sym, Int)
- : AssumeSymEQ(state, Sym, Int);
+ return AssumeSymNE(state, Sym, Int, Adjustment);
+
case BinaryOperator::GT:
- return Assumption ? AssumeSymGT(state, Sym, Int)
- : AssumeSymLE(state, Sym, Int);
+ return AssumeSymGT(state, Sym, Int, Adjustment);
case BinaryOperator::GE:
- return Assumption ? AssumeSymGE(state, Sym, Int)
- : AssumeSymLT(state, Sym, Int);
+ return AssumeSymGE(state, Sym, Int, Adjustment);
case BinaryOperator::LT:
- return Assumption ? AssumeSymLT(state, Sym, Int)
- : AssumeSymGE(state, Sym, Int);
+ return AssumeSymLT(state, Sym, Int, Adjustment);
case BinaryOperator::LE:
- return Assumption ? AssumeSymLE(state, Sym, Int)
- : AssumeSymGT(state, Sym, Int);
+ return AssumeSymLE(state, Sym, Int, Adjustment);
} // end switch
}
Index: lib/Checker/SimpleConstraintManager.h
===================================================================
--- lib/Checker/SimpleConstraintManager.h (revision 105949)
+++ lib/Checker/SimpleConstraintManager.h (working copy)
@@ -38,8 +38,10 @@
const GRState *Assume(const GRState *state, NonLoc Cond, bool Assumption);
- const GRState *AssumeSymInt(const GRState *state, bool Assumption,
- const SymIntExpr *SE);
+ const GRState *AssumeSymRel(const GRState *state,
+ const SymExpr *LHS,
+ BinaryOperator::Opcode op,
+ const llvm::APSInt& Int);
const GRState *AssumeInBound(const GRState *state, DefinedSVal Idx,
DefinedSVal UpperBound,
@@ -51,23 +53,31 @@
// Interface that subclasses must implement.
//===------------------------------------------------------------------===//
+ // Each of these is of the form "$sym+Adj <> V", where "<>" is the comparison
+ // operation for the method being invoked.
virtual const GRState *AssumeSymNE(const GRState *state, SymbolRef sym,
- const llvm::APSInt& V) = 0;
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment) = 0;
virtual const GRState *AssumeSymEQ(const GRState *state, SymbolRef sym,
- const llvm::APSInt& V) = 0;
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment) = 0;
virtual const GRState *AssumeSymLT(const GRState *state, SymbolRef sym,
- const llvm::APSInt& V) = 0;
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment) = 0;
virtual const GRState *AssumeSymGT(const GRState *state, SymbolRef sym,
- const llvm::APSInt& V) = 0;
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment) = 0;
virtual const GRState *AssumeSymLE(const GRState *state, SymbolRef sym,
- const llvm::APSInt& V) = 0;
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment) = 0;
virtual const GRState *AssumeSymGE(const GRState *state, SymbolRef sym,
- const llvm::APSInt& V) = 0;
+ const llvm::APSInt& V,
+ const llvm::APSInt& Adjustment) = 0;
//===------------------------------------------------------------------===//
// Internal implementation.
Index: lib/Checker/SimpleSValuator.cpp
===================================================================
--- lib/Checker/SimpleSValuator.cpp (revision 105949)
+++ lib/Checker/SimpleSValuator.cpp (working copy)
@@ -261,63 +261,88 @@
}
}
case nonloc::SymExprValKind: {
- // Logical not?
- if (!(op == BinaryOperator::EQ && rhs.isZeroConstant()))
+ nonloc::SymExprVal *selhs = cast<nonloc::SymExprVal>(&lhs);
+
+ // Only handle LHS of the form "$sym op constant", at least for now.
+ const SymIntExpr *symIntExpr =
+ dyn_cast<SymIntExpr>(selhs->getSymbolicExpression());
+
+ if (!symIntExpr)
return UnknownVal();
- const SymExpr *symExpr =
- cast<nonloc::SymExprVal>(lhs).getSymbolicExpression();
+ // Is this a logical not? (!x is represented as x == 0.)
+ if (op == BinaryOperator::EQ && rhs.isZeroConstant()) {
+ // We know how to negate certain expressions. Simplify them here.
- // Only handle ($sym op constant) for now.
- if (const SymIntExpr *symIntExpr = dyn_cast<SymIntExpr>(symExpr)) {
BinaryOperator::Opcode opc = symIntExpr->getOpcode();
switch (opc) {
- case BinaryOperator::LAnd:
- case BinaryOperator::LOr:
- assert(false && "Logical operators handled by branching logic.");
- return UnknownVal();
- case BinaryOperator::Assign:
- case BinaryOperator::MulAssign:
- case BinaryOperator::DivAssign:
- case BinaryOperator::RemAssign:
- case BinaryOperator::AddAssign:
- case BinaryOperator::SubAssign:
- case BinaryOperator::ShlAssign:
- case BinaryOperator::ShrAssign:
- case BinaryOperator::AndAssign:
- case BinaryOperator::XorAssign:
- case BinaryOperator::OrAssign:
- case BinaryOperator::Comma:
- assert(false && "'=' and ',' operators handled by GRExprEngine.");
- return UnknownVal();
- case BinaryOperator::PtrMemD:
- case BinaryOperator::PtrMemI:
- assert(false && "Pointer arithmetic not handled here.");
- return UnknownVal();
- case BinaryOperator::Mul:
- case BinaryOperator::Div:
- case BinaryOperator::Rem:
- case BinaryOperator::Add:
- case BinaryOperator::Sub:
- case BinaryOperator::Shl:
- case BinaryOperator::Shr:
- case BinaryOperator::And:
- case BinaryOperator::Xor:
- case BinaryOperator::Or:
- // Not handled yet.
- return UnknownVal();
- case BinaryOperator::LT:
- case BinaryOperator::GT:
- case BinaryOperator::LE:
- case BinaryOperator::GE:
- case BinaryOperator::EQ:
- case BinaryOperator::NE:
- opc = NegateComparison(opc);
- assert(symIntExpr->getType(ValMgr.getContext()) == resultTy);
- return ValMgr.makeNonLoc(symIntExpr->getLHS(), opc,
- symIntExpr->getRHS(), resultTy);
+ default:
+ // We don't know how to negate this operation.
+ // Just handle it as if it were a normal comparison to 0.
+ break;
+ case BinaryOperator::LAnd:
+ case BinaryOperator::LOr:
+ assert(false && "Logical operators handled by branching logic.");
+ return UnknownVal();
+ case BinaryOperator::Assign:
+ case BinaryOperator::MulAssign:
+ case BinaryOperator::DivAssign:
+ case BinaryOperator::RemAssign:
+ case BinaryOperator::AddAssign:
+ case BinaryOperator::SubAssign:
+ case BinaryOperator::ShlAssign:
+ case BinaryOperator::ShrAssign:
+ case BinaryOperator::AndAssign:
+ case BinaryOperator::XorAssign:
+ case BinaryOperator::OrAssign:
+ case BinaryOperator::Comma:
+ assert(false && "'=' and ',' operators handled by GRExprEngine.");
+ return UnknownVal();
+ case BinaryOperator::PtrMemD:
+ case BinaryOperator::PtrMemI:
+ assert(false && "Pointer arithmetic not handled here.");
+ return UnknownVal();
+ case BinaryOperator::LT:
+ case BinaryOperator::GT:
+ case BinaryOperator::LE:
+ case BinaryOperator::GE:
+ case BinaryOperator::EQ:
+ case BinaryOperator::NE:
+ // Negate the comparison and make a value.
+ opc = NegateComparison(opc);
+ assert(symIntExpr->getType(ValMgr.getContext()) == resultTy);
+ return ValMgr.makeNonLoc(symIntExpr->getLHS(), opc,
+ symIntExpr->getRHS(), resultTy);
}
}
+
+ // For now, only handle expressions whose RHS is a constant.
+ const nonloc::ConcreteInt *rhsInt = dyn_cast<nonloc::ConcreteInt>(&rhs);
+ if (!rhsInt)
+ return UnknownVal();
+
+ // If both the LHS and the current expression are additive,
+ // fold their constants.
+ if (BinaryOperator::isAdditiveOp(op)) {
+ BinaryOperator::Opcode lop = symIntExpr->getOpcode();
+ if (BinaryOperator::isAdditiveOp(lop)) {
+ BasicValueFactory &BVF = ValMgr.getBasicValueFactory();
+ const llvm::APSInt *newRHS;
+ if (lop == op)
+ newRHS = BVF.EvaluateAPSInt(BinaryOperator::Add,
+ symIntExpr->getRHS(),
+ rhsInt->getValue());
+ else
+ newRHS = BVF.EvaluateAPSInt(BinaryOperator::Sub,
+ symIntExpr->getRHS(),
+ rhsInt->getValue());
+ return ValMgr.makeNonLoc(symIntExpr->getLHS(), lop, *newRHS,
+ resultTy);
+ }
+ }
+
+ // Otherwise, make a SymExprVal out of the expression.
+ return ValMgr.makeNonLoc(symIntExpr, op, rhsInt->getValue(), resultTy);
}
case nonloc::ConcreteIntKind: {
if (isa<nonloc::ConcreteInt>(rhs)) {
Index: include/clang/AST/Expr.h
===================================================================
--- include/clang/AST/Expr.h (revision 105949)
+++ include/clang/AST/Expr.h (working copy)
@@ -2169,7 +2169,8 @@
/// predicates to categorize the respective opcodes.
bool isMultiplicativeOp() const { return Opc >= Mul && Opc <= Rem; }
- bool isAdditiveOp() const { return Opc == Add || Opc == Sub; }
+ static bool isAdditiveOp(Opcode Opc) { return Opc == Add || Opc == Sub; }
+ bool isAdditiveOp() const { return isAdditiveOp(Opc); }
static bool isShiftOp(Opcode Opc) { return Opc == Shl || Opc == Shr; }
bool isShiftOp() const { return isShiftOp(Opc); }
Index: test/Analysis/additive-folding.c
===================================================================
--- test/Analysis/additive-folding.c (revision 0)
+++ test/Analysis/additive-folding.c (revision 0)
@@ -0,0 +1,163 @@
+// RUN: %clang_cc1 -analyze -analyzer-check-objc-mem -analyzer-experimental-checks -verify -analyzer-constraints=basic %s
+// RUN: %clang_cc1 -analyze -analyzer-check-objc-mem -analyzer-experimental-checks -verify -analyzer-constraints=range %s
+#include <limits.h>
+
+// These are used to trigger warnings.
+typedef typeof(sizeof(int)) size_t;
+void *malloc(size_t);
+void free(void *);
+#define NULL ((void*)0)
+
+//---------------
+// Plus/minus
+//---------------
+
+void separateExpressions (int a) {
+ int b = a + 1;
+ --b;
+
+ char* buf = malloc(1);
+ if (a != 0 && b == 0)
+ return; // no-warning
+ free(buf);
+}
+
+void oneLongExpression (int a) {
+ // Expression canonicalization should still allow this to work, even though
+ // the first term is on the left.
+ int b = 15 + a + 15 - 10 - 20;
+
+ char* buf = malloc(1);
+ if (a != 0 && b == 0)
+ return; // no-warning
+ free(buf);
+}
+
+//---------------
+// Comparisons
+//---------------
+
+// Equality and inequality only
+void eq_ne (unsigned a) {
+ char* b = NULL;
+ if (a == UINT_MAX)
+ b = malloc(1);
+ if (a+1 != 0)
+ return; // no-warning
+ if (a-1 != UINT_MAX-1)
+ return; // no-warning
+ free(b);
+}
+
+void ne_eq (unsigned a) {
+ char* b = NULL;
+ if (a != UINT_MAX)
+ b = malloc(1);
+ if (a+1 == 0)
+ return; // no-warning
+ if (a-1 == UINT_MAX-1)
+ return; // no-warning
+ free(b);
+}
+
+
+// Simple order comparisons with no adjustment
+void baselineGT (unsigned a) {
+ char* b = NULL;
+ if (a > 0)
+ b = malloc(1);
+ if (a == 0)
+ return; // no-warning
+ free(b);
+}
+
+void baselineGE (unsigned a) {
+ char* b = NULL;
+ if (a >= UINT_MAX)
+ b = malloc(1);
+ if (a == UINT_MAX)
+ free(b);
+ return; // no-warning
+}
+
+void baselineLT (unsigned a) {
+ char* b = NULL;
+ if (a < UINT_MAX)
+ b = malloc(1);
+ if (a == UINT_MAX)
+ return; // no-warning
+ free(b);
+}
+
+void baselineLE (unsigned a) {
+ char* b = NULL;
+ if (a <= 0)
+ b = malloc(1);
+ if (a == 0)
+ free(b);
+ return; // no-warning
+}
+
+
+// Adjustment gives each of these an extra solution!
+void adjustedGT (unsigned a) {
+ char* b = NULL;
+ if (a-1 > UINT_MAX-1)
+ b = malloc(1);
+ return; // expected-warning{{leak}}
+}
+
+void adjustedGE (unsigned a) {
+ char* b = NULL;
+ if (a-1 >= UINT_MAX-1)
+ b = malloc(1);
+ if (a == UINT_MAX)
+ free(b);
+ return; // expected-warning{{leak}}
+}
+
+void adjustedLT (unsigned a) {
+ char* b = NULL;
+ if (a+1 < 1)
+ b = malloc(1);
+ return; // expected-warning{{leak}}
+}
+
+void adjustedLE (unsigned a) {
+ char* b = NULL;
+ if (a+1 <= 1)
+ b = malloc(1);
+ if (a == 0)
+ free(b);
+ return; // expected-warning{{leak}}
+}
+
+
+// Tautologies
+void tautologyGT (unsigned a) {
+ char* b = malloc(1);
+ if (a > UINT_MAX)
+ return; // no-warning
+ free(b);
+}
+
+void tautologyGE (unsigned a) {
+ char* b = malloc(1);
+ if (a >= 0)
+ free(b);
+ return; // no-warning
+}
+
+void tautologyLT (unsigned a) {
+ char* b = malloc(1);
+ if (a < 0)
+ return; // no-warning
+ free(b);
+}
+
+void tautologyLE (unsigned a) {
+ char* b = malloc(1);
+ if (a <= UINT_MAX)
+ free(b);
+ return; // no-warning
+}
Index: test/Analysis/additive-folding-range-constraints.c
===================================================================
--- test/Analysis/additive-folding-range-constraints.c (revision 0)
+++ test/Analysis/additive-folding-range-constraints.c (revision 0)
@@ -0,0 +1,99 @@
+// RUN: %clang_cc1 -analyze -analyzer-check-objc-mem -analyzer-experimental-checks -verify -analyzer-constraints=range %s
+#include <limits.h>
+
+// These are used to trigger warnings.
+typedef typeof(sizeof(int)) size_t;
+void *malloc(size_t);
+void free(void *);
+#define NULL ((void*)0)
+
+// Each of these adjusted ranges has an adjustment small enough to split the
+// solution range across an overflow boundary (Min for <, Max for >).
+// This corresponds to one set of branches in RangeConstraintManager.
+void smallAdjustmentGT (unsigned a) {
+ char* b = NULL;
+ if (a+2 > 1)
+ b = malloc(1);
+ if (a == UINT_MAX-1 || a == UINT_MAX)
+ return; // no-warning
+ else if (a < UINT_MAX-1)
+ free(b);
+ return; // no-warning
+}
+
+void smallAdjustmentGE (unsigned a) {
+ char* b = NULL;
+ if (a+2 >= 1)
+ b = malloc(1);
+ if (a == UINT_MAX-1)
+ return; // no-warning
+ else if (a < UINT_MAX-1 || a == UINT_MAX)
+ free(b);
+ return; // no-warning
+}
+
+void smallAdjustmentLT (unsigned a) {
+ char* b = NULL;
+ if (a+1 < 2)
+ b = malloc(1);
+ if (a == 0 || a == UINT_MAX)
+ free(b);
+ return; // no-warning
+}
+
+void smallAdjustmentLE (unsigned a) {
+ char* b = NULL;
+ if (a+1 <= 2)
+ b = malloc(1);
+ if (a == 0 || a == 1 || a == UINT_MAX)
+ free(b);
+ return; // no-warning
+}
+
+
+// Each of these adjusted ranges has an adjustment large enough to push the
+// comparison value over an overflow boundary (Min for <, Max for >).
+// This corresponds to one set of branches in RangeConstraintManager.
+void largeAdjustmentGT (unsigned a) {
+ char* b = NULL;
+ if (a-2 > UINT_MAX-1)
+ b = malloc(1);
+ if (a == 1 || a == 0)
+ free(b);
+ else if (a > 1)
+ free(b);
+ return; // no-warning
+}
+
+void largeAdjustmentGE (unsigned a) {
+ char* b = NULL;
+ if (a-2 >= UINT_MAX-1)
+ b = malloc(1);
+ if (a > 1)
+ return; // no-warning
+ else if (a == 1 || a == 0)
+ free(b);
+ return; // no-warning
+}
+
+void largeAdjustmentLT (unsigned a) {
+ char* b = NULL;
+ if (a+2 < 1)
+ b = malloc(1);
+ if (a == UINT_MAX-1 || a == UINT_MAX)
+ free(b);
+ else if (a < UINT_MAX-1)
+ return; // no-warning
+ return; // no-warning
+}
+
+void largeAdjustmentLE (unsigned a) {
+ char* b = NULL;
+ if (a+2 <= 1)
+ b = malloc(1);
+ if (a < UINT_MAX-1)
+ return; // no-warning
+ else if (a == UINT_MAX-1 || a == UINT_MAX)
+ free(b);
+ return; // no-warning
+}
More information about the cfe-commits
mailing list