blob: 8f8528dbde6430501b1ae08829c55fffd26b7ff7 [file] [log] [blame]
Ted Kremenek45021952009-02-14 17:08:39 +00001//== 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 Stump1eb44332009-09-09 15:08:12 +000010// This file defines RangeConstraintManager, a class that tracks simple
Ted Kremenek45021952009-02-14 17:08:39 +000011// equality and inequality constraints on symbolic values of GRState.
12//
13//===----------------------------------------------------------------------===//
14
15#include "SimpleConstraintManager.h"
Argyrios Kyrtzidis98cabba2010-12-22 18:51:49 +000016#include "clang/GR/PathSensitive/GRState.h"
17#include "clang/GR/PathSensitive/GRStateTrait.h"
Argyrios Kyrtzidisd2592a32010-12-22 18:53:44 +000018#include "clang/GR/PathSensitive/TransferFuncs.h"
Argyrios Kyrtzidis98cabba2010-12-22 18:51:49 +000019#include "clang/GR/ManagerRegistry.h"
Ted Kremenek45021952009-02-14 17:08:39 +000020#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
25using namespace clang;
Argyrios Kyrtzidis5a4f98f2010-12-22 18:53:20 +000026using namespace GR;
Ted Kremenek45021952009-02-14 17:08:39 +000027
Kovarththanan Rajaratnamba5fb5a2009-11-28 06:07:30 +000028namespace { class ConstraintRange {}; }
Ted Kremenek9beefec2009-02-17 19:28:04 +000029static int ConstraintRangeIndex = 0;
Ted Kremenek45021952009-02-14 17:08:39 +000030
Ted Kremenek9beefec2009-02-17 19:28:04 +000031/// 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 Kremenekb103f012009-02-18 05:22:01 +000034namespace {
Kovarththanan Rajaratnamba5fb5a2009-11-28 06:07:30 +000035class Range : public std::pair<const llvm::APSInt*,
Ted Kremenekb103f012009-02-18 05:22:01 +000036 const llvm::APSInt*> {
Ted Kremenek45021952009-02-14 17:08:39 +000037public:
38 Range(const llvm::APSInt &from, const llvm::APSInt &to)
Ted Kremenek9beefec2009-02-17 19:28:04 +000039 : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) {
Ted Kremenek45021952009-02-14 17:08:39 +000040 assert(from <= to);
41 }
42 bool Includes(const llvm::APSInt &v) const {
Ted Kremenek9beefec2009-02-17 19:28:04 +000043 return *first <= v && v <= *second;
Ted Kremenek45021952009-02-14 17:08:39 +000044 }
45 const llvm::APSInt &From() const {
Ted Kremenek9beefec2009-02-17 19:28:04 +000046 return *first;
Ted Kremenek45021952009-02-14 17:08:39 +000047 }
48 const llvm::APSInt &To() const {
Ted Kremenek9beefec2009-02-17 19:28:04 +000049 return *second;
Ted Kremenek45021952009-02-14 17:08:39 +000050 }
Ted Kremenek9beefec2009-02-17 19:28:04 +000051 const llvm::APSInt *getConcreteValue() const {
52 return &From() == &To() ? &From() : NULL;
Ted Kremenek45021952009-02-14 17:08:39 +000053 }
54
55 void Profile(llvm::FoldingSetNodeID &ID) const {
Ted Kremenek9beefec2009-02-17 19:28:04 +000056 ID.AddPointer(&From());
57 ID.AddPointer(&To());
Ted Kremenek45021952009-02-14 17:08:39 +000058 }
59};
60
Ted Kremenekb103f012009-02-18 05:22:01 +000061
Kovarththanan Rajaratnamba5fb5a2009-11-28 06:07:30 +000062class RangeTrait : public llvm::ImutContainerInfo<Range> {
Ted Kremenekb103f012009-02-18 05:22:01 +000063public:
64 // When comparing if one Range is less than another, we should compare
Ted Kremeneke53f8202009-02-18 17:42:44 +000065 // 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 Kremenekb103f012009-02-18 05:22:01 +000068 static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
Mike Stump1eb44332009-09-09 15:08:12 +000069 return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) &&
Ted Kremenekb103f012009-02-18 05:22:01 +000070 *lhs.second < *rhs.second);
71 }
72};
73
Ted Kremenek9beefec2009-02-17 19:28:04 +000074/// 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 Rajaratnamba5fb5a2009-11-28 06:07:30 +000077class RangeSet {
Ted Kremenekb103f012009-02-18 05:22:01 +000078 typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
Ted Kremenek45021952009-02-14 17:08:39 +000079 PrimRangeSet ranges; // no need to make const, since it is an
80 // ImmutableSet - this allows default operator=
Mike Stump1eb44332009-09-09 15:08:12 +000081 // to work.
Ted Kremenek45021952009-02-14 17:08:39 +000082public:
Ted Kremenek9beefec2009-02-17 19:28:04 +000083 typedef PrimRangeSet::Factory Factory;
84 typedef PrimRangeSet::iterator iterator;
85
86 RangeSet(PrimRangeSet RS) : ranges(RS) {}
Ted Kremenek9beefec2009-02-17 19:28:04 +000087
88 iterator begin() const { return ranges.begin(); }
89 iterator end() const { return ranges.end(); }
Mike Stump1eb44332009-09-09 15:08:12 +000090
Ted Kremenek9beefec2009-02-17 19:28:04 +000091 bool isEmpty() const { return ranges.isEmpty(); }
Mike Stump1eb44332009-09-09 15:08:12 +000092
Ted Kremenek9beefec2009-02-17 19:28:04 +000093 /// Construct a new RangeSet representing '{ [from, to] }'.
94 RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
Ted Kremenek3baf6722010-11-24 00:54:37 +000095 : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
Mike Stump1eb44332009-09-09 15:08:12 +000096
Ted Kremenek9beefec2009-02-17 19:28:04 +000097 /// 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 Kremenek45021952009-02-14 17:08:39 +0000106 }
107
Jordy Roseba0f61c2010-06-18 22:49:11 +0000108private:
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 Kremenek9beefec2009-02-17 19:28:04 +0000128 break;
Ted Kremenek45021952009-02-14 17:08:39 +0000129 }
Mike Stump1eb44332009-09-09 15:08:12 +0000130
Jordy Roseba0f61c2010-06-18 22:49:11 +0000131 if (i->Includes(Lower)) {
132 if (i->Includes(Upper)) {
Ted Kremenek3baf6722010-11-24 00:54:37 +0000133 newRanges = F.add(newRanges, Range(BV.getValue(Lower),
Jordy Roseba0f61c2010-06-18 22:49:11 +0000134 BV.getValue(Upper)));
135 break;
136 } else
Ted Kremenek3baf6722010-11-24 00:54:37 +0000137 newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
Jordy Roseba0f61c2010-06-18 22:49:11 +0000138 } else {
139 if (i->Includes(Upper)) {
Ted Kremenek3baf6722010-11-24 00:54:37 +0000140 newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper)));
Jordy Roseba0f61c2010-06-18 22:49:11 +0000141 break;
142 } else
Ted Kremenek3baf6722010-11-24 00:54:37 +0000143 newRanges = F.add(newRanges, *i);
Jordy Roseba0f61c2010-06-18 22:49:11 +0000144 }
145 }
Ted Kremenek45021952009-02-14 17:08:39 +0000146 }
147
Jordy Roseba0f61c2010-06-18 22:49:11 +0000148public:
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 Kremenek3baf6722010-11-24 00:54:37 +0000159 PrimRangeSet newRanges = F.getEmptySet();
Ted Kremenek9beefec2009-02-17 19:28:04 +0000160
Jordy Roseba0f61c2010-06-18 22:49:11 +0000161 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 Kremenek9beefec2009-02-17 19:28:04 +0000170 }
Ted Kremenek9beefec2009-02-17 19:28:04 +0000171 return newRanges;
Ted Kremenek45021952009-02-14 17:08:39 +0000172 }
173
Ted Kremenek53ba0b62009-06-24 23:06:47 +0000174 void print(llvm::raw_ostream &os) const {
Ted Kremenek9beefec2009-02-17 19:28:04 +0000175 bool isFirst = true;
Ted Kremenek45021952009-02-14 17:08:39 +0000176 os << "{ ";
Ted Kremenek9beefec2009-02-17 19:28:04 +0000177 for (iterator i = begin(), e = end(); i != e; ++i) {
178 if (isFirst)
179 isFirst = false;
180 else
Ted Kremenek45021952009-02-14 17:08:39 +0000181 os << ", ";
Mike Stump1eb44332009-09-09 15:08:12 +0000182
Ted Kremenek45021952009-02-14 17:08:39 +0000183 os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
184 << ']';
185 }
Mike Stump1eb44332009-09-09 15:08:12 +0000186 os << " }";
Ted Kremenek9beefec2009-02-17 19:28:04 +0000187 }
Mike Stump1eb44332009-09-09 15:08:12 +0000188
Ted Kremenek45021952009-02-14 17:08:39 +0000189 bool operator==(const RangeSet &other) const {
190 return ranges == other.ranges;
191 }
192};
Ted Kremenekb103f012009-02-18 05:22:01 +0000193} // end anonymous namespace
Ted Kremenek45021952009-02-14 17:08:39 +0000194
Ted Kremenek9beefec2009-02-17 19:28:04 +0000195typedef llvm::ImmutableMap<SymbolRef,RangeSet> ConstraintRangeTy;
Ted Kremenek45021952009-02-14 17:08:39 +0000196
197namespace clang {
Argyrios Kyrtzidis5a4f98f2010-12-22 18:53:20 +0000198namespace GR {
Ted Kremenek45021952009-02-14 17:08:39 +0000199template<>
Ted Kremenek9beefec2009-02-17 19:28:04 +0000200struct GRStateTrait<ConstraintRange>
201 : public GRStatePartialTrait<ConstraintRangeTy> {
Mike Stump1eb44332009-09-09 15:08:12 +0000202 static inline void* GDMIndex() { return &ConstraintRangeIndex; }
Ted Kremenek45021952009-02-14 17:08:39 +0000203};
Mike Stump1eb44332009-09-09 15:08:12 +0000204}
Argyrios Kyrtzidis5a4f98f2010-12-22 18:53:20 +0000205}
Mike Stump1eb44332009-09-09 15:08:12 +0000206
Ted Kremenek45021952009-02-14 17:08:39 +0000207namespace {
Kovarththanan Rajaratnamba5fb5a2009-11-28 06:07:30 +0000208class RangeConstraintManager : public SimpleConstraintManager{
Mike Stump1eb44332009-09-09 15:08:12 +0000209 RangeSet GetRange(const GRState *state, SymbolRef sym);
Ted Kremenek45021952009-02-14 17:08:39 +0000210public:
Argyrios Kyrtzidisd2592a32010-12-22 18:53:44 +0000211 RangeConstraintManager(SubEngine &subengine)
Ted Kremenek32a58082010-01-05 00:15:18 +0000212 : SimpleConstraintManager(subengine) {}
Ted Kremenek45021952009-02-14 17:08:39 +0000213
Ted Kremenek28f47b92010-12-01 22:16:56 +0000214 const GRState *assumeSymNE(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000215 const llvm::APSInt& Int,
216 const llvm::APSInt& Adjustment);
Ted Kremenek45021952009-02-14 17:08:39 +0000217
Ted Kremenek28f47b92010-12-01 22:16:56 +0000218 const GRState *assumeSymEQ(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000219 const llvm::APSInt& Int,
220 const llvm::APSInt& Adjustment);
Ted Kremenek45021952009-02-14 17:08:39 +0000221
Ted Kremenek28f47b92010-12-01 22:16:56 +0000222 const GRState *assumeSymLT(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000223 const llvm::APSInt& Int,
224 const llvm::APSInt& Adjustment);
Ted Kremenek45021952009-02-14 17:08:39 +0000225
Ted Kremenek28f47b92010-12-01 22:16:56 +0000226 const GRState *assumeSymGT(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000227 const llvm::APSInt& Int,
228 const llvm::APSInt& Adjustment);
Ted Kremenek45021952009-02-14 17:08:39 +0000229
Ted Kremenek28f47b92010-12-01 22:16:56 +0000230 const GRState *assumeSymGE(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000231 const llvm::APSInt& Int,
232 const llvm::APSInt& Adjustment);
Ted Kremenek45021952009-02-14 17:08:39 +0000233
Ted Kremenek28f47b92010-12-01 22:16:56 +0000234 const GRState *assumeSymLE(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000235 const llvm::APSInt& Int,
236 const llvm::APSInt& Adjustment);
Ted Kremenek45021952009-02-14 17:08:39 +0000237
Ted Kremenek45021952009-02-14 17:08:39 +0000238 const llvm::APSInt* getSymVal(const GRState* St, SymbolRef sym) const;
Mike Stump1eb44332009-09-09 15:08:12 +0000239
Ted Kremenek9beefec2009-02-17 19:28:04 +0000240 // 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 Kremenek45021952009-02-14 17:08:39 +0000245
Ted Kremenek45021952009-02-14 17:08:39 +0000246 const GRState* RemoveDeadBindings(const GRState* St, SymbolReaper& SymReaper);
247
Mike Stump1eb44332009-09-09 15:08:12 +0000248 void print(const GRState* St, llvm::raw_ostream& Out,
Ted Kremenek45021952009-02-14 17:08:39 +0000249 const char* nl, const char *sep);
250
251private:
Ted Kremenek9beefec2009-02-17 19:28:04 +0000252 RangeSet::Factory F;
Ted Kremenek45021952009-02-14 17:08:39 +0000253};
254
255} // end anonymous namespace
256
Argyrios Kyrtzidis5a4f98f2010-12-22 18:53:20 +0000257ConstraintManager* GR::CreateRangeConstraintManager(GRStateManager&,
Argyrios Kyrtzidisd2592a32010-12-22 18:53:44 +0000258 SubEngine &subeng) {
Ted Kremenek32a58082010-01-05 00:15:18 +0000259 return new RangeConstraintManager(subeng);
Ted Kremenek45021952009-02-14 17:08:39 +0000260}
261
Ted Kremenek45021952009-02-14 17:08:39 +0000262const llvm::APSInt* RangeConstraintManager::getSymVal(const GRState* St,
263 SymbolRef sym) const {
Ted Kremenek9beefec2009-02-17 19:28:04 +0000264 const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym);
265 return T ? T->getConcreteValue() : NULL;
Ted Kremenek45021952009-02-14 17:08:39 +0000266}
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.
270const GRState*
Ted Kremenekc8781382009-06-17 22:28:13 +0000271RangeConstraintManager::RemoveDeadBindings(const GRState* state,
Ted Kremenek45021952009-02-14 17:08:39 +0000272 SymbolReaper& SymReaper) {
Ted Kremenek45021952009-02-14 17:08:39 +0000273
Ted Kremenekc8781382009-06-17 22:28:13 +0000274 ConstraintRangeTy CR = state->get<ConstraintRange>();
275 ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>();
Ted Kremenek45021952009-02-14 17:08:39 +0000276
Ted Kremenek9beefec2009-02-17 19:28:04 +0000277 for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
Mike Stump1eb44332009-09-09 15:08:12 +0000278 SymbolRef sym = I.getKey();
Ted Kremenek45021952009-02-14 17:08:39 +0000279 if (SymReaper.maybeDead(sym))
Ted Kremenek3baf6722010-11-24 00:54:37 +0000280 CR = CRFactory.remove(CR, sym);
Ted Kremenek45021952009-02-14 17:08:39 +0000281 }
Mike Stump1eb44332009-09-09 15:08:12 +0000282
Ted Kremenekc8781382009-06-17 22:28:13 +0000283 return state->set<ConstraintRange>(CR);
Ted Kremenek45021952009-02-14 17:08:39 +0000284}
285
Ted Kremenek9beefec2009-02-17 19:28:04 +0000286RangeSet
Ted Kremenekc8781382009-06-17 22:28:13 +0000287RangeConstraintManager::GetRange(const GRState *state, SymbolRef sym) {
288 if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
Ted Kremenek9beefec2009-02-17 19:28:04 +0000289 return *V;
Mike Stump1eb44332009-09-09 15:08:12 +0000290
Ted Kremenek9beefec2009-02-17 19:28:04 +0000291 // Lazily generate a new RangeSet representing all possible values for the
292 // given symbol type.
Ted Kremenekc8781382009-06-17 22:28:13 +0000293 QualType T = state->getSymbolManager().getType(sym);
Mike Stump1eb44332009-09-09 15:08:12 +0000294 BasicValueFactory& BV = state->getBasicVals();
Ted Kremenek9beefec2009-02-17 19:28:04 +0000295 return RangeSet(F, BV.getMinValue(T), BV.getMaxValue(T));
296}
297
298//===------------------------------------------------------------------------===
Ted Kremenek28f47b92010-12-01 22:16:56 +0000299// assumeSymX methods: public interface for RangeConstraintManager.
Ted Kremenek9beefec2009-02-17 19:28:04 +0000300//===------------------------------------------------------------------------===/
301
Jordy Roseba0f61c2010-06-18 22:49:11 +0000302// 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
310const GRState*
Ted Kremenek28f47b92010-12-01 22:16:56 +0000311RangeConstraintManager::assumeSymNE(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000312 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 Kremenek9beefec2009-02-17 19:28:04 +0000325}
326
Jordy Roseba0f61c2010-06-18 22:49:11 +0000327const GRState*
Ted Kremenek28f47b92010-12-01 22:16:56 +0000328RangeConstraintManager::assumeSymEQ(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000329 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
338const GRState*
Ted Kremenek28f47b92010-12-01 22:16:56 +0000339RangeConstraintManager::assumeSymLT(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000340 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
359const GRState*
Ted Kremenek28f47b92010-12-01 22:16:56 +0000360RangeConstraintManager::assumeSymGT(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000361 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
380const GRState*
Ted Kremenek28f47b92010-12-01 22:16:56 +0000381RangeConstraintManager::assumeSymGE(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000382 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
402const GRState*
Ted Kremenek28f47b92010-12-01 22:16:56 +0000403RangeConstraintManager::assumeSymLE(const GRState* state, SymbolRef sym,
Jordy Roseba0f61c2010-06-18 22:49:11 +0000404 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 Kremenek9beefec2009-02-17 19:28:04 +0000423
424//===------------------------------------------------------------------------===
425// Pretty-printing.
426//===------------------------------------------------------------------------===/
427
Mike Stump1eb44332009-09-09 15:08:12 +0000428void RangeConstraintManager::print(const GRState* St, llvm::raw_ostream& Out,
Ted Kremenek45021952009-02-14 17:08:39 +0000429 const char* nl, const char *sep) {
Mike Stump1eb44332009-09-09 15:08:12 +0000430
Ted Kremenek9beefec2009-02-17 19:28:04 +0000431 ConstraintRangeTy Ranges = St->get<ConstraintRange>();
Mike Stump1eb44332009-09-09 15:08:12 +0000432
Ted Kremenekdd28d002009-02-16 18:42:56 +0000433 if (Ranges.isEmpty())
434 return;
Mike Stump1eb44332009-09-09 15:08:12 +0000435
Ted Kremenekdd28d002009-02-16 18:42:56 +0000436 Out << nl << sep << "ranges of symbol values:";
Mike Stump1eb44332009-09-09 15:08:12 +0000437
Ted Kremenek9beefec2009-02-17 19:28:04 +0000438 for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){
Ted Kremenekec751c42009-04-21 22:37:11 +0000439 Out << nl << ' ' << I.getKey() << " : ";
Ted Kremenek53ba0b62009-06-24 23:06:47 +0000440 I.getData().print(Out);
Ted Kremenek45021952009-02-14 17:08:39 +0000441 }
Ted Kremenek45021952009-02-14 17:08:39 +0000442}