Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 1 | //= ValueState*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 | // |
Gabor Greif | 843e934 | 2008-03-06 10:40:09 +0000 | [diff] [blame] | 10 | // This file defines SymbolID, ExprBindKey, and ValueState* |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 11 | // |
| 12 | //===----------------------------------------------------------------------===// |
| 13 | |
Ted Kremenek | 0f5f059 | 2008-02-27 06:07:00 +0000 | [diff] [blame] | 14 | #include "clang/Analysis/PathSensitive/ValueState.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 | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 20 | bool ValueState::isNotEqual(SymbolID sym, const llvm::APSInt& V) const { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 21 | |
| 22 | // Retrieve the NE-set associated with the given symbol. |
Ted Kremenek | e8fdc83 | 2008-07-07 16:21:19 +0000 | [diff] [blame] | 23 | const ConstNotEqTy::data_type* T = ConstNotEq.lookup(sym); |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 24 | |
| 25 | // See if V is present in the NE-set. |
Ted Kremenek | e8fdc83 | 2008-07-07 16:21:19 +0000 | [diff] [blame] | 26 | return T ? T->contains(&V) : false; |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 27 | } |
| 28 | |
| 29 | const llvm::APSInt* ValueState::getSymVal(SymbolID sym) const { |
Ted Kremenek | e8fdc83 | 2008-07-07 16:21:19 +0000 | [diff] [blame] | 30 | ConstEqTy::data_type* T = ConstEq.lookup(sym); |
| 31 | return T ? *T : NULL; |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 32 | } |
| 33 | |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 34 | const ValueState* |
| 35 | ValueStateManager::RemoveDeadBindings(const ValueState* St, Stmt* Loc, |
Ted Kremenek | 77d7ef8 | 2008-04-24 18:31:42 +0000 | [diff] [blame] | 36 | const LiveVariables& Liveness, |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 37 | DeadSymbolsTy& DSymbols) { |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 38 | |
| 39 | // This code essentially performs a "mark-and-sweep" of the VariableBindings. |
| 40 | // The roots are any Block-level exprs and Decls that our liveness algorithm |
| 41 | // tells us are live. We then see what Decls they may reference, and keep |
| 42 | // those around. This code more than likely can be made faster, and the |
| 43 | // frequency of which this method is called should be experimented with |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 44 | // for optimum performance. |
| 45 | DRoots.clear(); |
| 46 | StoreManager::LiveSymbolsTy LSymbols; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 47 | |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 48 | ValueState NewSt = *St; |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 49 | |
| 50 | // FIXME: Put this in environment. |
| 51 | // Clean up the environment. |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 52 | |
| 53 | // Drop bindings for subexpressions. |
Ted Kremenek | 8133a26 | 2008-07-08 21:46:56 +0000 | [diff] [blame] | 54 | NewSt.Env = EnvMgr.RemoveSubExprBindings(NewSt.Env); |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 55 | |
| 56 | // Iterate over the block-expr bindings. |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 57 | |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 58 | for (ValueState::beb_iterator I = St->beb_begin(), E = St->beb_end(); |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 59 | I!=E ; ++I) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 60 | Expr* BlkExpr = I.getKey(); |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 61 | |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 62 | if (Liveness.isLive(Loc, BlkExpr)) { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 63 | RVal X = I.getData(); |
Ted Kremenek | 90e1481 | 2008-02-14 23:25:54 +0000 | [diff] [blame] | 64 | |
| 65 | if (isa<lval::DeclVal>(X)) { |
| 66 | lval::DeclVal LV = cast<lval::DeclVal>(X); |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 67 | DRoots.push_back(LV.getDecl()); |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 68 | } |
Ted Kremenek | 90e1481 | 2008-02-14 23:25:54 +0000 | [diff] [blame] | 69 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 70 | for (RVal::symbol_iterator SI = X.symbol_begin(), SE = X.symbol_end(); |
| 71 | SI != SE; ++SI) { |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 72 | LSymbols.insert(*SI); |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 73 | } |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 74 | } |
Ted Kremenek | 05a2378 | 2008-02-26 19:05:15 +0000 | [diff] [blame] | 75 | else { |
| 76 | RVal X = I.getData(); |
| 77 | |
Ted Kremenek | 4a4e524 | 2008-02-28 09:25:22 +0000 | [diff] [blame] | 78 | if (X.isUndef() && cast<UndefinedVal>(X).getData()) |
Ted Kremenek | 05a2378 | 2008-02-26 19:05:15 +0000 | [diff] [blame] | 79 | continue; |
| 80 | |
Ted Kremenek | 8133a26 | 2008-07-08 21:46:56 +0000 | [diff] [blame] | 81 | NewSt.Env = EnvMgr.RemoveBlkExpr(NewSt.Env, BlkExpr); |
Ted Kremenek | 05a2378 | 2008-02-26 19:05:15 +0000 | [diff] [blame] | 82 | } |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 83 | } |
Ted Kremenek | 016f52f | 2008-02-08 21:10:02 +0000 | [diff] [blame] | 84 | |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 85 | // Clean up the store. |
| 86 | DSymbols.clear(); |
| 87 | NewSt.St = StMgr->RemoveDeadBindings(St->getStore(), Loc, Liveness, DRoots, |
| 88 | LSymbols, DSymbols); |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 89 | |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 90 | // Remove the dead symbols from the symbol tracker. |
Ted Kremenek | 77d7ef8 | 2008-04-24 18:31:42 +0000 | [diff] [blame] | 91 | for (ValueState::ce_iterator I = St->ce_begin(), E=St->ce_end(); I!=E; ++I) { |
| 92 | |
| 93 | SymbolID sym = I.getKey(); |
| 94 | |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 95 | if (!LSymbols.count(sym)) { |
| 96 | DSymbols.insert(sym); |
Ted Kremenek | 77d7ef8 | 2008-04-24 18:31:42 +0000 | [diff] [blame] | 97 | NewSt.ConstEq = CEFactory.Remove(NewSt.ConstEq, sym); |
| 98 | } |
| 99 | } |
| 100 | |
| 101 | for (ValueState::cne_iterator I = St->cne_begin(), E=St->cne_end(); I!=E;++I){ |
| 102 | |
| 103 | SymbolID sym = I.getKey(); |
| 104 | |
Ted Kremenek | f59bf48 | 2008-07-17 18:38:48 +0000 | [diff] [blame] | 105 | if (!LSymbols.count(sym)) { |
| 106 | DSymbols.insert(sym); |
Ted Kremenek | 77d7ef8 | 2008-04-24 18:31:42 +0000 | [diff] [blame] | 107 | NewSt.ConstNotEq = CNEFactory.Remove(NewSt.ConstNotEq, sym); |
| 108 | } |
| 109 | } |
Ted Kremenek | 90e1481 | 2008-02-14 23:25:54 +0000 | [diff] [blame] | 110 | |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 111 | return getPersistentState(NewSt); |
Ted Kremenek | b87d909 | 2008-02-08 19:17:19 +0000 | [diff] [blame] | 112 | } |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 113 | |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 114 | const ValueState* ValueStateManager::SetRVal(const ValueState* St, LVal LV, |
| 115 | RVal V) { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 116 | |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 117 | Store OldStore = St->getStore(); |
| 118 | Store NewStore = StMgr->SetRVal(OldStore, LV, V); |
Ted Kremenek | 3271f8d | 2008-02-07 04:16:04 +0000 | [diff] [blame] | 119 | |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 120 | if (NewStore == OldStore) |
| 121 | return St; |
Ted Kremenek | 692416c | 2008-02-18 22:57:02 +0000 | [diff] [blame] | 122 | |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 123 | ValueState NewSt = *St; |
| 124 | NewSt.St = NewStore; |
| 125 | return getPersistentState(NewSt); |
Ted Kremenek | f66ea2cd | 2008-02-04 21:59:22 +0000 | [diff] [blame] | 126 | } |
| 127 | |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 128 | const ValueState* ValueStateManager::Unbind(const ValueState* St, LVal LV) { |
| 129 | Store OldStore = St->getStore(); |
| 130 | Store NewStore = StMgr->Remove(OldStore, LV); |
| 131 | |
| 132 | if (NewStore == OldStore) |
| 133 | return St; |
| 134 | |
| 135 | ValueState NewSt = *St; |
| 136 | NewSt.St = NewStore; |
| 137 | return getPersistentState(NewSt); |
| 138 | } |
| 139 | |
| 140 | |
| 141 | const ValueState* ValueStateManager::AddNE(const ValueState* St, SymbolID sym, |
| 142 | const llvm::APSInt& V) { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 143 | |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 144 | // First, retrieve the NE-set associated with the given symbol. |
Ted Kremenek | e8fdc83 | 2008-07-07 16:21:19 +0000 | [diff] [blame] | 145 | ValueState::ConstNotEqTy::data_type* T = St->ConstNotEq.lookup(sym); |
| 146 | ValueState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet(); |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 147 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 148 | // Now add V to the NE set. |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 149 | S = ISetFactory.Add(S, &V); |
| 150 | |
| 151 | // Create a new state with the old binding replaced. |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 152 | ValueState NewSt = *St; |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 153 | NewSt.ConstNotEq = CNEFactory.Add(NewSt.ConstNotEq, sym, S); |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 154 | |
| 155 | // Get the persistent copy. |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 156 | return getPersistentState(NewSt); |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 157 | } |
| 158 | |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 159 | const ValueState* ValueStateManager::AddEQ(const ValueState* St, SymbolID sym, |
| 160 | const llvm::APSInt& V) { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 161 | |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 162 | // Create a new state with the old binding replaced. |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 163 | ValueState NewSt = *St; |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 164 | NewSt.ConstEq = CEFactory.Add(NewSt.ConstEq, sym, &V); |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 165 | |
| 166 | // Get the persistent copy. |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 167 | return getPersistentState(NewSt); |
Ted Kremenek | 862d5bb | 2008-02-06 00:54:14 +0000 | [diff] [blame] | 168 | } |
| 169 | |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 170 | const ValueState* ValueStateManager::getInitialState() { |
Ted Kremenek | 5a7b382 | 2008-02-26 23:37:01 +0000 | [diff] [blame] | 171 | |
Ted Kremenek | 8133a26 | 2008-07-08 21:46:56 +0000 | [diff] [blame] | 172 | ValueState StateImpl(EnvMgr.getInitialEnvironment(), |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 173 | StMgr->getInitialStore(), |
Ted Kremenek | 8133a26 | 2008-07-08 21:46:56 +0000 | [diff] [blame] | 174 | CNEFactory.GetEmptyMap(), |
| 175 | CEFactory.GetEmptyMap()); |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 176 | |
| 177 | return getPersistentState(StateImpl); |
| 178 | } |
| 179 | |
Ted Kremenek | 4323a57 | 2008-07-10 22:03:41 +0000 | [diff] [blame] | 180 | const ValueState* ValueStateManager::getPersistentState(ValueState& State) { |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 181 | |
| 182 | llvm::FoldingSetNodeID ID; |
| 183 | State.Profile(ID); |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 184 | void* InsertPos; |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 185 | |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 186 | if (ValueState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos)) |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 187 | return I; |
| 188 | |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 189 | ValueState* I = (ValueState*) Alloc.Allocate<ValueState>(); |
| 190 | new (I) ValueState(State); |
Ted Kremenek | 9153f73 | 2008-02-05 07:17:49 +0000 | [diff] [blame] | 191 | StateSet.InsertNode(I, InsertPos); |
| 192 | return I; |
| 193 | } |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 194 | |
Ted Kremenek | 461f977 | 2008-03-11 18:57:24 +0000 | [diff] [blame] | 195 | void ValueState::printDOT(std::ostream& Out, CheckerStatePrinter* P) const { |
| 196 | print(Out, P, "\\l", "\\|"); |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 197 | } |
| 198 | |
Ted Kremenek | 461f977 | 2008-03-11 18:57:24 +0000 | [diff] [blame] | 199 | void ValueState::printStdErr(CheckerStatePrinter* P) const { |
| 200 | print(*llvm::cerr, P); |
| 201 | } |
| 202 | |
| 203 | void ValueState::print(std::ostream& Out, CheckerStatePrinter* P, |
| 204 | const char* nl, const char* sep) const { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 205 | |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 206 | // Print Variable Bindings |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 207 | Out << "Variables:" << nl; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 208 | |
| 209 | bool isFirst = true; |
| 210 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 211 | for (vb_iterator I = vb_begin(), E = vb_end(); I != E; ++I) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 212 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 213 | if (isFirst) isFirst = false; |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 214 | else Out << nl; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 215 | |
| 216 | Out << ' ' << I.getKey()->getName() << " : "; |
| 217 | I.getData().print(Out); |
| 218 | } |
| 219 | |
| 220 | // Print Subexpression bindings. |
| 221 | |
| 222 | isFirst = true; |
| 223 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 224 | for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 225 | |
| 226 | if (isFirst) { |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 227 | Out << nl << nl << "Sub-Expressions:" << nl; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 228 | isFirst = false; |
| 229 | } |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 230 | else { Out << nl; } |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 231 | |
| 232 | Out << " (" << (void*) I.getKey() << ") "; |
| 233 | I.getKey()->printPretty(Out); |
| 234 | Out << " : "; |
| 235 | I.getData().print(Out); |
| 236 | } |
| 237 | |
| 238 | // Print block-expression bindings. |
| 239 | |
| 240 | isFirst = true; |
| 241 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 242 | for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 243 | |
| 244 | if (isFirst) { |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 245 | Out << nl << nl << "Block-level Expressions:" << nl; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 246 | isFirst = false; |
| 247 | } |
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 << " (" << (void*) I.getKey() << ") "; |
| 251 | I.getKey()->printPretty(Out); |
| 252 | Out << " : "; |
| 253 | I.getData().print(Out); |
| 254 | } |
| 255 | |
| 256 | // Print equality constraints. |
| 257 | |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 258 | if (!ConstEq.isEmpty()) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 259 | |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 260 | Out << nl << sep << "'==' constraints:"; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 261 | |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 262 | for (ConstEqTy::iterator I = ConstEq.begin(), |
| 263 | E = ConstEq.end(); I!=E; ++I) { |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 264 | |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 265 | Out << nl << " $" << I.getKey() |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 266 | << " : " << I.getData()->toString(); |
| 267 | } |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 268 | } |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 269 | |
| 270 | // Print != constraints. |
| 271 | |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 272 | if (!ConstNotEq.isEmpty()) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 273 | |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 274 | Out << nl << sep << "'!=' constraints:"; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 275 | |
Ted Kremenek | aed9b6a | 2008-02-28 10:21:43 +0000 | [diff] [blame] | 276 | for (ConstNotEqTy::iterator I = ConstNotEq.begin(), |
| 277 | EI = ConstNotEq.end(); I != EI; ++I) { |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 278 | |
Ted Kremenek | 59894f9 | 2008-03-04 18:30:35 +0000 | [diff] [blame] | 279 | Out << nl << " $" << I.getKey() << " : "; |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 280 | isFirst = true; |
| 281 | |
Ted Kremenek | aa1c4e5 | 2008-02-21 18:02:17 +0000 | [diff] [blame] | 282 | IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end(); |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 283 | |
| 284 | for ( ; J != EJ; ++J) { |
| 285 | if (isFirst) isFirst = false; |
| 286 | else Out << ", "; |
| 287 | |
| 288 | Out << (*J)->toString(); |
| 289 | } |
| 290 | } |
| 291 | } |
Ted Kremenek | 461f977 | 2008-03-11 18:57:24 +0000 | [diff] [blame] | 292 | |
| 293 | // Print checker-specific data. |
| 294 | |
| 295 | if (P && CheckerState) |
| 296 | P->PrintCheckerState(Out, CheckerState, nl, sep); |
Ted Kremenek | e7d2211 | 2008-02-11 19:21:59 +0000 | [diff] [blame] | 297 | } |
Ted Kremenek | 729a9a2 | 2008-07-17 23:15:45 +0000 | [diff] [blame^] | 298 | |
| 299 | //===----------------------------------------------------------------------===// |
| 300 | // "Assume" logic. |
| 301 | //===----------------------------------------------------------------------===// |
| 302 | |
| 303 | const ValueState* ValueStateManager::Assume(const ValueState* St, LVal Cond, |
| 304 | bool Assumption, bool& isFeasible) { |
| 305 | |
| 306 | St = AssumeAux(St, Cond, Assumption, isFeasible); |
| 307 | |
| 308 | return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible) |
| 309 | : St; |
| 310 | } |
| 311 | |
| 312 | const ValueState* ValueStateManager::AssumeAux(const ValueState* St, LVal Cond, |
| 313 | bool Assumption, bool& isFeasible) { |
| 314 | |
| 315 | switch (Cond.getSubKind()) { |
| 316 | default: |
| 317 | assert (false && "'Assume' not implemented for this LVal."); |
| 318 | return St; |
| 319 | |
| 320 | case lval::SymbolValKind: |
| 321 | if (Assumption) |
| 322 | return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(), |
| 323 | BasicVals.getZeroWithPtrWidth(), isFeasible); |
| 324 | else |
| 325 | return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(), |
| 326 | BasicVals.getZeroWithPtrWidth(), isFeasible); |
| 327 | |
| 328 | |
| 329 | case lval::DeclValKind: |
| 330 | case lval::FuncValKind: |
| 331 | case lval::GotoLabelKind: |
| 332 | case lval::StringLiteralValKind: |
| 333 | isFeasible = Assumption; |
| 334 | return St; |
| 335 | |
| 336 | case lval::FieldOffsetKind: |
| 337 | return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(), |
| 338 | Assumption, isFeasible); |
| 339 | |
| 340 | case lval::ArrayOffsetKind: |
| 341 | return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(), |
| 342 | Assumption, isFeasible); |
| 343 | |
| 344 | case lval::ConcreteIntKind: { |
| 345 | bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0; |
| 346 | isFeasible = b ? Assumption : !Assumption; |
| 347 | return St; |
| 348 | } |
| 349 | } |
| 350 | } |
| 351 | |
| 352 | const ValueState* ValueStateManager::Assume(const ValueState* St, NonLVal Cond, |
| 353 | bool Assumption, bool& isFeasible) { |
| 354 | |
| 355 | St = AssumeAux(St, Cond, Assumption, isFeasible); |
| 356 | |
| 357 | return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible) |
| 358 | : St; |
| 359 | } |
| 360 | |
| 361 | const ValueState* ValueStateManager::AssumeAux(const ValueState* St, NonLVal Cond, |
| 362 | bool Assumption, bool& isFeasible) { |
| 363 | switch (Cond.getSubKind()) { |
| 364 | default: |
| 365 | assert (false && "'Assume' not implemented for this NonLVal."); |
| 366 | return St; |
| 367 | |
| 368 | |
| 369 | case nonlval::SymbolValKind: { |
| 370 | nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond); |
| 371 | SymbolID sym = SV.getSymbol(); |
| 372 | |
| 373 | if (Assumption) |
| 374 | return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)), |
| 375 | isFeasible); |
| 376 | else |
| 377 | return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)), |
| 378 | isFeasible); |
| 379 | } |
| 380 | |
| 381 | case nonlval::SymIntConstraintValKind: |
| 382 | return |
| 383 | AssumeSymInt(St, Assumption, |
| 384 | cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(), |
| 385 | isFeasible); |
| 386 | |
| 387 | case nonlval::ConcreteIntKind: { |
| 388 | bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0; |
| 389 | isFeasible = b ? Assumption : !Assumption; |
| 390 | return St; |
| 391 | } |
| 392 | |
| 393 | case nonlval::LValAsIntegerKind: { |
| 394 | return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(), |
| 395 | Assumption, isFeasible); |
| 396 | } |
| 397 | } |
| 398 | } |
| 399 | |
| 400 | const ValueState* ValueStateManager::AssumeSymNE(const ValueState* St, |
| 401 | SymbolID sym, const llvm::APSInt& V, |
| 402 | bool& isFeasible) { |
| 403 | |
| 404 | // First, determine if sym == X, where X != V. |
| 405 | if (const llvm::APSInt* X = St->getSymVal(sym)) { |
| 406 | isFeasible = *X != V; |
| 407 | return St; |
| 408 | } |
| 409 | |
| 410 | // Second, determine if sym != V. |
| 411 | if (St->isNotEqual(sym, V)) { |
| 412 | isFeasible = true; |
| 413 | return St; |
| 414 | } |
| 415 | |
| 416 | // If we reach here, sym is not a constant and we don't know if it is != V. |
| 417 | // Make that assumption. |
| 418 | |
| 419 | isFeasible = true; |
| 420 | return AddNE(St, sym, V); |
| 421 | } |
| 422 | |
| 423 | const ValueState* ValueStateManager::AssumeSymEQ(const ValueState* St, SymbolID sym, |
| 424 | const llvm::APSInt& V, bool& isFeasible) { |
| 425 | |
| 426 | // First, determine if sym == X, where X != V. |
| 427 | if (const llvm::APSInt* X = St->getSymVal(sym)) { |
| 428 | isFeasible = *X == V; |
| 429 | return St; |
| 430 | } |
| 431 | |
| 432 | // Second, determine if sym != V. |
| 433 | if (St->isNotEqual(sym, V)) { |
| 434 | isFeasible = false; |
| 435 | return St; |
| 436 | } |
| 437 | |
| 438 | // If we reach here, sym is not a constant and we don't know if it is == V. |
| 439 | // Make that assumption. |
| 440 | |
| 441 | isFeasible = true; |
| 442 | return AddEQ(St, sym, V); |
| 443 | } |
| 444 | |
| 445 | const ValueState* ValueStateManager::AssumeSymInt(const ValueState* St, |
| 446 | bool Assumption, |
| 447 | const SymIntConstraint& C, |
| 448 | bool& isFeasible) { |
| 449 | |
| 450 | switch (C.getOpcode()) { |
| 451 | default: |
| 452 | // No logic yet for other operators. |
| 453 | isFeasible = true; |
| 454 | return St; |
| 455 | |
| 456 | case BinaryOperator::EQ: |
| 457 | if (Assumption) |
| 458 | return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible); |
| 459 | else |
| 460 | return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 461 | |
| 462 | case BinaryOperator::NE: |
| 463 | if (Assumption) |
| 464 | return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 465 | else |
| 466 | return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible); |
| 467 | } |
| 468 | } |