SimpleConstraintManager.cpp revision 28f47b92e760ccf641ac91cb0fe1c12d9ca89795
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" 161309f9a3b225ea846e5822691c39a77423125505Ted Kremenek#include "clang/Checker/PathSensitive/GRExprEngine.h" 171309f9a3b225ea846e5822691c39a77423125505Ted Kremenek#include "clang/Checker/PathSensitive/GRState.h" 181309f9a3b225ea846e5822691c39a77423125505Ted Kremenek#include "clang/Checker/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. 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 5828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenekconst GRState *SimpleConstraintManager::assume(const GRState *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 6728f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenekconst GRState *SimpleConstraintManager::assume(const GRState *state, Loc cond, 6832a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 6928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 7032a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek return SU.ProcessAssume(state, cond, assumption); 714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 7328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenekconst GRState *SimpleConstraintManager::assumeAux(const GRState *state, 74a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Loc Cond, bool Assumption) { 751eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 76a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicValueFactory &BasicVals = state->getBasicVals(); 774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert (false && "'Assume' not implemented for this Loc."); 81a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::MemRegionKind: { 844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: Should this go into the storemanager? 851eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 86a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion(); 87a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const SubRegion *SubR = dyn_cast<SubRegion>(R); 884502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek while (SubR) { 904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: now we only find the first symbolic region. 91a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { 92ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth(); 933330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu if (Assumption) 9428f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, SymR->getSymbol(), zero, zero); 953330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu else 9628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, SymR->getSymbol(), zero, zero); 973330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu } 984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1001eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1014502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FALL-THROUGH. 1024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1031eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::GotoLabelKind: 105a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? state : NULL; 1064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::ConcreteIntKind: { 1081eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; 109a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 110a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 11528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenekconst GRState *SimpleConstraintManager::assume(const GRState *state, 11632a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek NonLoc cond, 11732a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 11828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 11932a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek return SU.ProcessAssume(state, cond, assumption); 1204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 122ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rosestatic BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) { 123ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // FIXME: This should probably be part of BinaryOperator, since this isn't 124846eabd187be4bfe992e8bca131166b734d86e0dTed Kremenek // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.) 125ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 126ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose default: 127ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose assert(false && "Invalid opcode."); 1282de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LT: return BO_GE; 1292de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GT: return BO_LE; 1302de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LE: return BO_GT; 1312de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GE: return BO_LT; 1322de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_EQ: return BO_NE; 1332de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_NE: return BO_EQ; 134ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 135ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 136ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 13728f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenekconst GRState *SimpleConstraintManager::assumeAux(const GRState *state, 138a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek NonLoc Cond, 139a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 1401eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 141ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We cannot reason about SymSymExprs, 142ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // and can only reason about some SymIntExprs. 143a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu if (!canReasonAbout(Cond)) { 144a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // Just return the current state indicating that the path is feasible. 145a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // This may be an over-approximation of what is possible. 146a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 1471eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 148a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu 149a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicValueFactory &BasicVals = state->getBasicVals(); 150a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek SymbolManager &SymMgr = state->getSymbolManager(); 1514502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1524502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 1534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 1544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert(false && "'Assume' not implemented for this NonLoc"); 1554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1564502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::SymbolValKind: { 1574502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); 1584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym = SV.getSymbol(); 1591eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump QualType T = SymMgr.getType(sym); 160a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const llvm::APSInt &zero = BasicVals.getValue(0, T); 161ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (Assumption) 16228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, sym, zero, zero); 163ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose else 16428f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, sym, zero, zero); 1654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 167e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case nonloc::SymExprValKind: { 168e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond); 1691eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 170ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // For now, we only handle expressions whose RHS is an integer. 171ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // All other expressions are assumed to be feasible. 172ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression()); 173ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!SE) 174ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 175ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 176ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op = SE->getOpcode(); 1775ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose // Implicitly compare non-comparison expressions to 0. 1785ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose if (!BinaryOperator::isComparisonOp(op)) { 1795ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose QualType T = SymMgr.getType(SE); 1805ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose const llvm::APSInt &zero = BasicVals.getValue(0, T); 1812de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall op = (Assumption ? BO_NE : BO_EQ); 18228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymRel(state, SE, op, zero); 1835ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose } 184ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 185ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // From here on out, op is the real comparison we'll be testing. 186ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!Assumption) 187ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose op = NegateComparison(op); 188ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 18928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 190e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 1914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1924502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::ConcreteIntKind: { 1934502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; 194a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 195a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::LocAsIntegerKind: 19928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), 200a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Assumption); 2014502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 20428f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenekconst GRState *SimpleConstraintManager::assumeSymRel(const GRState *state, 205ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymExpr *LHS, 206ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op, 207ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int) { 208ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose assert(BinaryOperator::isComparisonOp(op) && 209ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose "Non-comparison ops should be rewritten as comparisons to zero."); 210ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 211ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We only handle simple comparisons of the form "$sym == constant" 212ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // or "($sym+constant1) == constant2". 213ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // The adjustment is "constant1" in the above expression. It's used to 214ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // "slide" the solution range around for modular arithmetic. For example, 215ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 216ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 217ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // the subclasses of SimpleConstraintManager to handle the adjustment. 218b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose llvm::APSInt Adjustment; 219ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 220ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // First check if the LHS is a simple symbol reference. 221ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose SymbolRef Sym = dyn_cast<SymbolData>(LHS); 222b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose if (Sym) { 223b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose Adjustment = 0; 224b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose } else { 225ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Next, see if it's a "($sym+constant1)" expression. 226ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS); 227ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 228ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't handle "($sym1+$sym2)". 229ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Give up and assume the constraint is feasible. 230ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!SE) 231ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 232ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 233ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't handle "(<expr>+constant1)". 234ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Give up and assume the constraint is feasible. 235ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose Sym = dyn_cast<SymbolData>(SE->getLHS()); 236ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!Sym) 237ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 238ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 239ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Get the constant out of the expression "($sym+constant1)". 240ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (SE->getOpcode()) { 2412de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Add: 242ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose Adjustment = SE->getRHS(); 243ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose break; 2442de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Sub: 245ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose Adjustment = -SE->getRHS(); 246ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose break; 247ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose default: 248ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't handle non-additive operators. 249ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Give up and assume the constraint is feasible. 250ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 251ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 252ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 2531eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 254b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // FIXME: This next section is a hack. It silently converts the integers to 255b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // be of the same type as the symbol, which is not always correct. Really the 256b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // comparisons should be performed using the Int's type, then mapped back to 257b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // the symbol's range of values. 258b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose GRStateManager &StateMgr = state->getStateManager(); 259b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose ASTContext &Ctx = StateMgr.getContext(); 260b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 261b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose QualType T = Sym->getType(Ctx); 262b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose assert(T->isIntegerType() || Loc::IsLocType(T)); 263b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose unsigned bitwidth = Ctx.getTypeSize(T); 264b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose bool isSymUnsigned = T->isUnsignedIntegerType() || Loc::IsLocType(T); 265b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 266b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // Convert the adjustment. 267b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose Adjustment.setIsUnsigned(isSymUnsigned); 268b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose Adjustment.extOrTrunc(bitwidth); 269b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 270b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // Convert the right-hand side integer. 271b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose llvm::APSInt ConvertedInt(Int, isSymUnsigned); 272b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose ConvertedInt.extOrTrunc(bitwidth); 273b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 274ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 2754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 27628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek // No logic yet for other operators. assume the constraint is feasible. 277a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 2784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2792de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_EQ: 28028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 2814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2822de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_NE: 28328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 284ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2852de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GT: 28628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 2874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2882de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GE: 28928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 2904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2912de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LT: 29228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 2931eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2942de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LE: 29528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 2964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} // end of namespace clang 300