RangeConstraintManager.cpp revision 9c378f705405d37f49795d5e915989de774fe11f
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"
194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/Support/Debug.h"
204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/ADT/FoldingSet.h"
214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/ADT/ImmutableSet.h"
224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/Support/raw_ostream.h"
234502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekusing namespace clang;
259ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenekusing namespace ento;
264502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
27ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamnamespace { class ConstraintRange {}; }
289beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenekstatic int ConstraintRangeIndex = 0;
294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
309beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// A Range represents the closed range [from, to].  The caller must
319beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// guarantee that from <= to.  Note that Range is immutable, so as not
329beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// to subvert RangeSet's immutability.
33b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremeneknamespace {
34ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass Range : public std::pair<const llvm::APSInt*,
35b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek                                                const llvm::APSInt*> {
364502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic:
374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  Range(const llvm::APSInt &from, const llvm::APSInt &to)
389beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) {
394502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    assert(from <= to);
404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  bool Includes(const llvm::APSInt &v) const {
429beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *first <= v && v <= *second;
434502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  const llvm::APSInt &From() const {
459beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *first;
464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  const llvm::APSInt &To() const {
489beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *second;
494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
509beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  const llvm::APSInt *getConcreteValue() const {
519beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return &From() == &To() ? &From() : NULL;
524502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  void Profile(llvm::FoldingSetNodeID &ID) const {
559beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    ID.AddPointer(&From());
569beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    ID.AddPointer(&To());
574502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
60b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek
61ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeTrait : public llvm::ImutContainerInfo<Range> {
62b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenekpublic:
63b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  // When comparing if one Range is less than another, we should compare
64e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek  // the actual APSInt values instead of their pointers.  This keeps the order
65e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek  // consistent (instead of comparing by pointer values) and can potentially
66e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek  // be used to speed up some of the operations in RangeSet.
67b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
681eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) &&
69b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek                                       *lhs.second < *rhs.second);
70b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  }
71b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek};
72b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek
739beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// RangeSet contains a set of ranges. If the set is empty, then
749beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek///  there the value of a symbol is overly constrained and there are no
759beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek///  possible values for that symbol.
76ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeSet {
77b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  PrimRangeSet ranges; // no need to make const, since it is an
794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                       // ImmutableSet - this allows default operator=
801eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump                       // to work.
814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic:
829beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  typedef PrimRangeSet::Factory Factory;
839beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  typedef PrimRangeSet::iterator iterator;
844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
859beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  RangeSet(PrimRangeSet RS) : ranges(RS) {}
864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
879beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  iterator begin() const { return ranges.begin(); }
889beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  iterator end() const { return ranges.end(); }
891eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
909beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  bool isEmpty() const { return ranges.isEmpty(); }
911eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
929beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  /// Construct a new RangeSet representing '{ [from, to] }'.
939beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
943baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek    : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
951eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
969beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  /// Profile - Generates a hash profile of this RangeSet for use
979beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ///  by FoldingSet.
989beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1009beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  /// getConcreteValue - If a symbol is contrained to equal a specific integer
1019beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ///  constant then this method returns that value.  Otherwise, it returns
1029beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ///  NULL.
1039beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  const llvm::APSInt* getConcreteValue() const {
1049beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0;
1054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
107ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseprivate:
108ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  void IntersectInRange(BasicValueFactory &BV, Factory &F,
109ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        const llvm::APSInt &Lower,
110ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        const llvm::APSInt &Upper,
111ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        PrimRangeSet &newRanges,
112ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        PrimRangeSet::iterator &i,
113ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        PrimRangeSet::iterator &e) const {
114ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    // There are six cases for each range R in the set:
115ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   1. R is entirely before the intersection range.
116ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   2. R is entirely after the intersection range.
117ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   3. R contains the entire intersection range.
118ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   4. R starts before the intersection range and ends in the middle.
119ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   5. R starts in the middle of the intersection range and ends after it.
120ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   6. R is entirely contained in the intersection range.
121ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    // These correspond to each of the conditions below.
122ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    for (/* i = begin(), e = end() */; i != e; ++i) {
123ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      if (i->To() < Lower) {
124ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        continue;
125ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      }
126ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      if (i->From() > Upper) {
1279beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek        break;
1284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek      }
1294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
130ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      if (i->Includes(Lower)) {
131ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        if (i->Includes(Upper)) {
1323baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, Range(BV.getValue(Lower),
133ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                             BV.getValue(Upper)));
134ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose          break;
135ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        } else
1363baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
137ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      } else {
138ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        if (i->Includes(Upper)) {
1393baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper)));
140ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose          break;
141ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        } else
1423baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, *i);
143ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      }
1444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    }
1454502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
147ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rosepublic:
148ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Returns a set containing the values in the receiving set, intersected with
149ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // the closed range [Lower, Upper]. Unlike the Range type, this range uses
150ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // modular arithmetic, corresponding to the common treatment of C integer
151ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // overflow. Thus, if the Lower bound is greater than the Upper bound, the
152ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // range is taken to wrap around. This is equivalent to taking the
153ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // intersection with the two ranges [Min, Upper] and [Lower, Max],
154ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // or, alternatively, /removing/ all integers between Upper and Lower.
155ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet Intersect(BasicValueFactory &BV, Factory &F,
156ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                     const llvm::APSInt &Lower,
157ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                     const llvm::APSInt &Upper) const {
1583baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek    PrimRangeSet newRanges = F.getEmptySet();
1594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
160ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    PrimRangeSet::iterator i = begin(), e = end();
161ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    if (Lower <= Upper)
162ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);
163ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    else {
164ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      // The order of the next two statements is important!
165ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      // IntersectInRange() does not reset the iteration state for i and e.
166ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      // Therefore, the lower range most be handled first.
167ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
168ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
1694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    }
1709beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return newRanges;
1714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1735f9e272e632e951b1efe824cd16acb4d96077930Chris Lattner  void print(raw_ostream &os) const {
1749beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    bool isFirst = true;
1754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    os << "{ ";
1769beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    for (iterator i = begin(), e = end(); i != e; ++i) {
1779beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek      if (isFirst)
1789beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek        isFirst = false;
1799beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek      else
1804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek        os << ", ";
1811eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek      os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
1834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek         << ']';
1844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    }
1851eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    os << " }";
1869beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  }
1871eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1884502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  bool operator==(const RangeSet &other) const {
1894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    return ranges == other.ranges;
1904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
192b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek} // end anonymous namespace
1934502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1949beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenektypedef llvm::ImmutableMap<SymbolRef,RangeSet> ConstraintRangeTy;
1954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang {
1979ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento {
1984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenektemplate<>
1999beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenekstruct GRStateTrait<ConstraintRange>
2009beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  : public GRStatePartialTrait<ConstraintRangeTy> {
2019c378f705405d37f49795d5e915989de774fe11fTed Kremenek  static inline void *GDMIndex() { return &ConstraintRangeIndex; }
2024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
2031eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump}
2045a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis}
2051eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace {
207ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeConstraintManager : public SimpleConstraintManager{
2081eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  RangeSet GetRange(const GRState *state, SymbolRef sym);
2094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic:
210d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis  RangeConstraintManager(SubEngine &subengine)
21132a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek    : SimpleConstraintManager(subengine) {}
2124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2139c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const GRState *assumeSymNE(const GRState *state, SymbolRef sym,
214ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
215ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2164502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2179c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const GRState *assumeSymEQ(const GRState *state, SymbolRef sym,
218ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
219ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2219c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const GRState *assumeSymLT(const GRState *state, SymbolRef sym,
222ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
223ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2259c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const GRState *assumeSymGT(const GRState *state, SymbolRef sym,
226ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
227ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2299c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const GRState *assumeSymGE(const GRState *state, SymbolRef sym,
230ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
231ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2324502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2339c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const GRState *assumeSymLE(const GRState *state, SymbolRef sym,
234ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
235ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
2364502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2379c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const llvm::APSInt* getSymVal(const GRState *St, SymbolRef sym) const;
2381eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2399beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  // FIXME: Refactor into SimpleConstraintManager?
2409c378f705405d37f49795d5e915989de774fe11fTed Kremenek  bool isEqual(const GRState *St, SymbolRef sym, const llvm::APSInt& V) const {
2419beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    const llvm::APSInt *i = getSymVal(St, sym);
2429beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return i ? *i == V : false;
2439beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  }
2444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2459c378f705405d37f49795d5e915989de774fe11fTed Kremenek  const GRState *removeDeadBindings(const GRState *St, SymbolReaper& SymReaper);
2464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2479c378f705405d37f49795d5e915989de774fe11fTed Kremenek  void print(const GRState *St, raw_ostream &Out,
2484502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek             const char* nl, const char *sep);
2494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2504502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekprivate:
2519beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  RangeSet::Factory F;
2524502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
2534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} // end anonymous namespace
2554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2569ef6537a894c33003359b1f9b9676e9178e028b7Ted KremenekConstraintManager* ento::CreateRangeConstraintManager(GRStateManager&,
257d2592a34a059e7cbb2b11dc53649ac4912422909Argyrios Kyrtzidis                                                    SubEngine &subeng) {
25832a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek  return new RangeConstraintManager(subeng);
2594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
2604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2619c378f705405d37f49795d5e915989de774fe11fTed Kremenekconst llvm::APSInt* RangeConstraintManager::getSymVal(const GRState *St,
2624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                                      SymbolRef sym) const {
2639beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym);
2649beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  return T ? T->getConcreteValue() : NULL;
2654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
2664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// Scan all symbols referenced by the constraints. If the symbol is not alive
2684502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// as marked in LSymbols, mark it as dead in DSymbols.
2694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekconst GRState*
2709c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::removeDeadBindings(const GRState *state,
2714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                           SymbolReaper& SymReaper) {
2724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
273c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  ConstraintRangeTy CR = state->get<ConstraintRange>();
274c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>();
2754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2769beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
2771eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    SymbolRef sym = I.getKey();
2784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    if (SymReaper.maybeDead(sym))
2793baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek      CR = CRFactory.remove(CR, sym);
2804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
2811eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
282c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  return state->set<ConstraintRange>(CR);
2839beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek}
2849beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
2859beefec2a9f5d34ab70fef06515c7987cb041f07Ted KremenekRangeSet
286c87813824896a7124d2dd1c08e4661bbe119abf5Ted KremenekRangeConstraintManager::GetRange(const GRState *state, SymbolRef sym) {
287c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
2889beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *V;
2891eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2909beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  // Lazily generate a new RangeSet representing all possible values for the
2919beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  // given symbol type.
292c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  QualType T = state->getSymbolManager().getType(sym);
2931eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  BasicValueFactory& BV = state->getBasicVals();
2949beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  return RangeSet(F, BV.getMinValue(T), BV.getMaxValue(T));
2954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
2964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2979beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===
29828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek// assumeSymX methods: public interface for RangeConstraintManager.
2999beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/
3009beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
301ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// The syntax for ranges below is mathematical, using [x, y] for closed ranges
302ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// and (x, y) for open ranges. These ranges are modular, corresponding with
303ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// a common treatment of C integer overflow. This means that these methods
304ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// do not have to worry about overflow; RangeSet::Intersect can handle such a
305ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// "wraparound" range.
306ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
307ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// UINT_MAX, 0, 1, and 2.
308ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
309ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
3109c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymNE(const GRState *state, SymbolRef sym,
311ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
312ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
313ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
314ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
315ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Int-Adjustment;
316ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Lower;
317ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  --Lower;
318ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  ++Upper;
319ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
320ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // [Int-Adjustment+1, Int-Adjustment-1]
321ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Notice that the lower bound is greater than the upper bound.
322ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, Upper, Lower);
323ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
3249beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek}
3259beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
326ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
3279c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymEQ(const GRState *state, SymbolRef sym,
328ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
329ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
330ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // [Int-Adjustment, Int-Adjustment]
331ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
332ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt AdjInt = Int-Adjustment;
333ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, AdjInt, AdjInt);
334ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
335ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
336ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
337ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
3389c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymLT(const GRState *state, SymbolRef sym,
339ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
340ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
341ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
342ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
343ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  QualType T = state->getSymbolManager().getType(sym);
344ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Min = BV.getMinValue(T);
345ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
346ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Min. This is always false.
347ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  if (Int == Min)
348ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    return NULL;
349ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
350ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Min-Adjustment;
351ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Int-Adjustment;
352ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  --Upper;
353ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
354ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
355ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
356ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
357ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
358ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
3599c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymGT(const GRState *state, SymbolRef sym,
360ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
361ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
362ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
363ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
364ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  QualType T = state->getSymbolManager().getType(sym);
365ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Max = BV.getMaxValue(T);
366ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
367ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Max. This is always false.
368ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  if (Int == Max)
369ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    return NULL;
370ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
371ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Int-Adjustment;
372ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Max-Adjustment;
373ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  ++Lower;
374ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
375ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
376ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
377ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
378ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
379ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
3809c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymGE(const GRState *state, SymbolRef sym,
381ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
382ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
383ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
384ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
385ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  QualType T = state->getSymbolManager().getType(sym);
386ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Min = BV.getMinValue(T);
387ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
388ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Min. This is always feasible.
389ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  if (Int == Min)
390ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    return state;
391ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
392ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Max = BV.getMaxValue(T);
393ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
394ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Int-Adjustment;
395ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Max-Adjustment;
396ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
397ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
398ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
399ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
400ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
401ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState*
4029c378f705405d37f49795d5e915989de774fe11fTed KremenekRangeConstraintManager::assumeSymLE(const GRState *state, SymbolRef sym,
403ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Int,
404ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                    const llvm::APSInt& Adjustment) {
405ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  BasicValueFactory &BV = state->getBasicVals();
406ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
407ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  QualType T = state->getSymbolManager().getType(sym);
408ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Max = BV.getMaxValue(T);
409ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
410ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Max. This is always feasible.
411ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  if (Int == Max)
412ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    return state;
413ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
414ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  const llvm::APSInt &Min = BV.getMinValue(T);
415ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
416ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Min-Adjustment;
417ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Int-Adjustment;
418ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
419ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
420ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
421ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
4229beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
4239beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===
4249beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek// Pretty-printing.
4259beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/
4269beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
4279c378f705405d37f49795d5e915989de774fe11fTed Kremenekvoid RangeConstraintManager::print(const GRState *St, raw_ostream &Out,
4284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                   const char* nl, const char *sep) {
4291eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4309beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ConstraintRangeTy Ranges = St->get<ConstraintRange>();
4311eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
432dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek  if (Ranges.isEmpty())
433dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek    return;
4341eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
435dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek  Out << nl << sep << "ranges of symbol values:";
4361eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
4379beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){
438ec751c48bc904ec42bc3ce93a198b14a46dc8e01Ted Kremenek    Out << nl << ' ' << I.getKey() << " : ";
43953ba0b636194dbeaa65a6f85316c9397a0c5298bTed Kremenek    I.getData().print(Out);
4404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
4414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
442