Home | History | Annotate | Download | only in Core 
      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   Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
     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 (Optional<NonLoc> NV = Cond.getAs<NonLoc>())
     62     return assume(state, *NV, Assumption);
     63   return assume(state, Cond.castAs<Loc>(), Assumption);
     64 }
     65 
     66 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond,
     67                                                bool assumption) {
     68   state = assumeAux(state, cond, assumption);
     69   if (NotifyAssumeClients && SU)
     70     return SU->processAssume(state, cond, assumption);
     71   return state;
     72 }
     73 
     74 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
     75                                                   Loc Cond, bool Assumption) {
     76   switch (Cond.getSubKind()) {
     77   default:
     78     assert (false && "'Assume' not implemented for this Loc.");
     79     return state;
     80 
     81   case loc::MemRegionKind: {
     82     // FIXME: Should this go into the storemanager?
     83 
     84     const MemRegion *R = Cond.castAs<loc::MemRegionVal>().getRegion();
     85     const SubRegion *SubR = dyn_cast<SubRegion>(R);
     86 
     87     while (SubR) {
     88       // FIXME: now we only find the first symbolic region.
     89       if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
     90         const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth();
     91         if (Assumption)
     92           return assumeSymNE(state, SymR->getSymbol(), zero, zero);
     93         else
     94           return assumeSymEQ(state, SymR->getSymbol(), zero, zero);
     95       }
     96       SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
     97     }
     98 
     99     // FALL-THROUGH.
    100   }
    101 
    102   case loc::GotoLabelKind:
    103     return Assumption ? state : NULL;
    104 
    105   case loc::ConcreteIntKind: {
    106     bool b = Cond.castAs<loc::ConcreteInt>().getValue() != 0;
    107     bool isFeasible = b ? Assumption : !Assumption;
    108     return isFeasible ? state : NULL;
    109   }
    110   } // end switch
    111 }
    112 
    113 ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
    114                                                NonLoc cond,
    115                                                bool assumption) {
    116   state = assumeAux(state, cond, assumption);
    117   if (NotifyAssumeClients && SU)
    118     return SU->processAssume(state, cond, assumption);
    119   return state;
    120 }
    121 
    122 static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
    123   // FIXME: This should probably be part of BinaryOperator, since this isn't
    124   // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.)
    125   switch (op) {
    126   default:
    127     llvm_unreachable("Invalid opcode.");
    128   case BO_LT: return BO_GE;
    129   case BO_GT: return BO_LE;
    130   case BO_LE: return BO_GT;
    131   case BO_GE: return BO_LT;
    132   case BO_EQ: return BO_NE;
    133   case BO_NE: return BO_EQ;
    134   }
    135 }
    136 
    137 
    138 ProgramStateRef
    139 SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
    140                                             SymbolRef Sym, bool Assumption) {
    141   BasicValueFactory &BVF = getBasicVals();
    142   QualType T = Sym->getType();
    143 
    144   // None of the constraint solvers currently support non-integer types.
    145   if (!T->isIntegerType())
    146     return State;
    147 
    148   const llvm::APSInt &zero = BVF.getValue(0, T);
    149   if (Assumption)
    150     return assumeSymNE(State, Sym, zero, zero);
    151   else
    152     return assumeSymEQ(State, Sym, zero, zero);
    153 }
    154 
    155 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
    156                                                   NonLoc Cond,
    157                                                   bool Assumption) {
    158 
    159   // We cannot reason about SymSymExprs, and can only reason about some
    160   // SymIntExprs.
    161   if (!canReasonAbout(Cond)) {
    162     // Just add the constraint to the expression without trying to simplify.
    163     SymbolRef sym = Cond.getAsSymExpr();
    164     return assumeAuxForSymbol(state, sym, Assumption);
    165   }
    166 
    167   BasicValueFactory &BasicVals = getBasicVals();
    168 
    169   switch (Cond.getSubKind()) {
    170   default:
    171     llvm_unreachable("'Assume' not implemented for this NonLoc");
    172 
    173   case nonloc::SymbolValKind: {
    174     nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>();
    175     SymbolRef sym = SV.getSymbol();
    176     assert(sym);
    177 
    178     // Handle SymbolData.
    179     if (!SV.isExpression()) {
    180       return assumeAuxForSymbol(state, sym, Assumption);
    181 
    182     // Handle symbolic expression.
    183     } else {
    184       // We can only simplify expressions whose RHS is an integer.
    185       const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
    186       if (!SE)
    187         return assumeAuxForSymbol(state, sym, Assumption);
    188 
    189       BinaryOperator::Opcode op = SE->getOpcode();
    190       // Implicitly compare non-comparison expressions to 0.
    191       if (!BinaryOperator::isComparisonOp(op)) {
    192         QualType T = SE->getType();
    193         const llvm::APSInt &zero = BasicVals.getValue(0, T);
    194         op = (Assumption ? BO_NE : BO_EQ);
    195         return assumeSymRel(state, SE, op, zero);
    196       }
    197       // From here on out, op is the real comparison we'll be testing.
    198       if (!Assumption)
    199         op = NegateComparison(op);
    200 
    201       return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
    202     }
    203   }
    204 
    205   case nonloc::ConcreteIntKind: {
    206     bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0;
    207     bool isFeasible = b ? Assumption : !Assumption;
    208     return isFeasible ? state : NULL;
    209   }
    210 
    211   case nonloc::LocAsIntegerKind:
    212     return assumeAux(state, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
    213                      Assumption);
    214   } // end switch
    215 }
    216 
    217 static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
    218   // Is it a "($sym+constant1)" expression?
    219   if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
    220     BinaryOperator::Opcode Op = SE->getOpcode();
    221     if (Op == BO_Add || Op == BO_Sub) {
    222       Sym = SE->getLHS();
    223       Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
    224 
    225       // Don't forget to negate the adjustment if it's being subtracted.
    226       // This should happen /after/ promotion, in case the value being
    227       // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
    228       if (Op == BO_Sub)
    229         Adjustment = -Adjustment;
    230     }
    231   }
    232 }
    233 
    234 ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state,
    235                                                      const SymExpr *LHS,
    236                                                      BinaryOperator::Opcode op,
    237                                                      const llvm::APSInt& Int) {
    238   assert(BinaryOperator::isComparisonOp(op) &&
    239          "Non-comparison ops should be rewritten as comparisons to zero.");
    240 
    241   // Get the type used for calculating wraparound.
    242   BasicValueFactory &BVF = getBasicVals();
    243   APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
    244 
    245   // We only handle simple comparisons of the form "$sym == constant"
    246   // or "($sym+constant1) == constant2".
    247   // The adjustment is "constant1" in the above expression. It's used to
    248   // "slide" the solution range around for modular arithmetic. For example,
    249   // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
    250   // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
    251   // the subclasses of SimpleConstraintManager to handle the adjustment.
    252   SymbolRef Sym = LHS;
    253   llvm::APSInt Adjustment = WraparoundType.getZeroValue();
    254   computeAdjustment(Sym, Adjustment);
    255 
    256   // Convert the right-hand side integer as necessary.
    257   APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
    258   llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
    259 
    260   switch (op) {
    261   default:
    262     // No logic yet for other operators.  assume the constraint is feasible.
    263     return state;
    264 
    265   case BO_EQ:
    266     return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);
    267 
    268   case BO_NE:
    269     return assumeSymNE(state, Sym, ConvertedInt, Adjustment);
    270 
    271   case BO_GT:
    272     return assumeSymGT(state, Sym, ConvertedInt, Adjustment);
    273 
    274   case BO_GE:
    275     return assumeSymGE(state, Sym, ConvertedInt, Adjustment);
    276 
    277   case BO_LT:
    278     return assumeSymLT(state, Sym, ConvertedInt, Adjustment);
    279 
    280   case BO_LE:
    281     return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
    282   } // end switch
    283 }
    284 
    285 } // end of namespace ento
    286 
    287 } // end of namespace clang
    288