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