blob: dd9bf697155ab430e96520acb764cc4333a13c9b [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"
Chris Lattner1c8962e2008-08-23 22:23:37 +000018#include "llvm/Support/raw_ostream.h"
Ted Kremenek0eb0afa2008-02-04 21:59:22 +000019using 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
Ted Kremenek3a539162008-08-20 17:08:29 +000091 NewSt.Env = EnvMgr.RemoveDeadBindings(NewSt.Env, Loc, Liveness,
92 DRoots, LSymbols);
Ted Kremenek08cfd832008-02-08 21:10:02 +000093
Ted Kremenekee930122008-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 Kremenekb8958d62008-02-08 19:17:19 +000098
Ted Kremenek80fcbb92008-08-17 03:10:22 +000099
100 GRStateRef state(getPersistentState(NewSt), *this);
101
Ted Kremenekee930122008-07-17 18:38:48 +0000102 // Remove the dead symbols from the symbol tracker.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000103 // FIXME: Refactor into something else that manages symbol values.
Ted Kremenek7487f942008-04-24 18:31:42 +0000104
Ted Kremenek80fcbb92008-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 Kremenekee930122008-07-17 18:38:48 +0000110 if (!LSymbols.count(sym)) {
111 DSymbols.insert(sym);
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000112 CE = CEFactory.Remove(CE, sym);
Ted Kremenek7487f942008-04-24 18:31:42 +0000113 }
114 }
Ted Kremenek2b697d02008-08-20 16:59:15 +0000115 state = state.set<ConstEqTy>(CE);
116
Ted Kremenekb0f2b9e2008-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 Kremenekee930122008-07-17 18:38:48 +0000122 if (!LSymbols.count(sym)) {
123 DSymbols.insert(sym);
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000124 CNE = CNEFactory.Remove(CNE, sym);
Ted Kremenek7487f942008-04-24 18:31:42 +0000125 }
126 }
Ted Kremenek0e39dcf2008-02-14 23:25:54 +0000127
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000128 return state.set<ConstNotEqTy>(CNE);
Ted Kremenekb8958d62008-02-08 19:17:19 +0000129}
Ted Kremenek13f31562008-02-06 00:54:14 +0000130
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000131const GRState* GRStateManager::SetRVal(const GRState* St, LVal LV,
Ted Kremenekf22f8682008-07-10 22:03:41 +0000132 RVal V) {
Ted Kremenek07baa252008-02-21 18:02:17 +0000133
Ted Kremenekf22f8682008-07-10 22:03:41 +0000134 Store OldStore = St->getStore();
135 Store NewStore = StMgr->SetRVal(OldStore, LV, V);
Ted Kremenek9b32cd02008-02-07 04:16:04 +0000136
Ted Kremenekf22f8682008-07-10 22:03:41 +0000137 if (NewStore == OldStore)
138 return St;
Ted Kremenekbc965a62008-02-18 22:57:02 +0000139
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000140 GRState NewSt = *St;
Ted Kremenekf22f8682008-07-10 22:03:41 +0000141 NewSt.St = NewStore;
142 return getPersistentState(NewSt);
Ted Kremenek0eb0afa2008-02-04 21:59:22 +0000143}
144
Zhongxing Xu2378ba02008-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 Kremenek4fbc6412008-08-23 00:50:55 +0000151 NewStore = StMgr->AddDecl(OldStore, *this, VD, Ex,
Zhongxing Xu2378ba02008-08-21 22:34:01 +0000152 GetRVal(St, Ex), Count);
153 else
Ted Kremenek4fbc6412008-08-23 00:50:55 +0000154 NewStore = StMgr->AddDecl(OldStore, *this, VD, Ex);
Zhongxing Xu2378ba02008-08-21 22:34:01 +0000155
156 if (NewStore == OldStore)
157 return St;
Ted Kremenek4fbc6412008-08-23 00:50:55 +0000158
Zhongxing Xu2378ba02008-08-21 22:34:01 +0000159 GRState NewSt = *St;
160 NewSt.St = NewStore;
161 return getPersistentState(NewSt);
162}
163
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000164const GRState* GRStateManager::Unbind(const GRState* St, LVal LV) {
Ted Kremenekf22f8682008-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 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);
174}
175
176
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000177const GRState* GRStateManager::AddNE(const GRState* St, SymbolID sym,
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000178 const llvm::APSInt& V) {
179
180 GRStateRef state(St, *this);
Ted Kremenek07baa252008-02-21 18:02:17 +0000181
Ted Kremenek13f31562008-02-06 00:54:14 +0000182 // First, retrieve the NE-set associated with the given symbol.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000183 ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym);
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000184 GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
Ted Kremenek13f31562008-02-06 00:54:14 +0000185
Ted Kremenek07baa252008-02-21 18:02:17 +0000186 // Now add V to the NE set.
Ted Kremenek13f31562008-02-06 00:54:14 +0000187 S = ISetFactory.Add(S, &V);
188
189 // Create a new state with the old binding replaced.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000190 return state.set<ConstNotEqTy>(sym, S);
Ted Kremenek13f31562008-02-06 00:54:14 +0000191}
192
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000193const GRState* GRStateManager::AddEQ(const GRState* St, SymbolID sym,
Ted Kremenekf22f8682008-07-10 22:03:41 +0000194 const llvm::APSInt& V) {
Ted Kremenek13f31562008-02-06 00:54:14 +0000195 // Create a new state with the old binding replaced.
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000196 GRStateRef state(St, *this);
197 return state.set<ConstEqTy>(sym, &V);
Ted Kremenek13f31562008-02-06 00:54:14 +0000198}
199
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000200const GRState* GRStateManager::getInitialState() {
Ted Kremenekad5d5c52008-02-26 23:37:01 +0000201
Ted Kremeneke2fb8c72008-08-19 16:51:45 +0000202 GRState StateImpl(EnvMgr.getInitialEnvironment(),
203 StMgr->getInitialStore(*this),
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000204 GDMFactory.GetEmptyMap());
Ted Kremeneke2fb8c72008-08-19 16:51:45 +0000205
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000206 return getPersistentState(StateImpl);
207}
208
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000209const GRState* GRStateManager::getPersistentState(GRState& State) {
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000210
211 llvm::FoldingSetNodeID ID;
212 State.Profile(ID);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000213 void* InsertPos;
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000214
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000215 if (GRState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos))
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000216 return I;
217
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000218 GRState* I = (GRState*) Alloc.Allocate<GRState>();
219 new (I) GRState(State);
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000220 StateSet.InsertNode(I, InsertPos);
221 return I;
222}
Ted Kremenek17c5f112008-02-11 19:21:59 +0000223
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000224
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000225//===----------------------------------------------------------------------===//
226// State pretty-printing.
227//===----------------------------------------------------------------------===//
Ted Kremenekd3656492008-03-11 18:57:24 +0000228
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000229void GRState::print(std::ostream& Out, StoreManager& StoreMgr,
230 Printer** Beg, Printer** End,
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000231 const char* nl, const char* sep) const {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000232
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000233 // Print the store.
234 StoreMgr.print(getStore(), Out, nl, sep);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000235
236 // Print Subexpression bindings.
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000237 bool isFirst = true;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000238
Ted Kremenek07baa252008-02-21 18:02:17 +0000239 for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000240
241 if (isFirst) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000242 Out << nl << nl << "Sub-Expressions:" << nl;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000243 isFirst = false;
244 }
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000245 else { Out << nl; }
Ted Kremenek17c5f112008-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 Kremenek17c5f112008-02-11 19:21:59 +0000254 isFirst = true;
255
Ted Kremenek07baa252008-02-21 18:02:17 +0000256 for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000257
258 if (isFirst) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000259 Out << nl << nl << "Block-level Expressions:" << nl;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000260 isFirst = false;
261 }
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000262 else { Out << nl; }
Ted Kremenek17c5f112008-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 Kremenekbccfbcc2008-08-13 21:24:49 +0000271 // FIXME: Make just another printer do this.
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000272 ConstEqTy CE = get<ConstEqTy>();
273
274 if (!CE.isEmpty()) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000275 Out << nl << sep << "'==' constraints:";
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000276
Chris Lattner1c8962e2008-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 Kremenek17c5f112008-02-11 19:21:59 +0000282 }
Ted Kremenek17c5f112008-02-11 19:21:59 +0000283
284 // Print != constraints.
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000285 // FIXME: Make just another printer do this.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000286
287 ConstNotEqTy CNE = get<ConstNotEqTy>();
288
289 if (!CNE.isEmpty()) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000290 Out << nl << sep << "'!=' constraints:";
Ted Kremenek17c5f112008-02-11 19:21:59 +0000291
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000292 for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000293 Out << nl << " $" << I.getKey() << " : ";
Ted Kremenek17c5f112008-02-11 19:21:59 +0000294 isFirst = true;
295
Ted Kremenek07baa252008-02-21 18:02:17 +0000296 IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end();
Ted Kremenek17c5f112008-02-11 19:21:59 +0000297
298 for ( ; J != EJ; ++J) {
299 if (isFirst) isFirst = false;
300 else Out << ", ";
301
Chris Lattneread053a2008-08-17 07:19:51 +0000302 Out << *J;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000303 }
304 }
305 }
Ted Kremenekd3656492008-03-11 18:57:24 +0000306
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000307 // Print checker-specific data.
308 for ( ; Beg != End ; ++Beg) (*Beg)->Print(Out, this, nl, sep);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000309}
Ted Kremenekc7469542008-07-17 23:15:45 +0000310
Ted Kremenekb0f2b9e2008-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 Kremenekbdff9a92008-08-19 22:24:03 +0000322 St->print(Out, *Mgr->StMgr, beg, end, nl, sep);
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000323}
324
Ted Kremenek4ae925c2008-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 Kremenekb0f2b9e2008-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 Kremenek4ae925c2008-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 Kremenekbbafa5b2008-07-22 00:46:16 +0000358
359//===----------------------------------------------------------------------===//
360// Queries.
361//===----------------------------------------------------------------------===//
362
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000363bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000364 const llvm::APSInt& Y) {
365
Ted Kremenekbbafa5b2008-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 Kremenekb0f2b9e2008-08-16 00:49:49 +0000383bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) {
Ted Kremenekbbafa5b2008-07-22 00:46:16 +0000384 return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
385}
386
Ted Kremenekc7469542008-07-17 23:15:45 +0000387//===----------------------------------------------------------------------===//
388// "Assume" logic.
389//===----------------------------------------------------------------------===//
390
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000391const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
Ted Kremenekc7469542008-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 Kremenekabd89ac2008-08-13 04:27:00 +0000400const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
Ted Kremenekc7469542008-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 Kremenekc7469542008-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 Kremenekabd89ac2008-08-13 04:27:00 +0000439const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
Ted Kremenekc7469542008-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 Kremenekabd89ac2008-08-13 04:27:00 +0000448const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
Ted Kremenekc7469542008-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 Kremenekc7469542008-07-17 23:15:45 +0000487
Ted Kremenekc7469542008-07-17 23:15:45 +0000488
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000489const GRState* GRStateManager::AssumeSymInt(const GRState* St,
Ted Kremenekc7469542008-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 Kremenek26da9702008-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 Kremenekc7469542008-07-17 23:15:45 +0000523 }
524}
Ted Kremenek26da9702008-08-07 22:30:22 +0000525
526//===----------------------------------------------------------------------===//
527// FIXME: This should go into a plug-in constraint engine.
528//===----------------------------------------------------------------------===//
529
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000530const GRState*
531GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-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 Kremenekabd89ac2008-08-13 04:27:00 +0000553const GRState*
554GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-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 Kremenekabd89ac2008-08-13 04:27:00 +0000576const GRState*
577GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-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 Kremenekabd89ac2008-08-13 04:27:00 +0000584const GRState*
585GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-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 Kremenekabd89ac2008-08-13 04:27:00 +0000592const GRState*
593GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-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 Kremenekabd89ac2008-08-13 04:27:00 +0000608const GRState*
609GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-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