Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 1 | //== RangeConstraintManager.cpp - Manage range constraints.------*- C++ -*--==// |
| 2 | // |
| 3 | // The LLVM Compiler Infrastructure |
| 4 | // |
| 5 | // This file is distributed under the University of Illinois Open Source |
| 6 | // License. See LICENSE.TXT for details. |
| 7 | // |
| 8 | //===----------------------------------------------------------------------===// |
| 9 | // |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 10 | // This file defines RangeConstraintManager, a class that tracks simple |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 11 | // equality and inequality constraints on symbolic values of GRState. |
| 12 | // |
| 13 | //===----------------------------------------------------------------------===// |
| 14 | |
| 15 | #include "SimpleConstraintManager.h" |
Ted Kremenek | 1309f9a | 2010-01-25 04:41:41 +0000 | [diff] [blame] | 16 | #include "clang/Checker/PathSensitive/GRState.h" |
| 17 | #include "clang/Checker/PathSensitive/GRStateTrait.h" |
| 18 | #include "clang/Checker/PathSensitive/GRTransferFuncs.h" |
| 19 | #include "clang/Checker/ManagerRegistry.h" |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 20 | #include "llvm/Support/Debug.h" |
| 21 | #include "llvm/ADT/FoldingSet.h" |
| 22 | #include "llvm/ADT/ImmutableSet.h" |
| 23 | #include "llvm/Support/raw_ostream.h" |
| 24 | |
| 25 | using namespace clang; |
| 26 | |
Kovarththanan Rajaratnam | ba5fb5a | 2009-11-28 06:07:30 +0000 | [diff] [blame] | 27 | namespace { class ConstraintRange {}; } |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 28 | static int ConstraintRangeIndex = 0; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 29 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 30 | /// A Range represents the closed range [from, to]. The caller must |
| 31 | /// guarantee that from <= to. Note that Range is immutable, so as not |
| 32 | /// to subvert RangeSet's immutability. |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame] | 33 | namespace { |
Kovarththanan Rajaratnam | ba5fb5a | 2009-11-28 06:07:30 +0000 | [diff] [blame] | 34 | class Range : public std::pair<const llvm::APSInt*, |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame] | 35 | const llvm::APSInt*> { |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 36 | public: |
| 37 | Range(const llvm::APSInt &from, const llvm::APSInt &to) |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 38 | : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) { |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 39 | assert(from <= to); |
| 40 | } |
| 41 | bool Includes(const llvm::APSInt &v) const { |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 42 | return *first <= v && v <= *second; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 43 | } |
| 44 | const llvm::APSInt &From() const { |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 45 | return *first; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 46 | } |
| 47 | const llvm::APSInt &To() const { |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 48 | return *second; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 49 | } |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 50 | const llvm::APSInt *getConcreteValue() const { |
| 51 | return &From() == &To() ? &From() : NULL; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 52 | } |
| 53 | |
| 54 | void Profile(llvm::FoldingSetNodeID &ID) const { |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 55 | ID.AddPointer(&From()); |
| 56 | ID.AddPointer(&To()); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 57 | } |
| 58 | }; |
| 59 | |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame] | 60 | |
Kovarththanan Rajaratnam | ba5fb5a | 2009-11-28 06:07:30 +0000 | [diff] [blame] | 61 | class RangeTrait : public llvm::ImutContainerInfo<Range> { |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame] | 62 | public: |
| 63 | // When comparing if one Range is less than another, we should compare |
Ted Kremenek | e53f820 | 2009-02-18 17:42:44 +0000 | [diff] [blame] | 64 | // the actual APSInt values instead of their pointers. This keeps the order |
| 65 | // consistent (instead of comparing by pointer values) and can potentially |
| 66 | // be used to speed up some of the operations in RangeSet. |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame] | 67 | static inline bool isLess(key_type_ref lhs, key_type_ref rhs) { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 68 | return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) && |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame] | 69 | *lhs.second < *rhs.second); |
| 70 | } |
| 71 | }; |
| 72 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 73 | /// RangeSet contains a set of ranges. If the set is empty, then |
| 74 | /// there the value of a symbol is overly constrained and there are no |
| 75 | /// possible values for that symbol. |
Kovarththanan Rajaratnam | ba5fb5a | 2009-11-28 06:07:30 +0000 | [diff] [blame] | 76 | class RangeSet { |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame] | 77 | typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 78 | PrimRangeSet ranges; // no need to make const, since it is an |
| 79 | // ImmutableSet - this allows default operator= |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 80 | // to work. |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 81 | public: |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 82 | typedef PrimRangeSet::Factory Factory; |
| 83 | typedef PrimRangeSet::iterator iterator; |
| 84 | |
| 85 | RangeSet(PrimRangeSet RS) : ranges(RS) {} |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 86 | |
| 87 | iterator begin() const { return ranges.begin(); } |
| 88 | iterator end() const { return ranges.end(); } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 89 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 90 | bool isEmpty() const { return ranges.isEmpty(); } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 91 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 92 | /// Construct a new RangeSet representing '{ [from, to] }'. |
| 93 | RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to) |
Ted Kremenek | 3baf672 | 2010-11-24 00:54:37 +0000 | [diff] [blame] | 94 | : ranges(F.add(F.getEmptySet(), Range(from, to))) {} |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 95 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 96 | /// Profile - Generates a hash profile of this RangeSet for use |
| 97 | /// by FoldingSet. |
| 98 | void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); } |
| 99 | |
| 100 | /// getConcreteValue - If a symbol is contrained to equal a specific integer |
| 101 | /// constant then this method returns that value. Otherwise, it returns |
| 102 | /// NULL. |
| 103 | const llvm::APSInt* getConcreteValue() const { |
| 104 | return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 105 | } |
| 106 | |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 107 | private: |
| 108 | void IntersectInRange(BasicValueFactory &BV, Factory &F, |
| 109 | const llvm::APSInt &Lower, |
| 110 | const llvm::APSInt &Upper, |
| 111 | PrimRangeSet &newRanges, |
| 112 | PrimRangeSet::iterator &i, |
| 113 | PrimRangeSet::iterator &e) const { |
| 114 | // There are six cases for each range R in the set: |
| 115 | // 1. R is entirely before the intersection range. |
| 116 | // 2. R is entirely after the intersection range. |
| 117 | // 3. R contains the entire intersection range. |
| 118 | // 4. R starts before the intersection range and ends in the middle. |
| 119 | // 5. R starts in the middle of the intersection range and ends after it. |
| 120 | // 6. R is entirely contained in the intersection range. |
| 121 | // These correspond to each of the conditions below. |
| 122 | for (/* i = begin(), e = end() */; i != e; ++i) { |
| 123 | if (i->To() < Lower) { |
| 124 | continue; |
| 125 | } |
| 126 | if (i->From() > Upper) { |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 127 | break; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 128 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 129 | |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 130 | if (i->Includes(Lower)) { |
| 131 | if (i->Includes(Upper)) { |
Ted Kremenek | 3baf672 | 2010-11-24 00:54:37 +0000 | [diff] [blame] | 132 | newRanges = F.add(newRanges, Range(BV.getValue(Lower), |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 133 | BV.getValue(Upper))); |
| 134 | break; |
| 135 | } else |
Ted Kremenek | 3baf672 | 2010-11-24 00:54:37 +0000 | [diff] [blame] | 136 | newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To())); |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 137 | } else { |
| 138 | if (i->Includes(Upper)) { |
Ted Kremenek | 3baf672 | 2010-11-24 00:54:37 +0000 | [diff] [blame] | 139 | newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper))); |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 140 | break; |
| 141 | } else |
Ted Kremenek | 3baf672 | 2010-11-24 00:54:37 +0000 | [diff] [blame] | 142 | newRanges = F.add(newRanges, *i); |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 143 | } |
| 144 | } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 145 | } |
| 146 | |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 147 | public: |
| 148 | // Returns a set containing the values in the receiving set, intersected with |
| 149 | // the closed range [Lower, Upper]. Unlike the Range type, this range uses |
| 150 | // modular arithmetic, corresponding to the common treatment of C integer |
| 151 | // overflow. Thus, if the Lower bound is greater than the Upper bound, the |
| 152 | // range is taken to wrap around. This is equivalent to taking the |
| 153 | // intersection with the two ranges [Min, Upper] and [Lower, Max], |
| 154 | // or, alternatively, /removing/ all integers between Upper and Lower. |
| 155 | RangeSet Intersect(BasicValueFactory &BV, Factory &F, |
| 156 | const llvm::APSInt &Lower, |
| 157 | const llvm::APSInt &Upper) const { |
Ted Kremenek | 3baf672 | 2010-11-24 00:54:37 +0000 | [diff] [blame] | 158 | PrimRangeSet newRanges = F.getEmptySet(); |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 159 | |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 160 | PrimRangeSet::iterator i = begin(), e = end(); |
| 161 | if (Lower <= Upper) |
| 162 | IntersectInRange(BV, F, Lower, Upper, newRanges, i, e); |
| 163 | else { |
| 164 | // The order of the next two statements is important! |
| 165 | // IntersectInRange() does not reset the iteration state for i and e. |
| 166 | // Therefore, the lower range most be handled first. |
| 167 | IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e); |
| 168 | IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e); |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 169 | } |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 170 | return newRanges; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 171 | } |
| 172 | |
Ted Kremenek | 53ba0b6 | 2009-06-24 23:06:47 +0000 | [diff] [blame] | 173 | void print(llvm::raw_ostream &os) const { |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 174 | bool isFirst = true; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 175 | os << "{ "; |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 176 | for (iterator i = begin(), e = end(); i != e; ++i) { |
| 177 | if (isFirst) |
| 178 | isFirst = false; |
| 179 | else |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 180 | os << ", "; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 181 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 182 | os << '[' << i->From().toString(10) << ", " << i->To().toString(10) |
| 183 | << ']'; |
| 184 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 185 | os << " }"; |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 186 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 187 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 188 | bool operator==(const RangeSet &other) const { |
| 189 | return ranges == other.ranges; |
| 190 | } |
| 191 | }; |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame] | 192 | } // end anonymous namespace |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 193 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 194 | typedef llvm::ImmutableMap<SymbolRef,RangeSet> ConstraintRangeTy; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 195 | |
| 196 | namespace clang { |
| 197 | template<> |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 198 | struct GRStateTrait<ConstraintRange> |
| 199 | : public GRStatePartialTrait<ConstraintRangeTy> { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 200 | static inline void* GDMIndex() { return &ConstraintRangeIndex; } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 201 | }; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 202 | } |
| 203 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 204 | namespace { |
Kovarththanan Rajaratnam | ba5fb5a | 2009-11-28 06:07:30 +0000 | [diff] [blame] | 205 | class RangeConstraintManager : public SimpleConstraintManager{ |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 206 | RangeSet GetRange(const GRState *state, SymbolRef sym); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 207 | public: |
Ted Kremenek | 32a5808 | 2010-01-05 00:15:18 +0000 | [diff] [blame] | 208 | RangeConstraintManager(GRSubEngine &subengine) |
| 209 | : SimpleConstraintManager(subengine) {} |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 210 | |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 211 | const GRState *assumeSymNE(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 212 | const llvm::APSInt& Int, |
| 213 | const llvm::APSInt& Adjustment); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 214 | |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 215 | const GRState *assumeSymEQ(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 216 | const llvm::APSInt& Int, |
| 217 | const llvm::APSInt& Adjustment); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 218 | |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 219 | const GRState *assumeSymLT(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 220 | const llvm::APSInt& Int, |
| 221 | const llvm::APSInt& Adjustment); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 222 | |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 223 | const GRState *assumeSymGT(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 224 | const llvm::APSInt& Int, |
| 225 | const llvm::APSInt& Adjustment); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 226 | |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 227 | const GRState *assumeSymGE(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 228 | const llvm::APSInt& Int, |
| 229 | const llvm::APSInt& Adjustment); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 230 | |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 231 | const GRState *assumeSymLE(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 232 | const llvm::APSInt& Int, |
| 233 | const llvm::APSInt& Adjustment); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 234 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 235 | const llvm::APSInt* getSymVal(const GRState* St, SymbolRef sym) const; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 236 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 237 | // FIXME: Refactor into SimpleConstraintManager? |
| 238 | bool isEqual(const GRState* St, SymbolRef sym, const llvm::APSInt& V) const { |
| 239 | const llvm::APSInt *i = getSymVal(St, sym); |
| 240 | return i ? *i == V : false; |
| 241 | } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 242 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 243 | const GRState* RemoveDeadBindings(const GRState* St, SymbolReaper& SymReaper); |
| 244 | |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 245 | void print(const GRState* St, llvm::raw_ostream& Out, |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 246 | const char* nl, const char *sep); |
| 247 | |
| 248 | private: |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 249 | RangeSet::Factory F; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 250 | }; |
| 251 | |
| 252 | } // end anonymous namespace |
| 253 | |
Ted Kremenek | 32a5808 | 2010-01-05 00:15:18 +0000 | [diff] [blame] | 254 | ConstraintManager* clang::CreateRangeConstraintManager(GRStateManager&, |
| 255 | GRSubEngine &subeng) { |
| 256 | return new RangeConstraintManager(subeng); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 257 | } |
| 258 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 259 | const llvm::APSInt* RangeConstraintManager::getSymVal(const GRState* St, |
| 260 | SymbolRef sym) const { |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 261 | const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym); |
| 262 | return T ? T->getConcreteValue() : NULL; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 263 | } |
| 264 | |
| 265 | /// Scan all symbols referenced by the constraints. If the symbol is not alive |
| 266 | /// as marked in LSymbols, mark it as dead in DSymbols. |
| 267 | const GRState* |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 268 | RangeConstraintManager::RemoveDeadBindings(const GRState* state, |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 269 | SymbolReaper& SymReaper) { |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 270 | |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 271 | ConstraintRangeTy CR = state->get<ConstraintRange>(); |
| 272 | ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 273 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 274 | for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 275 | SymbolRef sym = I.getKey(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 276 | if (SymReaper.maybeDead(sym)) |
Ted Kremenek | 3baf672 | 2010-11-24 00:54:37 +0000 | [diff] [blame] | 277 | CR = CRFactory.remove(CR, sym); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 278 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 279 | |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 280 | return state->set<ConstraintRange>(CR); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 281 | } |
| 282 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 283 | RangeSet |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 284 | RangeConstraintManager::GetRange(const GRState *state, SymbolRef sym) { |
| 285 | if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym)) |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 286 | return *V; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 287 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 288 | // Lazily generate a new RangeSet representing all possible values for the |
| 289 | // given symbol type. |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 290 | QualType T = state->getSymbolManager().getType(sym); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 291 | BasicValueFactory& BV = state->getBasicVals(); |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 292 | return RangeSet(F, BV.getMinValue(T), BV.getMaxValue(T)); |
| 293 | } |
| 294 | |
| 295 | //===------------------------------------------------------------------------=== |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 296 | // assumeSymX methods: public interface for RangeConstraintManager. |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 297 | //===------------------------------------------------------------------------===/ |
| 298 | |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 299 | // The syntax for ranges below is mathematical, using [x, y] for closed ranges |
| 300 | // and (x, y) for open ranges. These ranges are modular, corresponding with |
| 301 | // a common treatment of C integer overflow. This means that these methods |
| 302 | // do not have to worry about overflow; RangeSet::Intersect can handle such a |
| 303 | // "wraparound" range. |
| 304 | // As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1, |
| 305 | // UINT_MAX, 0, 1, and 2. |
| 306 | |
| 307 | const GRState* |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 308 | RangeConstraintManager::assumeSymNE(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 309 | const llvm::APSInt& Int, |
| 310 | const llvm::APSInt& Adjustment) { |
| 311 | BasicValueFactory &BV = state->getBasicVals(); |
| 312 | |
| 313 | llvm::APSInt Lower = Int-Adjustment; |
| 314 | llvm::APSInt Upper = Lower; |
| 315 | --Lower; |
| 316 | ++Upper; |
| 317 | |
| 318 | // [Int-Adjustment+1, Int-Adjustment-1] |
| 319 | // Notice that the lower bound is greater than the upper bound. |
| 320 | RangeSet New = GetRange(state, sym).Intersect(BV, F, Upper, Lower); |
| 321 | return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 322 | } |
| 323 | |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 324 | const GRState* |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 325 | RangeConstraintManager::assumeSymEQ(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 326 | const llvm::APSInt& Int, |
| 327 | const llvm::APSInt& Adjustment) { |
| 328 | // [Int-Adjustment, Int-Adjustment] |
| 329 | BasicValueFactory &BV = state->getBasicVals(); |
| 330 | llvm::APSInt AdjInt = Int-Adjustment; |
| 331 | RangeSet New = GetRange(state, sym).Intersect(BV, F, AdjInt, AdjInt); |
| 332 | return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); |
| 333 | } |
| 334 | |
| 335 | const GRState* |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 336 | RangeConstraintManager::assumeSymLT(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 337 | const llvm::APSInt& Int, |
| 338 | const llvm::APSInt& Adjustment) { |
| 339 | BasicValueFactory &BV = state->getBasicVals(); |
| 340 | |
| 341 | QualType T = state->getSymbolManager().getType(sym); |
| 342 | const llvm::APSInt &Min = BV.getMinValue(T); |
| 343 | |
| 344 | // Special case for Int == Min. This is always false. |
| 345 | if (Int == Min) |
| 346 | return NULL; |
| 347 | |
| 348 | llvm::APSInt Lower = Min-Adjustment; |
| 349 | llvm::APSInt Upper = Int-Adjustment; |
| 350 | --Upper; |
| 351 | |
| 352 | RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper); |
| 353 | return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); |
| 354 | } |
| 355 | |
| 356 | const GRState* |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 357 | RangeConstraintManager::assumeSymGT(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 358 | const llvm::APSInt& Int, |
| 359 | const llvm::APSInt& Adjustment) { |
| 360 | BasicValueFactory &BV = state->getBasicVals(); |
| 361 | |
| 362 | QualType T = state->getSymbolManager().getType(sym); |
| 363 | const llvm::APSInt &Max = BV.getMaxValue(T); |
| 364 | |
| 365 | // Special case for Int == Max. This is always false. |
| 366 | if (Int == Max) |
| 367 | return NULL; |
| 368 | |
| 369 | llvm::APSInt Lower = Int-Adjustment; |
| 370 | llvm::APSInt Upper = Max-Adjustment; |
| 371 | ++Lower; |
| 372 | |
| 373 | RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper); |
| 374 | return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); |
| 375 | } |
| 376 | |
| 377 | const GRState* |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 378 | RangeConstraintManager::assumeSymGE(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 379 | const llvm::APSInt& Int, |
| 380 | const llvm::APSInt& Adjustment) { |
| 381 | BasicValueFactory &BV = state->getBasicVals(); |
| 382 | |
| 383 | QualType T = state->getSymbolManager().getType(sym); |
| 384 | const llvm::APSInt &Min = BV.getMinValue(T); |
| 385 | |
| 386 | // Special case for Int == Min. This is always feasible. |
| 387 | if (Int == Min) |
| 388 | return state; |
| 389 | |
| 390 | const llvm::APSInt &Max = BV.getMaxValue(T); |
| 391 | |
| 392 | llvm::APSInt Lower = Int-Adjustment; |
| 393 | llvm::APSInt Upper = Max-Adjustment; |
| 394 | |
| 395 | RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper); |
| 396 | return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); |
| 397 | } |
| 398 | |
| 399 | const GRState* |
Ted Kremenek | 28f47b9 | 2010-12-01 22:16:56 +0000 | [diff] [blame^] | 400 | RangeConstraintManager::assumeSymLE(const GRState* state, SymbolRef sym, |
Jordy Rose | ba0f61c | 2010-06-18 22:49:11 +0000 | [diff] [blame] | 401 | const llvm::APSInt& Int, |
| 402 | const llvm::APSInt& Adjustment) { |
| 403 | BasicValueFactory &BV = state->getBasicVals(); |
| 404 | |
| 405 | QualType T = state->getSymbolManager().getType(sym); |
| 406 | const llvm::APSInt &Max = BV.getMaxValue(T); |
| 407 | |
| 408 | // Special case for Int == Max. This is always feasible. |
| 409 | if (Int == Max) |
| 410 | return state; |
| 411 | |
| 412 | const llvm::APSInt &Min = BV.getMinValue(T); |
| 413 | |
| 414 | llvm::APSInt Lower = Min-Adjustment; |
| 415 | llvm::APSInt Upper = Int-Adjustment; |
| 416 | |
| 417 | RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper); |
| 418 | return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New); |
| 419 | } |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 420 | |
| 421 | //===------------------------------------------------------------------------=== |
| 422 | // Pretty-printing. |
| 423 | //===------------------------------------------------------------------------===/ |
| 424 | |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 425 | void RangeConstraintManager::print(const GRState* St, llvm::raw_ostream& Out, |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 426 | const char* nl, const char *sep) { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 427 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 428 | ConstraintRangeTy Ranges = St->get<ConstraintRange>(); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 429 | |
Ted Kremenek | dd28d00 | 2009-02-16 18:42:56 +0000 | [diff] [blame] | 430 | if (Ranges.isEmpty()) |
| 431 | return; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 432 | |
Ted Kremenek | dd28d00 | 2009-02-16 18:42:56 +0000 | [diff] [blame] | 433 | Out << nl << sep << "ranges of symbol values:"; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 434 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 435 | for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){ |
Ted Kremenek | ec751c4 | 2009-04-21 22:37:11 +0000 | [diff] [blame] | 436 | Out << nl << ' ' << I.getKey() << " : "; |
Ted Kremenek | 53ba0b6 | 2009-06-24 23:06:47 +0000 | [diff] [blame] | 437 | I.getData().print(Out); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 438 | } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 439 | } |