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/ADT/FoldingSet.h" 204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/ADT/ImmutableSet.h" 2155fc873017f10f6f566b182b70f6fc22aefa3464Chandler Carruth#include "llvm/Support/Debug.h" 224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/Support/raw_ostream.h" 234502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekusing namespace clang; 259ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenekusing namespace ento; 264502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 279beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// A Range represents the closed range [from, to]. The caller must 289beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// guarantee that from <= to. Note that Range is immutable, so as not 299beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// to subvert RangeSet's immutability. 30b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremeneknamespace { 31ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass Range : public std::pair<const llvm::APSInt*, 32b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek const llvm::APSInt*> { 334502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic: 344502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek Range(const llvm::APSInt &from, const llvm::APSInt &to) 359beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) { 364502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert(from <= to); 374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 384502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool Includes(const llvm::APSInt &v) const { 399beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return *first <= v && v <= *second; 404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const llvm::APSInt &From() const { 429beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return *first; 434502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const llvm::APSInt &To() const { 459beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return *second; 464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 479beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek const llvm::APSInt *getConcreteValue() const { 489beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return &From() == &To() ? &From() : NULL; 494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 504502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 514502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek void Profile(llvm::FoldingSetNodeID &ID) const { 529beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek ID.AddPointer(&From()); 539beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek ID.AddPointer(&To()); 544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 564502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 57b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek 58ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeTrait : public llvm::ImutContainerInfo<Range> { 59b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenekpublic: 60b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek // When comparing if one Range is less than another, we should compare 61e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek // the actual APSInt values instead of their pointers. This keeps the order 62e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek // consistent (instead of comparing by pointer values) and can potentially 63e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek // be used to speed up some of the operations in RangeSet. 64b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek static inline bool isLess(key_type_ref lhs, key_type_ref rhs) { 651eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) && 66b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek *lhs.second < *rhs.second); 67b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek } 68b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek}; 69b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek 709beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// RangeSet contains a set of ranges. If the set is empty, then 719beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// there the value of a symbol is overly constrained and there are no 729beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// possible values for that symbol. 73ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeSet { 74b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet; 754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek PrimRangeSet ranges; // no need to make const, since it is an 764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // ImmutableSet - this allows default operator= 771eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump // to work. 784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic: 799beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek typedef PrimRangeSet::Factory Factory; 809beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek typedef PrimRangeSet::iterator iterator; 814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 829beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek RangeSet(PrimRangeSet RS) : ranges(RS) {} 834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 849beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek iterator begin() const { return ranges.begin(); } 859beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek iterator end() const { return ranges.end(); } 861eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 879beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek bool isEmpty() const { return ranges.isEmpty(); } 881eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 899beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// Construct a new RangeSet representing '{ [from, to] }'. 909beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to) 913baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek : ranges(F.add(F.getEmptySet(), Range(from, to))) {} 921eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 939beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// Profile - Generates a hash profile of this RangeSet for use 949beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// by FoldingSet. 959beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); } 964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 979beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// getConcreteValue - If a symbol is contrained to equal a specific integer 989beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// constant then this method returns that value. Otherwise, it returns 999beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek /// NULL. 1009beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek const llvm::APSInt* getConcreteValue() const { 1019beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0; 1024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 104ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseprivate: 105ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose void IntersectInRange(BasicValueFactory &BV, Factory &F, 106ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Lower, 107ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &Upper, 108ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose PrimRangeSet &newRanges, 109ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose PrimRangeSet::iterator &i, 110ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose PrimRangeSet::iterator &e) const { 111ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // There are six cases for each range R in the set: 112ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 1. R is entirely before the intersection range. 113ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 2. R is entirely after the intersection range. 114ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 3. R contains the entire intersection range. 115ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 4. R starts before the intersection range and ends in the middle. 116ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 5. R starts in the middle of the intersection range and ends after it. 117ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // 6. R is entirely contained in the intersection range. 118ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // These correspond to each of the conditions below. 119ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose for (/* i = begin(), e = end() */; i != e; ++i) { 120ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (i->To() < Lower) { 121ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose continue; 122ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 123ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (i->From() > Upper) { 1249beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek break; 1254502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1264502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 127ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (i->Includes(Lower)) { 128ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (i->Includes(Upper)) { 1293baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek newRanges = F.add(newRanges, Range(BV.getValue(Lower), 130ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BV.getValue(Upper))); 131ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose break; 132ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } else 1333baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To())); 134ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } else { 135ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (i->Includes(Upper)) { 1363baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper))); 137ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose break; 138ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } else 1393baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek newRanges = F.add(newRanges, *i); 140ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 1414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1434502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1441d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &getMinValue() const { 1451d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose assert(!isEmpty()); 1461d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return ranges.begin()->From(); 1471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 1481d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 1491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const { 1501d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // This function has nine cases, the cartesian product of range-testing 1511d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // both the upper and lower bounds against the symbol's type. 1521d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Each case requires a different pinning operation. 1531d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The function returns false if the described range is entirely outside 1541d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // the range of values for the associated symbol. 1551d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType Type(getMinValue()); 1564708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower, true); 1574708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper, true); 1581d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 1591d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (LowerTest) { 1601d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 1611d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (UpperTest) { 1621d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 1631d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The entire range is outside the symbol's set of possible values. 1641d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // If this is a conventionally-ordered range, the state is infeasible. 1651d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Lower < Upper) 1661d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return false; 1671d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 1681d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // However, if the range wraps around, it spans all possible values. 1691d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Lower = Type.getMinValue(); 1701d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Upper = Type.getMaxValue(); 1711d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1721d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 1731d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range starts below what's possible but ends within it. Pin. 1741d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Lower = Type.getMinValue(); 1751d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Upper); 1761d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1771d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 1781d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range spans all possible values for the symbol. Pin. 1791d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Lower = Type.getMinValue(); 1801d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Upper = Type.getMaxValue(); 1811d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1821d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 1831d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 1851d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (UpperTest) { 1861d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 1871d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range wraps around, but all lower values are not possible. 1881d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Lower); 1891d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Upper = Type.getMaxValue(); 1901d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1911d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 1921d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range may or may not wrap around, but both limits are valid. 1931d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Lower); 1941d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Upper); 1951d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 1961d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 1971d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range starts within what's possible but ends above it. Pin. 1981d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Lower); 1991d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Upper = Type.getMaxValue(); 2001d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 2011d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 2021d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 2031d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 2041d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose switch (UpperTest) { 2051d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 2061d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range wraps but is outside the symbol's set of possible values. 2071d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return false; 2081d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 2091d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The range starts above what's possible but ends within it (wrap). 2101d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Lower = Type.getMinValue(); 2111d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Type.apply(Upper); 2121d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 2131d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 2141d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // The entire range is outside the symbol's set of possible values. 2151d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // If this is a conventionally-ordered range, the state is infeasible. 2161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Lower < Upper) 2171d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return false; 2181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // However, if the range wraps around, it spans all possible values. 2201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Lower = Type.getMinValue(); 2211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Upper = Type.getMaxValue(); 2221d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 2231d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 2241d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 2251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 2261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return true; 2281d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 2291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 230ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rosepublic: 231ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Returns a set containing the values in the receiving set, intersected with 232ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // the closed range [Lower, Upper]. Unlike the Range type, this range uses 233ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // modular arithmetic, corresponding to the common treatment of C integer 234ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // overflow. Thus, if the Lower bound is greater than the Upper bound, the 235ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // range is taken to wrap around. This is equivalent to taking the 236ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // intersection with the two ranges [Min, Upper] and [Lower, Max], 237ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // or, alternatively, /removing/ all integers between Upper and Lower. 238ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose RangeSet Intersect(BasicValueFactory &BV, Factory &F, 2391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Lower, llvm::APSInt Upper) const { 2401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (!pin(Lower, Upper)) 2411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return F.getEmptySet(); 2421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2433baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek PrimRangeSet newRanges = F.getEmptySet(); 2444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 245ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose PrimRangeSet::iterator i = begin(), e = end(); 246ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (Lower <= Upper) 247ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose IntersectInRange(BV, F, Lower, Upper, newRanges, i, e); 248ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose else { 249ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // The order of the next two statements is important! 250ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // IntersectInRange() does not reset the iteration state for i and e. 251ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Therefore, the lower range most be handled first. 252ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e); 253ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e); 2544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2551d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2569beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return newRanges; 2574502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2595f9e272e632e951b1efe824cd16acb4d96077930Chris Lattner void print(raw_ostream &os) const { 2609beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek bool isFirst = true; 2614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek os << "{ "; 2629beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek for (iterator i = begin(), e = end(); i != e; ++i) { 2639beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek if (isFirst) 2649beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek isFirst = false; 2659beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek else 2664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek os << ", "; 2671eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2684502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek os << '[' << i->From().toString(10) << ", " << i->To().toString(10) 2694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek << ']'; 2704502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2711eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump os << " }"; 2729beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek } 2731eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool operator==(const RangeSet &other) const { 2754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return ranges == other.ranges; 2764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 278b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek} // end anonymous namespace 2794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 28040d8551890bc8454c4e0a28c9072c9c1d1dd588aJordan RoseREGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintRange, 28140d8551890bc8454c4e0a28c9072c9c1d1dd588aJordan Rose CLANG_ENTO_PROGRAMSTATE_MAP(SymbolRef, 28240d8551890bc8454c4e0a28c9072c9c1d1dd588aJordan Rose RangeSet)) 2831eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace { 285ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeConstraintManager : public SimpleConstraintManager{ 2868bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek RangeSet GetRange(ProgramStateRef state, SymbolRef sym); 2874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic: 28878114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose RangeConstraintManager(SubEngine *subengine, SValBuilder &SVB) 28978114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose : SimpleConstraintManager(subengine, SVB) {} 2904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2918bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym, 292ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 293ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 2944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2958bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym, 296ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 297ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 2984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2998bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym, 300ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 301ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 3024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3038bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym, 304ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 305ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 3064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3078bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym, 308ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 309ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 3104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3118bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym, 312ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int, 313ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Adjustment); 3144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3158bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek const llvm::APSInt* getSymVal(ProgramStateRef St, SymbolRef sym) const; 316c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym); 3171eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3188bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek ProgramStateRef removeDeadBindings(ProgramStateRef St, SymbolReaper& SymReaper); 3194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3208bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek void print(ProgramStateRef St, raw_ostream &Out, 3214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const char* nl, const char *sep); 3224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3234502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekprivate: 3249beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek RangeSet::Factory F; 3254502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}; 3264502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3274502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} // end anonymous namespace 3284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseConstraintManager * 330ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Roseento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) { 33178114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose return new RangeConstraintManager(Eng, StMgr.getSValBuilder()); 3324502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 3334502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3348bef8238181a30e52dea380789a7e2d760eac532Ted Kremenekconst llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St, 3354502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym) const { 3369beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym); 3379beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return T ? T->getConcreteValue() : NULL; 3384502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 3394502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 340c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan RoseConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State, 341c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose SymbolRef Sym) { 342c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose const RangeSet *Ranges = State->get<ConstraintRange>(Sym); 343c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose 344c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose // If we don't have any information about this symbol, it's underconstrained. 345c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose if (!Ranges) 346c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose return ConditionTruthVal(); 347c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose 348c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose // If we have a concrete value, see if it's zero. 349c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose if (const llvm::APSInt *Value = Ranges->getConcreteValue()) 350c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose return *Value == 0; 351c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose 352c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose BasicValueFactory &BV = getBasicVals(); 353c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose APSIntType IntType = BV.getAPSIntType(Sym->getType()); 354c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose llvm::APSInt Zero = IntType.getZeroValue(); 355c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose 356c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose // Check if zero is in the set of possible values. 357c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose if (Ranges->Intersect(BV, F, Zero, Zero).isEmpty()) 358c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose return false; 359c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose 360c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose // Zero is a possible value, but it is not the /only/ possible value. 361c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose return ConditionTruthVal(); 362c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose} 363c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose 3644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// Scan all symbols referenced by the constraints. If the symbol is not alive 3654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// as marked in LSymbols, mark it as dead in DSymbols. 3668bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 3678bef8238181a30e52dea380789a7e2d760eac532Ted KremenekRangeConstraintManager::removeDeadBindings(ProgramStateRef state, 3684502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolReaper& SymReaper) { 3694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 370c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek ConstraintRangeTy CR = state->get<ConstraintRange>(); 371c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>(); 3724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3739beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) { 3741eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump SymbolRef sym = I.getKey(); 3754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (SymReaper.maybeDead(sym)) 3763baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek CR = CRFactory.remove(CR, sym); 3774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 3781eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 379c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek return state->set<ConstraintRange>(CR); 3809beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek} 3819beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 3829beefec2a9f5d34ab70fef06515c7987cb041f07Ted KremenekRangeSet 3838bef8238181a30e52dea380789a7e2d760eac532Ted KremenekRangeConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) { 384c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym)) 3859beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek return *V; 3861eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3879beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek // Lazily generate a new RangeSet representing all possible values for the 3889beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek // given symbol type. 3891d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BasicValueFactory &BV = getBasicVals(); 390732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek QualType T = sym->getType(); 391efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek 392efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek RangeSet Result(F, BV.getMinValue(T), BV.getMaxValue(T)); 393efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek 394efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek // Special case: references are known to be non-zero. 395efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (T->isReferenceType()) { 396efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek APSIntType IntType = BV.getAPSIntType(T); 397efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek Result = Result.Intersect(BV, F, ++IntType.getZeroValue(), 398efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek --IntType.getZeroValue()); 399efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek } 400efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek 401efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek return Result; 4024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 4034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 4049beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------=== 40528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek// assumeSymX methods: public interface for RangeConstraintManager. 4069beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/ 4079beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 408ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// The syntax for ranges below is mathematical, using [x, y] for closed ranges 409ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// and (x, y) for open ranges. These ranges are modular, corresponding with 410ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// a common treatment of C integer overflow. This means that these methods 411ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// do not have to worry about overflow; RangeSet::Intersect can handle such a 412ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// "wraparound" range. 413ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1, 414ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// UINT_MAX, 0, 1, and 2. 415ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 4168bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 4171d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym, 4181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 4191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 4201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 4211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 4224708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within) 4231d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 4241d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 4251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment; 426ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Upper = Lower; 427ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose --Lower; 428ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose ++Upper; 429ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 430ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // [Int-Adjustment+1, Int-Adjustment-1] 431ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Notice that the lower bound is greater than the upper bound. 4321d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower); 4331d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 4349beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek} 4359beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 4368bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 4371d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym, 4381d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 4391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 4401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 4411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 4424708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within) 4431d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return NULL; 4441d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 445ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // [Int-Adjustment, Int-Adjustment] 4461d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment; 4471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt); 4481d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 449ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 450ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 4518bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 4521d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym, 4531d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 4541d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 4551d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 4561d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 4574708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose switch (AdjustmentType.testInRange(Int, true)) { 4581d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 4591d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return NULL; 4601d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 4611d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 4621d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 4631d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 4641d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 465ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 466ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Min. This is always false. 4671d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 4681d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Min = AdjustmentType.getMinValue(); 4691d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (ComparisonVal == Min) 470ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return NULL; 471ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 472ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Lower = Min-Adjustment; 4731d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Upper = ComparisonVal-Adjustment; 474ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose --Upper; 475ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 4761d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 4771d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 478ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 479ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 4808bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 4811d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym, 4821d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 4831d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 4841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 4851d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 4864708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose switch (AdjustmentType.testInRange(Int, true)) { 4871d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 4881d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 4891d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 4901d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 4911d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 4921d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return NULL; 4931d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 494ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 495ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Max. This is always false. 4961d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 4971d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Max = AdjustmentType.getMaxValue(); 4981d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (ComparisonVal == Max) 499ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return NULL; 500ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5011d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Lower = ComparisonVal-Adjustment; 502ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Upper = Max-Adjustment; 503ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose ++Lower; 504ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5051d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 5061d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 507ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 508ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5098bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 5101d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym, 5111d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 5121d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 5131d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 5141d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 5154708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose switch (AdjustmentType.testInRange(Int, true)) { 5161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 5171d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 5181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 5191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 5201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 5211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return NULL; 5221d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 523ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 524ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Min. This is always feasible. 5251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 5261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Min = AdjustmentType.getMinValue(); 5271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (ComparisonVal == Min) 5281d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 529ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Max = AdjustmentType.getMaxValue(); 5311d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Lower = ComparisonVal-Adjustment; 532ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Upper = Max-Adjustment; 533ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5341d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 5351d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 536ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 537ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5388bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef 5391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym, 5401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Int, 5411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &Adjustment) { 5421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Before we do any real work, see if the value can even show up. 5431d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType AdjustmentType(Adjustment); 5444708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose switch (AdjustmentType.testInRange(Int, true)) { 5451d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Below: 5461d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return NULL; 5471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Within: 5481d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose break; 5491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose case APSIntType::RTR_Above: 5501d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 5511d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 552ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 553ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Special case for Int == Max. This is always feasible. 5541d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ComparisonVal = AdjustmentType.convert(Int); 5551d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Max = AdjustmentType.getMaxValue(); 5561d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (ComparisonVal == Max) 5571d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return St; 558ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5591d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Min = AdjustmentType.getMinValue(); 560ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose llvm::APSInt Lower = Min-Adjustment; 5611d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Upper = ComparisonVal-Adjustment; 562ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 5631d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper); 5641d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New); 565ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 5669beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 5679beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------=== 5689beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek// Pretty-printing. 5699beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/ 5709beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek 5718bef8238181a30e52dea380789a7e2d760eac532Ted Kremenekvoid RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out, 5724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const char* nl, const char *sep) { 5731eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5749beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek ConstraintRangeTy Ranges = St->get<ConstraintRange>(); 5751eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5761a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks if (Ranges.isEmpty()) { 5771a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks Out << nl << sep << "Ranges are empty." << nl; 578dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek return; 5791a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks } 5801eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5811a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks Out << nl << sep << "Ranges of symbol values:"; 5829beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){ 583b35007cc4de8256b39dc1ed9abdeb8b2458c3c01Ted Kremenek Out << nl << ' ' << I.getKey() << " : "; 58453ba0b636194dbeaa65a6f85316c9397a0c5298bTed Kremenek I.getData().print(Out); 5854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 5861a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks Out << nl; 5874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 588