clang  3.9.0svn
RangeConstraintManager.cpp
Go to the documentation of this file.
00001 //== RangeConstraintManager.cpp - Manage range constraints.------*- C++ -*--==//
00002 //
00003 //                     The LLVM Compiler Infrastructure
00004 //
00005 // This file is distributed under the University of Illinois Open Source
00006 // License. See LICENSE.TXT for details.
00007 //
00008 //===----------------------------------------------------------------------===//
00009 //
00010 //  This file defines RangeConstraintManager, a class that tracks simple
00011 //  equality and inequality constraints on symbolic values of ProgramState.
00012 //
00013 //===----------------------------------------------------------------------===//
00014 
00015 #include "SimpleConstraintManager.h"
00016 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
00017 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
00018 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
00019 #include "llvm/ADT/FoldingSet.h"
00020 #include "llvm/ADT/ImmutableSet.h"
00021 #include "llvm/Support/Debug.h"
00022 #include "llvm/Support/raw_ostream.h"
00023 
00024 using namespace clang;
00025 using namespace ento;
00026 
00027 /// A Range represents the closed range [from, to].  The caller must
00028 /// guarantee that from <= to.  Note that Range is immutable, so as not
00029 /// to subvert RangeSet's immutability.
00030 namespace {
00031 class Range : public std::pair<const llvm::APSInt*,
00032                                                 const llvm::APSInt*> {
00033 public:
00034   Range(const llvm::APSInt &from, const llvm::APSInt &to)
00035     : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) {
00036     assert(from <= to);
00037   }
00038   bool Includes(const llvm::APSInt &v) const {
00039     return *first <= v && v <= *second;
00040   }
00041   const llvm::APSInt &From() const {
00042     return *first;
00043   }
00044   const llvm::APSInt &To() const {
00045     return *second;
00046   }
00047   const llvm::APSInt *getConcreteValue() const {
00048     return &From() == &To() ? &From() : nullptr;
00049   }
00050 
00051   void Profile(llvm::FoldingSetNodeID &ID) const {
00052     ID.AddPointer(&From());
00053     ID.AddPointer(&To());
00054   }
00055 };
00056 
00057 
00058 class RangeTrait : public llvm::ImutContainerInfo<Range> {
00059 public:
00060   // When comparing if one Range is less than another, we should compare
00061   // the actual APSInt values instead of their pointers.  This keeps the order
00062   // consistent (instead of comparing by pointer values) and can potentially
00063   // be used to speed up some of the operations in RangeSet.
00064   static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
00065     return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) &&
00066                                        *lhs.second < *rhs.second);
00067   }
00068 };
00069 
00070 /// RangeSet contains a set of ranges. If the set is empty, then
00071 ///  there the value of a symbol is overly constrained and there are no
00072 ///  possible values for that symbol.
00073 class RangeSet {
00074   typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
00075   PrimRangeSet ranges; // no need to make const, since it is an
00076                        // ImmutableSet - this allows default operator=
00077                        // to work.
00078 public:
00079   typedef PrimRangeSet::Factory Factory;
00080   typedef PrimRangeSet::iterator iterator;
00081 
00082   RangeSet(PrimRangeSet RS) : ranges(RS) {}
00083 
00084   /// Create a new set with all ranges of this set and RS.
00085   /// Possible intersections are not checked here.
00086   RangeSet addRange(Factory &F, const RangeSet &RS) {
00087     PrimRangeSet Ranges(RS.ranges);
00088     for (const auto &range : ranges)
00089       Ranges = F.add(Ranges, range);
00090     return RangeSet(Ranges);
00091   }
00092 
00093   iterator begin() const { return ranges.begin(); }
00094   iterator end() const { return ranges.end(); }
00095 
00096   bool isEmpty() const { return ranges.isEmpty(); }
00097 
00098   /// Construct a new RangeSet representing '{ [from, to] }'.
00099   RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
00100     : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
00101 
00102   /// Profile - Generates a hash profile of this RangeSet for use
00103   ///  by FoldingSet.
00104   void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
00105 
00106   /// getConcreteValue - If a symbol is contrained to equal a specific integer
00107   ///  constant then this method returns that value.  Otherwise, it returns
00108   ///  NULL.
00109   const llvm::APSInt* getConcreteValue() const {
00110     return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
00111   }
00112 
00113 private:
00114   void IntersectInRange(BasicValueFactory &BV, Factory &F,
00115                         const llvm::APSInt &Lower,
00116                         const llvm::APSInt &Upper,
00117                         PrimRangeSet &newRanges,
00118                         PrimRangeSet::iterator &i,
00119                         PrimRangeSet::iterator &e) const {
00120     // There are six cases for each range R in the set:
00121     //   1. R is entirely before the intersection range.
00122     //   2. R is entirely after the intersection range.
00123     //   3. R contains the entire intersection range.
00124     //   4. R starts before the intersection range and ends in the middle.
00125     //   5. R starts in the middle of the intersection range and ends after it.
00126     //   6. R is entirely contained in the intersection range.
00127     // These correspond to each of the conditions below.
00128     for (/* i = begin(), e = end() */; i != e; ++i) {
00129       if (i->To() < Lower) {
00130         continue;
00131       }
00132       if (i->From() > Upper) {
00133         break;
00134       }
00135 
00136       if (i->Includes(Lower)) {
00137         if (i->Includes(Upper)) {
00138           newRanges = F.add(newRanges, Range(BV.getValue(Lower),
00139                                              BV.getValue(Upper)));
00140           break;
00141         } else
00142           newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
00143       } else {
00144         if (i->Includes(Upper)) {
00145           newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper)));
00146           break;
00147         } else
00148           newRanges = F.add(newRanges, *i);
00149       }
00150     }
00151   }
00152 
00153   const llvm::APSInt &getMinValue() const {
00154     assert(!isEmpty());
00155     return ranges.begin()->From();
00156   }
00157 
00158   bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const {
00159     // This function has nine cases, the cartesian product of range-testing
00160     // both the upper and lower bounds against the symbol's type.
00161     // Each case requires a different pinning operation.
00162     // The function returns false if the described range is entirely outside
00163     // the range of values for the associated symbol.
00164     APSIntType Type(getMinValue());
00165     APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower, true);
00166     APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper, true);
00167 
00168     switch (LowerTest) {
00169     case APSIntType::RTR_Below:
00170       switch (UpperTest) {
00171       case APSIntType::RTR_Below:
00172         // The entire range is outside the symbol's set of possible values.
00173         // If this is a conventionally-ordered range, the state is infeasible.
00174         if (Lower <= Upper)
00175           return false;
00176 
00177         // However, if the range wraps around, it spans all possible values.
00178         Lower = Type.getMinValue();
00179         Upper = Type.getMaxValue();
00180         break;
00181       case APSIntType::RTR_Within:
00182         // The range starts below what's possible but ends within it. Pin.
00183         Lower = Type.getMinValue();
00184         Type.apply(Upper);
00185         break;
00186       case APSIntType::RTR_Above:
00187         // The range spans all possible values for the symbol. Pin.
00188         Lower = Type.getMinValue();
00189         Upper = Type.getMaxValue();
00190         break;
00191       }
00192       break;
00193     case APSIntType::RTR_Within:
00194       switch (UpperTest) {
00195       case APSIntType::RTR_Below:
00196         // The range wraps around, but all lower values are not possible.
00197         Type.apply(Lower);
00198         Upper = Type.getMaxValue();
00199         break;
00200       case APSIntType::RTR_Within:
00201         // The range may or may not wrap around, but both limits are valid.
00202         Type.apply(Lower);
00203         Type.apply(Upper);
00204         break;
00205       case APSIntType::RTR_Above:
00206         // The range starts within what's possible but ends above it. Pin.
00207         Type.apply(Lower);
00208         Upper = Type.getMaxValue();
00209         break;
00210       }
00211       break;
00212     case APSIntType::RTR_Above:
00213       switch (UpperTest) {
00214       case APSIntType::RTR_Below:
00215         // The range wraps but is outside the symbol's set of possible values.
00216         return false;
00217       case APSIntType::RTR_Within:
00218         // The range starts above what's possible but ends within it (wrap).
00219         Lower = Type.getMinValue();
00220         Type.apply(Upper);
00221         break;
00222       case APSIntType::RTR_Above:
00223         // The entire range is outside the symbol's set of possible values.
00224         // If this is a conventionally-ordered range, the state is infeasible.
00225         if (Lower <= Upper)
00226           return false;
00227 
00228         // However, if the range wraps around, it spans all possible values.
00229         Lower = Type.getMinValue();
00230         Upper = Type.getMaxValue();
00231         break;
00232       }
00233       break;
00234     }
00235 
00236     return true;
00237   }
00238 
00239 public:
00240   // Returns a set containing the values in the receiving set, intersected with
00241   // the closed range [Lower, Upper]. Unlike the Range type, this range uses
00242   // modular arithmetic, corresponding to the common treatment of C integer
00243   // overflow. Thus, if the Lower bound is greater than the Upper bound, the
00244   // range is taken to wrap around. This is equivalent to taking the
00245   // intersection with the two ranges [Min, Upper] and [Lower, Max],
00246   // or, alternatively, /removing/ all integers between Upper and Lower.
00247   RangeSet Intersect(BasicValueFactory &BV, Factory &F,
00248                      llvm::APSInt Lower, llvm::APSInt Upper) const {
00249     if (!pin(Lower, Upper))
00250       return F.getEmptySet();
00251 
00252     PrimRangeSet newRanges = F.getEmptySet();
00253 
00254     PrimRangeSet::iterator i = begin(), e = end();
00255     if (Lower <= Upper)
00256       IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);
00257     else {
00258       // The order of the next two statements is important!
00259       // IntersectInRange() does not reset the iteration state for i and e.
00260       // Therefore, the lower range most be handled first.
00261       IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
00262       IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
00263     }
00264 
00265     return newRanges;
00266   }
00267 
00268   void print(raw_ostream &os) const {
00269     bool isFirst = true;
00270     os << "{ ";
00271     for (iterator i = begin(), e = end(); i != e; ++i) {
00272       if (isFirst)
00273         isFirst = false;
00274       else
00275         os << ", ";
00276 
00277       os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
00278          << ']';
00279     }
00280     os << " }";
00281   }
00282 
00283   bool operator==(const RangeSet &other) const {
00284     return ranges == other.ranges;
00285   }
00286 };
00287 } // end anonymous namespace
00288 
00289 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintRange,
00290                                  CLANG_ENTO_PROGRAMSTATE_MAP(SymbolRef,
00291                                                              RangeSet))
00292 
00293 namespace {
00294 class RangeConstraintManager : public SimpleConstraintManager{
00295   RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
00296 public:
00297   RangeConstraintManager(SubEngine *subengine, SValBuilder &SVB)
00298     : SimpleConstraintManager(subengine, SVB) {}
00299 
00300   ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
00301                              const llvm::APSInt& Int,
00302                              const llvm::APSInt& Adjustment) override;
00303 
00304   ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
00305                              const llvm::APSInt& Int,
00306                              const llvm::APSInt& Adjustment) override;
00307 
00308   ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
00309                              const llvm::APSInt& Int,
00310                              const llvm::APSInt& Adjustment) override;
00311 
00312   ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
00313                              const llvm::APSInt& Int,
00314                              const llvm::APSInt& Adjustment) override;
00315 
00316   ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
00317                              const llvm::APSInt& Int,
00318                              const llvm::APSInt& Adjustment) override;
00319 
00320   ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
00321                              const llvm::APSInt& Int,
00322                              const llvm::APSInt& Adjustment) override;
00323 
00324   ProgramStateRef assumeSymbolWithinInclusiveRange(
00325         ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
00326         const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
00327 
00328   ProgramStateRef assumeSymbolOutOfInclusiveRange(
00329         ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
00330         const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
00331 
00332   const llvm::APSInt* getSymVal(ProgramStateRef St,
00333                                 SymbolRef sym) const override;
00334   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
00335 
00336   ProgramStateRef removeDeadBindings(ProgramStateRef St,
00337                                      SymbolReaper& SymReaper) override;
00338 
00339   void print(ProgramStateRef St, raw_ostream &Out,
00340              const char* nl, const char *sep) override;
00341 
00342 private:
00343   RangeSet::Factory F;
00344   RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
00345                          const llvm::APSInt &Int,
00346                          const llvm::APSInt &Adjustment);
00347   RangeSet getSymGTRange(ProgramStateRef St, SymbolRef Sym,
00348                          const llvm::APSInt &Int,
00349                          const llvm::APSInt &Adjustment);
00350   RangeSet getSymLERange(ProgramStateRef St, SymbolRef Sym,
00351                          const llvm::APSInt &Int,
00352                          const llvm::APSInt &Adjustment);
00353   RangeSet getSymLERange(const RangeSet &RS, const llvm::APSInt &Int,
00354                          const llvm::APSInt &Adjustment);
00355   RangeSet getSymGERange(ProgramStateRef St, SymbolRef Sym,
00356                          const llvm::APSInt &Int,
00357                          const llvm::APSInt &Adjustment);
00358 };
00359 
00360 } // end anonymous namespace
00361 
00362 std::unique_ptr<ConstraintManager>
00363 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
00364   return llvm::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
00365 }
00366 
00367 const llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St,
00368                                                       SymbolRef sym) const {
00369   const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym);
00370   return T ? T->getConcreteValue() : nullptr;
00371 }
00372 
00373 ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
00374                                                     SymbolRef Sym) {
00375   const RangeSet *Ranges = State->get<ConstraintRange>(Sym);
00376 
00377   // If we don't have any information about this symbol, it's underconstrained.
00378   if (!Ranges)
00379     return ConditionTruthVal();
00380 
00381   // If we have a concrete value, see if it's zero.
00382   if (const llvm::APSInt *Value = Ranges->getConcreteValue())
00383     return *Value == 0;
00384 
00385   BasicValueFactory &BV = getBasicVals();
00386   APSIntType IntType = BV.getAPSIntType(Sym->getType());
00387   llvm::APSInt Zero = IntType.getZeroValue();
00388 
00389   // Check if zero is in the set of possible values.
00390   if (Ranges->Intersect(BV, F, Zero, Zero).isEmpty())
00391     return false;
00392 
00393   // Zero is a possible value, but it is not the /only/ possible value.
00394   return ConditionTruthVal();
00395 }
00396 
00397 /// Scan all symbols referenced by the constraints. If the symbol is not alive
00398 /// as marked in LSymbols, mark it as dead in DSymbols.
00399 ProgramStateRef
00400 RangeConstraintManager::removeDeadBindings(ProgramStateRef state,
00401                                            SymbolReaper& SymReaper) {
00402 
00403   ConstraintRangeTy CR = state->get<ConstraintRange>();
00404   ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>();
00405 
00406   for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
00407     SymbolRef sym = I.getKey();
00408     if (SymReaper.maybeDead(sym))
00409       CR = CRFactory.remove(CR, sym);
00410   }
00411 
00412   return state->set<ConstraintRange>(CR);
00413 }
00414 
00415 RangeSet
00416 RangeConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) {
00417   if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
00418     return *V;
00419 
00420   // Lazily generate a new RangeSet representing all possible values for the
00421   // given symbol type.
00422   BasicValueFactory &BV = getBasicVals();
00423   QualType T = sym->getType();
00424 
00425   RangeSet Result(F, BV.getMinValue(T), BV.getMaxValue(T));
00426 
00427   // Special case: references are known to be non-zero.
00428   if (T->isReferenceType()) {
00429     APSIntType IntType = BV.getAPSIntType(T);
00430     Result = Result.Intersect(BV, F, ++IntType.getZeroValue(),
00431                                      --IntType.getZeroValue());
00432   }
00433 
00434   return Result;
00435 }
00436 
00437 //===------------------------------------------------------------------------===
00438 // assumeSymX methods: public interface for RangeConstraintManager.
00439 //===------------------------------------------------------------------------===/
00440 
00441 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
00442 // and (x, y) for open ranges. These ranges are modular, corresponding with
00443 // a common treatment of C integer overflow. This means that these methods
00444 // do not have to worry about overflow; RangeSet::Intersect can handle such a
00445 // "wraparound" range.
00446 // As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
00447 // UINT_MAX, 0, 1, and 2.
00448 
00449 ProgramStateRef
00450 RangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
00451                                     const llvm::APSInt &Int,
00452                                     const llvm::APSInt &Adjustment) {
00453   // Before we do any real work, see if the value can even show up.
00454   APSIntType AdjustmentType(Adjustment);
00455   if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
00456     return St;
00457 
00458   llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment;
00459   llvm::APSInt Upper = Lower;
00460   --Lower;
00461   ++Upper;
00462 
00463   // [Int-Adjustment+1, Int-Adjustment-1]
00464   // Notice that the lower bound is greater than the upper bound.
00465   RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
00466   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00467 }
00468 
00469 ProgramStateRef
00470 RangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
00471                                     const llvm::APSInt &Int,
00472                                     const llvm::APSInt &Adjustment) {
00473   // Before we do any real work, see if the value can even show up.
00474   APSIntType AdjustmentType(Adjustment);
00475   if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
00476     return nullptr;
00477 
00478   // [Int-Adjustment, Int-Adjustment]
00479   llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
00480   RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
00481   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00482 }
00483 
00484 RangeSet RangeConstraintManager::getSymLTRange(ProgramStateRef St,
00485                                                SymbolRef Sym,
00486                                                const llvm::APSInt &Int,
00487                                                const llvm::APSInt &Adjustment) {
00488   // Before we do any real work, see if the value can even show up.
00489   APSIntType AdjustmentType(Adjustment);
00490   switch (AdjustmentType.testInRange(Int, true)) {
00491   case APSIntType::RTR_Below:
00492     return F.getEmptySet();
00493   case APSIntType::RTR_Within:
00494     break;
00495   case APSIntType::RTR_Above:
00496     return GetRange(St, Sym);
00497   }
00498 
00499   // Special case for Int == Min. This is always false.
00500   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
00501   llvm::APSInt Min = AdjustmentType.getMinValue();
00502   if (ComparisonVal == Min)
00503     return F.getEmptySet();
00504 
00505   llvm::APSInt Lower = Min - Adjustment;
00506   llvm::APSInt Upper = ComparisonVal - Adjustment;
00507   --Upper;
00508 
00509   return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
00510 }
00511 
00512 ProgramStateRef
00513 RangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
00514                                     const llvm::APSInt &Int,
00515                                     const llvm::APSInt &Adjustment) {
00516   RangeSet New = getSymLTRange(St, Sym, Int, Adjustment);
00517   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00518 }
00519 
00520 RangeSet
00521 RangeConstraintManager::getSymGTRange(ProgramStateRef St, SymbolRef Sym,
00522                                       const llvm::APSInt &Int,
00523                                       const llvm::APSInt &Adjustment) {
00524   // Before we do any real work, see if the value can even show up.
00525   APSIntType AdjustmentType(Adjustment);
00526   switch (AdjustmentType.testInRange(Int, true)) {
00527   case APSIntType::RTR_Below:
00528     return GetRange(St, Sym);
00529   case APSIntType::RTR_Within:
00530     break;
00531   case APSIntType::RTR_Above:
00532     return F.getEmptySet();
00533   }
00534 
00535   // Special case for Int == Max. This is always false.
00536   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
00537   llvm::APSInt Max = AdjustmentType.getMaxValue();
00538   if (ComparisonVal == Max)
00539     return F.getEmptySet();
00540 
00541   llvm::APSInt Lower = ComparisonVal - Adjustment;
00542   llvm::APSInt Upper = Max - Adjustment;
00543   ++Lower;
00544 
00545   return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
00546 }
00547 
00548 ProgramStateRef
00549 RangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
00550                                     const llvm::APSInt &Int,
00551                                     const llvm::APSInt &Adjustment) {
00552   RangeSet New = getSymGTRange(St, Sym, Int, Adjustment);
00553   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00554 }
00555 
00556 RangeSet
00557 RangeConstraintManager::getSymGERange(ProgramStateRef St, SymbolRef Sym,
00558                                       const llvm::APSInt &Int,
00559                                       const llvm::APSInt &Adjustment) {
00560   // Before we do any real work, see if the value can even show up.
00561   APSIntType AdjustmentType(Adjustment);
00562   switch (AdjustmentType.testInRange(Int, true)) {
00563   case APSIntType::RTR_Below:
00564     return GetRange(St, Sym);
00565   case APSIntType::RTR_Within:
00566     break;
00567   case APSIntType::RTR_Above:
00568     return F.getEmptySet();
00569   }
00570 
00571   // Special case for Int == Min. This is always feasible.
00572   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
00573   llvm::APSInt Min = AdjustmentType.getMinValue();
00574   if (ComparisonVal == Min)
00575     return GetRange(St, Sym);
00576 
00577   llvm::APSInt Max = AdjustmentType.getMaxValue();
00578   llvm::APSInt Lower = ComparisonVal - Adjustment;
00579   llvm::APSInt Upper = Max - Adjustment;
00580 
00581   return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
00582 }
00583 
00584 ProgramStateRef
00585 RangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
00586                                     const llvm::APSInt &Int,
00587                                     const llvm::APSInt &Adjustment) {
00588   RangeSet New = getSymGERange(St, Sym, Int, Adjustment);
00589   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00590 }
00591 
00592 RangeSet
00593 RangeConstraintManager::getSymLERange(const RangeSet &RS,
00594                                       const llvm::APSInt &Int,
00595                                       const llvm::APSInt &Adjustment) {
00596   // Before we do any real work, see if the value can even show up.
00597   APSIntType AdjustmentType(Adjustment);
00598   switch (AdjustmentType.testInRange(Int, true)) {
00599   case APSIntType::RTR_Below:
00600     return F.getEmptySet();
00601   case APSIntType::RTR_Within:
00602     break;
00603   case APSIntType::RTR_Above:
00604     return RS;
00605   }
00606 
00607   // Special case for Int == Max. This is always feasible.
00608   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
00609   llvm::APSInt Max = AdjustmentType.getMaxValue();
00610   if (ComparisonVal == Max)
00611     return RS;
00612 
00613   llvm::APSInt Min = AdjustmentType.getMinValue();
00614   llvm::APSInt Lower = Min - Adjustment;
00615   llvm::APSInt Upper = ComparisonVal - Adjustment;
00616 
00617   return RS.Intersect(getBasicVals(), F, Lower, Upper);
00618 }
00619 
00620 RangeSet
00621 RangeConstraintManager::getSymLERange(ProgramStateRef St, SymbolRef Sym,
00622                                       const llvm::APSInt &Int,
00623                                       const llvm::APSInt &Adjustment) {
00624   // Before we do any real work, see if the value can even show up.
00625   APSIntType AdjustmentType(Adjustment);
00626   switch (AdjustmentType.testInRange(Int, true)) {
00627   case APSIntType::RTR_Below:
00628     return F.getEmptySet();
00629   case APSIntType::RTR_Within:
00630     break;
00631   case APSIntType::RTR_Above:
00632     return GetRange(St, Sym);
00633   }
00634 
00635   // Special case for Int == Max. This is always feasible.
00636   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
00637   llvm::APSInt Max = AdjustmentType.getMaxValue();
00638   if (ComparisonVal == Max)
00639     return GetRange(St, Sym);
00640 
00641   llvm::APSInt Min = AdjustmentType.getMinValue();
00642   llvm::APSInt Lower = Min - Adjustment;
00643   llvm::APSInt Upper = ComparisonVal - Adjustment;
00644 
00645   return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
00646 }
00647 
00648 ProgramStateRef
00649 RangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
00650                                     const llvm::APSInt &Int,
00651                                     const llvm::APSInt &Adjustment) {
00652   RangeSet New = getSymLERange(St, Sym, Int, Adjustment);
00653   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
00654 }
00655 
00656 ProgramStateRef
00657 RangeConstraintManager::assumeSymbolWithinInclusiveRange(
00658     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
00659     const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
00660   RangeSet New = getSymGERange(State, Sym, From, Adjustment);
00661   if (New.isEmpty())
00662     return nullptr;
00663   New = getSymLERange(New, To, Adjustment);
00664   return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
00665 }
00666 
00667 ProgramStateRef
00668 RangeConstraintManager::assumeSymbolOutOfInclusiveRange(
00669     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
00670     const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
00671   RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment);
00672   RangeSet RangeGT = getSymGTRange(State, Sym, To, Adjustment);
00673   RangeSet New(RangeLT.addRange(F, RangeGT));
00674   return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
00675 }
00676 
00677 //===------------------------------------------------------------------------===
00678 // Pretty-printing.
00679 //===------------------------------------------------------------------------===/
00680 
00681 void RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out,
00682                                    const char* nl, const char *sep) {
00683 
00684   ConstraintRangeTy Ranges = St->get<ConstraintRange>();
00685 
00686   if (Ranges.isEmpty()) {
00687     Out << nl << sep << "Ranges are empty." << nl;
00688     return;
00689   }
00690 
00691   Out << nl << sep << "Ranges of symbol values:";
00692   for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){
00693     Out << nl << ' ' << I.getKey() << " : ";
00694     I.getData().print(Out);
00695   }
00696   Out << nl;
00697 }