SimpleConstraintManager.cpp revision 4708b3dde86b06f40927ae9cf30a2de83949a8f2
16f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org//== SimpleConstraintManager.cpp --------------------------------*- C++ -*--==// 26f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org// 36f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org// The LLVM Compiler Infrastructure 46f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org// 56f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org// This file is distributed under the University of Illinois Open Source 66f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org// License. See LICENSE.TXT for details. 76f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org// 86f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org//===----------------------------------------------------------------------===// 96f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org// 106f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org// This file defines SimpleConstraintManager, a class that holds code shared 116f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org// between BasicConstraintManager and RangeConstraintManager. 126f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org// 136f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org//===----------------------------------------------------------------------===// 146f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 156f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org#include "SimpleConstraintManager.h" 166f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" 176f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" 186f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 196f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 206f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgnamespace clang { 216f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 226f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgnamespace ento { 236f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 246f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgSimpleConstraintManager::~SimpleConstraintManager() {} 256f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 266f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgbool SimpleConstraintManager::canReasonAbout(SVal X) const { 276f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>(); 286f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (SymVal && SymVal->isExpression()) { 296f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org const SymExpr *SE = SymVal->getSymbol(); 306f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 316f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) { 326f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org switch (SIE->getOpcode()) { 336f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // We don't reason yet about bitwise-constraints on symbolic values. 346f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_And: 356f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_Or: 366f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_Xor: 376f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return false; 386f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // We don't reason yet about these arithmetic constraints on 396f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // symbolic values. 406f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_Mul: 416f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_Div: 426f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_Rem: 436f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_Shl: 446f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_Shr: 456f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return false; 466f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // All other cases. 476f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org default: 486f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return true; 496f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 506f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 516f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 526f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) { 536f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (BinaryOperator::isComparisonOp(SSE->getOpcode())) 546f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return true; 556f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 566f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 576f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return false; 586f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 596f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 606f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return true; 616f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org} 626f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 636f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 646f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org DefinedSVal Cond, 656f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org bool Assumption) { 666f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (Optional<NonLoc> NV = Cond.getAs<NonLoc>()) 676f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assume(state, *NV, Assumption); 686f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assume(state, Cond.castAs<Loc>(), Assumption); 696f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org} 706f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 716f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond, 726f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org bool assumption) { 736f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org state = assumeAux(state, cond, assumption); 746f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (NotifyAssumeClients && SU) 756f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return SU->processAssume(state, cond, assumption); 766f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return state; 776f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org} 786f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 796f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 806f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org Loc Cond, bool Assumption) { 816f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org switch (Cond.getSubKind()) { 826f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org default: 836f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org assert (false && "'Assume' not implemented for this Loc."); 846f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return state; 856f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 866f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case loc::MemRegionKind: { 876f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // FIXME: Should this go into the storemanager? 886f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 896f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org const MemRegion *R = Cond.castAs<loc::MemRegionVal>().getRegion(); 906f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org const SubRegion *SubR = dyn_cast<SubRegion>(R); 916f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 926f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org while (SubR) { 936f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // FIXME: now we only find the first symbolic region. 946f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { 956f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth(); 966f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (Assumption) 976f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymNE(state, SymR->getSymbol(), zero, zero); 986f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org else 996f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymEQ(state, SymR->getSymbol(), zero, zero); 1006f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 1016f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 1026f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 1036f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1046f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // FALL-THROUGH. 1056f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 1066f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1076f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case loc::GotoLabelKind: 1086f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return Assumption ? state : NULL; 1096f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1106f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case loc::ConcreteIntKind: { 1116f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org bool b = Cond.castAs<loc::ConcreteInt>().getValue() != 0; 1126f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org bool isFeasible = b ? Assumption : !Assumption; 1136f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return isFeasible ? state : NULL; 1146f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 1156f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } // end switch 1166f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org} 1176f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1186f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 1196f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org NonLoc cond, 1206f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org bool assumption) { 1216f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org state = assumeAux(state, cond, assumption); 1226f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (NotifyAssumeClients && SU) 1236f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return SU->processAssume(state, cond, assumption); 1246f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return state; 1256f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org} 1266f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1276f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1286f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgProgramStateRef 1296f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgSimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State, 1306f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org SymbolRef Sym, bool Assumption) { 1316f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org BasicValueFactory &BVF = getBasicVals(); 1326f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org QualType T = Sym->getType(); 1336f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1346f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // None of the constraint solvers currently support non-integer types. 1356f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (!T->isIntegerType()) 1366f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return State; 1376f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1386f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org const llvm::APSInt &zero = BVF.getValue(0, T); 1396f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (Assumption) 1406f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymNE(State, Sym, zero, zero); 1416f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org else 1426f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymEQ(State, Sym, zero, zero); 1436f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org} 1446f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1456f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 1466f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org NonLoc Cond, 1476f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org bool Assumption) { 1486f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1496f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // We cannot reason about SymSymExprs, and can only reason about some 1506f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // SymIntExprs. 1516f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (!canReasonAbout(Cond)) { 1526f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // Just add the constraint to the expression without trying to simplify. 1536f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org SymbolRef sym = Cond.getAsSymExpr(); 1546f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeAuxForSymbol(state, sym, Assumption); 1556f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 1566f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1576f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org switch (Cond.getSubKind()) { 1586f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org default: 1596f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org llvm_unreachable("'Assume' not implemented for this NonLoc"); 1606f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1616f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case nonloc::SymbolValKind: { 1626f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>(); 1636f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org SymbolRef sym = SV.getSymbol(); 1646f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org assert(sym); 1656f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1666f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // Handle SymbolData. 1676f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (!SV.isExpression()) { 1686f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeAuxForSymbol(state, sym, Assumption); 1696f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1706f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // Handle symbolic expression. 1716f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym)) { 1726f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // We can only simplify expressions whose RHS is an integer. 1736f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1746f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org BinaryOperator::Opcode op = SE->getOpcode(); 1756f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (BinaryOperator::isComparisonOp(op)) { 1766f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (!Assumption) 1776f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org op = BinaryOperator::negateComparisonOp(op); 1786f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1796f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 1806f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 1816f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1826f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) { 1836f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // Translate "a != b" to "(b - a) != 0". 1846f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // We invert the order of the operands as a heuristic for how loop 1856f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // conditions are usually written ("begin != end") as compared to length 1866f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // calculations ("end - begin"). The more correct thing to do would be to 1876f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // canonicalize "a - b" and "b - a", which would allow us to treat 1886f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // "a != b" and "b != a" the same. 1896f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org SymbolManager &SymMgr = getSymbolManager(); 1906f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org BinaryOperator::Opcode Op = SSE->getOpcode(); 1916f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org assert(BinaryOperator::isComparisonOp(Op)); 1926f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 1936f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // For now, we only support comparing pointers. 1946f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org assert(Loc::isLocType(SSE->getLHS()->getType())); 1956f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org assert(Loc::isLocType(SSE->getRHS()->getType())); 1966f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org QualType DiffTy = SymMgr.getContext().getPointerDiffType(); 1976f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, 1986f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org SSE->getLHS(), DiffTy); 1996f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2006f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy); 2016f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org Op = BinaryOperator::reverseComparisonOp(Op); 2026f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (!Assumption) 2036f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org Op = BinaryOperator::negateComparisonOp(Op); 2046f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymRel(state, Subtraction, Op, Zero); 2056f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 2066f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2076f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // If we get here, there's nothing else we can do but treat the symbol as 2086f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // opaque. 2096f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeAuxForSymbol(state, sym, Assumption); 2106f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 2116f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2126f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case nonloc::ConcreteIntKind: { 2136f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0; 2146f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org bool isFeasible = b ? Assumption : !Assumption; 2156f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return isFeasible ? state : NULL; 2166f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 2176f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2186f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case nonloc::LocAsIntegerKind: 2196f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeAux(state, Cond.castAs<nonloc::LocAsInteger>().getLoc(), 2206f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org Assumption); 2216f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } // end switch 2226f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org} 2236f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2246f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgstatic void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { 2256f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // Is it a "($sym+constant1)" expression? 2266f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) { 2276f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org BinaryOperator::Opcode Op = SE->getOpcode(); 2286f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (Op == BO_Add || Op == BO_Sub) { 2296f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org Sym = SE->getLHS(); 2306f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); 2316f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2326f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // Don't forget to negate the adjustment if it's being subtracted. 2336f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // This should happen /after/ promotion, in case the value being 2346f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. 2356f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (Op == BO_Sub) 2366f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org Adjustment = -Adjustment; 2376f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 2386f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } 2396f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org} 2406f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2416f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.orgProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state, 2426f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org const SymExpr *LHS, 2436f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org BinaryOperator::Opcode op, 2446f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org const llvm::APSInt& Int) { 2456f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org assert(BinaryOperator::isComparisonOp(op) && 2466f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org "Non-comparison ops should be rewritten as comparisons to zero."); 2476f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2486f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // Get the type used for calculating wraparound. 2496f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org BasicValueFactory &BVF = getBasicVals(); 2506f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType()); 2516f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2526f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // We only handle simple comparisons of the form "$sym == constant" 2536f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // or "($sym+constant1) == constant2". 2546f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // The adjustment is "constant1" in the above expression. It's used to 2556f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // "slide" the solution range around for modular arithmetic. For example, 2566f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 2576f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 2586f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // the subclasses of SimpleConstraintManager to handle the adjustment. 2596f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org SymbolRef Sym = LHS; 2606f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org llvm::APSInt Adjustment = WraparoundType.getZeroValue(); 2616f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org computeAdjustment(Sym, Adjustment); 2626f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2636f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // Convert the right-hand side integer as necessary. 2646f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); 2656f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org llvm::APSInt ConvertedInt = ComparisonType.convert(Int); 2666f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2676f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org // Prefer unsigned comparisons. 2686f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() && 2696f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) 2706f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org Adjustment.setIsSigned(false); 2716f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2726f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org switch (op) { 2736f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org default: 2746f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org llvm_unreachable("invalid operation not caught by assertion above"); 2756f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2766f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_EQ: 2776f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 2786f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2796f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_NE: 2806f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 2816f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2826f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_GT: 2836f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 2846f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2856f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_GE: 2866f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 2876f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2886f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_LT: 2896f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 2906f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2916f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org case BO_LE: 2926f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 2936f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org } // end switch 2946f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org} 2956f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2966f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org} // end of namespace ento 2976f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org 2986f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org} // end of namespace clang 2996f31ac30b9092fd02a8c97e5216cf53f3e4fae4jshin@chromium.org