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