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   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)
     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   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
    138 SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
    139                                             SymbolRef Sym, bool Assumption) {
    140   BasicValueFactory &BVF = getBasicVals();
    141   QualType T = Sym->getType(BVF.getContext());
    142 
    143   // None of the constraint solvers currently support non-integer types.
    144   if (!T->isIntegerType())
    145     return State;
    146 
    147   const llvm::APSInt &zero = BVF.getValue(0, T);
    148   if (Assumption)
    149     return assumeSymNE(State, Sym, zero, zero);
    150   else
    151     return assumeSymEQ(State, Sym, zero, zero);
    152 }
    153 
    154 ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
    155                                                   NonLoc Cond,
    156                                                   bool Assumption) {
    157 
    158   // We cannot reason about SymSymExprs, and can only reason about some
    159   // SymIntExprs.
    160   if (!canReasonAbout(Cond)) {
    161     // Just add the constraint to the expression without trying to simplify.
    162     SymbolRef sym = Cond.getAsSymExpr();
    163     return assumeAuxForSymbol(state, sym, Assumption);
    164   }
    165 
    166   BasicValueFactory &BasicVals = getBasicVals();
    167 
    168   switch (Cond.getSubKind()) {
    169   default:
    170     llvm_unreachable("'Assume' not implemented for this NonLoc");
    171 
    172   case nonloc::SymbolValKind: {
    173     nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
    174     SymbolRef sym = SV.getSymbol();
    175     assert(sym);
    176 
    177     // Handle SymbolData.
    178     if (!SV.isExpression()) {
    179       return assumeAuxForSymbol(state, sym, Assumption);
    180 
    181     // Handle symbolic expression.
    182     } else {
    183       // We can only simplify expressions whose RHS is an integer.
    184       const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
    185       if (!SE)
    186         return assumeAuxForSymbol(state, sym, Assumption);
    187 
    188       BinaryOperator::Opcode op = SE->getOpcode();
    189       // Implicitly compare non-comparison expressions to 0.
    190       if (!BinaryOperator::isComparisonOp(op)) {
    191         QualType T = SE->getType(BasicVals.getContext());
    192         const llvm::APSInt &zero = BasicVals.getValue(0, T);
    193         op = (Assumption ? BO_NE : BO_EQ);
    194         return assumeSymRel(state, SE, op, zero);
    195       }
    196       // From here on out, op is the real comparison we'll be testing.
    197       if (!Assumption)
    198         op = NegateComparison(op);
    199 
    200       return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
    201     }
    202   }
    203 
    204   case nonloc::ConcreteIntKind: {
    205     bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
    206     bool isFeasible = b ? Assumption : !Assumption;
    207     return isFeasible ? state : NULL;
    208   }
    209 
    210   case nonloc::LocAsIntegerKind:
    211     return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
    212                      Assumption);
    213   } // end switch
    214 }
    215 
    216 static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
    217   // Is it a "($sym+constant1)" expression?
    218   if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
    219     BinaryOperator::Opcode Op = SE->getOpcode();
    220     if (Op == BO_Add || Op == BO_Sub) {
    221       Sym = SE->getLHS();
    222       Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
    223 
    224       // Don't forget to negate the adjustment if it's being subtracted.
    225       // This should happen /after/ promotion, in case the value being
    226       // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
    227       if (Op == BO_Sub)
    228         Adjustment = -Adjustment;
    229     }
    230   }
    231 }
    232 
    233 ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state,
    234                                                      const SymExpr *LHS,
    235                                                      BinaryOperator::Opcode op,
    236                                                      const llvm::APSInt& Int) {
    237   assert(BinaryOperator::isComparisonOp(op) &&
    238          "Non-comparison ops should be rewritten as comparisons to zero.");
    239 
    240   BasicValueFactory &BVF = getBasicVals();
    241   ASTContext &Ctx = BVF.getContext();
    242 
    243   // Get the type used for calculating wraparound.
    244   APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType(Ctx));
    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
    289