SimpleConstraintManager.cpp revision 8f7bfb40b72f478d83b018a280f99c0386576ae3
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 { 27dc84cd5efdd3430efb22546b4ac656aa0540b210David Blaikie 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 5278114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) { 538f7bfb40b72f478d83b018a280f99c0386576ae3Jordan Rose if (BinaryOperator::isComparisonOp(SSE->getOpcode())) { 548f7bfb40b72f478d83b018a280f99c0386576ae3Jordan Rose // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc. 558f7bfb40b72f478d83b018a280f99c0386576ae3Jordan Rose if (Loc::isLocType(SSE->getLHS()->getType())) { 568f7bfb40b72f478d83b018a280f99c0386576ae3Jordan Rose assert(Loc::isLocType(SSE->getRHS()->getType())); 578f7bfb40b72f478d83b018a280f99c0386576ae3Jordan Rose return true; 588f7bfb40b72f478d83b018a280f99c0386576ae3Jordan Rose } 598f7bfb40b72f478d83b018a280f99c0386576ae3Jordan Rose } 6078114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose } 6178114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose 62e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 637de20fe9aac00705dd943690563db66fa4b35b5bTed Kremenek } 647de20fe9aac00705dd943690563db66fa4b35b5bTed Kremenek 6566b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek return true; 6666b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek} 671eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 688bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 695b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek DefinedSVal Cond, 705b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek bool Assumption) { 71dc84cd5efdd3430efb22546b4ac656aa0540b210David Blaikie if (Optional<NonLoc> NV = Cond.getAs<NonLoc>()) 725251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie return assume(state, *NV, Assumption); 735251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie return assume(state, Cond.castAs<Loc>(), Assumption); 744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 768bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond, 7732a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 7828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 79ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose if (NotifyAssumeClients && SU) 80ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose return SU->processAssume(state, cond, assumption); 8147cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek return state; 824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 848bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 85a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Loc Cond, bool Assumption) { 864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 884502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert (false && "'Assume' not implemented for this Loc."); 89a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::MemRegionKind: { 924502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: Should this go into the storemanager? 931eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 945251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie const MemRegion *R = Cond.castAs<loc::MemRegionVal>().getRegion(); 95a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const SubRegion *SubR = dyn_cast<SubRegion>(R); 964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek while (SubR) { 98efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek // FIXME: now we only find the first symbolic region. 99efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { 100efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth(); 101efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (Assumption) 102efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek return assumeSymNE(state, SymR->getSymbol(), zero, zero); 103efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek else 104efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek return assumeSymEQ(state, SymR->getSymbol(), zero, zero); 105efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek } 1064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 1074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1081eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FALL-THROUGH. 1104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1111eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::GotoLabelKind: 113a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? state : NULL; 1144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::ConcreteIntKind: { 1165251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie bool b = Cond.castAs<loc::ConcreteInt>().getValue() != 0; 117a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 118a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1238bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 12432a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek NonLoc cond, 12532a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 12628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 127ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose if (NotifyAssumeClients && SU) 128ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose return SU->processAssume(state, cond, assumption); 12905c3b9ac74e12238e7ec5f237132e2348a8b5f4eAnna Zaks return state; 1304502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1314502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1323cdf584e068056540769dab56cad333e95a89750Anna Zaks 1331d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseProgramStateRef 1341d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseSimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State, 1351d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose SymbolRef Sym, bool Assumption) { 1361d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BasicValueFactory &BVF = getBasicVals(); 137732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek QualType T = Sym->getType(); 138b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks 139efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek // None of the constraint solvers currently support non-integer types. 140efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (!T->isIntegerType()) 141b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks return State; 142b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks 1431d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &zero = BVF.getValue(0, T); 1443cdf584e068056540769dab56cad333e95a89750Anna Zaks if (Assumption) 1453cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymNE(State, Sym, zero, zero); 1463cdf584e068056540769dab56cad333e95a89750Anna Zaks else 1473cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymEQ(State, Sym, zero, zero); 1483cdf584e068056540769dab56cad333e95a89750Anna Zaks} 1493cdf584e068056540769dab56cad333e95a89750Anna Zaks 1508bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 151a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek NonLoc Cond, 152a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 1531eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1543cdf584e068056540769dab56cad333e95a89750Anna Zaks // We cannot reason about SymSymExprs, and can only reason about some 1553cdf584e068056540769dab56cad333e95a89750Anna Zaks // SymIntExprs. 156a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu if (!canReasonAbout(Cond)) { 1573cdf584e068056540769dab56cad333e95a89750Anna Zaks // Just add the constraint to the expression without trying to simplify. 1583cdf584e068056540769dab56cad333e95a89750Anna Zaks SymbolRef sym = Cond.getAsSymExpr(); 1593cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 1601eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 161a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu 1624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 1634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 164b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie llvm_unreachable("'Assume' not implemented for this NonLoc"); 1654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::SymbolValKind: { 1675251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>(); 1684502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym = SV.getSymbol(); 1693cdf584e068056540769dab56cad333e95a89750Anna Zaks assert(sym); 1703cdf584e068056540769dab56cad333e95a89750Anna Zaks 1715344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Handle SymbolData. 1725344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!SV.isExpression()) { 1733cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 174ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 1755344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Handle symbolic expression. 17678114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym)) { 1775344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // We can only simplify expressions whose RHS is an integer. 1785344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks 1795344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks BinaryOperator::Opcode op = SE->getOpcode(); 18078114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose if (BinaryOperator::isComparisonOp(op)) { 18178114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose if (!Assumption) 1828569281fb7ce9b5ca164a0528b876acbb45eb989Jordan Rose op = BinaryOperator::negateComparisonOp(op); 18378114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose 18478114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 185efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek } 186ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 18778114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) { 18878114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // Translate "a != b" to "(b - a) != 0". 18978114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // We invert the order of the operands as a heuristic for how loop 19078114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // conditions are usually written ("begin != end") as compared to length 19178114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // calculations ("end - begin"). The more correct thing to do would be to 19278114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // canonicalize "a - b" and "b - a", which would allow us to treat 19378114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // "a != b" and "b != a" the same. 194281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose SymbolManager &SymMgr = getSymbolManager(); 195281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose BinaryOperator::Opcode Op = SSE->getOpcode(); 196281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose assert(BinaryOperator::isComparisonOp(Op)); 197281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose 198281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose // For now, we only support comparing pointers. 199281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose assert(Loc::isLocType(SSE->getLHS()->getType())); 200281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose assert(Loc::isLocType(SSE->getRHS()->getType())); 201281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose QualType DiffTy = SymMgr.getContext().getPointerDiffType(); 202281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, 203281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose SSE->getLHS(), DiffTy); 204281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose 205281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy); 206281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose Op = BinaryOperator::reverseComparisonOp(Op); 207281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose if (!Assumption) 208281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose Op = BinaryOperator::negateComparisonOp(Op); 209281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose return assumeSymRel(state, Subtraction, Op, Zero); 2105344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks } 21178114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose 21278114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // If we get here, there's nothing else we can do but treat the symbol as 21378114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // opaque. 21478114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose return assumeAuxForSymbol(state, sym, Assumption); 215e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 2164502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::ConcreteIntKind: { 2185251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0; 219a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 220a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 2214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2234502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::LocAsIntegerKind: 2245251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie return assumeAux(state, Cond.castAs<nonloc::LocAsInteger>().getLoc(), 225a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Assumption); 2264502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2274502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rosestatic void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { 2301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Is it a "($sym+constant1)" expression? 2311d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) { 2321d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BinaryOperator::Opcode Op = SE->getOpcode(); 2331d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Op == BO_Add || Op == BO_Sub) { 2341d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Sym = SE->getLHS(); 2351d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); 2361d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2371d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Don't forget to negate the adjustment if it's being subtracted. 2381d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // This should happen /after/ promotion, in case the value being 2391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. 2401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Op == BO_Sub) 2411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Adjustment = -Adjustment; 2421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 24376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks } 24476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks} 24576462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks 2468bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state, 247ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymExpr *LHS, 248ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op, 249ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int) { 250ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose assert(BinaryOperator::isComparisonOp(op) && 251ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose "Non-comparison ops should be rewritten as comparisons to zero."); 252ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2531d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Get the type used for calculating wraparound. 254732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek BasicValueFactory &BVF = getBasicVals(); 255732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType()); 2561d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 25776462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // We only handle simple comparisons of the form "$sym == constant" 25876462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // or "($sym+constant1) == constant2". 25976462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // The adjustment is "constant1" in the above expression. It's used to 26076462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // "slide" the solution range around for modular arithmetic. For example, 26176462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 26276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 26376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // the subclasses of SimpleConstraintManager to handle the adjustment. 26476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks SymbolRef Sym = LHS; 2651d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Adjustment = WraparoundType.getZeroValue(); 2661d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose computeAdjustment(Sym, Adjustment); 2671d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2681d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Convert the right-hand side integer as necessary. 2691d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); 2701d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ConvertedInt = ComparisonType.convert(Int); 271b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 2724708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose // Prefer unsigned comparisons. 2734708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() && 2744708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) 2754708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose Adjustment.setIsSigned(false); 2764708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose 277ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 2784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 2794708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose llvm_unreachable("invalid operation not caught by assertion above"); 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