SimpleConstraintManager.cpp revision 5251abea41b446c26e3239c8dd6c7edea6fc335d
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" 161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" 179b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" 1818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang { 214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 229ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento { 235a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 244502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::~SimpleConstraintManager() {} 254502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2666b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenekbool SimpleConstraintManager::canReasonAbout(SVal X) const { 275251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie llvm::Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>(); 285344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (SymVal && SymVal->isExpression()) { 295344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks const SymExpr *SE = SymVal->getSymbol(); 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 588bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 595b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek DefinedSVal Cond, 605b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek bool Assumption) { 615251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie if (llvm::Optional<NonLoc> NV = Cond.getAs<NonLoc>()) 625251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie return assume(state, *NV, Assumption); 635251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie return assume(state, Cond.castAs<Loc>(), Assumption); 644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 668bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond, 6732a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 6828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 69ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose if (NotifyAssumeClients && SU) 70ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose return SU->processAssume(state, cond, assumption); 7147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek return state; 724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 748bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 75a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Loc Cond, bool Assumption) { 764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert (false && "'Assume' not implemented for this Loc."); 79a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::MemRegionKind: { 824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: Should this go into the storemanager? 831eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 845251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie const MemRegion *R = Cond.castAs<loc::MemRegionVal>().getRegion(); 85a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const SubRegion *SubR = dyn_cast<SubRegion>(R); 864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek while (SubR) { 88efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek // FIXME: now we only find the first symbolic region. 89efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { 90efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth(); 91efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (Assumption) 92efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek return assumeSymNE(state, SymR->getSymbol(), zero, zero); 93efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek else 94efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek return assumeSymEQ(state, SymR->getSymbol(), zero, zero); 95efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek } 964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 981eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FALL-THROUGH. 1004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1011eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::GotoLabelKind: 103a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? state : NULL; 1044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::ConcreteIntKind: { 1065251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie bool b = Cond.castAs<loc::ConcreteInt>().getValue() != 0; 107a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 108a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1138bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 11432a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek NonLoc cond, 11532a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 11628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 117ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose if (NotifyAssumeClients && SU) 118ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose return SU->processAssume(state, cond, assumption); 11905c3b9ac74e12238e7ec5f237132e2348a8b5f4eAnna Zaks return state; 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: 127b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie llvm_unreachable("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 1373cdf584e068056540769dab56cad333e95a89750Anna Zaks 1381d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseProgramStateRef 1391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseSimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State, 1401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose SymbolRef Sym, bool Assumption) { 1411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BasicValueFactory &BVF = getBasicVals(); 142732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek QualType T = Sym->getType(); 143b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks 144efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek // None of the constraint solvers currently support non-integer types. 145efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (!T->isIntegerType()) 146b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks return State; 147b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks 1481d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &zero = BVF.getValue(0, T); 1493cdf584e068056540769dab56cad333e95a89750Anna Zaks if (Assumption) 1503cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymNE(State, Sym, zero, zero); 1513cdf584e068056540769dab56cad333e95a89750Anna Zaks else 1523cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymEQ(State, Sym, zero, zero); 1533cdf584e068056540769dab56cad333e95a89750Anna Zaks} 1543cdf584e068056540769dab56cad333e95a89750Anna Zaks 1558bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 156a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek NonLoc Cond, 157a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 1581eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1593cdf584e068056540769dab56cad333e95a89750Anna Zaks // We cannot reason about SymSymExprs, and can only reason about some 1603cdf584e068056540769dab56cad333e95a89750Anna Zaks // SymIntExprs. 161a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu if (!canReasonAbout(Cond)) { 1623cdf584e068056540769dab56cad333e95a89750Anna Zaks // Just add the constraint to the expression without trying to simplify. 1633cdf584e068056540769dab56cad333e95a89750Anna Zaks SymbolRef sym = Cond.getAsSymExpr(); 1643cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 1651eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 166a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu 167efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek BasicValueFactory &BasicVals = getBasicVals(); 168efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek 1694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 1704502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 171b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie llvm_unreachable("'Assume' not implemented for this NonLoc"); 1724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::SymbolValKind: { 1745251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>(); 1754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym = SV.getSymbol(); 1763cdf584e068056540769dab56cad333e95a89750Anna Zaks assert(sym); 1773cdf584e068056540769dab56cad333e95a89750Anna Zaks 1785344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Handle SymbolData. 1795344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!SV.isExpression()) { 1803cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 181ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 1825344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Handle symbolic expression. 1835344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks } else { 1845344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // We can only simplify expressions whose RHS is an integer. 1855344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym); 1865344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!SE) 1875344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks return assumeAuxForSymbol(state, sym, Assumption); 1885344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks 1895344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks BinaryOperator::Opcode op = SE->getOpcode(); 1905344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Implicitly compare non-comparison expressions to 0. 191efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (!BinaryOperator::isComparisonOp(op)) { 192732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek QualType T = SE->getType(); 193efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek const llvm::APSInt &zero = BasicVals.getValue(0, T); 194efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek op = (Assumption ? BO_NE : BO_EQ); 195efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek return assumeSymRel(state, SE, op, zero); 196efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek } 1975344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // From here on out, op is the real comparison we'll be testing. 1985344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!Assumption) 1995344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks op = NegateComparison(op); 200ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2015344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 2025344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks } 203e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 2044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::ConcreteIntKind: { 2065251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0; 207a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 208a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 2094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::LocAsIntegerKind: 2125251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie return assumeAux(state, Cond.castAs<nonloc::LocAsInteger>().getLoc(), 213a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Assumption); 2144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2164502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2171d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rosestatic void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { 2181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Is it a "($sym+constant1)" expression? 2191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) { 2201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BinaryOperator::Opcode Op = SE->getOpcode(); 2211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Op == BO_Add || Op == BO_Sub) { 2221d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Sym = SE->getLHS(); 2231d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); 2241d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Don't forget to negate the adjustment if it's being subtracted. 2261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // This should happen /after/ promotion, in case the value being 2271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. 2281d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Op == BO_Sub) 2291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Adjustment = -Adjustment; 2301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 23176462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks } 23276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks} 23376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks 2348bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state, 235ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymExpr *LHS, 236ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op, 237ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int) { 238ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose assert(BinaryOperator::isComparisonOp(op) && 239ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose "Non-comparison ops should be rewritten as comparisons to zero."); 240ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Get the type used for calculating wraparound. 242732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek BasicValueFactory &BVF = getBasicVals(); 243732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType()); 2441d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 24576462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // We only handle simple comparisons of the form "$sym == constant" 24676462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // or "($sym+constant1) == constant2". 24776462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // The adjustment is "constant1" in the above expression. It's used to 24876462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // "slide" the solution range around for modular arithmetic. For example, 24976462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 25076462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 25176462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // the subclasses of SimpleConstraintManager to handle the adjustment. 25276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks SymbolRef Sym = LHS; 2531d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Adjustment = WraparoundType.getZeroValue(); 2541d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose computeAdjustment(Sym, Adjustment); 2551d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2561d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Convert the right-hand side integer as necessary. 2571d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); 2581d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ConvertedInt = ComparisonType.convert(Int); 259b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 260ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 2614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 26228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek // No logic yet for other operators. assume the constraint is feasible. 263a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 2644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2652de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_EQ: 26628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 2674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2682de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_NE: 26928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 270ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2712de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GT: 27228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 2734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2742de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GE: 27528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 2764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2772de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LT: 27828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 2791eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2802de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LE: 28128f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 2824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2859ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenek} // end of namespace ento 2865a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 2875a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end of namespace clang 288