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/APSIntType.h"
  17 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
  18 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
  19
  20 namespace clang {
  21
  22 namespace ento {
  23
  24 SimpleConstraintManager::~SimpleConstraintManager() {}
  25
  26 bool SimpleConstraintManager::canReasonAbout(SVal X) const {
  27   nonloc::SymbolVal *SymVal = dyn_cast<nonloc::SymbolVal>(&X);
  28   if (SymVal && SymVal->isExpression()) {
  29     const SymExpr *SE = SymVal->getSymbol();
  30
  31     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
  32       switch (SIE->getOpcode()) {
  33           // We don't reason yet about bitwise-constraints on symbolic values.
  34         case BO_And:
  35         case BO_Or:
  36         case BO_Xor:
  37           return false;
  38         // We don't reason yet about these arithmetic constraints on
  39         // symbolic values.
  40         case BO_Mul:
  41         case BO_Div:
  42         case BO_Rem:
  43         case BO_Shl:
  44         case BO_Shr:
  45           return false;
  46         // All other cases.
  47         default:
  48           return true;
  49       }
  50     }
  51
  52     return false;
  53   }
  54
  55   return true;
  56 }
  57
  58 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
  59                                                DefinedSVal Cond,
  60                                                bool Assumption) {
  61   if (isa<NonLoc>(Cond))
  62     return assume(state, cast<NonLoc>(Cond), Assumption);
  63   else
  64     return assume(state, cast<Loc>(Cond), Assumption);
  65 }
  66
  67 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond,
  68                                                bool assumption) {
  69   state = assumeAux(state, cond, assumption);
  70   if (NotifyAssumeClients && SU)
  71     return SU->processAssume(state, cond, assumption);
  72   return state;
  73 }
  74
  75 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
  76                                                   Loc Cond, bool Assumption) {
  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 = getBasicVals().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   if (NotifyAssumeClients && SU)
 119     return SU->processAssume(state, cond, assumption);
 120   return state;
 121 }
 122
 123 static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
 124   // FIXME: This should probably be part of BinaryOperator, since this isn't
 125   // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.)
 126   switch (op) {
 127   default:
 128     llvm_unreachable("Invalid opcode.");
 129   case BO_LT: return BO_GE;
 130   case BO_GT: return BO_LE;
 131   case BO_LE: return BO_GT;
 132   case BO_GE: return BO_LT;
 133   case BO_EQ: return BO_NE;
 134   case BO_NE: return BO_EQ;
 135   }
 136 }
 137
 138
 139 ProgramStateRef
 140 SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
 141                                             SymbolRef Sym, bool Assumption) {
 142   BasicValueFactory &BVF = getBasicVals();
 143   QualType T = Sym->getType();
 144
 145   // None of the constraint solvers currently support non-integer types.
 146   if (!T->isIntegerType())
 147     return State;
 148
 149   const llvm::APSInt &zero = BVF.getValue(0, T);
 150   if (Assumption)
 151     return assumeSymNE(State, Sym, zero, zero);
 152   else
 153     return assumeSymEQ(State, Sym, zero, zero);
 154 }
 155
 156 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
 157                                                   NonLoc Cond,
 158                                                   bool Assumption) {
 159
 160   // We cannot reason about SymSymExprs, and can only reason about some
 161   // SymIntExprs.
 162   if (!canReasonAbout(Cond)) {
 163     // Just add the constraint to the expression without trying to simplify.
 164     SymbolRef sym = Cond.getAsSymExpr();
 165     return assumeAuxForSymbol(state, sym, Assumption);
 166   }
 167
 168   BasicValueFactory &BasicVals = getBasicVals();
 169
 170   switch (Cond.getSubKind()) {
 171   default:
 172     llvm_unreachable("'Assume' not implemented for this NonLoc");
 173
 174   case nonloc::SymbolValKind: {
 175     nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
 176     SymbolRef sym = SV.getSymbol();
 177     assert(sym);
 178
 179     // Handle SymbolData.
 180     if (!SV.isExpression()) {
 181       return assumeAuxForSymbol(state, sym, Assumption);
 182
 183     // Handle symbolic expression.
 184     } else {
 185       // We can only simplify expressions whose RHS is an integer.
 186       const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
 187       if (!SE)
 188         return assumeAuxForSymbol(state, sym, Assumption);
 189
 190       BinaryOperator::Opcode op = SE->getOpcode();
 191       // Implicitly compare non-comparison expressions to 0.
 192       if (!BinaryOperator::isComparisonOp(op)) {
 193         QualType T = SE->getType();
 194         const llvm::APSInt &zero = BasicVals.getValue(0, T);
 195         op = (Assumption ? BO_NE : BO_EQ);
 196         return assumeSymRel(state, SE, op, zero);
 197       }
 198       // From here on out, op is the real comparison we'll be testing.
 199       if (!Assumption)
 200         op = NegateComparison(op);
 201
 202       return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
 203     }
 204   }
 205
 206   case nonloc::ConcreteIntKind: {
 207     bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
 208     bool isFeasible = b ? Assumption : !Assumption;
 209     return isFeasible ? state : NULL;
 210   }
 211
 212   case nonloc::LocAsIntegerKind:
 213     return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
 214                      Assumption);
 215   } // end switch
 216 }
 217
 218 static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
 219   // Is it a "($sym+constant1)" expression?
 220   if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
 221     BinaryOperator::Opcode Op = SE->getOpcode();
 222     if (Op == BO_Add || Op == BO_Sub) {
 223       Sym = SE->getLHS();
 224       Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
 225
 226       // Don't forget to negate the adjustment if it's being subtracted.
 227       // This should happen /after/ promotion, in case the value being
 228       // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
 229       if (Op == BO_Sub)
 230         Adjustment = -Adjustment;
 231     }
 232   }
 233 }
 234
 235 ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state,
 236                                                      const SymExpr *LHS,
 237                                                      BinaryOperator::Opcode op,
 238                                                      const llvm::APSInt& Int) {
 239   assert(BinaryOperator::isComparisonOp(op) &&
 240          "Non-comparison ops should be rewritten as comparisons to zero.");
 241
 242   // Get the type used for calculating wraparound.
 243   BasicValueFactory &BVF = getBasicVals();
 244   APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
 245
 246   // We only handle simple comparisons of the form "$sym == constant"
 247   // or "($sym+constant1) == constant2".
 248   // The adjustment is "constant1" in the above expression. It's used to
 249   // "slide" the solution range around for modular arithmetic. For example,
 250   // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
 251   // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
 252   // the subclasses of SimpleConstraintManager to handle the adjustment.
 253   SymbolRef Sym = LHS;
 254   llvm::APSInt Adjustment = WraparoundType.getZeroValue();
 255   computeAdjustment(Sym, Adjustment);
 256
 257   // Convert the right-hand side integer as necessary.
 258   APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
 259   llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
 260
 261   switch (op) {
 262   default:
 263     // No logic yet for other operators.  assume the constraint is feasible.
 264     return state;
 265
 266   case BO_EQ:
 267     return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);
 268
 269   case BO_NE:
 270     return assumeSymNE(state, Sym, ConvertedInt, Adjustment);
 271
 272   case BO_GT:
 273     return assumeSymGT(state, Sym, ConvertedInt, Adjustment);
 274
 275   case BO_GE:
 276     return assumeSymGE(state, Sym, ConvertedInt, Adjustment);
 277
 278   case BO_LT:
 279     return assumeSymLT(state, Sym, ConvertedInt, Adjustment);
 280
 281   case BO_LE:
 282     return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
 283   } // end switch
 284 }
 285
 286 } // end of namespace ento
 287
 288 } // end of namespace clang