blob: f9257274a6afaa30be0c818169dc30a34831001a [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)
151 NewStore = StMgr->AddDecl(OldStore, BasicVals, SymMgr, VD, Ex,
152 GetRVal(St, Ex), Count);
153 else
154 NewStore = StMgr->AddDecl(OldStore, BasicVals, SymMgr, VD, Ex);
155
156 if (NewStore == OldStore)
157 return St;
158 GRState NewSt = *St;
159 NewSt.St = NewStore;
160 return getPersistentState(NewSt);
161}
162
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000163const GRState* GRStateManager::Unbind(const GRState* St, LVal LV) {
Ted Kremenek4323a572008-07-10 22:03:41 +0000164 Store OldStore = St->getStore();
165 Store NewStore = StMgr->Remove(OldStore, LV);
166
167 if (NewStore == OldStore)
168 return St;
169
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000170 GRState NewSt = *St;
Ted Kremenek4323a572008-07-10 22:03:41 +0000171 NewSt.St = NewStore;
172 return getPersistentState(NewSt);
173}
174
175
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000176const GRState* GRStateManager::AddNE(const GRState* St, SymbolID sym,
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000177 const llvm::APSInt& V) {
178
179 GRStateRef state(St, *this);
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000180
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000181 // First, retrieve the NE-set associated with the given symbol.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000182 ConstNotEqTy::data_type* T = state.get<ConstNotEqTy>(sym);
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000183 GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000184
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000185 // Now add V to the NE set.
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000186 S = ISetFactory.Add(S, &V);
187
188 // Create a new state with the old binding replaced.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000189 return state.set<ConstNotEqTy>(sym, S);
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000190}
191
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000192const GRState* GRStateManager::AddEQ(const GRState* St, SymbolID sym,
Ted Kremenek4323a572008-07-10 22:03:41 +0000193 const llvm::APSInt& V) {
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000194 // Create a new state with the old binding replaced.
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000195 GRStateRef state(St, *this);
196 return state.set<ConstEqTy>(sym, &V);
Ted Kremenek862d5bb2008-02-06 00:54:14 +0000197}
198
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000199const GRState* GRStateManager::getInitialState() {
Ted Kremenek5a7b3822008-02-26 23:37:01 +0000200
Ted Kremenekcaa37242008-08-19 16:51:45 +0000201 GRState StateImpl(EnvMgr.getInitialEnvironment(),
202 StMgr->getInitialStore(*this),
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000203 GDMFactory.GetEmptyMap());
Ted Kremenekcaa37242008-08-19 16:51:45 +0000204
Ted Kremenek9153f732008-02-05 07:17:49 +0000205 return getPersistentState(StateImpl);
206}
207
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000208const GRState* GRStateManager::getPersistentState(GRState& State) {
Ted Kremenek9153f732008-02-05 07:17:49 +0000209
210 llvm::FoldingSetNodeID ID;
211 State.Profile(ID);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000212 void* InsertPos;
Ted Kremenek9153f732008-02-05 07:17:49 +0000213
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000214 if (GRState* I = StateSet.FindNodeOrInsertPos(ID, InsertPos))
Ted Kremenek9153f732008-02-05 07:17:49 +0000215 return I;
216
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000217 GRState* I = (GRState*) Alloc.Allocate<GRState>();
218 new (I) GRState(State);
Ted Kremenek9153f732008-02-05 07:17:49 +0000219 StateSet.InsertNode(I, InsertPos);
220 return I;
221}
Ted Kremeneke7d22112008-02-11 19:21:59 +0000222
Ted Kremenek59894f92008-03-04 18:30:35 +0000223
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000224//===----------------------------------------------------------------------===//
225// State pretty-printing.
226//===----------------------------------------------------------------------===//
Ted Kremenek461f9772008-03-11 18:57:24 +0000227
Ted Kremeneka622d8c2008-08-19 22:24:03 +0000228void GRState::print(std::ostream& Out, StoreManager& StoreMgr,
229 Printer** Beg, Printer** End,
Ted Kremenekae6814e2008-08-13 21:24:49 +0000230 const char* nl, const char* sep) const {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000231
Ted Kremeneka622d8c2008-08-19 22:24:03 +0000232 // Print the store.
233 StoreMgr.print(getStore(), Out, nl, sep);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000234
235 // Print Subexpression bindings.
Ted Kremeneka622d8c2008-08-19 22:24:03 +0000236 bool isFirst = true;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000237
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000238 for (seb_iterator I = seb_begin(), E = seb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000239
240 if (isFirst) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000241 Out << nl << nl << "Sub-Expressions:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000242 isFirst = false;
243 }
Ted Kremenek59894f92008-03-04 18:30:35 +0000244 else { Out << nl; }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000245
246 Out << " (" << (void*) I.getKey() << ") ";
247 I.getKey()->printPretty(Out);
248 Out << " : ";
249 I.getData().print(Out);
250 }
251
252 // Print block-expression bindings.
Ted Kremeneke7d22112008-02-11 19:21:59 +0000253 isFirst = true;
254
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000255 for (beb_iterator I = beb_begin(), E = beb_end(); I != E; ++I) {
Ted Kremeneke7d22112008-02-11 19:21:59 +0000256
257 if (isFirst) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000258 Out << nl << nl << "Block-level Expressions:" << nl;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000259 isFirst = false;
260 }
Ted Kremenek59894f92008-03-04 18:30:35 +0000261 else { Out << nl; }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000262
263 Out << " (" << (void*) I.getKey() << ") ";
264 I.getKey()->printPretty(Out);
265 Out << " : ";
266 I.getData().print(Out);
267 }
268
269 // Print equality constraints.
Ted Kremenekae6814e2008-08-13 21:24:49 +0000270 // FIXME: Make just another printer do this.
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000271 ConstEqTy CE = get<ConstEqTy>();
272
273 if (!CE.isEmpty()) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000274 Out << nl << sep << "'==' constraints:";
Ted Kremenekffdbefd2008-08-17 03:10:22 +0000275
276 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I)
Ted Kremenek59894f92008-03-04 18:30:35 +0000277 Out << nl << " $" << I.getKey()
Chris Lattner9aa77f12008-08-17 07:19:51 +0000278 << " : " << *I.getData();
Ted Kremeneke7d22112008-02-11 19:21:59 +0000279 }
Ted Kremeneke7d22112008-02-11 19:21:59 +0000280
281 // Print != constraints.
Ted Kremenekae6814e2008-08-13 21:24:49 +0000282 // FIXME: Make just another printer do this.
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000283
284 ConstNotEqTy CNE = get<ConstNotEqTy>();
285
286 if (!CNE.isEmpty()) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000287 Out << nl << sep << "'!=' constraints:";
Ted Kremeneke7d22112008-02-11 19:21:59 +0000288
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000289 for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
Ted Kremenek59894f92008-03-04 18:30:35 +0000290 Out << nl << " $" << I.getKey() << " : ";
Ted Kremeneke7d22112008-02-11 19:21:59 +0000291 isFirst = true;
292
Ted Kremenekaa1c4e52008-02-21 18:02:17 +0000293 IntSetTy::iterator J = I.getData().begin(), EJ = I.getData().end();
Ted Kremeneke7d22112008-02-11 19:21:59 +0000294
295 for ( ; J != EJ; ++J) {
296 if (isFirst) isFirst = false;
297 else Out << ", ";
298
Chris Lattner9aa77f12008-08-17 07:19:51 +0000299 Out << *J;
Ted Kremeneke7d22112008-02-11 19:21:59 +0000300 }
301 }
302 }
Ted Kremenek461f9772008-03-11 18:57:24 +0000303
Ted Kremenekae6814e2008-08-13 21:24:49 +0000304 // Print checker-specific data.
305 for ( ; Beg != End ; ++Beg) (*Beg)->Print(Out, this, nl, sep);
Ted Kremeneke7d22112008-02-11 19:21:59 +0000306}
Ted Kremenek729a9a22008-07-17 23:15:45 +0000307
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000308void GRStateRef::printDOT(std::ostream& Out) const {
309 print(Out, "\\l", "\\|");
310}
311
312void GRStateRef::printStdErr() const {
313 print(*llvm::cerr);
314}
315
316void GRStateRef::print(std::ostream& Out, const char* nl, const char* sep)const{
317 GRState::Printer **beg = Mgr->Printers.empty() ? 0 : &Mgr->Printers[0];
318 GRState::Printer **end = !beg ? 0 : beg + Mgr->Printers.size();
Ted Kremeneka622d8c2008-08-19 22:24:03 +0000319 St->print(Out, *Mgr->StMgr, beg, end, nl, sep);
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000320}
321
Ted Kremenek72cd17f2008-08-14 21:16:54 +0000322//===----------------------------------------------------------------------===//
323// Generic Data Map.
324//===----------------------------------------------------------------------===//
325
326void* const* GRState::FindGDM(void* K) const {
327 return GDM.lookup(K);
328}
329
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000330void*
331GRStateManager::FindGDMContext(void* K,
332 void* (*CreateContext)(llvm::BumpPtrAllocator&),
333 void (*DeleteContext)(void*)) {
334
335 std::pair<void*, void (*)(void*)>& p = GDMContexts[K];
336 if (!p.first) {
337 p.first = CreateContext(Alloc);
338 p.second = DeleteContext;
339 }
340
341 return p.first;
342}
343
Ted Kremenek72cd17f2008-08-14 21:16:54 +0000344const GRState* GRStateManager::addGDM(const GRState* St, void* Key, void* Data){
345 GRState::GenericDataMap M1 = St->getGDM();
346 GRState::GenericDataMap M2 = GDMFactory.Add(M1, Key, Data);
347
348 if (M1 == M2)
349 return St;
350
351 GRState NewSt = *St;
352 NewSt.GDM = M2;
353 return getPersistentState(NewSt);
354}
Ted Kremenek584def72008-07-22 00:46:16 +0000355
356//===----------------------------------------------------------------------===//
357// Queries.
358//===----------------------------------------------------------------------===//
359
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000360bool GRStateManager::isEqual(const GRState* state, Expr* Ex,
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000361 const llvm::APSInt& Y) {
362
Ted Kremenek584def72008-07-22 00:46:16 +0000363 RVal V = GetRVal(state, Ex);
364
365 if (lval::ConcreteInt* X = dyn_cast<lval::ConcreteInt>(&V))
366 return X->getValue() == Y;
367
368 if (nonlval::ConcreteInt* X = dyn_cast<nonlval::ConcreteInt>(&V))
369 return X->getValue() == Y;
370
371 if (nonlval::SymbolVal* X = dyn_cast<nonlval::SymbolVal>(&V))
372 return state->isEqual(X->getSymbol(), Y);
373
374 if (lval::SymbolVal* X = dyn_cast<lval::SymbolVal>(&V))
375 return state->isEqual(X->getSymbol(), Y);
376
377 return false;
378}
379
Ted Kremenek1c72ef02008-08-16 00:49:49 +0000380bool GRStateManager::isEqual(const GRState* state, Expr* Ex, uint64_t x) {
Ted Kremenek584def72008-07-22 00:46:16 +0000381 return isEqual(state, Ex, BasicVals.getValue(x, Ex->getType()));
382}
383
Ted Kremenek729a9a22008-07-17 23:15:45 +0000384//===----------------------------------------------------------------------===//
385// "Assume" logic.
386//===----------------------------------------------------------------------===//
387
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000388const GRState* GRStateManager::Assume(const GRState* St, LVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000389 bool Assumption, bool& isFeasible) {
390
391 St = AssumeAux(St, Cond, Assumption, isFeasible);
392
393 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
394 : St;
395}
396
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000397const GRState* GRStateManager::AssumeAux(const GRState* St, LVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000398 bool Assumption, bool& isFeasible) {
399
400 switch (Cond.getSubKind()) {
401 default:
402 assert (false && "'Assume' not implemented for this LVal.");
403 return St;
404
405 case lval::SymbolValKind:
406 if (Assumption)
407 return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
408 BasicVals.getZeroWithPtrWidth(), isFeasible);
409 else
410 return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
411 BasicVals.getZeroWithPtrWidth(), isFeasible);
412
Ted Kremenek729a9a22008-07-17 23:15:45 +0000413 case lval::DeclValKind:
414 case lval::FuncValKind:
415 case lval::GotoLabelKind:
416 case lval::StringLiteralValKind:
417 isFeasible = Assumption;
418 return St;
419
420 case lval::FieldOffsetKind:
421 return AssumeAux(St, cast<lval::FieldOffset>(Cond).getBase(),
422 Assumption, isFeasible);
423
424 case lval::ArrayOffsetKind:
425 return AssumeAux(St, cast<lval::ArrayOffset>(Cond).getBase(),
426 Assumption, isFeasible);
427
428 case lval::ConcreteIntKind: {
429 bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
430 isFeasible = b ? Assumption : !Assumption;
431 return St;
432 }
433 }
434}
435
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000436const GRState* GRStateManager::Assume(const GRState* St, NonLVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000437 bool Assumption, bool& isFeasible) {
438
439 St = AssumeAux(St, Cond, Assumption, isFeasible);
440
441 return isFeasible ? TF->EvalAssume(*this, St, Cond, Assumption, isFeasible)
442 : St;
443}
444
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000445const GRState* GRStateManager::AssumeAux(const GRState* St, NonLVal Cond,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000446 bool Assumption, bool& isFeasible) {
447 switch (Cond.getSubKind()) {
448 default:
449 assert (false && "'Assume' not implemented for this NonLVal.");
450 return St;
451
452
453 case nonlval::SymbolValKind: {
454 nonlval::SymbolVal& SV = cast<nonlval::SymbolVal>(Cond);
455 SymbolID sym = SV.getSymbol();
456
457 if (Assumption)
458 return AssumeSymNE(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
459 isFeasible);
460 else
461 return AssumeSymEQ(St, sym, BasicVals.getValue(0, SymMgr.getType(sym)),
462 isFeasible);
463 }
464
465 case nonlval::SymIntConstraintValKind:
466 return
467 AssumeSymInt(St, Assumption,
468 cast<nonlval::SymIntConstraintVal>(Cond).getConstraint(),
469 isFeasible);
470
471 case nonlval::ConcreteIntKind: {
472 bool b = cast<nonlval::ConcreteInt>(Cond).getValue() != 0;
473 isFeasible = b ? Assumption : !Assumption;
474 return St;
475 }
476
477 case nonlval::LValAsIntegerKind: {
478 return AssumeAux(St, cast<nonlval::LValAsInteger>(Cond).getLVal(),
479 Assumption, isFeasible);
480 }
481 }
482}
483
Ted Kremenek729a9a22008-07-17 23:15:45 +0000484
Ted Kremenek729a9a22008-07-17 23:15:45 +0000485
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000486const GRState* GRStateManager::AssumeSymInt(const GRState* St,
Ted Kremenek729a9a22008-07-17 23:15:45 +0000487 bool Assumption,
488 const SymIntConstraint& C,
489 bool& isFeasible) {
490
491 switch (C.getOpcode()) {
492 default:
493 // No logic yet for other operators.
494 isFeasible = true;
495 return St;
496
497 case BinaryOperator::EQ:
498 if (Assumption)
499 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
500 else
501 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
502
503 case BinaryOperator::NE:
504 if (Assumption)
505 return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible);
506 else
507 return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenek2619be02008-08-07 22:30:22 +0000508
509 case BinaryOperator::GE:
510 if (Assumption)
511 return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible);
512 else
513 return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible);
514
515 case BinaryOperator::LE:
516 if (Assumption)
517 return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible);
518 else
519 return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible);
Ted Kremenek729a9a22008-07-17 23:15:45 +0000520 }
521}
Ted Kremenek2619be02008-08-07 22:30:22 +0000522
523//===----------------------------------------------------------------------===//
524// FIXME: This should go into a plug-in constraint engine.
525//===----------------------------------------------------------------------===//
526
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000527const GRState*
528GRStateManager::AssumeSymNE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000529 const llvm::APSInt& V, bool& isFeasible) {
530
531 // First, determine if sym == X, where X != V.
532 if (const llvm::APSInt* X = St->getSymVal(sym)) {
533 isFeasible = *X != V;
534 return St;
535 }
536
537 // Second, determine if sym != V.
538 if (St->isNotEqual(sym, V)) {
539 isFeasible = true;
540 return St;
541 }
542
543 // If we reach here, sym is not a constant and we don't know if it is != V.
544 // Make that assumption.
545
546 isFeasible = true;
547 return AddNE(St, sym, V);
548}
549
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000550const GRState*
551GRStateManager::AssumeSymEQ(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000552 const llvm::APSInt& V, bool& isFeasible) {
553
554 // First, determine if sym == X, where X != V.
555 if (const llvm::APSInt* X = St->getSymVal(sym)) {
556 isFeasible = *X == V;
557 return St;
558 }
559
560 // Second, determine if sym != V.
561 if (St->isNotEqual(sym, V)) {
562 isFeasible = false;
563 return St;
564 }
565
566 // If we reach here, sym is not a constant and we don't know if it is == V.
567 // Make that assumption.
568
569 isFeasible = true;
570 return AddEQ(St, sym, V);
571}
572
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000573const GRState*
574GRStateManager::AssumeSymLT(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000575 const llvm::APSInt& V, bool& isFeasible) {
576
577 // FIXME: For now have assuming x < y be the same as assuming sym != V;
578 return AssumeSymNE(St, sym, V, isFeasible);
579}
580
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000581const GRState*
582GRStateManager::AssumeSymGT(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000583 const llvm::APSInt& V, bool& isFeasible) {
584
585 // FIXME: For now have assuming x > y be the same as assuming sym != V;
586 return AssumeSymNE(St, sym, V, isFeasible);
587}
588
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000589const GRState*
590GRStateManager::AssumeSymGE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000591 const llvm::APSInt& V, bool& isFeasible) {
592
593 // FIXME: Primitive logic for now. Only reject a path if the value of
594 // sym is a constant X and !(X >= V).
595
596 if (const llvm::APSInt* X = St->getSymVal(sym)) {
597 isFeasible = *X >= V;
598 return St;
599 }
600
601 isFeasible = true;
602 return St;
603}
604
Ted Kremenek4adc81e2008-08-13 04:27:00 +0000605const GRState*
606GRStateManager::AssumeSymLE(const GRState* St, SymbolID sym,
Ted Kremenek2619be02008-08-07 22:30:22 +0000607 const llvm::APSInt& V, bool& isFeasible) {
608
609 // FIXME: Primitive logic for now. Only reject a path if the value of
610 // sym is a constant X and !(X <= V).
611
612 if (const llvm::APSInt* X = St->getSymVal(sym)) {
613 isFeasible = *X <= V;
614 return St;
615 }
616
617 isFeasible = true;
618 return St;
619}
620