blob: e4022a2663bee82f805d05d214bd1ffb3aa4697a [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 Kremenekcaa37242008-08-19 16:51:45 +0000214 GRState StateImpl(EnvMgr.getInitialEnvironment(),
215 StMgr->getInitialStore(*this),
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000216 GDMFactory.GetEmptyMap());
Ted Kremenekcaa37242008-08-19 16:51:45 +0000217
Ted Kremenek9153f732008-02-05 07:17:49 +0000218 return getPersistentState(StateImpl);
219}
220
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000221const GRState* GRStateManager::getPersistentState(GRState& State) {
Ted Kremenek9153f732008-02-05 07:17:49 +0000222
223 llvm::FoldingSetNodeID ID;
224 State.Profile(ID);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000225 void* InsertPos;
Ted Kremenek9153f732008-02-05 07:17:49 +0000226
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000227 if (GRState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos))
Ted Kremenek9153f732008-02-05 07:17:49 +0000228 return I;
229
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000230 GRState* I = (GRState*) Alloc.Allocate<GRState>();
231 new (I) GRState(State);
Ted Kremenek9153f732008-02-05 07:17:49 +0000232 StateSet.InsertNode(I, InsertPos);
233 return I;
234}
Ted Kremeneke7d22112008-02-11 19:21:59 +0000235
Ted Kremenek59894f92008-03-04 18:30:35 +0000236
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000237//===----------------------------------------------------------------------===//
238// State pretty-printing.
239//===----------------------------------------------------------------------===//
Ted Kremenek461f9772008-03-11 18:57:24 +0000240
Ted Kremenekae6814e2008-08-13 21:24:49 +0000241void GRState::print(std::ostream& Out, Printer** Beg, Printer** End,
242 const char* nl, const char* sep) const {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000243
Ted Kremeneke7d22112008-02-11 19:21:59 +0000244 // Print Variable Bindings
Ted Kremenek59894f92008-03-04 18:30:35 +0000245 Out << "Variables:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000246
247 bool isFirst = true;
248
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000249 for (vb_iterator I = vb_begin(), E = vb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000250
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000251 if (isFirst) isFirst = false;
Ted Kremenek59894f92008-03-04 18:30:35 +0000252 else Out << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000253
254 Out << ' ' << I.getKey()->getName() << " : ";
255 I.getData().print(Out);
256 }
257
258 // Print Subexpression bindings.
259
260 isFirst = true;
261
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000262 for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000263
264 if (isFirst) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000265 Out << nl << nl << "Sub-Expressions:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000266 isFirst = false;
267 }
Ted Kremenek59894f92008-03-04 18:30:35 +0000268 else { Out << nl; }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000269
270 Out << " (" << (void*) I.getKey() << ") ";
271 I.getKey()->printPretty(Out);
272 Out << " : ";
273 I.getData().print(Out);
274 }
275
276 // Print block-expression bindings.
277
278 isFirst = true;
279
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000280 for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000281
282 if (isFirst) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000283 Out << nl << nl << "Block-level Expressions:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000284 isFirst = false;
285 }
Ted Kremenek59894f92008-03-04 18:30:35 +0000286 else { Out << nl; }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000287
288 Out << " (" << (void*) I.getKey() << ") ";
289 I.getKey()->printPretty(Out);
290 Out << " : ";
291 I.getData().print(Out);
292 }
293
294 // Print equality constraints.
Ted Kremenekae6814e2008-08-13 21:24:49 +0000295 // FIXME: Make just another printer do this.
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000296 ConstEqTy CE = get<ConstEqTy>();
297
298 if (!CE.isEmpty()) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000299 Out << nl << sep << "'==' constraints:";
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000300
301 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I)
Ted Kremenek59894f92008-03-04 18:30:35 +0000302 Out << nl << " $" << I.getKey()
Chris Lattner9aa77f12008-08-17 07:19:51 +0000303 << " : " << *I.getData();
Ted Kremeneke7d22112008-02-11 19:21:59 +0000304 }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000305
306 // Print != constraints.
Ted Kremenekae6814e2008-08-13 21:24:49 +0000307 // FIXME: Make just another printer do this.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000308
309 ConstNotEqTy CNE = get<ConstNotEqTy>();
310
311 if (!CNE.isEmpty()) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000312 Out << nl << sep << "'!=' constraints:";
Ted Kremeneke7d22112008-02-11 19:21:59 +0000313
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000314 for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000315 Out << nl << " $" << I.getKey() << " : ";
Ted Kremeneke7d22112008-02-11 19:21:59 +0000316 isFirst = true;
317
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000318 IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end();
Ted Kremeneke7d22112008-02-11 19:21:59 +0000319
320 for ( ; J != EJ; ++J) {
321 if (isFirst) isFirst = false;
322 else Out << ", ";
323
Chris Lattner9aa77f12008-08-17 07:19:51 +0000324 Out << *J;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000325 }
326 }
327 }
Ted Kremenek461f9772008-03-11 18:57:24 +0000328
Ted Kremenekae6814e2008-08-13 21:24:49 +0000329 // Print checker-specific data.
330 for ( ; Beg != End ; ++Beg) (*Beg)->Print(Out, this, nl, sep);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000331}
Ted Kremenek729a9a22008-07-17 23:15:45 +0000332
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000333void GRStateRef::printDOT(std::ostream& Out) const {
334 print(Out, "\\l", "\\|");
335}
336
337void GRStateRef::printStdErr() const {
338 print(*llvm::cerr);
339}
340
341void 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 Kremenek72cd17f2008-08-14 21:16:54 +0000347//===----------------------------------------------------------------------===//
348// Generic Data Map.
349//===----------------------------------------------------------------------===//
350
351void* const* GRState::FindGDM(void* K) const {
352 return GDM.lookup(K);
353}
354
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000355void*
356GRStateManager::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 Kremenek72cd17f2008-08-14 21:16:54 +0000369const 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 Kremenek584def72008-07-22 00:46:16 +0000380
381//===----------------------------------------------------------------------===//
382// Queries.
383//===----------------------------------------------------------------------===//
384
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000385bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000386 const llvm::APSInt& Y) {
387
Ted Kremenek584def72008-07-22 00:46:16 +0000388 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 Kremenek1c72ef02008-08-16 00:49:49 +0000405bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) {
Ted Kremenek584def72008-07-22 00:46:16 +0000406 return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
407}
408
Ted Kremenek729a9a22008-07-17 23:15:45 +0000409//===----------------------------------------------------------------------===//
410// "Assume" logic.
411//===----------------------------------------------------------------------===//
412
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000413const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000414 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 Kremenek4adc81e2008-08-13 04:27:00 +0000422const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000423 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 Kremenek729a9a22008-07-17 23:15:45 +0000438 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 Kremenek4adc81e2008-08-13 04:27:00 +0000461const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000462 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 Kremenek4adc81e2008-08-13 04:27:00 +0000470const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000471 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 Kremenek729a9a22008-07-17 23:15:45 +0000509
Ted Kremenek729a9a22008-07-17 23:15:45 +0000510
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000511const GRState* GRStateManager::AssumeSymInt(const GRState* St,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000512 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 Kremenek2619be02008-08-07 22:30:22 +0000533
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 Kremenek729a9a22008-07-17 23:15:45 +0000545 }
546}
Ted Kremenek2619be02008-08-07 22:30:22 +0000547
548//===----------------------------------------------------------------------===//
549// FIXME: This should go into a plug-in constraint engine.
550//===----------------------------------------------------------------------===//
551
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000552const GRState*
553GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000554 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 Kremenek4adc81e2008-08-13 04:27:00 +0000575const GRState*
576GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000577 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 Kremenek4adc81e2008-08-13 04:27:00 +0000598const GRState*
599GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000600 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 Kremenek4adc81e2008-08-13 04:27:00 +0000606const GRState*
607GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000608 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 Kremenek4adc81e2008-08-13 04:27:00 +0000614const GRState*
615GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000616 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 Kremenek4adc81e2008-08-13 04:27:00 +0000630const GRState*
631GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000632 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