1 //== BasicConstraintManager.cpp - Manage basic constraints.------*- C++ -*--==//
3 // The LLVM Compiler Infrastructure
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
8 //===----------------------------------------------------------------------===//
10 // This file defines BasicConstraintManager, a class that tracks simple
11 // equality and inequality constraints on symbolic values of GRState.
13 //===----------------------------------------------------------------------===//
15 #include "SimpleConstraintManager.h"
16 #include "clang/GR/PathSensitive/GRState.h"
17 #include "clang/GR/PathSensitive/GRStateTrait.h"
18 #include "clang/GR/PathSensitive/GRTransferFuncs.h"
19 #include "llvm/Support/raw_ostream.h"
21 using namespace clang
;
25 namespace { class ConstNotEq
{}; }
26 namespace { class ConstEq
{}; }
28 typedef llvm::ImmutableMap
<SymbolRef
,GRState::IntSetTy
> ConstNotEqTy
;
29 typedef llvm::ImmutableMap
<SymbolRef
,const llvm::APSInt
*> ConstEqTy
;
31 static int ConstEqIndex
= 0;
32 static int ConstNotEqIndex
= 0;
37 struct GRStateTrait
<ConstNotEq
> : public GRStatePartialTrait
<ConstNotEqTy
> {
38 static inline void* GDMIndex() { return &ConstNotEqIndex
; }
42 struct GRStateTrait
<ConstEq
> : public GRStatePartialTrait
<ConstEqTy
> {
43 static inline void* GDMIndex() { return &ConstEqIndex
; }
49 // BasicConstraintManager only tracks equality and inequality constraints of
50 // constants and integer variables.
51 class BasicConstraintManager
52 : public SimpleConstraintManager
{
53 GRState::IntSetTy::Factory ISetFactory
;
55 BasicConstraintManager(GRStateManager
&statemgr
, GRSubEngine
&subengine
)
56 : SimpleConstraintManager(subengine
),
57 ISetFactory(statemgr
.getAllocator()) {}
59 const GRState
*assumeSymNE(const GRState
* state
, SymbolRef sym
,
60 const llvm::APSInt
& V
,
61 const llvm::APSInt
& Adjustment
);
63 const GRState
*assumeSymEQ(const GRState
* state
, SymbolRef sym
,
64 const llvm::APSInt
& V
,
65 const llvm::APSInt
& Adjustment
);
67 const GRState
*assumeSymLT(const GRState
* state
, SymbolRef sym
,
68 const llvm::APSInt
& V
,
69 const llvm::APSInt
& Adjustment
);
71 const GRState
*assumeSymGT(const GRState
* state
, SymbolRef sym
,
72 const llvm::APSInt
& V
,
73 const llvm::APSInt
& Adjustment
);
75 const GRState
*assumeSymGE(const GRState
* state
, SymbolRef sym
,
76 const llvm::APSInt
& V
,
77 const llvm::APSInt
& Adjustment
);
79 const GRState
*assumeSymLE(const GRState
* state
, SymbolRef sym
,
80 const llvm::APSInt
& V
,
81 const llvm::APSInt
& Adjustment
);
83 const GRState
* AddEQ(const GRState
* state
, SymbolRef sym
, const llvm::APSInt
& V
);
85 const GRState
* AddNE(const GRState
* state
, SymbolRef sym
, const llvm::APSInt
& V
);
87 const llvm::APSInt
* getSymVal(const GRState
* state
, SymbolRef sym
) const;
88 bool isNotEqual(const GRState
* state
, SymbolRef sym
, const llvm::APSInt
& V
)
90 bool isEqual(const GRState
* state
, SymbolRef sym
, const llvm::APSInt
& V
)
93 const GRState
* RemoveDeadBindings(const GRState
* state
, SymbolReaper
& SymReaper
);
95 void print(const GRState
* state
, llvm::raw_ostream
& Out
,
96 const char* nl
, const char *sep
);
99 } // end anonymous namespace
101 ConstraintManager
* GR::CreateBasicConstraintManager(GRStateManager
& statemgr
,
102 GRSubEngine
&subengine
) {
103 return new BasicConstraintManager(statemgr
, subengine
);
108 BasicConstraintManager::assumeSymNE(const GRState
*state
, SymbolRef sym
,
109 const llvm::APSInt
&V
,
110 const llvm::APSInt
&Adjustment
) {
111 // First, determine if sym == X, where X+Adjustment != V.
112 llvm::APSInt Adjusted
= V
-Adjustment
;
113 if (const llvm::APSInt
* X
= getSymVal(state
, sym
)) {
114 bool isFeasible
= (*X
!= Adjusted
);
115 return isFeasible
? state
: NULL
;
118 // Second, determine if sym+Adjustment != V.
119 if (isNotEqual(state
, sym
, Adjusted
))
122 // If we reach here, sym is not a constant and we don't know if it is != V.
123 // Make that assumption.
124 return AddNE(state
, sym
, Adjusted
);
128 BasicConstraintManager::assumeSymEQ(const GRState
*state
, SymbolRef sym
,
129 const llvm::APSInt
&V
,
130 const llvm::APSInt
&Adjustment
) {
131 // First, determine if sym == X, where X+Adjustment != V.
132 llvm::APSInt Adjusted
= V
-Adjustment
;
133 if (const llvm::APSInt
* X
= getSymVal(state
, sym
)) {
134 bool isFeasible
= (*X
== Adjusted
);
135 return isFeasible
? state
: NULL
;
138 // Second, determine if sym+Adjustment != V.
139 if (isNotEqual(state
, sym
, Adjusted
))
142 // If we reach here, sym is not a constant and we don't know if it is == V.
143 // Make that assumption.
144 return AddEQ(state
, sym
, Adjusted
);
147 // The logic for these will be handled in another ConstraintManager.
149 BasicConstraintManager::assumeSymLT(const GRState
*state
, SymbolRef sym
,
150 const llvm::APSInt
&V
,
151 const llvm::APSInt
&Adjustment
) {
152 // Is 'V' the smallest possible value?
153 if (V
== llvm::APSInt::getMinValue(V
.getBitWidth(), V
.isUnsigned())) {
154 // sym cannot be any value less than 'V'. This path is infeasible.
158 // FIXME: For now have assuming x < y be the same as assuming sym != V;
159 return assumeSymNE(state
, sym
, V
, Adjustment
);
163 BasicConstraintManager::assumeSymGT(const GRState
*state
, SymbolRef sym
,
164 const llvm::APSInt
&V
,
165 const llvm::APSInt
&Adjustment
) {
166 // Is 'V' the largest possible value?
167 if (V
== llvm::APSInt::getMaxValue(V
.getBitWidth(), V
.isUnsigned())) {
168 // sym cannot be any value greater than 'V'. This path is infeasible.
172 // FIXME: For now have assuming x > y be the same as assuming sym != V;
173 return assumeSymNE(state
, sym
, V
, Adjustment
);
177 BasicConstraintManager::assumeSymGE(const GRState
*state
, SymbolRef sym
,
178 const llvm::APSInt
&V
,
179 const llvm::APSInt
&Adjustment
) {
180 // Reject a path if the value of sym is a constant X and !(X+Adj >= V).
181 if (const llvm::APSInt
*X
= getSymVal(state
, sym
)) {
182 bool isFeasible
= (*X
>= V
-Adjustment
);
183 return isFeasible
? state
: NULL
;
186 // Sym is not a constant, but it is worth looking to see if V is the
187 // maximum integer value.
188 if (V
== llvm::APSInt::getMaxValue(V
.getBitWidth(), V
.isUnsigned())) {
189 llvm::APSInt Adjusted
= V
-Adjustment
;
191 // If we know that sym != V (after adjustment), then this condition
192 // is infeasible since there is no other value greater than V.
193 bool isFeasible
= !isNotEqual(state
, sym
, Adjusted
);
195 // If the path is still feasible then as a consequence we know that
196 // 'sym+Adjustment == V' because there are no larger values.
197 // Add this constraint.
198 return isFeasible
? AddEQ(state
, sym
, Adjusted
) : NULL
;
205 BasicConstraintManager::assumeSymLE(const GRState
*state
, SymbolRef sym
,
206 const llvm::APSInt
&V
,
207 const llvm::APSInt
&Adjustment
) {
208 // Reject a path if the value of sym is a constant X and !(X+Adj <= V).
209 if (const llvm::APSInt
* X
= getSymVal(state
, sym
)) {
210 bool isFeasible
= (*X
<= V
-Adjustment
);
211 return isFeasible
? state
: NULL
;
214 // Sym is not a constant, but it is worth looking to see if V is the
215 // minimum integer value.
216 if (V
== llvm::APSInt::getMinValue(V
.getBitWidth(), V
.isUnsigned())) {
217 llvm::APSInt Adjusted
= V
-Adjustment
;
219 // If we know that sym != V (after adjustment), then this condition
220 // is infeasible since there is no other value less than V.
221 bool isFeasible
= !isNotEqual(state
, sym
, Adjusted
);
223 // If the path is still feasible then as a consequence we know that
224 // 'sym+Adjustment == V' because there are no smaller values.
225 // Add this constraint.
226 return isFeasible
? AddEQ(state
, sym
, Adjusted
) : NULL
;
232 const GRState
* BasicConstraintManager::AddEQ(const GRState
* state
, SymbolRef sym
,
233 const llvm::APSInt
& V
) {
234 // Create a new state with the old binding replaced.
235 return state
->set
<ConstEq
>(sym
, &state
->getBasicVals().getValue(V
));
238 const GRState
* BasicConstraintManager::AddNE(const GRState
* state
, SymbolRef sym
,
239 const llvm::APSInt
& V
) {
241 // First, retrieve the NE-set associated with the given symbol.
242 ConstNotEqTy::data_type
* T
= state
->get
<ConstNotEq
>(sym
);
243 GRState::IntSetTy S
= T
? *T
: ISetFactory
.getEmptySet();
245 // Now add V to the NE set.
246 S
= ISetFactory
.add(S
, &state
->getBasicVals().getValue(V
));
248 // Create a new state with the old binding replaced.
249 return state
->set
<ConstNotEq
>(sym
, S
);
252 const llvm::APSInt
* BasicConstraintManager::getSymVal(const GRState
* state
,
253 SymbolRef sym
) const {
254 const ConstEqTy::data_type
* T
= state
->get
<ConstEq
>(sym
);
255 return T
? *T
: NULL
;
258 bool BasicConstraintManager::isNotEqual(const GRState
* state
, SymbolRef sym
,
259 const llvm::APSInt
& V
) const {
261 // Retrieve the NE-set associated with the given symbol.
262 const ConstNotEqTy::data_type
* T
= state
->get
<ConstNotEq
>(sym
);
264 // See if V is present in the NE-set.
265 return T
? T
->contains(&state
->getBasicVals().getValue(V
)) : false;
268 bool BasicConstraintManager::isEqual(const GRState
* state
, SymbolRef sym
,
269 const llvm::APSInt
& V
) const {
270 // Retrieve the EQ-set associated with the given symbol.
271 const ConstEqTy::data_type
* T
= state
->get
<ConstEq
>(sym
);
272 // See if V is present in the EQ-set.
273 return T
? **T
== V
: false;
276 /// Scan all symbols referenced by the constraints. If the symbol is not alive
277 /// as marked in LSymbols, mark it as dead in DSymbols.
279 BasicConstraintManager::RemoveDeadBindings(const GRState
* state
,
280 SymbolReaper
& SymReaper
) {
282 ConstEqTy CE
= state
->get
<ConstEq
>();
283 ConstEqTy::Factory
& CEFactory
= state
->get_context
<ConstEq
>();
285 for (ConstEqTy::iterator I
= CE
.begin(), E
= CE
.end(); I
!=E
; ++I
) {
286 SymbolRef sym
= I
.getKey();
287 if (SymReaper
.maybeDead(sym
))
288 CE
= CEFactory
.remove(CE
, sym
);
290 state
= state
->set
<ConstEq
>(CE
);
292 ConstNotEqTy CNE
= state
->get
<ConstNotEq
>();
293 ConstNotEqTy::Factory
& CNEFactory
= state
->get_context
<ConstNotEq
>();
295 for (ConstNotEqTy::iterator I
= CNE
.begin(), E
= CNE
.end(); I
!= E
; ++I
) {
296 SymbolRef sym
= I
.getKey();
297 if (SymReaper
.maybeDead(sym
))
298 CNE
= CNEFactory
.remove(CNE
, sym
);
301 return state
->set
<ConstNotEq
>(CNE
);
304 void BasicConstraintManager::print(const GRState
* state
, llvm::raw_ostream
& Out
,
305 const char* nl
, const char *sep
) {
306 // Print equality constraints.
308 ConstEqTy CE
= state
->get
<ConstEq
>();
311 Out
<< nl
<< sep
<< "'==' constraints:";
312 for (ConstEqTy::iterator I
= CE
.begin(), E
= CE
.end(); I
!=E
; ++I
)
313 Out
<< nl
<< " $" << I
.getKey() << " : " << *I
.getData();
316 // Print != constraints.
318 ConstNotEqTy CNE
= state
->get
<ConstNotEq
>();
320 if (!CNE
.isEmpty()) {
321 Out
<< nl
<< sep
<< "'!=' constraints:";
323 for (ConstNotEqTy::iterator I
= CNE
.begin(), EI
= CNE
.end(); I
!=EI
; ++I
) {
324 Out
<< nl
<< " $" << I
.getKey() << " : ";
327 GRState::IntSetTy::iterator J
= I
.getData().begin(),
328 EJ
= I
.getData().end();
330 for ( ; J
!= EJ
; ++J
) {
331 if (isFirst
) isFirst
= false;
334 Out
<< (*J
)->getSExtValue(); // Hack: should print to raw_ostream.