SimpleConstraintManager.cpp revision 76462f00854171d2aa3ebc34f9aac1c60021b0ea
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" 169b663716449b618ba0390b1dbebc54fa8e971124Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" 1718c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 184502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 194502195fecf399fdbbb9ee2393ad08148c394179Ted Kremeneknamespace clang { 204502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 219ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremeneknamespace ento { 225a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 234502195fecf399fdbbb9ee2393ad08148c394179Ted KremenekSimpleConstraintManager::~SimpleConstraintManager() {} 244502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2566b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenekbool SimpleConstraintManager::canReasonAbout(SVal X) const { 26e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) { 27e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek const SymExpr *SE = SymVal->getSymbolicExpression(); 281eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 29e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (isa<SymbolData>(SE)) 30e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return true; 311eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 32e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) { 33e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek switch (SIE->getOpcode()) { 34e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // We don't reason yet about bitwise-constraints on symbolic values. 352de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_And: 362de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Or: 372de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Xor: 38e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 39ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // We don't reason yet about these arithmetic constraints on 40ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // symbolic values. 412de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Mul: 422de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Div: 432de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Rem: 442de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Shl: 452de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_Shr: 46e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 47e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek // All other cases. 48e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek default: 49e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return true; 501eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 51e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 52e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek 53e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek return false; 547de20fe9aac00705dd943690563db66fa4b35b5bTed Kremenek } 557de20fe9aac00705dd943690563db66fa4b35b5bTed Kremenek 5666b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek return true; 5766b527193aa6f3aa94c03f6769c42d7642e1e147Ted Kremenek} 581eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 5918c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assume(const ProgramState *state, 605b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek DefinedSVal Cond, 615b9bd2137ebef350af803c634e3fdf5d74678100Ted Kremenek bool Assumption) { 624502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek if (isa<NonLoc>(Cond)) 6328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assume(state, cast<NonLoc>(Cond), Assumption); 644502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek else 6528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assume(state, cast<Loc>(Cond), Assumption); 664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 6818c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assume(const ProgramState *state, Loc cond, 6932a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 7028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 71e36de1fe51c39d9161915dd3dbef880954af6476Ted Kremenek return SU.processAssume(state, cond, assumption); 724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 734502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 7418c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state, 75a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Loc Cond, bool Assumption) { 761eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 77a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicValueFactory &BasicVals = state->getBasicVals(); 784502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 794502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 804502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 814502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek assert (false && "'Assume' not implemented for this Loc."); 82a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 834502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 844502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::MemRegionKind: { 854502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: Should this go into the storemanager? 861eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 87a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion(); 88a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek const SubRegion *SubR = dyn_cast<SubRegion>(R); 894502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 904502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek while (SubR) { 914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FIXME: now we only find the first symbolic region. 92a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { 93ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth(); 943330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu if (Assumption) 9528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, SymR->getSymbol(), zero, zero); 963330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu else 9728f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, SymR->getSymbol(), zero, zero); 983330dcb0da654fb06e78dc410ba15ab90c1b08e7Zhongxing Xu } 994502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 1004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1011eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek // FALL-THROUGH. 1034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1041eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1054502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::GotoLabelKind: 106a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return Assumption ? state : NULL; 1074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1084502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case loc::ConcreteIntKind: { 1091eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; 110a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 111a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 1124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 1144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 1154502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 11618c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assume(const ProgramState *state, 11732a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek NonLoc cond, 11832a58084a4c53e6938dd81bfce224db25a5976d1Ted Kremenek bool assumption) { 11928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek state = assumeAux(state, cond, assumption); 120e36de1fe51c39d9161915dd3dbef880954af6476Ted Kremenek return SU.processAssume(state, cond, assumption); 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 1393cdf584e068056540769dab56cad333e95a89750Anna Zaksconst ProgramState *SimpleConstraintManager::assumeAuxForSymbol( 1403cdf584e068056540769dab56cad333e95a89750Anna Zaks const ProgramState *State, 1413cdf584e068056540769dab56cad333e95a89750Anna Zaks SymbolRef Sym, 1423cdf584e068056540769dab56cad333e95a89750Anna Zaks bool Assumption) { 1433cdf584e068056540769dab56cad333e95a89750Anna Zaks QualType T = State->getSymbolManager().getType(Sym); 1443cdf584e068056540769dab56cad333e95a89750Anna Zaks const llvm::APSInt &zero = State->getBasicVals().getValue(0, T); 1453cdf584e068056540769dab56cad333e95a89750Anna Zaks if (Assumption) 1463cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymNE(State, Sym, zero, zero); 1473cdf584e068056540769dab56cad333e95a89750Anna Zaks else 1483cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeSymEQ(State, Sym, zero, zero); 1493cdf584e068056540769dab56cad333e95a89750Anna Zaks} 1503cdf584e068056540769dab56cad333e95a89750Anna Zaks 15118c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state, 152a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek NonLoc Cond, 153a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool Assumption) { 1541eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1553cdf584e068056540769dab56cad333e95a89750Anna Zaks // We cannot reason about SymSymExprs, and can only reason about some 1563cdf584e068056540769dab56cad333e95a89750Anna Zaks // SymIntExprs. 157a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu if (!canReasonAbout(Cond)) { 1583cdf584e068056540769dab56cad333e95a89750Anna Zaks // Just add the constraint to the expression without trying to simplify. 1593cdf584e068056540769dab56cad333e95a89750Anna Zaks SymbolRef sym = Cond.getAsSymExpr(); 1603cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 1611eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump } 162a129eb974d8ff0ad4a4dd94ad1e6c5f98897ddb4Zhongxing Xu 163a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek BasicValueFactory &BasicVals = state->getBasicVals(); 164a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek SymbolManager &SymMgr = state->getSymbolManager(); 1654502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1664502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek switch (Cond.getSubKind()) { 1674502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 168b219cfc4d75f0a03630b7c4509ef791b7e97b2c8David Blaikie llvm_unreachable("'Assume' not implemented for this NonLoc"); 1694502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 1704502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::SymbolValKind: { 1714502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); 1724502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek SymbolRef sym = SV.getSymbol(); 1733cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 1744502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 1754502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 176e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek case nonloc::SymExprValKind: { 177e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond); 1781eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 1793cdf584e068056540769dab56cad333e95a89750Anna Zaks SymbolRef sym = V.getSymbolicExpression(); 1803cdf584e068056540769dab56cad333e95a89750Anna Zaks assert(sym); 1813cdf584e068056540769dab56cad333e95a89750Anna Zaks 1823cdf584e068056540769dab56cad333e95a89750Anna Zaks // We can only simplify expressions whose RHS is an integer. 1833cdf584e068056540769dab56cad333e95a89750Anna Zaks const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym); 184ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!SE) 1853cdf584e068056540769dab56cad333e95a89750Anna Zaks return assumeAuxForSymbol(state, sym, Assumption); 186ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 187ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op = SE->getOpcode(); 1885ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose // Implicitly compare non-comparison expressions to 0. 1895ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose if (!BinaryOperator::isComparisonOp(op)) { 1905ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose QualType T = SymMgr.getType(SE); 1915ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose const llvm::APSInt &zero = BasicVals.getValue(0, T); 1922de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall op = (Assumption ? BO_NE : BO_EQ); 19328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymRel(state, SE, op, zero); 1945ca129c2558a13d7d4b2b76fee8404bc07466ce9Jordy Rose } 195ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 196ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose // From here on out, op is the real comparison we'll be testing. 197ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose if (!Assumption) 198ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose op = NegateComparison(op); 199ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 20028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 201e0e4ebf6bfca5a71b2344d8a1b748b852509279cTed Kremenek } 2024502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::ConcreteIntKind: { 2044502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; 205a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek bool isFeasible = b ? Assumption : !Assumption; 206a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return isFeasible ? state : NULL; 2074502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } 2084502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek case nonloc::LocAsIntegerKind: 21028f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), 211a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek Assumption); 2124502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 2134502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 2144502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 21576462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaksstatic llvm::APSInt computeAdjustment(const SymExpr *LHS, 21676462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks SymbolRef &Sym) { 21776462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks llvm::APSInt DefaultAdjustment; 21876462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks DefaultAdjustment = 0; 21976462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks 22076462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // First check if the LHS is a simple symbol reference. 22176462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks if (isa<SymbolData>(LHS)) 22276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks return DefaultAdjustment; 22376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks 22476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // Next, see if it's a "($sym+constant1)" expression. 22576462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS); 22676462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks 22776462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // We cannot simplify "($sym1+$sym2)". 22876462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks if (!SE) 22976462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks return DefaultAdjustment; 23076462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks 23176462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // Get the constant out of the expression "($sym+constant1)" or 23276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // "<expr>+constant1". 23376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks Sym = SE->getLHS(); 23476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks switch (SE->getOpcode()) { 23576462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks case BO_Add: 23676462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks return SE->getRHS(); 23776462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks break; 23876462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks case BO_Sub: 23976462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks return -SE->getRHS(); 24076462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks break; 24176462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks default: 24276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // We cannot simplify non-additive operators. 24376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks return DefaultAdjustment; 24476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks } 24576462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks 24676462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks return DefaultAdjustment; 24776462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks} 24876462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks 24918c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenekconst ProgramState *SimpleConstraintManager::assumeSymRel(const ProgramState *state, 250ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const SymExpr *LHS, 251ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose BinaryOperator::Opcode op, 252ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose const llvm::APSInt& Int) { 253ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose assert(BinaryOperator::isComparisonOp(op) && 254ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose "Non-comparison ops should be rewritten as comparisons to zero."); 255ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 25676462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // We only handle simple comparisons of the form "$sym == constant" 25776462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // or "($sym+constant1) == constant2". 25876462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // The adjustment is "constant1" in the above expression. It's used to 25976462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // "slide" the solution range around for modular arithmetic. For example, 26076462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 26176462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 26276462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks // the subclasses of SimpleConstraintManager to handle the adjustment. 26376462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks SymbolRef Sym = LHS; 26476462f00854171d2aa3ebc34f9aac1c60021b0eaAnna Zaks llvm::APSInt Adjustment = computeAdjustment(LHS, Sym); 2651eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 266b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // FIXME: This next section is a hack. It silently converts the integers to 267b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // be of the same type as the symbol, which is not always correct. Really the 268b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // comparisons should be performed using the Int's type, then mapped back to 269b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // the symbol's range of values. 27018c66fdc3c4008d335885695fe36fb5353c5f672Ted Kremenek ProgramStateManager &StateMgr = state->getStateManager(); 271b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose ASTContext &Ctx = StateMgr.getContext(); 272b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 273b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose QualType T = Sym->getType(Ctx); 2747dfc9420babe83e236a47e752f8723bd06070d9dZhanyong Wan assert(T->isIntegerType() || Loc::isLocType(T)); 275b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose unsigned bitwidth = Ctx.getTypeSize(T); 2765e9ebb3c0fb554d9285aa99c470abdf283272bd9Douglas Gregor bool isSymUnsigned 2775e9ebb3c0fb554d9285aa99c470abdf283272bd9Douglas Gregor = T->isUnsignedIntegerOrEnumerationType() || Loc::isLocType(T); 278b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 279b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // Convert the adjustment. 280b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose Adjustment.setIsUnsigned(isSymUnsigned); 2819f71a8f4c7a182a5236da9e747d57cc1d1bd24c2Jay Foad Adjustment = Adjustment.extOrTrunc(bitwidth); 282b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 283b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose // Convert the right-hand side integer. 284b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose llvm::APSInt ConvertedInt(Int, isSymUnsigned); 2859f71a8f4c7a182a5236da9e747d57cc1d1bd24c2Jay Foad ConvertedInt = ConvertedInt.extOrTrunc(bitwidth); 286b4954a4175b36d912bdfc43834d09754faddd855Jordy Rose 287ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose switch (op) { 2884502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek default: 28928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek // No logic yet for other operators. assume the constraint is feasible. 290a591bc04d21fa62ebffcb2c7814d738ca8f5e2f9Ted Kremenek return state; 2914502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2922de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_EQ: 29328f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 2944502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 2952de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_NE: 29628f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 297ba0f61cf5363f80e3241dc754235dfb246afe320Jordy Rose 2982de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GT: 29928f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 3004502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3012de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_GE: 30228f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 3034502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3042de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LT: 30528f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 3061eb4433ac451dc16f4133a88af2d002ac26c58efMike Stump 3072de56d1d0c3a504ad1529de2677628bdfbb95cd4John McCall case BO_LE: 30828f47b92e760ccf641ac91cb0fe1c12d9ca89795Ted Kremenek return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 3094502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek } // end switch 3104502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek} 3114502195fecf399fdbbb9ee2393ad08148c394179Ted Kremenek 3129ef6537a894c33003359b1f9b9676e9178e028b7Ted Kremenek} // end of namespace ento 3135a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis 3145a4f98ff943e6a501b0fe47ade007c9bbf96cb88Argyrios Kyrtzidis} // end of namespace clang 315