1 //== BasicConstraintManager.cpp - Manage basic constraints.------*- 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 BasicConstraintManager, a class that tracks simple 11 // equality and inequality constraints on symbolic values of ProgramState. 12 // 13 //===----------------------------------------------------------------------===// 14 15 #include "SimpleConstraintManager.h" 16 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" 17 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" 18 #include "llvm/Support/raw_ostream.h" 19 20 using namespace clang; 21 using namespace ento; 22 23 24 namespace { class ConstNotEq {}; } 25 namespace { class ConstEq {}; } 26 27 typedef llvm::ImmutableMap<SymbolRef,ProgramState::IntSetTy> ConstNotEqTy; 28 typedef llvm::ImmutableMap<SymbolRef,const llvm::APSInt*> ConstEqTy; 29 30 static int ConstEqIndex = 0; 31 static int ConstNotEqIndex = 0; 32 33 namespace clang { 34 namespace ento { 35 template<> 36 struct ProgramStateTrait<ConstNotEq> : 37 public ProgramStatePartialTrait<ConstNotEqTy> { 38 static inline void *GDMIndex() { return &ConstNotEqIndex; } 39 }; 40 41 template<> 42 struct ProgramStateTrait<ConstEq> : public ProgramStatePartialTrait<ConstEqTy> { 43 static inline void *GDMIndex() { return &ConstEqIndex; } 44 }; 45 } 46 } 47 48 namespace { 49 // BasicConstraintManager only tracks equality and inequality constraints of 50 // constants and integer variables. 51 class BasicConstraintManager 52 : public SimpleConstraintManager { 53 ProgramState::IntSetTy::Factory ISetFactory; 54 public: 55 BasicConstraintManager(ProgramStateManager &statemgr, SubEngine &subengine) 56 : SimpleConstraintManager(subengine), 57 ISetFactory(statemgr.getAllocator()) {} 58 59 ProgramStateRef assumeSymNE(ProgramStateRef state, 60 SymbolRef sym, 61 const llvm::APSInt& V, 62 const llvm::APSInt& Adjustment); 63 64 ProgramStateRef assumeSymEQ(ProgramStateRef state, 65 SymbolRef sym, 66 const llvm::APSInt& V, 67 const llvm::APSInt& Adjustment); 68 69 ProgramStateRef assumeSymLT(ProgramStateRef state, 70 SymbolRef sym, 71 const llvm::APSInt& V, 72 const llvm::APSInt& Adjustment); 73 74 ProgramStateRef assumeSymGT(ProgramStateRef state, 75 SymbolRef sym, 76 const llvm::APSInt& V, 77 const llvm::APSInt& Adjustment); 78 79 ProgramStateRef assumeSymGE(ProgramStateRef state, 80 SymbolRef sym, 81 const llvm::APSInt& V, 82 const llvm::APSInt& Adjustment); 83 84 ProgramStateRef assumeSymLE(ProgramStateRef state, 85 SymbolRef sym, 86 const llvm::APSInt& V, 87 const llvm::APSInt& Adjustment); 88 89 ProgramStateRef AddEQ(ProgramStateRef state, 90 SymbolRef sym, 91 const llvm::APSInt& V); 92 93 ProgramStateRef AddNE(ProgramStateRef state, 94 SymbolRef sym, 95 const llvm::APSInt& V); 96 97 const llvm::APSInt* getSymVal(ProgramStateRef state, 98 SymbolRef sym) const; 99 100 bool isNotEqual(ProgramStateRef state, 101 SymbolRef sym, 102 const llvm::APSInt& V) const; 103 104 bool isEqual(ProgramStateRef state, 105 SymbolRef sym, 106 const llvm::APSInt& V) const; 107 108 ProgramStateRef removeDeadBindings(ProgramStateRef state, 109 SymbolReaper& SymReaper); 110 111 void print(ProgramStateRef state, 112 raw_ostream &Out, 113 const char* nl, 114 const char *sep); 115 }; 116 117 } // end anonymous namespace 118 119 ConstraintManager* 120 ento::CreateBasicConstraintManager(ProgramStateManager& statemgr, 121 SubEngine &subengine) { 122 return new BasicConstraintManager(statemgr, subengine); 123 } 124 125 ProgramStateRef 126 BasicConstraintManager::assumeSymNE(ProgramStateRef state, 127 SymbolRef sym, 128 const llvm::APSInt &V, 129 const llvm::APSInt &Adjustment) { 130 // First, determine if sym == X, where X+Adjustment != V. 131 llvm::APSInt Adjusted = V-Adjustment; 132 if (const llvm::APSInt* X = getSymVal(state, sym)) { 133 bool isFeasible = (*X != Adjusted); 134 return isFeasible ? state : NULL; 135 } 136 137 // Second, determine if sym+Adjustment != V. 138 if (isNotEqual(state, sym, Adjusted)) 139 return state; 140 141 // If we reach here, sym is not a constant and we don't know if it is != V. 142 // Make that assumption. 143 return AddNE(state, sym, Adjusted); 144 } 145 146 ProgramStateRef 147 BasicConstraintManager::assumeSymEQ(ProgramStateRef state, 148 SymbolRef sym, 149 const llvm::APSInt &V, 150 const llvm::APSInt &Adjustment) { 151 // First, determine if sym == X, where X+Adjustment != V. 152 llvm::APSInt Adjusted = V-Adjustment; 153 if (const llvm::APSInt* X = getSymVal(state, sym)) { 154 bool isFeasible = (*X == Adjusted); 155 return isFeasible ? state : NULL; 156 } 157 158 // Second, determine if sym+Adjustment != V. 159 if (isNotEqual(state, sym, Adjusted)) 160 return NULL; 161 162 // If we reach here, sym is not a constant and we don't know if it is == V. 163 // Make that assumption. 164 return AddEQ(state, sym, Adjusted); 165 } 166 167 // The logic for these will be handled in another ConstraintManager. 168 ProgramStateRef 169 BasicConstraintManager::assumeSymLT(ProgramStateRef state, 170 SymbolRef sym, 171 const llvm::APSInt &V, 172 const llvm::APSInt &Adjustment) { 173 // Is 'V' the smallest possible value? 174 if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) { 175 // sym cannot be any value less than 'V'. This path is infeasible. 176 return NULL; 177 } 178 179 // FIXME: For now have assuming x < y be the same as assuming sym != V; 180 return assumeSymNE(state, sym, V, Adjustment); 181 } 182 183 ProgramStateRef 184 BasicConstraintManager::assumeSymGT(ProgramStateRef state, 185 SymbolRef sym, 186 const llvm::APSInt &V, 187 const llvm::APSInt &Adjustment) { 188 // Is 'V' the largest possible value? 189 if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) { 190 // sym cannot be any value greater than 'V'. This path is infeasible. 191 return NULL; 192 } 193 194 // FIXME: For now have assuming x > y be the same as assuming sym != V; 195 return assumeSymNE(state, sym, V, Adjustment); 196 } 197 198 ProgramStateRef 199 BasicConstraintManager::assumeSymGE(ProgramStateRef state, 200 SymbolRef sym, 201 const llvm::APSInt &V, 202 const llvm::APSInt &Adjustment) { 203 // Reject a path if the value of sym is a constant X and !(X+Adj >= V). 204 if (const llvm::APSInt *X = getSymVal(state, sym)) { 205 bool isFeasible = (*X >= V-Adjustment); 206 return isFeasible ? state : NULL; 207 } 208 209 // Sym is not a constant, but it is worth looking to see if V is the 210 // maximum integer value. 211 if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) { 212 llvm::APSInt Adjusted = V-Adjustment; 213 214 // If we know that sym != V (after adjustment), then this condition 215 // is infeasible since there is no other value greater than V. 216 bool isFeasible = !isNotEqual(state, sym, Adjusted); 217 218 // If the path is still feasible then as a consequence we know that 219 // 'sym+Adjustment == V' because there are no larger values. 220 // Add this constraint. 221 return isFeasible ? AddEQ(state, sym, Adjusted) : NULL; 222 } 223 224 return state; 225 } 226 227 ProgramStateRef 228 BasicConstraintManager::assumeSymLE(ProgramStateRef state, 229 SymbolRef sym, 230 const llvm::APSInt &V, 231 const llvm::APSInt &Adjustment) { 232 // Reject a path if the value of sym is a constant X and !(X+Adj <= V). 233 if (const llvm::APSInt* X = getSymVal(state, sym)) { 234 bool isFeasible = (*X <= V-Adjustment); 235 return isFeasible ? state : NULL; 236 } 237 238 // Sym is not a constant, but it is worth looking to see if V is the 239 // minimum integer value. 240 if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) { 241 llvm::APSInt Adjusted = V-Adjustment; 242 243 // If we know that sym != V (after adjustment), then this condition 244 // is infeasible since there is no other value less than V. 245 bool isFeasible = !isNotEqual(state, sym, Adjusted); 246 247 // If the path is still feasible then as a consequence we know that 248 // 'sym+Adjustment == V' because there are no smaller values. 249 // Add this constraint. 250 return isFeasible ? AddEQ(state, sym, Adjusted) : NULL; 251 } 252 253 return state; 254 } 255 256 ProgramStateRef BasicConstraintManager::AddEQ(ProgramStateRef state, 257 SymbolRef sym, 258 const llvm::APSInt& V) { 259 // Create a new state with the old binding replaced. 260 return state->set<ConstEq>(sym, &state->getBasicVals().getValue(V)); 261 } 262 263 ProgramStateRef BasicConstraintManager::AddNE(ProgramStateRef state, 264 SymbolRef sym, 265 const llvm::APSInt& V) { 266 267 // First, retrieve the NE-set associated with the given symbol. 268 ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym); 269 ProgramState::IntSetTy S = T ? *T : ISetFactory.getEmptySet(); 270 271 // Now add V to the NE set. 272 S = ISetFactory.add(S, &state->getBasicVals().getValue(V)); 273 274 // Create a new state with the old binding replaced. 275 return state->set<ConstNotEq>(sym, S); 276 } 277 278 const llvm::APSInt* BasicConstraintManager::getSymVal(ProgramStateRef state, 279 SymbolRef sym) const { 280 const ConstEqTy::data_type* T = state->get<ConstEq>(sym); 281 return T ? *T : NULL; 282 } 283 284 bool BasicConstraintManager::isNotEqual(ProgramStateRef state, 285 SymbolRef sym, 286 const llvm::APSInt& V) const { 287 288 // Retrieve the NE-set associated with the given symbol. 289 const ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym); 290 291 // See if V is present in the NE-set. 292 return T ? T->contains(&state->getBasicVals().getValue(V)) : false; 293 } 294 295 bool BasicConstraintManager::isEqual(ProgramStateRef state, 296 SymbolRef sym, 297 const llvm::APSInt& V) const { 298 // Retrieve the EQ-set associated with the given symbol. 299 const ConstEqTy::data_type* T = state->get<ConstEq>(sym); 300 // See if V is present in the EQ-set. 301 return T ? **T == V : false; 302 } 303 304 /// Scan all symbols referenced by the constraints. If the symbol is not alive 305 /// as marked in LSymbols, mark it as dead in DSymbols. 306 ProgramStateRef 307 BasicConstraintManager::removeDeadBindings(ProgramStateRef state, 308 SymbolReaper& SymReaper) { 309 310 ConstEqTy CE = state->get<ConstEq>(); 311 ConstEqTy::Factory& CEFactory = state->get_context<ConstEq>(); 312 313 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) { 314 SymbolRef sym = I.getKey(); 315 if (SymReaper.maybeDead(sym)) 316 CE = CEFactory.remove(CE, sym); 317 } 318 state = state->set<ConstEq>(CE); 319 320 ConstNotEqTy CNE = state->get<ConstNotEq>(); 321 ConstNotEqTy::Factory& CNEFactory = state->get_context<ConstNotEq>(); 322 323 for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) { 324 SymbolRef sym = I.getKey(); 325 if (SymReaper.maybeDead(sym)) 326 CNE = CNEFactory.remove(CNE, sym); 327 } 328 329 return state->set<ConstNotEq>(CNE); 330 } 331 332 void BasicConstraintManager::print(ProgramStateRef state, 333 raw_ostream &Out, 334 const char* nl, const char *sep) { 335 // Print equality constraints. 336 337 ConstEqTy CE = state->get<ConstEq>(); 338 339 if (!CE.isEmpty()) { 340 Out << nl << sep << "'==' constraints:"; 341 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) 342 Out << nl << " $" << I.getKey() << " : " << *I.getData(); 343 } 344 345 // Print != constraints. 346 347 ConstNotEqTy CNE = state->get<ConstNotEq>(); 348 349 if (!CNE.isEmpty()) { 350 Out << nl << sep << "'!=' constraints:"; 351 352 for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) { 353 Out << nl << " $" << I.getKey() << " : "; 354 bool isFirst = true; 355 356 ProgramState::IntSetTy::iterator J = I.getData().begin(), 357 EJ = I.getData().end(); 358 359 for ( ; J != EJ; ++J) { 360 if (isFirst) isFirst = false; 361 else Out << ", "; 362 363 Out << (*J)->getSExtValue(); // Hack: should print to raw_ostream. 364 } 365 } 366 } 367 } 368
