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