SimpleConstraintManager.cpp revision 3aa6f431897edf5fec32cbede8fcddbfb8fa16f7
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) { 713aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose // If we have a Loc value, cast it to a bool NonLoc first. 723aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose if (Optional<Loc> LV = Cond.getAs<Loc>()) { 733aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose SValBuilder &SVB = state->getStateManager().getSValBuilder(); 743aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose QualType T; 753aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose const MemRegion *MR = LV->getAsRegion(); 763aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose if (const TypedRegion *TR = dyn_cast_or_null<TypedRegion>(MR)) 773aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose T = TR->getLocationType(); 783aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose else 793aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose T = SVB.getContext().VoidPtrTy; 803aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose 813aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose Cond = SVB.evalCast(*LV, SVB.getContext().BoolTy, T).castAs<DefinedSVal>(); 824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 831eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 843aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose return assume(state, Cond.castAs<NonLoc>(), Assumption); 854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 878bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 8832a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek NonLoc cond, 8932a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 9028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 91ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose if (NotifyAssumeClients && SU) 92ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose return SU->processAssume(state, cond, assumption); 9305c3b9ac74e12238e7ec5f237132e2348a8b5f4eAnna Zaks return state; 944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 963cdf584e068056540769dab56cad333e95a89750Anna Zaks 971d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseProgramStateRef 981d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseSimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State, 991d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose SymbolRef Sym, bool Assumption) { 1001d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BasicValueFactory &BVF = getBasicVals(); 101732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek QualType T = Sym->getType(); 102b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks 103efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek // None of the constraint solvers currently support non-integer types. 104a5796f87229b4aeebca71fa6ee1790ae7a5a0382Jordan Rose if (!T->isIntegralOrEnumerationType()) 105b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks return State; 106b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks 1071d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &zero = BVF.getValue(0, T); 1083cdf584e068056540769dab56cad333e95a89750Anna Zaks if (Assumption) 1093cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymNE(State, Sym, zero, zero); 1103cdf584e068056540769dab56cad333e95a89750Anna Zaks else 1113cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymEQ(State, Sym, zero, zero); 1123cdf584e068056540769dab56cad333e95a89750Anna Zaks} 1133cdf584e068056540769dab56cad333e95a89750Anna Zaks 1148bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 115a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek NonLoc Cond, 116a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 1171eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1183cdf584e068056540769dab56cad333e95a89750Anna Zaks // We cannot reason about SymSymExprs, and can only reason about some 1193cdf584e068056540769dab56cad333e95a89750Anna Zaks // SymIntExprs. 120a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu if (!canReasonAbout(Cond)) { 1213cdf584e068056540769dab56cad333e95a89750Anna Zaks // Just add the constraint to the expression without trying to simplify. 1223cdf584e068056540769dab56cad333e95a89750Anna Zaks SymbolRef sym = Cond.getAsSymExpr(); 1233cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 1241eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 125a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu 1264502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 1274502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 128b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie llvm_unreachable("'Assume' not implemented for this NonLoc"); 1294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1304502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::SymbolValKind: { 1315251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>(); 1324502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym = SV.getSymbol(); 1333cdf584e068056540769dab56cad333e95a89750Anna Zaks assert(sym); 1343cdf584e068056540769dab56cad333e95a89750Anna Zaks 1355344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Handle SymbolData. 1365344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!SV.isExpression()) { 1373cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 138ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 1395344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Handle symbolic expression. 14078114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym)) { 1415344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // We can only simplify expressions whose RHS is an integer. 1425344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks 1435344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks BinaryOperator::Opcode op = SE->getOpcode(); 14478114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose if (BinaryOperator::isComparisonOp(op)) { 14578114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose if (!Assumption) 1468569281fb7ce9b5ca164a0528b876acbb45eb989Jordan Rose op = BinaryOperator::negateComparisonOp(op); 14778114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose 14878114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 149efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek } 150ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 15178114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) { 15278114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // Translate "a != b" to "(b - a) != 0". 15378114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // We invert the order of the operands as a heuristic for how loop 15478114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // conditions are usually written ("begin != end") as compared to length 15578114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // calculations ("end - begin"). The more correct thing to do would be to 15678114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // canonicalize "a - b" and "b - a", which would allow us to treat 15778114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // "a != b" and "b != a" the same. 158281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose SymbolManager &SymMgr = getSymbolManager(); 159281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose BinaryOperator::Opcode Op = SSE->getOpcode(); 160281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose assert(BinaryOperator::isComparisonOp(Op)); 161281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose 162281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose // For now, we only support comparing pointers. 163281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose assert(Loc::isLocType(SSE->getLHS()->getType())); 164281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose assert(Loc::isLocType(SSE->getRHS()->getType())); 165281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose QualType DiffTy = SymMgr.getContext().getPointerDiffType(); 166281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, 167281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose SSE->getLHS(), DiffTy); 168281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose 169281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy); 170281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose Op = BinaryOperator::reverseComparisonOp(Op); 171281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose if (!Assumption) 172281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose Op = BinaryOperator::negateComparisonOp(Op); 173281698935f62ac1d35ddd3533a562c1589aadc8bJordan Rose return assumeSymRel(state, Subtraction, Op, Zero); 1745344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks } 17578114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose 17678114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // If we get here, there's nothing else we can do but treat the symbol as 17778114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose // opaque. 17878114a58f8cf5e9b948e82448b2f0904f5b6c19eJordan Rose return assumeAuxForSymbol(state, sym, Assumption); 179e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 1804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::ConcreteIntKind: { 1825251abea41b446c26e3239c8dd6c7edea6fc335dDavid Blaikie bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0; 183a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 184a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::LocAsIntegerKind: 1883aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose return assume(state, Cond.castAs<nonloc::LocAsInteger>().getLoc(), 1893aa6f431897edf5fec32cbede8fcddbfb8fa16f7Jordan Rose Assumption); 1904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1924502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1931d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rosestatic void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { 1941d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Is it a "($sym+constant1)" expression? 1951d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) { 1961d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BinaryOperator::Opcode Op = SE->getOpcode(); 1971d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Op == BO_Add || Op == BO_Sub) { 1981d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Sym = SE->getLHS(); 1991d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); 2001d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2011d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Don't forget to negate the adjustment if it's being subtracted. 2021d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // This should happen /after/ promotion, in case the value being 2031d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. 2041d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Op == BO_Sub) 2051d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Adjustment = -Adjustment; 2061d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 20776462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks } 20876462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks} 20976462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks 2108bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state, 211ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymExpr *LHS, 212ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op, 213ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int) { 214ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose assert(BinaryOperator::isComparisonOp(op) && 215ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose "Non-comparison ops should be rewritten as comparisons to zero."); 216ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2171d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Get the type used for calculating wraparound. 218732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek BasicValueFactory &BVF = getBasicVals(); 219732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType()); 2201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 22176462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // We only handle simple comparisons of the form "$sym == constant" 22276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // or "($sym+constant1) == constant2". 22376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // The adjustment is "constant1" in the above expression. It's used to 22476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // "slide" the solution range around for modular arithmetic. For example, 22576462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 22676462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 22776462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // the subclasses of SimpleConstraintManager to handle the adjustment. 22876462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks SymbolRef Sym = LHS; 2291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Adjustment = WraparoundType.getZeroValue(); 2301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose computeAdjustment(Sym, Adjustment); 2311d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2321d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Convert the right-hand side integer as necessary. 2331d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); 2341d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ConvertedInt = ComparisonType.convert(Int); 235b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 2364708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose // Prefer unsigned comparisons. 2374708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() && 2384708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) 2394708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose Adjustment.setIsSigned(false); 2404708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose 241ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 2424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 2434708b3dde86b06f40927ae9cf30a2de83949a8f2Jordan Rose llvm_unreachable("invalid operation not caught by assertion above"); 2444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2452de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_EQ: 24628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 2474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2482de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_NE: 24928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 250ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2512de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GT: 25228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 2534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2542de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GE: 25528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 2564502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2572de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LT: 25828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 2591eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2602de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LE: 26128f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 2624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2659ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenek} // end of namespace ento 2665a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 2675a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end of namespace clang 268