Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 1 | //= GRState*cpp - Path-Sens. "State" for tracking valuues -----*- C++ -*--=// |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 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 | // |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 10 | // This file defines SymbolID, ExprBindKey, and GRState* |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 11 | // |
| 12 | //===----------------------------------------------------------------------===// |
| 13 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 14 | #include "clang/Analysis/PathSensitive/GRState.h" |
Ted Kremenek | 90e1481 | 2008-02-14 23:25:54 +0000 | [diff] [blame] | 15 | #include "llvm/ADT/SmallSet.h" |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 16 | #include "clang/Analysis/PathSensitive/GRTransferFuncs.h" |
Ted Kremenek | f66ea2cd | 2008-02-04 21:59:22 +0000 | [diff] [blame] | 17 | |
| 18 | using namespace clang; |
| 19 | |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 20 | GRStateManager::~GRStateManager() { |
| 21 | for (std::vector<GRState::Printer*>::iterator I=Printers.begin(), |
| 22 | E=Printers.end(); I!=E; ++I) |
| 23 | delete *I; |
| 24 | |
| 25 | for (GDMContextsTy::iterator I=GDMContexts.begin(), E=GDMContexts.end(); |
| 26 | I!=E; ++I) |
| 27 | I->second.second(I->second.first); |
| 28 | } |
| 29 | |
| 30 | //===----------------------------------------------------------------------===// |
| 31 | // Basic symbolic analysis. This will eventually be refactored into a |
| 32 | // separate component. |
| 33 | //===----------------------------------------------------------------------===// |
| 34 | |
| 35 | typedef llvm::ImmutableMap<SymbolID,GRState::IntSetTy> ConstNotEqTy; |
| 36 | |
| 37 | static int ConstNotEqTyIndex = 0; |
| 38 | |
| 39 | namespace clang { |
| 40 | template<> struct GRStateTrait<ConstNotEqTy> { |
| 41 | typedef ConstNotEqTy data_type; |
| 42 | typedef ConstNotEqTy::Factory& context_type; |
| 43 | typedef SymbolID key_type; |
| 44 | typedef GRState::IntSetTy value_type; |
| 45 | typedef const GRState::IntSetTy* lookup_type; |
| 46 | |
| 47 | static data_type MakeData(void* const* p) { |
| 48 | return p ? ConstNotEqTy((ConstNotEqTy::TreeTy*) *p) : ConstNotEqTy(0); |
| 49 | } |
| 50 | static void* MakeVoidPtr(ConstNotEqTy B) { |
| 51 | return B.getRoot(); |
| 52 | } |
| 53 | static void* GDMIndex() { |
| 54 | return &ConstNotEqTyIndex; |
| 55 | } |
| 56 | static lookup_type Lookup(ConstNotEqTy B, SymbolID K) { |
| 57 | return B.lookup(K); |
| 58 | } |
| 59 | static data_type Set(data_type B, key_type K, value_type E,context_type F){ |
| 60 | return F.Add(B, K, E); |
| 61 | } |
| 62 | |
| 63 | static data_type Remove(ConstNotEqTy B, SymbolID K, context_type F) { |
| 64 | return F.Remove(B, K); |
| 65 | } |
| 66 | |
| 67 | static context_type MakeContext(void* p) { |
| 68 | return *((ConstNotEqTy::Factory*) p); |
| 69 | } |
| 70 | |
| 71 | static void* CreateContext(llvm::BumpPtrAllocator& Alloc) { |
| 72 | return new ConstNotEqTy::Factory(Alloc); |
| 73 | } |
| 74 | |
| 75 | static void DeleteContext(void* Ctx) { |
| 76 | delete (ConstNotEqTy::Factory*) Ctx; |
| 77 | } |
| 78 | }; |
| 79 | } |
| 80 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 81 | bool GRState::isNotEqual(SymbolID sym, const llvm::APSInt& V) const { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 82 | |
| 83 | // Retrieve the NE-set associated with the given symbol. |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 84 | const ConstNotEqTy::data_type* T = get<ConstNotEqTy>(sym); |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 85 | |
| 86 | // See if V is present in the NE-set. |
Ted Kremenek | e8fdc83 | 2008-07-07 16:21:19 +0000 | [diff] [blame] | 87 | return T ? T->contains(&V) : false; |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 88 | } |
| 89 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 90 | bool GRState::isEqual(SymbolID sym, const llvm::APSInt& V) const { |
Ted Kremenek | 584def7 | 2008-07-22 00:46:16 +0000 | [diff] [blame] | 91 | |
| 92 | // Retrieve the EQ-set associated with the given symbol. |
| 93 | const ConstEqTy::data_type* T = ConstEq.lookup(sym); |
| 94 | |
| 95 | // See if V is present in the EQ-set. |
| 96 | return T ? **T == V : false; |
| 97 | } |
| 98 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 99 | const llvm::APSInt* GRState::getSymVal(SymbolID sym) const { |
Ted Kremenek | e8fdc83 | 2008-07-07 16:21:19 +0000 | [diff] [blame] | 100 | ConstEqTy::data_type* T = ConstEq.lookup(sym); |
| 101 | return T ? *T : NULL; |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 102 | } |
| 103 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 104 | const GRState* |
| 105 | GRStateManager::RemoveDeadBindings(const GRState* St, Stmt* Loc, |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 106 | const LiveVariables& Liveness, |
| 107 | DeadSymbolsTy& DSymbols) { |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 108 | |
| 109 | // This code essentially performs a "mark-and-sweep" of the VariableBindings. |
| 110 | // The roots are any Block-level exprs and Decls that our liveness algorithm |
| 111 | // tells us are live. We then see what Decls they may reference, and keep |
| 112 | // those around. This code more than likely can be made faster, and the |
| 113 | // frequency of which this method is called should be experimented with |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 114 | // for optimum performance. |
| 115 | DRoots.clear(); |
| 116 | StoreManager::LiveSymbolsTy LSymbols; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 117 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 118 | GRState NewSt = *St; |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 119 | |
| 120 | // FIXME: Put this in environment. |
| 121 | // Clean up the environment. |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 122 | |
| 123 | // Drop bindings for subexpressions. |
Ted Kremenek | 8133a26 | 2008-07-08 21:46:56 +0000 | [diff] [blame] | 124 | NewSt.Env = EnvMgr.RemoveSubExprBindings(NewSt.Env); |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 125 | |
| 126 | // Iterate over the block-expr bindings. |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 127 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 128 | for (GRState::beb_iterator I = St->beb_begin(), E = St->beb_end(); |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 129 | I!=E ; ++I) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 130 | Expr* BlkExpr = I.getKey(); |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 131 | |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 132 | if (Liveness.isLive(Loc, BlkExpr)) { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 133 | RVal X = I.getData(); |
Ted Kremenek | 90e1481 | 2008-02-14 23:25:54 +0000 | [diff] [blame] | 134 | |
| 135 | if (isa<lval::DeclVal>(X)) { |
| 136 | lval::DeclVal LV = cast<lval::DeclVal>(X); |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 137 | DRoots.push_back(LV.getDecl()); |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 138 | } |
Ted Kremenek | 90e1481 | 2008-02-14 23:25:54 +0000 | [diff] [blame] | 139 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 140 | for (RVal::symbol_iterator SI = X.symbol_begin(), SE = X.symbol_end(); |
| 141 | SI != SE; ++SI) { |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 142 | LSymbols.insert(*SI); |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 143 | } |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 144 | } |
Ted Kremenek | 05a2378 | 2008-02-26 19:05:15 +0000 | [diff] [blame] | 145 | else { |
| 146 | RVal X = I.getData(); |
| 147 | |
Ted Kremenek | 4a4e524 | 2008-02-28 09:25:22 +0000 | [diff] [blame] | 148 | if (X.isUndef() && cast<UndefinedVal>(X).getData()) |
Ted Kremenek | 05a2378 | 2008-02-26 19:05:15 +0000 | [diff] [blame] | 149 | continue; |
| 150 | |
Ted Kremenek | 8133a26 | 2008-07-08 21:46:56 +0000 | [diff] [blame] | 151 | NewSt.Env = EnvMgr.RemoveBlkExpr(NewSt.Env, BlkExpr); |
Ted Kremenek | 05a2378 | 2008-02-26 19:05:15 +0000 | [diff] [blame] | 152 | } |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 153 | } |
Ted Kremenek | 016f52f | 2008-02-08 21:10:02 +0000 | [diff] [blame] | 154 | |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 155 | // Clean up the store. |
| 156 | DSymbols.clear(); |
| 157 | NewSt.St = StMgr->RemoveDeadBindings(St->getStore(), Loc, Liveness, DRoots, |
| 158 | LSymbols, DSymbols); |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 159 | |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 160 | // Remove the dead symbols from the symbol tracker. |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 161 | // FIXME: Refactor into something else that manages symbol values. |
| 162 | for (GRState::ConstEqTy::iterator I = St->ConstEq.begin(), |
| 163 | E=St->ConstEq.end(); I!=E; ++I) { |
Ted Kremenek | 77d7ef8 | 2008-04-24 18:31:42 +0000 | [diff] [blame] | 164 | |
| 165 | SymbolID sym = I.getKey(); |
| 166 | |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 167 | if (!LSymbols.count(sym)) { |
| 168 | DSymbols.insert(sym); |
Ted Kremenek | 77d7ef8 | 2008-04-24 18:31:42 +0000 | [diff] [blame] | 169 | NewSt.ConstEq = CEFactory.Remove(NewSt.ConstEq, sym); |
| 170 | } |
| 171 | } |
| 172 | |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 173 | GRStateRef state(getPersistentState(NewSt), *this); |
| 174 | ConstNotEqTy CNE = state.get<ConstNotEqTy>(); |
| 175 | ConstNotEqTy::Factory& CNEFactory = state.get_context<ConstNotEqTy>(); |
| 176 | |
| 177 | for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) { |
| 178 | SymbolID sym = I.getKey(); |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 179 | if (!LSymbols.count(sym)) { |
| 180 | DSymbols.insert(sym); |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 181 | CNE = CNEFactory.Remove(CNE, sym); |
Ted Kremenek | 77d7ef8 | 2008-04-24 18:31:42 +0000 | [diff] [blame] | 182 | } |
| 183 | } |
Ted Kremenek | 90e1481 | 2008-02-14 23:25:54 +0000 | [diff] [blame] | 184 | |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 185 | return state.set<ConstNotEqTy>(CNE); |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 186 | } |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 187 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 188 | const GRState* GRStateManager::SetRVal(const GRState* St, LVal LV, |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 189 | RVal V) { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 190 | |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 191 | Store OldStore = St->getStore(); |
| 192 | Store NewStore = StMgr->SetRVal(OldStore, LV, V); |
Ted Kremenek | 3271f8d | 2008-02-07 04:16:04 +0000 | [diff] [blame] | 193 | |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 194 | if (NewStore == OldStore) |
| 195 | return St; |
Ted Kremenek | 692416c | 2008-02-18 22:57:02 +0000 | [diff] [blame] | 196 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 197 | GRState NewSt = *St; |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 198 | NewSt.St = NewStore; |
| 199 | return getPersistentState(NewSt); |
Ted Kremenek | f66ea2cd | 2008-02-04 21:59:22 +0000 | [diff] [blame] | 200 | } |
| 201 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 202 | const GRState* GRStateManager::Unbind(const GRState* St, LVal LV) { |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 203 | Store OldStore = St->getStore(); |
| 204 | Store NewStore = StMgr->Remove(OldStore, LV); |
| 205 | |
| 206 | if (NewStore == OldStore) |
| 207 | return St; |
| 208 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 209 | GRState NewSt = *St; |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 210 | NewSt.St = NewStore; |
| 211 | return getPersistentState(NewSt); |
| 212 | } |
| 213 | |
| 214 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 215 | const GRState* GRStateManager::AddNE(const GRState* St, SymbolID sym, |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 216 | const llvm::APSInt& V) { |
| 217 | |
| 218 | GRStateRef state(St, *this); |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 219 | |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 220 | // First, retrieve the NE-set associated with the given symbol. |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 221 | ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym); |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 222 | GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet(); |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 223 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 224 | // Now add V to the NE set. |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 225 | S = ISetFactory.Add(S, &V); |
| 226 | |
| 227 | // Create a new state with the old binding replaced. |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 228 | return state.set<ConstNotEqTy>(sym, S); |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 229 | } |
| 230 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 231 | const GRState* GRStateManager::AddEQ(const GRState* St, SymbolID sym, |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 232 | const llvm::APSInt& V) { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 233 | |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 234 | // Create a new state with the old binding replaced. |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 235 | GRState NewSt = *St; |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 236 | NewSt.ConstEq = CEFactory.Add(NewSt.ConstEq, sym, &V); |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 237 | |
| 238 | // Get the persistent copy. |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 239 | return getPersistentState(NewSt); |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 240 | } |
| 241 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 242 | const GRState* GRStateManager::getInitialState() { |
Ted Kremenek | 5a7b382 | 2008-02-26 23:37:01 +0000 | [diff] [blame] | 243 | |
Ted Kremenek | 72cd17f | 2008-08-14 21:16:54 +0000 | [diff] [blame] | 244 | GRState StateImpl(EnvMgr.getInitialEnvironment(), StMgr->getInitialStore(), |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 245 | GDMFactory.GetEmptyMap(), |
Ted Kremenek | 72cd17f | 2008-08-14 21:16:54 +0000 | [diff] [blame] | 246 | CEFactory.GetEmptyMap()); |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 247 | |
| 248 | return getPersistentState(StateImpl); |
| 249 | } |
| 250 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 251 | const GRState* GRStateManager::getPersistentState(GRState& State) { |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 252 | |
| 253 | llvm::FoldingSetNodeID ID; |
| 254 | State.Profile(ID); |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 255 | void* InsertPos; |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 256 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 257 | if (GRState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos)) |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 258 | return I; |
| 259 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 260 | GRState* I = (GRState*) Alloc.Allocate<GRState>(); |
| 261 | new (I) GRState(State); |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 262 | StateSet.InsertNode(I, InsertPos); |
| 263 | return I; |
| 264 | } |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 265 | |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 266 | |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 267 | //===----------------------------------------------------------------------===// |
| 268 | // State pretty-printing. |
| 269 | //===----------------------------------------------------------------------===// |
Ted Kremenek | 461f977 | 2008-03-11 18:57:24 +0000 | [diff] [blame] | 270 | |
Ted Kremenek | ae6814e | 2008-08-13 21:24:49 +0000 | [diff] [blame] | 271 | void GRState::print(std::ostream& Out, Printer** Beg, Printer** End, |
| 272 | const char* nl, const char* sep) const { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 273 | |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 274 | // Print Variable Bindings |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 275 | Out << "Variables:" << nl; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 276 | |
| 277 | bool isFirst = true; |
| 278 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 279 | for (vb_iterator I = vb_begin(), E = vb_end(); I != E; ++I) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 280 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 281 | if (isFirst) isFirst = false; |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 282 | else Out << nl; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 283 | |
| 284 | Out << ' ' << I.getKey()->getName() << " : "; |
| 285 | I.getData().print(Out); |
| 286 | } |
| 287 | |
| 288 | // Print Subexpression bindings. |
| 289 | |
| 290 | isFirst = true; |
| 291 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 292 | for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 293 | |
| 294 | if (isFirst) { |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 295 | Out << nl << nl << "Sub-Expressions:" << nl; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 296 | isFirst = false; |
| 297 | } |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 298 | else { Out << nl; } |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 299 | |
| 300 | Out << " (" << (void*) I.getKey() << ") "; |
| 301 | I.getKey()->printPretty(Out); |
| 302 | Out << " : "; |
| 303 | I.getData().print(Out); |
| 304 | } |
| 305 | |
| 306 | // Print block-expression bindings. |
| 307 | |
| 308 | isFirst = true; |
| 309 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 310 | for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 311 | |
| 312 | if (isFirst) { |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 313 | Out << nl << nl << "Block-level Expressions:" << nl; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 314 | isFirst = false; |
| 315 | } |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 316 | else { Out << nl; } |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 317 | |
| 318 | Out << " (" << (void*) I.getKey() << ") "; |
| 319 | I.getKey()->printPretty(Out); |
| 320 | Out << " : "; |
| 321 | I.getData().print(Out); |
| 322 | } |
| 323 | |
| 324 | // Print equality constraints. |
Ted Kremenek | ae6814e | 2008-08-13 21:24:49 +0000 | [diff] [blame] | 325 | // FIXME: Make just another printer do this. |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 326 | |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 327 | if (!ConstEq.isEmpty()) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 328 | |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 329 | Out << nl << sep << "'==' constraints:"; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 330 | |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 331 | for (ConstEqTy::iterator I = ConstEq.begin(), |
| 332 | E = ConstEq.end(); I!=E; ++I) { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 333 | |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 334 | Out << nl << " $" << I.getKey() |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 335 | << " : " << I.getData()->toString(); |
| 336 | } |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 337 | } |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 338 | |
| 339 | // Print != constraints. |
Ted Kremenek | ae6814e | 2008-08-13 21:24:49 +0000 | [diff] [blame] | 340 | // FIXME: Make just another printer do this. |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 341 | |
| 342 | ConstNotEqTy CNE = get<ConstNotEqTy>(); |
| 343 | |
| 344 | if (!CNE.isEmpty()) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 345 | |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 346 | Out << nl << sep << "'!=' constraints:"; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 347 | |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 348 | for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) { |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 349 | Out << nl << " $" << I.getKey() << " : "; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 350 | isFirst = true; |
| 351 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 352 | IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end(); |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 353 | |
| 354 | for ( ; J != EJ; ++J) { |
| 355 | if (isFirst) isFirst = false; |
| 356 | else Out << ", "; |
| 357 | |
| 358 | Out << (*J)->toString(); |
| 359 | } |
| 360 | } |
| 361 | } |
Ted Kremenek | 461f977 | 2008-03-11 18:57:24 +0000 | [diff] [blame] | 362 | |
Ted Kremenek | ae6814e | 2008-08-13 21:24:49 +0000 | [diff] [blame] | 363 | // Print checker-specific data. |
| 364 | for ( ; Beg != End ; ++Beg) (*Beg)->Print(Out, this, nl, sep); |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 365 | } |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 366 | |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 367 | void GRStateRef::printDOT(std::ostream& Out) const { |
| 368 | print(Out, "\\l", "\\|"); |
| 369 | } |
| 370 | |
| 371 | void GRStateRef::printStdErr() const { |
| 372 | print(*llvm::cerr); |
| 373 | } |
| 374 | |
| 375 | void GRStateRef::print(std::ostream& Out, const char* nl, const char* sep)const{ |
| 376 | GRState::Printer **beg = Mgr->Printers.empty() ? 0 : &Mgr->Printers[0]; |
| 377 | GRState::Printer **end = !beg ? 0 : beg + Mgr->Printers.size(); |
| 378 | St->print(Out, beg, end, nl, sep); |
| 379 | } |
| 380 | |
Ted Kremenek | 72cd17f | 2008-08-14 21:16:54 +0000 | [diff] [blame] | 381 | //===----------------------------------------------------------------------===// |
| 382 | // Generic Data Map. |
| 383 | //===----------------------------------------------------------------------===// |
| 384 | |
| 385 | void* const* GRState::FindGDM(void* K) const { |
| 386 | return GDM.lookup(K); |
| 387 | } |
| 388 | |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 389 | void* |
| 390 | GRStateManager::FindGDMContext(void* K, |
| 391 | void* (*CreateContext)(llvm::BumpPtrAllocator&), |
| 392 | void (*DeleteContext)(void*)) { |
| 393 | |
| 394 | std::pair<void*, void (*)(void*)>& p = GDMContexts[K]; |
| 395 | if (!p.first) { |
| 396 | p.first = CreateContext(Alloc); |
| 397 | p.second = DeleteContext; |
| 398 | } |
| 399 | |
| 400 | return p.first; |
| 401 | } |
| 402 | |
Ted Kremenek | 72cd17f | 2008-08-14 21:16:54 +0000 | [diff] [blame] | 403 | const GRState* GRStateManager::addGDM(const GRState* St, void* Key, void* Data){ |
| 404 | GRState::GenericDataMap M1 = St->getGDM(); |
| 405 | GRState::GenericDataMap M2 = GDMFactory.Add(M1, Key, Data); |
| 406 | |
| 407 | if (M1 == M2) |
| 408 | return St; |
| 409 | |
| 410 | GRState NewSt = *St; |
| 411 | NewSt.GDM = M2; |
| 412 | return getPersistentState(NewSt); |
| 413 | } |
Ted Kremenek | 584def7 | 2008-07-22 00:46:16 +0000 | [diff] [blame] | 414 | |
| 415 | //===----------------------------------------------------------------------===// |
| 416 | // Queries. |
| 417 | //===----------------------------------------------------------------------===// |
| 418 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 419 | bool GRStateManager::isEqual(const GRState* state, Expr* Ex, |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 420 | const llvm::APSInt& Y) { |
| 421 | |
Ted Kremenek | 584def7 | 2008-07-22 00:46:16 +0000 | [diff] [blame] | 422 | RVal V = GetRVal(state, Ex); |
| 423 | |
| 424 | if (lval::ConcreteInt* X = dyn_cast<lval::ConcreteInt>(&V)) |
| 425 | return X->getValue() == Y; |
| 426 | |
| 427 | if (nonlval::ConcreteInt* X = dyn_cast<nonlval::ConcreteInt>(&V)) |
| 428 | return X->getValue() == Y; |
| 429 | |
| 430 | if (nonlval::SymbolVal* X = dyn_cast<nonlval::SymbolVal>(&V)) |
| 431 | return state->isEqual(X->getSymbol(), Y); |
| 432 | |
| 433 | if (lval::SymbolVal* X = dyn_cast<lval::SymbolVal>(&V)) |
| 434 | return state->isEqual(X->getSymbol(), Y); |
| 435 | |
| 436 | return false; |
| 437 | } |
| 438 | |
Ted Kremenek | 1c72ef0 | 2008-08-16 00:49:49 +0000 | [diff] [blame^] | 439 | bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) { |
Ted Kremenek | 584def7 | 2008-07-22 00:46:16 +0000 | [diff] [blame] | 440 | return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType())); |
| 441 | } |
| 442 | |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 443 | //===----------------------------------------------------------------------===// |
| 444 | // "Assume" logic. |
| 445 | //===----------------------------------------------------------------------===// |
| 446 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 447 | const GRState* GRStateManager::Assume(const GRState* St, LVal Cond, |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 448 | bool Assumption, bool& isFeasible) { |
| 449 | |
| 450 | St = AssumeAux(St, Cond, Assumption, isFeasible); |
| 451 | |
| 452 | return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible) |
| 453 | : St; |
| 454 | } |
| 455 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 456 | const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond, |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 457 | bool Assumption, bool& isFeasible) { |
| 458 | |
| 459 | switch (Cond.getSubKind()) { |
| 460 | default: |
| 461 | assert (false && "'Assume' not implemented for this LVal."); |
| 462 | return St; |
| 463 | |
| 464 | case lval::SymbolValKind: |
| 465 | if (Assumption) |
| 466 | return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(), |
| 467 | BasicVals.getZeroWithPtrWidth(), isFeasible); |
| 468 | else |
| 469 | return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(), |
| 470 | BasicVals.getZeroWithPtrWidth(), isFeasible); |
| 471 | |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 472 | case lval::DeclValKind: |
| 473 | case lval::FuncValKind: |
| 474 | case lval::GotoLabelKind: |
| 475 | case lval::StringLiteralValKind: |
| 476 | isFeasible = Assumption; |
| 477 | return St; |
| 478 | |
| 479 | case lval::FieldOffsetKind: |
| 480 | return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(), |
| 481 | Assumption, isFeasible); |
| 482 | |
| 483 | case lval::ArrayOffsetKind: |
| 484 | return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(), |
| 485 | Assumption, isFeasible); |
| 486 | |
| 487 | case lval::ConcreteIntKind: { |
| 488 | bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0; |
| 489 | isFeasible = b ? Assumption : !Assumption; |
| 490 | return St; |
| 491 | } |
| 492 | } |
| 493 | } |
| 494 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 495 | const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond, |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 496 | bool Assumption, bool& isFeasible) { |
| 497 | |
| 498 | St = AssumeAux(St, Cond, Assumption, isFeasible); |
| 499 | |
| 500 | return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible) |
| 501 | : St; |
| 502 | } |
| 503 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 504 | const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond, |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 505 | bool Assumption, bool& isFeasible) { |
| 506 | switch (Cond.getSubKind()) { |
| 507 | default: |
| 508 | assert (false && "'Assume' not implemented for this NonLVal."); |
| 509 | return St; |
| 510 | |
| 511 | |
| 512 | case nonlval::SymbolValKind: { |
| 513 | nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond); |
| 514 | SymbolID sym = SV.getSymbol(); |
| 515 | |
| 516 | if (Assumption) |
| 517 | return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)), |
| 518 | isFeasible); |
| 519 | else |
| 520 | return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)), |
| 521 | isFeasible); |
| 522 | } |
| 523 | |
| 524 | case nonlval::SymIntConstraintValKind: |
| 525 | return |
| 526 | AssumeSymInt(St, Assumption, |
| 527 | cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(), |
| 528 | isFeasible); |
| 529 | |
| 530 | case nonlval::ConcreteIntKind: { |
| 531 | bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0; |
| 532 | isFeasible = b ? Assumption : !Assumption; |
| 533 | return St; |
| 534 | } |
| 535 | |
| 536 | case nonlval::LValAsIntegerKind: { |
| 537 | return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(), |
| 538 | Assumption, isFeasible); |
| 539 | } |
| 540 | } |
| 541 | } |
| 542 | |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 543 | |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 544 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 545 | const GRState* GRStateManager::AssumeSymInt(const GRState* St, |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 546 | bool Assumption, |
| 547 | const SymIntConstraint& C, |
| 548 | bool& isFeasible) { |
| 549 | |
| 550 | switch (C.getOpcode()) { |
| 551 | default: |
| 552 | // No logic yet for other operators. |
| 553 | isFeasible = true; |
| 554 | return St; |
| 555 | |
| 556 | case BinaryOperator::EQ: |
| 557 | if (Assumption) |
| 558 | return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible); |
| 559 | else |
| 560 | return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 561 | |
| 562 | case BinaryOperator::NE: |
| 563 | if (Assumption) |
| 564 | return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 565 | else |
| 566 | return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible); |
Ted Kremenek | 2619be0 | 2008-08-07 22:30:22 +0000 | [diff] [blame] | 567 | |
| 568 | case BinaryOperator::GE: |
| 569 | if (Assumption) |
| 570 | return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 571 | else |
| 572 | return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible); |
| 573 | |
| 574 | case BinaryOperator::LE: |
| 575 | if (Assumption) |
| 576 | return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 577 | else |
| 578 | return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible); |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame] | 579 | } |
| 580 | } |
Ted Kremenek | 2619be0 | 2008-08-07 22:30:22 +0000 | [diff] [blame] | 581 | |
| 582 | //===----------------------------------------------------------------------===// |
| 583 | // FIXME: This should go into a plug-in constraint engine. |
| 584 | //===----------------------------------------------------------------------===// |
| 585 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 586 | const GRState* |
| 587 | GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym, |
Ted Kremenek | 2619be0 | 2008-08-07 22:30:22 +0000 | [diff] [blame] | 588 | const llvm::APSInt& V, bool& isFeasible) { |
| 589 | |
| 590 | // First, determine if sym == X, where X != V. |
| 591 | if (const llvm::APSInt* X = St->getSymVal(sym)) { |
| 592 | isFeasible = *X != V; |
| 593 | return St; |
| 594 | } |
| 595 | |
| 596 | // Second, determine if sym != V. |
| 597 | if (St->isNotEqual(sym, V)) { |
| 598 | isFeasible = true; |
| 599 | return St; |
| 600 | } |
| 601 | |
| 602 | // If we reach here, sym is not a constant and we don't know if it is != V. |
| 603 | // Make that assumption. |
| 604 | |
| 605 | isFeasible = true; |
| 606 | return AddNE(St, sym, V); |
| 607 | } |
| 608 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 609 | const GRState* |
| 610 | GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym, |
Ted Kremenek | 2619be0 | 2008-08-07 22:30:22 +0000 | [diff] [blame] | 611 | const llvm::APSInt& V, bool& isFeasible) { |
| 612 | |
| 613 | // First, determine if sym == X, where X != V. |
| 614 | if (const llvm::APSInt* X = St->getSymVal(sym)) { |
| 615 | isFeasible = *X == V; |
| 616 | return St; |
| 617 | } |
| 618 | |
| 619 | // Second, determine if sym != V. |
| 620 | if (St->isNotEqual(sym, V)) { |
| 621 | isFeasible = false; |
| 622 | return St; |
| 623 | } |
| 624 | |
| 625 | // If we reach here, sym is not a constant and we don't know if it is == V. |
| 626 | // Make that assumption. |
| 627 | |
| 628 | isFeasible = true; |
| 629 | return AddEQ(St, sym, V); |
| 630 | } |
| 631 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 632 | const GRState* |
| 633 | GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym, |
Ted Kremenek | 2619be0 | 2008-08-07 22:30:22 +0000 | [diff] [blame] | 634 | const llvm::APSInt& V, bool& isFeasible) { |
| 635 | |
| 636 | // FIXME: For now have assuming x < y be the same as assuming sym != V; |
| 637 | return AssumeSymNE(St, sym, V, isFeasible); |
| 638 | } |
| 639 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 640 | const GRState* |
| 641 | GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym, |
Ted Kremenek | 2619be0 | 2008-08-07 22:30:22 +0000 | [diff] [blame] | 642 | const llvm::APSInt& V, bool& isFeasible) { |
| 643 | |
| 644 | // FIXME: For now have assuming x > y be the same as assuming sym != V; |
| 645 | return AssumeSymNE(St, sym, V, isFeasible); |
| 646 | } |
| 647 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 648 | const GRState* |
| 649 | GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym, |
Ted Kremenek | 2619be0 | 2008-08-07 22:30:22 +0000 | [diff] [blame] | 650 | const llvm::APSInt& V, bool& isFeasible) { |
| 651 | |
| 652 | // FIXME: Primitive logic for now. Only reject a path if the value of |
| 653 | // sym is a constant X and !(X >= V). |
| 654 | |
| 655 | if (const llvm::APSInt* X = St->getSymVal(sym)) { |
| 656 | isFeasible = *X >= V; |
| 657 | return St; |
| 658 | } |
| 659 | |
| 660 | isFeasible = true; |
| 661 | return St; |
| 662 | } |
| 663 | |
Ted Kremenek | 4adc81e | 2008-08-13 04:27:00 +0000 | [diff] [blame] | 664 | const GRState* |
| 665 | GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym, |
Ted Kremenek | 2619be0 | 2008-08-07 22:30:22 +0000 | [diff] [blame] | 666 | const llvm::APSInt& V, bool& isFeasible) { |
| 667 | |
| 668 | // FIXME: Primitive logic for now. Only reject a path if the value of |
| 669 | // sym is a constant X and !(X <= V). |
| 670 | |
| 671 | if (const llvm::APSInt* X = St->getSymVal(sym)) { |
| 672 | isFeasible = *X <= V; |
| 673 | return St; |
| 674 | } |
| 675 | |
| 676 | isFeasible = true; |
| 677 | return St; |
| 678 | } |
| 679 | |