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 | // |
| 10 | // This file defines RangeConstraintManager, a class that tracks simple |
| 11 | // equality and inequality constraints on symbolic values of GRState. |
| 12 | // |
| 13 | //===----------------------------------------------------------------------===// |
| 14 | |
| 15 | #include "SimpleConstraintManager.h" |
| 16 | #include "clang/Analysis/PathSensitive/GRState.h" |
| 17 | #include "clang/Analysis/PathSensitive/GRStateTrait.h" |
| 18 | #include "clang/Analysis/PathSensitive/GRTransferFuncs.h" |
| 19 | #include "clang/Driver/ManagerRegistry.h" |
| 20 | #include "llvm/Support/Compiler.h" |
| 21 | #include "llvm/Support/Debug.h" |
| 22 | #include "llvm/ADT/FoldingSet.h" |
| 23 | #include "llvm/ADT/ImmutableSet.h" |
| 24 | #include "llvm/Support/raw_ostream.h" |
| 25 | |
| 26 | using namespace clang; |
| 27 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 28 | namespace { class VISIBILITY_HIDDEN ConstraintRange {}; } |
| 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 { |
| 35 | class VISIBILITY_HIDDEN Range : public std::pair<const llvm::APSInt*, |
| 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 | |
| 62 | class VISIBILITY_HIDDEN RangeTrait : public llvm::ImutContainerInfo<Range> { |
| 63 | public: |
| 64 | // When comparing if one Range is less than another, we should compare |
| 65 | // the actual APSInt values instead of their pointers. This ensures that |
| 66 | // ImmutableSets based on Range objects always are constructed |
| 67 | // with the same ordering between Ranges. The definition if 'isEqual' can |
| 68 | // remain as it is (compare pointers) because all APSInt objects within |
| 69 | // Range are uniqued by BasicValueManager. |
| 70 | static inline bool isLess(key_type_ref lhs, key_type_ref rhs) { |
| 71 | return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) && |
| 72 | *lhs.second < *rhs.second); |
| 73 | } |
| 74 | }; |
| 75 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 76 | /// RangeSet contains a set of ranges. If the set is empty, then |
| 77 | /// there the value of a symbol is overly constrained and there are no |
| 78 | /// possible values for that symbol. |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame^] | 79 | class VISIBILITY_HIDDEN RangeSet { |
| 80 | typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 81 | PrimRangeSet ranges; // no need to make const, since it is an |
| 82 | // ImmutableSet - this allows default operator= |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 83 | // to work. |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 84 | public: |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 85 | typedef PrimRangeSet::Factory Factory; |
| 86 | typedef PrimRangeSet::iterator iterator; |
| 87 | |
| 88 | RangeSet(PrimRangeSet RS) : ranges(RS) {} |
| 89 | RangeSet(Factory& F) : ranges(F.GetEmptySet()) {} |
| 90 | |
| 91 | iterator begin() const { return ranges.begin(); } |
| 92 | iterator end() const { return ranges.end(); } |
| 93 | |
| 94 | bool isEmpty() const { return ranges.isEmpty(); } |
| 95 | |
| 96 | /// Construct a new RangeSet representing '{ [from, to] }'. |
| 97 | RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to) |
| 98 | : ranges(F.Add(F.GetEmptySet(), Range(from, to))) {} |
| 99 | |
| 100 | /// Profile - Generates a hash profile of this RangeSet for use |
| 101 | /// by FoldingSet. |
| 102 | void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); } |
| 103 | |
| 104 | /// getConcreteValue - If a symbol is contrained to equal a specific integer |
| 105 | /// constant then this method returns that value. Otherwise, it returns |
| 106 | /// NULL. |
| 107 | const llvm::APSInt* getConcreteValue() const { |
| 108 | return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 109 | } |
| 110 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 111 | /// AddEQ - Create a new RangeSet with the additional constraint that the |
| 112 | /// value be equal to V. |
| 113 | RangeSet AddEQ(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 114 | // Search for a range that includes 'V'. If so, return a new RangeSet |
| 115 | // representing { [V, V] }. |
| 116 | for (PrimRangeSet::iterator i = begin(), e = end(); i!=e; ++i) |
| 117 | if (i->Includes(V)) |
| 118 | return RangeSet(F, V, V); |
| 119 | |
| 120 | return RangeSet(F); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 121 | } |
| 122 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 123 | /// AddNE - Create a new RangeSet with the additional constraint that the |
| 124 | /// value be not be equal to V. |
| 125 | RangeSet AddNE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 126 | PrimRangeSet newRanges = ranges; |
| 127 | |
| 128 | // FIXME: We can perhaps enhance ImmutableSet to do this search for us |
| 129 | // in log(N) time using the sorted property of the internal AVL tree. |
| 130 | for (iterator i = begin(), e = end(); i != e; ++i) { |
| 131 | if (i->Includes(V)) { |
| 132 | // Remove the old range. |
| 133 | newRanges = F.Remove(newRanges, *i); |
| 134 | // Split the old range into possibly one or two ranges. |
| 135 | if (V != i->From()) |
| 136 | newRanges = F.Add(newRanges, Range(i->From(), BV.Sub1(V))); |
| 137 | if (V != i->To()) |
| 138 | newRanges = F.Add(newRanges, Range(BV.Add1(V), i->To())); |
| 139 | // All of the ranges are non-overlapping, so we can stop. |
| 140 | break; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 141 | } |
| 142 | } |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 143 | |
| 144 | return newRanges; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 145 | } |
| 146 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 147 | /// AddNE - Create a new RangeSet with the additional constraint that the |
| 148 | /// value be less than V. |
| 149 | RangeSet AddLT(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 150 | PrimRangeSet newRanges = F.GetEmptySet(); |
| 151 | |
| 152 | for (iterator i = begin(), e = end() ; i != e ; ++i) { |
| 153 | if (i->Includes(V) && i->From() < V) |
| 154 | newRanges = F.Add(newRanges, Range(i->From(), BV.Sub1(V))); |
| 155 | else if (i->To() < V) |
| 156 | newRanges = F.Add(newRanges, *i); |
| 157 | } |
| 158 | |
| 159 | return newRanges; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 160 | } |
| 161 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 162 | RangeSet AddLE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 163 | PrimRangeSet newRanges = F.GetEmptySet(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 164 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 165 | for (iterator i = begin(), e = end(); i != e; ++i) { |
| 166 | // Strictly we should test for includes *V + 1, but no harm is |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 167 | // done by this formulation |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 168 | if (i->Includes(V)) |
| 169 | newRanges = F.Add(newRanges, Range(i->From(), V)); |
| 170 | else if (i->To() <= V) |
| 171 | newRanges = F.Add(newRanges, *i); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 172 | } |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 173 | |
| 174 | return newRanges; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 175 | } |
| 176 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 177 | RangeSet AddGT(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 178 | PrimRangeSet newRanges = F.GetEmptySet(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 179 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 180 | for (PrimRangeSet::iterator i = begin(), e = end(); i != e; ++i) { |
| 181 | if (i->Includes(V) && i->To() > V) |
| 182 | newRanges = F.Add(newRanges, Range(BV.Add1(V), i->To())); |
| 183 | else if (i->From() > V) |
| 184 | newRanges = F.Add(newRanges, *i); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 185 | } |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 186 | |
| 187 | return newRanges; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 188 | } |
| 189 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 190 | RangeSet AddGE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 191 | PrimRangeSet newRanges = F.GetEmptySet(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 192 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 193 | for (PrimRangeSet::iterator i = begin(), e = end(); i != e; ++i) { |
| 194 | // Strictly we should test for includes *V - 1, but no harm is |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 195 | // done by this formulation |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 196 | if (i->Includes(V)) |
| 197 | newRanges = F.Add(newRanges, Range(V, i->To())); |
| 198 | else if (i->From() >= V) |
| 199 | newRanges = F.Add(newRanges, *i); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 200 | } |
| 201 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 202 | return newRanges; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 203 | } |
| 204 | |
| 205 | void Print(std::ostream &os) const { |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 206 | bool isFirst = true; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 207 | os << "{ "; |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 208 | for (iterator i = begin(), e = end(); i != e; ++i) { |
| 209 | if (isFirst) |
| 210 | isFirst = false; |
| 211 | else |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 212 | os << ", "; |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 213 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 214 | os << '[' << i->From().toString(10) << ", " << i->To().toString(10) |
| 215 | << ']'; |
| 216 | } |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 217 | os << " }"; |
| 218 | } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 219 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 220 | bool operator==(const RangeSet &other) const { |
| 221 | return ranges == other.ranges; |
| 222 | } |
| 223 | }; |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame^] | 224 | } // end anonymous namespace |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 225 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 226 | typedef llvm::ImmutableMap<SymbolRef,RangeSet> ConstraintRangeTy; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 227 | |
| 228 | namespace clang { |
| 229 | template<> |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 230 | struct GRStateTrait<ConstraintRange> |
| 231 | : public GRStatePartialTrait<ConstraintRangeTy> { |
| 232 | static inline void* GDMIndex() { return &ConstraintRangeIndex; } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 233 | }; |
| 234 | } |
| 235 | |
| 236 | namespace { |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame^] | 237 | class VISIBILITY_HIDDEN RangeConstraintManager : public SimpleConstraintManager{ |
| 238 | RangeSet GetRange(GRStateRef state, SymbolRef sym); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 239 | public: |
| 240 | RangeConstraintManager(GRStateManager& statemgr) |
| 241 | : SimpleConstraintManager(statemgr) {} |
| 242 | |
| 243 | const GRState* AssumeSymNE(const GRState* St, SymbolRef sym, |
| 244 | const llvm::APSInt& V, bool& isFeasible); |
| 245 | |
| 246 | const GRState* AssumeSymEQ(const GRState* St, SymbolRef sym, |
| 247 | const llvm::APSInt& V, bool& isFeasible); |
| 248 | |
| 249 | const GRState* AssumeSymLT(const GRState* St, SymbolRef sym, |
| 250 | const llvm::APSInt& V, bool& isFeasible); |
| 251 | |
| 252 | const GRState* AssumeSymGT(const GRState* St, SymbolRef sym, |
| 253 | const llvm::APSInt& V, bool& isFeasible); |
| 254 | |
| 255 | const GRState* AssumeSymGE(const GRState* St, SymbolRef sym, |
| 256 | const llvm::APSInt& V, bool& isFeasible); |
| 257 | |
| 258 | const GRState* AssumeSymLE(const GRState* St, SymbolRef sym, |
| 259 | const llvm::APSInt& V, bool& isFeasible); |
| 260 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 261 | const llvm::APSInt* getSymVal(const GRState* St, SymbolRef sym) const; |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 262 | |
| 263 | // FIXME: Refactor into SimpleConstraintManager? |
| 264 | bool isEqual(const GRState* St, SymbolRef sym, const llvm::APSInt& V) const { |
| 265 | const llvm::APSInt *i = getSymVal(St, sym); |
| 266 | return i ? *i == V : false; |
| 267 | } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 268 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 269 | const GRState* RemoveDeadBindings(const GRState* St, SymbolReaper& SymReaper); |
| 270 | |
| 271 | void print(const GRState* St, std::ostream& Out, |
| 272 | const char* nl, const char *sep); |
| 273 | |
| 274 | private: |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 275 | RangeSet::Factory F; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 276 | }; |
| 277 | |
| 278 | } // end anonymous namespace |
| 279 | |
| 280 | ConstraintManager* clang::CreateRangeConstraintManager(GRStateManager& StateMgr) |
| 281 | { |
| 282 | return new RangeConstraintManager(StateMgr); |
| 283 | } |
| 284 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 285 | const llvm::APSInt* RangeConstraintManager::getSymVal(const GRState* St, |
| 286 | SymbolRef sym) const { |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 287 | const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym); |
| 288 | return T ? T->getConcreteValue() : NULL; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 289 | } |
| 290 | |
| 291 | /// Scan all symbols referenced by the constraints. If the symbol is not alive |
| 292 | /// as marked in LSymbols, mark it as dead in DSymbols. |
| 293 | const GRState* |
| 294 | RangeConstraintManager::RemoveDeadBindings(const GRState* St, |
| 295 | SymbolReaper& SymReaper) { |
| 296 | GRStateRef state(St, StateMgr); |
| 297 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 298 | ConstraintRangeTy CR = state.get<ConstraintRange>(); |
| 299 | ConstraintRangeTy::Factory& CRFactory = state.get_context<ConstraintRange>(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 300 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 301 | for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) { |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 302 | SymbolRef sym = I.getKey(); |
| 303 | if (SymReaper.maybeDead(sym)) |
| 304 | CR = CRFactory.Remove(CR, sym); |
| 305 | } |
| 306 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 307 | return state.set<ConstraintRange>(CR); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 308 | } |
| 309 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 310 | //===------------------------------------------------------------------------=== |
| 311 | // AssumeSymX methods: public interface for RangeConstraintManager. |
| 312 | //===------------------------------------------------------------------------===/ |
| 313 | |
| 314 | RangeSet |
| 315 | RangeConstraintManager::GetRange(GRStateRef state, SymbolRef sym) { |
| 316 | if (ConstraintRangeTy::data_type* V = state.get<ConstraintRange>(sym)) |
| 317 | return *V; |
| 318 | |
| 319 | // Lazily generate a new RangeSet representing all possible values for the |
| 320 | // given symbol type. |
| 321 | QualType T = state.getSymbolManager().getType(sym); |
| 322 | BasicValueFactory& BV = state.getBasicVals(); |
| 323 | return RangeSet(F, BV.getMinValue(T), BV.getMaxValue(T)); |
| 324 | } |
| 325 | |
| 326 | //===------------------------------------------------------------------------=== |
| 327 | // AssumeSymX methods: public interface for RangeConstraintManager. |
| 328 | //===------------------------------------------------------------------------===/ |
| 329 | |
| 330 | #define AssumeX(OP)\ |
| 331 | const GRState*\ |
| 332 | RangeConstraintManager::AssumeSym ## OP(const GRState* St, SymbolRef sym,\ |
| 333 | const llvm::APSInt& V, bool& isFeasible){\ |
| 334 | GRStateRef state(St, StateMgr);\ |
| 335 | const RangeSet& R = GetRange(state, sym).Add##OP(state.getBasicVals(), F, V);\ |
| 336 | isFeasible = !R.isEmpty();\ |
| 337 | return isFeasible ? state.set<ConstraintRange>(sym, R).getState() : 0;\ |
| 338 | } |
| 339 | |
| 340 | AssumeX(EQ) |
| 341 | AssumeX(NE) |
| 342 | AssumeX(LT) |
| 343 | AssumeX(GT) |
| 344 | AssumeX(LE) |
| 345 | AssumeX(GE) |
| 346 | |
| 347 | //===------------------------------------------------------------------------=== |
| 348 | // Pretty-printing. |
| 349 | //===------------------------------------------------------------------------===/ |
| 350 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 351 | void RangeConstraintManager::print(const GRState* St, std::ostream& Out, |
| 352 | const char* nl, const char *sep) { |
Ted Kremenek | dd28d00 | 2009-02-16 18:42:56 +0000 | [diff] [blame] | 353 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 354 | ConstraintRangeTy Ranges = St->get<ConstraintRange>(); |
Ted Kremenek | dd28d00 | 2009-02-16 18:42:56 +0000 | [diff] [blame] | 355 | |
| 356 | if (Ranges.isEmpty()) |
| 357 | return; |
| 358 | |
| 359 | Out << nl << sep << "ranges of symbol values:"; |
| 360 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 361 | for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){ |
Ted Kremenek | dd28d00 | 2009-02-16 18:42:56 +0000 | [diff] [blame] | 362 | Out << nl << " $" << I.getKey() << " : "; |
| 363 | I.getData().Print(Out); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 364 | } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 365 | } |