SimpleConstraintManager.cpp revision 218887
1//== SimpleConstraintManager.cpp --------------------------------*- C++ -*--==// 2// 3// The LLVM Compiler Infrastructure 4// 5// This file is distributed under the University of Illinois Open Source 6// License. See LICENSE.TXT for details. 7// 8//===----------------------------------------------------------------------===// 9// 10// This file defines SimpleConstraintManager, a class that holds code shared 11// between BasicConstraintManager and RangeConstraintManager. 12// 13//===----------------------------------------------------------------------===// 14 15#include "SimpleConstraintManager.h" 16#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" 17#include "clang/StaticAnalyzer/Core/PathSensitive/GRState.h" 18#include "clang/StaticAnalyzer/Core/PathSensitive/Checker.h" 19 20namespace clang { 21 22namespace ento { 23 24SimpleConstraintManager::~SimpleConstraintManager() {} 25 26bool SimpleConstraintManager::canReasonAbout(SVal X) const { 27 if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) { 28 const SymExpr *SE = SymVal->getSymbolicExpression(); 29 30 if (isa<SymbolData>(SE)) 31 return true; 32 33 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) { 34 switch (SIE->getOpcode()) { 35 // We don't reason yet about bitwise-constraints on symbolic values. 36 case BO_And: 37 case BO_Or: 38 case BO_Xor: 39 return false; 40 // We don't reason yet about these arithmetic constraints on 41 // symbolic values. 42 case BO_Mul: 43 case BO_Div: 44 case BO_Rem: 45 case BO_Shl: 46 case BO_Shr: 47 return false; 48 // All other cases. 49 default: 50 return true; 51 } 52 } 53 54 return false; 55 } 56 57 return true; 58} 59 60const GRState *SimpleConstraintManager::assume(const GRState *state, 61 DefinedSVal Cond, 62 bool Assumption) { 63 if (isa<NonLoc>(Cond)) 64 return assume(state, cast<NonLoc>(Cond), Assumption); 65 else 66 return assume(state, cast<Loc>(Cond), Assumption); 67} 68 69const GRState *SimpleConstraintManager::assume(const GRState *state, Loc cond, 70 bool assumption) { 71 state = assumeAux(state, cond, assumption); 72 return SU.processAssume(state, cond, assumption); 73} 74 75const GRState *SimpleConstraintManager::assumeAux(const GRState *state, 76 Loc Cond, bool Assumption) { 77 78 BasicValueFactory &BasicVals = state->getBasicVals(); 79 80 switch (Cond.getSubKind()) { 81 default: 82 assert (false && "'Assume' not implemented for this Loc."); 83 return state; 84 85 case loc::MemRegionKind: { 86 // FIXME: Should this go into the storemanager? 87 88 const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion(); 89 const SubRegion *SubR = dyn_cast<SubRegion>(R); 90 91 while (SubR) { 92 // FIXME: now we only find the first symbolic region. 93 if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { 94 const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth(); 95 if (Assumption) 96 return assumeSymNE(state, SymR->getSymbol(), zero, zero); 97 else 98 return assumeSymEQ(state, SymR->getSymbol(), zero, zero); 99 } 100 SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 101 } 102 103 // FALL-THROUGH. 104 } 105 106 case loc::GotoLabelKind: 107 return Assumption ? state : NULL; 108 109 case loc::ConcreteIntKind: { 110 bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; 111 bool isFeasible = b ? Assumption : !Assumption; 112 return isFeasible ? state : NULL; 113 } 114 } // end switch 115} 116 117const GRState *SimpleConstraintManager::assume(const GRState *state, 118 NonLoc cond, 119 bool assumption) { 120 state = assumeAux(state, cond, assumption); 121 return SU.processAssume(state, cond, assumption); 122} 123 124static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) { 125 // FIXME: This should probably be part of BinaryOperator, since this isn't 126 // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.) 127 switch (op) { 128 default: 129 assert(false && "Invalid opcode."); 130 case BO_LT: return BO_GE; 131 case BO_GT: return BO_LE; 132 case BO_LE: return BO_GT; 133 case BO_GE: return BO_LT; 134 case BO_EQ: return BO_NE; 135 case BO_NE: return BO_EQ; 136 } 137} 138 139const GRState *SimpleConstraintManager::assumeAux(const GRState *state, 140 NonLoc Cond, 141 bool Assumption) { 142 143 // We cannot reason about SymSymExprs, 144 // and can only reason about some SymIntExprs. 145 if (!canReasonAbout(Cond)) { 146 // Just return the current state indicating that the path is feasible. 147 // This may be an over-approximation of what is possible. 148 return state; 149 } 150 151 BasicValueFactory &BasicVals = state->getBasicVals(); 152 SymbolManager &SymMgr = state->getSymbolManager(); 153 154 switch (Cond.getSubKind()) { 155 default: 156 assert(false && "'Assume' not implemented for this NonLoc"); 157 158 case nonloc::SymbolValKind: { 159 nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); 160 SymbolRef sym = SV.getSymbol(); 161 QualType T = SymMgr.getType(sym); 162 const llvm::APSInt &zero = BasicVals.getValue(0, T); 163 if (Assumption) 164 return assumeSymNE(state, sym, zero, zero); 165 else 166 return assumeSymEQ(state, sym, zero, zero); 167 } 168 169 case nonloc::SymExprValKind: { 170 nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond); 171 172 // For now, we only handle expressions whose RHS is an integer. 173 // All other expressions are assumed to be feasible. 174 const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression()); 175 if (!SE) 176 return state; 177 178 BinaryOperator::Opcode op = SE->getOpcode(); 179 // Implicitly compare non-comparison expressions to 0. 180 if (!BinaryOperator::isComparisonOp(op)) { 181 QualType T = SymMgr.getType(SE); 182 const llvm::APSInt &zero = BasicVals.getValue(0, T); 183 op = (Assumption ? BO_NE : BO_EQ); 184 return assumeSymRel(state, SE, op, zero); 185 } 186 187 // From here on out, op is the real comparison we'll be testing. 188 if (!Assumption) 189 op = NegateComparison(op); 190 191 return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 192 } 193 194 case nonloc::ConcreteIntKind: { 195 bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; 196 bool isFeasible = b ? Assumption : !Assumption; 197 return isFeasible ? state : NULL; 198 } 199 200 case nonloc::LocAsIntegerKind: 201 return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), 202 Assumption); 203 } // end switch 204} 205 206const GRState *SimpleConstraintManager::assumeSymRel(const GRState *state, 207 const SymExpr *LHS, 208 BinaryOperator::Opcode op, 209 const llvm::APSInt& Int) { 210 assert(BinaryOperator::isComparisonOp(op) && 211 "Non-comparison ops should be rewritten as comparisons to zero."); 212 213 // We only handle simple comparisons of the form "$sym == constant" 214 // or "($sym+constant1) == constant2". 215 // The adjustment is "constant1" in the above expression. It's used to 216 // "slide" the solution range around for modular arithmetic. For example, 217 // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 218 // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 219 // the subclasses of SimpleConstraintManager to handle the adjustment. 220 llvm::APSInt Adjustment; 221 222 // First check if the LHS is a simple symbol reference. 223 SymbolRef Sym = dyn_cast<SymbolData>(LHS); 224 if (Sym) { 225 Adjustment = 0; 226 } else { 227 // Next, see if it's a "($sym+constant1)" expression. 228 const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS); 229 230 // We don't handle "($sym1+$sym2)". 231 // Give up and assume the constraint is feasible. 232 if (!SE) 233 return state; 234 235 // We don't handle "(<expr>+constant1)". 236 // Give up and assume the constraint is feasible. 237 Sym = dyn_cast<SymbolData>(SE->getLHS()); 238 if (!Sym) 239 return state; 240 241 // Get the constant out of the expression "($sym+constant1)". 242 switch (SE->getOpcode()) { 243 case BO_Add: 244 Adjustment = SE->getRHS(); 245 break; 246 case BO_Sub: 247 Adjustment = -SE->getRHS(); 248 break; 249 default: 250 // We don't handle non-additive operators. 251 // Give up and assume the constraint is feasible. 252 return state; 253 } 254 } 255 256 // FIXME: This next section is a hack. It silently converts the integers to 257 // be of the same type as the symbol, which is not always correct. Really the 258 // comparisons should be performed using the Int's type, then mapped back to 259 // the symbol's range of values. 260 GRStateManager &StateMgr = state->getStateManager(); 261 ASTContext &Ctx = StateMgr.getContext(); 262 263 QualType T = Sym->getType(Ctx); 264 assert(T->isIntegerType() || Loc::isLocType(T)); 265 unsigned bitwidth = Ctx.getTypeSize(T); 266 bool isSymUnsigned = T->isUnsignedIntegerType() || Loc::isLocType(T); 267 268 // Convert the adjustment. 269 Adjustment.setIsUnsigned(isSymUnsigned); 270 Adjustment = Adjustment.extOrTrunc(bitwidth); 271 272 // Convert the right-hand side integer. 273 llvm::APSInt ConvertedInt(Int, isSymUnsigned); 274 ConvertedInt = ConvertedInt.extOrTrunc(bitwidth); 275 276 switch (op) { 277 default: 278 // No logic yet for other operators. assume the constraint is feasible. 279 return state; 280 281 case BO_EQ: 282 return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 283 284 case BO_NE: 285 return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 286 287 case BO_GT: 288 return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 289 290 case BO_GE: 291 return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 292 293 case BO_LT: 294 return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 295 296 case BO_LE: 297 return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 298 } // end switch 299} 300 301} // end of namespace ento 302 303} // end of namespace clang 304