SimpleConstraintManager.cpp revision 32a58084a4c53e6938dd81bfce224db25a5976d1
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" 18b94b81a9ab46c99b00c7ad28c5e1e212c63fc9acZhongxing Xu#include "clang/Analysis/PathSensitive/Checker.h" 194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang { 214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 224502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::~SimpleConstraintManager() {} 234502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2466b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenekbool SimpleConstraintManager::canReasonAbout(SVal X) const { 25e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) { 26e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek const SymExpr *SE = SymVal->getSymbolicExpression(); 271eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 28e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (isa<SymbolData>(SE)) 29e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return true; 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. 34e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::And: 35e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Or: 36e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Xor: 37e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 38e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // We don't reason yet about arithmetic constraints on symbolic values. 39e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Mul: 40e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Div: 41e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Rem: 42e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Add: 43e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Sub: 44e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Shl: 45e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Shr: 46e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 47e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // All other cases. 48e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek default: 49e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return true; 501eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 51e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 52e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek 53e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 547de20fe9aac00705dd943690563db66fa4b35b5bTed Kremenek } 557de20fe9aac00705dd943690563db66fa4b35b5bTed Kremenek 5666b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek return true; 5766b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek} 581eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 59a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::Assume(const GRState *state, 605b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek DefinedSVal Cond, 615b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek bool Assumption) { 624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (isa<NonLoc>(Cond)) 63a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assume(state, cast<NonLoc>(Cond), Assumption); 644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek else 65a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assume(state, cast<Loc>(Cond), Assumption); 664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 6832a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenekconst GRState *SimpleConstraintManager::Assume(const GRState *state, Loc cond, 6932a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 7032a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek state = AssumeAux(state, cond, assumption); 7132a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek return SU.ProcessAssume(state, cond, assumption); 724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 74a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::AssumeAux(const GRState *state, 75a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Loc Cond, bool Assumption) { 761eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 77a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicValueFactory &BasicVals = state->getBasicVals(); 784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert (false && "'Assume' not implemented for this Loc."); 82a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::MemRegionKind: { 854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: Should this go into the storemanager? 861eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 87a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion(); 88a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const SubRegion *SubR = dyn_cast<SubRegion>(R); 894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek while (SubR) { 914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: now we only find the first symbolic region. 92a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { 933330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu if (Assumption) 941eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump return AssumeSymNE(state, SymR->getSymbol(), 95a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicVals.getZeroWithPtrWidth()); 963330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu else 97a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return AssumeSymEQ(state, SymR->getSymbol(), 98a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicVals.getZeroWithPtrWidth()); 993330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu } 1004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 1014502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1021eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FALL-THROUGH. 1044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1051eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::GotoLabelKind: 107a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? state : NULL; 1084502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::ConcreteIntKind: { 1101eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; 111a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 112a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1164502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 117a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::Assume(const GRState *state, 11832a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek NonLoc cond, 11932a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 12032a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek state = AssumeAux(state, cond, assumption); 12132a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek return SU.ProcessAssume(state, cond, assumption); 1224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1234502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 124a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::AssumeAux(const GRState *state, 125a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek NonLoc Cond, 126a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 1271eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 128a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu // We cannot reason about SymIntExpr and SymSymExpr. 129a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu if (!canReasonAbout(Cond)) { 130a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // Just return the current state indicating that the path is feasible. 131a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // This may be an over-approximation of what is possible. 132a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 1331eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 134a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu 135a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicValueFactory &BasicVals = state->getBasicVals(); 136a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek SymbolManager &SymMgr = state->getSymbolManager(); 1374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1384502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 1394502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 1404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert(false && "'Assume' not implemented for this NonLoc"); 1414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::SymbolValKind: { 1434502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); 1444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym = SV.getSymbol(); 1451eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump QualType T = SymMgr.getType(sym); 146a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const llvm::APSInt &zero = BasicVals.getValue(0, T); 147a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek 148a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? AssumeSymNE(state, sym, zero) 149a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek : AssumeSymEQ(state, sym, zero); 1504502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1514502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 152e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case nonloc::SymExprValKind: { 153e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond); 15480417471b01ab2726cd04773b2ab700ce564073cTed Kremenek if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression())){ 15580417471b01ab2726cd04773b2ab700ce564073cTed Kremenek // FIXME: This is a hack. It silently converts the RHS integer to be 15680417471b01ab2726cd04773b2ab700ce564073cTed Kremenek // of the same type as on the left side. This should be removed once 15780417471b01ab2726cd04773b2ab700ce564073cTed Kremenek // we support truncation/extension of symbolic values. 15880417471b01ab2726cd04773b2ab700ce564073cTed Kremenek GRStateManager &StateMgr = state->getStateManager(); 15980417471b01ab2726cd04773b2ab700ce564073cTed Kremenek ASTContext &Ctx = StateMgr.getContext(); 16080417471b01ab2726cd04773b2ab700ce564073cTed Kremenek QualType LHSType = SE->getLHS()->getType(Ctx); 16180417471b01ab2726cd04773b2ab700ce564073cTed Kremenek BasicValueFactory &BasicVals = StateMgr.getBasicVals(); 16280417471b01ab2726cd04773b2ab700ce564073cTed Kremenek const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS()); 16380417471b01ab2726cd04773b2ab700ce564073cTed Kremenek SymIntExpr SENew(SE->getLHS(), SE->getOpcode(), RHS, SE->getType(Ctx)); 16480417471b01ab2726cd04773b2ab700ce564073cTed Kremenek 16580417471b01ab2726cd04773b2ab700ce564073cTed Kremenek return AssumeSymInt(state, Assumption, &SENew); 16680417471b01ab2726cd04773b2ab700ce564073cTed Kremenek } 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