blob: 23467e2046dab4f18f352da93bf167a4b57a3187 [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 }
147
Ted Kremenekb0f2b9e2008-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 Kremenekee930122008-07-17 18:38:48 +0000153 if (!LSymbols.count(sym)) {
154 DSymbols.insert(sym);
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000155 CNE = CNEFactory.Remove(CNE, sym);
Ted Kremenek7487f942008-04-24 18:31:42 +0000156 }
157 }
Ted Kremenek0e39dcf2008-02-14 23:25:54 +0000158
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000159 return state.set<ConstNotEqTy>(CNE);
Ted Kremenekb8958d62008-02-08 19:17:19 +0000160}
Ted Kremenek13f31562008-02-06 00:54:14 +0000161
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000162const GRState* GRStateManager::SetRVal(const GRState* St, LVal LV,
Ted Kremenekf22f8682008-07-10 22:03:41 +0000163 RVal V) {
Ted Kremenek07baa252008-02-21 18:02:17 +0000164
Ted Kremenekf22f8682008-07-10 22:03:41 +0000165 Store OldStore = St->getStore();
166 Store NewStore = StMgr->SetRVal(OldStore, LV, V);
Ted Kremenek9b32cd02008-02-07 04:16:04 +0000167
Ted Kremenekf22f8682008-07-10 22:03:41 +0000168 if (NewStore == OldStore)
169 return St;
Ted Kremenekbc965a62008-02-18 22:57:02 +0000170
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000171 GRState NewSt = *St;
Ted Kremenekf22f8682008-07-10 22:03:41 +0000172 NewSt.St = NewStore;
173 return getPersistentState(NewSt);
Ted Kremenek0eb0afa2008-02-04 21:59:22 +0000174}
175
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000176const GRState* GRStateManager::Unbind(const GRState* St, LVal LV) {
Ted Kremenekf22f8682008-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 Kremenekabd89ac2008-08-13 04:27:00 +0000183 GRState NewSt = *St;
Ted Kremenekf22f8682008-07-10 22:03:41 +0000184 NewSt.St = NewStore;
185 return getPersistentState(NewSt);
186}
187
188
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000189const GRState* GRStateManager::AddNE(const GRState* St, SymbolID sym,
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000190 const llvm::APSInt& V) {
191
192 GRStateRef state(St, *this);
Ted Kremenek07baa252008-02-21 18:02:17 +0000193
Ted Kremenek13f31562008-02-06 00:54:14 +0000194 // First, retrieve the NE-set associated with the given symbol.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000195 ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym);
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000196 GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
Ted Kremenek13f31562008-02-06 00:54:14 +0000197
Ted Kremenek07baa252008-02-21 18:02:17 +0000198 // Now add V to the NE set.
Ted Kremenek13f31562008-02-06 00:54:14 +0000199 S = ISetFactory.Add(S, &V);
200
201 // Create a new state with the old binding replaced.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000202 return state.set<ConstNotEqTy>(sym, S);
Ted Kremenek13f31562008-02-06 00:54:14 +0000203}
204
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000205const GRState* GRStateManager::AddEQ(const GRState* St, SymbolID sym,
Ted Kremenekf22f8682008-07-10 22:03:41 +0000206 const llvm::APSInt& V) {
Ted Kremenek13f31562008-02-06 00:54:14 +0000207 // Create a new state with the old binding replaced.
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000208 GRStateRef state(St, *this);
209 return state.set<ConstEqTy>(sym, &V);
Ted Kremenek13f31562008-02-06 00:54:14 +0000210}
211
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000212const GRState* GRStateManager::getInitialState() {
Ted Kremenekad5d5c52008-02-26 23:37:01 +0000213
Ted Kremeneke2fb8c72008-08-19 16:51:45 +0000214 GRState StateImpl(EnvMgr.getInitialEnvironment(),
215 StMgr->getInitialStore(*this),
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000216 GDMFactory.GetEmptyMap());
Ted Kremeneke2fb8c72008-08-19 16:51:45 +0000217
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000218 return getPersistentState(StateImpl);
219}
220
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000221const GRState* GRStateManager::getPersistentState(GRState& State) {
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000222
223 llvm::FoldingSetNodeID ID;
224 State.Profile(ID);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000225 void* InsertPos;
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000226
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000227 if (GRState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos))
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000228 return I;
229
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000230 GRState* I = (GRState*) Alloc.Allocate<GRState>();
231 new (I) GRState(State);
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000232 StateSet.InsertNode(I, InsertPos);
233 return I;
234}
Ted Kremenek17c5f112008-02-11 19:21:59 +0000235
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000236
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000237//===----------------------------------------------------------------------===//
238// State pretty-printing.
239//===----------------------------------------------------------------------===//
Ted Kremenekd3656492008-03-11 18:57:24 +0000240
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000241void GRState::print(std::ostream& Out, StoreManager& StoreMgr,
242 Printer** Beg, Printer** End,
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000243 const char* nl, const char* sep) const {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000244
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000245 // Print the store.
246 StoreMgr.print(getStore(), Out, nl, sep);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000247
248 // Print Subexpression bindings.
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000249 bool isFirst = true;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000250
Ted Kremenek07baa252008-02-21 18:02:17 +0000251 for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000252
253 if (isFirst) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000254 Out << nl << nl << "Sub-Expressions:" << nl;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000255 isFirst = false;
256 }
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000257 else { Out << nl; }
Ted Kremenek17c5f112008-02-11 19:21:59 +0000258
259 Out << " (" << (void*) I.getKey() << ") ";
260 I.getKey()->printPretty(Out);
261 Out << " : ";
262 I.getData().print(Out);
263 }
264
265 // Print block-expression bindings.
Ted Kremenek17c5f112008-02-11 19:21:59 +0000266 isFirst = true;
267
Ted Kremenek07baa252008-02-21 18:02:17 +0000268 for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000269
270 if (isFirst) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000271 Out << nl << nl << "Block-level Expressions:" << nl;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000272 isFirst = false;
273 }
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000274 else { Out << nl; }
Ted Kremenek17c5f112008-02-11 19:21:59 +0000275
276 Out << " (" << (void*) I.getKey() << ") ";
277 I.getKey()->printPretty(Out);
278 Out << " : ";
279 I.getData().print(Out);
280 }
281
282 // Print equality constraints.
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000283 // FIXME: Make just another printer do this.
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000284 ConstEqTy CE = get<ConstEqTy>();
285
286 if (!CE.isEmpty()) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000287 Out << nl << sep << "'==' constraints:";
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000288
289 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I)
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000290 Out << nl << " $" << I.getKey()
Chris Lattneread053a2008-08-17 07:19:51 +0000291 << " : " << *I.getData();
Ted Kremenek17c5f112008-02-11 19:21:59 +0000292 }
Ted Kremenek17c5f112008-02-11 19:21:59 +0000293
294 // Print != constraints.
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000295 // FIXME: Make just another printer do this.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000296
297 ConstNotEqTy CNE = get<ConstNotEqTy>();
298
299 if (!CNE.isEmpty()) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000300 Out << nl << sep << "'!=' constraints:";
Ted Kremenek17c5f112008-02-11 19:21:59 +0000301
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000302 for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000303 Out << nl << " $" << I.getKey() << " : ";
Ted Kremenek17c5f112008-02-11 19:21:59 +0000304 isFirst = true;
305
Ted Kremenek07baa252008-02-21 18:02:17 +0000306 IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end();
Ted Kremenek17c5f112008-02-11 19:21:59 +0000307
308 for ( ; J != EJ; ++J) {
309 if (isFirst) isFirst = false;
310 else Out << ", ";
311
Chris Lattneread053a2008-08-17 07:19:51 +0000312 Out << *J;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000313 }
314 }
315 }
Ted Kremenekd3656492008-03-11 18:57:24 +0000316
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000317 // Print checker-specific data.
318 for ( ; Beg != End ; ++Beg) (*Beg)->Print(Out, this, nl, sep);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000319}
Ted Kremenekc7469542008-07-17 23:15:45 +0000320
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000321void GRStateRef::printDOT(std::ostream& Out) const {
322 print(Out, "\\l", "\\|");
323}
324
325void GRStateRef::printStdErr() const {
326 print(*llvm::cerr);
327}
328
329void GRStateRef::print(std::ostream& Out, const char* nl, const char* sep)const{
330 GRState::Printer **beg = Mgr->Printers.empty() ? 0 : &Mgr->Printers[0];
331 GRState::Printer **end = !beg ? 0 : beg + Mgr->Printers.size();
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000332 St->print(Out, *Mgr->StMgr, beg, end, nl, sep);
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000333}
334
Ted Kremenek4ae925c2008-08-14 21:16:54 +0000335//===----------------------------------------------------------------------===//
336// Generic Data Map.
337//===----------------------------------------------------------------------===//
338
339void* const* GRState::FindGDM(void* K) const {
340 return GDM.lookup(K);
341}
342
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000343void*
344GRStateManager::FindGDMContext(void* K,
345 void* (*CreateContext)(llvm::BumpPtrAllocator&),
346 void (*DeleteContext)(void*)) {
347
348 std::pair<void*, void (*)(void*)>& p = GDMContexts[K];
349 if (!p.first) {
350 p.first = CreateContext(Alloc);
351 p.second = DeleteContext;
352 }
353
354 return p.first;
355}
356
Ted Kremenek4ae925c2008-08-14 21:16:54 +0000357const GRState* GRStateManager::addGDM(const GRState* St, void* Key, void* Data){
358 GRState::GenericDataMap M1 = St->getGDM();
359 GRState::GenericDataMap M2 = GDMFactory.Add(M1, Key, Data);
360
361 if (M1 == M2)
362 return St;
363
364 GRState NewSt = *St;
365 NewSt.GDM = M2;
366 return getPersistentState(NewSt);
367}
Ted Kremenekbbafa5b2008-07-22 00:46:16 +0000368
369//===----------------------------------------------------------------------===//
370// Queries.
371//===----------------------------------------------------------------------===//
372
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000373bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000374 const llvm::APSInt& Y) {
375
Ted Kremenekbbafa5b2008-07-22 00:46:16 +0000376 RVal V = GetRVal(state, Ex);
377
378 if (lval::ConcreteInt* X = dyn_cast<lval::ConcreteInt>(&V))
379 return X->getValue() == Y;
380
381 if (nonlval::ConcreteInt* X = dyn_cast<nonlval::ConcreteInt>(&V))
382 return X->getValue() == Y;
383
384 if (nonlval::SymbolVal* X = dyn_cast<nonlval::SymbolVal>(&V))
385 return state->isEqual(X->getSymbol(), Y);
386
387 if (lval::SymbolVal* X = dyn_cast<lval::SymbolVal>(&V))
388 return state->isEqual(X->getSymbol(), Y);
389
390 return false;
391}
392
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000393bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) {
Ted Kremenekbbafa5b2008-07-22 00:46:16 +0000394 return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
395}
396
Ted Kremenekc7469542008-07-17 23:15:45 +0000397//===----------------------------------------------------------------------===//
398// "Assume" logic.
399//===----------------------------------------------------------------------===//
400
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000401const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000402 bool Assumption, bool& isFeasible) {
403
404 St = AssumeAux(St, Cond, Assumption, isFeasible);
405
406 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
407 : St;
408}
409
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000410const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000411 bool Assumption, bool& isFeasible) {
412
413 switch (Cond.getSubKind()) {
414 default:
415 assert (false && "'Assume' not implemented for this LVal.");
416 return St;
417
418 case lval::SymbolValKind:
419 if (Assumption)
420 return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
421 BasicVals.getZeroWithPtrWidth(), isFeasible);
422 else
423 return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
424 BasicVals.getZeroWithPtrWidth(), isFeasible);
425
Ted Kremenekc7469542008-07-17 23:15:45 +0000426 case lval::DeclValKind:
427 case lval::FuncValKind:
428 case lval::GotoLabelKind:
429 case lval::StringLiteralValKind:
430 isFeasible = Assumption;
431 return St;
432
433 case lval::FieldOffsetKind:
434 return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
435 Assumption, isFeasible);
436
437 case lval::ArrayOffsetKind:
438 return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
439 Assumption, isFeasible);
440
441 case lval::ConcreteIntKind: {
442 bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
443 isFeasible = b ? Assumption : !Assumption;
444 return St;
445 }
446 }
447}
448
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000449const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000450 bool Assumption, bool& isFeasible) {
451
452 St = AssumeAux(St, Cond, Assumption, isFeasible);
453
454 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
455 : St;
456}
457
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000458const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000459 bool Assumption, bool& isFeasible) {
460 switch (Cond.getSubKind()) {
461 default:
462 assert (false && "'Assume' not implemented for this NonLVal.");
463 return St;
464
465
466 case nonlval::SymbolValKind: {
467 nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
468 SymbolID sym = SV.getSymbol();
469
470 if (Assumption)
471 return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
472 isFeasible);
473 else
474 return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
475 isFeasible);
476 }
477
478 case nonlval::SymIntConstraintValKind:
479 return
480 AssumeSymInt(St, Assumption,
481 cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
482 isFeasible);
483
484 case nonlval::ConcreteIntKind: {
485 bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
486 isFeasible = b ? Assumption : !Assumption;
487 return St;
488 }
489
490 case nonlval::LValAsIntegerKind: {
491 return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
492 Assumption, isFeasible);
493 }
494 }
495}
496
Ted Kremenekc7469542008-07-17 23:15:45 +0000497
Ted Kremenekc7469542008-07-17 23:15:45 +0000498
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000499const GRState* GRStateManager::AssumeSymInt(const GRState* St,
Ted Kremenekc7469542008-07-17 23:15:45 +0000500 bool Assumption,
501 const SymIntConstraint& C,
502 bool& isFeasible) {
503
504 switch (C.getOpcode()) {
505 default:
506 // No logic yet for other operators.
507 isFeasible = true;
508 return St;
509
510 case BinaryOperator::EQ:
511 if (Assumption)
512 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
513 else
514 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
515
516 case BinaryOperator::NE:
517 if (Assumption)
518 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
519 else
520 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenek26da9702008-08-07 22:30:22 +0000521
522 case BinaryOperator::GE:
523 if (Assumption)
524 return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
525 else
526 return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
527
528 case BinaryOperator::LE:
529 if (Assumption)
530 return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
531 else
532 return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenekc7469542008-07-17 23:15:45 +0000533 }
534}
Ted Kremenek26da9702008-08-07 22:30:22 +0000535
536//===----------------------------------------------------------------------===//
537// FIXME: This should go into a plug-in constraint engine.
538//===----------------------------------------------------------------------===//
539
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000540const GRState*
541GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000542 const llvm::APSInt& V, bool& isFeasible) {
543
544 // First, determine if sym == X, where X != V.
545 if (const llvm::APSInt* X = St->getSymVal(sym)) {
546 isFeasible = *X != V;
547 return St;
548 }
549
550 // Second, determine if sym != V.
551 if (St->isNotEqual(sym, V)) {
552 isFeasible = true;
553 return St;
554 }
555
556 // If we reach here, sym is not a constant and we don't know if it is != V.
557 // Make that assumption.
558
559 isFeasible = true;
560 return AddNE(St, sym, V);
561}
562
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000563const GRState*
564GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000565 const llvm::APSInt& V, bool& isFeasible) {
566
567 // First, determine if sym == X, where X != V.
568 if (const llvm::APSInt* X = St->getSymVal(sym)) {
569 isFeasible = *X == V;
570 return St;
571 }
572
573 // Second, determine if sym != V.
574 if (St->isNotEqual(sym, V)) {
575 isFeasible = false;
576 return St;
577 }
578
579 // If we reach here, sym is not a constant and we don't know if it is == V.
580 // Make that assumption.
581
582 isFeasible = true;
583 return AddEQ(St, sym, V);
584}
585
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000586const GRState*
587GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000588 const llvm::APSInt& V, bool& isFeasible) {
589
590 // FIXME: For now have assuming x < y be the same as assuming sym != V;
591 return AssumeSymNE(St, sym, V, isFeasible);
592}
593
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000594const GRState*
595GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000596 const llvm::APSInt& V, bool& isFeasible) {
597
598 // FIXME: For now have assuming x > y be the same as assuming sym != V;
599 return AssumeSymNE(St, sym, V, isFeasible);
600}
601
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000602const GRState*
603GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000604 const llvm::APSInt& V, bool& isFeasible) {
605
606 // FIXME: Primitive logic for now. Only reject a path if the value of
607 // sym is a constant X and !(X >= V).
608
609 if (const llvm::APSInt* X = St->getSymVal(sym)) {
610 isFeasible = *X >= V;
611 return St;
612 }
613
614 isFeasible = true;
615 return St;
616}
617
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000618const GRState*
619GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000620 const llvm::APSInt& V, bool& isFeasible) {
621
622 // FIXME: Primitive logic for now. Only reject a path if the value of
623 // sym is a constant X and !(X <= V).
624
625 if (const llvm::APSInt* X = St->getSymVal(sym)) {
626 isFeasible = *X <= V;
627 return St;
628 }
629
630 isFeasible = true;
631 return St;
632}
633