blob: e5dd6788dcf3277a1b3880dda6f39ac7b8c5d279 [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;
37
38static int ConstNotEqTyIndex = 0;
39
40namespace clang {
Ted Kremeneke7aa9a12008-08-17 02:59:30 +000041 template<>
42 struct GRStateTrait<ConstNotEqTy> : public GRStatePartialTrait<ConstNotEqTy> {
43 static inline void* GDMIndex() { return &ConstNotEqTyIndex; }
Ted Kremenek1c72ef02008-08-16 00:49:49 +000044 };
45}
46
Ted Kremenek4adc81e2008-08-13 04:27:00 +000047bool GRState::isNotEqual(SymbolID sym, const llvm::APSInt& V) const {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +000048
49 // Retrieve the NE-set associated with the given symbol.
Ted Kremenek1c72ef02008-08-16 00:49:49 +000050 const ConstNotEqTy::data_type* T = get<ConstNotEqTy>(sym);
Ted Kremenekaa1c4e52008-02-21 18:02:17 +000051
52 // See if V is present in the NE-set.
Ted Kremeneke8fdc832008-07-07 16:21:19 +000053 return T ? T->contains(&V) : false;
Ted Kremenek862d5bb2008-02-06 00:54:14 +000054}
55
Ted Kremenek4adc81e2008-08-13 04:27:00 +000056bool GRState::isEqual(SymbolID sym, const llvm::APSInt& V) const {
Ted Kremenek584def72008-07-22 00:46:16 +000057
58 // Retrieve the EQ-set associated with the given symbol.
59 const ConstEqTy::data_type* T = ConstEq.lookup(sym);
60
61 // See if V is present in the EQ-set.
62 return T ? **T == V : false;
63}
64
Ted Kremenek4adc81e2008-08-13 04:27:00 +000065const llvm::APSInt* GRState::getSymVal(SymbolID sym) const {
Ted Kremeneke8fdc832008-07-07 16:21:19 +000066 ConstEqTy::data_type* T = ConstEq.lookup(sym);
67 return T ? *T : NULL;
Ted Kremenek862d5bb2008-02-06 00:54:14 +000068}
69
Ted Kremenek4adc81e2008-08-13 04:27:00 +000070const GRState*
71GRStateManager::RemoveDeadBindings(const GRState* St, Stmt* Loc,
Ted Kremenek1c72ef02008-08-16 00:49:49 +000072 const LiveVariables& Liveness,
73 DeadSymbolsTy& DSymbols) {
Ted Kremenekb87d9092008-02-08 19:17:19 +000074
75 // This code essentially performs a "mark-and-sweep" of the VariableBindings.
76 // The roots are any Block-level exprs and Decls that our liveness algorithm
77 // tells us are live. We then see what Decls they may reference, and keep
78 // those around. This code more than likely can be made faster, and the
79 // frequency of which this method is called should be experimented with
Ted Kremenekf59bf482008-07-17 18:38:48 +000080 // for optimum performance.
81 DRoots.clear();
82 StoreManager::LiveSymbolsTy LSymbols;
Ted Kremeneke7d22112008-02-11 19:21:59 +000083
Ted Kremenek4adc81e2008-08-13 04:27:00 +000084 GRState NewSt = *St;
Ted Kremenekf59bf482008-07-17 18:38:48 +000085
86 // FIXME: Put this in environment.
87 // Clean up the environment.
Ted Kremeneke7d22112008-02-11 19:21:59 +000088
89 // Drop bindings for subexpressions.
Ted Kremenek8133a262008-07-08 21:46:56 +000090 NewSt.Env = EnvMgr.RemoveSubExprBindings(NewSt.Env);
Ted Kremeneke7d22112008-02-11 19:21:59 +000091
92 // Iterate over the block-expr bindings.
Ted Kremenekaa1c4e52008-02-21 18:02:17 +000093
Ted Kremenek4adc81e2008-08-13 04:27:00 +000094 for (GRState::beb_iterator I = St->beb_begin(), E = St->beb_end();
Ted Kremenekaa1c4e52008-02-21 18:02:17 +000095 I!=E ; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +000096 Expr* BlkExpr = I.getKey();
Ted Kremenekb87d9092008-02-08 19:17:19 +000097
Ted Kremeneke7d22112008-02-11 19:21:59 +000098 if (Liveness.isLive(Loc, BlkExpr)) {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +000099 RVal X = I.getData();
Ted Kremenek90e14812008-02-14 23:25:54 +0000100
101 if (isa<lval::DeclVal>(X)) {
102 lval::DeclVal LV = cast<lval::DeclVal>(X);
Ted Kremenekf59bf482008-07-17 18:38:48 +0000103 DRoots.push_back(LV.getDecl());
Ted Kremenekb87d9092008-02-08 19:17:19 +0000104 }
Ted Kremenek90e14812008-02-14 23:25:54 +0000105
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000106 for (RVal::symbol_iterator SI = X.symbol_begin(), SE = X.symbol_end();
107 SI != SE; ++SI) {
Ted Kremenekf59bf482008-07-17 18:38:48 +0000108 LSymbols.insert(*SI);
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000109 }
Ted Kremenekb87d9092008-02-08 19:17:19 +0000110 }
Ted Kremenek05a23782008-02-26 19:05:15 +0000111 else {
112 RVal X = I.getData();
113
Ted Kremenek4a4e5242008-02-28 09:25:22 +0000114 if (X.isUndef() && cast<UndefinedVal>(X).getData())
Ted Kremenek05a23782008-02-26 19:05:15 +0000115 continue;
116
Ted Kremenek8133a262008-07-08 21:46:56 +0000117 NewSt.Env = EnvMgr.RemoveBlkExpr(NewSt.Env, BlkExpr);
Ted Kremenek05a23782008-02-26 19:05:15 +0000118 }
Ted Kremenekb87d9092008-02-08 19:17:19 +0000119 }
Ted Kremenek016f52f2008-02-08 21:10:02 +0000120
Ted Kremenekf59bf482008-07-17 18:38:48 +0000121 // Clean up the store.
122 DSymbols.clear();
123 NewSt.St = StMgr->RemoveDeadBindings(St->getStore(), Loc, Liveness, DRoots,
124 LSymbols, DSymbols);
Ted Kremenekb87d9092008-02-08 19:17:19 +0000125
Ted Kremenekf59bf482008-07-17 18:38:48 +0000126 // Remove the dead symbols from the symbol tracker.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000127 // FIXME: Refactor into something else that manages symbol values.
128 for (GRState::ConstEqTy::iterator I = St->ConstEq.begin(),
129 E=St->ConstEq.end(); I!=E; ++I) {
Ted Kremenek77d7ef82008-04-24 18:31:42 +0000130
131 SymbolID sym = I.getKey();
132
Ted Kremenekf59bf482008-07-17 18:38:48 +0000133 if (!LSymbols.count(sym)) {
134 DSymbols.insert(sym);
Ted Kremenek77d7ef82008-04-24 18:31:42 +0000135 NewSt.ConstEq = CEFactory.Remove(NewSt.ConstEq, sym);
136 }
137 }
138
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000139 GRStateRef state(getPersistentState(NewSt), *this);
140 ConstNotEqTy CNE = state.get<ConstNotEqTy>();
141 ConstNotEqTy::Factory& CNEFactory = state.get_context<ConstNotEqTy>();
142
143 for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) {
144 SymbolID sym = I.getKey();
Ted Kremenekf59bf482008-07-17 18:38:48 +0000145 if (!LSymbols.count(sym)) {
146 DSymbols.insert(sym);
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000147 CNE = CNEFactory.Remove(CNE, sym);
Ted Kremenek77d7ef82008-04-24 18:31:42 +0000148 }
149 }
Ted Kremenek90e14812008-02-14 23:25:54 +0000150
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000151 return state.set<ConstNotEqTy>(CNE);
Ted Kremenekb87d9092008-02-08 19:17:19 +0000152}
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000153
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000154const GRState* GRStateManager::SetRVal(const GRState* St, LVal LV,
Ted Kremenek4323a572008-07-10 22:03:41 +0000155 RVal V) {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000156
Ted Kremenek4323a572008-07-10 22:03:41 +0000157 Store OldStore = St->getStore();
158 Store NewStore = StMgr->SetRVal(OldStore, LV, V);
Ted Kremenek3271f8d2008-02-07 04:16:04 +0000159
Ted Kremenek4323a572008-07-10 22:03:41 +0000160 if (NewStore == OldStore)
161 return St;
Ted Kremenek692416c2008-02-18 22:57:02 +0000162
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000163 GRState NewSt = *St;
Ted Kremenek4323a572008-07-10 22:03:41 +0000164 NewSt.St = NewStore;
165 return getPersistentState(NewSt);
Ted Kremenekf66ea2cd2008-02-04 21:59:22 +0000166}
167
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000168const GRState* GRStateManager::Unbind(const GRState* St, LVal LV) {
Ted Kremenek4323a572008-07-10 22:03:41 +0000169 Store OldStore = St->getStore();
170 Store NewStore = StMgr->Remove(OldStore, LV);
171
172 if (NewStore == OldStore)
173 return St;
174
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000175 GRState NewSt = *St;
Ted Kremenek4323a572008-07-10 22:03:41 +0000176 NewSt.St = NewStore;
177 return getPersistentState(NewSt);
178}
179
180
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000181const GRState* GRStateManager::AddNE(const GRState* St, SymbolID sym,
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000182 const llvm::APSInt& V) {
183
184 GRStateRef state(St, *this);
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000185
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000186 // First, retrieve the NE-set associated with the given symbol.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000187 ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym);
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000188 GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000189
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000190 // Now add V to the NE set.
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000191 S = ISetFactory.Add(S, &V);
192
193 // Create a new state with the old binding replaced.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000194 return state.set<ConstNotEqTy>(sym, S);
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000195}
196
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000197const GRState* GRStateManager::AddEQ(const GRState* St, SymbolID sym,
Ted Kremenek4323a572008-07-10 22:03:41 +0000198 const llvm::APSInt& V) {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000199
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000200 // Create a new state with the old binding replaced.
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000201 GRState NewSt = *St;
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000202 NewSt.ConstEq = CEFactory.Add(NewSt.ConstEq, sym, &V);
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000203
204 // Get the persistent copy.
Ted Kremeneke7d22112008-02-11 19:21:59 +0000205 return getPersistentState(NewSt);
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000206}
207
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000208const GRState* GRStateManager::getInitialState() {
Ted Kremenek5a7b3822008-02-26 23:37:01 +0000209
Ted Kremenek72cd17f2008-08-14 21:16:54 +0000210 GRState StateImpl(EnvMgr.getInitialEnvironment(), StMgr->getInitialStore(),
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000211 GDMFactory.GetEmptyMap(),
Ted Kremenek72cd17f2008-08-14 21:16:54 +0000212 CEFactory.GetEmptyMap());
Ted Kremenek9153f732008-02-05 07:17:49 +0000213
214 return getPersistentState(StateImpl);
215}
216
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000217const GRState* GRStateManager::getPersistentState(GRState& State) {
Ted Kremenek9153f732008-02-05 07:17:49 +0000218
219 llvm::FoldingSetNodeID ID;
220 State.Profile(ID);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000221 void* InsertPos;
Ted Kremenek9153f732008-02-05 07:17:49 +0000222
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000223 if (GRState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos))
Ted Kremenek9153f732008-02-05 07:17:49 +0000224 return I;
225
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000226 GRState* I = (GRState*) Alloc.Allocate<GRState>();
227 new (I) GRState(State);
Ted Kremenek9153f732008-02-05 07:17:49 +0000228 StateSet.InsertNode(I, InsertPos);
229 return I;
230}
Ted Kremeneke7d22112008-02-11 19:21:59 +0000231
Ted Kremenek59894f92008-03-04 18:30:35 +0000232
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000233//===----------------------------------------------------------------------===//
234// State pretty-printing.
235//===----------------------------------------------------------------------===//
Ted Kremenek461f9772008-03-11 18:57:24 +0000236
Ted Kremenekae6814e2008-08-13 21:24:49 +0000237void GRState::print(std::ostream& Out, Printer** Beg, Printer** End,
238 const char* nl, const char* sep) const {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000239
Ted Kremeneke7d22112008-02-11 19:21:59 +0000240 // Print Variable Bindings
Ted Kremenek59894f92008-03-04 18:30:35 +0000241 Out << "Variables:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000242
243 bool isFirst = true;
244
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000245 for (vb_iterator I = vb_begin(), E = vb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000246
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000247 if (isFirst) isFirst = false;
Ted Kremenek59894f92008-03-04 18:30:35 +0000248 else Out << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000249
250 Out << ' ' << I.getKey()->getName() << " : ";
251 I.getData().print(Out);
252 }
253
254 // Print Subexpression bindings.
255
256 isFirst = true;
257
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000258 for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000259
260 if (isFirst) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000261 Out << nl << nl << "Sub-Expressions:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000262 isFirst = false;
263 }
Ted Kremenek59894f92008-03-04 18:30:35 +0000264 else { Out << nl; }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000265
266 Out << " (" << (void*) I.getKey() << ") ";
267 I.getKey()->printPretty(Out);
268 Out << " : ";
269 I.getData().print(Out);
270 }
271
272 // Print block-expression bindings.
273
274 isFirst = true;
275
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000276 for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000277
278 if (isFirst) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000279 Out << nl << nl << "Block-level Expressions:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000280 isFirst = false;
281 }
Ted Kremenek59894f92008-03-04 18:30:35 +0000282 else { Out << nl; }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000283
284 Out << " (" << (void*) I.getKey() << ") ";
285 I.getKey()->printPretty(Out);
286 Out << " : ";
287 I.getData().print(Out);
288 }
289
290 // Print equality constraints.
Ted Kremenekae6814e2008-08-13 21:24:49 +0000291 // FIXME: Make just another printer do this.
Ted Kremeneke7d22112008-02-11 19:21:59 +0000292
Ted Kremenekaed9b6a2008-02-28 10:21:43 +0000293 if (!ConstEq.isEmpty()) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000294
Ted Kremenek59894f92008-03-04 18:30:35 +0000295 Out << nl << sep << "'==' constraints:";
Ted Kremeneke7d22112008-02-11 19:21:59 +0000296
Ted Kremenekaed9b6a2008-02-28 10:21:43 +0000297 for (ConstEqTy::iterator I = ConstEq.begin(),
298 E = ConstEq.end(); I!=E; ++I) {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000299
Ted Kremenek59894f92008-03-04 18:30:35 +0000300 Out << nl << " $" << I.getKey()
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000301 << " : " << I.getData()->toString();
302 }
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 Kremeneke7d22112008-02-11 19:21:59 +0000311
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
324 Out << (*J)->toString();
325 }
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