blob: 1cee484357b259683df98b8942ea93ad88e818c7 [file] [log] [blame]
Ted Kremenekabd89ac2008-08-13 04:27:00 +00001//= GRState*cpp - Path-Sens. "State" for tracking valuues -----*- C++ -*--=//
Ted Kremenek2d8dce32008-02-05 07:17:49 +00002//
3// The LLVM Compiler Infrastructure
4//
5// This file is distributed under the University of Illinois Open Source
6// License. See LICENSE.TXT for details.
7//
8//===----------------------------------------------------------------------===//
9//
Ted Kremenekabd89ac2008-08-13 04:27:00 +000010// This file defines SymbolID, ExprBindKey, and GRState*
Ted Kremenek2d8dce32008-02-05 07:17:49 +000011//
12//===----------------------------------------------------------------------===//
13
Ted Kremenek67ff8b92008-08-17 02:59:30 +000014#include "clang/Analysis/PathSensitive/GRStateTrait.h"
Ted Kremenekabd89ac2008-08-13 04:27:00 +000015#include "clang/Analysis/PathSensitive/GRState.h"
Ted Kremenek0e39dcf2008-02-14 23:25:54 +000016#include "llvm/ADT/SmallSet.h"
Ted Kremenekc7469542008-07-17 23:15:45 +000017#include "clang/Analysis/PathSensitive/GRTransferFuncs.h"
Ted Kremenek0eb0afa2008-02-04 21:59:22 +000018
19using namespace clang;
20
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000021GRStateManager::~GRStateManager() {
22 for (std::vector<GRState::Printer*>::iterator I=Printers.begin(),
23 E=Printers.end(); I!=E; ++I)
24 delete *I;
25
26 for (GDMContextsTy::iterator I=GDMContexts.begin(), E=GDMContexts.end();
27 I!=E; ++I)
28 I->second.second(I->second.first);
29}
30
31//===----------------------------------------------------------------------===//
32// Basic symbolic analysis. This will eventually be refactored into a
33// separate component.
34//===----------------------------------------------------------------------===//
35
36typedef llvm::ImmutableMap<SymbolID,GRState::IntSetTy> ConstNotEqTy;
Ted Kremenek80fcbb92008-08-17 03:10:22 +000037typedef llvm::ImmutableMap<SymbolID,const llvm::APSInt*> ConstEqTy;
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000038
Ted Kremenek80fcbb92008-08-17 03:10:22 +000039static int ConstEqTyIndex = 0;
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000040static int ConstNotEqTyIndex = 0;
41
42namespace clang {
Ted Kremenek67ff8b92008-08-17 02:59:30 +000043 template<>
44 struct GRStateTrait<ConstNotEqTy> : public GRStatePartialTrait<ConstNotEqTy> {
45 static inline void* GDMIndex() { return &ConstNotEqTyIndex; }
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000046 };
Ted Kremenek80fcbb92008-08-17 03:10:22 +000047
48 template<>
49 struct GRStateTrait<ConstEqTy> : public GRStatePartialTrait<ConstEqTy> {
50 static inline void* GDMIndex() { return &ConstEqTyIndex; }
51 };
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000052}
53
Ted Kremenekabd89ac2008-08-13 04:27:00 +000054bool GRState::isNotEqual(SymbolID sym, const llvm::APSInt& V) const {
Ted Kremenek07baa252008-02-21 18:02:17 +000055
56 // Retrieve the NE-set associated with the given symbol.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000057 const ConstNotEqTy::data_type* T = get<ConstNotEqTy>(sym);
Ted Kremenek07baa252008-02-21 18:02:17 +000058
59 // See if V is present in the NE-set.
Ted Kremenek6064a362008-07-07 16:21:19 +000060 return T ? T->contains(&V) : false;
Ted Kremenek13f31562008-02-06 00:54:14 +000061}
62
Ted Kremenekabd89ac2008-08-13 04:27:00 +000063bool GRState::isEqual(SymbolID sym, const llvm::APSInt& V) const {
Ted Kremenekbbafa5b2008-07-22 00:46:16 +000064 // Retrieve the EQ-set associated with the given symbol.
Ted Kremenek80fcbb92008-08-17 03:10:22 +000065 const ConstEqTy::data_type* T = get<ConstEqTy>(sym);
Ted Kremenekbbafa5b2008-07-22 00:46:16 +000066 // See if V is present in the EQ-set.
67 return T ? **T == V : false;
68}
69
Ted Kremenekabd89ac2008-08-13 04:27:00 +000070const llvm::APSInt* GRState::getSymVal(SymbolID sym) const {
Ted Kremenek80fcbb92008-08-17 03:10:22 +000071 const ConstEqTy::data_type* T = get<ConstEqTy>(sym);
Ted Kremenek6064a362008-07-07 16:21:19 +000072 return T ? *T : NULL;
Ted Kremenek13f31562008-02-06 00:54:14 +000073}
74
Ted Kremenekabd89ac2008-08-13 04:27:00 +000075const GRState*
76GRStateManager::RemoveDeadBindings(const GRState* St, Stmt* Loc,
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +000077 const LiveVariables& Liveness,
78 DeadSymbolsTy& DSymbols) {
Ted Kremenekb8958d62008-02-08 19:17:19 +000079
80 // This code essentially performs a "mark-and-sweep" of the VariableBindings.
81 // The roots are any Block-level exprs and Decls that our liveness algorithm
82 // tells us are live. We then see what Decls they may reference, and keep
83 // those around. This code more than likely can be made faster, and the
84 // frequency of which this method is called should be experimented with
Ted Kremenekee930122008-07-17 18:38:48 +000085 // for optimum performance.
86 DRoots.clear();
87 StoreManager::LiveSymbolsTy LSymbols;
Ted Kremenek17c5f112008-02-11 19:21:59 +000088
Ted Kremenekabd89ac2008-08-13 04:27:00 +000089 GRState NewSt = *St;
Ted Kremenekee930122008-07-17 18:38:48 +000090
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
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000145const GRState* GRStateManager::Unbind(const GRState* St, LVal LV) {
Ted Kremenekf22f8682008-07-10 22:03:41 +0000146 Store OldStore = St->getStore();
147 Store NewStore = StMgr->Remove(OldStore, LV);
148
149 if (NewStore == OldStore)
150 return St;
151
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000152 GRState NewSt = *St;
Ted Kremenekf22f8682008-07-10 22:03:41 +0000153 NewSt.St = NewStore;
154 return getPersistentState(NewSt);
155}
156
157
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000158const GRState* GRStateManager::AddNE(const GRState* St, SymbolID sym,
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000159 const llvm::APSInt& V) {
160
161 GRStateRef state(St, *this);
Ted Kremenek07baa252008-02-21 18:02:17 +0000162
Ted Kremenek13f31562008-02-06 00:54:14 +0000163 // First, retrieve the NE-set associated with the given symbol.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000164 ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym);
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000165 GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
Ted Kremenek13f31562008-02-06 00:54:14 +0000166
Ted Kremenek07baa252008-02-21 18:02:17 +0000167 // Now add V to the NE set.
Ted Kremenek13f31562008-02-06 00:54:14 +0000168 S = ISetFactory.Add(S, &V);
169
170 // Create a new state with the old binding replaced.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000171 return state.set<ConstNotEqTy>(sym, S);
Ted Kremenek13f31562008-02-06 00:54:14 +0000172}
173
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000174const GRState* GRStateManager::AddEQ(const GRState* St, SymbolID sym,
Ted Kremenekf22f8682008-07-10 22:03:41 +0000175 const llvm::APSInt& V) {
Ted Kremenek13f31562008-02-06 00:54:14 +0000176 // Create a new state with the old binding replaced.
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000177 GRStateRef state(St, *this);
178 return state.set<ConstEqTy>(sym, &V);
Ted Kremenek13f31562008-02-06 00:54:14 +0000179}
180
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000181const GRState* GRStateManager::getInitialState() {
Ted Kremenekad5d5c52008-02-26 23:37:01 +0000182
Ted Kremeneke2fb8c72008-08-19 16:51:45 +0000183 GRState StateImpl(EnvMgr.getInitialEnvironment(),
184 StMgr->getInitialStore(*this),
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000185 GDMFactory.GetEmptyMap());
Ted Kremeneke2fb8c72008-08-19 16:51:45 +0000186
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000187 return getPersistentState(StateImpl);
188}
189
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000190const GRState* GRStateManager::getPersistentState(GRState& State) {
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000191
192 llvm::FoldingSetNodeID ID;
193 State.Profile(ID);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000194 void* InsertPos;
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000195
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000196 if (GRState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos))
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000197 return I;
198
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000199 GRState* I = (GRState*) Alloc.Allocate<GRState>();
200 new (I) GRState(State);
Ted Kremenek2d8dce32008-02-05 07:17:49 +0000201 StateSet.InsertNode(I, InsertPos);
202 return I;
203}
Ted Kremenek17c5f112008-02-11 19:21:59 +0000204
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000205
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000206//===----------------------------------------------------------------------===//
207// State pretty-printing.
208//===----------------------------------------------------------------------===//
Ted Kremenekd3656492008-03-11 18:57:24 +0000209
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000210void GRState::print(std::ostream& Out, StoreManager& StoreMgr,
211 Printer** Beg, Printer** End,
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000212 const char* nl, const char* sep) const {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000213
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000214 // Print the store.
215 StoreMgr.print(getStore(), Out, nl, sep);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000216
217 // Print Subexpression bindings.
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000218 bool isFirst = true;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000219
Ted Kremenek07baa252008-02-21 18:02:17 +0000220 for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000221
222 if (isFirst) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000223 Out << nl << nl << "Sub-Expressions:" << nl;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000224 isFirst = false;
225 }
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000226 else { Out << nl; }
Ted Kremenek17c5f112008-02-11 19:21:59 +0000227
228 Out << " (" << (void*) I.getKey() << ") ";
229 I.getKey()->printPretty(Out);
230 Out << " : ";
231 I.getData().print(Out);
232 }
233
234 // Print block-expression bindings.
Ted Kremenek17c5f112008-02-11 19:21:59 +0000235 isFirst = true;
236
Ted Kremenek07baa252008-02-21 18:02:17 +0000237 for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) {
Ted Kremenek17c5f112008-02-11 19:21:59 +0000238
239 if (isFirst) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000240 Out << nl << nl << "Block-level Expressions:" << nl;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000241 isFirst = false;
242 }
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000243 else { Out << nl; }
Ted Kremenek17c5f112008-02-11 19:21:59 +0000244
245 Out << " (" << (void*) I.getKey() << ") ";
246 I.getKey()->printPretty(Out);
247 Out << " : ";
248 I.getData().print(Out);
249 }
250
251 // Print equality constraints.
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000252 // FIXME: Make just another printer do this.
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000253 ConstEqTy CE = get<ConstEqTy>();
254
255 if (!CE.isEmpty()) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000256 Out << nl << sep << "'==' constraints:";
Ted Kremenek80fcbb92008-08-17 03:10:22 +0000257
258 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I)
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000259 Out << nl << " $" << I.getKey()
Chris Lattneread053a2008-08-17 07:19:51 +0000260 << " : " << *I.getData();
Ted Kremenek17c5f112008-02-11 19:21:59 +0000261 }
Ted Kremenek17c5f112008-02-11 19:21:59 +0000262
263 // Print != constraints.
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000264 // FIXME: Make just another printer do this.
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000265
266 ConstNotEqTy CNE = get<ConstNotEqTy>();
267
268 if (!CNE.isEmpty()) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000269 Out << nl << sep << "'!=' constraints:";
Ted Kremenek17c5f112008-02-11 19:21:59 +0000270
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000271 for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
Ted Kremeneke1cfa992008-03-04 18:30:35 +0000272 Out << nl << " $" << I.getKey() << " : ";
Ted Kremenek17c5f112008-02-11 19:21:59 +0000273 isFirst = true;
274
Ted Kremenek07baa252008-02-21 18:02:17 +0000275 IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end();
Ted Kremenek17c5f112008-02-11 19:21:59 +0000276
277 for ( ; J != EJ; ++J) {
278 if (isFirst) isFirst = false;
279 else Out << ", ";
280
Chris Lattneread053a2008-08-17 07:19:51 +0000281 Out << *J;
Ted Kremenek17c5f112008-02-11 19:21:59 +0000282 }
283 }
284 }
Ted Kremenekd3656492008-03-11 18:57:24 +0000285
Ted Kremenekbccfbcc2008-08-13 21:24:49 +0000286 // Print checker-specific data.
287 for ( ; Beg != End ; ++Beg) (*Beg)->Print(Out, this, nl, sep);
Ted Kremenek17c5f112008-02-11 19:21:59 +0000288}
Ted Kremenekc7469542008-07-17 23:15:45 +0000289
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000290void GRStateRef::printDOT(std::ostream& Out) const {
291 print(Out, "\\l", "\\|");
292}
293
294void GRStateRef::printStdErr() const {
295 print(*llvm::cerr);
296}
297
298void GRStateRef::print(std::ostream& Out, const char* nl, const char* sep)const{
299 GRState::Printer **beg = Mgr->Printers.empty() ? 0 : &Mgr->Printers[0];
300 GRState::Printer **end = !beg ? 0 : beg + Mgr->Printers.size();
Ted Kremenekbdff9a92008-08-19 22:24:03 +0000301 St->print(Out, *Mgr->StMgr, beg, end, nl, sep);
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000302}
303
Ted Kremenek4ae925c2008-08-14 21:16:54 +0000304//===----------------------------------------------------------------------===//
305// Generic Data Map.
306//===----------------------------------------------------------------------===//
307
308void* const* GRState::FindGDM(void* K) const {
309 return GDM.lookup(K);
310}
311
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000312void*
313GRStateManager::FindGDMContext(void* K,
314 void* (*CreateContext)(llvm::BumpPtrAllocator&),
315 void (*DeleteContext)(void*)) {
316
317 std::pair<void*, void (*)(void*)>& p = GDMContexts[K];
318 if (!p.first) {
319 p.first = CreateContext(Alloc);
320 p.second = DeleteContext;
321 }
322
323 return p.first;
324}
325
Ted Kremenek4ae925c2008-08-14 21:16:54 +0000326const GRState* GRStateManager::addGDM(const GRState* St, void* Key, void* Data){
327 GRState::GenericDataMap M1 = St->getGDM();
328 GRState::GenericDataMap M2 = GDMFactory.Add(M1, Key, Data);
329
330 if (M1 == M2)
331 return St;
332
333 GRState NewSt = *St;
334 NewSt.GDM = M2;
335 return getPersistentState(NewSt);
336}
Ted Kremenekbbafa5b2008-07-22 00:46:16 +0000337
338//===----------------------------------------------------------------------===//
339// Queries.
340//===----------------------------------------------------------------------===//
341
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000342bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000343 const llvm::APSInt& Y) {
344
Ted Kremenekbbafa5b2008-07-22 00:46:16 +0000345 RVal V = GetRVal(state, Ex);
346
347 if (lval::ConcreteInt* X = dyn_cast<lval::ConcreteInt>(&V))
348 return X->getValue() == Y;
349
350 if (nonlval::ConcreteInt* X = dyn_cast<nonlval::ConcreteInt>(&V))
351 return X->getValue() == Y;
352
353 if (nonlval::SymbolVal* X = dyn_cast<nonlval::SymbolVal>(&V))
354 return state->isEqual(X->getSymbol(), Y);
355
356 if (lval::SymbolVal* X = dyn_cast<lval::SymbolVal>(&V))
357 return state->isEqual(X->getSymbol(), Y);
358
359 return false;
360}
361
Ted Kremenekb0f2b9e2008-08-16 00:49:49 +0000362bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) {
Ted Kremenekbbafa5b2008-07-22 00:46:16 +0000363 return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
364}
365
Ted Kremenekc7469542008-07-17 23:15:45 +0000366//===----------------------------------------------------------------------===//
367// "Assume" logic.
368//===----------------------------------------------------------------------===//
369
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000370const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000371 bool Assumption, bool& isFeasible) {
372
373 St = AssumeAux(St, Cond, Assumption, isFeasible);
374
375 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
376 : St;
377}
378
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000379const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000380 bool Assumption, bool& isFeasible) {
381
382 switch (Cond.getSubKind()) {
383 default:
384 assert (false && "'Assume' not implemented for this LVal.");
385 return St;
386
387 case lval::SymbolValKind:
388 if (Assumption)
389 return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
390 BasicVals.getZeroWithPtrWidth(), isFeasible);
391 else
392 return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
393 BasicVals.getZeroWithPtrWidth(), isFeasible);
394
Ted Kremenekc7469542008-07-17 23:15:45 +0000395 case lval::DeclValKind:
396 case lval::FuncValKind:
397 case lval::GotoLabelKind:
398 case lval::StringLiteralValKind:
399 isFeasible = Assumption;
400 return St;
401
402 case lval::FieldOffsetKind:
403 return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
404 Assumption, isFeasible);
405
406 case lval::ArrayOffsetKind:
407 return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
408 Assumption, isFeasible);
409
410 case lval::ConcreteIntKind: {
411 bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
412 isFeasible = b ? Assumption : !Assumption;
413 return St;
414 }
415 }
416}
417
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000418const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000419 bool Assumption, bool& isFeasible) {
420
421 St = AssumeAux(St, Cond, Assumption, isFeasible);
422
423 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
424 : St;
425}
426
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000427const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
Ted Kremenekc7469542008-07-17 23:15:45 +0000428 bool Assumption, bool& isFeasible) {
429 switch (Cond.getSubKind()) {
430 default:
431 assert (false && "'Assume' not implemented for this NonLVal.");
432 return St;
433
434
435 case nonlval::SymbolValKind: {
436 nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
437 SymbolID sym = SV.getSymbol();
438
439 if (Assumption)
440 return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
441 isFeasible);
442 else
443 return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
444 isFeasible);
445 }
446
447 case nonlval::SymIntConstraintValKind:
448 return
449 AssumeSymInt(St, Assumption,
450 cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
451 isFeasible);
452
453 case nonlval::ConcreteIntKind: {
454 bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
455 isFeasible = b ? Assumption : !Assumption;
456 return St;
457 }
458
459 case nonlval::LValAsIntegerKind: {
460 return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
461 Assumption, isFeasible);
462 }
463 }
464}
465
Ted Kremenekc7469542008-07-17 23:15:45 +0000466
Ted Kremenekc7469542008-07-17 23:15:45 +0000467
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000468const GRState* GRStateManager::AssumeSymInt(const GRState* St,
Ted Kremenekc7469542008-07-17 23:15:45 +0000469 bool Assumption,
470 const SymIntConstraint& C,
471 bool& isFeasible) {
472
473 switch (C.getOpcode()) {
474 default:
475 // No logic yet for other operators.
476 isFeasible = true;
477 return St;
478
479 case BinaryOperator::EQ:
480 if (Assumption)
481 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
482 else
483 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
484
485 case BinaryOperator::NE:
486 if (Assumption)
487 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
488 else
489 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenek26da9702008-08-07 22:30:22 +0000490
491 case BinaryOperator::GE:
492 if (Assumption)
493 return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
494 else
495 return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
496
497 case BinaryOperator::LE:
498 if (Assumption)
499 return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
500 else
501 return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenekc7469542008-07-17 23:15:45 +0000502 }
503}
Ted Kremenek26da9702008-08-07 22:30:22 +0000504
505//===----------------------------------------------------------------------===//
506// FIXME: This should go into a plug-in constraint engine.
507//===----------------------------------------------------------------------===//
508
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000509const GRState*
510GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000511 const llvm::APSInt& V, bool& isFeasible) {
512
513 // First, determine if sym == X, where X != V.
514 if (const llvm::APSInt* X = St->getSymVal(sym)) {
515 isFeasible = *X != V;
516 return St;
517 }
518
519 // Second, determine if sym != V.
520 if (St->isNotEqual(sym, V)) {
521 isFeasible = true;
522 return St;
523 }
524
525 // If we reach here, sym is not a constant and we don't know if it is != V.
526 // Make that assumption.
527
528 isFeasible = true;
529 return AddNE(St, sym, V);
530}
531
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000532const GRState*
533GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000534 const llvm::APSInt& V, bool& isFeasible) {
535
536 // First, determine if sym == X, where X != V.
537 if (const llvm::APSInt* X = St->getSymVal(sym)) {
538 isFeasible = *X == V;
539 return St;
540 }
541
542 // Second, determine if sym != V.
543 if (St->isNotEqual(sym, V)) {
544 isFeasible = false;
545 return St;
546 }
547
548 // If we reach here, sym is not a constant and we don't know if it is == V.
549 // Make that assumption.
550
551 isFeasible = true;
552 return AddEQ(St, sym, V);
553}
554
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000555const GRState*
556GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000557 const llvm::APSInt& V, bool& isFeasible) {
558
559 // FIXME: For now have assuming x < y be the same as assuming sym != V;
560 return AssumeSymNE(St, sym, V, isFeasible);
561}
562
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000563const GRState*
564GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000565 const llvm::APSInt& V, bool& isFeasible) {
566
567 // FIXME: For now have assuming x > y be the same as assuming sym != V;
568 return AssumeSymNE(St, sym, V, isFeasible);
569}
570
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000571const GRState*
572GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000573 const llvm::APSInt& V, bool& isFeasible) {
574
575 // FIXME: Primitive logic for now. Only reject a path if the value of
576 // sym is a constant X and !(X >= V).
577
578 if (const llvm::APSInt* X = St->getSymVal(sym)) {
579 isFeasible = *X >= V;
580 return St;
581 }
582
583 isFeasible = true;
584 return St;
585}
586
Ted Kremenekabd89ac2008-08-13 04:27:00 +0000587const GRState*
588GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
Ted Kremenek26da9702008-08-07 22:30:22 +0000589 const llvm::APSInt& V, bool& isFeasible) {
590
591 // FIXME: Primitive logic for now. Only reject a path if the value of
592 // sym is a constant X and !(X <= V).
593
594 if (const llvm::APSInt* X = St->getSymVal(sym)) {
595 isFeasible = *X <= V;
596 return St;
597 }
598
599 isFeasible = true;
600 return St;
601}
602