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