RangeConstraintManager.cpp revision ca5d78d0bc3010164f2f9682967d64d7e305a167
14502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//== RangeConstraintManager.cpp - Manage range constraints.------*- C++ -*--==//
24502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
34502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//                     The LLVM Compiler Infrastructure
44502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
54502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// This file is distributed under the University of Illinois Open Source
64502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek// License. See LICENSE.TXT for details.
74502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
84502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===//
94502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
101eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump//  This file defines RangeConstraintManager, a class that tracks simple
1118c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek//  equality and inequality constraints on symbolic values of ProgramState.
124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===//
144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "SimpleConstraintManager.h"
161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
1718c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
1818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/Support/Debug.h"
204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/ADT/FoldingSet.h"
214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/ADT/ImmutableSet.h"
224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "llvm/Support/raw_ostream.h"
234502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekusing namespace clang;
259ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenekusing namespace ento;
264502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
27ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamnamespace { class ConstraintRange {}; }
289beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenekstatic int ConstraintRangeIndex = 0;
294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
309beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// A Range represents the closed range [from, to].  The caller must
319beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// guarantee that from <= to.  Note that Range is immutable, so as not
329beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// to subvert RangeSet's immutability.
33b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremeneknamespace {
34ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass Range : public std::pair<const llvm::APSInt*,
35b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek                                                const llvm::APSInt*> {
364502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic:
374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  Range(const llvm::APSInt &from, const llvm::APSInt &to)
389beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) {
394502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    assert(from <= to);
404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  bool Includes(const llvm::APSInt &v) const {
429beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *first <= v && v <= *second;
434502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  const llvm::APSInt &From() const {
459beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *first;
464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  const llvm::APSInt &To() const {
489beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *second;
494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
509beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  const llvm::APSInt *getConcreteValue() const {
519beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return &From() == &To() ? &From() : NULL;
524502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  void Profile(llvm::FoldingSetNodeID &ID) const {
559beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    ID.AddPointer(&From());
569beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    ID.AddPointer(&To());
574502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
60b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek
61ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeTrait : public llvm::ImutContainerInfo<Range> {
62b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenekpublic:
63b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  // When comparing if one Range is less than another, we should compare
64e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek  // the actual APSInt values instead of their pointers.  This keeps the order
65e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek  // consistent (instead of comparing by pointer values) and can potentially
66e53f8206ebb36a17e95e64270704e2608d1796f4Ted Kremenek  // be used to speed up some of the operations in RangeSet.
67b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
681eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) &&
69b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek                                       *lhs.second < *rhs.second);
70b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  }
71b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek};
72b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek
739beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek/// RangeSet contains a set of ranges. If the set is empty, then
749beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek///  there the value of a symbol is overly constrained and there are no
759beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek///  possible values for that symbol.
76ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeSet {
77b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek  typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  PrimRangeSet ranges; // no need to make const, since it is an
794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                       // ImmutableSet - this allows default operator=
801eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump                       // to work.
814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic:
829beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  typedef PrimRangeSet::Factory Factory;
839beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  typedef PrimRangeSet::iterator iterator;
844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
859beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  RangeSet(PrimRangeSet RS) : ranges(RS) {}
864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
879beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  iterator begin() const { return ranges.begin(); }
889beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  iterator end() const { return ranges.end(); }
891eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
909beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  bool isEmpty() const { return ranges.isEmpty(); }
911eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
929beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  /// Construct a new RangeSet representing '{ [from, to] }'.
939beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
943baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek    : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
951eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
969beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  /// Profile - Generates a hash profile of this RangeSet for use
979beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ///  by FoldingSet.
989beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1009beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  /// getConcreteValue - If a symbol is contrained to equal a specific integer
1019beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ///  constant then this method returns that value.  Otherwise, it returns
1029beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ///  NULL.
1039beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  const llvm::APSInt* getConcreteValue() const {
1049beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0;
1054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
107ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseprivate:
108ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  void IntersectInRange(BasicValueFactory &BV, Factory &F,
109ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        const llvm::APSInt &Lower,
110ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        const llvm::APSInt &Upper,
111ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        PrimRangeSet &newRanges,
112ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        PrimRangeSet::iterator &i,
113ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                        PrimRangeSet::iterator &e) const {
114ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    // There are six cases for each range R in the set:
115ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   1. R is entirely before the intersection range.
116ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   2. R is entirely after the intersection range.
117ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   3. R contains the entire intersection range.
118ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   4. R starts before the intersection range and ends in the middle.
119ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   5. R starts in the middle of the intersection range and ends after it.
120ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    //   6. R is entirely contained in the intersection range.
121ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    // These correspond to each of the conditions below.
122ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    for (/* i = begin(), e = end() */; i != e; ++i) {
123ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      if (i->To() < Lower) {
124ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        continue;
125ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      }
126ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      if (i->From() > Upper) {
1279beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek        break;
1284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek      }
1294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
130ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      if (i->Includes(Lower)) {
131ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        if (i->Includes(Upper)) {
1323baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, Range(BV.getValue(Lower),
133ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                             BV.getValue(Upper)));
134ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose          break;
135ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        } else
1363baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
137ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      } else {
138ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        if (i->Includes(Upper)) {
1393baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper)));
140ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose          break;
141ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        } else
1423baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek          newRanges = F.add(newRanges, *i);
143ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      }
1444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    }
1454502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  const llvm::APSInt &getMinValue() const {
1481d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    assert(!isEmpty());
1491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return ranges.begin()->From();
1501d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  }
1511d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
1521d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const {
1531d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    // This function has nine cases, the cartesian product of range-testing
1541d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    // both the upper and lower bounds against the symbol's type.
1551d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    // Each case requires a different pinning operation.
1561d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    // The function returns false if the described range is entirely outside
1571d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    // the range of values for the associated symbol.
1581d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    APSIntType Type(getMinValue());
1591d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower);
1601d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper);
1611d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
1621d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    switch (LowerTest) {
1631d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    case APSIntType::RTR_Below:
1641d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      switch (UpperTest) {
1651d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      case APSIntType::RTR_Below:
1661d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // The entire range is outside the symbol's set of possible values.
1671d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // If this is a conventionally-ordered range, the state is infeasible.
1681d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        if (Lower < Upper)
1691d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose          return false;
1701d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
1711d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // However, if the range wraps around, it spans all possible values.
1721d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Lower = Type.getMinValue();
1731d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Upper = Type.getMaxValue();
1741d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        break;
1751d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      case APSIntType::RTR_Within:
1761d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // The range starts below what's possible but ends within it. Pin.
1771d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Lower = Type.getMinValue();
1781d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Type.apply(Upper);
1791d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        break;
1801d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      case APSIntType::RTR_Above:
1811d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // The range spans all possible values for the symbol. Pin.
1821d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Lower = Type.getMinValue();
1831d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Upper = Type.getMaxValue();
1841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        break;
1851d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      }
1861d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      break;
1871d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    case APSIntType::RTR_Within:
1881d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      switch (UpperTest) {
1891d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      case APSIntType::RTR_Below:
1901d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // The range wraps around, but all lower values are not possible.
1911d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Type.apply(Lower);
1921d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Upper = Type.getMaxValue();
1931d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        break;
1941d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      case APSIntType::RTR_Within:
1951d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // The range may or may not wrap around, but both limits are valid.
1961d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Type.apply(Lower);
1971d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Type.apply(Upper);
1981d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        break;
1991d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      case APSIntType::RTR_Above:
2001d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // The range starts within what's possible but ends above it. Pin.
2011d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Type.apply(Lower);
2021d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Upper = Type.getMaxValue();
2031d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        break;
2041d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      }
2051d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      break;
2061d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    case APSIntType::RTR_Above:
2071d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      switch (UpperTest) {
2081d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      case APSIntType::RTR_Below:
2091d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // The range wraps but is outside the symbol's set of possible values.
2101d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        return false;
2111d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      case APSIntType::RTR_Within:
2121d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // The range starts above what's possible but ends within it (wrap).
2131d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Lower = Type.getMinValue();
2141d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Type.apply(Upper);
2151d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        break;
2161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      case APSIntType::RTR_Above:
2171d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // The entire range is outside the symbol's set of possible values.
2181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // If this is a conventionally-ordered range, the state is infeasible.
2191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        if (Lower < Upper)
2201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose          return false;
2211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
2221d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        // However, if the range wraps around, it spans all possible values.
2231d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Lower = Type.getMinValue();
2241d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Upper = Type.getMaxValue();
2251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        break;
2261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      }
2271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      break;
2281d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    }
2291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
2301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return true;
2311d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  }
2321d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
233ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rosepublic:
234ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Returns a set containing the values in the receiving set, intersected with
235ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // the closed range [Lower, Upper]. Unlike the Range type, this range uses
236ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // modular arithmetic, corresponding to the common treatment of C integer
237ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // overflow. Thus, if the Lower bound is greater than the Upper bound, the
238ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // range is taken to wrap around. This is equivalent to taking the
239ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // intersection with the two ranges [Min, Upper] and [Lower, Max],
240ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // or, alternatively, /removing/ all integers between Upper and Lower.
241ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  RangeSet Intersect(BasicValueFactory &BV, Factory &F,
2421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                     llvm::APSInt Lower, llvm::APSInt Upper) const {
2431d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    if (!pin(Lower, Upper))
2441d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      return F.getEmptySet();
2451d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
2463baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek    PrimRangeSet newRanges = F.getEmptySet();
2474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
248ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    PrimRangeSet::iterator i = begin(), e = end();
249ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    if (Lower <= Upper)
250ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);
251ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    else {
252ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      // The order of the next two statements is important!
253ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      // IntersectInRange() does not reset the iteration state for i and e.
254ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      // Therefore, the lower range most be handled first.
255ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
256ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose      IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
2574502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    }
2581d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
2599beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return newRanges;
2604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
2614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2625f9e272e632e951b1efe824cd16acb4d96077930Chris Lattner  void print(raw_ostream &os) const {
2639beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    bool isFirst = true;
2644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    os << "{ ";
2659beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    for (iterator i = begin(), e = end(); i != e; ++i) {
2669beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek      if (isFirst)
2679beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek        isFirst = false;
2689beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek      else
2694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek        os << ", ";
2701eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek      os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
2724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek         << ']';
2734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    }
2741eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    os << " }";
2759beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  }
2761eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  bool operator==(const RangeSet &other) const {
2784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    return ranges == other.ranges;
2794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
2804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
281b103f01e5e2072c04ea5619c587a2b7ff2e63022Ted Kremenek} // end anonymous namespace
2824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2839beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenektypedef llvm::ImmutableMap<SymbolRef,RangeSet> ConstraintRangeTy;
2844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang {
2869ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento {
2874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenektemplate<>
28818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekstruct ProgramStateTrait<ConstraintRange>
28918c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek  : public ProgramStatePartialTrait<ConstraintRangeTy> {
2909c378f705405d37f49795d5e915989de774fe11fTed Kremenek  static inline void *GDMIndex() { return &ConstraintRangeIndex; }
2914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
2921eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump}
2935a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis}
2941eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace {
296ba5fb5a955c896815c439289fc51c03cf0635129Kovarththanan Rajaratnamclass RangeConstraintManager : public SimpleConstraintManager{
2978bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
2984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekpublic:
299ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose  RangeConstraintManager(SubEngine *subengine, BasicValueFactory &BVF)
3001d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    : SimpleConstraintManager(subengine, BVF) {}
3014502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3028bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
303ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
304ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
3054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3068bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
307ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
308ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
3094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3108bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
311ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
312ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
3134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3148bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
315ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
316ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
3174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3188bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
319ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
320ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
3214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3228bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
323ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Int,
324ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                             const llvm::APSInt& Adjustment);
3254502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3268bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  const llvm::APSInt* getSymVal(ProgramStateRef St, SymbolRef sym) const;
3271eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
3288bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  ProgramStateRef removeDeadBindings(ProgramStateRef St, SymbolReaper& SymReaper);
3294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3308bef8238181a30e52dea380789a7e2d760eac532Ted Kremenek  void print(ProgramStateRef St, raw_ostream &Out,
3314502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek             const char* nl, const char *sep);
3324502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3334502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekprivate:
3349beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  RangeSet::Factory F;
3354502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek};
3364502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} // end anonymous namespace
3384502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseConstraintManager *
340ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Roseento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
3411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  return new RangeConstraintManager(Eng, StMgr.getBasicVals());
3424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
3434502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3448bef8238181a30e52dea380789a7e2d760eac532Ted Kremenekconst llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St,
3454502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                                      SymbolRef sym) const {
3469beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym);
3479beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  return T ? T->getConcreteValue() : NULL;
3484502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
3494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3504502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// Scan all symbols referenced by the constraints. If the symbol is not alive
3514502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek/// as marked in LSymbols, mark it as dead in DSymbols.
3528bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
3538bef8238181a30e52dea380789a7e2d760eac532Ted KremenekRangeConstraintManager::removeDeadBindings(ProgramStateRef state,
3544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                           SymbolReaper& SymReaper) {
3554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
356c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  ConstraintRangeTy CR = state->get<ConstraintRange>();
357c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>();
3584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3599beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
3601eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    SymbolRef sym = I.getKey();
3614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    if (SymReaper.maybeDead(sym))
3623baf672378f105602d2b12f03f00277ae1936fe9Ted Kremenek      CR = CRFactory.remove(CR, sym);
3634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
3641eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
365c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  return state->set<ConstraintRange>(CR);
3669beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek}
3679beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
3689beefec2a9f5d34ab70fef06515c7987cb041f07Ted KremenekRangeSet
3698bef8238181a30e52dea380789a7e2d760eac532Ted KremenekRangeConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) {
370c87813824896a7124d2dd1c08e4661bbe119abf5Ted Kremenek  if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
3719beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek    return *V;
3721eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
3739beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  // Lazily generate a new RangeSet representing all possible values for the
3749beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  // given symbol type.
3751d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  BasicValueFactory &BV = getBasicVals();
376732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek  QualType T = sym->getType();
377efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek
378efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek  RangeSet Result(F, BV.getMinValue(T), BV.getMaxValue(T));
379efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek
380efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek  // Special case: references are known to be non-zero.
381efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek  if (T->isReferenceType()) {
382efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek    APSIntType IntType = BV.getAPSIntType(T);
383efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek    Result = Result.Intersect(BV, F, ++IntType.getZeroValue(),
384efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek                                     --IntType.getZeroValue());
385efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek  }
386efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek
387efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek  return Result;
3884502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
3894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
3909beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===
39128f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek// assumeSymX methods: public interface for RangeConstraintManager.
3929beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/
3939beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
394ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// The syntax for ranges below is mathematical, using [x, y] for closed ranges
395ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// and (x, y) for open ranges. These ranges are modular, corresponding with
396ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// a common treatment of C integer overflow. This means that these methods
397ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// do not have to worry about overflow; RangeSet::Intersect can handle such a
398ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// "wraparound" range.
399ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
400ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose// UINT_MAX, 0, 1, and 2.
401ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
4028bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
4031d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymNE(ProgramStateRef St, SymbolRef Sym,
4041d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
4051d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
4061d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
4071d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
4081d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  if (AdjustmentType.testInRange(Int) != APSIntType::RTR_Within)
4091d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
4101d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
4111d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment;
412ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Lower;
413ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  --Lower;
414ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  ++Upper;
415ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
416ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // [Int-Adjustment+1, Int-Adjustment-1]
417ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Notice that the lower bound is greater than the upper bound.
4181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
4191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
4209beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek}
4219beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
4228bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
4231d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymEQ(ProgramStateRef St, SymbolRef Sym,
4241d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
4251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
4261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
4271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
4281d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  if (AdjustmentType.testInRange(Int) != APSIntType::RTR_Within)
4291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return NULL;
4301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
431ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // [Int-Adjustment, Int-Adjustment]
4321d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
4331d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
4341d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
435ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
436ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
4378bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
4381d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymLT(ProgramStateRef St, SymbolRef Sym,
4391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
4401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
4411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
4421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
4431d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  switch (AdjustmentType.testInRange(Int)) {
4441d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Below:
4451d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return NULL;
4461d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Within:
4471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    break;
4481d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Above:
4491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
4501d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  }
451ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
452ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Min. This is always false.
4531d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
4541d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Min = AdjustmentType.getMinValue();
4551d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  if (ComparisonVal == Min)
456ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    return NULL;
457ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
458ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Min-Adjustment;
4591d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Upper = ComparisonVal-Adjustment;
460ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  --Upper;
461ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
4621d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
4631d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
464ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
465ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
4668bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
4671d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymGT(ProgramStateRef St, SymbolRef Sym,
4681d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
4691d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
4701d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
4711d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
4721d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  switch (AdjustmentType.testInRange(Int)) {
4731d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Below:
4741d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
4751d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Within:
4761d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    break;
4771d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Above:
4781d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return NULL;
4791d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  }
480ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
481ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Max. This is always false.
4821d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
4831d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Max = AdjustmentType.getMaxValue();
4841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  if (ComparisonVal == Max)
485ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose    return NULL;
486ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
4871d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Lower = ComparisonVal-Adjustment;
488ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Max-Adjustment;
489ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  ++Lower;
490ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
4911d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
4921d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
493ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
494ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
4958bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
4961d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymGE(ProgramStateRef St, SymbolRef Sym,
4971d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
4981d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
4991d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
5001d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
5011d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  switch (AdjustmentType.testInRange(Int)) {
5021d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Below:
5031d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
5041d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Within:
5051d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    break;
5061d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Above:
5071d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return NULL;
5081d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  }
509ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
510ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Min. This is always feasible.
5111d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
5121d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Min = AdjustmentType.getMinValue();
5131d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  if (ComparisonVal == Min)
5141d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
515ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Max = AdjustmentType.getMaxValue();
5171d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Lower = ComparisonVal-Adjustment;
518ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Upper = Max-Adjustment;
519ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
5211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
522ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
523ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5248bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef
5251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseRangeConstraintManager::assumeSymLE(ProgramStateRef St, SymbolRef Sym,
5261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Int,
5271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                    const llvm::APSInt &Adjustment) {
5281d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Before we do any real work, see if the value can even show up.
5291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType AdjustmentType(Adjustment);
5301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  switch (AdjustmentType.testInRange(Int)) {
5311d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Below:
5321d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return NULL;
5331d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Within:
5341d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    break;
5351d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  case APSIntType::RTR_Above:
5361d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
5371d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  }
538ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
539ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // Special case for Int == Max. This is always feasible.
5401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
5411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Max = AdjustmentType.getMaxValue();
5421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  if (ComparisonVal == Max)
5431d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    return St;
544ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5451d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Min = AdjustmentType.getMinValue();
546ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  llvm::APSInt Lower = Min-Adjustment;
5471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Upper = ComparisonVal-Adjustment;
548ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
5491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
5501d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
551ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
5529beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
5539beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===
5549beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek// Pretty-printing.
5559beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek//===------------------------------------------------------------------------===/
5569beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek
5578bef8238181a30e52dea380789a7e2d760eac532Ted Kremenekvoid RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out,
5584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek                                   const char* nl, const char *sep) {
5591eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5609beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  ConstraintRangeTy Ranges = St->get<ConstraintRange>();
5611eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5621a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks  if (Ranges.isEmpty()) {
5631a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks    Out << nl << sep << "Ranges are empty." << nl;
564dd28d00a2f5cc10b0ccf3705adcf4d8a62ecc8aaTed Kremenek    return;
5651a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks  }
5661eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
5671a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks  Out << nl << sep << "Ranges of symbol values:";
5689beefec2a9f5d34ab70fef06515c7987cb041f07Ted Kremenek  for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){
569b35007cc4de8256b39dc1ed9abdeb8b2458c3c01Ted Kremenek    Out << nl << ' ' << I.getKey() << " : ";
57053ba0b636194dbeaa65a6f85316c9397a0c5298bTed Kremenek    I.getData().print(Out);
5714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
5721a00eef3b02230ccad30fb34d8357a4e376c47faAnna Zaks  Out << nl;
5734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
574