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 if (NotifyAssumeClients) 71 return SU.processAssume(state, cond, assumption); 72 return state; 73 } 74 75 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 76 Loc Cond, bool Assumption) { 77 switch (Cond.getSubKind()) { 78 default: 79 assert (false && "'Assume' not implemented for this Loc."); 80 return state; 81 82 case loc::MemRegionKind: { 83 // FIXME: Should this go into the storemanager? 84 85 const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion(); 86 const SubRegion *SubR = dyn_cast<SubRegion>(R); 87 88 while (SubR) { 89 // FIXME: now we only find the first symbolic region. 90 if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { 91 const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth(); 92 if (Assumption) 93 return assumeSymNE(state, SymR->getSymbol(), zero, zero); 94 else 95 return assumeSymEQ(state, SymR->getSymbol(), zero, zero); 96 } 97 SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); 98 } 99 100 // FALL-THROUGH. 101 } 102 103 case loc::GotoLabelKind: 104 return Assumption ? state : NULL; 105 106 case loc::ConcreteIntKind: { 107 bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; 108 bool isFeasible = b ? Assumption : !Assumption; 109 return isFeasible ? state : NULL; 110 } 111 } // end switch 112 } 113 114 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, 115 NonLoc cond, 116 bool assumption) { 117 state = assumeAux(state, cond, assumption); 118 return SU.processAssume(state, cond, assumption); 119 } 120 121 static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) { 122 // FIXME: This should probably be part of BinaryOperator, since this isn't 123 // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.) 124 switch (op) { 125 default: 126 llvm_unreachable("Invalid opcode."); 127 case BO_LT: return BO_GE; 128 case BO_GT: return BO_LE; 129 case BO_LE: return BO_GT; 130 case BO_GE: return BO_LT; 131 case BO_EQ: return BO_NE; 132 case BO_NE: return BO_EQ; 133 } 134 } 135 136 137 ProgramStateRef 138 SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State, 139 SymbolRef Sym, bool Assumption) { 140 BasicValueFactory &BVF = getBasicVals(); 141 QualType T = Sym->getType(BVF.getContext()); 142 143 // None of the constraint solvers currently support non-integer types. 144 if (!T->isIntegerType()) 145 return State; 146 147 const llvm::APSInt &zero = BVF.getValue(0, T); 148 if (Assumption) 149 return assumeSymNE(State, Sym, zero, zero); 150 else 151 return assumeSymEQ(State, Sym, zero, zero); 152 } 153 154 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state, 155 NonLoc Cond, 156 bool Assumption) { 157 158 // We cannot reason about SymSymExprs, and can only reason about some 159 // SymIntExprs. 160 if (!canReasonAbout(Cond)) { 161 // Just add the constraint to the expression without trying to simplify. 162 SymbolRef sym = Cond.getAsSymExpr(); 163 return assumeAuxForSymbol(state, sym, Assumption); 164 } 165 166 BasicValueFactory &BasicVals = getBasicVals(); 167 168 switch (Cond.getSubKind()) { 169 default: 170 llvm_unreachable("'Assume' not implemented for this NonLoc"); 171 172 case nonloc::SymbolValKind: { 173 nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); 174 SymbolRef sym = SV.getSymbol(); 175 assert(sym); 176 177 // Handle SymbolData. 178 if (!SV.isExpression()) { 179 return assumeAuxForSymbol(state, sym, Assumption); 180 181 // Handle symbolic expression. 182 } else { 183 // We can only simplify expressions whose RHS is an integer. 184 const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym); 185 if (!SE) 186 return assumeAuxForSymbol(state, sym, Assumption); 187 188 BinaryOperator::Opcode op = SE->getOpcode(); 189 // Implicitly compare non-comparison expressions to 0. 190 if (!BinaryOperator::isComparisonOp(op)) { 191 QualType T = SE->getType(BasicVals.getContext()); 192 const llvm::APSInt &zero = BasicVals.getValue(0, T); 193 op = (Assumption ? BO_NE : BO_EQ); 194 return assumeSymRel(state, SE, op, zero); 195 } 196 // From here on out, op is the real comparison we'll be testing. 197 if (!Assumption) 198 op = NegateComparison(op); 199 200 return assumeSymRel(state, SE->getLHS(), op, SE->getRHS()); 201 } 202 } 203 204 case nonloc::ConcreteIntKind: { 205 bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; 206 bool isFeasible = b ? Assumption : !Assumption; 207 return isFeasible ? state : NULL; 208 } 209 210 case nonloc::LocAsIntegerKind: 211 return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), 212 Assumption); 213 } // end switch 214 } 215 216 static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) { 217 // Is it a "($sym+constant1)" expression? 218 if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) { 219 BinaryOperator::Opcode Op = SE->getOpcode(); 220 if (Op == BO_Add || Op == BO_Sub) { 221 Sym = SE->getLHS(); 222 Adjustment = APSIntType(Adjustment).convert(SE->getRHS()); 223 224 // Don't forget to negate the adjustment if it's being subtracted. 225 // This should happen /after/ promotion, in case the value being 226 // subtracted is, say, CHAR_MIN, and the promoted type is 'int'. 227 if (Op == BO_Sub) 228 Adjustment = -Adjustment; 229 } 230 } 231 } 232 233 ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state, 234 const SymExpr *LHS, 235 BinaryOperator::Opcode op, 236 const llvm::APSInt& Int) { 237 assert(BinaryOperator::isComparisonOp(op) && 238 "Non-comparison ops should be rewritten as comparisons to zero."); 239 240 BasicValueFactory &BVF = getBasicVals(); 241 ASTContext &Ctx = BVF.getContext(); 242 243 // Get the type used for calculating wraparound. 244 APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType(Ctx)); 245 246 // We only handle simple comparisons of the form "$sym == constant" 247 // or "($sym+constant1) == constant2". 248 // The adjustment is "constant1" in the above expression. It's used to 249 // "slide" the solution range around for modular arithmetic. For example, 250 // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which 251 // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to 252 // the subclasses of SimpleConstraintManager to handle the adjustment. 253 SymbolRef Sym = LHS; 254 llvm::APSInt Adjustment = WraparoundType.getZeroValue(); 255 computeAdjustment(Sym, Adjustment); 256 257 // Convert the right-hand side integer as necessary. 258 APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int)); 259 llvm::APSInt ConvertedInt = ComparisonType.convert(Int); 260 261 switch (op) { 262 default: 263 // No logic yet for other operators. assume the constraint is feasible. 264 return state; 265 266 case BO_EQ: 267 return assumeSymEQ(state, Sym, ConvertedInt, Adjustment); 268 269 case BO_NE: 270 return assumeSymNE(state, Sym, ConvertedInt, Adjustment); 271 272 case BO_GT: 273 return assumeSymGT(state, Sym, ConvertedInt, Adjustment); 274 275 case BO_GE: 276 return assumeSymGE(state, Sym, ConvertedInt, Adjustment); 277 278 case BO_LT: 279 return assumeSymLT(state, Sym, ConvertedInt, Adjustment); 280 281 case BO_LE: 282 return assumeSymLE(state, Sym, ConvertedInt, Adjustment); 283 } // end switch 284 } 285 286 } // end of namespace ento 287 288 } // end of namespace clang 289