Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 1 | //== SimpleConstraintManager.cpp --------------------------------*- 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 | // |
| 10 | // This file defines SimpleConstraintManager, a class that holds code shared |
| 11 | // between BasicConstraintManager and RangeConstraintManager. |
| 12 | // |
| 13 | //===----------------------------------------------------------------------===// |
| 14 | |
| 15 | #include "SimpleConstraintManager.h" |
| 16 | #include "clang/Analysis/PathSensitive/GRExprEngine.h" |
| 17 | #include "clang/Analysis/PathSensitive/GRState.h" |
| 18 | |
| 19 | namespace clang { |
| 20 | |
| 21 | SimpleConstraintManager::~SimpleConstraintManager() {} |
| 22 | |
Ted Kremenek | 66b5271 | 2009-03-11 02:22:59 +0000 | [diff] [blame] | 23 | bool SimpleConstraintManager::canReasonAbout(SVal X) const { |
Ted Kremenek | e0e4ebf | 2009-03-26 03:35:11 +0000 | [diff] [blame] | 24 | if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) { |
| 25 | const SymExpr *SE = SymVal->getSymbolicExpression(); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 26 | |
Ted Kremenek | e0e4ebf | 2009-03-26 03:35:11 +0000 | [diff] [blame] | 27 | if (isa<SymbolData>(SE)) |
| 28 | return true; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 29 | |
Ted Kremenek | e0e4ebf | 2009-03-26 03:35:11 +0000 | [diff] [blame] | 30 | if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) { |
| 31 | switch (SIE->getOpcode()) { |
| 32 | // We don't reason yet about bitwise-constraints on symbolic values. |
| 33 | case BinaryOperator::And: |
| 34 | case BinaryOperator::Or: |
| 35 | case BinaryOperator::Xor: |
| 36 | return false; |
| 37 | // We don't reason yet about arithmetic constraints on symbolic values. |
| 38 | case BinaryOperator::Mul: |
| 39 | case BinaryOperator::Div: |
| 40 | case BinaryOperator::Rem: |
| 41 | case BinaryOperator::Add: |
| 42 | case BinaryOperator::Sub: |
| 43 | case BinaryOperator::Shl: |
| 44 | case BinaryOperator::Shr: |
| 45 | return false; |
| 46 | // All other cases. |
| 47 | default: |
| 48 | return true; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 49 | } |
Ted Kremenek | e0e4ebf | 2009-03-26 03:35:11 +0000 | [diff] [blame] | 50 | } |
| 51 | |
| 52 | return false; |
Ted Kremenek | 7de20fe | 2009-03-11 02:29:48 +0000 | [diff] [blame] | 53 | } |
| 54 | |
Ted Kremenek | 66b5271 | 2009-03-11 02:22:59 +0000 | [diff] [blame] | 55 | return true; |
| 56 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 57 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 58 | const GRState *SimpleConstraintManager::Assume(const GRState *state, |
Ted Kremenek | 5b9bd21 | 2009-09-11 22:07:28 +0000 | [diff] [blame] | 59 | DefinedSVal Cond, |
| 60 | bool Assumption) { |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 61 | if (isa<NonLoc>(Cond)) |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 62 | return Assume(state, cast<NonLoc>(Cond), Assumption); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 63 | else |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 64 | return Assume(state, cast<Loc>(Cond), Assumption); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 65 | } |
| 66 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 67 | const GRState *SimpleConstraintManager::Assume(const GRState *state, Loc Cond, |
| 68 | bool Assumption) { |
| 69 | |
| 70 | state = AssumeAux(state, Cond, Assumption); |
| 71 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 72 | // EvalAssume is used to call into the GRTransferFunction object to perform |
| 73 | // any checker-specific update of the state based on this assumption being |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 74 | // true or false. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 75 | return state ? state->getTransferFuncs().EvalAssume(state, Cond, Assumption) |
| 76 | : NULL; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 77 | } |
| 78 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 79 | const GRState *SimpleConstraintManager::AssumeAux(const GRState *state, |
| 80 | Loc Cond, bool Assumption) { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 81 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 82 | BasicValueFactory &BasicVals = state->getBasicVals(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 83 | |
| 84 | switch (Cond.getSubKind()) { |
| 85 | default: |
| 86 | assert (false && "'Assume' not implemented for this Loc."); |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 87 | return state; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 88 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 89 | case loc::MemRegionKind: { |
| 90 | // FIXME: Should this go into the storemanager? |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 91 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 92 | const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion(); |
| 93 | const SubRegion *SubR = dyn_cast<SubRegion>(R); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 94 | |
| 95 | while (SubR) { |
| 96 | // FIXME: now we only find the first symbolic region. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 97 | if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) { |
Zhongxing Xu | 3330dcb | 2009-04-10 06:06:13 +0000 | [diff] [blame] | 98 | if (Assumption) |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 99 | return AssumeSymNE(state, SymR->getSymbol(), |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 100 | BasicVals.getZeroWithPtrWidth()); |
Zhongxing Xu | 3330dcb | 2009-04-10 06:06:13 +0000 | [diff] [blame] | 101 | else |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 102 | return AssumeSymEQ(state, SymR->getSymbol(), |
| 103 | BasicVals.getZeroWithPtrWidth()); |
Zhongxing Xu | 3330dcb | 2009-04-10 06:06:13 +0000 | [diff] [blame] | 104 | } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 105 | SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); |
| 106 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 107 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 108 | // FALL-THROUGH. |
| 109 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 110 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 111 | case loc::GotoLabelKind: |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 112 | return Assumption ? state : NULL; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 113 | |
| 114 | case loc::ConcreteIntKind: { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 115 | bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 116 | bool isFeasible = b ? Assumption : !Assumption; |
| 117 | return isFeasible ? state : NULL; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 118 | } |
| 119 | } // end switch |
| 120 | } |
| 121 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 122 | const GRState *SimpleConstraintManager::Assume(const GRState *state, |
| 123 | NonLoc Cond, |
| 124 | bool Assumption) { |
| 125 | |
| 126 | state = AssumeAux(state, Cond, Assumption); |
| 127 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 128 | // EvalAssume is used to call into the GRTransferFunction object to perform |
| 129 | // any checker-specific update of the state based on this assumption being |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 130 | // true or false. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 131 | return state ? state->getTransferFuncs().EvalAssume(state, Cond, Assumption) |
| 132 | : NULL; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 133 | } |
| 134 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 135 | const GRState *SimpleConstraintManager::AssumeAux(const GRState *state, |
| 136 | NonLoc Cond, |
| 137 | bool Assumption) { |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 138 | |
Zhongxing Xu | a129eb9 | 2009-03-25 05:58:37 +0000 | [diff] [blame] | 139 | // We cannot reason about SymIntExpr and SymSymExpr. |
| 140 | if (!canReasonAbout(Cond)) { |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 141 | // Just return the current state indicating that the path is feasible. |
| 142 | // This may be an over-approximation of what is possible. |
| 143 | return state; |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 144 | } |
Zhongxing Xu | a129eb9 | 2009-03-25 05:58:37 +0000 | [diff] [blame] | 145 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 146 | BasicValueFactory &BasicVals = state->getBasicVals(); |
| 147 | SymbolManager &SymMgr = state->getSymbolManager(); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 148 | |
| 149 | switch (Cond.getSubKind()) { |
| 150 | default: |
| 151 | assert(false && "'Assume' not implemented for this NonLoc"); |
| 152 | |
| 153 | case nonloc::SymbolValKind: { |
| 154 | nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); |
| 155 | SymbolRef sym = SV.getSymbol(); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 156 | QualType T = SymMgr.getType(sym); |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 157 | const llvm::APSInt &zero = BasicVals.getValue(0, T); |
| 158 | |
| 159 | return Assumption ? AssumeSymNE(state, sym, zero) |
| 160 | : AssumeSymEQ(state, sym, zero); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 161 | } |
| 162 | |
Ted Kremenek | e0e4ebf | 2009-03-26 03:35:11 +0000 | [diff] [blame] | 163 | case nonloc::SymExprValKind: { |
| 164 | nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond); |
Ted Kremenek | 8041747 | 2009-09-25 00:18:15 +0000 | [diff] [blame] | 165 | if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression())){ |
| 166 | // FIXME: This is a hack. It silently converts the RHS integer to be |
| 167 | // of the same type as on the left side. This should be removed once |
| 168 | // we support truncation/extension of symbolic values. |
| 169 | GRStateManager &StateMgr = state->getStateManager(); |
| 170 | ASTContext &Ctx = StateMgr.getContext(); |
| 171 | QualType LHSType = SE->getLHS()->getType(Ctx); |
| 172 | BasicValueFactory &BasicVals = StateMgr.getBasicVals(); |
| 173 | const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS()); |
| 174 | SymIntExpr SENew(SE->getLHS(), SE->getOpcode(), RHS, SE->getType(Ctx)); |
| 175 | |
| 176 | return AssumeSymInt(state, Assumption, &SENew); |
| 177 | } |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 178 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 179 | // For all other symbolic expressions, over-approximate and consider |
| 180 | // the constraint feasible. |
| 181 | return state; |
Ted Kremenek | e0e4ebf | 2009-03-26 03:35:11 +0000 | [diff] [blame] | 182 | } |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 183 | |
| 184 | case nonloc::ConcreteIntKind: { |
| 185 | bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 186 | bool isFeasible = b ? Assumption : !Assumption; |
| 187 | return isFeasible ? state : NULL; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 188 | } |
| 189 | |
| 190 | case nonloc::LocAsIntegerKind: |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 191 | return AssumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(), |
| 192 | Assumption); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 193 | } // end switch |
| 194 | } |
| 195 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 196 | const GRState *SimpleConstraintManager::AssumeSymInt(const GRState *state, |
| 197 | bool Assumption, |
| 198 | const SymIntExpr *SE) { |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 199 | |
Ted Kremenek | e0e4ebf | 2009-03-26 03:35:11 +0000 | [diff] [blame] | 200 | |
| 201 | // Here we assume that LHS is a symbol. This is consistent with the |
| 202 | // rest of the constraint manager logic. |
| 203 | SymbolRef Sym = cast<SymbolData>(SE->getLHS()); |
| 204 | const llvm::APSInt &Int = SE->getRHS(); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 205 | |
Ted Kremenek | e0e4ebf | 2009-03-26 03:35:11 +0000 | [diff] [blame] | 206 | switch (SE->getOpcode()) { |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 207 | default: |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 208 | // No logic yet for other operators. Assume the constraint is feasible. |
| 209 | return state; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 210 | |
| 211 | case BinaryOperator::EQ: |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 212 | return Assumption ? AssumeSymEQ(state, Sym, Int) |
| 213 | : AssumeSymNE(state, Sym, Int); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 214 | |
| 215 | case BinaryOperator::NE: |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 216 | return Assumption ? AssumeSymNE(state, Sym, Int) |
| 217 | : AssumeSymEQ(state, Sym, Int); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 218 | case BinaryOperator::GT: |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 219 | return Assumption ? AssumeSymGT(state, Sym, Int) |
| 220 | : AssumeSymLE(state, Sym, Int); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 221 | |
| 222 | case BinaryOperator::GE: |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 223 | return Assumption ? AssumeSymGE(state, Sym, Int) |
| 224 | : AssumeSymLT(state, Sym, Int); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 225 | |
| 226 | case BinaryOperator::LT: |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 227 | return Assumption ? AssumeSymLT(state, Sym, Int) |
| 228 | : AssumeSymGE(state, Sym, Int); |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 229 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 230 | case BinaryOperator::LE: |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 231 | return Assumption ? AssumeSymLE(state, Sym, Int) |
| 232 | : AssumeSymGT(state, Sym, Int); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 233 | } // end switch |
| 234 | } |
| 235 | |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 236 | const GRState *SimpleConstraintManager::AssumeInBound(const GRState *state, |
Ted Kremenek | 5b9bd21 | 2009-09-11 22:07:28 +0000 | [diff] [blame] | 237 | DefinedSVal Idx, |
| 238 | DefinedSVal UpperBound, |
Mike Stump | 1eb4433 | 2009-09-09 15:08:12 +0000 | [diff] [blame] | 239 | bool Assumption) { |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 240 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 241 | // Only support ConcreteInt for now. |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 242 | if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound))) |
| 243 | return state; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 244 | |
Ted Kremenek | f1b8227 | 2009-06-18 23:20:05 +0000 | [diff] [blame] | 245 | const llvm::APSInt& Zero = state->getBasicVals().getZeroWithPtrWidth(false); |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 246 | llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue(); |
| 247 | // IdxV might be too narrow. |
| 248 | if (IdxV.getBitWidth() < Zero.getBitWidth()) |
| 249 | IdxV.extend(Zero.getBitWidth()); |
| 250 | // UBV might be too narrow, too. |
| 251 | llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue(); |
| 252 | if (UBV.getBitWidth() < Zero.getBitWidth()) |
| 253 | UBV.extend(Zero.getBitWidth()); |
| 254 | |
| 255 | bool InBound = (Zero <= IdxV) && (IdxV < UBV); |
Ted Kremenek | a591bc0 | 2009-06-18 22:57:13 +0000 | [diff] [blame] | 256 | bool isFeasible = Assumption ? InBound : !InBound; |
| 257 | return isFeasible ? state : NULL; |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 258 | } |
| 259 | |
| 260 | } // end of namespace clang |