RangeConstraintManager.cpp revision 9b663716449b618ba0390b1dbebc54fa8e971124
14502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//== RangeConstraintManager.cpp - Manage range constraints.------*- C++ -*--==//
24502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
34502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//                     The LLVM Compiler Infrastructure
44502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
54502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// This file is distributed under the University of Illinois Open Source
64502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// License. See LICENSE.TXT for details.
74502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
84502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===//
94502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
101eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump//  This file defines RangeConstraintManager, a class that tracks simple
114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//  equality and inequality constraints on symbolic values of GRState.
124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===//
144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "SimpleConstraintManager.h"
169b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/GRState.h"
179b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/GRStateTrait.h"
189b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/TransferFuncs.h"
199b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/ManagerRegistry.h"
204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/Support/Debug.h"
214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/ADT/FoldingSet.h"
224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/ADT/ImmutableSet.h"
234502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/Support/raw_ostream.h"
244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
254502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekusing namespace clang;
269ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenekusing namespace ento;
274502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
28ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamnamespace { class ConstraintRange {}; }
299beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenekstatic int ConstraintRangeIndex = 0;
304502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
319beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// A Range represents the closed range [from, to].  The caller must
329beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// guarantee that from <= to.  Note that Range is immutable, so as not
339beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// to subvert RangeSet's immutability.
34b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremeneknamespace {
35ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass Range : public std::pair<const llvm::APSInt*,
36b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek                                                const llvm::APSInt*> {
374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic:
384502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  Range(const llvm::APSInt &from, const llvm::APSInt &to)
399beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) {
404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    assert(from <= to);
414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  bool Includes(const llvm::APSInt &v) const {
439beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *first <= v && v <= *second;
444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
454502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  const llvm::APSInt &From() const {
469beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *first;
474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
484502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  const llvm::APSInt &To() const {
499beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *second;
504502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
519beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  const llvm::APSInt *getConcreteValue() const {
529beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return &From() == &To() ? &From() : NULL;
534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  void Profile(llvm::FoldingSetNodeID &ID) const {
569beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    ID.AddPointer(&From());
579beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    ID.AddPointer(&To());
584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
61b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek
62ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeTrait : public llvm::ImutContainerInfo<Range> {
63b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenekpublic:
64b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  // When comparing if one Range is less than another, we should compare
65e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek  // the actual APSInt values instead of their pointers.  This keeps the order
66e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek  // consistent (instead of comparing by pointer values) and can potentially
67e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek  // be used to speed up some of the operations in RangeSet.
68b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
691eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) &&
70b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek                                       *lhs.second < *rhs.second);
71b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  }
72b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek};
73b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek
749beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// RangeSet contains a set of ranges. If the set is empty, then
759beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek///  there the value of a symbol is overly constrained and there are no
769beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek///  possible values for that symbol.
77ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeSet {
78b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  PrimRangeSet ranges; // no need to make const, since it is an
804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                       // ImmutableSet - this allows default operator=
811eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump                       // to work.
824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic:
839beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  typedef PrimRangeSet::Factory Factory;
849beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  typedef PrimRangeSet::iterator iterator;
854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
869beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  RangeSet(PrimRangeSet RS) : ranges(RS) {}
874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
889beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  iterator begin() const { return ranges.begin(); }
899beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  iterator end() const { return ranges.end(); }
901eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
919beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  bool isEmpty() const { return ranges.isEmpty(); }
921eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
939beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  /// Construct a new RangeSet representing '{ [from, to] }'.
949beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
953baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek    : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
961eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
979beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  /// Profile - Generates a hash profile of this RangeSet for use
989beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ///  by FoldingSet.
999beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
1004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1019beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  /// getConcreteValue - If a symbol is contrained to equal a specific integer
1029beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ///  constant then this method returns that value.  Otherwise, it returns
1039beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ///  NULL.
1049beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  const llvm::APSInt* getConcreteValue() const {
1059beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0;
1064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
108ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseprivate:
109ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  void IntersectInRange(BasicValueFactory &BV, Factory &F,
110ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        const llvm::APSInt &Lower,
111ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        const llvm::APSInt &Upper,
112ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        PrimRangeSet &newRanges,
113ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        PrimRangeSet::iterator &i,
114ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        PrimRangeSet::iterator &e) const {
115ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    // There are six cases for each range R in the set:
116ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   1. R is entirely before the intersection range.
117ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   2. R is entirely after the intersection range.
118ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   3. R contains the entire intersection range.
119ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   4. R starts before the intersection range and ends in the middle.
120ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   5. R starts in the middle of the intersection range and ends after it.
121ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   6. R is entirely contained in the intersection range.
122ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    // These correspond to each of the conditions below.
123ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    for (/* i = begin(), e = end() */; i != e; ++i) {
124ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      if (i->To() < Lower) {
125ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        continue;
126ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      }
127ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      if (i->From() > Upper) {
1289beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek        break;
1294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek      }
1304502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
131ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      if (i->Includes(Lower)) {
132ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        if (i->Includes(Upper)) {
1333baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, Range(BV.getValue(Lower),
134ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                             BV.getValue(Upper)));
135ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose          break;
136ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        } else
1373baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
138ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      } else {
139ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        if (i->Includes(Upper)) {
1403baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper)));
141ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose          break;
142ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        } else
1433baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, *i);
144ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      }
1454502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    }
1464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
148ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rosepublic:
149ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Returns a set containing the values in the receiving set, intersected with
150ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // the closed range [Lower, Upper]. Unlike the Range type, this range uses
151ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // modular arithmetic, corresponding to the common treatment of C integer
152ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // overflow. Thus, if the Lower bound is greater than the Upper bound, the
153ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // range is taken to wrap around. This is equivalent to taking the
154ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // intersection with the two ranges [Min, Upper] and [Lower, Max],
155ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // or, alternatively, /removing/ all integers between Upper and Lower.
156ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet Intersect(BasicValueFactory &BV, Factory &F,
157ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                     const llvm::APSInt &Lower,
158ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                     const llvm::APSInt &Upper) const {
1593baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek    PrimRangeSet newRanges = F.getEmptySet();
1604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
161ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    PrimRangeSet::iterator i = begin(), e = end();
162ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    if (Lower <= Upper)
163ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);
164ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    else {
165ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      // The order of the next two statements is important!
166ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      // IntersectInRange() does not reset the iteration state for i and e.
167ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      // Therefore, the lower range most be handled first.
168ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
169ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
1704502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    }
1719beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return newRanges;
1724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
17453ba0b636194dbeaa65a6f85316c9397a0c5298bTed Kremenek  void print(llvm::raw_ostream &os) const {
1759beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    bool isFirst = true;
1764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    os << "{ ";
1779beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    for (iterator i = begin(), e = end(); i != e; ++i) {
1789beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek      if (isFirst)
1799beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek        isFirst = false;
1809beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek      else
1814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek        os << ", ";
1821eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek      os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
1844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek         << ']';
1854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    }
1861eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    os << " }";
1879beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  }
1881eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  bool operator==(const RangeSet &other) const {
1904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    return ranges == other.ranges;
1914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1924502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
193b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek} // end anonymous namespace
1944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1959beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenektypedef llvm::ImmutableMap<SymbolRef,RangeSet> ConstraintRangeTy;
1964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang {
1989ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento {
1994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenektemplate<>
2009beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenekstruct GRStateTrait<ConstraintRange>
2019beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  : public GRStatePartialTrait<ConstraintRangeTy> {
2021eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  static inline void* GDMIndex() { return &ConstraintRangeIndex; }
2034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
2041eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump}
2055a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis}
2061eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace {
208ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeConstraintManager : public SimpleConstraintManager{
2091eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  RangeSet GetRange(const GRState *state, SymbolRef sym);
2104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic:
211d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  RangeConstraintManager(SubEngine &subengine)
21232a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek    : SimpleConstraintManager(subengine) {}
2134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
21428f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek  const GRState *assumeSymNE(const GRState* state, SymbolRef sym,
215ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
216ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
21828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek  const GRState *assumeSymEQ(const GRState* state, SymbolRef sym,
219ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
220ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
22228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek  const GRState *assumeSymLT(const GRState* state, SymbolRef sym,
223ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
224ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2254502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
22628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek  const GRState *assumeSymGT(const GRState* state, SymbolRef sym,
227ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
228ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
23028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek  const GRState *assumeSymGE(const GRState* state, SymbolRef sym,
231ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
232ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2334502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
23428f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek  const GRState *assumeSymLE(const GRState* state, SymbolRef sym,
235ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
236ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2384502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  const llvm::APSInt* getSymVal(const GRState* St, SymbolRef sym) const;
2391eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2409beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  // FIXME: Refactor into SimpleConstraintManager?
2419beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  bool isEqual(const GRState* St, SymbolRef sym, const llvm::APSInt& V) const {
2429beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    const llvm::APSInt *i = getSymVal(St, sym);
2439beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return i ? *i == V : false;
2449beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  }
2454502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
246db0594bfc013131f88429add4eb653c285fa94fbTed Kremenek  const GRState* removeDeadBindings(const GRState* St, SymbolReaper& SymReaper);
2474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2481eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  void print(const GRState* St, llvm::raw_ostream& Out,
2494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek             const char* nl, const char *sep);
2504502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2514502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekprivate:
2529beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  RangeSet::Factory F;
2534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
2544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} // end anonymous namespace
2564502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2579ef6537a894c33003359b1f9b9676e9178e028b7Ted KremenekConstraintManager* ento::CreateRangeConstraintManager(GRStateManager&,
258d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis                                                    SubEngine &subeng) {
25932a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek  return new RangeConstraintManager(subeng);
2604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
2614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekconst llvm::APSInt* RangeConstraintManager::getSymVal(const GRState* St,
2634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                                      SymbolRef sym) const {
2649beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym);
2659beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  return T ? T->getConcreteValue() : NULL;
2664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
2674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2684502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// Scan all symbols referenced by the constraints. If the symbol is not alive
2694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// as marked in LSymbols, mark it as dead in DSymbols.
2704502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekconst GRState*
271db0594bfc013131f88429add4eb653c285fa94fbTed KremenekRangeConstraintManager::removeDeadBindings(const GRState* state,
2724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                           SymbolReaper& SymReaper) {
2734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
274c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  ConstraintRangeTy CR = state->get<ConstraintRange>();
275c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>();
2764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2779beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
2781eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    SymbolRef sym = I.getKey();
2794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    if (SymReaper.maybeDead(sym))
2803baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek      CR = CRFactory.remove(CR, sym);
2814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
2821eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
283c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  return state->set<ConstraintRange>(CR);
2849beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek}
2859beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
2869beefec2a9f5d34ab70fef06515c7987cb041f07Ted KremenekRangeSet
287c87813824896a7124d2dd1c08e4661bbe119abf5Ted KremenekRangeConstraintManager::GetRange(const GRState *state, SymbolRef sym) {
288c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
2899beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *V;
2901eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2919beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  // Lazily generate a new RangeSet representing all possible values for the
2929beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  // given symbol type.
293c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  QualType T = state->getSymbolManager().getType(sym);
2941eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  BasicValueFactory& BV = state->getBasicVals();
2959beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  return RangeSet(F, BV.getMinValue(T), BV.getMaxValue(T));
2964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
2974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2989beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===
29928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek// assumeSymX methods: public interface for RangeConstraintManager.
3009beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/
3019beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
302ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// The syntax for ranges below is mathematical, using [x, y] for closed ranges
303ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// and (x, y) for open ranges. These ranges are modular, corresponding with
304ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// a common treatment of C integer overflow. This means that these methods
305ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// do not have to worry about overflow; RangeSet::Intersect can handle such a
306ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// "wraparound" range.
307ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
308ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// UINT_MAX, 0, 1, and 2.
309ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
310ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
31128f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted KremenekRangeConstraintManager::assumeSymNE(const GRState* state, SymbolRef sym,
312ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
313ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
314ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
315ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
316ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Int-Adjustment;
317ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Lower;
318ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  --Lower;
319ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  ++Upper;
320ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
321ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // [Int-Adjustment+1, Int-Adjustment-1]
322ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Notice that the lower bound is greater than the upper bound.
323ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, Upper, Lower);
324ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
3259beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek}
3269beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
327ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
32828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted KremenekRangeConstraintManager::assumeSymEQ(const GRState* state, SymbolRef sym,
329ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
330ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
331ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // [Int-Adjustment, Int-Adjustment]
332ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
333ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt AdjInt = Int-Adjustment;
334ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, AdjInt, AdjInt);
335ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
336ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
337ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
338ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
33928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted KremenekRangeConstraintManager::assumeSymLT(const GRState* state, SymbolRef sym,
340ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
341ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
342ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
343ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
344ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  QualType T = state->getSymbolManager().getType(sym);
345ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Min = BV.getMinValue(T);
346ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
347ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Min. This is always false.
348ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  if (Int == Min)
349ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    return NULL;
350ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
351ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Min-Adjustment;
352ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Int-Adjustment;
353ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  --Upper;
354ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
355ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
356ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
357ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
358ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
359ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
36028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted KremenekRangeConstraintManager::assumeSymGT(const GRState* state, SymbolRef sym,
361ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
362ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
363ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
364ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
365ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  QualType T = state->getSymbolManager().getType(sym);
366ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Max = BV.getMaxValue(T);
367ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
368ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Max. This is always false.
369ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  if (Int == Max)
370ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    return NULL;
371ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
372ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Int-Adjustment;
373ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Max-Adjustment;
374ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  ++Lower;
375ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
376ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
377ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
378ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
379ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
380ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
38128f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted KremenekRangeConstraintManager::assumeSymGE(const GRState* state, SymbolRef sym,
382ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
383ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
384ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
385ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
386ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  QualType T = state->getSymbolManager().getType(sym);
387ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Min = BV.getMinValue(T);
388ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
389ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Min. This is always feasible.
390ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  if (Int == Min)
391ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    return state;
392ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
393ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Max = BV.getMaxValue(T);
394ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
395ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Int-Adjustment;
396ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Max-Adjustment;
397ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
398ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
399ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
400ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
401ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
402ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
40328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted KremenekRangeConstraintManager::assumeSymLE(const GRState* state, SymbolRef sym,
404ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
405ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
406ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
407ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
408ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  QualType T = state->getSymbolManager().getType(sym);
409ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Max = BV.getMaxValue(T);
410ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
411ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Max. This is always feasible.
412ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  if (Int == Max)
413ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    return state;
414ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
415ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Min = BV.getMinValue(T);
416ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
417ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Min-Adjustment;
418ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Int-Adjustment;
419ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
420ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
421ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
422ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
4239beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
4249beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===
4259beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek// Pretty-printing.
4269beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/
4279beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
4281eb4433ac451dc16f4133a88af2d002ac26c58efMike Stumpvoid RangeConstraintManager::print(const GRState* St, llvm::raw_ostream& Out,
4294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                   const char* nl, const char *sep) {
4301eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4319beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ConstraintRangeTy Ranges = St->get<ConstraintRange>();
4321eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
433dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek  if (Ranges.isEmpty())
434dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek    return;
4351eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
436dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek  Out << nl << sep << "ranges of symbol values:";
4371eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4389beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){
439ec751c48bc904ec42bc3ce93a198b14a46dc8e01Ted Kremenek    Out << nl << ' ' << I.getKey() << " : ";
44053ba0b636194dbeaa65a6f85316c9397a0c5298bTed Kremenek    I.getData().print(Out);
4414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
4424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
443