1218887Sdim//== RangeConstraintManager.cpp - Manage range constraints.------*- C++ -*--==// 2218887Sdim// 3218887Sdim// The LLVM Compiler Infrastructure 4218887Sdim// 5218887Sdim// This file is distributed under the University of Illinois Open Source 6218887Sdim// License. See LICENSE.TXT for details. 7218887Sdim// 8218887Sdim//===----------------------------------------------------------------------===// 9218887Sdim// 10218887Sdim// This file defines RangeConstraintManager, a class that tracks simple 11226633Sdim// equality and inequality constraints on symbolic values of ProgramState. 12218887Sdim// 13218887Sdim//===----------------------------------------------------------------------===// 14218887Sdim 15218887Sdim#include "SimpleConstraintManager.h" 16239462Sdim#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" 17226633Sdim#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 18226633Sdim#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" 19218887Sdim#include "llvm/ADT/FoldingSet.h" 20218887Sdim#include "llvm/ADT/ImmutableSet.h" 21249423Sdim#include "llvm/Support/Debug.h" 22218887Sdim#include "llvm/Support/raw_ostream.h" 23218887Sdim 24218887Sdimusing namespace clang; 25218887Sdimusing namespace ento; 26218887Sdim 27218887Sdim/// A Range represents the closed range [from, to]. The caller must 28218887Sdim/// guarantee that from <= to. Note that Range is immutable, so as not 29218887Sdim/// to subvert RangeSet's immutability. 30218887Sdimnamespace { 31218887Sdimclass Range : public std::pair<const llvm::APSInt*, 32218887Sdim const llvm::APSInt*> { 33218887Sdimpublic: 34218887Sdim Range(const llvm::APSInt &from, const llvm::APSInt &to) 35218887Sdim : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) { 36218887Sdim assert(from <= to); 37218887Sdim } 38218887Sdim bool Includes(const llvm::APSInt &v) const { 39218887Sdim return *first <= v && v <= *second; 40218887Sdim } 41218887Sdim const llvm::APSInt &From() const { 42218887Sdim return *first; 43218887Sdim } 44218887Sdim const llvm::APSInt &To() const { 45218887Sdim return *second; 46218887Sdim } 47218887Sdim const llvm::APSInt *getConcreteValue() const { 48218887Sdim return &From() == &To() ? &From() : NULL; 49218887Sdim } 50218887Sdim 51218887Sdim void Profile(llvm::FoldingSetNodeID &ID) const { 52218887Sdim ID.AddPointer(&From()); 53218887Sdim ID.AddPointer(&To()); 54218887Sdim } 55218887Sdim}; 56218887Sdim 57218887Sdim 58218887Sdimclass RangeTrait : public llvm::ImutContainerInfo<Range> { 59218887Sdimpublic: 60218887Sdim // When comparing if one Range is less than another, we should compare 61218887Sdim // the actual APSInt values instead of their pointers. This keeps the order 62218887Sdim // consistent (instead of comparing by pointer values) and can potentially 63218887Sdim // be used to speed up some of the operations in RangeSet. 64218887Sdim static inline bool isLess(key_type_ref lhs, key_type_ref rhs) { 65218887Sdim return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) && 66218887Sdim *lhs.second < *rhs.second); 67218887Sdim } 68218887Sdim}; 69218887Sdim 70218887Sdim/// RangeSet contains a set of ranges. If the set is empty, then 71218887Sdim/// there the value of a symbol is overly constrained and there are no 72218887Sdim/// possible values for that symbol. 73218887Sdimclass RangeSet { 74218887Sdim typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet; 75218887Sdim PrimRangeSet ranges; // no need to make const, since it is an 76218887Sdim // ImmutableSet - this allows default operator= 77218887Sdim // to work. 78218887Sdimpublic: 79218887Sdim typedef PrimRangeSet::Factory Factory; 80218887Sdim typedef PrimRangeSet::iterator iterator; 81218887Sdim 82218887Sdim RangeSet(PrimRangeSet RS) : ranges(RS) {} 83218887Sdim 84218887Sdim iterator begin() const { return ranges.begin(); } 85218887Sdim iterator end() const { return ranges.end(); } 86218887Sdim 87218887Sdim bool isEmpty() const { return ranges.isEmpty(); } 88218887Sdim 89218887Sdim /// Construct a new RangeSet representing '{ [from, to] }'. 90218887Sdim RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to) 91218887Sdim : ranges(F.add(F.getEmptySet(), Range(from, to))) {} 92218887Sdim 93218887Sdim /// Profile - Generates a hash profile of this RangeSet for use 94218887Sdim /// by FoldingSet. 95218887Sdim void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); } 96218887Sdim 97218887Sdim /// getConcreteValue - If a symbol is contrained to equal a specific integer 98218887Sdim /// constant then this method returns that value. Otherwise, it returns 99218887Sdim /// NULL. 100218887Sdim const llvm::APSInt* getConcreteValue() const { 101218887Sdim return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0; 102218887Sdim } 103218887Sdim 104218887Sdimprivate: 105218887Sdim void IntersectInRange(BasicValueFactory &BV, Factory &F, 106218887Sdim const llvm::APSInt &Lower, 107218887Sdim const llvm::APSInt &Upper, 108218887Sdim PrimRangeSet &newRanges, 109218887Sdim PrimRangeSet::iterator &i, 110218887Sdim PrimRangeSet::iterator &e) const { 111218887Sdim // There are six cases for each range R in the set: 112218887Sdim // 1. R is entirely before the intersection range. 113218887Sdim // 2. R is entirely after the intersection range. 114218887Sdim // 3. R contains the entire intersection range. 115218887Sdim // 4. R starts before the intersection range and ends in the middle. 116218887Sdim // 5. R starts in the middle of the intersection range and ends after it. 117218887Sdim // 6. R is entirely contained in the intersection range. 118218887Sdim // These correspond to each of the conditions below. 119218887Sdim for (/* i = begin(), e = end() */; i != e; ++i) { 120218887Sdim if (i->To() < Lower) { 121218887Sdim continue; 122218887Sdim } 123218887Sdim if (i->From() > Upper) { 124218887Sdim break; 125218887Sdim } 126218887Sdim 127218887Sdim if (i->Includes(Lower)) { 128218887Sdim if (i->Includes(Upper)) { 129218887Sdim newRanges = F.add(newRanges, Range(BV.getValue(Lower), 130218887Sdim BV.getValue(Upper))); 131218887Sdim break; 132218887Sdim } else 133218887Sdim newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To())); 134218887Sdim } else { 135218887Sdim if (i->Includes(Upper)) { 136218887Sdim newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper))); 137218887Sdim break; 138218887Sdim } else 139218887Sdim newRanges = F.add(newRanges, *i); 140218887Sdim } 141218887Sdim } 142218887Sdim } 143218887Sdim 144239462Sdim const llvm::APSInt &getMinValue() const { 145239462Sdim assert(!isEmpty()); 146239462Sdim return ranges.begin()->From(); 147239462Sdim } 148239462Sdim 149239462Sdim bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const { 150239462Sdim // This function has nine cases, the cartesian product of range-testing 151239462Sdim // both the upper and lower bounds against the symbol's type. 152239462Sdim // Each case requires a different pinning operation. 153239462Sdim // The function returns false if the described range is entirely outside 154239462Sdim // the range of values for the associated symbol. 155239462Sdim APSIntType Type(getMinValue()); 156249423Sdim APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower, true); 157249423Sdim APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper, true); 158239462Sdim 159239462Sdim switch (LowerTest) { 160239462Sdim case APSIntType::RTR_Below: 161239462Sdim switch (UpperTest) { 162239462Sdim case APSIntType::RTR_Below: 163239462Sdim // The entire range is outside the symbol's set of possible values. 164239462Sdim // If this is a conventionally-ordered range, the state is infeasible. 165239462Sdim if (Lower < Upper) 166239462Sdim return false; 167239462Sdim 168239462Sdim // However, if the range wraps around, it spans all possible values. 169239462Sdim Lower = Type.getMinValue(); 170239462Sdim Upper = Type.getMaxValue(); 171239462Sdim break; 172239462Sdim case APSIntType::RTR_Within: 173239462Sdim // The range starts below what's possible but ends within it. Pin. 174239462Sdim Lower = Type.getMinValue(); 175239462Sdim Type.apply(Upper); 176239462Sdim break; 177239462Sdim case APSIntType::RTR_Above: 178239462Sdim // The range spans all possible values for the symbol. Pin. 179239462Sdim Lower = Type.getMinValue(); 180239462Sdim Upper = Type.getMaxValue(); 181239462Sdim break; 182239462Sdim } 183239462Sdim break; 184239462Sdim case APSIntType::RTR_Within: 185239462Sdim switch (UpperTest) { 186239462Sdim case APSIntType::RTR_Below: 187239462Sdim // The range wraps around, but all lower values are not possible. 188239462Sdim Type.apply(Lower); 189239462Sdim Upper = Type.getMaxValue(); 190239462Sdim break; 191239462Sdim case APSIntType::RTR_Within: 192239462Sdim // The range may or may not wrap around, but both limits are valid. 193239462Sdim Type.apply(Lower); 194239462Sdim Type.apply(Upper); 195239462Sdim break; 196239462Sdim case APSIntType::RTR_Above: 197239462Sdim // The range starts within what's possible but ends above it. Pin. 198239462Sdim Type.apply(Lower); 199239462Sdim Upper = Type.getMaxValue(); 200239462Sdim break; 201239462Sdim } 202239462Sdim break; 203239462Sdim case APSIntType::RTR_Above: 204239462Sdim switch (UpperTest) { 205239462Sdim case APSIntType::RTR_Below: 206239462Sdim // The range wraps but is outside the symbol's set of possible values. 207239462Sdim return false; 208239462Sdim case APSIntType::RTR_Within: 209239462Sdim // The range starts above what's possible but ends within it (wrap). 210239462Sdim Lower = Type.getMinValue(); 211239462Sdim Type.apply(Upper); 212239462Sdim break; 213239462Sdim case APSIntType::RTR_Above: 214239462Sdim // The entire range is outside the symbol's set of possible values. 215239462Sdim // If this is a conventionally-ordered range, the state is infeasible. 216239462Sdim if (Lower < Upper) 217239462Sdim return false; 218239462Sdim 219239462Sdim // However, if the range wraps around, it spans all possible values. 220239462Sdim Lower = Type.getMinValue(); 221239462Sdim Upper = Type.getMaxValue(); 222239462Sdim break; 223239462Sdim } 224239462Sdim break; 225239462Sdim } 226239462Sdim 227239462Sdim return true; 228239462Sdim } 229239462Sdim 230218887Sdimpublic: 231218887Sdim // Returns a set containing the values in the receiving set, intersected with 232218887Sdim // the closed range [Lower, Upper]. Unlike the Range type, this range uses 233218887Sdim // modular arithmetic, corresponding to the common treatment of C integer 234218887Sdim // overflow. Thus, if the Lower bound is greater than the Upper bound, the 235218887Sdim // range is taken to wrap around. This is equivalent to taking the 236218887Sdim // intersection with the two ranges [Min, Upper] and [Lower, Max], 237218887Sdim // or, alternatively, /removing/ all integers between Upper and Lower. 238218887Sdim RangeSet Intersect(BasicValueFactory &BV, Factory &F, 239239462Sdim llvm::APSInt Lower, llvm::APSInt Upper) const { 240239462Sdim if (!pin(Lower, Upper)) 241239462Sdim return F.getEmptySet(); 242239462Sdim 243218887Sdim PrimRangeSet newRanges = F.getEmptySet(); 244218887Sdim 245218887Sdim PrimRangeSet::iterator i = begin(), e = end(); 246218887Sdim if (Lower <= Upper) 247218887Sdim IntersectInRange(BV, F, Lower, Upper, newRanges, i, e); 248218887Sdim else { 249218887Sdim // The order of the next two statements is important! 250218887Sdim // IntersectInRange() does not reset the iteration state for i and e. 251218887Sdim // Therefore, the lower range most be handled first. 252218887Sdim IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e); 253218887Sdim IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e); 254218887Sdim } 255239462Sdim 256218887Sdim return newRanges; 257218887Sdim } 258218887Sdim 259226633Sdim void print(raw_ostream &os) const { 260218887Sdim bool isFirst = true; 261218887Sdim os << "{ "; 262218887Sdim for (iterator i = begin(), e = end(); i != e; ++i) { 263218887Sdim if (isFirst) 264218887Sdim isFirst = false; 265218887Sdim else 266218887Sdim os << ", "; 267218887Sdim 268218887Sdim os << '[' << i->From().toString(10) << ", " << i->To().toString(10) 269218887Sdim << ']'; 270218887Sdim } 271218887Sdim os << " }"; 272218887Sdim } 273218887Sdim 274218887Sdim bool operator==(const RangeSet &other) const { 275218887Sdim return ranges == other.ranges; 276218887Sdim } 277218887Sdim}; 278218887Sdim} // end anonymous namespace 279218887Sdim 280243830SdimREGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintRange, 281243830Sdim CLANG_ENTO_PROGRAMSTATE_MAP(SymbolRef, 282243830Sdim RangeSet)) 283218887Sdim 284218887Sdimnamespace { 285218887Sdimclass RangeConstraintManager : public SimpleConstraintManager{ 286234353Sdim RangeSet GetRange(ProgramStateRef state, SymbolRef sym); 287218887Sdimpublic: 288249423Sdim RangeConstraintManager(SubEngine *subengine, SValBuilder &SVB) 289249423Sdim : SimpleConstraintManager(subengine, SVB) {} 290218887Sdim 291234353Sdim ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym, 292218887Sdim const llvm::APSInt& Int, 293218887Sdim const llvm::APSInt& Adjustment); 294218887Sdim 295234353Sdim ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym, 296218887Sdim const llvm::APSInt& Int, 297218887Sdim const llvm::APSInt& Adjustment); 298218887Sdim 299234353Sdim ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym, 300218887Sdim const llvm::APSInt& Int, 301218887Sdim const llvm::APSInt& Adjustment); 302218887Sdim 303234353Sdim ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym, 304218887Sdim const llvm::APSInt& Int, 305218887Sdim const llvm::APSInt& Adjustment); 306218887Sdim 307234353Sdim ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym, 308218887Sdim const llvm::APSInt& Int, 309218887Sdim const llvm::APSInt& Adjustment); 310218887Sdim 311234353Sdim ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym, 312218887Sdim const llvm::APSInt& Int, 313218887Sdim const llvm::APSInt& Adjustment); 314218887Sdim 315234353Sdim const llvm::APSInt* getSymVal(ProgramStateRef St, SymbolRef sym) const; 316243830Sdim ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); 317218887Sdim 318234353Sdim ProgramStateRef removeDeadBindings(ProgramStateRef St, SymbolReaper& SymReaper); 319218887Sdim 320234353Sdim void print(ProgramStateRef St, raw_ostream &Out, 321218887Sdim const char* nl, const char *sep); 322218887Sdim 323218887Sdimprivate: 324218887Sdim RangeSet::Factory F; 325218887Sdim}; 326218887Sdim 327218887Sdim} // end anonymous namespace 328218887Sdim 329239462SdimConstraintManager * 330243830Sdimento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) { 331249423Sdim return new RangeConstraintManager(Eng, StMgr.getSValBuilder()); 332218887Sdim} 333218887Sdim 334234353Sdimconst llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St, 335218887Sdim SymbolRef sym) const { 336218887Sdim const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym); 337218887Sdim return T ? T->getConcreteValue() : NULL; 338218887Sdim} 339218887Sdim 340243830SdimConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State, 341243830Sdim SymbolRef Sym) { 342243830Sdim const RangeSet *Ranges = State->get<ConstraintRange>(Sym); 343243830Sdim 344243830Sdim // If we don't have any information about this symbol, it's underconstrained. 345243830Sdim if (!Ranges) 346243830Sdim return ConditionTruthVal(); 347243830Sdim 348243830Sdim // If we have a concrete value, see if it's zero. 349243830Sdim if (const llvm::APSInt *Value = Ranges->getConcreteValue()) 350243830Sdim return *Value == 0; 351243830Sdim 352243830Sdim BasicValueFactory &BV = getBasicVals(); 353243830Sdim APSIntType IntType = BV.getAPSIntType(Sym->getType()); 354243830Sdim llvm::APSInt Zero = IntType.getZeroValue(); 355243830Sdim 356243830Sdim // Check if zero is in the set of possible values. 357243830Sdim if (Ranges->Intersect(BV, F, Zero, Zero).isEmpty()) 358243830Sdim return false; 359243830Sdim 360243830Sdim // Zero is a possible value, but it is not the /only/ possible value. 361243830Sdim return ConditionTruthVal(); 362243830Sdim} 363243830Sdim 364218887Sdim/// Scan all symbols referenced by the constraints. If the symbol is not alive 365218887Sdim/// as marked in LSymbols, mark it as dead in DSymbols. 366234353SdimProgramStateRef 367234353SdimRangeConstraintManager::removeDeadBindings(ProgramStateRef state, 368218887Sdim SymbolReaper& SymReaper) { 369218887Sdim 370218887Sdim ConstraintRangeTy CR = state->get<ConstraintRange>(); 371218887Sdim ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>(); 372218887Sdim 373218887Sdim for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) { 374218887Sdim SymbolRef sym = I.getKey(); 375218887Sdim if (SymReaper.maybeDead(sym)) 376218887Sdim CR = CRFactory.remove(CR, sym); 377218887Sdim } 378218887Sdim 379218887Sdim return state->set<ConstraintRange>(CR); 380218887Sdim} 381218887Sdim 382218887SdimRangeSet 383234353SdimRangeConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) { 384218887Sdim if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym)) 385218887Sdim return *V; 386218887Sdim 387218887Sdim // Lazily generate a new RangeSet representing all possible values for the 388218887Sdim // given symbol type. 389239462Sdim BasicValueFactory &BV = getBasicVals(); 390243830Sdim QualType T = sym->getType(); 391243830Sdim 392243830Sdim RangeSet Result(F, BV.getMinValue(T), BV.getMaxValue(T)); 393243830Sdim 394243830Sdim // Special case: references are known to be non-zero. 395243830Sdim if (T->isReferenceType()) { 396243830Sdim APSIntType IntType = BV.getAPSIntType(T); 397243830Sdim Result = Result.Intersect(BV, F, ++IntType.getZeroValue(), 398243830Sdim --IntType.getZeroValue()); 399243830Sdim } 400243830Sdim 401243830Sdim return Result; 402218887Sdim} 403218887Sdim 404218887Sdim//===------------------------------------------------------------------------=== 405218887Sdim// assumeSymX methods: public interface for RangeConstraintManager. 406218887Sdim//===------------------------------------------------------------------------===/ 407218887Sdim 408218887Sdim// The syntax for ranges below is mathematical, using [x, y] for closed ranges 409218887Sdim// and (x, y) for open ranges. These ranges are modular, corresponding with 410218887Sdim// a common treatment of C integer overflow. This means that these methods 411218887Sdim// do not have to worry about overflow; RangeSet::Intersect can handle such a 412218887Sdim// "wraparound" range. 413218887Sdim// As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1, 414218887Sdim// UINT_MAX, 0, 1, and 2. 415218887Sdim 416234353SdimProgramStateRef 417239462SdimRangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym, 418239462Sdim const llvm::APSInt &Int, 419239462Sdim const llvm::APSInt &Adjustment) { 420239462Sdim // Before we do any real work, see if the value can even show up. 421239462Sdim APSIntType AdjustmentType(Adjustment); 422249423Sdim if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within) 423239462Sdim return St; 424218887Sdim 425239462Sdim llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment; 426218887Sdim llvm::APSInt Upper = Lower; 427218887Sdim --Lower; 428218887Sdim ++Upper; 429218887Sdim 430218887Sdim // [Int-Adjustment+1, Int-Adjustment-1] 431218887Sdim // Notice that the lower bound is greater than the upper bound. 432239462Sdim RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower); 433239462Sdim return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 434218887Sdim} 435218887Sdim 436234353SdimProgramStateRef 437239462SdimRangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym, 438239462Sdim const llvm::APSInt &Int, 439239462Sdim const llvm::APSInt &Adjustment) { 440239462Sdim // Before we do any real work, see if the value can even show up. 441239462Sdim APSIntType AdjustmentType(Adjustment); 442249423Sdim if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within) 443239462Sdim return NULL; 444239462Sdim 445218887Sdim // [Int-Adjustment, Int-Adjustment] 446239462Sdim llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment; 447239462Sdim RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt); 448239462Sdim return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 449218887Sdim} 450218887Sdim 451234353SdimProgramStateRef 452239462SdimRangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym, 453239462Sdim const llvm::APSInt &Int, 454239462Sdim const llvm::APSInt &Adjustment) { 455239462Sdim // Before we do any real work, see if the value can even show up. 456239462Sdim APSIntType AdjustmentType(Adjustment); 457249423Sdim switch (AdjustmentType.testInRange(Int, true)) { 458239462Sdim case APSIntType::RTR_Below: 459239462Sdim return NULL; 460239462Sdim case APSIntType::RTR_Within: 461239462Sdim break; 462239462Sdim case APSIntType::RTR_Above: 463239462Sdim return St; 464239462Sdim } 465218887Sdim 466218887Sdim // Special case for Int == Min. This is always false. 467239462Sdim llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 468239462Sdim llvm::APSInt Min = AdjustmentType.getMinValue(); 469239462Sdim if (ComparisonVal == Min) 470218887Sdim return NULL; 471218887Sdim 472218887Sdim llvm::APSInt Lower = Min-Adjustment; 473239462Sdim llvm::APSInt Upper = ComparisonVal-Adjustment; 474218887Sdim --Upper; 475218887Sdim 476239462Sdim RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 477239462Sdim return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 478218887Sdim} 479218887Sdim 480234353SdimProgramStateRef 481239462SdimRangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym, 482239462Sdim const llvm::APSInt &Int, 483239462Sdim const llvm::APSInt &Adjustment) { 484239462Sdim // Before we do any real work, see if the value can even show up. 485239462Sdim APSIntType AdjustmentType(Adjustment); 486249423Sdim switch (AdjustmentType.testInRange(Int, true)) { 487239462Sdim case APSIntType::RTR_Below: 488239462Sdim return St; 489239462Sdim case APSIntType::RTR_Within: 490239462Sdim break; 491239462Sdim case APSIntType::RTR_Above: 492239462Sdim return NULL; 493239462Sdim } 494218887Sdim 495218887Sdim // Special case for Int == Max. This is always false. 496239462Sdim llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 497239462Sdim llvm::APSInt Max = AdjustmentType.getMaxValue(); 498239462Sdim if (ComparisonVal == Max) 499218887Sdim return NULL; 500218887Sdim 501239462Sdim llvm::APSInt Lower = ComparisonVal-Adjustment; 502218887Sdim llvm::APSInt Upper = Max-Adjustment; 503218887Sdim ++Lower; 504218887Sdim 505239462Sdim RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 506239462Sdim return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 507218887Sdim} 508218887Sdim 509234353SdimProgramStateRef 510239462SdimRangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym, 511239462Sdim const llvm::APSInt &Int, 512239462Sdim const llvm::APSInt &Adjustment) { 513239462Sdim // Before we do any real work, see if the value can even show up. 514239462Sdim APSIntType AdjustmentType(Adjustment); 515249423Sdim switch (AdjustmentType.testInRange(Int, true)) { 516239462Sdim case APSIntType::RTR_Below: 517239462Sdim return St; 518239462Sdim case APSIntType::RTR_Within: 519239462Sdim break; 520239462Sdim case APSIntType::RTR_Above: 521239462Sdim return NULL; 522239462Sdim } 523218887Sdim 524218887Sdim // Special case for Int == Min. This is always feasible. 525239462Sdim llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 526239462Sdim llvm::APSInt Min = AdjustmentType.getMinValue(); 527239462Sdim if (ComparisonVal == Min) 528239462Sdim return St; 529218887Sdim 530239462Sdim llvm::APSInt Max = AdjustmentType.getMaxValue(); 531239462Sdim llvm::APSInt Lower = ComparisonVal-Adjustment; 532218887Sdim llvm::APSInt Upper = Max-Adjustment; 533218887Sdim 534239462Sdim RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 535239462Sdim return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 536218887Sdim} 537218887Sdim 538234353SdimProgramStateRef 539239462SdimRangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym, 540239462Sdim const llvm::APSInt &Int, 541239462Sdim const llvm::APSInt &Adjustment) { 542239462Sdim // Before we do any real work, see if the value can even show up. 543239462Sdim APSIntType AdjustmentType(Adjustment); 544249423Sdim switch (AdjustmentType.testInRange(Int, true)) { 545239462Sdim case APSIntType::RTR_Below: 546239462Sdim return NULL; 547239462Sdim case APSIntType::RTR_Within: 548239462Sdim break; 549239462Sdim case APSIntType::RTR_Above: 550239462Sdim return St; 551239462Sdim } 552218887Sdim 553218887Sdim // Special case for Int == Max. This is always feasible. 554239462Sdim llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 555239462Sdim llvm::APSInt Max = AdjustmentType.getMaxValue(); 556239462Sdim if (ComparisonVal == Max) 557239462Sdim return St; 558218887Sdim 559239462Sdim llvm::APSInt Min = AdjustmentType.getMinValue(); 560218887Sdim llvm::APSInt Lower = Min-Adjustment; 561239462Sdim llvm::APSInt Upper = ComparisonVal-Adjustment; 562218887Sdim 563239462Sdim RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 564239462Sdim return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 565218887Sdim} 566218887Sdim 567218887Sdim//===------------------------------------------------------------------------=== 568218887Sdim// Pretty-printing. 569218887Sdim//===------------------------------------------------------------------------===/ 570218887Sdim 571234353Sdimvoid RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out, 572218887Sdim const char* nl, const char *sep) { 573218887Sdim 574218887Sdim ConstraintRangeTy Ranges = St->get<ConstraintRange>(); 575218887Sdim 576234353Sdim if (Ranges.isEmpty()) { 577234353Sdim Out << nl << sep << "Ranges are empty." << nl; 578218887Sdim return; 579234353Sdim } 580218887Sdim 581234353Sdim Out << nl << sep << "Ranges of symbol values:"; 582218887Sdim for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){ 583218887Sdim Out << nl << ' ' << I.getKey() << " : "; 584218887Sdim I.getData().print(Out); 585218887Sdim } 586234353Sdim Out << nl; 587218887Sdim} 588