SimpleConstraintManager.cpp revision 1d8db493f86761df9470254a2ad572fc6abf1bf6
14502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//== SimpleConstraintManager.cpp --------------------------------*- 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//
104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//  This file defines SimpleConstraintManager, a class that holds code shared
114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//  between BasicConstraintManager and RangeConstraintManager.
124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//
134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek//===----------------------------------------------------------------------===//
144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "SimpleConstraintManager.h"
161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
179b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
1818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang {
214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
229ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento {
235a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis
244502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::~SimpleConstraintManager() {}
254502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2666b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenekbool SimpleConstraintManager::canReasonAbout(SVal X) const {
275344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks  nonloc::SymbolVal *SymVal = dyn_cast<nonloc::SymbolVal>(&X);
285344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks  if (SymVal && SymVal->isExpression()) {
295344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks    const SymExpr *SE = SymVal->getSymbol();
301eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
31e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
32e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek      switch (SIE->getOpcode()) {
33e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek          // We don't reason yet about bitwise-constraints on symbolic values.
342de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall        case BO_And:
352de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall        case BO_Or:
362de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall        case BO_Xor:
37e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek          return false;
38ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        // We don't reason yet about these arithmetic constraints on
39ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose        // symbolic values.
402de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall        case BO_Mul:
412de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall        case BO_Div:
422de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall        case BO_Rem:
432de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall        case BO_Shl:
442de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall        case BO_Shr:
45e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek          return false;
46e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek        // All other cases.
47e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek        default:
48e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek          return true;
491eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump      }
50e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek    }
51e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek
52e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek    return false;
537de20fe9aac00705dd943690563db66fa4b35b5bTed Kremenek  }
547de20fe9aac00705dd943690563db66fa4b35b5bTed Kremenek
5566b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek  return true;
5666b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek}
571eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
588bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
595b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek                                               DefinedSVal Cond,
605b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek                                               bool Assumption) {
614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  if (isa<NonLoc>(Cond))
6228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek    return assume(state, cast<NonLoc>(Cond), Assumption);
634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  else
6428f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek    return assume(state, cast<Loc>(Cond), Assumption);
654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
678bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond,
6832a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek                                               bool assumption) {
6928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek  state = assumeAux(state, cond, assumption);
70e36de1fe51c39d9161915dd3dbef880954af6476Ted Kremenek  return SU.processAssume(state, cond, assumption);
714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
738bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
74a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek                                                  Loc Cond, bool Assumption) {
754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  switch (Cond.getSubKind()) {
764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  default:
774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    assert (false && "'Assume' not implemented for this Loc.");
78a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek    return state;
794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  case loc::MemRegionKind: {
814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    // FIXME: Should this go into the storemanager?
821eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
83a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek    const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion();
84a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek    const SubRegion *SubR = dyn_cast<SubRegion>(R);
854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    while (SubR) {
874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek      // FIXME: now we only find the first symbolic region.
88a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek      if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
891d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth();
903330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu        if (Assumption)
9128f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek          return assumeSymNE(state, SymR->getSymbol(), zero, zero);
923330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu        else
9328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek          return assumeSymEQ(state, SymR->getSymbol(), zero, zero);
943330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu      }
954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek      SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    }
971eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    // FALL-THROUGH.
994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1001eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1014502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  case loc::GotoLabelKind:
102a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek    return Assumption ? state : NULL;
1034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  case loc::ConcreteIntKind: {
1051eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump    bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
106a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek    bool isFeasible = b ? Assumption : !Assumption;
107a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek    return isFeasible ? state : NULL;
1084502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
1094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  } // end switch
1104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
1114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1128bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
11332a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek                                               NonLoc cond,
11432a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek                                               bool assumption) {
11528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek  state = assumeAux(state, cond, assumption);
116e36de1fe51c39d9161915dd3dbef880954af6476Ted Kremenek  return SU.processAssume(state, cond, assumption);
1174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
1184502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
119ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rosestatic BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
120ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  // FIXME: This should probably be part of BinaryOperator, since this isn't
121846eabd187be4bfe992e8bca131166b734d86e0dTed Kremenek  // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.)
122ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  switch (op) {
123ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  default:
124b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie    llvm_unreachable("Invalid opcode.");
1252de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_LT: return BO_GE;
1262de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_GT: return BO_LE;
1272de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_LE: return BO_GT;
1282de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_GE: return BO_LT;
1292de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_EQ: return BO_NE;
1302de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_NE: return BO_EQ;
131ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  }
132ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose}
133ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
1343cdf584e068056540769dab56cad333e95a89750Anna Zaks
1351d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseProgramStateRef
1361d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseSimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
1371d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose                                            SymbolRef Sym, bool Assumption) {
1381d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  BasicValueFactory &BVF = getBasicVals();
1391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  QualType T = Sym->getType(BVF.getContext());
1401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  const llvm::APSInt &zero = BVF.getValue(0, T);
1413cdf584e068056540769dab56cad333e95a89750Anna Zaks  if (Assumption)
1423cdf584e068056540769dab56cad333e95a89750Anna Zaks    return assumeSymNE(State, Sym, zero, zero);
1433cdf584e068056540769dab56cad333e95a89750Anna Zaks  else
1443cdf584e068056540769dab56cad333e95a89750Anna Zaks    return assumeSymEQ(State, Sym, zero, zero);
1453cdf584e068056540769dab56cad333e95a89750Anna Zaks}
1463cdf584e068056540769dab56cad333e95a89750Anna Zaks
1478bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
148a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek                                                  NonLoc Cond,
149a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek                                                  bool Assumption) {
1501eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
1513cdf584e068056540769dab56cad333e95a89750Anna Zaks  // We cannot reason about SymSymExprs, and can only reason about some
1523cdf584e068056540769dab56cad333e95a89750Anna Zaks  // SymIntExprs.
153a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu  if (!canReasonAbout(Cond)) {
1543cdf584e068056540769dab56cad333e95a89750Anna Zaks    // Just add the constraint to the expression without trying to simplify.
1553cdf584e068056540769dab56cad333e95a89750Anna Zaks    SymbolRef sym = Cond.getAsSymExpr();
1563cdf584e068056540769dab56cad333e95a89750Anna Zaks    return assumeAuxForSymbol(state, sym, Assumption);
1571eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump  }
158a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu
1591d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  BasicValueFactory &BasicVals = getBasicVals();
1604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  switch (Cond.getSubKind()) {
1624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  default:
163b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie    llvm_unreachable("'Assume' not implemented for this NonLoc");
1644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  case nonloc::SymbolValKind: {
1664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
1674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    SymbolRef sym = SV.getSymbol();
1683cdf584e068056540769dab56cad333e95a89750Anna Zaks    assert(sym);
1693cdf584e068056540769dab56cad333e95a89750Anna Zaks
1705344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks    // Handle SymbolData.
1715344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks    if (!SV.isExpression()) {
1723cdf584e068056540769dab56cad333e95a89750Anna Zaks      return assumeAuxForSymbol(state, sym, Assumption);
173ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
1745344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks    // Handle symbolic expression.
1755344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks    } else {
1765344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks      // We can only simplify expressions whose RHS is an integer.
1775344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks      const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
1785344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks      if (!SE)
1795344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks        return assumeAuxForSymbol(state, sym, Assumption);
1805344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks
1815344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks      BinaryOperator::Opcode op = SE->getOpcode();
1825344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks      // Implicitly compare non-comparison expressions to 0.
1835344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks      if (!BinaryOperator::isComparisonOp(op)) {
1841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        QualType T = SE->getType(BasicVals.getContext());
1855344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks        const llvm::APSInt &zero = BasicVals.getValue(0, T);
1865344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks        op = (Assumption ? BO_NE : BO_EQ);
1875344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks        return assumeSymRel(state, SE, op, zero);
1885344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks      }
1895344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks      // From here on out, op is the real comparison we'll be testing.
1905344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks      if (!Assumption)
1915344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks        op = NegateComparison(op);
192ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
1935344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks      return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
1945344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks    }
195e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek  }
1964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
1974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  case nonloc::ConcreteIntKind: {
1984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek    bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
199a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek    bool isFeasible = b ? Assumption : !Assumption;
200a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek    return isFeasible ? state : NULL;
2014502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  }
2024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  case nonloc::LocAsIntegerKind:
20428f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek    return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
205a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek                     Assumption);
2064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  } // end switch
2074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
2084502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2091d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rosestatic void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
2101d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Is it a "($sym+constant1)" expression?
2111d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
2121d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    BinaryOperator::Opcode Op = SE->getOpcode();
2131d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    if (Op == BO_Add || Op == BO_Sub) {
2141d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      Sym = SE->getLHS();
2151d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
2161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
2171d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      // Don't forget to negate the adjustment if it's being subtracted.
2181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      // This should happen /after/ promotion, in case the value being
2191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
2201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose      if (Op == BO_Sub)
2211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose        Adjustment = -Adjustment;
2221d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose    }
22376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks  }
22476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks}
22576462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks
2268bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state,
227ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                                     const SymExpr *LHS,
228ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                                     BinaryOperator::Opcode op,
229ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose                                                     const llvm::APSInt& Int) {
230ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  assert(BinaryOperator::isComparisonOp(op) &&
231ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose         "Non-comparison ops should be rewritten as comparisons to zero.");
232ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
2331d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  BasicValueFactory &BVF = getBasicVals();
2341d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  ASTContext &Ctx = BVF.getContext();
2351d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
2361d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Get the type used for calculating wraparound.
2371d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType(Ctx));
2381d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
23976462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks  // We only handle simple comparisons of the form "$sym == constant"
24076462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks  // or "($sym+constant1) == constant2".
24176462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks  // The adjustment is "constant1" in the above expression. It's used to
24276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks  // "slide" the solution range around for modular arithmetic. For example,
24376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks  // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
24476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks  // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
24576462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks  // the subclasses of SimpleConstraintManager to handle the adjustment.
24676462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks  SymbolRef Sym = LHS;
2471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
2481d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  computeAdjustment(Sym, Adjustment);
2491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose
2501d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  // Convert the right-hand side integer as necessary.
2511d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
2521d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose  llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
253b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose
254ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose  switch (op) {
2554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  default:
25628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek    // No logic yet for other operators.  assume the constraint is feasible.
257a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek    return state;
2584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2592de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_EQ:
26028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek    return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);
2614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2622de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_NE:
26328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek    return assumeSymNE(state, Sym, ConvertedInt, Adjustment);
264ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose
2652de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_GT:
26628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek    return assumeSymGT(state, Sym, ConvertedInt, Adjustment);
2674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2682de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_GE:
26928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek    return assumeSymGE(state, Sym, ConvertedInt, Adjustment);
2704502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2712de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_LT:
27228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek    return assumeSymLT(state, Sym, ConvertedInt, Adjustment);
2731eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump
2742de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall  case BO_LE:
27528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek    return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
2764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek  } // end switch
2774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek}
2784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek
2799ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenek} // end of namespace ento
2805a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis
2815a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end of namespace clang
282