SimpleConstraintManager.cpp revision e0e4ebf6bfca5a71b2344d8a1b748b852509279c
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" 164502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "clang/Analysis/PathSensitive/GRExprEngine.h" 174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek#include "clang/Analysis/PathSensitive/GRState.h" 184502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang { 204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 214502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::~SimpleConstraintManager() {} 224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2366b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenekbool SimpleConstraintManager::canReasonAbout(SVal X) const { 24e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) { 25e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek const SymExpr *SE = SymVal->getSymbolicExpression(); 26e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek 27e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (isa<SymbolData>(SE)) 28e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return true; 29e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek 30e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) { 31e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek switch (SIE->getOpcode()) { 32e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // We don't reason yet about bitwise-constraints on symbolic values. 33e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::And: 34e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Or: 35e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Xor: 36e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 37e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // We don't reason yet about arithmetic constraints on symbolic values. 38e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Mul: 39e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Div: 40e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Rem: 41e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Add: 42e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Sub: 43e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Shl: 44e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case BinaryOperator::Shr: 45e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 46e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // All other cases. 47e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek default: 48e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return true; 49e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 50e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 51e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek 52e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 537de20fe9aac00705dd943690563db66fa4b35b5bTed Kremenek } 547de20fe9aac00705dd943690563db66fa4b35b5bTed Kremenek 5566b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek return true; 5666b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek} 5766b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek 584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekconst GRState* 594502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::Assume(const GRState* St, SVal Cond, bool Assumption, 604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool& isFeasible) { 614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (Cond.isUnknown()) { 624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek isFeasible = true; 634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return St; 644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (isa<NonLoc>(Cond)) 674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return Assume(St, cast<NonLoc>(Cond), Assumption, isFeasible); 684502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek else 694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return Assume(St, cast<Loc>(Cond), Assumption, isFeasible); 704502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekconst GRState* 734502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::Assume(const GRState* St, Loc Cond, bool Assumption, 744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool& isFeasible) { 754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek St = AssumeAux(St, Cond, Assumption, isFeasible); 764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 774502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (!isFeasible) 784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return St; 794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // EvalAssume is used to call into the GRTransferFunction object to perform 814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // any checker-specific update of the state based on this assumption being 824502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // true or false. 834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption, 844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek isFeasible); 854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekconst GRState* 884502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::AssumeAux(const GRState* St, Loc Cond, bool Assumption, 894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool& isFeasible) { 904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek BasicValueFactory& BasicVals = StateMgr.getBasicVals(); 914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 924502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 934502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert (false && "'Assume' not implemented for this Loc."); 954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return St; 964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::SymbolValKind: 984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (Assumption) 994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return AssumeSymNE(St, cast<loc::SymbolVal>(Cond).getSymbol(), 1004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek BasicVals.getZeroWithPtrWidth(), isFeasible); 1014502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek else 1024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return AssumeSymEQ(St, cast<loc::SymbolVal>(Cond).getSymbol(), 1034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek BasicVals.getZeroWithPtrWidth(), isFeasible); 1044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::MemRegionKind: { 1064502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: Should this go into the storemanager? 1074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1084502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const MemRegion* R = cast<loc::MemRegionVal>(Cond).getRegion(); 1094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const SubRegion* SubR = dyn_cast<SubRegion>(R); 1104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek while (SubR) { 1124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: now we only find the first symbolic region. 1134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (const SymbolicRegion* SymR = dyn_cast<SymbolicRegion>(SubR)) 1144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return AssumeAux(St, loc::SymbolVal(SymR->getSymbol()), Assumption, 1154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek isFeasible); 1164502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 1174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1184502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FALL-THROUGH. 1204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::FuncValKind: 1234502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::GotoLabelKind: 1244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek isFeasible = Assumption; 1254502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return St; 1264502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1274502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::ConcreteIntKind: { 1284502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; 1294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek isFeasible = b ? Assumption : !Assumption; 1304502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return St; 1314502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1324502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1334502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1344502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1354502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekconst GRState* 1364502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::Assume(const GRState* St, NonLoc Cond, bool Assumption, 1374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool& isFeasible) { 1384502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek St = AssumeAux(St, Cond, Assumption, isFeasible); 1394502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (!isFeasible) 1414502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return St; 1424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1434502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // EvalAssume is used to call into the GRTransferFunction object to perform 1444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // any checker-specific update of the state based on this assumption being 1454502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // true or false. 1464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption, 1474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek isFeasible); 1484502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1504502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekconst GRState* 1514502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::AssumeAux(const GRState* St,NonLoc Cond, 1524502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool Assumption, bool& isFeasible) { 153a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu // We cannot reason about SymIntExpr and SymSymExpr. 154a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu if (!canReasonAbout(Cond)) { 155a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu isFeasible = true; 156a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu return St; 157a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu } 158a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu 1594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek BasicValueFactory& BasicVals = StateMgr.getBasicVals(); 1604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolManager& SymMgr = StateMgr.getSymbolManager(); 1614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 1634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 1644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert(false && "'Assume' not implemented for this NonLoc"); 1654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::SymbolValKind: { 1674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); 1684502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym = SV.getSymbol(); 1694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek QualType T = SymMgr.getType(sym); 1704502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (Assumption) 1724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return AssumeSymNE(St, sym, BasicVals.getValue(0, T), isFeasible); 1734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek else 1744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return AssumeSymEQ(St, sym, BasicVals.getValue(0, T), isFeasible); 1754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1764502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 177e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case nonloc::SymExprValKind: { 178e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond); 179e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression())) 180e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return AssumeSymInt(St, Assumption, SE, isFeasible); 181e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek 182e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek isFeasible = true; 183e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return St; 184e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 1854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1864502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::ConcreteIntKind: { 1874502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; 1884502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek isFeasible = b ? Assumption : !Assumption; 1894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return St; 1904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1924502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::LocAsIntegerKind: 1934502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return AssumeAux(St, cast<nonloc::LocAsInteger>(Cond).getLoc(), 1944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek Assumption, isFeasible); 1954502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1964502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1974502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1984502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekconst GRState* 1994502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::AssumeSymInt(const GRState* St, bool Assumption, 200e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek const SymIntExpr *SE, bool& isFeasible) { 201e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek 2024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 203e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // Here we assume that LHS is a symbol. This is consistent with the 204e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // rest of the constraint manager logic. 205e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek SymbolRef Sym = cast<SymbolData>(SE->getLHS()); 206e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek const llvm::APSInt &Int = SE->getRHS(); 207e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek 208e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek switch (SE->getOpcode()) { 2094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 2104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // No logic yet for other operators. 2114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek isFeasible = true; 2124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return St; 2134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::EQ: 215e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return Assumption ? AssumeSymEQ(St, Sym, Int, isFeasible) 216e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek : AssumeSymNE(St, Sym, Int, isFeasible); 2174502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2184502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::NE: 219e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return Assumption ? AssumeSymNE(St, Sym, Int, isFeasible) 220e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek : AssumeSymEQ(St, Sym, Int, isFeasible); 2214502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2224502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::GT: 223e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return Assumption ? AssumeSymGT(St, Sym, Int, isFeasible) 224e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek : AssumeSymLE(St, Sym, Int, isFeasible); 2254502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2264502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::GE: 227e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return Assumption ? AssumeSymGE(St, Sym, Int, isFeasible) 228e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek : AssumeSymLT(St, Sym, Int, isFeasible); 2294502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2304502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::LT: 231e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return Assumption ? AssumeSymLT(St, Sym, Int, isFeasible) 232e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek : AssumeSymGE(St, Sym, Int, isFeasible); 2334502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2344502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case BinaryOperator::LE: 235e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return Assumption ? AssumeSymLE(St, Sym, Int, isFeasible) 236e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek : AssumeSymGT(St, Sym, Int, isFeasible); 2374502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2384502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2394502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2404502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenekconst GRState* 2414502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::AssumeInBound(const GRState* St, SVal Idx, 2424502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SVal UpperBound, bool Assumption, 2434502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool& isFeasible) { 2444502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // Only support ConcreteInt for now. 2454502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound))){ 2464502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek isFeasible = true; 2474502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return St; 2484502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2494502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2504502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek const llvm::APSInt& Zero = getBasicVals().getZeroWithPtrWidth(false); 2514502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue(); 2524502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // IdxV might be too narrow. 2534502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (IdxV.getBitWidth() < Zero.getBitWidth()) 2544502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek IdxV.extend(Zero.getBitWidth()); 2554502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // UBV might be too narrow, too. 2564502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue(); 2574502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (UBV.getBitWidth() < Zero.getBitWidth()) 2584502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek UBV.extend(Zero.getBitWidth()); 2594502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2604502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool InBound = (Zero <= IdxV) && (IdxV < UBV); 2614502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek isFeasible = Assumption ? InBound : !InBound; 2634502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek return St; 2654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} // end of namespace clang 268