SimpleConstraintManager.cpp revision 251662
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) { 71249423Sdim if (Optional<NonLoc> NV = Cond.getAs<NonLoc>()) 72249423Sdim return assume(state, *NV, Assumption); 73249423Sdim return assume(state, Cond.castAs<Loc>(), Assumption); 74218887Sdim} 75218887Sdim 76234353SdimProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond, 77218887Sdim bool assumption) { 78218887Sdim state = assumeAux(state, cond, assumption); 79243830Sdim if (NotifyAssumeClients && SU) 80243830Sdim return SU->processAssume(state, cond, assumption); 81243830Sdim return state; 82218887Sdim} 83218887Sdim 84234353SdimProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 85218887Sdim Loc Cond, bool Assumption) { 86218887Sdim switch (Cond.getSubKind()) { 87218887Sdim default: 88218887Sdim assert (false && "'Assume' not implemented for this Loc."); 89218887Sdim return state; 90218887Sdim 91218887Sdim case loc::MemRegionKind: { 92218887Sdim // FIXME: Should this go into the storemanager? 93249423Sdim const MemRegion *R = Cond.castAs<loc::MemRegionVal>().getRegion(); 94218887Sdim 95251662Sdim // FIXME: now we only find the first symbolic region. 96251662Sdim if (const SymbolicRegion *SymR = R->getSymbolicBase()) { 97251662Sdim const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth(); 98251662Sdim if (Assumption) 99251662Sdim return assumeSymNE(state, SymR->getSymbol(), zero, zero); 100251662Sdim else 101251662Sdim return assumeSymEQ(state, SymR->getSymbol(), zero, zero); 102218887Sdim } 103218887Sdim 104218887Sdim // FALL-THROUGH. 105218887Sdim } 106218887Sdim 107218887Sdim case loc::GotoLabelKind: 108218887Sdim return Assumption ? state : NULL; 109218887Sdim 110218887Sdim case loc::ConcreteIntKind: { 111249423Sdim bool b = Cond.castAs<loc::ConcreteInt>().getValue() != 0; 112218887Sdim bool isFeasible = b ? Assumption : !Assumption; 113218887Sdim return isFeasible ? state : NULL; 114218887Sdim } 115218887Sdim } // end switch 116218887Sdim} 117218887Sdim 118234353SdimProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 119218887Sdim NonLoc cond, 120218887Sdim bool assumption) { 121218887Sdim state = assumeAux(state, cond, assumption); 122243830Sdim if (NotifyAssumeClients && SU) 123243830Sdim return SU->processAssume(state, cond, assumption); 124243830Sdim return state; 125218887Sdim} 126218887Sdim 127218887Sdim 128239462SdimProgramStateRef 129239462SdimSimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State, 130239462Sdim SymbolRef Sym, bool Assumption) { 131239462Sdim BasicValueFactory &BVF = getBasicVals(); 132243830Sdim QualType T = Sym->getType(); 133239462Sdim 134239462Sdim // None of the constraint solvers currently support non-integer types. 135251662Sdim if (!T->isIntegralOrEnumerationType()) 136239462Sdim return State; 137239462Sdim 138239462Sdim const llvm::APSInt &zero = BVF.getValue(0, T); 139234353Sdim if (Assumption) 140234353Sdim return assumeSymNE(State, Sym, zero, zero); 141234353Sdim else 142234353Sdim return assumeSymEQ(State, Sym, zero, zero); 143234353Sdim} 144234353Sdim 145234353SdimProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 146218887Sdim NonLoc Cond, 147218887Sdim bool Assumption) { 148218887Sdim 149234353Sdim // We cannot reason about SymSymExprs, and can only reason about some 150234353Sdim // SymIntExprs. 151218887Sdim if (!canReasonAbout(Cond)) { 152234353Sdim // Just add the constraint to the expression without trying to simplify. 153234353Sdim SymbolRef sym = Cond.getAsSymExpr(); 154234353Sdim return assumeAuxForSymbol(state, sym, Assumption); 155218887Sdim } 156218887Sdim 157218887Sdim switch (Cond.getSubKind()) { 158218887Sdim default: 159226633Sdim llvm_unreachable("'Assume' not implemented for this NonLoc"); 160218887Sdim 161218887Sdim case nonloc::SymbolValKind: { 162249423Sdim nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>(); 163218887Sdim SymbolRef sym = SV.getSymbol(); 164234353Sdim assert(sym); 165218887Sdim 166234353Sdim // Handle SymbolData. 167234353Sdim if (!SV.isExpression()) { 168234353Sdim return assumeAuxForSymbol(state, sym, Assumption); 169218887Sdim 170234353Sdim // Handle symbolic expression. 171249423Sdim } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym)) { 172234353Sdim // We can only simplify expressions whose RHS is an integer. 173218887Sdim 174234353Sdim BinaryOperator::Opcode op = SE->getOpcode(); 175249423Sdim if (BinaryOperator::isComparisonOp(op)) { 176249423Sdim if (!Assumption) 177249423Sdim op = BinaryOperator::negateComparisonOp(op); 178249423Sdim 179249423Sdim return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 180234353Sdim } 181249423Sdim 182249423Sdim } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) { 183249423Sdim // Translate "a != b" to "(b - a) != 0". 184249423Sdim // We invert the order of the operands as a heuristic for how loop 185249423Sdim // conditions are usually written ("begin != end") as compared to length 186249423Sdim // calculations ("end - begin"). The more correct thing to do would be to 187249423Sdim // canonicalize "a - b" and "b - a", which would allow us to treat 188249423Sdim // "a != b" and "b != a" the same. 189249423Sdim SymbolManager &SymMgr = getSymbolManager(); 190249423Sdim BinaryOperator::Opcode Op = SSE->getOpcode(); 191249423Sdim assert(BinaryOperator::isComparisonOp(Op)); 192249423Sdim 193249423Sdim // For now, we only support comparing pointers. 194249423Sdim assert(Loc::isLocType(SSE->getLHS()->getType())); 195249423Sdim assert(Loc::isLocType(SSE->getRHS()->getType())); 196249423Sdim QualType DiffTy = SymMgr.getContext().getPointerDiffType(); 197249423Sdim SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, 198249423Sdim SSE->getLHS(), DiffTy); 199249423Sdim 200249423Sdim const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy); 201249423Sdim Op = BinaryOperator::reverseComparisonOp(Op); 202234353Sdim if (!Assumption) 203249423Sdim Op = BinaryOperator::negateComparisonOp(Op); 204249423Sdim return assumeSymRel(state, Subtraction, Op, Zero); 205249423Sdim } 206234353Sdim 207249423Sdim // If we get here, there's nothing else we can do but treat the symbol as 208249423Sdim // opaque. 209249423Sdim return assumeAuxForSymbol(state, sym, Assumption); 210218887Sdim } 211218887Sdim 212218887Sdim case nonloc::ConcreteIntKind: { 213249423Sdim bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0; 214218887Sdim bool isFeasible = b ? Assumption : !Assumption; 215218887Sdim return isFeasible ? state : NULL; 216218887Sdim } 217218887Sdim 218218887Sdim case nonloc::LocAsIntegerKind: 219249423Sdim return assumeAux(state, Cond.castAs<nonloc::LocAsInteger>().getLoc(), 220218887Sdim Assumption); 221218887Sdim } // end switch 222218887Sdim} 223218887Sdim 224239462Sdimstatic void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { 225239462Sdim // Is it a "($sym+constant1)" expression? 226239462Sdim if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) { 227239462Sdim BinaryOperator::Opcode Op = SE->getOpcode(); 228239462Sdim if (Op == BO_Add || Op == BO_Sub) { 229239462Sdim Sym = SE->getLHS(); 230239462Sdim Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); 231234353Sdim 232239462Sdim // Don't forget to negate the adjustment if it's being subtracted. 233239462Sdim // This should happen /after/ promotion, in case the value being 234239462Sdim // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. 235239462Sdim if (Op == BO_Sub) 236239462Sdim Adjustment = -Adjustment; 237239462Sdim } 238234353Sdim } 239234353Sdim} 240234353Sdim 241234353SdimProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state, 242218887Sdim const SymExpr *LHS, 243218887Sdim BinaryOperator::Opcode op, 244218887Sdim const llvm::APSInt& Int) { 245218887Sdim assert(BinaryOperator::isComparisonOp(op) && 246218887Sdim "Non-comparison ops should be rewritten as comparisons to zero."); 247218887Sdim 248243830Sdim // Get the type used for calculating wraparound. 249239462Sdim BasicValueFactory &BVF = getBasicVals(); 250243830Sdim APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType()); 251239462Sdim 252234353Sdim // We only handle simple comparisons of the form "$sym == constant" 253234353Sdim // or "($sym+constant1) == constant2". 254234353Sdim // The adjustment is "constant1" in the above expression. It's used to 255234353Sdim // "slide" the solution range around for modular arithmetic. For example, 256234353Sdim // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 257234353Sdim // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 258234353Sdim // the subclasses of SimpleConstraintManager to handle the adjustment. 259234353Sdim SymbolRef Sym = LHS; 260239462Sdim llvm::APSInt Adjustment = WraparoundType.getZeroValue(); 261239462Sdim computeAdjustment(Sym, Adjustment); 262218887Sdim 263239462Sdim // Convert the right-hand side integer as necessary. 264239462Sdim APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); 265239462Sdim llvm::APSInt ConvertedInt = ComparisonType.convert(Int); 266218887Sdim 267249423Sdim // Prefer unsigned comparisons. 268249423Sdim if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() && 269249423Sdim ComparisonType.isUnsigned() && !WraparoundType.isUnsigned()) 270249423Sdim Adjustment.setIsSigned(false); 271249423Sdim 272218887Sdim switch (op) { 273218887Sdim default: 274249423Sdim llvm_unreachable("invalid operation not caught by assertion above"); 275218887Sdim 276218887Sdim case BO_EQ: 277218887Sdim return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 278218887Sdim 279218887Sdim case BO_NE: 280218887Sdim return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 281218887Sdim 282218887Sdim case BO_GT: 283218887Sdim return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 284218887Sdim 285218887Sdim case BO_GE: 286218887Sdim return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 287218887Sdim 288218887Sdim case BO_LT: 289218887Sdim return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 290218887Sdim 291218887Sdim case BO_LE: 292218887Sdim return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 293218887Sdim } // end switch 294218887Sdim} 295218887Sdim 296218887Sdim} // end of namespace ento 297218887Sdim 298218887Sdim} // end of namespace clang 299