SimpleConstraintManager.cpp revision 1d8db493f86761df9470254a2ad572fc6abf1bf6
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); 70e36de1fe51c39d9161915dd3dbef880954af6476Ted Kremenek return SU.processAssume(state, cond, assumption); 714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 738bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 74a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Loc Cond, bool Assumption) { 754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert (false && "'Assume' not implemented for this Loc."); 78a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::MemRegionKind: { 814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: Should this go into the storemanager? 821eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 83a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion(); 84a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const SubRegion *SubR = dyn_cast<SubRegion>(R); 854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek while (SubR) { 874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: now we only find the first symbolic region. 88a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { 891d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth(); 903330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu if (Assumption) 9128f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, SymR->getSymbol(), zero, zero); 923330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu else 9328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, SymR->getSymbol(), zero, zero); 943330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu } 954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 971eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FALL-THROUGH. 994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1001eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1014502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::GotoLabelKind: 102a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? state : NULL; 1034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::ConcreteIntKind: { 1051eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; 106a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 107a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1084502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1128bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 11332a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek NonLoc cond, 11432a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 11528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 116e36de1fe51c39d9161915dd3dbef880954af6476Ted Kremenek return SU.processAssume(state, cond, assumption); 1174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1184502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 119ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rosestatic BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) { 120ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // FIXME: This should probably be part of BinaryOperator, since this isn't 121846eabd187be4bfe992e8bca131166b734d86e0dTed Kremenek // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.) 122ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 123ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose default: 124b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie llvm_unreachable("Invalid opcode."); 1252de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LT: return BO_GE; 1262de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GT: return BO_LE; 1272de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LE: return BO_GT; 1282de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GE: return BO_LT; 1292de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_EQ: return BO_NE; 1302de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_NE: return BO_EQ; 131ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose } 132ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose} 133ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 1343cdf584e068056540769dab56cad333e95a89750Anna Zaks 1351d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseProgramStateRef 1361d8db493f86761df9470254a2ad572fc6abf1bf6Jordy RoseSimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State, 1371d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose SymbolRef Sym, bool Assumption) { 1381d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BasicValueFactory &BVF = getBasicVals(); 1391d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose QualType T = Sym->getType(BVF.getContext()); 1401d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose const llvm::APSInt &zero = BVF.getValue(0, T); 1413cdf584e068056540769dab56cad333e95a89750Anna Zaks if (Assumption) 1423cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymNE(State, Sym, zero, zero); 1433cdf584e068056540769dab56cad333e95a89750Anna Zaks else 1443cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymEQ(State, Sym, zero, zero); 1453cdf584e068056540769dab56cad333e95a89750Anna Zaks} 1463cdf584e068056540769dab56cad333e95a89750Anna Zaks 1478bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 148a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek NonLoc Cond, 149a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 1501eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1513cdf584e068056540769dab56cad333e95a89750Anna Zaks // We cannot reason about SymSymExprs, and can only reason about some 1523cdf584e068056540769dab56cad333e95a89750Anna Zaks // SymIntExprs. 153a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu if (!canReasonAbout(Cond)) { 1543cdf584e068056540769dab56cad333e95a89750Anna Zaks // Just add the constraint to the expression without trying to simplify. 1553cdf584e068056540769dab56cad333e95a89750Anna Zaks SymbolRef sym = Cond.getAsSymExpr(); 1563cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 1571eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 158a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu 1591d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BasicValueFactory &BasicVals = getBasicVals(); 1604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 1624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 163b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie llvm_unreachable("'Assume' not implemented for this NonLoc"); 1644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::SymbolValKind: { 1664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); 1674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym = SV.getSymbol(); 1683cdf584e068056540769dab56cad333e95a89750Anna Zaks assert(sym); 1693cdf584e068056540769dab56cad333e95a89750Anna Zaks 1705344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Handle SymbolData. 1715344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!SV.isExpression()) { 1723cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 173ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 1745344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Handle symbolic expression. 1755344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks } else { 1765344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // We can only simplify expressions whose RHS is an integer. 1775344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym); 1785344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!SE) 1795344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks return assumeAuxForSymbol(state, sym, Assumption); 1805344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks 1815344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks BinaryOperator::Opcode op = SE->getOpcode(); 1825344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // Implicitly compare non-comparison expressions to 0. 1835344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!BinaryOperator::isComparisonOp(op)) { 1841d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose QualType T = SE->getType(BasicVals.getContext()); 1855344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks const llvm::APSInt &zero = BasicVals.getValue(0, T); 1865344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks op = (Assumption ? BO_NE : BO_EQ); 1875344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks return assumeSymRel(state, SE, op, zero); 1885344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks } 1895344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks // From here on out, op is the real comparison we'll be testing. 1905344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks if (!Assumption) 1915344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks op = NegateComparison(op); 192ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 1935344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 1945344baa704f42b22d9df25c24ffbbf6b4716603bAnna Zaks } 195e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 1964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::ConcreteIntKind: { 1984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; 199a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 200a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 2014502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::LocAsIntegerKind: 20428f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), 205a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Assumption); 2064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2084502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2091d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rosestatic void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { 2101d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Is it a "($sym+constant1)" expression? 2111d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) { 2121d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BinaryOperator::Opcode Op = SE->getOpcode(); 2131d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Op == BO_Add || Op == BO_Sub) { 2141d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Sym = SE->getLHS(); 2151d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); 2161d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2171d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Don't forget to negate the adjustment if it's being subtracted. 2181d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // This should happen /after/ promotion, in case the value being 2191d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. 2201d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose if (Op == BO_Sub) 2211d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose Adjustment = -Adjustment; 2221d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose } 22376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks } 22476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks} 22576462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks 2268bef8238181a30e52dea380789a7e2d760eac532Ted KremenekProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state, 227ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymExpr *LHS, 228ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op, 229ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int) { 230ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose assert(BinaryOperator::isComparisonOp(op) && 231ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose "Non-comparison ops should be rewritten as comparisons to zero."); 232ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2331d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose BasicValueFactory &BVF = getBasicVals(); 2341d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose ASTContext &Ctx = BVF.getContext(); 2351d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2361d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Get the type used for calculating wraparound. 2371d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType(Ctx)); 2381d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 23976462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // We only handle simple comparisons of the form "$sym == constant" 24076462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // or "($sym+constant1) == constant2". 24176462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // The adjustment is "constant1" in the above expression. It's used to 24276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // "slide" the solution range around for modular arithmetic. For example, 24376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 24476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 24576462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // the subclasses of SimpleConstraintManager to handle the adjustment. 24676462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks SymbolRef Sym = LHS; 2471d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt Adjustment = WraparoundType.getZeroValue(); 2481d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose computeAdjustment(Sym, Adjustment); 2491d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose 2501d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose // Convert the right-hand side integer as necessary. 2511d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); 2521d8db493f86761df9470254a2ad572fc6abf1bf6Jordy Rose llvm::APSInt ConvertedInt = ComparisonType.convert(Int); 253b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 254ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 2554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 25628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek // No logic yet for other operators. assume the constraint is feasible. 257a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 2584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2592de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_EQ: 26028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 2614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2622de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_NE: 26328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 264ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2652de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GT: 26628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 2674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2682de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GE: 26928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 2704502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2712de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LT: 27228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 2731eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 2742de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LE: 27528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 2764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2799ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenek} // end of namespace ento 2805a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 2815a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end of namespace clang 282