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 ProgramState.
13 //===----------------------------------------------------------------------===//
15 #include "SimpleConstraintManager.h"
16 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
17 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
18 #include "llvm/Support/raw_ostream.h"
20 using namespace clang;
24 namespace { class ConstNotEq {}; }
25 namespace { class ConstEq {}; }
27 typedef llvm::ImmutableMap<SymbolRef,ProgramState::IntSetTy> ConstNotEqTy;
28 typedef llvm::ImmutableMap<SymbolRef,const llvm::APSInt*> ConstEqTy;
30 static int ConstEqIndex = 0;
31 static int ConstNotEqIndex = 0;
36 struct ProgramStateTrait<ConstNotEq> :
37 public ProgramStatePartialTrait<ConstNotEqTy> {
38 static inline void *GDMIndex() { return &ConstNotEqIndex; }
42 struct ProgramStateTrait<ConstEq> : public ProgramStatePartialTrait<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 ProgramState::IntSetTy::Factory ISetFactory;
55 BasicConstraintManager(ProgramStateManager &statemgr, SubEngine &subengine)
56 : SimpleConstraintManager(subengine),
57 ISetFactory(statemgr.getAllocator()) {}
59 const ProgramState *assumeSymNE(const ProgramState *state,
61 const llvm::APSInt& V,
62 const llvm::APSInt& Adjustment);
64 const ProgramState *assumeSymEQ(const ProgramState *state,
66 const llvm::APSInt& V,
67 const llvm::APSInt& Adjustment);
69 const ProgramState *assumeSymLT(const ProgramState *state,
71 const llvm::APSInt& V,
72 const llvm::APSInt& Adjustment);
74 const ProgramState *assumeSymGT(const ProgramState *state,
76 const llvm::APSInt& V,
77 const llvm::APSInt& Adjustment);
79 const ProgramState *assumeSymGE(const ProgramState *state,
81 const llvm::APSInt& V,
82 const llvm::APSInt& Adjustment);
84 const ProgramState *assumeSymLE(const ProgramState *state,
86 const llvm::APSInt& V,
87 const llvm::APSInt& Adjustment);
89 const ProgramState *AddEQ(const ProgramState *state,
91 const llvm::APSInt& V);
93 const ProgramState *AddNE(const ProgramState *state,
95 const llvm::APSInt& V);
97 const llvm::APSInt* getSymVal(const ProgramState *state,
100 bool isNotEqual(const ProgramState *state,
102 const llvm::APSInt& V) const;
104 bool isEqual(const ProgramState *state,
106 const llvm::APSInt& V) const;
108 const ProgramState *removeDeadBindings(const ProgramState *state,
109 SymbolReaper& SymReaper);
111 void print(const ProgramState *state,
117 } // end anonymous namespace
120 ento::CreateBasicConstraintManager(ProgramStateManager& statemgr,
121 SubEngine &subengine) {
122 return new BasicConstraintManager(statemgr, subengine);
126 BasicConstraintManager::assumeSymNE(const ProgramState *state,
128 const llvm::APSInt &V,
129 const llvm::APSInt &Adjustment) {
130 // First, determine if sym == X, where X+Adjustment != V.
131 llvm::APSInt Adjusted = V-Adjustment;
132 if (const llvm::APSInt* X = getSymVal(state, sym)) {
133 bool isFeasible = (*X != Adjusted);
134 return isFeasible ? state : NULL;
137 // Second, determine if sym+Adjustment != V.
138 if (isNotEqual(state, sym, Adjusted))
141 // If we reach here, sym is not a constant and we don't know if it is != V.
142 // Make that assumption.
143 return AddNE(state, sym, Adjusted);
147 BasicConstraintManager::assumeSymEQ(const ProgramState *state,
149 const llvm::APSInt &V,
150 const llvm::APSInt &Adjustment) {
151 // First, determine if sym == X, where X+Adjustment != V.
152 llvm::APSInt Adjusted = V-Adjustment;
153 if (const llvm::APSInt* X = getSymVal(state, sym)) {
154 bool isFeasible = (*X == Adjusted);
155 return isFeasible ? state : NULL;
158 // Second, determine if sym+Adjustment != V.
159 if (isNotEqual(state, sym, Adjusted))
162 // If we reach here, sym is not a constant and we don't know if it is == V.
163 // Make that assumption.
164 return AddEQ(state, sym, Adjusted);
167 // The logic for these will be handled in another ConstraintManager.
169 BasicConstraintManager::assumeSymLT(const ProgramState *state,
171 const llvm::APSInt &V,
172 const llvm::APSInt &Adjustment) {
173 // Is 'V' the smallest possible value?
174 if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
175 // sym cannot be any value less than 'V'. This path is infeasible.
179 // FIXME: For now have assuming x < y be the same as assuming sym != V;
180 return assumeSymNE(state, sym, V, Adjustment);
184 BasicConstraintManager::assumeSymGT(const ProgramState *state,
186 const llvm::APSInt &V,
187 const llvm::APSInt &Adjustment) {
188 // Is 'V' the largest possible value?
189 if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
190 // sym cannot be any value greater than 'V'. This path is infeasible.
194 // FIXME: For now have assuming x > y be the same as assuming sym != V;
195 return assumeSymNE(state, sym, V, Adjustment);
199 BasicConstraintManager::assumeSymGE(const ProgramState *state,
201 const llvm::APSInt &V,
202 const llvm::APSInt &Adjustment) {
203 // Reject a path if the value of sym is a constant X and !(X+Adj >= V).
204 if (const llvm::APSInt *X = getSymVal(state, sym)) {
205 bool isFeasible = (*X >= V-Adjustment);
206 return isFeasible ? state : NULL;
209 // Sym is not a constant, but it is worth looking to see if V is the
210 // maximum integer value.
211 if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
212 llvm::APSInt Adjusted = V-Adjustment;
214 // If we know that sym != V (after adjustment), then this condition
215 // is infeasible since there is no other value greater than V.
216 bool isFeasible = !isNotEqual(state, sym, Adjusted);
218 // If the path is still feasible then as a consequence we know that
219 // 'sym+Adjustment == V' because there are no larger values.
220 // Add this constraint.
221 return isFeasible ? AddEQ(state, sym, Adjusted) : NULL;
228 BasicConstraintManager::assumeSymLE(const ProgramState *state,
230 const llvm::APSInt &V,
231 const llvm::APSInt &Adjustment) {
232 // Reject a path if the value of sym is a constant X and !(X+Adj <= V).
233 if (const llvm::APSInt* X = getSymVal(state, sym)) {
234 bool isFeasible = (*X <= V-Adjustment);
235 return isFeasible ? state : NULL;
238 // Sym is not a constant, but it is worth looking to see if V is the
239 // minimum integer value.
240 if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
241 llvm::APSInt Adjusted = V-Adjustment;
243 // If we know that sym != V (after adjustment), then this condition
244 // is infeasible since there is no other value less than V.
245 bool isFeasible = !isNotEqual(state, sym, Adjusted);
247 // If the path is still feasible then as a consequence we know that
248 // 'sym+Adjustment == V' because there are no smaller values.
249 // Add this constraint.
250 return isFeasible ? AddEQ(state, sym, Adjusted) : NULL;
256 const ProgramState *BasicConstraintManager::AddEQ(const ProgramState *state,
258 const llvm::APSInt& V) {
259 // Create a new state with the old binding replaced.
260 return state->set<ConstEq>(sym, &state->getBasicVals().getValue(V));
263 const ProgramState *BasicConstraintManager::AddNE(const ProgramState *state,
265 const llvm::APSInt& V) {
267 // First, retrieve the NE-set associated with the given symbol.
268 ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym);
269 ProgramState::IntSetTy S = T ? *T : ISetFactory.getEmptySet();
271 // Now add V to the NE set.
272 S = ISetFactory.add(S, &state->getBasicVals().getValue(V));
274 // Create a new state with the old binding replaced.
275 return state->set<ConstNotEq>(sym, S);
278 const llvm::APSInt* BasicConstraintManager::getSymVal(const ProgramState *state,
279 SymbolRef sym) const {
280 const ConstEqTy::data_type* T = state->get<ConstEq>(sym);
281 return T ? *T : NULL;
284 bool BasicConstraintManager::isNotEqual(const ProgramState *state,
286 const llvm::APSInt& V) const {
288 // Retrieve the NE-set associated with the given symbol.
289 const ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym);
291 // See if V is present in the NE-set.
292 return T ? T->contains(&state->getBasicVals().getValue(V)) : false;
295 bool BasicConstraintManager::isEqual(const ProgramState *state,
297 const llvm::APSInt& V) const {
298 // Retrieve the EQ-set associated with the given symbol.
299 const ConstEqTy::data_type* T = state->get<ConstEq>(sym);
300 // See if V is present in the EQ-set.
301 return T ? **T == V : false;
304 /// Scan all symbols referenced by the constraints. If the symbol is not alive
305 /// as marked in LSymbols, mark it as dead in DSymbols.
307 BasicConstraintManager::removeDeadBindings(const ProgramState *state,
308 SymbolReaper& SymReaper) {
310 ConstEqTy CE = state->get<ConstEq>();
311 ConstEqTy::Factory& CEFactory = state->get_context<ConstEq>();
313 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) {
314 SymbolRef sym = I.getKey();
315 if (SymReaper.maybeDead(sym))
316 CE = CEFactory.remove(CE, sym);
318 state = state->set<ConstEq>(CE);
320 ConstNotEqTy CNE = state->get<ConstNotEq>();
321 ConstNotEqTy::Factory& CNEFactory = state->get_context<ConstNotEq>();
323 for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) {
324 SymbolRef sym = I.getKey();
325 if (SymReaper.maybeDead(sym))
326 CNE = CNEFactory.remove(CNE, sym);
329 return state->set<ConstNotEq>(CNE);
332 void BasicConstraintManager::print(const ProgramState *state,
334 const char* nl, const char *sep) {
335 // Print equality constraints.
337 ConstEqTy CE = state->get<ConstEq>();
340 Out << nl << sep << "'==' constraints:";
341 for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I)
342 Out << nl << " $" << I.getKey() << " : " << *I.getData();
345 // Print != constraints.
347 ConstNotEqTy CNE = state->get<ConstNotEq>();
349 if (!CNE.isEmpty()) {
350 Out << nl << sep << "'!=' constraints:";
352 for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) {
353 Out << nl << " $" << I.getKey() << " : ";
356 ProgramState::IntSetTy::iterator J = I.getData().begin(),
357 EJ = I.getData().end();
359 for ( ; J != EJ; ++J) {
360 if (isFirst) isFirst = false;
363 Out << (*J)->getSExtValue(); // Hack: should print to raw_ostream.