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