Zhongxing Xu | d19e21b | 2008-08-29 15:09:12 +0000 | [diff] [blame] | 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 GRState. |
| 12 | // |
| 13 | //===----------------------------------------------------------------------===// |
| 14 | |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 15 | #include "clang/Analysis/PathSensitive/ConstraintManager.h" |
| 16 | #include "clang/Analysis/PathSensitive/GRState.h" |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 17 | #include "clang/Analysis/PathSensitive/GRStateTrait.h" |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 18 | #include "llvm/Support/Compiler.h" |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 19 | #include "llvm/Support/raw_ostream.h" |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 20 | |
| 21 | using namespace clang; |
| 22 | |
| 23 | namespace { |
| 24 | |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 25 | typedef llvm::ImmutableMap<SymbolID,GRState::IntSetTy> ConstNotEqTy; |
| 26 | typedef llvm::ImmutableMap<SymbolID,const llvm::APSInt*> ConstEqTy; |
| 27 | |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 28 | // BasicConstraintManager only tracks equality and inequality constraints of |
| 29 | // constants and integer variables. |
| 30 | class VISIBILITY_HIDDEN BasicConstraintManager : public ConstraintManager { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 31 | GRStateManager& StateMgr; |
Zhongxing Xu | f0bc50e | 2008-11-27 06:08:40 +0000 | [diff] [blame] | 32 | GRState::IntSetTy::Factory ISetFactory; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 33 | public: |
Zhongxing Xu | f0bc50e | 2008-11-27 06:08:40 +0000 | [diff] [blame] | 34 | BasicConstraintManager(GRStateManager& statemgr) |
| 35 | : StateMgr(statemgr), ISetFactory(statemgr.getAllocator()) {} |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 36 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 37 | virtual const GRState* Assume(const GRState* St, SVal Cond, |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 38 | bool Assumption, bool& isFeasible); |
| 39 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 40 | const GRState* Assume(const GRState* St, Loc Cond, bool Assumption, |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 41 | bool& isFeasible); |
| 42 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 43 | const GRState* AssumeAux(const GRState* St, Loc Cond,bool Assumption, |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 44 | bool& isFeasible); |
| 45 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 46 | const GRState* Assume(const GRState* St, NonLoc Cond, bool Assumption, |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 47 | bool& isFeasible); |
| 48 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 49 | const GRState* AssumeAux(const GRState* St, NonLoc Cond, bool Assumption, |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 50 | bool& isFeasible); |
| 51 | |
| 52 | const GRState* AssumeSymInt(const GRState* St, bool Assumption, |
| 53 | const SymIntConstraint& C, bool& isFeasible); |
| 54 | |
| 55 | const GRState* AssumeSymNE(const GRState* St, SymbolID sym, |
| 56 | const llvm::APSInt& V, bool& isFeasible); |
| 57 | |
| 58 | const GRState* AssumeSymEQ(const GRState* St, SymbolID sym, |
| 59 | const llvm::APSInt& V, bool& isFeasible); |
| 60 | |
| 61 | const GRState* AssumeSymLT(const GRState* St, SymbolID sym, |
| 62 | const llvm::APSInt& V, bool& isFeasible); |
| 63 | |
| 64 | const GRState* AssumeSymGT(const GRState* St, SymbolID sym, |
| 65 | const llvm::APSInt& V, bool& isFeasible); |
| 66 | |
| 67 | const GRState* AssumeSymGE(const GRState* St, SymbolID sym, |
| 68 | const llvm::APSInt& V, bool& isFeasible); |
| 69 | |
| 70 | const GRState* AssumeSymLE(const GRState* St, SymbolID sym, |
| 71 | const llvm::APSInt& V, bool& isFeasible); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 72 | |
Zhongxing Xu | e8a964b | 2008-11-22 13:21:46 +0000 | [diff] [blame] | 73 | const GRState* AssumeInBound(const GRState* St, SVal Idx, SVal UpperBound, |
| 74 | bool Assumption, bool& isFeasible); |
| 75 | |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 76 | const GRState* AddEQ(const GRState* St, SymbolID sym, const llvm::APSInt& V); |
| 77 | |
| 78 | const GRState* AddNE(const GRState* St, SymbolID sym, const llvm::APSInt& V); |
| 79 | |
| 80 | const llvm::APSInt* getSymVal(const GRState* St, SymbolID sym); |
| 81 | bool isNotEqual(const GRState* St, SymbolID sym, const llvm::APSInt& V) const; |
| 82 | bool isEqual(const GRState* St, SymbolID sym, const llvm::APSInt& V) const; |
| 83 | |
| 84 | const GRState* RemoveDeadBindings(const GRState* St, |
| 85 | StoreManager::LiveSymbolsTy& LSymbols, |
| 86 | StoreManager::DeadSymbolsTy& DSymbols); |
| 87 | |
| 88 | void print(const GRState* St, std::ostream& Out, |
| 89 | const char* nl, const char *sep); |
Zhongxing Xu | e8a964b | 2008-11-22 13:21:46 +0000 | [diff] [blame] | 90 | |
| 91 | private: |
| 92 | BasicValueFactory& getBasicVals() { return StateMgr.getBasicVals(); } |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 93 | }; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 94 | |
| 95 | } // end anonymous namespace |
| 96 | |
| 97 | ConstraintManager* clang::CreateBasicConstraintManager(GRStateManager& StateMgr) |
| 98 | { |
| 99 | return new BasicConstraintManager(StateMgr); |
| 100 | } |
| 101 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 102 | const GRState* BasicConstraintManager::Assume(const GRState* St, SVal Cond, |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 103 | bool Assumption, bool& isFeasible) { |
| 104 | if (Cond.isUnknown()) { |
| 105 | isFeasible = true; |
| 106 | return St; |
| 107 | } |
| 108 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 109 | if (isa<NonLoc>(Cond)) |
| 110 | return Assume(St, cast<NonLoc>(Cond), Assumption, isFeasible); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 111 | else |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 112 | return Assume(St, cast<Loc>(Cond), Assumption, isFeasible); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 113 | } |
| 114 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 115 | const GRState* BasicConstraintManager::Assume(const GRState* St, Loc Cond, |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 116 | bool Assumption, bool& isFeasible) { |
| 117 | St = AssumeAux(St, Cond, Assumption, isFeasible); |
| 118 | // TF->EvalAssume(*this, St, Cond, Assumption, isFeasible) |
| 119 | return St; |
| 120 | } |
| 121 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 122 | const GRState* BasicConstraintManager::AssumeAux(const GRState* St, Loc Cond, |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 123 | bool Assumption, bool& isFeasible) { |
| 124 | BasicValueFactory& BasicVals = StateMgr.getBasicVals(); |
| 125 | |
| 126 | switch (Cond.getSubKind()) { |
| 127 | default: |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 128 | assert (false && "'Assume' not implemented for this Loc."); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 129 | return St; |
| 130 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 131 | case loc::SymbolValKind: |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 132 | if (Assumption) |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 133 | return AssumeSymNE(St, cast<loc::SymbolVal>(Cond).getSymbol(), |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 134 | BasicVals.getZeroWithPtrWidth(), isFeasible); |
| 135 | else |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 136 | return AssumeSymEQ(St, cast<loc::SymbolVal>(Cond).getSymbol(), |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 137 | BasicVals.getZeroWithPtrWidth(), isFeasible); |
| 138 | |
Ted Kremenek | c523471 | 2008-10-17 21:22:20 +0000 | [diff] [blame] | 139 | case loc::MemRegionKind: { |
| 140 | // FIXME: Should this go into the storemanager? |
| 141 | |
| 142 | const MemRegion* R = cast<loc::MemRegionVal>(Cond).getRegion(); |
| 143 | |
| 144 | while (R) { |
| 145 | if (const SubRegion* SubR = dyn_cast<SubRegion>(R)) { |
| 146 | R = SubR->getSuperRegion(); |
| 147 | continue; |
| 148 | } |
| 149 | else if (const SymbolicRegion* SymR = dyn_cast<SymbolicRegion>(R)) |
| 150 | return AssumeAux(St, loc::SymbolVal(SymR->getSymbol()), Assumption, |
| 151 | isFeasible); |
| 152 | |
| 153 | break; |
| 154 | } |
| 155 | |
| 156 | // FALL-THROUGH. |
| 157 | } |
| 158 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 159 | case loc::FuncValKind: |
| 160 | case loc::GotoLabelKind: |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 161 | isFeasible = Assumption; |
| 162 | return St; |
| 163 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 164 | case loc::ConcreteIntKind: { |
| 165 | bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 166 | isFeasible = b ? Assumption : !Assumption; |
| 167 | return St; |
| 168 | } |
| 169 | } // end switch |
| 170 | } |
| 171 | |
| 172 | const GRState* |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 173 | BasicConstraintManager::Assume(const GRState* St, NonLoc Cond, bool Assumption, |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 174 | bool& isFeasible) { |
| 175 | St = AssumeAux(St, Cond, Assumption, isFeasible); |
| 176 | // TF->EvalAssume() does nothing now. |
| 177 | return St; |
| 178 | } |
| 179 | |
| 180 | const GRState* |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 181 | BasicConstraintManager::AssumeAux(const GRState* St,NonLoc Cond, |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 182 | bool Assumption, bool& isFeasible) { |
| 183 | BasicValueFactory& BasicVals = StateMgr.getBasicVals(); |
| 184 | SymbolManager& SymMgr = StateMgr.getSymbolManager(); |
| 185 | |
| 186 | switch (Cond.getSubKind()) { |
| 187 | default: |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 188 | assert(false && "'Assume' not implemented for this NonLoc"); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 189 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 190 | case nonloc::SymbolValKind: { |
| 191 | nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 192 | SymbolID sym = SV.getSymbol(); |
| 193 | |
| 194 | if (Assumption) |
| 195 | return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)), |
| 196 | isFeasible); |
| 197 | else |
| 198 | return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)), |
| 199 | isFeasible); |
| 200 | } |
| 201 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 202 | case nonloc::SymIntConstraintValKind: |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 203 | return |
| 204 | AssumeSymInt(St, Assumption, |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 205 | cast<nonloc::SymIntConstraintVal>(Cond).getConstraint(), |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 206 | isFeasible); |
| 207 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 208 | case nonloc::ConcreteIntKind: { |
| 209 | bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 210 | isFeasible = b ? Assumption : !Assumption; |
| 211 | return St; |
| 212 | } |
| 213 | |
Zhongxing Xu | 1c96b24 | 2008-10-17 05:57:07 +0000 | [diff] [blame] | 214 | case nonloc::LocAsIntegerKind: |
| 215 | return AssumeAux(St, cast<nonloc::LocAsInteger>(Cond).getLoc(), |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 216 | Assumption, isFeasible); |
| 217 | } // end switch |
| 218 | } |
| 219 | |
| 220 | const GRState* |
| 221 | BasicConstraintManager::AssumeSymInt(const GRState* St, bool Assumption, |
| 222 | const SymIntConstraint& C, bool& isFeasible) { |
| 223 | |
| 224 | switch (C.getOpcode()) { |
| 225 | default: |
| 226 | // No logic yet for other operators. |
| 227 | isFeasible = true; |
| 228 | return St; |
| 229 | |
| 230 | case BinaryOperator::EQ: |
| 231 | if (Assumption) |
| 232 | return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible); |
| 233 | else |
| 234 | return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 235 | |
| 236 | case BinaryOperator::NE: |
| 237 | if (Assumption) |
| 238 | return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 239 | else |
| 240 | return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible); |
| 241 | |
Zhongxing Xu | 94b8312 | 2008-09-19 06:07:59 +0000 | [diff] [blame] | 242 | case BinaryOperator::GT: |
| 243 | if (Assumption) |
| 244 | return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible); |
| 245 | else |
| 246 | return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 247 | |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 248 | case BinaryOperator::GE: |
| 249 | if (Assumption) |
| 250 | return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 251 | else |
| 252 | return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible); |
| 253 | |
Ted Kremenek | 8c3e7fb | 2008-09-16 23:24:45 +0000 | [diff] [blame] | 254 | case BinaryOperator::LT: |
| 255 | if (Assumption) |
| 256 | return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible); |
| 257 | else |
| 258 | return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 259 | |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 260 | case BinaryOperator::LE: |
| 261 | if (Assumption) |
| 262 | return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 263 | else |
| 264 | return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible); |
| 265 | } // end switch |
| 266 | } |
| 267 | |
| 268 | const GRState* |
| 269 | BasicConstraintManager::AssumeSymNE(const GRState* St, SymbolID sym, |
| 270 | const llvm::APSInt& V, bool& isFeasible) { |
| 271 | // First, determine if sym == X, where X != V. |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 272 | if (const llvm::APSInt* X = getSymVal(St, sym)) { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 273 | isFeasible = (*X != V); |
| 274 | return St; |
| 275 | } |
| 276 | |
| 277 | // Second, determine if sym != V. |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 278 | if (isNotEqual(St, sym, V)) { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 279 | isFeasible = true; |
| 280 | return St; |
| 281 | } |
| 282 | |
| 283 | // If we reach here, sym is not a constant and we don't know if it is != V. |
| 284 | // Make that assumption. |
| 285 | isFeasible = true; |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 286 | return AddNE(St, sym, V); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 287 | } |
| 288 | |
| 289 | const GRState* |
| 290 | BasicConstraintManager::AssumeSymEQ(const GRState* St, SymbolID sym, |
| 291 | const llvm::APSInt& V, bool& isFeasible) { |
| 292 | // First, determine if sym == X, where X != V. |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 293 | if (const llvm::APSInt* X = getSymVal(St, sym)) { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 294 | isFeasible = *X == V; |
| 295 | return St; |
| 296 | } |
| 297 | |
| 298 | // Second, determine if sym != V. |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 299 | if (isNotEqual(St, sym, V)) { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 300 | isFeasible = false; |
| 301 | return St; |
| 302 | } |
| 303 | |
| 304 | // If we reach here, sym is not a constant and we don't know if it is == V. |
| 305 | // Make that assumption. |
| 306 | |
| 307 | isFeasible = true; |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 308 | return AddEQ(St, sym, V); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 309 | } |
| 310 | |
| 311 | // These logic will be handled in another ConstraintManager. |
| 312 | const GRState* |
| 313 | BasicConstraintManager::AssumeSymLT(const GRState* St, SymbolID sym, |
| 314 | const llvm::APSInt& V, bool& isFeasible) { |
Ted Kremenek | 73abd13 | 2008-12-03 18:56:12 +0000 | [diff] [blame^] | 315 | |
| 316 | // Is 'V' the smallest possible value? |
| 317 | if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isSigned())) { |
| 318 | // sym cannot be any value less than 'V'. This path is infeasible. |
| 319 | isFeasible = false; |
| 320 | return St; |
| 321 | } |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 322 | |
| 323 | // FIXME: For now have assuming x < y be the same as assuming sym != V; |
| 324 | return AssumeSymNE(St, sym, V, isFeasible); |
| 325 | } |
| 326 | |
| 327 | const GRState* |
| 328 | BasicConstraintManager::AssumeSymGT(const GRState* St, SymbolID sym, |
| 329 | const llvm::APSInt& V, bool& isFeasible) { |
| 330 | |
| 331 | // FIXME: For now have assuming x > y be the same as assuming sym != V; |
| 332 | return AssumeSymNE(St, sym, V, isFeasible); |
| 333 | } |
| 334 | |
| 335 | const GRState* |
| 336 | BasicConstraintManager::AssumeSymGE(const GRState* St, SymbolID sym, |
| 337 | const llvm::APSInt& V, bool& isFeasible) { |
| 338 | |
Ted Kremenek | 8c3e7fb | 2008-09-16 23:24:45 +0000 | [diff] [blame] | 339 | // Reject a path if the value of sym is a constant X and !(X >= V). |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 340 | if (const llvm::APSInt* X = getSymVal(St, sym)) { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 341 | isFeasible = *X >= V; |
| 342 | return St; |
| 343 | } |
| 344 | |
Ted Kremenek | 0a41e5a | 2008-09-19 18:00:36 +0000 | [diff] [blame] | 345 | isFeasible = !isNotEqual(St, sym, V) || |
| 346 | (V != llvm::APSInt::getMaxValue(V.getBitWidth(), V.isSigned())); |
| 347 | |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 348 | return St; |
| 349 | } |
| 350 | |
| 351 | const GRState* |
| 352 | BasicConstraintManager::AssumeSymLE(const GRState* St, SymbolID sym, |
| 353 | const llvm::APSInt& V, bool& isFeasible) { |
| 354 | |
Ted Kremenek | 73abd13 | 2008-12-03 18:56:12 +0000 | [diff] [blame^] | 355 | // Reject a path if the value of sym is a constant X and !(X <= V). |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 356 | if (const llvm::APSInt* X = getSymVal(St, sym)) { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 357 | isFeasible = *X <= V; |
| 358 | return St; |
| 359 | } |
Ted Kremenek | 0a41e5a | 2008-09-19 18:00:36 +0000 | [diff] [blame] | 360 | |
Ted Kremenek | 73abd13 | 2008-12-03 18:56:12 +0000 | [diff] [blame^] | 361 | // Sym is not a constant, but it is worth looking to see if V is the |
| 362 | // minimum integer value. |
| 363 | if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isSigned())) { |
| 364 | // If we know that sym != V, then this condition is infeasible since |
| 365 | // there is no other value less than V. |
| 366 | isFeasible = !isNotEqual(St, sym, V); |
| 367 | |
| 368 | // If the path is still feasible then as a consequence we know that |
| 369 | // 'sym == V' because we cannot have 'sym < V' (no smaller values). |
| 370 | // Add this constraint. |
| 371 | if (isFeasible) |
| 372 | return AddEQ(St, sym, V); |
| 373 | } |
| 374 | else |
| 375 | isFeasible = true; |
| 376 | |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 377 | return St; |
| 378 | } |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 379 | |
Zhongxing Xu | e8a964b | 2008-11-22 13:21:46 +0000 | [diff] [blame] | 380 | const GRState* |
| 381 | BasicConstraintManager::AssumeInBound(const GRState* St, SVal Idx, |
| 382 | SVal UpperBound, bool Assumption, |
| 383 | bool& isFeasible) { |
| 384 | // Only support ConcreteInt for now. |
| 385 | if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound))){ |
| 386 | isFeasible = true; |
| 387 | return St; |
| 388 | } |
| 389 | |
| 390 | const llvm::APSInt& Zero = getBasicVals().getZeroWithPtrWidth(false); |
Sebastian Redl | e95db4f | 2008-11-24 19:35:33 +0000 | [diff] [blame] | 391 | llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue(); |
| 392 | // IdxV might be too narrow. |
| 393 | if (IdxV.getBitWidth() < Zero.getBitWidth()) |
| 394 | IdxV.extend(Zero.getBitWidth()); |
| 395 | // UBV might be too narrow, too. |
| 396 | llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue(); |
| 397 | if (UBV.getBitWidth() < Zero.getBitWidth()) |
| 398 | UBV.extend(Zero.getBitWidth()); |
Zhongxing Xu | e8a964b | 2008-11-22 13:21:46 +0000 | [diff] [blame] | 399 | |
| 400 | bool InBound = (Zero <= IdxV) && (IdxV < UBV); |
| 401 | |
| 402 | isFeasible = Assumption ? InBound : !InBound; |
| 403 | |
| 404 | return St; |
| 405 | } |
| 406 | |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 407 | static int ConstEqTyIndex = 0; |
| 408 | static int ConstNotEqTyIndex = 0; |
| 409 | |
| 410 | namespace clang { |
| 411 | template<> |
| 412 | struct GRStateTrait<ConstNotEqTy> : public GRStatePartialTrait<ConstNotEqTy> { |
| 413 | static inline void* GDMIndex() { return &ConstNotEqTyIndex; } |
| 414 | }; |
| 415 | |
| 416 | template<> |
| 417 | struct GRStateTrait<ConstEqTy> : public GRStatePartialTrait<ConstEqTy> { |
| 418 | static inline void* GDMIndex() { return &ConstEqTyIndex; } |
| 419 | }; |
| 420 | } |
| 421 | |
| 422 | const GRState* BasicConstraintManager::AddEQ(const GRState* St, SymbolID sym, |
| 423 | const llvm::APSInt& V) { |
| 424 | // Create a new state with the old binding replaced. |
| 425 | GRStateRef state(St, StateMgr); |
| 426 | return state.set<ConstEqTy>(sym, &V); |
| 427 | } |
| 428 | |
| 429 | const GRState* BasicConstraintManager::AddNE(const GRState* St, SymbolID sym, |
| 430 | const llvm::APSInt& V) { |
Zhongxing Xu | f0bc50e | 2008-11-27 06:08:40 +0000 | [diff] [blame] | 431 | |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 432 | GRStateRef state(St, StateMgr); |
| 433 | |
| 434 | // First, retrieve the NE-set associated with the given symbol. |
| 435 | ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym); |
| 436 | GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet(); |
| 437 | |
| 438 | |
| 439 | // Now add V to the NE set. |
| 440 | S = ISetFactory.Add(S, &V); |
| 441 | |
| 442 | // Create a new state with the old binding replaced. |
| 443 | return state.set<ConstNotEqTy>(sym, S); |
| 444 | } |
| 445 | |
| 446 | const llvm::APSInt* BasicConstraintManager::getSymVal(const GRState* St, |
| 447 | SymbolID sym) { |
| 448 | const ConstEqTy::data_type* T = St->get<ConstEqTy>(sym); |
| 449 | return T ? *T : NULL; |
| 450 | } |
| 451 | |
| 452 | bool BasicConstraintManager::isNotEqual(const GRState* St, SymbolID sym, |
| 453 | const llvm::APSInt& V) const { |
| 454 | |
| 455 | // Retrieve the NE-set associated with the given symbol. |
| 456 | const ConstNotEqTy::data_type* T = St->get<ConstNotEqTy>(sym); |
| 457 | |
| 458 | // See if V is present in the NE-set. |
| 459 | return T ? T->contains(&V) : false; |
| 460 | } |
| 461 | |
| 462 | bool BasicConstraintManager::isEqual(const GRState* St, SymbolID sym, |
| 463 | const llvm::APSInt& V) const { |
| 464 | // Retrieve the EQ-set associated with the given symbol. |
| 465 | const ConstEqTy::data_type* T = St->get<ConstEqTy>(sym); |
| 466 | // See if V is present in the EQ-set. |
| 467 | return T ? **T == V : false; |
| 468 | } |
| 469 | |
Zhongxing Xu | 8fd9b35 | 2008-11-27 02:39:34 +0000 | [diff] [blame] | 470 | /// Scan all symbols referenced by the constraints. If the symbol is not alive |
| 471 | /// as marked in LSymbols, mark it as dead in DSymbols. |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 472 | const GRState* BasicConstraintManager::RemoveDeadBindings(const GRState* St, |
| 473 | StoreManager::LiveSymbolsTy& LSymbols, |
| 474 | StoreManager::DeadSymbolsTy& DSymbols) { |
| 475 | GRStateRef state(St, StateMgr); |
| 476 | ConstEqTy CE = state.get<ConstEqTy>(); |
| 477 | ConstEqTy::Factory& CEFactory = state.get_context<ConstEqTy>(); |
| 478 | |
| 479 | for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) { |
| 480 | SymbolID sym = I.getKey(); |
| 481 | if (!LSymbols.count(sym)) { |
| 482 | DSymbols.insert(sym); |
| 483 | CE = CEFactory.Remove(CE, sym); |
| 484 | } |
| 485 | } |
| 486 | state = state.set<ConstEqTy>(CE); |
| 487 | |
| 488 | ConstNotEqTy CNE = state.get<ConstNotEqTy>(); |
| 489 | ConstNotEqTy::Factory& CNEFactory = state.get_context<ConstNotEqTy>(); |
| 490 | |
| 491 | for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) { |
| 492 | SymbolID sym = I.getKey(); |
| 493 | if (!LSymbols.count(sym)) { |
| 494 | DSymbols.insert(sym); |
| 495 | CNE = CNEFactory.Remove(CNE, sym); |
| 496 | } |
| 497 | } |
| 498 | |
| 499 | return state.set<ConstNotEqTy>(CNE); |
| 500 | } |
| 501 | |
| 502 | void BasicConstraintManager::print(const GRState* St, std::ostream& Out, |
| 503 | const char* nl, const char *sep) { |
| 504 | // Print equality constraints. |
| 505 | |
| 506 | ConstEqTy CE = St->get<ConstEqTy>(); |
| 507 | |
| 508 | if (!CE.isEmpty()) { |
| 509 | Out << nl << sep << "'==' constraints:"; |
| 510 | |
| 511 | for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) { |
| 512 | Out << nl << " $" << I.getKey(); |
| 513 | llvm::raw_os_ostream OS(Out); |
| 514 | OS << " : " << *I.getData(); |
| 515 | } |
| 516 | } |
| 517 | |
| 518 | // Print != constraints. |
| 519 | |
| 520 | ConstNotEqTy CNE = St->get<ConstNotEqTy>(); |
| 521 | |
| 522 | if (!CNE.isEmpty()) { |
| 523 | Out << nl << sep << "'!=' constraints:"; |
| 524 | |
| 525 | for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) { |
| 526 | Out << nl << " $" << I.getKey() << " : "; |
| 527 | bool isFirst = true; |
| 528 | |
| 529 | GRState::IntSetTy::iterator J = I.getData().begin(), |
| 530 | EJ = I.getData().end(); |
| 531 | |
| 532 | for ( ; J != EJ; ++J) { |
| 533 | if (isFirst) isFirst = false; |
| 534 | else Out << ", "; |
| 535 | |
Zhongxing Xu | 7d94e26 | 2008-11-10 05:00:06 +0000 | [diff] [blame] | 536 | Out << (*J)->getSExtValue(); // Hack: should print to raw_ostream. |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 537 | } |
| 538 | } |
| 539 | } |
Daniel Dunbar | 0e194dd | 2008-08-30 02:06:22 +0000 | [diff] [blame] | 540 | } |