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/APSIntType.h" 17 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" 18 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 19 20 namespace clang { 21 22 namespace ento { 23 24 SimpleConstraintManager::~SimpleConstraintManager() {} 25 26 bool SimpleConstraintManager::canReasonAbout(SVal X) const { 27 nonloc::SymbolVal *SymVal = dyn_cast<nonloc::SymbolVal>(&X); 28 if (SymVal && SymVal->isExpression()) { 29 const SymExpr *SE = SymVal->getSymbol(); 30 31 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) { 32 switch (SIE->getOpcode()) { 33 // We don't reason yet about bitwise-constraints on symbolic values. 34 case BO_And: 35 case BO_Or: 36 case BO_Xor: 37 return false; 38 // We don't reason yet about these arithmetic constraints on 39 // symbolic values. 40 case BO_Mul: 41 case BO_Div: 42 case BO_Rem: 43 case BO_Shl: 44 case BO_Shr: 45 return false; 46 // All other cases. 47 default: 48 return true; 49 } 50 } 51 52 return false; 53 } 54 55 return true; 56 } 57 58 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 59 DefinedSVal Cond, 60 bool Assumption) { 61 if (isa<NonLoc>(Cond)) 62 return assume(state, cast<NonLoc>(Cond), Assumption); 63 else 64 return assume(state, cast<Loc>(Cond), Assumption); 65 } 66 67 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond, 68 bool assumption) { 69 state = assumeAux(state, cond, assumption); 70 return SU.processAssume(state, cond, assumption); 71 } 72 73 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 74 Loc Cond, bool Assumption) { 75 switch (Cond.getSubKind()) { 76 default: 77 assert (false && "'Assume' not implemented for this Loc."); 78 return state; 79 80 case loc::MemRegionKind: { 81 // FIXME: Should this go into the storemanager? 82 83 const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion(); 84 const SubRegion *SubR = dyn_cast<SubRegion>(R); 85 86 while (SubR) { 87 if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) 88 return assumeAuxForSymbol(state, SymR->getSymbol(), Assumption); 89 90 SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 91 } 92 93 // FALL-THROUGH. 94 } 95 96 case loc::GotoLabelKind: 97 return Assumption ? state : NULL; 98 99 case loc::ConcreteIntKind: { 100 bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; 101 bool isFeasible = b ? Assumption : !Assumption; 102 return isFeasible ? state : NULL; 103 } 104 } // end switch 105 } 106 107 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 108 NonLoc cond, 109 bool assumption) { 110 state = assumeAux(state, cond, assumption); 111 return SU.processAssume(state, cond, assumption); 112 } 113 114 static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) { 115 // FIXME: This should probably be part of BinaryOperator, since this isn't 116 // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.) 117 switch (op) { 118 default: 119 llvm_unreachable("Invalid opcode."); 120 case BO_LT: return BO_GE; 121 case BO_GT: return BO_LE; 122 case BO_LE: return BO_GT; 123 case BO_GE: return BO_LT; 124 case BO_EQ: return BO_NE; 125 case BO_NE: return BO_EQ; 126 } 127 } 128 129 130 ProgramStateRef 131 SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State, 132 SymbolRef Sym, bool Assumption) { 133 BasicValueFactory &BVF = getBasicVals(); 134 QualType T = Sym->getType(BVF.getContext()); 135 136 // Don't do anything if this isn't a type we can constrain. 137 if (!(T->isIntegralOrEnumerationType() || Loc::isLocType(T))) 138 return State; 139 140 if (T->isReferenceType()) 141 return Assumption ? State : NULL; 142 143 const llvm::APSInt &zero = BVF.getValue(0, T); 144 if (Assumption) 145 return assumeSymNE(State, Sym, zero, zero); 146 else 147 return assumeSymEQ(State, Sym, zero, zero); 148 } 149 150 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 151 NonLoc Cond, 152 bool Assumption) { 153 154 // We cannot reason about SymSymExprs, and can only reason about some 155 // SymIntExprs. 156 if (!canReasonAbout(Cond)) { 157 // Just add the constraint to the expression without trying to simplify. 158 SymbolRef sym = Cond.getAsSymExpr(); 159 return assumeAuxForSymbol(state, sym, Assumption); 160 } 161 162 switch (Cond.getSubKind()) { 163 default: 164 llvm_unreachable("'Assume' not implemented for this NonLoc"); 165 166 case nonloc::SymbolValKind: { 167 nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); 168 SymbolRef sym = SV.getSymbol(); 169 assert(sym); 170 171 // Handle SymbolData. 172 if (!SV.isExpression()) { 173 return assumeAuxForSymbol(state, sym, Assumption); 174 175 // Handle symbolic expression. 176 } else { 177 // We can only simplify expressions whose RHS is an integer. 178 const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym); 179 if (!SE) 180 return assumeAuxForSymbol(state, sym, Assumption); 181 182 BinaryOperator::Opcode op = SE->getOpcode(); 183 // Implicitly compare non-comparison expressions to 0. 184 if (!BinaryOperator::isComparisonOp(op)) 185 return assumeAuxForSymbol(state, SE, Assumption); 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 195 case nonloc::ConcreteIntKind: { 196 bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; 197 bool isFeasible = b ? Assumption : !Assumption; 198 return isFeasible ? state : NULL; 199 } 200 201 case nonloc::LocAsIntegerKind: 202 return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), 203 Assumption); 204 } // end switch 205 } 206 207 static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { 208 // Is it a "($sym+constant1)" expression? 209 if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) { 210 BinaryOperator::Opcode Op = SE->getOpcode(); 211 if (Op == BO_Add || Op == BO_Sub) { 212 Sym = SE->getLHS(); 213 Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); 214 215 // Don't forget to negate the adjustment if it's being subtracted. 216 // This should happen /after/ promotion, in case the value being 217 // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. 218 if (Op == BO_Sub) 219 Adjustment = -Adjustment; 220 } 221 } 222 } 223 224 ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state, 225 const SymExpr *LHS, 226 BinaryOperator::Opcode op, 227 const llvm::APSInt& Int) { 228 assert(BinaryOperator::isComparisonOp(op) && 229 "Non-comparison ops should be rewritten as comparisons to zero."); 230 231 BasicValueFactory &BVF = getBasicVals(); 232 ASTContext &Ctx = BVF.getContext(); 233 234 // Special case for references, which cannot be null. 235 QualType Ty = LHS->getType(Ctx); 236 if (Ty->isReferenceType() && Int == 0) { 237 switch (op) { 238 case BO_EQ: 239 case BO_LE: 240 case BO_LT: 241 return NULL; 242 case BO_NE: 243 case BO_GT: 244 case BO_GE: 245 return state; 246 default: 247 llvm_unreachable("We should only be handling comparisons here."); 248 } 249 } 250 251 // Get the type used for calculating wraparound. 252 APSIntType WraparoundType = BVF.getAPSIntType(Ty); 253 254 // We only handle simple comparisons of the form "$sym == constant" 255 // or "($sym+constant1) == constant2". 256 // The adjustment is "constant1" in the above expression. It's used to 257 // "slide" the solution range around for modular arithmetic. For example, 258 // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 259 // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 260 // the subclasses of SimpleConstraintManager to handle the adjustment. 261 SymbolRef Sym = LHS; 262 llvm::APSInt Adjustment = WraparoundType.getZeroValue(); 263 computeAdjustment(Sym, Adjustment); 264 265 // Convert the right-hand side integer as necessary. 266 APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); 267 llvm::APSInt ConvertedInt = ComparisonType.convert(Int); 268 269 switch (op) { 270 default: 271 // No logic yet for other operators. assume the constraint is feasible. 272 return state; 273 274 case BO_EQ: 275 return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 276 277 case BO_NE: 278 return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 279 280 case BO_GT: 281 return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 282 283 case BO_GE: 284 return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 285 286 case BO_LT: 287 return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 288 289 case BO_LE: 290 return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 291 } // end switch 292 } 293 294 } // end of namespace ento 295 296 } // end of namespace clang 297