SimpleConstraintManager.cpp revision ca5d78d0bc3010164f2f9682967d64d7e305a167
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 { 275344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks nonloc::SymbolVal *SymVal = dyn_cast<nonloc::SymbolVal>(&X); 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) { 614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (isa<NonLoc>(Cond)) 6228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assume(state, cast<NonLoc>(Cond), Assumption); 634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek else 6428f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assume(state, cast<Loc>(Cond), Assumption); 654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 678bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond, 6832a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 6928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 70ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose if (NotifyAssumeClients && SU) 71ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose return SU->processAssume(state, cond, assumption); 7247cbd0f3892c7965cf16a58393f9f17a22d4d4d9Ted Kremenek return state; 734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 758bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 76a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Loc Cond, bool Assumption) { 774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert (false && "'Assume' not implemented for this Loc."); 80a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::MemRegionKind: { 834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: Should this go into the storemanager? 841eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 85a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion(); 86a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const SubRegion *SubR = dyn_cast<SubRegion>(R); 874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 884502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek while (SubR) { 89efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek // FIXME: now we only find the first symbolic region. 90efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { 91efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth(); 92efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (Assumption) 93efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek return assumeSymNE(state, SymR->getSymbol(), zero, zero); 94efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek else 95efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek return assumeSymEQ(state, SymR->getSymbol(), zero, zero); 96efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek } 974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 991eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FALL-THROUGH. 1014502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1021eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::GotoLabelKind: 104a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? state : NULL; 1054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::ConcreteIntKind: { 1071eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; 108a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 109a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1148bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 11532a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek NonLoc cond, 11632a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 11728f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 118ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose if (NotifyAssumeClients && SU) 119ca5d78d0bc3010164f2f9682967d64d7e305a167Jordan Rose return SU->processAssume(state, cond, assumption); 12005c3b9ac74e12238e7ec5f237132e2348a8b5f4eAnna Zaks return state; 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 1383cdf584e068056540769dab56cad333e95a89750Anna Zaks 1391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseProgramStateRef 1401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseSimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State, 1411d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose SymbolRef Sym, bool Assumption) { 1421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BasicValueFactory &BVF = getBasicVals(); 143732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek QualType T = Sym->getType(); 144b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks 145efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek // None of the constraint solvers currently support non-integer types. 146efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (!T->isIntegerType()) 147b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks return State; 148b3b1ae85757a8722caccb742b73ca31b4b53bb0aAnna Zaks 1491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &zero = BVF.getValue(0, T); 1503cdf584e068056540769dab56cad333e95a89750Anna Zaks if (Assumption) 1513cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymNE(State, Sym, zero, zero); 1523cdf584e068056540769dab56cad333e95a89750Anna Zaks else 1533cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymEQ(State, Sym, zero, zero); 1543cdf584e068056540769dab56cad333e95a89750Anna Zaks} 1553cdf584e068056540769dab56cad333e95a89750Anna Zaks 1568bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 157a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek NonLoc Cond, 158a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 1591eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1603cdf584e068056540769dab56cad333e95a89750Anna Zaks // We cannot reason about SymSymExprs, and can only reason about some 1613cdf584e068056540769dab56cad333e95a89750Anna Zaks // SymIntExprs. 162a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu if (!canReasonAbout(Cond)) { 1633cdf584e068056540769dab56cad333e95a89750Anna Zaks // Just add the constraint to the expression without trying to simplify. 1643cdf584e068056540769dab56cad333e95a89750Anna Zaks SymbolRef sym = Cond.getAsSymExpr(); 1653cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 1661eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 167a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu 168efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek BasicValueFactory &BasicVals = getBasicVals(); 169efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek 1704502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 1714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 172b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie llvm_unreachable("'Assume' not implemented for this NonLoc"); 1734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::SymbolValKind: { 1754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); 1764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym = SV.getSymbol(); 1773cdf584e068056540769dab56cad333e95a89750Anna Zaks assert(sym); 1783cdf584e068056540769dab56cad333e95a89750Anna Zaks 1795344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Handle SymbolData. 1805344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!SV.isExpression()) { 1813cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 182ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 1835344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Handle symbolic expression. 1845344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks } else { 1855344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // We can only simplify expressions whose RHS is an integer. 1865344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym); 1875344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!SE) 1885344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks return assumeAuxForSymbol(state, sym, Assumption); 1895344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks 1905344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks BinaryOperator::Opcode op = SE->getOpcode(); 1915344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Implicitly compare non-comparison expressions to 0. 192efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek if (!BinaryOperator::isComparisonOp(op)) { 193732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek QualType T = SE->getType(); 194efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek const llvm::APSInt &zero = BasicVals.getValue(0, T); 195efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek op = (Assumption ? BO_NE : BO_EQ); 196efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek return assumeSymRel(state, SE, op, zero); 197efb3d56720654f5355ff8fc666499cc6554034f4Ted Kremenek } 1985344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // From here on out, op is the real comparison we'll be testing. 1995344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!Assumption) 2005344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks op = NegateComparison(op); 201ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2025344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 2035344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks } 204e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 2054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::ConcreteIntKind: { 2074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; 208a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 209a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 2104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::LocAsIntegerKind: 21328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), 214a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Assumption); 2154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2164502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rosestatic void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { 2191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Is it a "($sym+constant1)" expression? 2201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) { 2211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BinaryOperator::Opcode Op = SE->getOpcode(); 2221d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Op == BO_Add || Op == BO_Sub) { 2231d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Sym = SE->getLHS(); 2241d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); 2251d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2261d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Don't forget to negate the adjustment if it's being subtracted. 2271d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // This should happen /after/ promotion, in case the value being 2281d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. 2291d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Op == BO_Sub) 2301d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Adjustment = -Adjustment; 2311d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 23276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks } 23376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks} 23476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks 2358bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state, 236ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymExpr *LHS, 237ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op, 238ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int) { 239ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose assert(BinaryOperator::isComparisonOp(op) && 240ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose "Non-comparison ops should be rewritten as comparisons to zero."); 241ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2421d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Get the type used for calculating wraparound. 243732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek BasicValueFactory &BVF = getBasicVals(); 244732cdf383f9030ff2b9fb28dfbdae2285ded80c6Ted Kremenek APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType()); 2451d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 24676462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // We only handle simple comparisons of the form "$sym == constant" 24776462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // or "($sym+constant1) == constant2". 24876462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // The adjustment is "constant1" in the above expression. It's used to 24976462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // "slide" the solution range around for modular arithmetic. For example, 25076462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 25176462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 25276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // the subclasses of SimpleConstraintManager to handle the adjustment. 25376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks SymbolRef Sym = LHS; 2541d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Adjustment = WraparoundType.getZeroValue(); 2551d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose computeAdjustment(Sym, Adjustment); 2561d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2571d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Convert the right-hand side integer as necessary. 2581d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); 2591d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ConvertedInt = ComparisonType.convert(Int); 260b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 261ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 2624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 26328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek // No logic yet for other operators. assume the constraint is feasible. 264a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 2654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2662de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_EQ: 26728f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 2684502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2692de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_NE: 27028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 271ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2722de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GT: 27328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 2744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2752de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GE: 27628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 2774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2782de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LT: 27928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 2801eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2812de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LE: 28228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 2834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2869ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenek} // end of namespace ento 2875a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 2885a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end of namespace clang 289