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