contrib/llvm/tools/clang/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp

   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   const ProgramState *assumeSymNE(const ProgramState *state,
  60                                   SymbolRef sym,
  61                                   const llvm::APSInt& V,
  62                                   const llvm::APSInt& Adjustment);
  63
  64   const ProgramState *assumeSymEQ(const ProgramState *state,
  65                                   SymbolRef sym,
  66                                   const llvm::APSInt& V,
  67                                   const llvm::APSInt& Adjustment);
  68
  69   const ProgramState *assumeSymLT(const ProgramState *state,
  70                                   SymbolRef sym,
  71                                   const llvm::APSInt& V,
  72                                   const llvm::APSInt& Adjustment);
  73
  74   const ProgramState *assumeSymGT(const ProgramState *state,
  75                                   SymbolRef sym,
  76                                   const llvm::APSInt& V,
  77                                   const llvm::APSInt& Adjustment);
  78
  79   const ProgramState *assumeSymGE(const ProgramState *state,
  80                                   SymbolRef sym,
  81                                   const llvm::APSInt& V,
  82                                   const llvm::APSInt& Adjustment);
  83
  84   const ProgramState *assumeSymLE(const ProgramState *state,
  85                                   SymbolRef sym,
  86                                   const llvm::APSInt& V,
  87                                   const llvm::APSInt& Adjustment);
  88
  89   const ProgramState *AddEQ(const ProgramState *state,
  90                             SymbolRef sym,
  91                             const llvm::APSInt& V);
  92
  93   const ProgramState *AddNE(const ProgramState *state,
  94                             SymbolRef sym,
  95                             const llvm::APSInt& V);
  96
  97   const llvm::APSInt* getSymVal(const ProgramState *state,
  98                                 SymbolRef sym) const;
  99
 100   bool isNotEqual(const ProgramState *state,
 101                   SymbolRef sym,
 102                   const llvm::APSInt& V) const;
 103
 104   bool isEqual(const ProgramState *state,
 105                SymbolRef sym,
 106                const llvm::APSInt& V) const;
 107
 108   const ProgramState *removeDeadBindings(const ProgramState *state,
 109                                          SymbolReaper& SymReaper);
 110
 111   void print(const ProgramState *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 const ProgramState*
 126 BasicConstraintManager::assumeSymNE(const ProgramState *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 const ProgramState*
 147 BasicConstraintManager::assumeSymEQ(const ProgramState *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 const ProgramState*
 169 BasicConstraintManager::assumeSymLT(const ProgramState *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 const ProgramState*
 184 BasicConstraintManager::assumeSymGT(const ProgramState *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 const ProgramState*
 199 BasicConstraintManager::assumeSymGE(const ProgramState *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 const ProgramState*
 228 BasicConstraintManager::assumeSymLE(const ProgramState *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 const ProgramState *BasicConstraintManager::AddEQ(const ProgramState *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 const ProgramState *BasicConstraintManager::AddNE(const ProgramState *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(const ProgramState *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(const ProgramState *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(const ProgramState *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 const ProgramState*
 307 BasicConstraintManager::removeDeadBindings(const ProgramState *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(const ProgramState *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 }