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" |
| 16 | #include "clang/Analysis/PathSensitive/GRState.h" |
| 17 | #include "clang/Analysis/PathSensitive/GRStateTrait.h" |
| 18 | #include "clang/Analysis/PathSensitive/GRTransferFuncs.h" |
Chandler Carruth | f465e85 | 2009-11-11 19:10:59 +0000 | [diff] [blame] | 19 | #include "clang/Analysis/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) {} |
| 86 | RangeSet(Factory& F) : ranges(F.GetEmptySet()) {} |
| 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) |
| 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 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 108 | /// AddEQ - Create a new RangeSet with the additional constraint that the |
| 109 | /// value be equal to V. |
| 110 | RangeSet AddEQ(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 111 | // Search for a range that includes 'V'. If so, return a new RangeSet |
| 112 | // representing { [V, V] }. |
| 113 | for (PrimRangeSet::iterator i = begin(), e = end(); i!=e; ++i) |
| 114 | if (i->Includes(V)) |
| 115 | return RangeSet(F, V, V); |
| 116 | |
| 117 | return RangeSet(F); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 118 | } |
| 119 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 120 | /// AddNE - Create a new RangeSet with the additional constraint that the |
| 121 | /// value be not be equal to V. |
| 122 | RangeSet AddNE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 123 | PrimRangeSet newRanges = ranges; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 124 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 125 | // FIXME: We can perhaps enhance ImmutableSet to do this search for us |
| 126 | // in log(N) time using the sorted property of the internal AVL tree. |
| 127 | for (iterator i = begin(), e = end(); i != e; ++i) { |
| 128 | if (i->Includes(V)) { |
| 129 | // Remove the old range. |
| 130 | newRanges = F.Remove(newRanges, *i); |
| 131 | // Split the old range into possibly one or two ranges. |
| 132 | if (V != i->From()) |
| 133 | newRanges = F.Add(newRanges, Range(i->From(), BV.Sub1(V))); |
| 134 | if (V != i->To()) |
| 135 | newRanges = F.Add(newRanges, Range(BV.Add1(V), i->To())); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 136 | // All of the ranges are non-overlapping, so we can stop. |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 137 | break; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 138 | } |
| 139 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 140 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 141 | return newRanges; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 142 | } |
| 143 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 144 | /// AddNE - Create a new RangeSet with the additional constraint that the |
| 145 | /// value be less than V. |
| 146 | RangeSet AddLT(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 147 | PrimRangeSet newRanges = F.GetEmptySet(); |
| 148 | |
| 149 | for (iterator i = begin(), e = end() ; i != e ; ++i) { |
| 150 | if (i->Includes(V) && i->From() < V) |
| 151 | newRanges = F.Add(newRanges, Range(i->From(), BV.Sub1(V))); |
| 152 | else if (i->To() < V) |
| 153 | newRanges = F.Add(newRanges, *i); |
| 154 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 155 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 156 | return newRanges; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 157 | } |
| 158 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 159 | RangeSet AddLE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 160 | PrimRangeSet newRanges = F.GetEmptySet(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 161 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 162 | for (iterator i = begin(), e = end(); i != e; ++i) { |
| 163 | // Strictly we should test for includes *V + 1, but no harm is |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 164 | // done by this formulation |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 165 | if (i->Includes(V)) |
| 166 | newRanges = F.Add(newRanges, Range(i->From(), V)); |
| 167 | else if (i->To() <= V) |
| 168 | newRanges = F.Add(newRanges, *i); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 169 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +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 | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 174 | RangeSet AddGT(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 175 | PrimRangeSet newRanges = F.GetEmptySet(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 176 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 177 | for (PrimRangeSet::iterator i = begin(), e = end(); i != e; ++i) { |
| 178 | if (i->Includes(V) && i->To() > V) |
| 179 | newRanges = F.Add(newRanges, Range(BV.Add1(V), i->To())); |
| 180 | else if (i->From() > V) |
| 181 | newRanges = F.Add(newRanges, *i); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 182 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 183 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 184 | return newRanges; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 185 | } |
| 186 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 187 | RangeSet AddGE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) { |
| 188 | PrimRangeSet newRanges = F.GetEmptySet(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 189 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 190 | for (PrimRangeSet::iterator i = begin(), e = end(); i != e; ++i) { |
| 191 | // Strictly we should test for includes *V - 1, but no harm is |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 192 | // done by this formulation |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 193 | if (i->Includes(V)) |
| 194 | newRanges = F.Add(newRanges, Range(V, i->To())); |
| 195 | else if (i->From() >= V) |
| 196 | newRanges = F.Add(newRanges, *i); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 197 | } |
| 198 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 199 | return newRanges; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 200 | } |
| 201 | |
Ted Kremenek | 53ba0b6 | 2009-06-24 23:06:47 +0000 | [diff] [blame] | 202 | void print(llvm::raw_ostream &os) const { |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 203 | bool isFirst = true; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 204 | os << "{ "; |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 205 | for (iterator i = begin(), e = end(); i != e; ++i) { |
| 206 | if (isFirst) |
| 207 | isFirst = false; |
| 208 | else |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 209 | os << ", "; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 210 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 211 | os << '[' << i->From().toString(10) << ", " << i->To().toString(10) |
| 212 | << ']'; |
| 213 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 214 | os << " }"; |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 215 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 216 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 217 | bool operator==(const RangeSet &other) const { |
| 218 | return ranges == other.ranges; |
| 219 | } |
| 220 | }; |
Ted Kremenek | b103f01 | 2009-02-18 05:22:01 +0000 | [diff] [blame] | 221 | } // end anonymous namespace |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 222 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 223 | typedef llvm::ImmutableMap<SymbolRef,RangeSet> ConstraintRangeTy; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 224 | |
| 225 | namespace clang { |
| 226 | template<> |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 227 | struct GRStateTrait<ConstraintRange> |
| 228 | : public GRStatePartialTrait<ConstraintRangeTy> { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 229 | static inline void* GDMIndex() { return &ConstraintRangeIndex; } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 230 | }; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 231 | } |
| 232 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 233 | namespace { |
Kovarththanan Rajaratnam | ba5fb5a | 2009-11-28 06:07:30 +0000 | [diff] [blame] | 234 | class RangeConstraintManager : public SimpleConstraintManager{ |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 235 | RangeSet GetRange(const GRState *state, SymbolRef sym); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 236 | public: |
Ted Kremenek | f1b8227 | 2009-06-18 23:20:05 +0000 | [diff] [blame] | 237 | RangeConstraintManager() {} |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 238 | |
| 239 | const GRState* AssumeSymNE(const GRState* St, SymbolRef sym, |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 240 | const llvm::APSInt& V); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 241 | |
| 242 | const GRState* AssumeSymEQ(const GRState* St, SymbolRef sym, |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 243 | const llvm::APSInt& V); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 244 | |
| 245 | const GRState* AssumeSymLT(const GRState* St, SymbolRef sym, |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 246 | const llvm::APSInt& V); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 247 | |
| 248 | const GRState* AssumeSymGT(const GRState* St, SymbolRef sym, |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 249 | const llvm::APSInt& V); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 250 | |
| 251 | const GRState* AssumeSymGE(const GRState* St, SymbolRef sym, |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 252 | const llvm::APSInt& V); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 253 | |
| 254 | const GRState* AssumeSymLE(const GRState* St, SymbolRef sym, |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 255 | const llvm::APSInt& V); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 256 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 257 | const llvm::APSInt* getSymVal(const GRState* St, SymbolRef sym) const; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 258 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 259 | // FIXME: Refactor into SimpleConstraintManager? |
| 260 | bool isEqual(const GRState* St, SymbolRef sym, const llvm::APSInt& V) const { |
| 261 | const llvm::APSInt *i = getSymVal(St, sym); |
| 262 | return i ? *i == V : false; |
| 263 | } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 264 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 265 | const GRState* RemoveDeadBindings(const GRState* St, SymbolReaper& SymReaper); |
| 266 | |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 267 | void print(const GRState* St, llvm::raw_ostream& Out, |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 268 | const char* nl, const char *sep); |
| 269 | |
| 270 | private: |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 271 | RangeSet::Factory F; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 272 | }; |
| 273 | |
| 274 | } // end anonymous namespace |
| 275 | |
Ted Kremenek | f1b8227 | 2009-06-18 23:20:05 +0000 | [diff] [blame] | 276 | ConstraintManager* clang::CreateRangeConstraintManager(GRStateManager&) { |
| 277 | return new RangeConstraintManager(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 278 | } |
| 279 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 280 | const llvm::APSInt* RangeConstraintManager::getSymVal(const GRState* St, |
| 281 | SymbolRef sym) const { |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 282 | const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym); |
| 283 | return T ? T->getConcreteValue() : NULL; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 284 | } |
| 285 | |
| 286 | /// Scan all symbols referenced by the constraints. If the symbol is not alive |
| 287 | /// as marked in LSymbols, mark it as dead in DSymbols. |
| 288 | const GRState* |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 289 | RangeConstraintManager::RemoveDeadBindings(const GRState* state, |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 290 | SymbolReaper& SymReaper) { |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 291 | |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 292 | ConstraintRangeTy CR = state->get<ConstraintRange>(); |
| 293 | ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 294 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 295 | for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 296 | SymbolRef sym = I.getKey(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 297 | if (SymReaper.maybeDead(sym)) |
| 298 | CR = CRFactory.Remove(CR, sym); |
| 299 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 300 | |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 301 | return state->set<ConstraintRange>(CR); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 302 | } |
| 303 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 304 | //===------------------------------------------------------------------------=== |
| 305 | // AssumeSymX methods: public interface for RangeConstraintManager. |
| 306 | //===------------------------------------------------------------------------===/ |
| 307 | |
| 308 | RangeSet |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 309 | RangeConstraintManager::GetRange(const GRState *state, SymbolRef sym) { |
| 310 | if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym)) |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 311 | return *V; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 312 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 313 | // Lazily generate a new RangeSet representing all possible values for the |
| 314 | // given symbol type. |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 315 | QualType T = state->getSymbolManager().getType(sym); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 316 | BasicValueFactory& BV = state->getBasicVals(); |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 317 | return RangeSet(F, BV.getMinValue(T), BV.getMaxValue(T)); |
| 318 | } |
| 319 | |
| 320 | //===------------------------------------------------------------------------=== |
| 321 | // AssumeSymX methods: public interface for RangeConstraintManager. |
| 322 | //===------------------------------------------------------------------------===/ |
| 323 | |
| 324 | #define AssumeX(OP)\ |
| 325 | const GRState*\ |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 326 | RangeConstraintManager::AssumeSym ## OP(const GRState* state, SymbolRef sym,\ |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 327 | const llvm::APSInt& V){\ |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 328 | const RangeSet& R = GetRange(state, sym).Add##OP(state->getBasicVals(), F, V);\ |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 329 | return !R.isEmpty() ? state->set<ConstraintRange>(sym, R) : NULL;\ |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 330 | } |
| 331 | |
| 332 | AssumeX(EQ) |
| 333 | AssumeX(NE) |
| 334 | AssumeX(LT) |
| 335 | AssumeX(GT) |
| 336 | AssumeX(LE) |
| 337 | AssumeX(GE) |
| 338 | |
| 339 | //===------------------------------------------------------------------------=== |
| 340 | // Pretty-printing. |
| 341 | //===------------------------------------------------------------------------===/ |
| 342 | |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 343 | void RangeConstraintManager::print(const GRState* St, llvm::raw_ostream& Out, |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 344 | const char* nl, const char *sep) { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 345 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 346 | ConstraintRangeTy Ranges = St->get<ConstraintRange>(); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 347 | |
Ted Kremenek | dd28d00 | 2009-02-16 18:42:56 +0000 | [diff] [blame] | 348 | if (Ranges.isEmpty()) |
| 349 | return; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 350 | |
Ted Kremenek | dd28d00 | 2009-02-16 18:42:56 +0000 | [diff] [blame] | 351 | Out << nl << sep << "ranges of symbol values:"; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 352 | |
Ted Kremenek | 9beefec | 2009-02-17 19:28:04 +0000 | [diff] [blame] | 353 | for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){ |
Ted Kremenek | ec751c4 | 2009-04-21 22:37:11 +0000 | [diff] [blame] | 354 | Out << nl << ' ' << I.getKey() << " : "; |
Ted Kremenek | 53ba0b6 | 2009-06-24 23:06:47 +0000 | [diff] [blame] | 355 | I.getData().print(Out); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 356 | } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 357 | } |