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 | 7de20fe | 2009-03-11 02:29:48 +0000 | [diff] [blame] | 24 | if (nonloc::SymIntConstraintVal *Y = dyn_cast<nonloc::SymIntConstraintVal>(&X)) { |
| 25 | const SymIntConstraint& C = Y->getConstraint(); |
| 26 | switch (C.getOpcode()) { |
| 27 | // We don't reason yet about bitwise-constraints on symbolic values. |
| 28 | case BinaryOperator::And: |
| 29 | case BinaryOperator::Or: |
| 30 | case BinaryOperator::Xor: |
| 31 | return false; |
| 32 | default: |
| 33 | return true; |
| 34 | } |
| 35 | } |
| 36 | |
Ted Kremenek | 66b5271 | 2009-03-11 02:22:59 +0000 | [diff] [blame] | 37 | return true; |
| 38 | } |
| 39 | |
Ted Kremenek | 4502195 | 2009-02-14 17:08:39 +0000 | [diff] [blame] | 40 | const GRState* |
| 41 | SimpleConstraintManager::Assume(const GRState* St, SVal Cond, bool Assumption, |
| 42 | bool& isFeasible) { |
| 43 | if (Cond.isUnknown()) { |
| 44 | isFeasible = true; |
| 45 | return St; |
| 46 | } |
| 47 | |
| 48 | if (isa<NonLoc>(Cond)) |
| 49 | return Assume(St, cast<NonLoc>(Cond), Assumption, isFeasible); |
| 50 | else |
| 51 | return Assume(St, cast<Loc>(Cond), Assumption, isFeasible); |
| 52 | } |
| 53 | |
| 54 | const GRState* |
| 55 | SimpleConstraintManager::Assume(const GRState* St, Loc Cond, bool Assumption, |
| 56 | bool& isFeasible) { |
| 57 | St = AssumeAux(St, Cond, Assumption, isFeasible); |
| 58 | |
| 59 | if (!isFeasible) |
| 60 | return St; |
| 61 | |
| 62 | // EvalAssume is used to call into the GRTransferFunction object to perform |
| 63 | // any checker-specific update of the state based on this assumption being |
| 64 | // true or false. |
| 65 | return StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption, |
| 66 | isFeasible); |
| 67 | } |
| 68 | |
| 69 | const GRState* |
| 70 | SimpleConstraintManager::AssumeAux(const GRState* St, Loc Cond, bool Assumption, |
| 71 | bool& isFeasible) { |
| 72 | BasicValueFactory& BasicVals = StateMgr.getBasicVals(); |
| 73 | |
| 74 | switch (Cond.getSubKind()) { |
| 75 | default: |
| 76 | assert (false && "'Assume' not implemented for this Loc."); |
| 77 | return St; |
| 78 | |
| 79 | case loc::SymbolValKind: |
| 80 | if (Assumption) |
| 81 | return AssumeSymNE(St, cast<loc::SymbolVal>(Cond).getSymbol(), |
| 82 | BasicVals.getZeroWithPtrWidth(), isFeasible); |
| 83 | else |
| 84 | return AssumeSymEQ(St, cast<loc::SymbolVal>(Cond).getSymbol(), |
| 85 | BasicVals.getZeroWithPtrWidth(), isFeasible); |
| 86 | |
| 87 | case loc::MemRegionKind: { |
| 88 | // FIXME: Should this go into the storemanager? |
| 89 | |
| 90 | const MemRegion* R = cast<loc::MemRegionVal>(Cond).getRegion(); |
| 91 | const SubRegion* SubR = dyn_cast<SubRegion>(R); |
| 92 | |
| 93 | while (SubR) { |
| 94 | // FIXME: now we only find the first symbolic region. |
| 95 | if (const SymbolicRegion* SymR = dyn_cast<SymbolicRegion>(SubR)) |
| 96 | return AssumeAux(St, loc::SymbolVal(SymR->getSymbol()), Assumption, |
| 97 | isFeasible); |
| 98 | SubR = dyn_cast<SubRegion>(SubR->getSuperRegion()); |
| 99 | } |
| 100 | |
| 101 | // FALL-THROUGH. |
| 102 | } |
| 103 | |
| 104 | case loc::FuncValKind: |
| 105 | case loc::GotoLabelKind: |
| 106 | isFeasible = Assumption; |
| 107 | return St; |
| 108 | |
| 109 | case loc::ConcreteIntKind: { |
| 110 | bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0; |
| 111 | isFeasible = b ? Assumption : !Assumption; |
| 112 | return St; |
| 113 | } |
| 114 | } // end switch |
| 115 | } |
| 116 | |
| 117 | const GRState* |
| 118 | SimpleConstraintManager::Assume(const GRState* St, NonLoc Cond, bool Assumption, |
| 119 | bool& isFeasible) { |
| 120 | St = AssumeAux(St, Cond, Assumption, isFeasible); |
| 121 | |
| 122 | if (!isFeasible) |
| 123 | return St; |
| 124 | |
| 125 | // EvalAssume is used to call into the GRTransferFunction object to perform |
| 126 | // any checker-specific update of the state based on this assumption being |
| 127 | // true or false. |
| 128 | return StateMgr.getTransferFuncs().EvalAssume(StateMgr, St, Cond, Assumption, |
| 129 | isFeasible); |
| 130 | } |
| 131 | |
| 132 | const GRState* |
| 133 | SimpleConstraintManager::AssumeAux(const GRState* St,NonLoc Cond, |
| 134 | bool Assumption, bool& isFeasible) { |
| 135 | BasicValueFactory& BasicVals = StateMgr.getBasicVals(); |
| 136 | SymbolManager& SymMgr = StateMgr.getSymbolManager(); |
| 137 | |
| 138 | switch (Cond.getSubKind()) { |
| 139 | default: |
| 140 | assert(false && "'Assume' not implemented for this NonLoc"); |
| 141 | |
| 142 | case nonloc::SymbolValKind: { |
| 143 | nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond); |
| 144 | SymbolRef sym = SV.getSymbol(); |
| 145 | QualType T = SymMgr.getType(sym); |
| 146 | |
| 147 | if (Assumption) |
| 148 | return AssumeSymNE(St, sym, BasicVals.getValue(0, T), isFeasible); |
| 149 | else |
| 150 | return AssumeSymEQ(St, sym, BasicVals.getValue(0, T), isFeasible); |
| 151 | } |
| 152 | |
| 153 | case nonloc::SymIntConstraintValKind: |
| 154 | return |
| 155 | AssumeSymInt(St, Assumption, |
| 156 | cast<nonloc::SymIntConstraintVal>(Cond).getConstraint(), |
| 157 | isFeasible); |
| 158 | |
| 159 | case nonloc::ConcreteIntKind: { |
| 160 | bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0; |
| 161 | isFeasible = b ? Assumption : !Assumption; |
| 162 | return St; |
| 163 | } |
| 164 | |
| 165 | case nonloc::LocAsIntegerKind: |
| 166 | return AssumeAux(St, cast<nonloc::LocAsInteger>(Cond).getLoc(), |
| 167 | Assumption, isFeasible); |
| 168 | } // end switch |
| 169 | } |
| 170 | |
| 171 | const GRState* |
| 172 | SimpleConstraintManager::AssumeSymInt(const GRState* St, bool Assumption, |
| 173 | const SymIntConstraint& C, |
| 174 | bool& isFeasible) { |
| 175 | |
| 176 | switch (C.getOpcode()) { |
| 177 | default: |
| 178 | // No logic yet for other operators. |
| 179 | isFeasible = true; |
| 180 | return St; |
| 181 | |
| 182 | case BinaryOperator::EQ: |
| 183 | if (Assumption) |
| 184 | return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible); |
| 185 | else |
| 186 | return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 187 | |
| 188 | case BinaryOperator::NE: |
| 189 | if (Assumption) |
| 190 | return AssumeSymNE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 191 | else |
| 192 | return AssumeSymEQ(St, C.getSymbol(), C.getInt(), isFeasible); |
| 193 | |
| 194 | case BinaryOperator::GT: |
| 195 | if (Assumption) |
| 196 | return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible); |
| 197 | else |
| 198 | return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 199 | |
| 200 | case BinaryOperator::GE: |
| 201 | if (Assumption) |
| 202 | return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 203 | else |
| 204 | return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible); |
| 205 | |
| 206 | case BinaryOperator::LT: |
| 207 | if (Assumption) |
| 208 | return AssumeSymLT(St, C.getSymbol(), C.getInt(), isFeasible); |
| 209 | else |
| 210 | return AssumeSymGE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 211 | |
| 212 | case BinaryOperator::LE: |
| 213 | if (Assumption) |
| 214 | return AssumeSymLE(St, C.getSymbol(), C.getInt(), isFeasible); |
| 215 | else |
| 216 | return AssumeSymGT(St, C.getSymbol(), C.getInt(), isFeasible); |
| 217 | } // end switch |
| 218 | } |
| 219 | |
| 220 | const GRState* |
| 221 | SimpleConstraintManager::AssumeInBound(const GRState* St, SVal Idx, |
| 222 | SVal UpperBound, bool Assumption, |
| 223 | bool& isFeasible) { |
| 224 | // Only support ConcreteInt for now. |
| 225 | if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound))){ |
| 226 | isFeasible = true; |
| 227 | return St; |
| 228 | } |
| 229 | |
| 230 | const llvm::APSInt& Zero = getBasicVals().getZeroWithPtrWidth(false); |
| 231 | llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue(); |
| 232 | // IdxV might be too narrow. |
| 233 | if (IdxV.getBitWidth() < Zero.getBitWidth()) |
| 234 | IdxV.extend(Zero.getBitWidth()); |
| 235 | // UBV might be too narrow, too. |
| 236 | llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue(); |
| 237 | if (UBV.getBitWidth() < Zero.getBitWidth()) |
| 238 | UBV.extend(Zero.getBitWidth()); |
| 239 | |
| 240 | bool InBound = (Zero <= IdxV) && (IdxV < UBV); |
| 241 | |
| 242 | isFeasible = Assumption ? InBound : !InBound; |
| 243 | |
| 244 | return St; |
| 245 | } |
| 246 | |
| 247 | } // end of namespace clang |