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 {
486bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines    return &From() == &To() ? &From() : nullptr;
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 {
1016bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines    return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
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,
293651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines                             const llvm::APSInt& Adjustment) override;
2944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2958bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
296ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
297651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines                             const llvm::APSInt& Adjustment) override;
2984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2998bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
300ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
301651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines                             const llvm::APSInt& Adjustment) override;
3024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3038bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
304ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
305651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines                             const llvm::APSInt& Adjustment) override;
3064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3078bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
308ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
309651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines                             const llvm::APSInt& Adjustment) override;
3104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3118bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
312ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
313651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines                             const llvm::APSInt& Adjustment) override;
3144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
315651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines  const llvm::APSInt* getSymVal(ProgramStateRef St,
316651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines                                SymbolRef sym) const override;
317651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
3181eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
319651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines  ProgramStateRef removeDeadBindings(ProgramStateRef St,
320651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines                                     SymbolReaper& SymReaper) override;
3214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3228bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  void print(ProgramStateRef St, raw_ostream &Out,
323651f13cea278ec967336033dd032faef0e9fc2ecStephen Hines             const char* nl, const char *sep) override;
3244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3254502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekprivate:
3269beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  RangeSet::Factory F;
3274502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
3284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} // end anonymous namespace
3304502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3311d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseConstraintManager *
332ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Roseento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
33378114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose  return new RangeConstraintManager(Eng, StMgr.getSValBuilder());
3344502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
3354502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3368bef8238181a30e52dea380789a7e2d760eac532Ted Kremenekconst llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St,
3374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                                      SymbolRef sym) const {
3389beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym);
3396bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines  return T ? T->getConcreteValue() : nullptr;
3404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
3414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
342c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan RoseConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
343c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose                                                    SymbolRef Sym) {
344c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  const RangeSet *Ranges = State->get<ConstraintRange>(Sym);
345c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose
346c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  // If we don't have any information about this symbol, it's underconstrained.
347c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  if (!Ranges)
348c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose    return ConditionTruthVal();
349c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose
350c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  // If we have a concrete value, see if it's zero.
351c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  if (const llvm::APSInt *Value = Ranges->getConcreteValue())
352c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose    return *Value == 0;
353c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose
354c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  BasicValueFactory &BV = getBasicVals();
355c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  APSIntType IntType = BV.getAPSIntType(Sym->getType());
356c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  llvm::APSInt Zero = IntType.getZeroValue();
357c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose
358c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  // Check if zero is in the set of possible values.
359c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  if (Ranges->Intersect(BV, F, Zero, Zero).isEmpty())
360c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose    return false;
361c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose
362c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  // Zero is a possible value, but it is not the /only/ possible value.
363c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose  return ConditionTruthVal();
364c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose}
365c45bb4dcb648cd8b5250492afe7df254e4157aaaJordan Rose
3664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// Scan all symbols referenced by the constraints. If the symbol is not alive
3674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// as marked in LSymbols, mark it as dead in DSymbols.
3688bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
3698bef8238181a30e52dea380789a7e2d760eac532Ted KremenekRangeConstraintManager::removeDeadBindings(ProgramStateRef state,
3704502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                           SymbolReaper& SymReaper) {
3714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
372c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  ConstraintRangeTy CR = state->get<ConstraintRange>();
373c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>();
3744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3759beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
3761eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    SymbolRef sym = I.getKey();
3774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    if (SymReaper.maybeDead(sym))
3783baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek      CR = CRFactory.remove(CR, sym);
3794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
3801eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
381c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  return state->set<ConstraintRange>(CR);
3829beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek}
3839beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
3849beefec2a9f5d34ab70fef06515c7987cb041f07Ted KremenekRangeSet
3858bef8238181a30e52dea380789a7e2d760eac532Ted KremenekRangeConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) {
386c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
3879beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *V;
3881eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
3899beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  // Lazily generate a new RangeSet representing all possible values for the
3909beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  // given symbol type.
3911d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  BasicValueFactory &BV = getBasicVals();
392732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek  QualType T = sym->getType();
393efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek
394efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek  RangeSet Result(F, BV.getMinValue(T), BV.getMaxValue(T));
395efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek
396efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek  // Special case: references are known to be non-zero.
397efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek  if (T->isReferenceType()) {
398efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek    APSIntType IntType = BV.getAPSIntType(T);
399efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek    Result = Result.Intersect(BV, F, ++IntType.getZeroValue(),
400efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek                                     --IntType.getZeroValue());
401efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek  }
402efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek
403efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek  return Result;
4044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
4054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
4069beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===
40728f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek// assumeSymX methods: public interface for RangeConstraintManager.
4089beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/
4099beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
410ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// The syntax for ranges below is mathematical, using [x, y] for closed ranges
411ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// and (x, y) for open ranges. These ranges are modular, corresponding with
412ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// a common treatment of C integer overflow. This means that these methods
413ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// do not have to worry about overflow; RangeSet::Intersect can handle such a
414ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// "wraparound" range.
415ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
416ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// UINT_MAX, 0, 1, and 2.
417ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
4188bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
4191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
4201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
4211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
4221d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
4231d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
4244708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose  if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
4251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
4261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
4271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment;
428ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Lower;
429ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  --Lower;
430ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  ++Upper;
431ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
432ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // [Int-Adjustment+1, Int-Adjustment-1]
433ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Notice that the lower bound is greater than the upper bound.
4341d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
4356bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
4369beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek}
4379beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
4388bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
4391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
4401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
4411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
4421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
4431d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
4444708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose  if (AdjustmentType.testInRange(Int, true) != APSIntType::RTR_Within)
4456bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines    return nullptr;
4461d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
447ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // [Int-Adjustment, Int-Adjustment]
4481d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
4491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
4506bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
451ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
452ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
4538bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
4541d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
4551d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
4561d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
4571d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
4581d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
4594708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose  switch (AdjustmentType.testInRange(Int, true)) {
4601d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Below:
4616bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines    return nullptr;
4621d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Within:
4631d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    break;
4641d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Above:
4651d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
4661d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  }
467ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
468ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Min. This is always false.
4691d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
4701d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Min = AdjustmentType.getMinValue();
4711d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  if (ComparisonVal == Min)
4726bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines    return nullptr;
473ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
474ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Min-Adjustment;
4751d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Upper = ComparisonVal-Adjustment;
476ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  --Upper;
477ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
4781d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
4796bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
480ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
481ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
4828bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
4831d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
4841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
4851d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
4861d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
4871d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
4884708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose  switch (AdjustmentType.testInRange(Int, true)) {
4891d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Below:
4901d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
4911d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Within:
4921d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    break;
4931d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Above:
4946bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines    return nullptr;
4951d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  }
496ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
497ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Max. This is always false.
4981d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
4991d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Max = AdjustmentType.getMaxValue();
5001d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  if (ComparisonVal == Max)
5016bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines    return nullptr;
502ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5031d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Lower = ComparisonVal-Adjustment;
504ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Max-Adjustment;
505ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  ++Lower;
506ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5071d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
5086bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
509ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
510ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5118bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
5121d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
5131d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
5141d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
5151d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
5161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
5174708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose  switch (AdjustmentType.testInRange(Int, true)) {
5181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Below:
5191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
5201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Within:
5211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    break;
5221d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Above:
5236bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines    return nullptr;
5241d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  }
525ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
526ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Min. This is always feasible.
5271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
5281d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Min = AdjustmentType.getMinValue();
5291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  if (ComparisonVal == Min)
5301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
531ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5321d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Max = AdjustmentType.getMaxValue();
5331d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Lower = ComparisonVal-Adjustment;
534ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Max-Adjustment;
535ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5361d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
5376bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
538ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
539ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5408bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
5411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
5421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
5431d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
5441d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
5451d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
5464708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose  switch (AdjustmentType.testInRange(Int, true)) {
5471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Below:
5486bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines    return nullptr;
5491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Within:
5501d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    break;
5511d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Above:
5521d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
5531d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  }
554ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
555ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Max. This is always feasible.
5561d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
5571d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Max = AdjustmentType.getMaxValue();
5581d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  if (ComparisonVal == Max)
5591d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
560ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5611d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Min = AdjustmentType.getMinValue();
562ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Min-Adjustment;
5631d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Upper = ComparisonVal-Adjustment;
564ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5651d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
5666bcf27bb9a4b5c3f79cb44c0e4654a6d7619ad89Stephen Hines  return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
567ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
5689beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
5699beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===
5709beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek// Pretty-printing.
5719beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/
5729beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
5738bef8238181a30e52dea380789a7e2d760eac532Ted Kremenekvoid RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out,
5744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                   const char* nl, const char *sep) {
5751eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5769beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ConstraintRangeTy Ranges = St->get<ConstraintRange>();
5771eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5781a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks  if (Ranges.isEmpty()) {
5791a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks    Out << nl << sep << "Ranges are empty." << nl;
580dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek    return;
5811a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks  }
5821eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5831a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks  Out << nl << sep << "Ranges of symbol values:";
5849beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){
585b35007cc4de8256b39dc1ed9abdeb8b2458c3c01Ted Kremenek    Out << nl << ' ' << I.getKey() << " : ";
58653ba0b636194dbeaa65a6f85316c9397a0c5298bTed Kremenek    I.getData().print(Out);
5874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
5881a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks  Out << nl;
5894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
590