1218887Sdim//== SimpleConstraintManager.cpp --------------------------------*- C++ -*--==// 2218887Sdim// 3218887Sdim// The LLVM Compiler Infrastructure 4218887Sdim// 5218887Sdim// This file is distributed under the University of Illinois Open Source 6218887Sdim// License. See LICENSE.TXT for details. 7218887Sdim// 8218887Sdim//===----------------------------------------------------------------------===// 9218887Sdim// 10218887Sdim// This file defines SimpleConstraintManager, a class that holds code shared 11218887Sdim// between BasicConstraintManager and RangeConstraintManager. 12218887Sdim// 13218887Sdim//===----------------------------------------------------------------------===// 14218887Sdim 15218887Sdim#include "SimpleConstraintManager.h" 16239462Sdim#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" 17218887Sdim#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" 18226633Sdim#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 19218887Sdim 20218887Sdimnamespace clang { 21218887Sdim 22218887Sdimnamespace ento { 23218887Sdim 24218887SdimSimpleConstraintManager::~SimpleConstraintManager() {} 25218887Sdim 26218887Sdimbool SimpleConstraintManager::canReasonAbout(SVal X) const { 27249423Sdim Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>(); 28234353Sdim if (SymVal && SymVal->isExpression()) { 29234353Sdim const SymExpr *SE = SymVal->getSymbol(); 30218887Sdim 31218887Sdim if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) { 32218887Sdim switch (SIE->getOpcode()) { 33218887Sdim // We don't reason yet about bitwise-constraints on symbolic values. 34218887Sdim case BO_And: 35218887Sdim case BO_Or: 36218887Sdim case BO_Xor: 37218887Sdim return false; 38218887Sdim // We don't reason yet about these arithmetic constraints on 39218887Sdim // symbolic values. 40218887Sdim case BO_Mul: 41218887Sdim case BO_Div: 42218887Sdim case BO_Rem: 43218887Sdim case BO_Shl: 44218887Sdim case BO_Shr: 45218887Sdim return false; 46218887Sdim // All other cases. 47218887Sdim default: 48218887Sdim return true; 49218887Sdim } 50218887Sdim } 51218887Sdim 52249423Sdim if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) { 53249423Sdim if (BinaryOperator::isComparisonOp(SSE->getOpcode())) { 54249423Sdim // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc. 55249423Sdim if (Loc::isLocType(SSE->getLHS()->getType())) { 56249423Sdim assert(Loc::isLocType(SSE->getRHS()->getType())); 57249423Sdim return true; 58249423Sdim } 59249423Sdim } 60249423Sdim } 61249423Sdim 62218887Sdim return false; 63218887Sdim } 64218887Sdim 65218887Sdim return true; 66218887Sdim} 67218887Sdim 68234353SdimProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 69218887Sdim DefinedSVal Cond, 70218887Sdim bool Assumption) { 71263508Sdim // If we have a Loc value, cast it to a bool NonLoc first. 72263508Sdim if (Optional<Loc> LV = Cond.getAs<Loc>()) { 73263508Sdim SValBuilder &SVB = state->getStateManager().getSValBuilder(); 74263508Sdim QualType T; 75263508Sdim const MemRegion *MR = LV->getAsRegion(); 76263508Sdim if (const TypedRegion *TR = dyn_cast_or_null<TypedRegion>(MR)) 77263508Sdim T = TR->getLocationType(); 78263508Sdim else 79263508Sdim T = SVB.getContext().VoidPtrTy; 80218887Sdim 81263508Sdim Cond = SVB.evalCast(*LV, SVB.getContext().BoolTy, T).castAs<DefinedSVal>(); 82218887Sdim } 83218887Sdim 84263508Sdim return assume(state, Cond.castAs<NonLoc>(), Assumption); 85218887Sdim} 86218887Sdim 87234353SdimProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 88218887Sdim NonLoc cond, 89218887Sdim bool assumption) { 90218887Sdim state = assumeAux(state, cond, assumption); 91243830Sdim if (NotifyAssumeClients && SU) 92243830Sdim return SU->processAssume(state, cond, assumption); 93243830Sdim return state; 94218887Sdim} 95218887Sdim 96218887Sdim 97239462SdimProgramStateRef 98239462SdimSimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State, 99239462Sdim SymbolRef Sym, bool Assumption) { 100239462Sdim BasicValueFactory &BVF = getBasicVals(); 101243830Sdim QualType T = Sym->getType(); 102239462Sdim 103239462Sdim // None of the constraint solvers currently support non-integer types. 104251662Sdim if (!T->isIntegralOrEnumerationType()) 105239462Sdim return State; 106239462Sdim 107239462Sdim const llvm::APSInt &zero = BVF.getValue(0, T); 108234353Sdim if (Assumption) 109234353Sdim return assumeSymNE(State, Sym, zero, zero); 110234353Sdim else 111234353Sdim return assumeSymEQ(State, Sym, zero, zero); 112234353Sdim} 113234353Sdim 114234353SdimProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 115218887Sdim NonLoc Cond, 116218887Sdim bool Assumption) { 117218887Sdim 118234353Sdim // We cannot reason about SymSymExprs, and can only reason about some 119234353Sdim // SymIntExprs. 120218887Sdim if (!canReasonAbout(Cond)) { 121234353Sdim // Just add the constraint to the expression without trying to simplify. 122234353Sdim SymbolRef sym = Cond.getAsSymExpr(); 123234353Sdim return assumeAuxForSymbol(state, sym, Assumption); 124218887Sdim } 125218887Sdim 126218887Sdim switch (Cond.getSubKind()) { 127218887Sdim default: 128226633Sdim llvm_unreachable("'Assume' not implemented for this NonLoc"); 129218887Sdim 130218887Sdim case nonloc::SymbolValKind: { 131249423Sdim nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>(); 132218887Sdim SymbolRef sym = SV.getSymbol(); 133234353Sdim assert(sym); 134218887Sdim 135234353Sdim // Handle SymbolData. 136234353Sdim if (!SV.isExpression()) { 137234353Sdim return assumeAuxForSymbol(state, sym, Assumption); 138218887Sdim 139234353Sdim // Handle symbolic expression. 140249423Sdim } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym)) { 141234353Sdim // We can only simplify expressions whose RHS is an integer. 142218887Sdim 143234353Sdim BinaryOperator::Opcode op = SE->getOpcode(); 144249423Sdim if (BinaryOperator::isComparisonOp(op)) { 145249423Sdim if (!Assumption) 146249423Sdim op = BinaryOperator::negateComparisonOp(op); 147249423Sdim 148249423Sdim return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 149234353Sdim } 150249423Sdim 151249423Sdim } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) { 152249423Sdim // Translate "a != b" to "(b - a) != 0". 153249423Sdim // We invert the order of the operands as a heuristic for how loop 154249423Sdim // conditions are usually written ("begin != end") as compared to length 155249423Sdim // calculations ("end - begin"). The more correct thing to do would be to 156249423Sdim // canonicalize "a - b" and "b - a", which would allow us to treat 157249423Sdim // "a != b" and "b != a" the same. 158249423Sdim SymbolManager &SymMgr = getSymbolManager(); 159249423Sdim BinaryOperator::Opcode Op = SSE->getOpcode(); 160249423Sdim assert(BinaryOperator::isComparisonOp(Op)); 161249423Sdim 162249423Sdim // For now, we only support comparing pointers. 163249423Sdim assert(Loc::isLocType(SSE->getLHS()->getType())); 164249423Sdim assert(Loc::isLocType(SSE->getRHS()->getType())); 165249423Sdim QualType DiffTy = SymMgr.getContext().getPointerDiffType(); 166249423Sdim SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, 167249423Sdim SSE->getLHS(), DiffTy); 168249423Sdim 169249423Sdim const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy); 170249423Sdim Op = BinaryOperator::reverseComparisonOp(Op); 171234353Sdim if (!Assumption) 172249423Sdim Op = BinaryOperator::negateComparisonOp(Op); 173249423Sdim return assumeSymRel(state, Subtraction, Op, Zero); 174249423Sdim } 175234353Sdim 176249423Sdim // If we get here, there's nothing else we can do but treat the symbol as 177249423Sdim // opaque. 178249423Sdim return assumeAuxForSymbol(state, sym, Assumption); 179218887Sdim } 180218887Sdim 181218887Sdim case nonloc::ConcreteIntKind: { 182249423Sdim bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0; 183218887Sdim bool isFeasible = b ? Assumption : !Assumption; 184218887Sdim return isFeasible ? state : NULL; 185218887Sdim } 186218887Sdim 187218887Sdim case nonloc::LocAsIntegerKind: 188263508Sdim return assume(state, Cond.castAs<nonloc::LocAsInteger>().getLoc(), 189263508Sdim Assumption); 190218887Sdim } // end switch 191218887Sdim} 192218887Sdim 193239462Sdimstatic void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { 194239462Sdim // Is it a "($sym+constant1)" expression? 195239462Sdim if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) { 196239462Sdim BinaryOperator::Opcode Op = SE->getOpcode(); 197239462Sdim if (Op == BO_Add || Op == BO_Sub) { 198239462Sdim Sym = SE->getLHS(); 199239462Sdim Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); 200234353Sdim 201239462Sdim // Don't forget to negate the adjustment if it's being subtracted. 202239462Sdim // This should happen /after/ promotion, in case the value being 203239462Sdim // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. 204239462Sdim if (Op == BO_Sub) 205239462Sdim Adjustment = -Adjustment; 206239462Sdim } 207234353Sdim } 208234353Sdim} 209234353Sdim 210234353SdimProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state, 211218887Sdim const SymExpr *LHS, 212218887Sdim BinaryOperator::Opcode op, 213218887Sdim const llvm::APSInt& Int) { 214218887Sdim assert(BinaryOperator::isComparisonOp(op) && 215218887Sdim "Non-comparison ops should be rewritten as comparisons to zero."); 216218887Sdim 217243830Sdim // Get the type used for calculating wraparound. 218239462Sdim BasicValueFactory &BVF = getBasicVals(); 219243830Sdim APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType()); 220239462Sdim 221234353Sdim // We only handle simple comparisons of the form "$sym == constant" 222234353Sdim // or "($sym+constant1) == constant2". 223234353Sdim // The adjustment is "constant1" in the above expression. It's used to 224234353Sdim // "slide" the solution range around for modular arithmetic. For example, 225234353Sdim // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 226234353Sdim // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 227234353Sdim // the subclasses of SimpleConstraintManager to handle the adjustment. 228234353Sdim SymbolRef Sym = LHS; 229239462Sdim llvm::APSInt Adjustment = WraparoundType.getZeroValue(); 230239462Sdim computeAdjustment(Sym, Adjustment); 231218887Sdim 232239462Sdim // Convert the right-hand side integer as necessary. 233239462Sdim APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); 234239462Sdim llvm::APSInt ConvertedInt = ComparisonType.convert(Int); 235218887Sdim 236249423Sdim // Prefer unsigned comparisons. 237249423Sdim if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() && 238249423Sdim ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) 239249423Sdim Adjustment.setIsSigned(false); 240249423Sdim 241218887Sdim switch (op) { 242218887Sdim default: 243249423Sdim llvm_unreachable("invalid operation not caught by assertion above"); 244218887Sdim 245218887Sdim case BO_EQ: 246218887Sdim return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 247218887Sdim 248218887Sdim case BO_NE: 249218887Sdim return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 250218887Sdim 251218887Sdim case BO_GT: 252218887Sdim return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 253218887Sdim 254218887Sdim case BO_GE: 255218887Sdim return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 256218887Sdim 257218887Sdim case BO_LT: 258218887Sdim return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 259218887Sdim 260218887Sdim case BO_LE: 261218887Sdim return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 262218887Sdim } // end switch 263218887Sdim} 264218887Sdim 265218887Sdim} // end of namespace ento 266218887Sdim 267218887Sdim} // end of namespace clang 268