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