blob: c9494fe7ea82548a2c4ce47374416226a7333f50 [file] [log] [blame]
Ted Kremenekabd89ac2008-08-13 04:27:00 +00001//= GRState*cpp - Path-Sens. "State" for tracking valuues -----*- C++ -*--=//
Ted Kremenek2d8dce32008-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 Kremenekabd89ac2008-08-13 04:27:00 +000010// This file defines SymbolID, ExprBindKey, and GRState*
Ted Kremenek2d8dce32008-02-05 07:17:49 +000011//
12//===----------------------------------------------------------------------===//
13
Ted Kremenek67ff8b92008-08-17 02:59:30 +000014#include "clang/Analysis/PathSensitive/GRStateTrait.h"
Ted Kremenekabd89ac2008-08-13 04:27:00 +000015#include "clang/Analysis/PathSensitive/GRState.h"
Ted Kremenek0e39dcf2008-02-14 23:25:54 +000016#include "llvm/ADT/SmallSet.h"
Ted Kremenekc7469542008-07-17 23:15:45 +000017#include "clang/Analysis/PathSensitive/GRTransferFuncs.h"
Ted Kremenek0eb0afa2008-02-04 21:59:22 +000018
19using namespace clang;
20
Ted Kremenekb0f2b9e2008-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 Kremenek80fcbb92008-08-17 03:10:22 +000037typedef llvm::ImmutableMap<SymbolID,const llvm::APSInt*> ConstEqTy;
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000038
Ted Kremenek80fcbb92008-08-17 03:10:22 +000039static int ConstEqTyIndex = 0;
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000040static int ConstNotEqTyIndex = 0;
41
42namespace clang {
Ted Kremenek67ff8b92008-08-17 02:59:30 +000043 template<>
44 struct GRStateTrait<ConstNotEqTy> : public GRStatePartialTrait<ConstNotEqTy> {
45 static inline void* GDMIndex() { return &ConstNotEqTyIndex; }
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000046 };
Ted Kremenek80fcbb92008-08-17 03:10:22 +000047
48 template<>
49 struct GRStateTrait<ConstEqTy> : public GRStatePartialTrait<ConstEqTy> {
50 static inline void* GDMIndex() { return &ConstEqTyIndex; }
51 };
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000052}
53
Ted Kremenekabd89ac2008-08-13 04:27:00 +000054bool GRState::isNotEqual(SymbolID sym, const llvm::APSInt& V) const {
Ted Kremenek07baa252008-02-21 18:02:17 +000055
56 // Retrieve the NE-set associated with the given symbol.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000057 const ConstNotEqTy::data_type* T = get<ConstNotEqTy>(sym);
Ted Kremenek07baa252008-02-21 18:02:17 +000058
59 // See if V is present in the NE-set.
Ted Kremenek6064a362008-07-07 16:21:19 +000060 return T ? T->contains(&V) : false;
Ted Kremenek13f31562008-02-06 00:54:14 +000061}
62
Ted Kremenekabd89ac2008-08-13 04:27:00 +000063bool GRState::isEqual(SymbolID sym, const llvm::APSInt& V) const {
Ted Kremenekbbafa5b2008-07-22 00:46:16 +000064 // Retrieve the EQ-set associated with the given symbol.
Ted Kremenek80fcbb92008-08-17 03:10:22 +000065 const ConstEqTy::data_type* T = get<ConstEqTy>(sym);
Ted Kremenekbbafa5b2008-07-22 00:46:16 +000066 // See if V is present in the EQ-set.
67 return T ? **T == V : false;
68}
69
Ted Kremenekabd89ac2008-08-13 04:27:00 +000070const llvm::APSInt* GRState::getSymVal(SymbolID sym) const {
Ted Kremenek80fcbb92008-08-17 03:10:22 +000071 const ConstEqTy::data_type* T = get<ConstEqTy>(sym);
Ted Kremenek6064a362008-07-07 16:21:19 +000072 return T ? *T : NULL;
Ted Kremenek13f31562008-02-06 00:54:14 +000073}
74
Ted Kremenekabd89ac2008-08-13 04:27:00 +000075const GRState*
76GRStateManager::RemoveDeadBindings(const GRState* St, Stmt* Loc,
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000077 const LiveVariables& Liveness,
78 DeadSymbolsTy& DSymbols) {
Ted Kremenekb8958d62008-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 Kremenekee930122008-07-17 18:38:48 +000085 // for optimum performance.
86 DRoots.clear();
87 StoreManager::LiveSymbolsTy LSymbols;
Ted Kremenek17c5f112008-02-11 19:21:59 +000088
Ted Kremenekabd89ac2008-08-13 04:27:00 +000089 GRState NewSt = *St;
Ted Kremenekee930122008-07-17 18:38:48 +000090
91 // FIXME: Put this in environment.
92 // Clean up the environment.
Ted Kremenek17c5f112008-02-11 19:21:59 +000093
94 // Drop bindings for subexpressions.
Ted Kremenek587ecc52008-07-08 21:46:56 +000095 NewSt.Env = EnvMgr.RemoveSubExprBindings(NewSt.Env);
Ted Kremenek17c5f112008-02-11 19:21:59 +000096
97 // Iterate over the block-expr bindings.
Ted Kremenek07baa252008-02-21 18:02:17 +000098
Ted Kremenekabd89ac2008-08-13 04:27:00 +000099 for (GRState::beb_iterator I = St->beb_begin(), E = St->beb_end();
Ted Kremenek07baa252008-02-21 18:02:17 +0000100 I!=E ; ++I) {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000101 Expr* BlkExpr = I.getKey();
Ted Kremenekb8958d62008-02-08 19:17:19 +0000102
Ted Kremenek17c5f112008-02-11 19:21:59 +0000103 if (Liveness.isLive(Loc, BlkExpr)) {
Ted Kremenek07baa252008-02-21 18:02:17 +0000104 RVal X = I.getData();
Ted Kremenek0e39dcf2008-02-14 23:25:54 +0000105
106 if (isa<lval::DeclVal>(X)) {
107 lval::DeclVal LV = cast<lval::DeclVal>(X);
Ted Kremenekee930122008-07-17 18:38:48 +0000108 DRoots.push_back(LV.getDecl());
Ted Kremenekb8958d62008-02-08 19:17:19 +0000109 }
Ted Kremenek0e39dcf2008-02-14 23:25:54 +0000110
Ted Kremenek07baa252008-02-21 18:02:17 +0000111 for (RVal::symbol_iterator SI = X.symbol_begin(), SE = X.symbol_end();
112 SI != SE; ++SI) {
Ted Kremenekee930122008-07-17 18:38:48 +0000113 LSymbols.insert(*SI);
Ted Kremenek07baa252008-02-21 18:02:17 +0000114 }
Ted Kremenekb8958d62008-02-08 19:17:19 +0000115 }
Ted Kremenek99ecce72008-02-26 19:05:15 +0000116 else {
117 RVal X = I.getData();
118
Ted Kremenekb31af242008-02-28 09:25:22 +0000119 if (X.isUndef() && cast<UndefinedVal>(X).getData())
Ted Kremenek99ecce72008-02-26 19:05:15 +0000120 continue;
121
Ted Kremenek587ecc52008-07-08 21:46:56 +0000122 NewSt.Env = EnvMgr.RemoveBlkExpr(NewSt.Env, BlkExpr);
Ted Kremenek99ecce72008-02-26 19:05:15 +0000123 }
Ted Kremenekb8958d62008-02-08 19:17:19 +0000124 }
Ted Kremenek08cfd832008-02-08 21:10:02 +0000125
Ted Kremenekee930122008-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 Kremenekb8958d62008-02-08 19:17:19 +0000130
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000131
132 GRStateRef state(getPersistentState(NewSt), *this);
133
Ted Kremenekee930122008-07-17 18:38:48 +0000134 // Remove the dead symbols from the symbol tracker.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000135 // FIXME: Refactor into something else that manages symbol values.
Ted Kremenek7487f942008-04-24 18:31:42 +0000136
Ted Kremenek80fcbb92008-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 Kremenekee930122008-07-17 18:38:48 +0000142 if (!LSymbols.count(sym)) {
143 DSymbols.insert(sym);
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000144 CE = CEFactory.Remove(CE, sym);
Ted Kremenek7487f942008-04-24 18:31:42 +0000145 }
146 }
Ted Kremenek2b697d02008-08-20 16:59:15 +0000147 state = state.set<ConstEqTy>(CE);
148
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000149 ConstNotEqTy CNE = state.get<ConstNotEqTy>();
150 ConstNotEqTy::Factory& CNEFactory = state.get_context<ConstNotEqTy>();
151
152 for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) {
153 SymbolID sym = I.getKey();
Ted Kremenekee930122008-07-17 18:38:48 +0000154 if (!LSymbols.count(sym)) {
155 DSymbols.insert(sym);
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000156 CNE = CNEFactory.Remove(CNE, sym);
Ted Kremenek7487f942008-04-24 18:31:42 +0000157 }
158 }
Ted Kremenek0e39dcf2008-02-14 23:25:54 +0000159
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000160 return state.set<ConstNotEqTy>(CNE);
Ted Kremenekb8958d62008-02-08 19:17:19 +0000161}
Ted Kremenek13f31562008-02-06 00:54:14 +0000162
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000163const GRState* GRStateManager::SetRVal(const GRState* St, LVal LV,
Ted Kremenekf22f8682008-07-10 22:03:41 +0000164 RVal V) {
Ted Kremenek07baa252008-02-21 18:02:17 +0000165
Ted Kremenekf22f8682008-07-10 22:03:41 +0000166 Store OldStore = St->getStore();
167 Store NewStore = StMgr->SetRVal(OldStore, LV, V);
Ted Kremenek9b32cd02008-02-07 04:16:04 +0000168
Ted Kremenekf22f8682008-07-10 22:03:41 +0000169 if (NewStore == OldStore)
170 return St;
Ted Kremenekbc965a62008-02-18 22:57:02 +0000171
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000172 GRState NewSt = *St;
Ted Kremenekf22f8682008-07-10 22:03:41 +0000173 NewSt.St = NewStore;
174 return getPersistentState(NewSt);
Ted Kremenek0eb0afa2008-02-04 21:59:22 +0000175}
176
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000177const GRState* GRStateManager::Unbind(const GRState* St, LVal LV) {
Ted Kremenekf22f8682008-07-10 22:03:41 +0000178 Store OldStore = St->getStore();
179 Store NewStore = StMgr->Remove(OldStore, LV);
180
181 if (NewStore == OldStore)
182 return St;
183
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000184 GRState NewSt = *St;
Ted Kremenekf22f8682008-07-10 22:03:41 +0000185 NewSt.St = NewStore;
186 return getPersistentState(NewSt);
187}
188
189
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000190const GRState* GRStateManager::AddNE(const GRState* St, SymbolID sym,
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000191 const llvm::APSInt& V) {
192
193 GRStateRef state(St, *this);
Ted Kremenek07baa252008-02-21 18:02:17 +0000194
Ted Kremenek13f31562008-02-06 00:54:14 +0000195 // First, retrieve the NE-set associated with the given symbol.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000196 ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym);
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000197 GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
Ted Kremenek13f31562008-02-06 00:54:14 +0000198
Ted Kremenek07baa252008-02-21 18:02:17 +0000199 // Now add V to the NE set.
Ted Kremenek13f31562008-02-06 00:54:14 +0000200 S = ISetFactory.Add(S, &V);
201
202 // Create a new state with the old binding replaced.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000203 return state.set<ConstNotEqTy>(sym, S);
Ted Kremenek13f31562008-02-06 00:54:14 +0000204}
205
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000206const GRState* GRStateManager::AddEQ(const GRState* St, SymbolID sym,
Ted Kremenekf22f8682008-07-10 22:03:41 +0000207 const llvm::APSInt& V) {
Ted Kremenek13f31562008-02-06 00:54:14 +0000208 // Create a new state with the old binding replaced.
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000209 GRStateRef state(St, *this);
210 return state.set<ConstEqTy>(sym, &V);
Ted Kremenek13f31562008-02-06 00:54:14 +0000211}
212
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000213const GRState* GRStateManager::getInitialState() {
Ted Kremenekad5d5c52008-02-26 23:37:01 +0000214
Ted Kremeneke2fb8c72008-08-19 16:51:45 +0000215 GRState StateImpl(EnvMgr.getInitialEnvironment(),
216 StMgr->getInitialStore(*this),
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000217 GDMFactory.GetEmptyMap());
Ted Kremeneke2fb8c72008-08-19 16:51:45 +0000218
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000219 return getPersistentState(StateImpl);
220}
221
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000222const GRState* GRStateManager::getPersistentState(GRState& State) {
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000223
224 llvm::FoldingSetNodeID ID;
225 State.Profile(ID);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000226 void* InsertPos;
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000227
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000228 if (GRState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos))
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000229 return I;
230
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000231 GRState* I = (GRState*) Alloc.Allocate<GRState>();
232 new (I) GRState(State);
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000233 StateSet.InsertNode(I, InsertPos);
234 return I;
235}
Ted Kremenek17c5f112008-02-11 19:21:59 +0000236
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000237
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000238//===----------------------------------------------------------------------===//
239// State pretty-printing.
240//===----------------------------------------------------------------------===//
Ted Kremenekd3656492008-03-11 18:57:24 +0000241
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000242void GRState::print(std::ostream& Out, StoreManager& StoreMgr,
243 Printer** Beg, Printer** End,
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000244 const char* nl, const char* sep) const {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000245
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000246 // Print the store.
247 StoreMgr.print(getStore(), Out, nl, sep);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000248
249 // Print Subexpression bindings.
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000250 bool isFirst = true;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000251
Ted Kremenek07baa252008-02-21 18:02:17 +0000252 for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000253
254 if (isFirst) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000255 Out << nl << nl << "Sub-Expressions:" << nl;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000256 isFirst = false;
257 }
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000258 else { Out << nl; }
Ted Kremenek17c5f112008-02-11 19:21:59 +0000259
260 Out << " (" << (void*) I.getKey() << ") ";
261 I.getKey()->printPretty(Out);
262 Out << " : ";
263 I.getData().print(Out);
264 }
265
266 // Print block-expression bindings.
Ted Kremenek17c5f112008-02-11 19:21:59 +0000267 isFirst = true;
268
Ted Kremenek07baa252008-02-21 18:02:17 +0000269 for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000270
271 if (isFirst) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000272 Out << nl << nl << "Block-level Expressions:" << nl;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000273 isFirst = false;
274 }
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000275 else { Out << nl; }
Ted Kremenek17c5f112008-02-11 19:21:59 +0000276
277 Out << " (" << (void*) I.getKey() << ") ";
278 I.getKey()->printPretty(Out);
279 Out << " : ";
280 I.getData().print(Out);
281 }
282
283 // Print equality constraints.
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000284 // FIXME: Make just another printer do this.
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000285 ConstEqTy CE = get<ConstEqTy>();
286
287 if (!CE.isEmpty()) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000288 Out << nl << sep << "'==' constraints:";
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000289
290 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I)
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000291 Out << nl << " $" << I.getKey()
Chris Lattneread053a2008-08-17 07:19:51 +0000292 << " : " << *I.getData();
Ted Kremenek17c5f112008-02-11 19:21:59 +0000293 }
Ted Kremenek17c5f112008-02-11 19:21:59 +0000294
295 // Print != constraints.
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000296 // FIXME: Make just another printer do this.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000297
298 ConstNotEqTy CNE = get<ConstNotEqTy>();
299
300 if (!CNE.isEmpty()) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000301 Out << nl << sep << "'!=' constraints:";
Ted Kremenek17c5f112008-02-11 19:21:59 +0000302
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000303 for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000304 Out << nl << " $" << I.getKey() << " : ";
Ted Kremenek17c5f112008-02-11 19:21:59 +0000305 isFirst = true;
306
Ted Kremenek07baa252008-02-21 18:02:17 +0000307 IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end();
Ted Kremenek17c5f112008-02-11 19:21:59 +0000308
309 for ( ; J != EJ; ++J) {
310 if (isFirst) isFirst = false;
311 else Out << ", ";
312
Chris Lattneread053a2008-08-17 07:19:51 +0000313 Out << *J;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000314 }
315 }
316 }
Ted Kremenekd3656492008-03-11 18:57:24 +0000317
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000318 // Print checker-specific data.
319 for ( ; Beg != End ; ++Beg) (*Beg)->Print(Out, this, nl, sep);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000320}
Ted Kremenekc7469542008-07-17 23:15:45 +0000321
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000322void GRStateRef::printDOT(std::ostream& Out) const {
323 print(Out, "\\l", "\\|");
324}
325
326void GRStateRef::printStdErr() const {
327 print(*llvm::cerr);
328}
329
330void GRStateRef::print(std::ostream& Out, const char* nl, const char* sep)const{
331 GRState::Printer **beg = Mgr->Printers.empty() ? 0 : &Mgr->Printers[0];
332 GRState::Printer **end = !beg ? 0 : beg + Mgr->Printers.size();
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000333 St->print(Out, *Mgr->StMgr, beg, end, nl, sep);
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000334}
335
Ted Kremenek4ae925c2008-08-14 21:16:54 +0000336//===----------------------------------------------------------------------===//
337// Generic Data Map.
338//===----------------------------------------------------------------------===//
339
340void* const* GRState::FindGDM(void* K) const {
341 return GDM.lookup(K);
342}
343
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000344void*
345GRStateManager::FindGDMContext(void* K,
346 void* (*CreateContext)(llvm::BumpPtrAllocator&),
347 void (*DeleteContext)(void*)) {
348
349 std::pair<void*, void (*)(void*)>& p = GDMContexts[K];
350 if (!p.first) {
351 p.first = CreateContext(Alloc);
352 p.second = DeleteContext;
353 }
354
355 return p.first;
356}
357
Ted Kremenek4ae925c2008-08-14 21:16:54 +0000358const GRState* GRStateManager::addGDM(const GRState* St, void* Key, void* Data){
359 GRState::GenericDataMap M1 = St->getGDM();
360 GRState::GenericDataMap M2 = GDMFactory.Add(M1, Key, Data);
361
362 if (M1 == M2)
363 return St;
364
365 GRState NewSt = *St;
366 NewSt.GDM = M2;
367 return getPersistentState(NewSt);
368}
Ted Kremenekbbafa5b2008-07-22 00:46:16 +0000369
370//===----------------------------------------------------------------------===//
371// Queries.
372//===----------------------------------------------------------------------===//
373
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000374bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000375 const llvm::APSInt& Y) {
376
Ted Kremenekbbafa5b2008-07-22 00:46:16 +0000377 RVal V = GetRVal(state, Ex);
378
379 if (lval::ConcreteInt* X = dyn_cast<lval::ConcreteInt>(&V))
380 return X->getValue() == Y;
381
382 if (nonlval::ConcreteInt* X = dyn_cast<nonlval::ConcreteInt>(&V))
383 return X->getValue() == Y;
384
385 if (nonlval::SymbolVal* X = dyn_cast<nonlval::SymbolVal>(&V))
386 return state->isEqual(X->getSymbol(), Y);
387
388 if (lval::SymbolVal* X = dyn_cast<lval::SymbolVal>(&V))
389 return state->isEqual(X->getSymbol(), Y);
390
391 return false;
392}
393
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000394bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) {
Ted Kremenekbbafa5b2008-07-22 00:46:16 +0000395 return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
396}
397
Ted Kremenekc7469542008-07-17 23:15:45 +0000398//===----------------------------------------------------------------------===//
399// "Assume" logic.
400//===----------------------------------------------------------------------===//
401
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000402const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000403 bool Assumption, bool& isFeasible) {
404
405 St = AssumeAux(St, Cond, Assumption, isFeasible);
406
407 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
408 : St;
409}
410
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000411const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000412 bool Assumption, bool& isFeasible) {
413
414 switch (Cond.getSubKind()) {
415 default:
416 assert (false && "'Assume' not implemented for this LVal.");
417 return St;
418
419 case lval::SymbolValKind:
420 if (Assumption)
421 return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
422 BasicVals.getZeroWithPtrWidth(), isFeasible);
423 else
424 return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
425 BasicVals.getZeroWithPtrWidth(), isFeasible);
426
Ted Kremenekc7469542008-07-17 23:15:45 +0000427 case lval::DeclValKind:
428 case lval::FuncValKind:
429 case lval::GotoLabelKind:
430 case lval::StringLiteralValKind:
431 isFeasible = Assumption;
432 return St;
433
434 case lval::FieldOffsetKind:
435 return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
436 Assumption, isFeasible);
437
438 case lval::ArrayOffsetKind:
439 return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
440 Assumption, isFeasible);
441
442 case lval::ConcreteIntKind: {
443 bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
444 isFeasible = b ? Assumption : !Assumption;
445 return St;
446 }
447 }
448}
449
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000450const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000451 bool Assumption, bool& isFeasible) {
452
453 St = AssumeAux(St, Cond, Assumption, isFeasible);
454
455 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
456 : St;
457}
458
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000459const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000460 bool Assumption, bool& isFeasible) {
461 switch (Cond.getSubKind()) {
462 default:
463 assert (false && "'Assume' not implemented for this NonLVal.");
464 return St;
465
466
467 case nonlval::SymbolValKind: {
468 nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
469 SymbolID sym = SV.getSymbol();
470
471 if (Assumption)
472 return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
473 isFeasible);
474 else
475 return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
476 isFeasible);
477 }
478
479 case nonlval::SymIntConstraintValKind:
480 return
481 AssumeSymInt(St, Assumption,
482 cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
483 isFeasible);
484
485 case nonlval::ConcreteIntKind: {
486 bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
487 isFeasible = b ? Assumption : !Assumption;
488 return St;
489 }
490
491 case nonlval::LValAsIntegerKind: {
492 return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
493 Assumption, isFeasible);
494 }
495 }
496}
497
Ted Kremenekc7469542008-07-17 23:15:45 +0000498
Ted Kremenekc7469542008-07-17 23:15:45 +0000499
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000500const GRState* GRStateManager::AssumeSymInt(const GRState* St,
Ted Kremenekc7469542008-07-17 23:15:45 +0000501 bool Assumption,
502 const SymIntConstraint& C,
503 bool& isFeasible) {
504
505 switch (C.getOpcode()) {
506 default:
507 // No logic yet for other operators.
508 isFeasible = true;
509 return St;
510
511 case BinaryOperator::EQ:
512 if (Assumption)
513 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
514 else
515 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
516
517 case BinaryOperator::NE:
518 if (Assumption)
519 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
520 else
521 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenek26da9702008-08-07 22:30:22 +0000522
523 case BinaryOperator::GE:
524 if (Assumption)
525 return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
526 else
527 return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
528
529 case BinaryOperator::LE:
530 if (Assumption)
531 return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
532 else
533 return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenekc7469542008-07-17 23:15:45 +0000534 }
535}
Ted Kremenek26da9702008-08-07 22:30:22 +0000536
537//===----------------------------------------------------------------------===//
538// FIXME: This should go into a plug-in constraint engine.
539//===----------------------------------------------------------------------===//
540
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000541const GRState*
542GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000543 const llvm::APSInt& V, bool& isFeasible) {
544
545 // First, determine if sym == X, where X != V.
546 if (const llvm::APSInt* X = St->getSymVal(sym)) {
547 isFeasible = *X != V;
548 return St;
549 }
550
551 // Second, determine if sym != V.
552 if (St->isNotEqual(sym, V)) {
553 isFeasible = true;
554 return St;
555 }
556
557 // If we reach here, sym is not a constant and we don't know if it is != V.
558 // Make that assumption.
559
560 isFeasible = true;
561 return AddNE(St, sym, V);
562}
563
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000564const GRState*
565GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000566 const llvm::APSInt& V, bool& isFeasible) {
567
568 // First, determine if sym == X, where X != V.
569 if (const llvm::APSInt* X = St->getSymVal(sym)) {
570 isFeasible = *X == V;
571 return St;
572 }
573
574 // Second, determine if sym != V.
575 if (St->isNotEqual(sym, V)) {
576 isFeasible = false;
577 return St;
578 }
579
580 // If we reach here, sym is not a constant and we don't know if it is == V.
581 // Make that assumption.
582
583 isFeasible = true;
584 return AddEQ(St, sym, V);
585}
586
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000587const GRState*
588GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000589 const llvm::APSInt& V, bool& isFeasible) {
590
591 // FIXME: For now have assuming x < y be the same as assuming sym != V;
592 return AssumeSymNE(St, sym, V, isFeasible);
593}
594
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000595const GRState*
596GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000597 const llvm::APSInt& V, bool& isFeasible) {
598
599 // FIXME: For now have assuming x > y be the same as assuming sym != V;
600 return AssumeSymNE(St, sym, V, isFeasible);
601}
602
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000603const GRState*
604GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000605 const llvm::APSInt& V, bool& isFeasible) {
606
607 // FIXME: Primitive logic for now. Only reject a path if the value of
608 // sym is a constant X and !(X >= V).
609
610 if (const llvm::APSInt* X = St->getSymVal(sym)) {
611 isFeasible = *X >= V;
612 return St;
613 }
614
615 isFeasible = true;
616 return St;
617}
618
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000619const GRState*
620GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000621 const llvm::APSInt& V, bool& isFeasible) {
622
623 // FIXME: Primitive logic for now. Only reject a path if the value of
624 // sym is a constant X and !(X <= V).
625
626 if (const llvm::APSInt* X = St->getSymVal(sym)) {
627 isFeasible = *X <= V;
628 return St;
629 }
630
631 isFeasible = true;
632 return St;
633}
634