SimpleConstraintManager.cpp revision 5b9bd2137ebef350af803c634e3fdf5d74678100
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" 164502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "clang/Analysis/PathSensitive/GRExprEngine.h" 174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "clang/Analysis/PathSensitive/GRState.h" 184502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang { 204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 214502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::~SimpleConstraintManager() {} 224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2366b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenekbool SimpleConstraintManager::canReasonAbout(SVal X) const { 24e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) { 25e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek const SymExpr *SE = SymVal->getSymbolicExpression(); 261eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 27e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (isa<SymbolData>(SE)) 28e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return true; 291eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 30e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) { 31e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek switch (SIE->getOpcode()) { 32e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // We don't reason yet about bitwise-constraints on symbolic values. 33e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::And: 34e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Or: 35e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Xor: 36e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 37e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // We don't reason yet about arithmetic constraints on symbolic values. 38e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Mul: 39e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Div: 40e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Rem: 41e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Add: 42e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Sub: 43e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Shl: 44e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::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 58a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::Assume(const GRState *state, 595b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek DefinedSVal Cond, 605b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek bool Assumption) { 614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (isa<NonLoc>(Cond)) 62a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assume(state, cast<NonLoc>(Cond), Assumption); 634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek else 64a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assume(state, cast<Loc>(Cond), Assumption); 654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 67a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::Assume(const GRState *state, Loc Cond, 68a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 69a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek 70a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek state = AssumeAux(state, Cond, Assumption); 71a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek 724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // EvalAssume is used to call into the GRTransferFunction object to perform 734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // any checker-specific update of the state based on this assumption being 741eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump // true or false. 75a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state ? state->getTransferFuncs().EvalAssume(state, Cond, Assumption) 76a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek : NULL; 774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 79a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::AssumeAux(const GRState *state, 80a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Loc Cond, bool Assumption) { 811eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 82a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicValueFactory &BasicVals = state->getBasicVals(); 834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert (false && "'Assume' not implemented for this Loc."); 87a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 884502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::MemRegionKind: { 904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: Should this go into the storemanager? 911eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 92a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion(); 93a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const SubRegion *SubR = dyn_cast<SubRegion>(R); 944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek while (SubR) { 964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: now we only find the first symbolic region. 97a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { 983330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu if (Assumption) 991eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump return AssumeSymNE(state, SymR->getSymbol(), 100a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicVals.getZeroWithPtrWidth()); 1013330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu else 102a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return AssumeSymEQ(state, SymR->getSymbol(), 103a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicVals.getZeroWithPtrWidth()); 1043330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu } 1054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 1064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1071eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1084502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FALL-THROUGH. 1094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1101eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::GotoLabelKind: 112a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? state : NULL; 1134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::ConcreteIntKind: { 1151eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; 116a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 117a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1184502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 122a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::Assume(const GRState *state, 123a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek NonLoc Cond, 124a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 125a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek 126a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek state = AssumeAux(state, Cond, Assumption); 127a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek 1284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // EvalAssume is used to call into the GRTransferFunction object to perform 1294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // any checker-specific update of the state based on this assumption being 1301eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump // true or false. 131a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state ? state->getTransferFuncs().EvalAssume(state, Cond, Assumption) 132a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek : NULL; 1334502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1344502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 135a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::AssumeAux(const GRState *state, 136a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek NonLoc Cond, 137a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 1381eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 139a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu // We cannot reason about SymIntExpr and SymSymExpr. 140a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu if (!canReasonAbout(Cond)) { 141a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // Just return the current state indicating that the path is feasible. 142a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // This may be an over-approximation of what is possible. 143a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 1441eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 145a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu 146a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicValueFactory &BasicVals = state->getBasicVals(); 147a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek SymbolManager &SymMgr = state->getSymbolManager(); 1484502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 1504502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 1514502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert(false && "'Assume' not implemented for this NonLoc"); 1524502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::SymbolValKind: { 1544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); 1554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym = SV.getSymbol(); 1561eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump QualType T = SymMgr.getType(sym); 157a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const llvm::APSInt &zero = BasicVals.getValue(0, T); 158a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek 159a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? AssumeSymNE(state, sym, zero) 160a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek : AssumeSymEQ(state, sym, zero); 1614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 163e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case nonloc::SymExprValKind: { 164e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond); 165e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression())) 166a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return AssumeSymInt(state, Assumption, SE); 1671eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 168a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // For all other symbolic expressions, over-approximate and consider 169a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // the constraint feasible. 170a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 171e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 1724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::ConcreteIntKind: { 1744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; 175a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 176a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::LocAsIntegerKind: 180a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return AssumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), 181a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Assumption); 1824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 185a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::AssumeSymInt(const GRState *state, 186a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption, 187a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const SymIntExpr *SE) { 188e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek 1894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 190e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // Here we assume that LHS is a symbol. This is consistent with the 191e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // rest of the constraint manager logic. 192e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek SymbolRef Sym = cast<SymbolData>(SE->getLHS()); 193e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek const llvm::APSInt &Int = SE->getRHS(); 1941eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 195e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek switch (SE->getOpcode()) { 1964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 197a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // No logic yet for other operators. Assume the constraint is feasible. 198a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 1994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::EQ: 201a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? AssumeSymEQ(state, Sym, Int) 202a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek : AssumeSymNE(state, Sym, Int); 2034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::NE: 205a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? AssumeSymNE(state, Sym, Int) 206a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek : AssumeSymEQ(state, Sym, Int); 2074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::GT: 208a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? AssumeSymGT(state, Sym, Int) 209a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek : AssumeSymLE(state, Sym, Int); 2104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::GE: 212a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? AssumeSymGE(state, Sym, Int) 213a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek : AssumeSymLT(state, Sym, Int); 2144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::LT: 216a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? AssumeSymLT(state, Sym, Int) 217a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek : AssumeSymGE(state, Sym, Int); 2181eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::LE: 220a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? AssumeSymLE(state, Sym, Int) 221a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek : AssumeSymGT(state, Sym, Int); 2224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2234502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 225a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::AssumeInBound(const GRState *state, 2265b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek DefinedSVal Idx, 2275b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek DefinedSVal UpperBound, 2281eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump bool Assumption) { 229a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek 2304502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // Only support ConcreteInt for now. 231a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound))) 232a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 2334502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 234f1b8227d758721075e3a84a85e66cb7173334b13Ted Kremenek const llvm::APSInt& Zero = state->getBasicVals().getZeroWithPtrWidth(false); 2354502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue(); 2364502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // IdxV might be too narrow. 2374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (IdxV.getBitWidth() < Zero.getBitWidth()) 2384502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek IdxV.extend(Zero.getBitWidth()); 2394502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // UBV might be too narrow, too. 2404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue(); 2414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (UBV.getBitWidth() < Zero.getBitWidth()) 2424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek UBV.extend(Zero.getBitWidth()); 2434502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool InBound = (Zero <= IdxV) && (IdxV < UBV); 245a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = Assumption ? InBound : !InBound; 246a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 2474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2484502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} // end of namespace clang 250