Zhongxing Xu | d19e21b | 2008-08-29 15:09:12 +0000 | [diff] [blame] | 1 | //== BasicConstraintManager.cpp - Manage basic constraints.------*- C++ -*--==// |
| 2 | // |
| 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 | // |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 10 | // This file defines BasicConstraintManager, a class that tracks simple |
Zhongxing Xu | d19e21b | 2008-08-29 15:09:12 +0000 | [diff] [blame] | 11 | // equality and inequality constraints on symbolic values of GRState. |
| 12 | // |
| 13 | //===----------------------------------------------------------------------===// |
| 14 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 15 | #include "SimpleConstraintManager.h" |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 16 | #include "clang/Analysis/PathSensitive/GRState.h" |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 17 | #include "clang/Analysis/PathSensitive/GRStateTrait.h" |
Ted Kremenek | 2fb78a7 | 2008-12-17 21:50:35 +0000 | [diff] [blame] | 18 | #include "clang/Analysis/PathSensitive/GRTransferFuncs.h" |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 19 | #include "llvm/Support/raw_ostream.h" |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 20 | |
| 21 | using namespace clang; |
| 22 | |
Ted Kremenek | 8ee74d5 | 2009-01-26 06:04:53 +0000 | [diff] [blame] | 23 | |
Kovarththanan Rajaratnam | ba5fb5a | 2009-11-28 06:07:30 +0000 | [diff] [blame] | 24 | namespace { class ConstNotEq {}; } |
| 25 | namespace { class ConstEq {}; } |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 26 | |
Ted Kremenek | 2dabd43 | 2008-12-05 02:27:51 +0000 | [diff] [blame] | 27 | typedef llvm::ImmutableMap<SymbolRef,GRState::IntSetTy> ConstNotEqTy; |
| 28 | typedef llvm::ImmutableMap<SymbolRef,const llvm::APSInt*> ConstEqTy; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 29 | |
Ted Kremenek | 8ee74d5 | 2009-01-26 06:04:53 +0000 | [diff] [blame] | 30 | static int ConstEqIndex = 0; |
| 31 | static int ConstNotEqIndex = 0; |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 32 | |
Ted Kremenek | 8ee74d5 | 2009-01-26 06:04:53 +0000 | [diff] [blame] | 33 | namespace clang { |
| 34 | template<> |
| 35 | struct GRStateTrait<ConstNotEq> : public GRStatePartialTrait<ConstNotEqTy> { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 36 | static inline void* GDMIndex() { return &ConstNotEqIndex; } |
Ted Kremenek | 8ee74d5 | 2009-01-26 06:04:53 +0000 | [diff] [blame] | 37 | }; |
| 38 | |
| 39 | template<> |
| 40 | struct GRStateTrait<ConstEq> : public GRStatePartialTrait<ConstEqTy> { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 41 | static inline void* GDMIndex() { return &ConstEqIndex; } |
Ted Kremenek | 8ee74d5 | 2009-01-26 06:04:53 +0000 | [diff] [blame] | 42 | }; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 43 | } |
| 44 | |
Ted Kremenek | 8ee74d5 | 2009-01-26 06:04:53 +0000 | [diff] [blame] | 45 | namespace { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 46 | // BasicConstraintManager only tracks equality and inequality constraints of |
| 47 | // constants and integer variables. |
Kovarththanan Rajaratnam | ba5fb5a | 2009-11-28 06:07:30 +0000 | [diff] [blame] | 48 | class BasicConstraintManager |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 49 | : public SimpleConstraintManager { |
Zhongxing Xu | f0bc50e | 2008-11-27 06:08:40 +0000 | [diff] [blame] | 50 | GRState::IntSetTy::Factory ISetFactory; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 51 | public: |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 52 | BasicConstraintManager(GRStateManager& statemgr) |
Ted Kremenek | f1b8227 | 2009-06-18 23:20:05 +0000 | [diff] [blame] | 53 | : ISetFactory(statemgr.getAllocator()) {} |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 54 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 55 | const GRState* AssumeSymNE(const GRState* state, SymbolRef sym, |
| 56 | const llvm::APSInt& V); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 57 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 58 | const GRState* AssumeSymEQ(const GRState* state, SymbolRef sym, |
| 59 | const llvm::APSInt& V); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 60 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 61 | const GRState* AssumeSymLT(const GRState* state, SymbolRef sym, |
| 62 | const llvm::APSInt& V); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 63 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 64 | const GRState* AssumeSymGT(const GRState* state, SymbolRef sym, |
| 65 | const llvm::APSInt& V); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 66 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 67 | const GRState* AssumeSymGE(const GRState* state, SymbolRef sym, |
| 68 | const llvm::APSInt& V); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 69 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 70 | const GRState* AssumeSymLE(const GRState* state, SymbolRef sym, |
| 71 | const llvm::APSInt& V); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 72 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 73 | const GRState* AddEQ(const GRState* state, SymbolRef sym, const llvm::APSInt& V); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 74 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 75 | const GRState* AddNE(const GRState* state, SymbolRef sym, const llvm::APSInt& V); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 76 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 77 | const llvm::APSInt* getSymVal(const GRState* state, SymbolRef sym) const; |
| 78 | bool isNotEqual(const GRState* state, SymbolRef sym, const llvm::APSInt& V) |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 79 | const; |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 80 | bool isEqual(const GRState* state, SymbolRef sym, const llvm::APSInt& V) |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 81 | const; |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 82 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 83 | const GRState* RemoveDeadBindings(const GRState* state, SymbolReaper& SymReaper); |
Ted Kremenek | 241677a | 2009-01-21 22:26:05 +0000 | [diff] [blame] | 84 | |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 85 | void print(const GRState* state, llvm::raw_ostream& Out, |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 86 | const char* nl, const char *sep); |
| 87 | }; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 88 | |
| 89 | } // end anonymous namespace |
| 90 | |
| 91 | ConstraintManager* clang::CreateBasicConstraintManager(GRStateManager& StateMgr) |
| 92 | { |
| 93 | return new BasicConstraintManager(StateMgr); |
| 94 | } |
| 95 | |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 96 | const GRState* |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 97 | BasicConstraintManager::AssumeSymNE(const GRState *state, SymbolRef sym, |
| 98 | const llvm::APSInt& V) { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 99 | // First, determine if sym == X, where X != V. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 100 | if (const llvm::APSInt* X = getSymVal(state, sym)) { |
| 101 | bool isFeasible = (*X != V); |
| 102 | return isFeasible ? state : NULL; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 103 | } |
| 104 | |
| 105 | // Second, determine if sym != V. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 106 | if (isNotEqual(state, sym, V)) |
| 107 | return state; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 108 | |
| 109 | // If we reach here, sym is not a constant and we don't know if it is != V. |
| 110 | // Make that assumption. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 111 | return AddNE(state, sym, V); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 112 | } |
| 113 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 114 | const GRState *BasicConstraintManager::AssumeSymEQ(const GRState *state, |
| 115 | SymbolRef sym, |
| 116 | const llvm::APSInt &V) { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 117 | // First, determine if sym == X, where X != V. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 118 | if (const llvm::APSInt* X = getSymVal(state, sym)) { |
| 119 | bool isFeasible = *X == V; |
| 120 | return isFeasible ? state : NULL; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 121 | } |
| 122 | |
| 123 | // Second, determine if sym != V. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 124 | if (isNotEqual(state, sym, V)) |
| 125 | return NULL; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 126 | |
| 127 | // If we reach here, sym is not a constant and we don't know if it is == V. |
| 128 | // Make that assumption. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 129 | return AddEQ(state, sym, V); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 130 | } |
| 131 | |
| 132 | // These logic will be handled in another ConstraintManager. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 133 | const GRState *BasicConstraintManager::AssumeSymLT(const GRState *state, |
| 134 | SymbolRef sym, |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 135 | const llvm::APSInt& V) { |
Ted Kremenek | 73abd13 | 2008-12-03 18:56:12 +0000 | [diff] [blame] | 136 | // Is 'V' the smallest possible value? |
Chris Lattner | 071e04e | 2009-01-30 01:58:33 +0000 | [diff] [blame] | 137 | if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) { |
Ted Kremenek | 73abd13 | 2008-12-03 18:56:12 +0000 | [diff] [blame] | 138 | // sym cannot be any value less than 'V'. This path is infeasible. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 139 | return NULL; |
Ted Kremenek | 73abd13 | 2008-12-03 18:56:12 +0000 | [diff] [blame] | 140 | } |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 141 | |
| 142 | // FIXME: For now have assuming x < y be the same as assuming sym != V; |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 143 | return AssumeSymNE(state, sym, V); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 144 | } |
| 145 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 146 | const GRState *BasicConstraintManager::AssumeSymGT(const GRState *state, |
| 147 | SymbolRef sym, |
| 148 | const llvm::APSInt& V) { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 149 | |
Ted Kremenek | d7ff487 | 2008-12-03 19:06:30 +0000 | [diff] [blame] | 150 | // Is 'V' the largest possible value? |
Chris Lattner | 071e04e | 2009-01-30 01:58:33 +0000 | [diff] [blame] | 151 | if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) { |
Ted Kremenek | d7ff487 | 2008-12-03 19:06:30 +0000 | [diff] [blame] | 152 | // sym cannot be any value greater than 'V'. This path is infeasible. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 153 | return NULL; |
Ted Kremenek | d7ff487 | 2008-12-03 19:06:30 +0000 | [diff] [blame] | 154 | } |
| 155 | |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 156 | // FIXME: For now have assuming x > y be the same as assuming sym != V; |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 157 | return AssumeSymNE(state, sym, V); |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 158 | } |
| 159 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 160 | const GRState *BasicConstraintManager::AssumeSymGE(const GRState *state, |
| 161 | SymbolRef sym, |
| 162 | const llvm::APSInt &V) { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 163 | |
Ted Kremenek | 8c3e7fb | 2008-09-16 23:24:45 +0000 | [diff] [blame] | 164 | // Reject a path if the value of sym is a constant X and !(X >= V). |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 165 | if (const llvm::APSInt *X = getSymVal(state, sym)) { |
| 166 | bool isFeasible = *X >= V; |
| 167 | return isFeasible ? state : NULL; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 168 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 169 | |
Ted Kremenek | d7ff487 | 2008-12-03 19:06:30 +0000 | [diff] [blame] | 170 | // Sym is not a constant, but it is worth looking to see if V is the |
| 171 | // maximum integer value. |
Chris Lattner | 071e04e | 2009-01-30 01:58:33 +0000 | [diff] [blame] | 172 | if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) { |
Ted Kremenek | d7ff487 | 2008-12-03 19:06:30 +0000 | [diff] [blame] | 173 | // If we know that sym != V, then this condition is infeasible since |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 174 | // there is no other value greater than V. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 175 | bool isFeasible = !isNotEqual(state, sym, V); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 176 | |
Ted Kremenek | d7ff487 | 2008-12-03 19:06:30 +0000 | [diff] [blame] | 177 | // If the path is still feasible then as a consequence we know that |
| 178 | // 'sym == V' because we cannot have 'sym > V' (no larger values). |
| 179 | // Add this constraint. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 180 | return isFeasible ? AddEQ(state, sym, V) : NULL; |
Ted Kremenek | d7ff487 | 2008-12-03 19:06:30 +0000 | [diff] [blame] | 181 | } |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 182 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 183 | return state; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 184 | } |
| 185 | |
| 186 | const GRState* |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 187 | BasicConstraintManager::AssumeSymLE(const GRState* state, SymbolRef sym, |
| 188 | const llvm::APSInt& V) { |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 189 | |
Ted Kremenek | 73abd13 | 2008-12-03 18:56:12 +0000 | [diff] [blame] | 190 | // Reject a path if the value of sym is a constant X and !(X <= V). |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 191 | if (const llvm::APSInt* X = getSymVal(state, sym)) { |
| 192 | bool isFeasible = *X <= V; |
| 193 | return isFeasible ? state : NULL; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 194 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 195 | |
Ted Kremenek | 73abd13 | 2008-12-03 18:56:12 +0000 | [diff] [blame] | 196 | // Sym is not a constant, but it is worth looking to see if V is the |
| 197 | // minimum integer value. |
Chris Lattner | 071e04e | 2009-01-30 01:58:33 +0000 | [diff] [blame] | 198 | if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) { |
Ted Kremenek | 73abd13 | 2008-12-03 18:56:12 +0000 | [diff] [blame] | 199 | // If we know that sym != V, then this condition is infeasible since |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 200 | // there is no other value less than V. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 201 | bool isFeasible = !isNotEqual(state, sym, V); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 202 | |
Ted Kremenek | 73abd13 | 2008-12-03 18:56:12 +0000 | [diff] [blame] | 203 | // If the path is still feasible then as a consequence we know that |
| 204 | // 'sym == V' because we cannot have 'sym < V' (no smaller values). |
| 205 | // Add this constraint. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 206 | return isFeasible ? AddEQ(state, sym, V) : NULL; |
Ted Kremenek | 73abd13 | 2008-12-03 18:56:12 +0000 | [diff] [blame] | 207 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 208 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 209 | return state; |
Zhongxing Xu | 30ad167 | 2008-08-27 14:03:33 +0000 | [diff] [blame] | 210 | } |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 211 | |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 212 | const GRState* BasicConstraintManager::AddEQ(const GRState* state, SymbolRef sym, |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 213 | const llvm::APSInt& V) { |
| 214 | // Create a new state with the old binding replaced. |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 215 | return state->set<ConstEq>(sym, &V); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 216 | } |
| 217 | |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 218 | const GRState* BasicConstraintManager::AddNE(const GRState* state, SymbolRef sym, |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 219 | const llvm::APSInt& V) { |
Zhongxing Xu | f0bc50e | 2008-11-27 06:08:40 +0000 | [diff] [blame] | 220 | |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 221 | // First, retrieve the NE-set associated with the given symbol. |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 222 | ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 223 | GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet(); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 224 | |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 225 | // Now add V to the NE set. |
| 226 | S = ISetFactory.Add(S, &V); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 227 | |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 228 | // Create a new state with the old binding replaced. |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 229 | return state->set<ConstNotEq>(sym, S); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 230 | } |
| 231 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 232 | const llvm::APSInt* BasicConstraintManager::getSymVal(const GRState* state, |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 233 | SymbolRef sym) const { |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 234 | const ConstEqTy::data_type* T = state->get<ConstEq>(sym); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 235 | return T ? *T : NULL; |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 236 | } |
| 237 | |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 238 | bool BasicConstraintManager::isNotEqual(const GRState* state, SymbolRef sym, |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 239 | const llvm::APSInt& V) const { |
| 240 | |
| 241 | // Retrieve the NE-set associated with the given symbol. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 242 | const ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 243 | |
| 244 | // See if V is present in the NE-set. |
| 245 | return T ? T->contains(&V) : false; |
| 246 | } |
| 247 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 248 | bool BasicConstraintManager::isEqual(const GRState* state, SymbolRef sym, |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 249 | const llvm::APSInt& V) const { |
| 250 | // Retrieve the EQ-set associated with the given symbol. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 251 | const ConstEqTy::data_type* T = state->get<ConstEq>(sym); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 252 | // See if V is present in the EQ-set. |
| 253 | return T ? **T == V : false; |
| 254 | } |
| 255 | |
Zhongxing Xu | 8fd9b35 | 2008-11-27 02:39:34 +0000 | [diff] [blame] | 256 | /// Scan all symbols referenced by the constraints. If the symbol is not alive |
| 257 | /// as marked in LSymbols, mark it as dead in DSymbols. |
Ted Kremenek | 241677a | 2009-01-21 22:26:05 +0000 | [diff] [blame] | 258 | const GRState* |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 259 | BasicConstraintManager::RemoveDeadBindings(const GRState* state, |
Ted Kremenek | 241677a | 2009-01-21 22:26:05 +0000 | [diff] [blame] | 260 | SymbolReaper& SymReaper) { |
| 261 | |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 262 | ConstEqTy CE = state->get<ConstEq>(); |
| 263 | ConstEqTy::Factory& CEFactory = state->get_context<ConstEq>(); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 264 | |
| 265 | for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) { |
Ted Kremenek | 241677a | 2009-01-21 22:26:05 +0000 | [diff] [blame] | 266 | SymbolRef sym = I.getKey(); |
| 267 | if (SymReaper.maybeDead(sym)) CE = CEFactory.Remove(CE, sym); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 268 | } |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 269 | state = state->set<ConstEq>(CE); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 270 | |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 271 | ConstNotEqTy CNE = state->get<ConstNotEq>(); |
| 272 | ConstNotEqTy::Factory& CNEFactory = state->get_context<ConstNotEq>(); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 273 | |
| 274 | for (ConstNotEqTy::iterator I = CNE.begin(), E = CNE.end(); I != E; ++I) { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 275 | SymbolRef sym = I.getKey(); |
Ted Kremenek | 241677a | 2009-01-21 22:26:05 +0000 | [diff] [blame] | 276 | if (SymReaper.maybeDead(sym)) CNE = CNEFactory.Remove(CNE, sym); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 277 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 278 | |
Ted Kremenek | c878138 | 2009-06-17 22:28:13 +0000 | [diff] [blame] | 279 | return state->set<ConstNotEq>(CNE); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 280 | } |
| 281 | |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 282 | void BasicConstraintManager::print(const GRState* state, llvm::raw_ostream& Out, |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 283 | const char* nl, const char *sep) { |
| 284 | // Print equality constraints. |
| 285 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 286 | ConstEqTy CE = state->get<ConstEq>(); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 287 | |
| 288 | if (!CE.isEmpty()) { |
| 289 | Out << nl << sep << "'==' constraints:"; |
Ted Kremenek | 53ba0b6 | 2009-06-24 23:06:47 +0000 | [diff] [blame] | 290 | for (ConstEqTy::iterator I = CE.begin(), E = CE.end(); I!=E; ++I) |
| 291 | Out << nl << " $" << I.getKey() << " : " << *I.getData(); |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 292 | } |
| 293 | |
| 294 | // Print != constraints. |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 295 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 296 | ConstNotEqTy CNE = state->get<ConstNotEq>(); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 297 | |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 298 | if (!CNE.isEmpty()) { |
| 299 | Out << nl << sep << "'!=' constraints:"; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 300 | |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 301 | for (ConstNotEqTy::iterator I = CNE.begin(), EI = CNE.end(); I!=EI; ++I) { |
| 302 | Out << nl << " $" << I.getKey() << " : "; |
| 303 | bool isFirst = true; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 304 | |
| 305 | GRState::IntSetTy::iterator J = I.getData().begin(), |
| 306 | EJ = I.getData().end(); |
| 307 | |
| 308 | for ( ; J != EJ; ++J) { |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 309 | if (isFirst) isFirst = false; |
| 310 | else Out << ", "; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 311 | |
Zhongxing Xu | 7d94e26 | 2008-11-10 05:00:06 +0000 | [diff] [blame] | 312 | Out << (*J)->getSExtValue(); // Hack: should print to raw_ostream. |
Zhongxing Xu | 39cfed3 | 2008-08-29 14:52:36 +0000 | [diff] [blame] | 313 | } |
| 314 | } |
| 315 | } |
Daniel Dunbar | 0e194dd | 2008-08-30 02:06:22 +0000 | [diff] [blame] | 316 | } |