lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp

   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/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
  17 #include "clang/StaticAnalyzer/Core/PathSensitive/GRState.h"
  18 #include "clang/StaticAnalyzer/Core/PathSensitive/Checker.h"
  19
  20 namespace clang {
  21
  22 namespace ento {
  23
  24 SimpleConstraintManager::~SimpleConstraintManager() {}
  25
  26 bool SimpleConstraintManager::canReasonAbout(SVal X) const {
  27   if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) {
  28     const SymExpr *SE = SymVal->getSymbolicExpression();
  29
  30     if (isa<SymbolData>(SE))
  31       return true;
  32
  33     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
  34       switch (SIE->getOpcode()) {
  35           // We don't reason yet about bitwise-constraints on symbolic values.
  36         case BO_And:
  37         case BO_Or:
  38         case BO_Xor:
  39           return false;
  40         // We don't reason yet about these arithmetic constraints on
  41         // symbolic values.
  42         case BO_Mul:
  43         case BO_Div:
  44         case BO_Rem:
  45         case BO_Shl:
  46         case BO_Shr:
  47           return false;
  48         // All other cases.
  49         default:
  50           return true;
  51       }
  52     }
  53
  54     return false;
  55   }
  56
  57   return true;
  58 }
  59
  60 const GRState *SimpleConstraintManager::assume(const GRState *state,
  61                                                DefinedSVal Cond,
  62                                                bool Assumption) {
  63   if (isa<NonLoc>(Cond))
  64     return assume(state, cast<NonLoc>(Cond), Assumption);
  65   else
  66     return assume(state, cast<Loc>(Cond), Assumption);
  67 }
  68
  69 const GRState *SimpleConstraintManager::assume(const GRState *state, Loc cond,
  70                                                bool assumption) {
  71   state = assumeAux(state, cond, assumption);
  72   return SU.processAssume(state, cond, assumption);
  73 }
  74
  75 const GRState *SimpleConstraintManager::assumeAux(const GRState *state,
  76                                                   Loc Cond, bool Assumption) {
  77
  78   BasicValueFactory &BasicVals = state->getBasicVals();
  79
  80   switch (Cond.getSubKind()) {
  81   default:
  82     assert (false && "'Assume' not implemented for this Loc.");
  83     return state;
  84
  85   case loc::MemRegionKind: {
  86     // FIXME: Should this go into the storemanager?
  87
  88     const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion();
  89     const SubRegion *SubR = dyn_cast<SubRegion>(R);
  90
  91     while (SubR) {
  92       // FIXME: now we only find the first symbolic region.
  93       if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
  94         const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth();
  95         if (Assumption)
  96           return assumeSymNE(state, SymR->getSymbol(), zero, zero);
  97         else
  98           return assumeSymEQ(state, SymR->getSymbol(), zero, zero);
  99       }
 100       SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
 101     }
 102
 103     // FALL-THROUGH.
 104   }
 105
 106   case loc::GotoLabelKind:
 107     return Assumption ? state : NULL;
 108
 109   case loc::ConcreteIntKind: {
 110     bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
 111     bool isFeasible = b ? Assumption : !Assumption;
 112     return isFeasible ? state : NULL;
 113   }
 114   } // end switch
 115 }
 116
 117 const GRState *SimpleConstraintManager::assume(const GRState *state,
 118                                                NonLoc cond,
 119                                                bool assumption) {
 120   state = assumeAux(state, cond, assumption);
 121   return SU.processAssume(state, cond, assumption);
 122 }
 123
 124 static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
 125   // FIXME: This should probably be part of BinaryOperator, since this isn't
 126   // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.)
 127   switch (op) {
 128   default:
 129     assert(false && "Invalid opcode.");
 130   case BO_LT: return BO_GE;
 131   case BO_GT: return BO_LE;
 132   case BO_LE: return BO_GT;
 133   case BO_GE: return BO_LT;
 134   case BO_EQ: return BO_NE;
 135   case BO_NE: return BO_EQ;
 136   }
 137 }
 138
 139 const GRState *SimpleConstraintManager::assumeAux(const GRState *state,
 140                                                   NonLoc Cond,
 141                                                   bool Assumption) {
 142
 143   // We cannot reason about SymSymExprs,
 144   // and can only reason about some SymIntExprs.
 145   if (!canReasonAbout(Cond)) {
 146     // Just return the current state indicating that the path is feasible.
 147     // This may be an over-approximation of what is possible.
 148     return state;
 149   }
 150
 151   BasicValueFactory &BasicVals = state->getBasicVals();
 152   SymbolManager &SymMgr = state->getSymbolManager();
 153
 154   switch (Cond.getSubKind()) {
 155   default:
 156     assert(false && "'Assume' not implemented for this NonLoc");
 157
 158   case nonloc::SymbolValKind: {
 159     nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
 160     SymbolRef sym = SV.getSymbol();
 161     QualType T =  SymMgr.getType(sym);
 162     const llvm::APSInt &zero = BasicVals.getValue(0, T);
 163     if (Assumption)
 164       return assumeSymNE(state, sym, zero, zero);
 165     else
 166       return assumeSymEQ(state, sym, zero, zero);
 167   }
 168
 169   case nonloc::SymExprValKind: {
 170     nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
 171
 172     // For now, we only handle expressions whose RHS is an integer.
 173     // All other expressions are assumed to be feasible.
 174     const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression());
 175     if (!SE)
 176       return state;
 177
 178     BinaryOperator::Opcode op = SE->getOpcode();
 179     // Implicitly compare non-comparison expressions to 0.
 180     if (!BinaryOperator::isComparisonOp(op)) {
 181       QualType T = SymMgr.getType(SE);
 182       const llvm::APSInt &zero = BasicVals.getValue(0, T);
 183       op = (Assumption ? BO_NE : BO_EQ);
 184       return assumeSymRel(state, SE, op, zero);
 185     }
 186
 187     // From here on out, op is the real comparison we'll be testing.
 188     if (!Assumption)
 189       op = NegateComparison(op);
 190
 191     return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
 192   }
 193
 194   case nonloc::ConcreteIntKind: {
 195     bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
 196     bool isFeasible = b ? Assumption : !Assumption;
 197     return isFeasible ? state : NULL;
 198   }
 199
 200   case nonloc::LocAsIntegerKind:
 201     return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
 202                      Assumption);
 203   } // end switch
 204 }
 205
 206 const GRState *SimpleConstraintManager::assumeSymRel(const GRState *state,
 207                                                      const SymExpr *LHS,
 208                                                      BinaryOperator::Opcode op,
 209                                                      const llvm::APSInt& Int) {
 210   assert(BinaryOperator::isComparisonOp(op) &&
 211          "Non-comparison ops should be rewritten as comparisons to zero.");
 212
 213    // We only handle simple comparisons of the form "$sym == constant"
 214    // or "($sym+constant1) == constant2".
 215    // The adjustment is "constant1" in the above expression. It's used to
 216    // "slide" the solution range around for modular arithmetic. For example,
 217    // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
 218    // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
 219    // the subclasses of SimpleConstraintManager to handle the adjustment.
 220    llvm::APSInt Adjustment;
 221
 222   // First check if the LHS is a simple symbol reference.
 223   SymbolRef Sym = dyn_cast<SymbolData>(LHS);
 224   if (Sym) {
 225     Adjustment = 0;
 226   } else {
 227     // Next, see if it's a "($sym+constant1)" expression.
 228     const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
 229
 230     // We don't handle "($sym1+$sym2)".
 231     // Give up and assume the constraint is feasible.
 232     if (!SE)
 233       return state;
 234
 235     // We don't handle "(<expr>+constant1)".
 236     // Give up and assume the constraint is feasible.
 237     Sym = dyn_cast<SymbolData>(SE->getLHS());
 238     if (!Sym)
 239       return state;
 240
 241     // Get the constant out of the expression "($sym+constant1)".
 242     switch (SE->getOpcode()) {
 243     case BO_Add:
 244       Adjustment = SE->getRHS();
 245       break;
 246     case BO_Sub:
 247       Adjustment = -SE->getRHS();
 248       break;
 249     default:
 250       // We don't handle non-additive operators.
 251       // Give up and assume the constraint is feasible.
 252       return state;
 253     }
 254   }
 255
 256   // FIXME: This next section is a hack. It silently converts the integers to
 257   // be of the same type as the symbol, which is not always correct. Really the
 258   // comparisons should be performed using the Int's type, then mapped back to
 259   // the symbol's range of values.
 260   GRStateManager &StateMgr = state->getStateManager();
 261   ASTContext &Ctx = StateMgr.getContext();
 262
 263   QualType T = Sym->getType(Ctx);
 264   assert(T->isIntegerType() || Loc::isLocType(T));
 265   unsigned bitwidth = Ctx.getTypeSize(T);
 266   bool isSymUnsigned = T->isUnsignedIntegerType() || Loc::isLocType(T);
 267
 268   // Convert the adjustment.
 269   Adjustment.setIsUnsigned(isSymUnsigned);
 270   Adjustment = Adjustment.extOrTrunc(bitwidth);
 271
 272   // Convert the right-hand side integer.
 273   llvm::APSInt ConvertedInt(Int, isSymUnsigned);
 274   ConvertedInt = ConvertedInt.extOrTrunc(bitwidth);
 275
 276   switch (op) {
 277   default:
 278     // No logic yet for other operators.  assume the constraint is feasible.
 279     return state;
 280
 281   case BO_EQ:
 282     return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);
 283
 284   case BO_NE:
 285     return assumeSymNE(state, Sym, ConvertedInt, Adjustment);
 286
 287   case BO_GT:
 288     return assumeSymGT(state, Sym, ConvertedInt, Adjustment);
 289
 290   case BO_GE:
 291     return assumeSymGE(state, Sym, ConvertedInt, Adjustment);
 292
 293   case BO_LT:
 294     return assumeSymLT(state, Sym, ConvertedInt, Adjustment);
 295
 296   case BO_LE:
 297     return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
 298   } // end switch
 299 }
 300
 301 } // end of namespace ento
 302
 303 } // end of namespace clang