blob: dd9bf697155ab430e96520acb764cc4333a13c9b [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"
Chris Lattner405674c2008-08-23 22:23:37 +000018#include "llvm/Support/raw_ostream.h"
Ted Kremenekf66ea2cd2008-02-04 21:59:22 +000019using 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
Chris Lattner405674c2008-08-23 22:23:37 +0000277 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) {
278 Out << nl << " $" << I.getKey();
279 llvm::raw_os_ostream OS(Out);
280 OS << " : " << *I.getData();
281 }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000282 }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000283
284 // Print != constraints.
Ted Kremenekae6814e2008-08-13 21:24:49 +0000285 // FIXME: Make just another printer do this.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000286
287 ConstNotEqTy CNE = get<ConstNotEqTy>();
288
289 if (!CNE.isEmpty()) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000290 Out << nl << sep << "'!=' constraints:";
Ted Kremeneke7d22112008-02-11 19:21:59 +0000291
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000292 for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000293 Out << nl << " $" << I.getKey() << " : ";
Ted Kremeneke7d22112008-02-11 19:21:59 +0000294 isFirst = true;
295
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000296 IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end();
Ted Kremeneke7d22112008-02-11 19:21:59 +0000297
298 for ( ; J != EJ; ++J) {
299 if (isFirst) isFirst = false;
300 else Out << ", ";
301
Chris Lattner9aa77f12008-08-17 07:19:51 +0000302 Out << *J;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000303 }
304 }
305 }
Ted Kremenek461f9772008-03-11 18:57:24 +0000306
Ted Kremenekae6814e2008-08-13 21:24:49 +0000307 // Print checker-specific data.
308 for ( ; Beg != End ; ++Beg) (*Beg)->Print(Out, this, nl, sep);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000309}
Ted Kremenek729a9a22008-07-17 23:15:45 +0000310
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000311void GRStateRef::printDOT(std::ostream& Out) const {
312 print(Out, "\\l", "\\|");
313}
314
315void GRStateRef::printStdErr() const {
316 print(*llvm::cerr);
317}
318
319void GRStateRef::print(std::ostream& Out, const char* nl, const char* sep)const{
320 GRState::Printer **beg = Mgr->Printers.empty() ? 0 : &Mgr->Printers[0];
321 GRState::Printer **end = !beg ? 0 : beg + Mgr->Printers.size();
Ted Kremeneka622d8c2008-08-19 22:24:03 +0000322 St->print(Out, *Mgr->StMgr, beg, end, nl, sep);
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000323}
324
Ted Kremenek72cd17f2008-08-14 21:16:54 +0000325//===----------------------------------------------------------------------===//
326// Generic Data Map.
327//===----------------------------------------------------------------------===//
328
329void* const* GRState::FindGDM(void* K) const {
330 return GDM.lookup(K);
331}
332
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000333void*
334GRStateManager::FindGDMContext(void* K,
335 void* (*CreateContext)(llvm::BumpPtrAllocator&),
336 void (*DeleteContext)(void*)) {
337
338 std::pair<void*, void (*)(void*)>& p = GDMContexts[K];
339 if (!p.first) {
340 p.first = CreateContext(Alloc);
341 p.second = DeleteContext;
342 }
343
344 return p.first;
345}
346
Ted Kremenek72cd17f2008-08-14 21:16:54 +0000347const GRState* GRStateManager::addGDM(const GRState* St, void* Key, void* Data){
348 GRState::GenericDataMap M1 = St->getGDM();
349 GRState::GenericDataMap M2 = GDMFactory.Add(M1, Key, Data);
350
351 if (M1 == M2)
352 return St;
353
354 GRState NewSt = *St;
355 NewSt.GDM = M2;
356 return getPersistentState(NewSt);
357}
Ted Kremenek584def72008-07-22 00:46:16 +0000358
359//===----------------------------------------------------------------------===//
360// Queries.
361//===----------------------------------------------------------------------===//
362
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000363bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000364 const llvm::APSInt& Y) {
365
Ted Kremenek584def72008-07-22 00:46:16 +0000366 RVal V = GetRVal(state, Ex);
367
368 if (lval::ConcreteInt* X = dyn_cast<lval::ConcreteInt>(&V))
369 return X->getValue() == Y;
370
371 if (nonlval::ConcreteInt* X = dyn_cast<nonlval::ConcreteInt>(&V))
372 return X->getValue() == Y;
373
374 if (nonlval::SymbolVal* X = dyn_cast<nonlval::SymbolVal>(&V))
375 return state->isEqual(X->getSymbol(), Y);
376
377 if (lval::SymbolVal* X = dyn_cast<lval::SymbolVal>(&V))
378 return state->isEqual(X->getSymbol(), Y);
379
380 return false;
381}
382
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000383bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) {
Ted Kremenek584def72008-07-22 00:46:16 +0000384 return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
385}
386
Ted Kremenek729a9a22008-07-17 23:15:45 +0000387//===----------------------------------------------------------------------===//
388// "Assume" logic.
389//===----------------------------------------------------------------------===//
390
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000391const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000392 bool Assumption, bool& isFeasible) {
393
394 St = AssumeAux(St, Cond, Assumption, isFeasible);
395
396 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
397 : St;
398}
399
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000400const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000401 bool Assumption, bool& isFeasible) {
402
403 switch (Cond.getSubKind()) {
404 default:
405 assert (false && "'Assume' not implemented for this LVal.");
406 return St;
407
408 case lval::SymbolValKind:
409 if (Assumption)
410 return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
411 BasicVals.getZeroWithPtrWidth(), isFeasible);
412 else
413 return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
414 BasicVals.getZeroWithPtrWidth(), isFeasible);
415
Ted Kremenek729a9a22008-07-17 23:15:45 +0000416 case lval::DeclValKind:
417 case lval::FuncValKind:
418 case lval::GotoLabelKind:
419 case lval::StringLiteralValKind:
420 isFeasible = Assumption;
421 return St;
422
423 case lval::FieldOffsetKind:
424 return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
425 Assumption, isFeasible);
426
427 case lval::ArrayOffsetKind:
428 return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
429 Assumption, isFeasible);
430
431 case lval::ConcreteIntKind: {
432 bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
433 isFeasible = b ? Assumption : !Assumption;
434 return St;
435 }
436 }
437}
438
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000439const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000440 bool Assumption, bool& isFeasible) {
441
442 St = AssumeAux(St, Cond, Assumption, isFeasible);
443
444 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
445 : St;
446}
447
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000448const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000449 bool Assumption, bool& isFeasible) {
450 switch (Cond.getSubKind()) {
451 default:
452 assert (false && "'Assume' not implemented for this NonLVal.");
453 return St;
454
455
456 case nonlval::SymbolValKind: {
457 nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
458 SymbolID sym = SV.getSymbol();
459
460 if (Assumption)
461 return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
462 isFeasible);
463 else
464 return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
465 isFeasible);
466 }
467
468 case nonlval::SymIntConstraintValKind:
469 return
470 AssumeSymInt(St, Assumption,
471 cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
472 isFeasible);
473
474 case nonlval::ConcreteIntKind: {
475 bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
476 isFeasible = b ? Assumption : !Assumption;
477 return St;
478 }
479
480 case nonlval::LValAsIntegerKind: {
481 return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
482 Assumption, isFeasible);
483 }
484 }
485}
486
Ted Kremenek729a9a22008-07-17 23:15:45 +0000487
Ted Kremenek729a9a22008-07-17 23:15:45 +0000488
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000489const GRState* GRStateManager::AssumeSymInt(const GRState* St,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000490 bool Assumption,
491 const SymIntConstraint& C,
492 bool& isFeasible) {
493
494 switch (C.getOpcode()) {
495 default:
496 // No logic yet for other operators.
497 isFeasible = true;
498 return St;
499
500 case BinaryOperator::EQ:
501 if (Assumption)
502 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
503 else
504 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
505
506 case BinaryOperator::NE:
507 if (Assumption)
508 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
509 else
510 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenek2619be02008-08-07 22:30:22 +0000511
512 case BinaryOperator::GE:
513 if (Assumption)
514 return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
515 else
516 return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
517
518 case BinaryOperator::LE:
519 if (Assumption)
520 return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
521 else
522 return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenek729a9a22008-07-17 23:15:45 +0000523 }
524}
Ted Kremenek2619be02008-08-07 22:30:22 +0000525
526//===----------------------------------------------------------------------===//
527// FIXME: This should go into a plug-in constraint engine.
528//===----------------------------------------------------------------------===//
529
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000530const GRState*
531GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000532 const llvm::APSInt& V, bool& isFeasible) {
533
534 // First, determine if sym == X, where X != V.
535 if (const llvm::APSInt* X = St->getSymVal(sym)) {
536 isFeasible = *X != V;
537 return St;
538 }
539
540 // Second, determine if sym != V.
541 if (St->isNotEqual(sym, V)) {
542 isFeasible = true;
543 return St;
544 }
545
546 // If we reach here, sym is not a constant and we don't know if it is != V.
547 // Make that assumption.
548
549 isFeasible = true;
550 return AddNE(St, sym, V);
551}
552
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000553const GRState*
554GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000555 const llvm::APSInt& V, bool& isFeasible) {
556
557 // First, determine if sym == X, where X != V.
558 if (const llvm::APSInt* X = St->getSymVal(sym)) {
559 isFeasible = *X == V;
560 return St;
561 }
562
563 // Second, determine if sym != V.
564 if (St->isNotEqual(sym, V)) {
565 isFeasible = false;
566 return St;
567 }
568
569 // If we reach here, sym is not a constant and we don't know if it is == V.
570 // Make that assumption.
571
572 isFeasible = true;
573 return AddEQ(St, sym, V);
574}
575
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000576const GRState*
577GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000578 const llvm::APSInt& V, bool& isFeasible) {
579
580 // FIXME: For now have assuming x < y be the same as assuming sym != V;
581 return AssumeSymNE(St, sym, V, isFeasible);
582}
583
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000584const GRState*
585GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000586 const llvm::APSInt& V, bool& isFeasible) {
587
588 // FIXME: For now have assuming x > y be the same as assuming sym != V;
589 return AssumeSymNE(St, sym, V, isFeasible);
590}
591
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000592const GRState*
593GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000594 const llvm::APSInt& V, bool& isFeasible) {
595
596 // FIXME: Primitive logic for now. Only reject a path if the value of
597 // sym is a constant X and !(X >= V).
598
599 if (const llvm::APSInt* X = St->getSymVal(sym)) {
600 isFeasible = *X >= V;
601 return St;
602 }
603
604 isFeasible = true;
605 return St;
606}
607
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000608const GRState*
609GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000610 const llvm::APSInt& V, bool& isFeasible) {
611
612 // FIXME: Primitive logic for now. Only reject a path if the value of
613 // sym is a constant X and !(X <= V).
614
615 if (const llvm::APSInt* X = St->getSymVal(sym)) {
616 isFeasible = *X <= V;
617 return St;
618 }
619
620 isFeasible = true;
621 return St;
622}
623