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