SimpleConstraintManager.cpp revision b4954a4175b36d912bdfc43834d09754faddd855
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. 34e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::And: 35e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Or: 36e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Xor: 37e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 38ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't reason yet about these arithmetic constraints on 39ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // symbolic values. 40e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Mul: 41e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Div: 42e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Rem: 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 6732a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenekconst GRState *SimpleConstraintManager::Assume(const GRState *state, Loc cond, 6832a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 6932a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek state = AssumeAux(state, cond, assumption); 7032a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek return SU.ProcessAssume(state, cond, assumption); 714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 73a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted 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) 94ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return AssumeSymNE(state, SymR->getSymbol(), zero, zero); 953330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu else 96ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 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 115a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::Assume(const GRState *state, 11632a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek NonLoc cond, 11732a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 11832a58084a4c53e6938dd81bfce224db25a5976d1Ted 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 124ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // the only place it's used. (This code was copied from SimpleSValuator.cpp.) 125ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 126ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose default: 127ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose assert(false && "Invalid opcode."); 128ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose case BinaryOperator::LT: return BinaryOperator::GE; 129ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose case BinaryOperator::GT: return BinaryOperator::LE; 130ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose case BinaryOperator::LE: return BinaryOperator::GT; 131ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose case BinaryOperator::GE: return BinaryOperator::LT; 132ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose case BinaryOperator::EQ: return BinaryOperator::NE; 133ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose case BinaryOperator::NE: return BinaryOperator::EQ; 134ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 135ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 136ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 137a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted 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) 162ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return AssumeSymNE(state, sym, zero, zero); 163ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose else 164ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 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(); 177ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // FIXME: We should implicitly compare non-comparison expressions to 0. 178ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!BinaryOperator::isComparisonOp(op)) 179ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 180ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 181ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // From here on out, op is the real comparison we'll be testing. 182ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!Assumption) 183ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose op = NegateComparison(op); 184ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 185b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose return AssumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 186e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 1874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1884502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::ConcreteIntKind: { 1894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; 190a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 191a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1924502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1934502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::LocAsIntegerKind: 195a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return AssumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), 196a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Assumption); 1974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 200ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Roseconst GRState *SimpleConstraintManager::AssumeSymRel(const GRState *state, 201ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymExpr *LHS, 202ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op, 203ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int) { 204ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose assert(BinaryOperator::isComparisonOp(op) && 205ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose "Non-comparison ops should be rewritten as comparisons to zero."); 206ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 207ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We only handle simple comparisons of the form "$sym == constant" 208ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // or "($sym+constant1) == constant2". 209ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // The adjustment is "constant1" in the above expression. It's used to 210ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // "slide" the solution range around for modular arithmetic. For example, 211ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 212ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 213ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // the subclasses of SimpleConstraintManager to handle the adjustment. 214b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose llvm::APSInt Adjustment; 215ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 216ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // First check if the LHS is a simple symbol reference. 217ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose SymbolRef Sym = dyn_cast<SymbolData>(LHS); 218b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose if (Sym) { 219b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose Adjustment = 0; 220b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose } else { 221ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Next, see if it's a "($sym+constant1)" expression. 222ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS); 223ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 224ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't handle "($sym1+$sym2)". 225ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Give up and assume the constraint is feasible. 226ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!SE) 227ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 228ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 229ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't handle "(<expr>+constant1)". 230ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Give up and assume the constraint is feasible. 231ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose Sym = dyn_cast<SymbolData>(SE->getLHS()); 232ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!Sym) 233ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 234ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 235ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Get the constant out of the expression "($sym+constant1)". 236ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (SE->getOpcode()) { 237ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose case BinaryOperator::Add: 238ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose Adjustment = SE->getRHS(); 239ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose break; 240ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose case BinaryOperator::Sub: 241ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose Adjustment = -SE->getRHS(); 242ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose break; 243ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose default: 244ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't handle non-additive operators. 245ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Give up and assume the constraint is feasible. 246ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 247ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 248ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 2491eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 250b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // FIXME: This next section is a hack. It silently converts the integers to 251b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // be of the same type as the symbol, which is not always correct. Really the 252b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // comparisons should be performed using the Int's type, then mapped back to 253b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // the symbol's range of values. 254b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose GRStateManager &StateMgr = state->getStateManager(); 255b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose ASTContext &Ctx = StateMgr.getContext(); 256b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 257b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose QualType T = Sym->getType(Ctx); 258b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose assert(T->isIntegerType() || Loc::IsLocType(T)); 259b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose unsigned bitwidth = Ctx.getTypeSize(T); 260b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose bool isSymUnsigned = T->isUnsignedIntegerType() || Loc::IsLocType(T); 261b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 262b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // Convert the adjustment. 263b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose Adjustment.setIsUnsigned(isSymUnsigned); 264b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose Adjustment.extOrTrunc(bitwidth); 265b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 266b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // Convert the right-hand side integer. 267b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose llvm::APSInt ConvertedInt(Int, isSymUnsigned); 268b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose ConvertedInt.extOrTrunc(bitwidth); 269b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 270ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 2714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 272a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // No logic yet for other operators. Assume the constraint is feasible. 273a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 2744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::EQ: 276b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose return AssumeSymEQ(state, Sym, ConvertedInt, Adjustment); 2774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::NE: 279b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose return AssumeSymNE(state, Sym, ConvertedInt, Adjustment); 280ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::GT: 282b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose return AssumeSymGT(state, Sym, ConvertedInt, Adjustment); 2834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::GE: 285b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose return AssumeSymGE(state, Sym, ConvertedInt, Adjustment); 2864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::LT: 288b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose return AssumeSymLT(state, Sym, ConvertedInt, Adjustment); 2891eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::LE: 291b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose return AssumeSymLE(state, Sym, ConvertedInt, Adjustment); 2924502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2934502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 295a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenekconst GRState *SimpleConstraintManager::AssumeInBound(const GRState *state, 2965b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek DefinedSVal Idx, 2975b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek DefinedSVal UpperBound, 2981eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump bool Assumption) { 299a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek 3004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // Only support ConcreteInt for now. 301a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound))) 302a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 3034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 304f1b8227d758721075e3a84a85e66cb7173334b13Ted Kremenek const llvm::APSInt& Zero = state->getBasicVals().getZeroWithPtrWidth(false); 3054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue(); 3064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // IdxV might be too narrow. 3074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (IdxV.getBitWidth() < Zero.getBitWidth()) 3084502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek IdxV.extend(Zero.getBitWidth()); 3094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // UBV might be too narrow, too. 3104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue(); 3114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (UBV.getBitWidth() < Zero.getBitWidth()) 3124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek UBV.extend(Zero.getBitWidth()); 3134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool InBound = (Zero <= IdxV) && (IdxV < UBV); 315a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = Assumption ? InBound : !InBound; 316a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 3174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 3184502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} // end of namespace clang 320