RangeConstraintManager.cpp revision ca5d78d0bc3010164f2f9682967d64d7e305a167
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 1118c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek// equality and inequality constraints on symbolic values of ProgramState. 124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// 134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===// 144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "SimpleConstraintManager.h" 161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" 1718c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 1818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.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 1471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &getMinValue() const { 1481d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose assert(!isEmpty()); 1491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return ranges.begin()->From(); 1501d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 1511d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 1521d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const { 1531d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // This function has nine cases, the cartesian product of range-testing 1541d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // both the upper and lower bounds against the symbol's type. 1551d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Each case requires a different pinning operation. 1561d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The function returns false if the described range is entirely outside 1571d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // the range of values for the associated symbol. 1581d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType Type(getMinValue()); 1591d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower); 1601d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper); 1611d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 1621d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (LowerTest) { 1631d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 1641d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (UpperTest) { 1651d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 1661d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The entire range is outside the symbol's set of possible values. 1671d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // If this is a conventionally-ordered range, the state is infeasible. 1681d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Lower < Upper) 1691d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return false; 1701d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 1711d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // However, if the range wraps around, it spans all possible values. 1721d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Lower = Type.getMinValue(); 1731d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Upper = Type.getMaxValue(); 1741d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1751d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 1761d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range starts below what's possible but ends within it. Pin. 1771d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Lower = Type.getMinValue(); 1781d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Upper); 1791d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1801d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 1811d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range spans all possible values for the symbol. Pin. 1821d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Lower = Type.getMinValue(); 1831d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Upper = Type.getMaxValue(); 1841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1851d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 1861d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1871d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 1881d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (UpperTest) { 1891d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 1901d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range wraps around, but all lower values are not possible. 1911d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Lower); 1921d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Upper = Type.getMaxValue(); 1931d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1941d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 1951d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range may or may not wrap around, but both limits are valid. 1961d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Lower); 1971d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Upper); 1981d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1991d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 2001d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range starts within what's possible but ends above it. Pin. 2011d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Lower); 2021d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Upper = Type.getMaxValue(); 2031d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 2041d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 2051d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 2061d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 2071d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (UpperTest) { 2081d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 2091d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range wraps but is outside the symbol's set of possible values. 2101d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return false; 2111d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 2121d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range starts above what's possible but ends within it (wrap). 2131d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Lower = Type.getMinValue(); 2141d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Upper); 2151d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 2161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 2171d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The entire range is outside the symbol's set of possible values. 2181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // If this is a conventionally-ordered range, the state is infeasible. 2191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Lower < Upper) 2201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return false; 2211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2221d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // However, if the range wraps around, it spans all possible values. 2231d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Lower = Type.getMinValue(); 2241d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Upper = Type.getMaxValue(); 2251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 2261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 2271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 2281d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 2291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return true; 2311d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 2321d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 233ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rosepublic: 234ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Returns a set containing the values in the receiving set, intersected with 235ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // the closed range [Lower, Upper]. Unlike the Range type, this range uses 236ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // modular arithmetic, corresponding to the common treatment of C integer 237ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // overflow. Thus, if the Lower bound is greater than the Upper bound, the 238ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // range is taken to wrap around. This is equivalent to taking the 239ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // intersection with the two ranges [Min, Upper] and [Lower, Max], 240ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // or, alternatively, /removing/ all integers between Upper and Lower. 241ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose RangeSet Intersect(BasicValueFactory &BV, Factory &F, 2421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Lower, llvm::APSInt Upper) const { 2431d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (!pin(Lower, Upper)) 2441d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return F.getEmptySet(); 2451d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2463baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek PrimRangeSet newRanges = F.getEmptySet(); 2474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 248ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose PrimRangeSet::iterator i = begin(), e = end(); 249ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (Lower <= Upper) 250ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose IntersectInRange(BV, F, Lower, Upper, newRanges, i, e); 251ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose else { 252ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // The order of the next two statements is important! 253ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // IntersectInRange() does not reset the iteration state for i and e. 254ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Therefore, the lower range most be handled first. 255ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e); 256ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e); 2574502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2581d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2599beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return newRanges; 2604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2625f9e272e632e951b1efe824cd16acb4d96077930Chris Lattner void print(raw_ostream &os) const { 2639beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek bool isFirst = true; 2644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek os << "{ "; 2659beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek for (iterator i = begin(), e = end(); i != e; ++i) { 2669beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek if (isFirst) 2679beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek isFirst = false; 2689beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek else 2694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek os << ", "; 2701eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek os << '[' << i->From().toString(10) << ", " << i->To().toString(10) 2724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek << ']'; 2734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2741eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump os << " }"; 2759beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek } 2761eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool operator==(const RangeSet &other) const { 2784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return ranges == other.ranges; 2794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 281b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek} // end anonymous namespace 2824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2839beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenektypedef llvm::ImmutableMap<SymbolRef,RangeSet> ConstraintRangeTy; 2844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang { 2869ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento { 2874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenektemplate<> 28818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekstruct ProgramStateTrait<ConstraintRange> 28918c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek : public ProgramStatePartialTrait<ConstraintRangeTy> { 2909c378f705405d37f49795d5e915989de774fe11fTed Kremenek static inline void *GDMIndex() { return &ConstraintRangeIndex; } 2914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 2921eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump} 2935a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} 2941eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace { 296ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeConstraintManager : public SimpleConstraintManager{ 2978bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek RangeSet GetRange(ProgramStateRef state, SymbolRef sym); 2984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic: 299ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose RangeConstraintManager(SubEngine *subengine, BasicValueFactory &BVF) 3001d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose : SimpleConstraintManager(subengine, BVF) {} 3014502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3028bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym, 303ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 304ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 3054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3068bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym, 307ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 308ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 3094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3108bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym, 311ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 312ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 3134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3148bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym, 315ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 316ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 3174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3188bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym, 319ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 320ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 3214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3228bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym, 323ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 324ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 3254502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3268bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek const llvm::APSInt* getSymVal(ProgramStateRef St, SymbolRef sym) const; 3271eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3288bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef removeDeadBindings(ProgramStateRef St, SymbolReaper& SymReaper); 3294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3308bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek void print(ProgramStateRef St, raw_ostream &Out, 3314502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const char* nl, const char *sep); 3324502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3334502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekprivate: 3349beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek RangeSet::Factory F; 3354502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 3364502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} // end anonymous namespace 3384502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseConstraintManager * 340ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Roseento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) { 3411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return new RangeConstraintManager(Eng, StMgr.getBasicVals()); 3424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 3434502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3448bef8238181a30e52dea380789a7e2d760eac532Ted Kremenekconst llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St, 3454502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym) const { 3469beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym); 3479beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return T ? T->getConcreteValue() : NULL; 3484502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 3494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3504502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// Scan all symbols referenced by the constraints. If the symbol is not alive 3514502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// as marked in LSymbols, mark it as dead in DSymbols. 3528bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 3538bef8238181a30e52dea380789a7e2d760eac532Ted KremenekRangeConstraintManager::removeDeadBindings(ProgramStateRef state, 3544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolReaper& SymReaper) { 3554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 356c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek ConstraintRangeTy CR = state->get<ConstraintRange>(); 357c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>(); 3584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3599beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) { 3601eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump SymbolRef sym = I.getKey(); 3614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (SymReaper.maybeDead(sym)) 3623baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek CR = CRFactory.remove(CR, sym); 3634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 3641eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 365c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek return state->set<ConstraintRange>(CR); 3669beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek} 3679beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 3689beefec2a9f5d34ab70fef06515c7987cb041f07Ted KremenekRangeSet 3698bef8238181a30e52dea380789a7e2d760eac532Ted KremenekRangeConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) { 370c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym)) 3719beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return *V; 3721eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3739beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek // Lazily generate a new RangeSet representing all possible values for the 3749beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek // given symbol type. 3751d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BasicValueFactory &BV = getBasicVals(); 376732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek QualType T = sym->getType(); 377efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek 378efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek RangeSet Result(F, BV.getMinValue(T), BV.getMaxValue(T)); 379efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek 380efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek // Special case: references are known to be non-zero. 381efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (T->isReferenceType()) { 382efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek APSIntType IntType = BV.getAPSIntType(T); 383efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek Result = Result.Intersect(BV, F, ++IntType.getZeroValue(), 384efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek --IntType.getZeroValue()); 385efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek } 386efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek 387efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek return Result; 3884502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 3894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3909beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------=== 39128f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek// assumeSymX methods: public interface for RangeConstraintManager. 3929beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/ 3939beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 394ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// The syntax for ranges below is mathematical, using [x, y] for closed ranges 395ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// and (x, y) for open ranges. These ranges are modular, corresponding with 396ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// a common treatment of C integer overflow. This means that these methods 397ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// do not have to worry about overflow; RangeSet::Intersect can handle such a 398ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// "wraparound" range. 399ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1, 400ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// UINT_MAX, 0, 1, and 2. 401ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 4028bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 4031d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym, 4041d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 4051d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 4061d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 4071d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 4081d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (AdjustmentType.testInRange(Int) != APSIntType::RTR_Within) 4091d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 4101d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 4111d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment; 412ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Upper = Lower; 413ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose --Lower; 414ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose ++Upper; 415ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 416ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // [Int-Adjustment+1, Int-Adjustment-1] 417ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Notice that the lower bound is greater than the upper bound. 4181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower); 4191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 4209beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek} 4219beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 4228bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 4231d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym, 4241d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 4251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 4261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 4271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 4281d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (AdjustmentType.testInRange(Int) != APSIntType::RTR_Within) 4291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return NULL; 4301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 431ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // [Int-Adjustment, Int-Adjustment] 4321d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment; 4331d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt); 4341d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 435ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 436ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 4378bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 4381d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym, 4391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 4401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 4411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 4421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 4431d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (AdjustmentType.testInRange(Int)) { 4441d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 4451d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return NULL; 4461d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 4471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 4481d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 4491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 4501d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 451ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 452ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Min. This is always false. 4531d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 4541d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Min = AdjustmentType.getMinValue(); 4551d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (ComparisonVal == Min) 456ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return NULL; 457ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 458ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Lower = Min-Adjustment; 4591d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Upper = ComparisonVal-Adjustment; 460ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose --Upper; 461ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 4621d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 4631d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 464ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 465ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 4668bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 4671d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym, 4681d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 4691d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 4701d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 4711d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 4721d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (AdjustmentType.testInRange(Int)) { 4731d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 4741d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 4751d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 4761d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 4771d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 4781d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return NULL; 4791d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 480ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 481ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Max. This is always false. 4821d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 4831d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Max = AdjustmentType.getMaxValue(); 4841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (ComparisonVal == Max) 485ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return NULL; 486ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 4871d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Lower = ComparisonVal-Adjustment; 488ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Upper = Max-Adjustment; 489ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose ++Lower; 490ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 4911d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 4921d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 493ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 494ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 4958bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 4961d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym, 4971d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 4981d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 4991d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 5001d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 5011d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (AdjustmentType.testInRange(Int)) { 5021d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 5031d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 5041d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 5051d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 5061d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 5071d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return NULL; 5081d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 509ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 510ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Min. This is always feasible. 5111d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 5121d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Min = AdjustmentType.getMinValue(); 5131d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (ComparisonVal == Min) 5141d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 515ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Max = AdjustmentType.getMaxValue(); 5171d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Lower = ComparisonVal-Adjustment; 518ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Upper = Max-Adjustment; 519ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 5211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 522ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 523ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5248bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 5251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym, 5261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 5271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 5281d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 5291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 5301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (AdjustmentType.testInRange(Int)) { 5311d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 5321d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return NULL; 5331d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 5341d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 5351d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 5361d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 5371d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 538ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 539ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Max. This is always feasible. 5401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 5411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Max = AdjustmentType.getMaxValue(); 5421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (ComparisonVal == Max) 5431d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 544ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5451d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Min = AdjustmentType.getMinValue(); 546ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Lower = Min-Adjustment; 5471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Upper = ComparisonVal-Adjustment; 548ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 5501d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 551ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 5529beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 5539beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------=== 5549beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek// Pretty-printing. 5559beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/ 5569beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 5578bef8238181a30e52dea380789a7e2d760eac532Ted Kremenekvoid RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out, 5584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const char* nl, const char *sep) { 5591eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5609beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek ConstraintRangeTy Ranges = St->get<ConstraintRange>(); 5611eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5621a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks if (Ranges.isEmpty()) { 5631a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks Out << nl << sep << "Ranges are empty." << nl; 564dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek return; 5651a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks } 5661eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5671a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks Out << nl << sep << "Ranges of symbol values:"; 5689beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){ 569b35007cc4de8256b39dc1ed9abdeb8b2458c3c01Ted Kremenek Out << nl << ' ' << I.getKey() << " : "; 57053ba0b636194dbeaa65a6f85316c9397a0c5298bTed Kremenek I.getData().print(Out); 5714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 5721a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks Out << nl; 5734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 574