lib/Checker/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/Checker/PathSensitive/GRExprEngine.h"
  17 #include "clang/Checker/PathSensitive/GRState.h"
  18 #include "clang/Checker/PathSensitive/Checker.h"
  19
  20 namespace clang {
  21
  22 SimpleConstraintManager::~SimpleConstraintManager() {}
  23
  24 bool SimpleConstraintManager::canReasonAbout(SVal X) const {
  25   if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) {
  26     const SymExpr *SE = SymVal->getSymbolicExpression();
  27
  28     if (isa<SymbolData>(SE))
  29       return true;
  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 BinaryOperator::And:
  35         case BinaryOperator::Or:
  36         case BinaryOperator::Xor:
  37           return false;
  38         // We don't reason yet about arithmetic constraints on symbolic values.
  39         case BinaryOperator::Mul:
  40         case BinaryOperator::Div:
  41         case BinaryOperator::Rem:
  42         case BinaryOperator::Add:
  43         case BinaryOperator::Sub:
  44         case BinaryOperator::Shl:
  45         case BinaryOperator::Shr:
  46           return false;
  47         // All other cases.
  48         default:
  49           return true;
  50       }
  51     }
  52
  53     return false;
  54   }
  55
  56   return true;
  57 }
  58
  59 const GRState *SimpleConstraintManager::Assume(const GRState *state,
  60                                                DefinedSVal Cond,
  61                                                bool Assumption) {
  62   if (isa<NonLoc>(Cond))
  63     return Assume(state, cast<NonLoc>(Cond), Assumption);
  64   else
  65     return Assume(state, cast<Loc>(Cond), Assumption);
  66 }
  67
  68 const GRState *SimpleConstraintManager::Assume(const GRState *state, Loc cond,
  69                                                bool assumption) {
  70   state = AssumeAux(state, cond, assumption);
  71   return SU.ProcessAssume(state, cond, assumption);
  72 }
  73
  74 const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
  75                                                   Loc Cond, bool Assumption) {
  76
  77   BasicValueFactory &BasicVals = state->getBasicVals();
  78
  79   switch (Cond.getSubKind()) {
  80   default:
  81     assert (false && "'Assume' not implemented for this Loc.");
  82     return state;
  83
  84   case loc::MemRegionKind: {
  85     // FIXME: Should this go into the storemanager?
  86
  87     const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion();
  88     const SubRegion *SubR = dyn_cast<SubRegion>(R);
  89
  90     while (SubR) {
  91       // FIXME: now we only find the first symbolic region.
  92       if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
  93         if (Assumption)
  94           return AssumeSymNE(state, SymR->getSymbol(),
  95                              BasicVals.getZeroWithPtrWidth());
  96         else
  97           return AssumeSymEQ(state, SymR->getSymbol(),
  98                              BasicVals.getZeroWithPtrWidth());
  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 const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
 125                                                   NonLoc Cond,
 126                                                   bool Assumption) {
 127
 128   // We cannot reason about SymIntExpr and SymSymExpr.
 129   if (!canReasonAbout(Cond)) {
 130     // Just return the current state indicating that the path is feasible.
 131     // This may be an over-approximation of what is possible.
 132     return state;
 133   }
 134
 135   BasicValueFactory &BasicVals = state->getBasicVals();
 136   SymbolManager &SymMgr = state->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     const llvm::APSInt &zero = BasicVals.getValue(0, T);
 147
 148     return Assumption ? AssumeSymNE(state, sym, zero)
 149                       : AssumeSymEQ(state, sym, zero);
 150   }
 151
 152   case nonloc::SymExprValKind: {
 153     nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
 154     if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression())){
 155       // FIXME: This is a hack.  It silently converts the RHS integer to be
 156       // of the same type as on the left side.  This should be removed once
 157       // we support truncation/extension of symbolic values.
 158       GRStateManager &StateMgr = state->getStateManager();
 159       ASTContext &Ctx = StateMgr.getContext();
 160       QualType LHSType = SE->getLHS()->getType(Ctx);
 161       BasicValueFactory &BasicVals = StateMgr.getBasicVals();
 162       const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS());
 163       SymIntExpr SENew(SE->getLHS(), SE->getOpcode(), RHS, SE->getType(Ctx));
 164
 165       return AssumeSymInt(state, Assumption, &SENew);
 166     }
 167
 168     // For all other symbolic expressions, over-approximate and consider
 169     // the constraint feasible.
 170     return state;
 171   }
 172
 173   case nonloc::ConcreteIntKind: {
 174     bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
 175     bool isFeasible = b ? Assumption : !Assumption;
 176     return isFeasible ? state : NULL;
 177   }
 178
 179   case nonloc::LocAsIntegerKind:
 180     return AssumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
 181                      Assumption);
 182   } // end switch
 183 }
 184
 185 const GRState *SimpleConstraintManager::AssumeSymInt(const GRState *state,
 186                                                      bool Assumption,
 187                                                      const SymIntExpr *SE) {
 188
 189
 190   // Here we assume that LHS is a symbol.  This is consistent with the
 191   // rest of the constraint manager logic.
 192   SymbolRef Sym = cast<SymbolData>(SE->getLHS());
 193   const llvm::APSInt &Int = SE->getRHS();
 194
 195   switch (SE->getOpcode()) {
 196   default:
 197     // No logic yet for other operators.  Assume the constraint is feasible.
 198     return state;
 199
 200   case BinaryOperator::EQ:
 201     return Assumption ? AssumeSymEQ(state, Sym, Int)
 202                       : AssumeSymNE(state, Sym, Int);
 203
 204   case BinaryOperator::NE:
 205     return Assumption ? AssumeSymNE(state, Sym, Int)
 206                       : AssumeSymEQ(state, Sym, Int);
 207   case BinaryOperator::GT:
 208     return Assumption ? AssumeSymGT(state, Sym, Int)
 209                       : AssumeSymLE(state, Sym, Int);
 210
 211   case BinaryOperator::GE:
 212     return Assumption ? AssumeSymGE(state, Sym, Int)
 213                       : AssumeSymLT(state, Sym, Int);
 214
 215   case BinaryOperator::LT:
 216     return Assumption ? AssumeSymLT(state, Sym, Int)
 217                       : AssumeSymGE(state, Sym, Int);
 218
 219   case BinaryOperator::LE:
 220     return Assumption ? AssumeSymLE(state, Sym, Int)
 221                       : AssumeSymGT(state, Sym, Int);
 222   } // end switch
 223 }
 224
 225 const GRState *SimpleConstraintManager::AssumeInBound(const GRState *state,
 226                                                       DefinedSVal Idx,
 227                                                       DefinedSVal UpperBound,
 228                                                       bool Assumption) {
 229
 230   // Only support ConcreteInt for now.
 231   if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound)))
 232     return state;
 233
 234   const llvm::APSInt& Zero = state->getBasicVals().getZeroWithPtrWidth(false);
 235   llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue();
 236   // IdxV might be too narrow.
 237   if (IdxV.getBitWidth() < Zero.getBitWidth())
 238     IdxV.extend(Zero.getBitWidth());
 239   // UBV might be too narrow, too.
 240   llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue();
 241   if (UBV.getBitWidth() < Zero.getBitWidth())
 242     UBV.extend(Zero.getBitWidth());
 243
 244   bool InBound = (Zero <= IdxV) && (IdxV < UBV);
 245   bool isFeasible = Assumption ? InBound : !InBound;
 246   return isFeasible ? state : NULL;
 247 }
 248
 249 }  // end of namespace clang