blob: f1e07907fd1e905b858df6bb546afbae9cf0a7b9 [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
Ted Kremenekdf9cdf82008-08-20 17:08:29 +000091 NewSt.Env = EnvMgr.RemoveDeadBindings(NewSt.Env, Loc, Liveness,
92 DRoots, LSymbols);
Ted Kremenek016f52f2008-02-08 21:10:02 +000093
Ted Kremenekf59bf482008-07-17 18:38:48 +000094 // Clean up the store.
95 DSymbols.clear();
96 NewSt.St = StMgr->RemoveDeadBindings(St->getStore(), Loc, Liveness, DRoots,
97 LSymbols, DSymbols);
Ted Kremenekb87d9092008-02-08 19:17:19 +000098
Ted Kremenekffdbefd2008-08-17 03:10:22 +000099
100 GRStateRef state(getPersistentState(NewSt), *this);
101
Ted Kremenekf59bf482008-07-17 18:38:48 +0000102 // Remove the dead symbols from the symbol tracker.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000103 // FIXME: Refactor into something else that manages symbol values.
Ted Kremenek77d7ef82008-04-24 18:31:42 +0000104
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000105 ConstEqTy CE = state.get<ConstEqTy>();
106 ConstEqTy::Factory& CEFactory = state.get_context<ConstEqTy>();
107
108 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) {
109 SymbolID sym = I.getKey();
Ted Kremenekf59bf482008-07-17 18:38:48 +0000110 if (!LSymbols.count(sym)) {
111 DSymbols.insert(sym);
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000112 CE = CEFactory.Remove(CE, sym);
Ted Kremenek77d7ef82008-04-24 18:31:42 +0000113 }
114 }
Ted Kremenek4f7b4832008-08-20 16:59:15 +0000115 state = state.set<ConstEqTy>(CE);
116
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000117 ConstNotEqTy CNE = state.get<ConstNotEqTy>();
118 ConstNotEqTy::Factory& CNEFactory = state.get_context<ConstNotEqTy>();
119
120 for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) {
121 SymbolID sym = I.getKey();
Ted Kremenekf59bf482008-07-17 18:38:48 +0000122 if (!LSymbols.count(sym)) {
123 DSymbols.insert(sym);
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000124 CNE = CNEFactory.Remove(CNE, sym);
Ted Kremenek77d7ef82008-04-24 18:31:42 +0000125 }
126 }
Ted Kremenek90e14812008-02-14 23:25:54 +0000127
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000128 return state.set<ConstNotEqTy>(CNE);
Ted Kremenekb87d9092008-02-08 19:17:19 +0000129}
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000130
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000131const GRState* GRStateManager::SetRVal(const GRState* St, LVal LV,
Ted Kremenek4323a572008-07-10 22:03:41 +0000132 RVal V) {
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000133
Ted Kremenek4323a572008-07-10 22:03:41 +0000134 Store OldStore = St->getStore();
135 Store NewStore = StMgr->SetRVal(OldStore, LV, V);
Ted Kremenek3271f8d2008-02-07 04:16:04 +0000136
Ted Kremenek4323a572008-07-10 22:03:41 +0000137 if (NewStore == OldStore)
138 return St;
Ted Kremenek692416c2008-02-18 22:57:02 +0000139
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000140 GRState NewSt = *St;
Ted Kremenek4323a572008-07-10 22:03:41 +0000141 NewSt.St = NewStore;
142 return getPersistentState(NewSt);
Ted Kremenekf66ea2cd2008-02-04 21:59:22 +0000143}
144
Zhongxing Xubbe8ff42008-08-21 22:34:01 +0000145const GRState* GRStateManager::AddDecl(const GRState* St, const VarDecl* VD,
146 Expr* Ex, unsigned Count) {
147 Store OldStore = St->getStore();
148 Store NewStore;
149
150 if (Ex)
Ted Kremeneke53c0692008-08-23 00:50:55 +0000151 NewStore = StMgr->AddDecl(OldStore, *this, VD, Ex,
Zhongxing Xubbe8ff42008-08-21 22:34:01 +0000152 GetRVal(St, Ex), Count);
153 else
Ted Kremeneke53c0692008-08-23 00:50:55 +0000154 NewStore = StMgr->AddDecl(OldStore, *this, VD, Ex);
Zhongxing Xubbe8ff42008-08-21 22:34:01 +0000155
156 if (NewStore == OldStore)
157 return St;
Ted Kremeneke53c0692008-08-23 00:50:55 +0000158
Zhongxing Xubbe8ff42008-08-21 22:34:01 +0000159 GRState NewSt = *St;
160 NewSt.St = NewStore;
161 return getPersistentState(NewSt);
162}
163
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000164const GRState* GRStateManager::Unbind(const GRState* St, LVal LV) {
Ted Kremenek4323a572008-07-10 22:03:41 +0000165 Store OldStore = St->getStore();
166 Store NewStore = StMgr->Remove(OldStore, LV);
167
168 if (NewStore == OldStore)
169 return St;
170
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);
174}
175
176
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000177const GRState* GRStateManager::AddNE(const GRState* St, SymbolID sym,
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000178 const llvm::APSInt& V) {
179
180 GRStateRef state(St, *this);
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000181
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000182 // First, retrieve the NE-set associated with the given symbol.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000183 ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym);
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000184 GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000185
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000186 // Now add V to the NE set.
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000187 S = ISetFactory.Add(S, &V);
188
189 // Create a new state with the old binding replaced.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000190 return state.set<ConstNotEqTy>(sym, S);
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000191}
192
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000193const GRState* GRStateManager::AddEQ(const GRState* St, SymbolID sym,
Ted Kremenek4323a572008-07-10 22:03:41 +0000194 const llvm::APSInt& V) {
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000195 // Create a new state with the old binding replaced.
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000196 GRStateRef state(St, *this);
197 return state.set<ConstEqTy>(sym, &V);
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000198}
199
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000200const GRState* GRStateManager::getInitialState() {
Ted Kremenek5a7b3822008-02-26 23:37:01 +0000201
Ted Kremenekcaa37242008-08-19 16:51:45 +0000202 GRState StateImpl(EnvMgr.getInitialEnvironment(),
203 StMgr->getInitialStore(*this),
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000204 GDMFactory.GetEmptyMap());
Ted Kremenekcaa37242008-08-19 16:51:45 +0000205
Ted Kremenek9153f732008-02-05 07:17:49 +0000206 return getPersistentState(StateImpl);
207}
208
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000209const GRState* GRStateManager::getPersistentState(GRState& State) {
Ted Kremenek9153f732008-02-05 07:17:49 +0000210
211 llvm::FoldingSetNodeID ID;
212 State.Profile(ID);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000213 void* InsertPos;
Ted Kremenek9153f732008-02-05 07:17:49 +0000214
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000215 if (GRState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos))
Ted Kremenek9153f732008-02-05 07:17:49 +0000216 return I;
217
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000218 GRState* I = (GRState*) Alloc.Allocate<GRState>();
219 new (I) GRState(State);
Ted Kremenek9153f732008-02-05 07:17:49 +0000220 StateSet.InsertNode(I, InsertPos);
221 return I;
222}
Ted Kremeneke7d22112008-02-11 19:21:59 +0000223
Ted Kremenek59894f92008-03-04 18:30:35 +0000224
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000225//===----------------------------------------------------------------------===//
226// State pretty-printing.
227//===----------------------------------------------------------------------===//
Ted Kremenek461f9772008-03-11 18:57:24 +0000228
Ted Kremeneka622d8c2008-08-19 22:24:03 +0000229void GRState::print(std::ostream& Out, StoreManager& StoreMgr,
230 Printer** Beg, Printer** End,
Ted Kremenekae6814e2008-08-13 21:24:49 +0000231 const char* nl, const char* sep) const {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000232
Ted Kremeneka622d8c2008-08-19 22:24:03 +0000233 // Print the store.
234 StoreMgr.print(getStore(), Out, nl, sep);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000235
236 // Print Subexpression bindings.
Ted Kremeneka622d8c2008-08-19 22:24:03 +0000237 bool isFirst = true;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000238
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000239 for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000240
241 if (isFirst) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000242 Out << nl << nl << "Sub-Expressions:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000243 isFirst = false;
244 }
Ted Kremenek59894f92008-03-04 18:30:35 +0000245 else { Out << nl; }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000246
247 Out << " (" << (void*) I.getKey() << ") ";
248 I.getKey()->printPretty(Out);
249 Out << " : ";
250 I.getData().print(Out);
251 }
252
253 // Print block-expression bindings.
Ted Kremeneke7d22112008-02-11 19:21:59 +0000254 isFirst = true;
255
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000256 for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000257
258 if (isFirst) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000259 Out << nl << nl << "Block-level Expressions:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000260 isFirst = false;
261 }
Ted Kremenek59894f92008-03-04 18:30:35 +0000262 else { Out << nl; }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000263
264 Out << " (" << (void*) I.getKey() << ") ";
265 I.getKey()->printPretty(Out);
266 Out << " : ";
267 I.getData().print(Out);
268 }
269
270 // Print equality constraints.
Ted Kremenekae6814e2008-08-13 21:24:49 +0000271 // FIXME: Make just another printer do this.
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000272 ConstEqTy CE = get<ConstEqTy>();
273
274 if (!CE.isEmpty()) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000275 Out << nl << sep << "'==' constraints:";
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000276
277 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I)
Ted Kremenek59894f92008-03-04 18:30:35 +0000278 Out << nl << " $" << I.getKey()
Chris Lattner9aa77f12008-08-17 07:19:51 +0000279 << " : " << *I.getData();
Ted Kremeneke7d22112008-02-11 19:21:59 +0000280 }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000281
282 // Print != constraints.
Ted Kremenekae6814e2008-08-13 21:24:49 +0000283 // FIXME: Make just another printer do this.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000284
285 ConstNotEqTy CNE = get<ConstNotEqTy>();
286
287 if (!CNE.isEmpty()) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000288 Out << nl << sep << "'!=' constraints:";
Ted Kremeneke7d22112008-02-11 19:21:59 +0000289
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000290 for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000291 Out << nl << " $" << I.getKey() << " : ";
Ted Kremeneke7d22112008-02-11 19:21:59 +0000292 isFirst = true;
293
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000294 IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end();
Ted Kremeneke7d22112008-02-11 19:21:59 +0000295
296 for ( ; J != EJ; ++J) {
297 if (isFirst) isFirst = false;
298 else Out << ", ";
299
Chris Lattner9aa77f12008-08-17 07:19:51 +0000300 Out << *J;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000301 }
302 }
303 }
Ted Kremenek461f9772008-03-11 18:57:24 +0000304
Ted Kremenekae6814e2008-08-13 21:24:49 +0000305 // Print checker-specific data.
306 for ( ; Beg != End ; ++Beg) (*Beg)->Print(Out, this, nl, sep);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000307}
Ted Kremenek729a9a22008-07-17 23:15:45 +0000308
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000309void GRStateRef::printDOT(std::ostream& Out) const {
310 print(Out, "\\l", "\\|");
311}
312
313void GRStateRef::printStdErr() const {
314 print(*llvm::cerr);
315}
316
317void GRStateRef::print(std::ostream& Out, const char* nl, const char* sep)const{
318 GRState::Printer **beg = Mgr->Printers.empty() ? 0 : &Mgr->Printers[0];
319 GRState::Printer **end = !beg ? 0 : beg + Mgr->Printers.size();
Ted Kremeneka622d8c2008-08-19 22:24:03 +0000320 St->print(Out, *Mgr->StMgr, beg, end, nl, sep);
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000321}
322
Ted Kremenek72cd17f2008-08-14 21:16:54 +0000323//===----------------------------------------------------------------------===//
324// Generic Data Map.
325//===----------------------------------------------------------------------===//
326
327void* const* GRState::FindGDM(void* K) const {
328 return GDM.lookup(K);
329}
330
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000331void*
332GRStateManager::FindGDMContext(void* K,
333 void* (*CreateContext)(llvm::BumpPtrAllocator&),
334 void (*DeleteContext)(void*)) {
335
336 std::pair<void*, void (*)(void*)>& p = GDMContexts[K];
337 if (!p.first) {
338 p.first = CreateContext(Alloc);
339 p.second = DeleteContext;
340 }
341
342 return p.first;
343}
344
Ted Kremenek72cd17f2008-08-14 21:16:54 +0000345const GRState* GRStateManager::addGDM(const GRState* St, void* Key, void* Data){
346 GRState::GenericDataMap M1 = St->getGDM();
347 GRState::GenericDataMap M2 = GDMFactory.Add(M1, Key, Data);
348
349 if (M1 == M2)
350 return St;
351
352 GRState NewSt = *St;
353 NewSt.GDM = M2;
354 return getPersistentState(NewSt);
355}
Ted Kremenek584def72008-07-22 00:46:16 +0000356
357//===----------------------------------------------------------------------===//
358// Queries.
359//===----------------------------------------------------------------------===//
360
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000361bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000362 const llvm::APSInt& Y) {
363
Ted Kremenek584def72008-07-22 00:46:16 +0000364 RVal V = GetRVal(state, Ex);
365
366 if (lval::ConcreteInt* X = dyn_cast<lval::ConcreteInt>(&V))
367 return X->getValue() == Y;
368
369 if (nonlval::ConcreteInt* X = dyn_cast<nonlval::ConcreteInt>(&V))
370 return X->getValue() == Y;
371
372 if (nonlval::SymbolVal* X = dyn_cast<nonlval::SymbolVal>(&V))
373 return state->isEqual(X->getSymbol(), Y);
374
375 if (lval::SymbolVal* X = dyn_cast<lval::SymbolVal>(&V))
376 return state->isEqual(X->getSymbol(), Y);
377
378 return false;
379}
380
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000381bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) {
Ted Kremenek584def72008-07-22 00:46:16 +0000382 return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
383}
384
Ted Kremenek729a9a22008-07-17 23:15:45 +0000385//===----------------------------------------------------------------------===//
386// "Assume" logic.
387//===----------------------------------------------------------------------===//
388
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000389const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000390 bool Assumption, bool& isFeasible) {
391
392 St = AssumeAux(St, Cond, Assumption, isFeasible);
393
394 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
395 : St;
396}
397
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000398const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000399 bool Assumption, bool& isFeasible) {
400
401 switch (Cond.getSubKind()) {
402 default:
403 assert (false && "'Assume' not implemented for this LVal.");
404 return St;
405
406 case lval::SymbolValKind:
407 if (Assumption)
408 return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
409 BasicVals.getZeroWithPtrWidth(), isFeasible);
410 else
411 return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
412 BasicVals.getZeroWithPtrWidth(), isFeasible);
413
Ted Kremenek729a9a22008-07-17 23:15:45 +0000414 case lval::DeclValKind:
415 case lval::FuncValKind:
416 case lval::GotoLabelKind:
417 case lval::StringLiteralValKind:
418 isFeasible = Assumption;
419 return St;
420
421 case lval::FieldOffsetKind:
422 return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
423 Assumption, isFeasible);
424
425 case lval::ArrayOffsetKind:
426 return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
427 Assumption, isFeasible);
428
429 case lval::ConcreteIntKind: {
430 bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
431 isFeasible = b ? Assumption : !Assumption;
432 return St;
433 }
434 }
435}
436
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000437const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000438 bool Assumption, bool& isFeasible) {
439
440 St = AssumeAux(St, Cond, Assumption, isFeasible);
441
442 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
443 : St;
444}
445
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000446const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000447 bool Assumption, bool& isFeasible) {
448 switch (Cond.getSubKind()) {
449 default:
450 assert (false && "'Assume' not implemented for this NonLVal.");
451 return St;
452
453
454 case nonlval::SymbolValKind: {
455 nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
456 SymbolID sym = SV.getSymbol();
457
458 if (Assumption)
459 return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
460 isFeasible);
461 else
462 return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
463 isFeasible);
464 }
465
466 case nonlval::SymIntConstraintValKind:
467 return
468 AssumeSymInt(St, Assumption,
469 cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
470 isFeasible);
471
472 case nonlval::ConcreteIntKind: {
473 bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
474 isFeasible = b ? Assumption : !Assumption;
475 return St;
476 }
477
478 case nonlval::LValAsIntegerKind: {
479 return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
480 Assumption, isFeasible);
481 }
482 }
483}
484
Ted Kremenek729a9a22008-07-17 23:15:45 +0000485
Ted Kremenek729a9a22008-07-17 23:15:45 +0000486
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000487const GRState* GRStateManager::AssumeSymInt(const GRState* St,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000488 bool Assumption,
489 const SymIntConstraint& C,
490 bool& isFeasible) {
491
492 switch (C.getOpcode()) {
493 default:
494 // No logic yet for other operators.
495 isFeasible = true;
496 return St;
497
498 case BinaryOperator::EQ:
499 if (Assumption)
500 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
501 else
502 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
503
504 case BinaryOperator::NE:
505 if (Assumption)
506 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
507 else
508 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenek2619be02008-08-07 22:30:22 +0000509
510 case BinaryOperator::GE:
511 if (Assumption)
512 return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
513 else
514 return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
515
516 case BinaryOperator::LE:
517 if (Assumption)
518 return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
519 else
520 return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenek729a9a22008-07-17 23:15:45 +0000521 }
522}
Ted Kremenek2619be02008-08-07 22:30:22 +0000523
524//===----------------------------------------------------------------------===//
525// FIXME: This should go into a plug-in constraint engine.
526//===----------------------------------------------------------------------===//
527
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000528const GRState*
529GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000530 const llvm::APSInt& V, bool& isFeasible) {
531
532 // First, determine if sym == X, where X != V.
533 if (const llvm::APSInt* X = St->getSymVal(sym)) {
534 isFeasible = *X != V;
535 return St;
536 }
537
538 // Second, determine if sym != V.
539 if (St->isNotEqual(sym, V)) {
540 isFeasible = true;
541 return St;
542 }
543
544 // If we reach here, sym is not a constant and we don't know if it is != V.
545 // Make that assumption.
546
547 isFeasible = true;
548 return AddNE(St, sym, V);
549}
550
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000551const GRState*
552GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000553 const llvm::APSInt& V, bool& isFeasible) {
554
555 // First, determine if sym == X, where X != V.
556 if (const llvm::APSInt* X = St->getSymVal(sym)) {
557 isFeasible = *X == V;
558 return St;
559 }
560
561 // Second, determine if sym != V.
562 if (St->isNotEqual(sym, V)) {
563 isFeasible = false;
564 return St;
565 }
566
567 // If we reach here, sym is not a constant and we don't know if it is == V.
568 // Make that assumption.
569
570 isFeasible = true;
571 return AddEQ(St, sym, V);
572}
573
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000574const GRState*
575GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000576 const llvm::APSInt& V, bool& isFeasible) {
577
578 // FIXME: For now have assuming x < y be the same as assuming sym != V;
579 return AssumeSymNE(St, sym, V, isFeasible);
580}
581
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000582const GRState*
583GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000584 const llvm::APSInt& V, bool& isFeasible) {
585
586 // FIXME: For now have assuming x > y be the same as assuming sym != V;
587 return AssumeSymNE(St, sym, V, isFeasible);
588}
589
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000590const GRState*
591GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000592 const llvm::APSInt& V, bool& isFeasible) {
593
594 // FIXME: Primitive logic for now. Only reject a path if the value of
595 // sym is a constant X and !(X >= V).
596
597 if (const llvm::APSInt* X = St->getSymVal(sym)) {
598 isFeasible = *X >= V;
599 return St;
600 }
601
602 isFeasible = true;
603 return St;
604}
605
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000606const GRState*
607GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000608 const llvm::APSInt& V, bool& isFeasible) {
609
610 // FIXME: Primitive logic for now. Only reject a path if the value of
611 // sym is a constant X and !(X <= V).
612
613 if (const llvm::APSInt* X = St->getSymVal(sym)) {
614 isFeasible = *X <= V;
615 return St;
616 }
617
618 isFeasible = true;
619 return St;
620}
621