blob: f8725470c00335f3ac161f00c5362157b5630df6 [file] [log] [blame]
Ted Kremenek4adc81e2008-08-13 04:27:00 +00001//= GRState*cpp - Path-Sens. "State" for tracking valuues -----*- C++ -*--=//
Ted Kremenek9153f732008-02-05 07:17:49 +00002//
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 Kremenek4adc81e2008-08-13 04:27:00 +000010// This file defines SymbolID, ExprBindKey, and GRState*
Ted Kremenek9153f732008-02-05 07:17:49 +000011//
12//===----------------------------------------------------------------------===//
13
Ted Kremeneke7aa9a12008-08-17 02:59:30 +000014#include "clang/Analysis/PathSensitive/GRStateTrait.h"
Ted Kremenek4adc81e2008-08-13 04:27:00 +000015#include "clang/Analysis/PathSensitive/GRState.h"
Ted Kremenek90e14812008-02-14 23:25:54 +000016#include "llvm/ADT/SmallSet.h"
Ted Kremenek729a9a22008-07-17 23:15:45 +000017#include "clang/Analysis/PathSensitive/GRTransferFuncs.h"
Ted Kremenekf66ea2cd2008-02-04 21:59:22 +000018
19using namespace clang;
20
Ted Kremenek1c72ef02008-08-16 00:49:49 +000021GRStateManager::~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
36typedef llvm::ImmutableMap<SymbolID,GRState::IntSetTy> ConstNotEqTy;
Ted Kremenekffdbefd2008-08-17 03:10:22 +000037typedef llvm::ImmutableMap<SymbolID,const llvm::APSInt*> ConstEqTy;
Ted Kremenek1c72ef02008-08-16 00:49:49 +000038
Ted Kremenekffdbefd2008-08-17 03:10:22 +000039static int ConstEqTyIndex = 0;
Ted Kremenek1c72ef02008-08-16 00:49:49 +000040static int ConstNotEqTyIndex = 0;
41
42namespace clang {
Ted Kremeneke7aa9a12008-08-17 02:59:30 +000043 template<>
44 struct GRStateTrait<ConstNotEqTy> : public GRStatePartialTrait<ConstNotEqTy> {
45 static inline void* GDMIndex() { return &ConstNotEqTyIndex; }
Ted Kremenek1c72ef02008-08-16 00:49:49 +000046 };
Ted Kremenekffdbefd2008-08-17 03:10:22 +000047
48 template<>
49 struct GRStateTrait<ConstEqTy> : public GRStatePartialTrait<ConstEqTy> {
50 static inline void* GDMIndex() { return &ConstEqTyIndex; }
51 };
Ted Kremenek1c72ef02008-08-16 00:49:49 +000052}
53
Ted Kremenek4adc81e2008-08-13 04:27:00 +000054bool GRState::isNotEqual(SymbolID sym, const llvm::APSInt& V) const {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +000055
56 // Retrieve the NE-set associated with the given symbol.
Ted Kremenek1c72ef02008-08-16 00:49:49 +000057 const ConstNotEqTy::data_type* T = get<ConstNotEqTy>(sym);
Ted Kremenekaa1c4e52008-02-21 18:02:17 +000058
59 // See if V is present in the NE-set.
Ted Kremeneke8fdc832008-07-07 16:21:19 +000060 return T ? T->contains(&V) : false;
Ted Kremenek862d5bb2008-02-06 00:54:14 +000061}
62
Ted Kremenek4adc81e2008-08-13 04:27:00 +000063bool GRState::isEqual(SymbolID sym, const llvm::APSInt& V) const {
Ted Kremenek584def72008-07-22 00:46:16 +000064 // Retrieve the EQ-set associated with the given symbol.
Ted Kremenekffdbefd2008-08-17 03:10:22 +000065 const ConstEqTy::data_type* T = get<ConstEqTy>(sym);
Ted Kremenek584def72008-07-22 00:46:16 +000066 // See if V is present in the EQ-set.
67 return T ? **T == V : false;
68}
69
Ted Kremenek4adc81e2008-08-13 04:27:00 +000070const llvm::APSInt* GRState::getSymVal(SymbolID sym) const {
Ted Kremenekffdbefd2008-08-17 03:10:22 +000071 const ConstEqTy::data_type* T = get<ConstEqTy>(sym);
Ted Kremeneke8fdc832008-07-07 16:21:19 +000072 return T ? *T : NULL;
Ted Kremenek862d5bb2008-02-06 00:54:14 +000073}
74
Ted Kremenek4adc81e2008-08-13 04:27:00 +000075const GRState*
76GRStateManager::RemoveDeadBindings(const GRState* St, Stmt* Loc,
Ted Kremenek1c72ef02008-08-16 00:49:49 +000077 const LiveVariables& Liveness,
78 DeadSymbolsTy& DSymbols) {
Ted Kremenekb87d9092008-02-08 19:17:19 +000079
80 // This code essentially performs a "mark-and-sweep" of the VariableBindings.
81 // The roots are any Block-level exprs and Decls that our liveness algorithm
82 // tells us are live. We then see what Decls they may reference, and keep
83 // those around. This code more than likely can be made faster, and the
84 // frequency of which this method is called should be experimented with
Ted Kremenekf59bf482008-07-17 18:38:48 +000085 // for optimum performance.
86 DRoots.clear();
87 StoreManager::LiveSymbolsTy LSymbols;
Ted Kremeneke7d22112008-02-11 19:21:59 +000088
Ted Kremenek4adc81e2008-08-13 04:27:00 +000089 GRState NewSt = *St;
Ted Kremenekf59bf482008-07-17 18:38:48 +000090
91 // FIXME: Put this in environment.
92 // Clean up the environment.
Ted Kremeneke7d22112008-02-11 19:21:59 +000093
94 // Drop bindings for subexpressions.
Ted Kremenek8133a262008-07-08 21:46:56 +000095 NewSt.Env = EnvMgr.RemoveSubExprBindings(NewSt.Env);
Ted Kremeneke7d22112008-02-11 19:21:59 +000096
97 // Iterate over the block-expr bindings.
Ted Kremenekaa1c4e52008-02-21 18:02:17 +000098
Ted Kremenek4adc81e2008-08-13 04:27:00 +000099 for (GRState::beb_iterator I = St->beb_begin(), E = St->beb_end();
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000100 I!=E ; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000101 Expr* BlkExpr = I.getKey();
Ted Kremenekb87d9092008-02-08 19:17:19 +0000102
Ted Kremeneke7d22112008-02-11 19:21:59 +0000103 if (Liveness.isLive(Loc, BlkExpr)) {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000104 RVal X = I.getData();
Ted Kremenek90e14812008-02-14 23:25:54 +0000105
106 if (isa<lval::DeclVal>(X)) {
107 lval::DeclVal LV = cast<lval::DeclVal>(X);
Ted Kremenekf59bf482008-07-17 18:38:48 +0000108 DRoots.push_back(LV.getDecl());
Ted Kremenekb87d9092008-02-08 19:17:19 +0000109 }
Ted Kremenek90e14812008-02-14 23:25:54 +0000110
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000111 for (RVal::symbol_iterator SI = X.symbol_begin(), SE = X.symbol_end();
112 SI != SE; ++SI) {
Ted Kremenekf59bf482008-07-17 18:38:48 +0000113 LSymbols.insert(*SI);
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000114 }
Ted Kremenekb87d9092008-02-08 19:17:19 +0000115 }
Ted Kremenek05a23782008-02-26 19:05:15 +0000116 else {
117 RVal X = I.getData();
118
Ted Kremenek4a4e5242008-02-28 09:25:22 +0000119 if (X.isUndef() && cast<UndefinedVal>(X).getData())
Ted Kremenek05a23782008-02-26 19:05:15 +0000120 continue;
121
Ted Kremenek8133a262008-07-08 21:46:56 +0000122 NewSt.Env = EnvMgr.RemoveBlkExpr(NewSt.Env, BlkExpr);
Ted Kremenek05a23782008-02-26 19:05:15 +0000123 }
Ted Kremenekb87d9092008-02-08 19:17:19 +0000124 }
Ted Kremenek016f52f2008-02-08 21:10:02 +0000125
Ted Kremenekf59bf482008-07-17 18:38:48 +0000126 // Clean up the store.
127 DSymbols.clear();
128 NewSt.St = StMgr->RemoveDeadBindings(St->getStore(), Loc, Liveness, DRoots,
129 LSymbols, DSymbols);
Ted Kremenekb87d9092008-02-08 19:17:19 +0000130
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000131
132 GRStateRef state(getPersistentState(NewSt), *this);
133
Ted Kremenekf59bf482008-07-17 18:38:48 +0000134 // Remove the dead symbols from the symbol tracker.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000135 // FIXME: Refactor into something else that manages symbol values.
Ted Kremenek77d7ef82008-04-24 18:31:42 +0000136
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000137 ConstEqTy CE = state.get<ConstEqTy>();
138 ConstEqTy::Factory& CEFactory = state.get_context<ConstEqTy>();
139
140 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) {
141 SymbolID sym = I.getKey();
Ted Kremenekf59bf482008-07-17 18:38:48 +0000142 if (!LSymbols.count(sym)) {
143 DSymbols.insert(sym);
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000144 CE = CEFactory.Remove(CE, sym);
Ted Kremenek77d7ef82008-04-24 18:31:42 +0000145 }
146 }
147
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000148 ConstNotEqTy CNE = state.get<ConstNotEqTy>();
149 ConstNotEqTy::Factory& CNEFactory = state.get_context<ConstNotEqTy>();
150
151 for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) {
152 SymbolID sym = I.getKey();
Ted Kremenekf59bf482008-07-17 18:38:48 +0000153 if (!LSymbols.count(sym)) {
154 DSymbols.insert(sym);
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000155 CNE = CNEFactory.Remove(CNE, sym);
Ted Kremenek77d7ef82008-04-24 18:31:42 +0000156 }
157 }
Ted Kremenek90e14812008-02-14 23:25:54 +0000158
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000159 return state.set<ConstNotEqTy>(CNE);
Ted Kremenekb87d9092008-02-08 19:17:19 +0000160}
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000161
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000162const GRState* GRStateManager::SetRVal(const GRState* St, LVal LV,
Ted Kremenek4323a572008-07-10 22:03:41 +0000163 RVal V) {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000164
Ted Kremenek4323a572008-07-10 22:03:41 +0000165 Store OldStore = St->getStore();
166 Store NewStore = StMgr->SetRVal(OldStore, LV, V);
Ted Kremenek3271f8d2008-02-07 04:16:04 +0000167
Ted Kremenek4323a572008-07-10 22:03:41 +0000168 if (NewStore == OldStore)
169 return St;
Ted Kremenek692416c2008-02-18 22:57:02 +0000170
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000171 GRState NewSt = *St;
Ted Kremenek4323a572008-07-10 22:03:41 +0000172 NewSt.St = NewStore;
173 return getPersistentState(NewSt);
Ted Kremenekf66ea2cd2008-02-04 21:59:22 +0000174}
175
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000176const GRState* GRStateManager::Unbind(const GRState* St, LVal LV) {
Ted Kremenek4323a572008-07-10 22:03:41 +0000177 Store OldStore = St->getStore();
178 Store NewStore = StMgr->Remove(OldStore, LV);
179
180 if (NewStore == OldStore)
181 return St;
182
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000183 GRState NewSt = *St;
Ted Kremenek4323a572008-07-10 22:03:41 +0000184 NewSt.St = NewStore;
185 return getPersistentState(NewSt);
186}
187
188
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000189const GRState* GRStateManager::AddNE(const GRState* St, SymbolID sym,
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000190 const llvm::APSInt& V) {
191
192 GRStateRef state(St, *this);
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000193
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000194 // First, retrieve the NE-set associated with the given symbol.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000195 ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym);
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000196 GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000197
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000198 // Now add V to the NE set.
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000199 S = ISetFactory.Add(S, &V);
200
201 // Create a new state with the old binding replaced.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000202 return state.set<ConstNotEqTy>(sym, S);
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000203}
204
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000205const GRState* GRStateManager::AddEQ(const GRState* St, SymbolID sym,
Ted Kremenek4323a572008-07-10 22:03:41 +0000206 const llvm::APSInt& V) {
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000207 // Create a new state with the old binding replaced.
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000208 GRStateRef state(St, *this);
209 return state.set<ConstEqTy>(sym, &V);
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000210}
211
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000212const GRState* GRStateManager::getInitialState() {
Ted Kremenek5a7b3822008-02-26 23:37:01 +0000213
Ted Kremenek72cd17f2008-08-14 21:16:54 +0000214 GRState StateImpl(EnvMgr.getInitialEnvironment(), StMgr->getInitialStore(),
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000215 GDMFactory.GetEmptyMap());
Ted Kremenek9153f732008-02-05 07:17:49 +0000216
217 return getPersistentState(StateImpl);
218}
219
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000220const GRState* GRStateManager::getPersistentState(GRState& State) {
Ted Kremenek9153f732008-02-05 07:17:49 +0000221
222 llvm::FoldingSetNodeID ID;
223 State.Profile(ID);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000224 void* InsertPos;
Ted Kremenek9153f732008-02-05 07:17:49 +0000225
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000226 if (GRState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos))
Ted Kremenek9153f732008-02-05 07:17:49 +0000227 return I;
228
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000229 GRState* I = (GRState*) Alloc.Allocate<GRState>();
230 new (I) GRState(State);
Ted Kremenek9153f732008-02-05 07:17:49 +0000231 StateSet.InsertNode(I, InsertPos);
232 return I;
233}
Ted Kremeneke7d22112008-02-11 19:21:59 +0000234
Ted Kremenek59894f92008-03-04 18:30:35 +0000235
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000236//===----------------------------------------------------------------------===//
237// State pretty-printing.
238//===----------------------------------------------------------------------===//
Ted Kremenek461f9772008-03-11 18:57:24 +0000239
Ted Kremenekae6814e2008-08-13 21:24:49 +0000240void GRState::print(std::ostream& Out, Printer** Beg, Printer** End,
241 const char* nl, const char* sep) const {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000242
Ted Kremeneke7d22112008-02-11 19:21:59 +0000243 // Print Variable Bindings
Ted Kremenek59894f92008-03-04 18:30:35 +0000244 Out << "Variables:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000245
246 bool isFirst = true;
247
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000248 for (vb_iterator I = vb_begin(), E = vb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000249
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000250 if (isFirst) isFirst = false;
Ted Kremenek59894f92008-03-04 18:30:35 +0000251 else Out << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000252
253 Out << ' ' << I.getKey()->getName() << " : ";
254 I.getData().print(Out);
255 }
256
257 // Print Subexpression bindings.
258
259 isFirst = true;
260
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000261 for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000262
263 if (isFirst) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000264 Out << nl << nl << "Sub-Expressions:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000265 isFirst = false;
266 }
Ted Kremenek59894f92008-03-04 18:30:35 +0000267 else { Out << nl; }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000268
269 Out << " (" << (void*) I.getKey() << ") ";
270 I.getKey()->printPretty(Out);
271 Out << " : ";
272 I.getData().print(Out);
273 }
274
275 // Print block-expression bindings.
276
277 isFirst = true;
278
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000279 for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000280
281 if (isFirst) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000282 Out << nl << nl << "Block-level Expressions:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000283 isFirst = false;
284 }
Ted Kremenek59894f92008-03-04 18:30:35 +0000285 else { Out << nl; }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000286
287 Out << " (" << (void*) I.getKey() << ") ";
288 I.getKey()->printPretty(Out);
289 Out << " : ";
290 I.getData().print(Out);
291 }
292
293 // Print equality constraints.
Ted Kremenekae6814e2008-08-13 21:24:49 +0000294 // FIXME: Make just another printer do this.
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000295 ConstEqTy CE = get<ConstEqTy>();
296
297 if (!CE.isEmpty()) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000298 Out << nl << sep << "'==' constraints:";
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000299
300 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I)
Ted Kremenek59894f92008-03-04 18:30:35 +0000301 Out << nl << " $" << I.getKey()
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000302 << " : " << I.getData()->toString();
Ted Kremeneke7d22112008-02-11 19:21:59 +0000303 }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000304
305 // Print != constraints.
Ted Kremenekae6814e2008-08-13 21:24:49 +0000306 // FIXME: Make just another printer do this.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000307
308 ConstNotEqTy CNE = get<ConstNotEqTy>();
309
310 if (!CNE.isEmpty()) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000311 Out << nl << sep << "'!=' constraints:";
Ted Kremeneke7d22112008-02-11 19:21:59 +0000312
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000313 for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000314 Out << nl << " $" << I.getKey() << " : ";
Ted Kremeneke7d22112008-02-11 19:21:59 +0000315 isFirst = true;
316
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000317 IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end();
Ted Kremeneke7d22112008-02-11 19:21:59 +0000318
319 for ( ; J != EJ; ++J) {
320 if (isFirst) isFirst = false;
321 else Out << ", ";
322
323 Out << (*J)->toString();
324 }
325 }
326 }
Ted Kremenek461f9772008-03-11 18:57:24 +0000327
Ted Kremenekae6814e2008-08-13 21:24:49 +0000328 // Print checker-specific data.
329 for ( ; Beg != End ; ++Beg) (*Beg)->Print(Out, this, nl, sep);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000330}
Ted Kremenek729a9a22008-07-17 23:15:45 +0000331
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000332void GRStateRef::printDOT(std::ostream& Out) const {
333 print(Out, "\\l", "\\|");
334}
335
336void GRStateRef::printStdErr() const {
337 print(*llvm::cerr);
338}
339
340void GRStateRef::print(std::ostream& Out, const char* nl, const char* sep)const{
341 GRState::Printer **beg = Mgr->Printers.empty() ? 0 : &Mgr->Printers[0];
342 GRState::Printer **end = !beg ? 0 : beg + Mgr->Printers.size();
343 St->print(Out, beg, end, nl, sep);
344}
345
Ted Kremenek72cd17f2008-08-14 21:16:54 +0000346//===----------------------------------------------------------------------===//
347// Generic Data Map.
348//===----------------------------------------------------------------------===//
349
350void* const* GRState::FindGDM(void* K) const {
351 return GDM.lookup(K);
352}
353
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000354void*
355GRStateManager::FindGDMContext(void* K,
356 void* (*CreateContext)(llvm::BumpPtrAllocator&),
357 void (*DeleteContext)(void*)) {
358
359 std::pair<void*, void (*)(void*)>& p = GDMContexts[K];
360 if (!p.first) {
361 p.first = CreateContext(Alloc);
362 p.second = DeleteContext;
363 }
364
365 return p.first;
366}
367
Ted Kremenek72cd17f2008-08-14 21:16:54 +0000368const GRState* GRStateManager::addGDM(const GRState* St, void* Key, void* Data){
369 GRState::GenericDataMap M1 = St->getGDM();
370 GRState::GenericDataMap M2 = GDMFactory.Add(M1, Key, Data);
371
372 if (M1 == M2)
373 return St;
374
375 GRState NewSt = *St;
376 NewSt.GDM = M2;
377 return getPersistentState(NewSt);
378}
Ted Kremenek584def72008-07-22 00:46:16 +0000379
380//===----------------------------------------------------------------------===//
381// Queries.
382//===----------------------------------------------------------------------===//
383
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000384bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000385 const llvm::APSInt& Y) {
386
Ted Kremenek584def72008-07-22 00:46:16 +0000387 RVal V = GetRVal(state, Ex);
388
389 if (lval::ConcreteInt* X = dyn_cast<lval::ConcreteInt>(&V))
390 return X->getValue() == Y;
391
392 if (nonlval::ConcreteInt* X = dyn_cast<nonlval::ConcreteInt>(&V))
393 return X->getValue() == Y;
394
395 if (nonlval::SymbolVal* X = dyn_cast<nonlval::SymbolVal>(&V))
396 return state->isEqual(X->getSymbol(), Y);
397
398 if (lval::SymbolVal* X = dyn_cast<lval::SymbolVal>(&V))
399 return state->isEqual(X->getSymbol(), Y);
400
401 return false;
402}
403
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000404bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) {
Ted Kremenek584def72008-07-22 00:46:16 +0000405 return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
406}
407
Ted Kremenek729a9a22008-07-17 23:15:45 +0000408//===----------------------------------------------------------------------===//
409// "Assume" logic.
410//===----------------------------------------------------------------------===//
411
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000412const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000413 bool Assumption, bool& isFeasible) {
414
415 St = AssumeAux(St, Cond, Assumption, isFeasible);
416
417 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
418 : St;
419}
420
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000421const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000422 bool Assumption, bool& isFeasible) {
423
424 switch (Cond.getSubKind()) {
425 default:
426 assert (false && "'Assume' not implemented for this LVal.");
427 return St;
428
429 case lval::SymbolValKind:
430 if (Assumption)
431 return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
432 BasicVals.getZeroWithPtrWidth(), isFeasible);
433 else
434 return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
435 BasicVals.getZeroWithPtrWidth(), isFeasible);
436
Ted Kremenek729a9a22008-07-17 23:15:45 +0000437 case lval::DeclValKind:
438 case lval::FuncValKind:
439 case lval::GotoLabelKind:
440 case lval::StringLiteralValKind:
441 isFeasible = Assumption;
442 return St;
443
444 case lval::FieldOffsetKind:
445 return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
446 Assumption, isFeasible);
447
448 case lval::ArrayOffsetKind:
449 return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
450 Assumption, isFeasible);
451
452 case lval::ConcreteIntKind: {
453 bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
454 isFeasible = b ? Assumption : !Assumption;
455 return St;
456 }
457 }
458}
459
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000460const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000461 bool Assumption, bool& isFeasible) {
462
463 St = AssumeAux(St, Cond, Assumption, isFeasible);
464
465 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
466 : St;
467}
468
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000469const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000470 bool Assumption, bool& isFeasible) {
471 switch (Cond.getSubKind()) {
472 default:
473 assert (false && "'Assume' not implemented for this NonLVal.");
474 return St;
475
476
477 case nonlval::SymbolValKind: {
478 nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
479 SymbolID sym = SV.getSymbol();
480
481 if (Assumption)
482 return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
483 isFeasible);
484 else
485 return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
486 isFeasible);
487 }
488
489 case nonlval::SymIntConstraintValKind:
490 return
491 AssumeSymInt(St, Assumption,
492 cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
493 isFeasible);
494
495 case nonlval::ConcreteIntKind: {
496 bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
497 isFeasible = b ? Assumption : !Assumption;
498 return St;
499 }
500
501 case nonlval::LValAsIntegerKind: {
502 return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
503 Assumption, isFeasible);
504 }
505 }
506}
507
Ted Kremenek729a9a22008-07-17 23:15:45 +0000508
Ted Kremenek729a9a22008-07-17 23:15:45 +0000509
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000510const GRState* GRStateManager::AssumeSymInt(const GRState* St,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000511 bool Assumption,
512 const SymIntConstraint& C,
513 bool& isFeasible) {
514
515 switch (C.getOpcode()) {
516 default:
517 // No logic yet for other operators.
518 isFeasible = true;
519 return St;
520
521 case BinaryOperator::EQ:
522 if (Assumption)
523 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
524 else
525 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
526
527 case BinaryOperator::NE:
528 if (Assumption)
529 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
530 else
531 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenek2619be02008-08-07 22:30:22 +0000532
533 case BinaryOperator::GE:
534 if (Assumption)
535 return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
536 else
537 return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
538
539 case BinaryOperator::LE:
540 if (Assumption)
541 return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
542 else
543 return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenek729a9a22008-07-17 23:15:45 +0000544 }
545}
Ted Kremenek2619be02008-08-07 22:30:22 +0000546
547//===----------------------------------------------------------------------===//
548// FIXME: This should go into a plug-in constraint engine.
549//===----------------------------------------------------------------------===//
550
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000551const GRState*
552GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000553 const llvm::APSInt& V, bool& isFeasible) {
554
555 // First, determine if sym == X, where X != V.
556 if (const llvm::APSInt* X = St->getSymVal(sym)) {
557 isFeasible = *X != V;
558 return St;
559 }
560
561 // Second, determine if sym != V.
562 if (St->isNotEqual(sym, V)) {
563 isFeasible = true;
564 return St;
565 }
566
567 // If we reach here, sym is not a constant and we don't know if it is != V.
568 // Make that assumption.
569
570 isFeasible = true;
571 return AddNE(St, sym, V);
572}
573
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000574const GRState*
575GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000576 const llvm::APSInt& V, bool& isFeasible) {
577
578 // First, determine if sym == X, where X != V.
579 if (const llvm::APSInt* X = St->getSymVal(sym)) {
580 isFeasible = *X == V;
581 return St;
582 }
583
584 // Second, determine if sym != V.
585 if (St->isNotEqual(sym, V)) {
586 isFeasible = false;
587 return St;
588 }
589
590 // If we reach here, sym is not a constant and we don't know if it is == V.
591 // Make that assumption.
592
593 isFeasible = true;
594 return AddEQ(St, sym, V);
595}
596
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000597const GRState*
598GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000599 const llvm::APSInt& V, bool& isFeasible) {
600
601 // FIXME: For now have assuming x < y be the same as assuming sym != V;
602 return AssumeSymNE(St, sym, V, isFeasible);
603}
604
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000605const GRState*
606GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000607 const llvm::APSInt& V, bool& isFeasible) {
608
609 // FIXME: For now have assuming x > y be the same as assuming sym != V;
610 return AssumeSymNE(St, sym, V, isFeasible);
611}
612
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000613const GRState*
614GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000615 const llvm::APSInt& V, bool& isFeasible) {
616
617 // FIXME: Primitive logic for now. Only reject a path if the value of
618 // sym is a constant X and !(X >= V).
619
620 if (const llvm::APSInt* X = St->getSymVal(sym)) {
621 isFeasible = *X >= V;
622 return St;
623 }
624
625 isFeasible = true;
626 return St;
627}
628
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000629const GRState*
630GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000631 const llvm::APSInt& V, bool& isFeasible) {
632
633 // FIXME: Primitive logic for now. Only reject a path if the value of
634 // sym is a constant X and !(X <= V).
635
636 if (const llvm::APSInt* X = St->getSymVal(sym)) {
637 isFeasible = *X <= V;
638 return St;
639 }
640
641 isFeasible = true;
642 return St;
643}
644