SimpleConstraintManager.cpp revision b219cfc4d75f0a03630b7c4509ef791b7e97b2c8
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" 169b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" 1718c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 184502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang { 204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 219ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento { 225a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 234502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::~SimpleConstraintManager() {} 244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2566b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenekbool SimpleConstraintManager::canReasonAbout(SVal X) const { 26e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) { 27e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek const SymExpr *SE = SymVal->getSymbolicExpression(); 281eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 29e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (isa<SymbolData>(SE)) 30e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return true; 311eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 32e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) { 33e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek switch (SIE->getOpcode()) { 34e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // We don't reason yet about bitwise-constraints on symbolic values. 352de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_And: 362de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Or: 372de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Xor: 38e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 39ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't reason yet about these arithmetic constraints on 40ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // symbolic values. 412de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Mul: 422de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Div: 432de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Rem: 442de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Shl: 452de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_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 5918c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assume(const ProgramState *state, 605b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek DefinedSVal Cond, 615b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek bool Assumption) { 624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (isa<NonLoc>(Cond)) 6328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assume(state, cast<NonLoc>(Cond), Assumption); 644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek else 6528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assume(state, cast<Loc>(Cond), Assumption); 664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 6818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assume(const ProgramState *state, Loc cond, 6932a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 7028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 71e36de1fe51c39d9161915dd3dbef880954af6476Ted Kremenek return SU.processAssume(state, cond, assumption); 724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 7418c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *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)) { 93ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth(); 943330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu if (Assumption) 9528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, SymR->getSymbol(), zero, zero); 963330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu else 9728f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, SymR->getSymbol(), zero, zero); 983330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu } 994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 1004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1011eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FALL-THROUGH. 1034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1041eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::GotoLabelKind: 106a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? state : NULL; 1074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1084502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::ConcreteIntKind: { 1091eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; 110a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 111a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 11618c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assume(const ProgramState *state, 11732a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek NonLoc cond, 11832a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 11928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 120e36de1fe51c39d9161915dd3dbef880954af6476Ted Kremenek return SU.processAssume(state, cond, assumption); 1214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 123ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rosestatic BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) { 124ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // FIXME: This should probably be part of BinaryOperator, since this isn't 125846eabd187be4bfe992e8bca131166b734d86e0dTed Kremenek // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.) 126ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 127ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose default: 128b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie llvm_unreachable("Invalid opcode."); 1292de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LT: return BO_GE; 1302de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GT: return BO_LE; 1312de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LE: return BO_GT; 1322de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GE: return BO_LT; 1332de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_EQ: return BO_NE; 1342de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_NE: return BO_EQ; 135ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 136ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 137ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 13818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state, 139a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek NonLoc Cond, 140a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 1411eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 142ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We cannot reason about SymSymExprs, 143ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // and can only reason about some SymIntExprs. 144a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu if (!canReasonAbout(Cond)) { 145a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // Just return the current state indicating that the path is feasible. 146a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek // This may be an over-approximation of what is possible. 147a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 1481eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 149a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu 150a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicValueFactory &BasicVals = state->getBasicVals(); 151a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek SymbolManager &SymMgr = state->getSymbolManager(); 1524502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 1544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 155b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie llvm_unreachable("'Assume' not implemented for this NonLoc"); 1564502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1574502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::SymbolValKind: { 1584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); 1594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym = SV.getSymbol(); 1601eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump QualType T = SymMgr.getType(sym); 161a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const llvm::APSInt &zero = BasicVals.getValue(0, T); 162ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (Assumption) 16328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, sym, zero, zero); 164ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose else 16528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, sym, zero, zero); 1664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 168e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case nonloc::SymExprValKind: { 169e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond); 1701eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 171ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // For now, we only handle expressions whose RHS is an integer. 172ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // All other expressions are assumed to be feasible. 173ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression()); 174ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!SE) 175ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 176ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 177ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op = SE->getOpcode(); 1785ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose // Implicitly compare non-comparison expressions to 0. 1795ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose if (!BinaryOperator::isComparisonOp(op)) { 1805ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose QualType T = SymMgr.getType(SE); 1815ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose const llvm::APSInt &zero = BasicVals.getValue(0, T); 1822de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall op = (Assumption ? BO_NE : BO_EQ); 18328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymRel(state, SE, op, zero); 1845ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose } 185ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 186ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // From here on out, op is the real comparison we'll be testing. 187ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!Assumption) 188ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose op = NegateComparison(op); 189ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 19028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 191e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 1924502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1934502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::ConcreteIntKind: { 1944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; 195a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 196a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::LocAsIntegerKind: 20028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), 201a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Assumption); 2024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 20518c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assumeSymRel(const ProgramState *state, 206ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymExpr *LHS, 207ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op, 208ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int) { 209ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose assert(BinaryOperator::isComparisonOp(op) && 210ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose "Non-comparison ops should be rewritten as comparisons to zero."); 211ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 212ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We only handle simple comparisons of the form "$sym == constant" 213ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // or "($sym+constant1) == constant2". 214ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // The adjustment is "constant1" in the above expression. It's used to 215ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // "slide" the solution range around for modular arithmetic. For example, 216ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 217ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 218ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // the subclasses of SimpleConstraintManager to handle the adjustment. 219b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose llvm::APSInt Adjustment; 220ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 221ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // First check if the LHS is a simple symbol reference. 222ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose SymbolRef Sym = dyn_cast<SymbolData>(LHS); 223b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose if (Sym) { 224b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose Adjustment = 0; 225b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose } else { 226ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Next, see if it's a "($sym+constant1)" expression. 227ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS); 228ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 229ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't handle "($sym1+$sym2)". 230ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Give up and assume the constraint is feasible. 231ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!SE) 232ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 233ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 234ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't handle "(<expr>+constant1)". 235ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Give up and assume the constraint is feasible. 236ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose Sym = dyn_cast<SymbolData>(SE->getLHS()); 237ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!Sym) 238ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 239ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 240ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Get the constant out of the expression "($sym+constant1)". 241ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (SE->getOpcode()) { 2422de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Add: 243ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose Adjustment = SE->getRHS(); 244ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose break; 2452de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Sub: 246ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose Adjustment = -SE->getRHS(); 247ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose break; 248ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose default: 249ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't handle non-additive operators. 250ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // Give up and assume the constraint is feasible. 251ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose return state; 252ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 253ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 2541eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 255b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // FIXME: This next section is a hack. It silently converts the integers to 256b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // be of the same type as the symbol, which is not always correct. Really the 257b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // comparisons should be performed using the Int's type, then mapped back to 258b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // the symbol's range of values. 25918c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek ProgramStateManager &StateMgr = state->getStateManager(); 260b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose ASTContext &Ctx = StateMgr.getContext(); 261b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 262b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose QualType T = Sym->getType(Ctx); 2637dfc9420babe83e236a47e752f8723bd06070d9dZhanyong Wan assert(T->isIntegerType() || Loc::isLocType(T)); 264b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose unsigned bitwidth = Ctx.getTypeSize(T); 2655e9ebb3c0fb554d9285aa99c470abdf283272bd9Douglas Gregor bool isSymUnsigned 2665e9ebb3c0fb554d9285aa99c470abdf283272bd9Douglas Gregor = T->isUnsignedIntegerOrEnumerationType() || Loc::isLocType(T); 267b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 268b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // Convert the adjustment. 269b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose Adjustment.setIsUnsigned(isSymUnsigned); 2709f71a8f4c7a182a5236da9e747d57cc1d1bd24c2Jay Foad Adjustment = Adjustment.extOrTrunc(bitwidth); 271b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 272b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // Convert the right-hand side integer. 273b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose llvm::APSInt ConvertedInt(Int, isSymUnsigned); 2749f71a8f4c7a182a5236da9e747d57cc1d1bd24c2Jay Foad ConvertedInt = ConvertedInt.extOrTrunc(bitwidth); 275b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 276ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 2774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 27828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek // No logic yet for other operators. assume the constraint is feasible. 279a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 2804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2812de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_EQ: 28228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 2834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2842de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_NE: 28528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 286ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2872de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GT: 28828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 2894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2902de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GE: 29128f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 2924502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2932de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LT: 29428f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 2951eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2962de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LE: 29728f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 2984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 3004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3019ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenek} // end of namespace ento 3025a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 3035a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end of namespace clang 304