SimpleConstraintManager.cpp revision 76462f00854171d2aa3ebc34f9aac1c60021b0ea 
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/ProgramState.h"
18
19namespace clang {
20
21namespace ento {
22
23SimpleConstraintManager::~SimpleConstraintManager() {}
24
25bool SimpleConstraintManager::canReasonAbout(SVal X) const {
26  if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) {
27    const SymExpr *SE = SymVal->getSymbolicExpression();
28
29    if (isa<SymbolData>(SE))
30      return true;
31
32    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
33      switch (SIE->getOpcode()) {
34          // We don't reason yet about bitwise-constraints on symbolic values.
35        case BO_And:
36        case BO_Or:
37        case BO_Xor:
38          return false;
39        // We don't reason yet about these arithmetic constraints on
40        // symbolic values.
41        case BO_Mul:
42        case BO_Div:
43        case BO_Rem:
44        case BO_Shl:
45        case BO_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
59const ProgramState *SimpleConstraintManager::assume(const ProgramState *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
68const ProgramState *SimpleConstraintManager::assume(const ProgramState *state, Loc cond,
69                                               bool assumption) {
70  state = assumeAux(state, cond, assumption);
71  return SU.processAssume(state, cond, assumption);
72}
73
74const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *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        const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth();
94        if (Assumption)
95          return assumeSymNE(state, SymR->getSymbol(), zero, zero);
96        else
97          return assumeSymEQ(state, SymR->getSymbol(), zero, zero);
98      }
99      SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
100    }
101
102    // FALL-THROUGH.
103  }
104
105  case loc::GotoLabelKind:
106    return Assumption ? state : NULL;
107
108  case loc::ConcreteIntKind: {
109    bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
110    bool isFeasible = b ? Assumption : !Assumption;
111    return isFeasible ? state : NULL;
112  }
113  } // end switch
114}
115
116const ProgramState *SimpleConstraintManager::assume(const ProgramState *state,
117                                               NonLoc cond,
118                                               bool assumption) {
119  state = assumeAux(state, cond, assumption);
120  return SU.processAssume(state, cond, assumption);
121}
122
123static 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
139const ProgramState *SimpleConstraintManager::assumeAuxForSymbol(
140                                              const ProgramState *State,
141                                              SymbolRef Sym,
142                                              bool Assumption) {
143  QualType T =  State->getSymbolManager().getType(Sym);
144  const llvm::APSInt &zero = State->getBasicVals().getValue(0, T);
145  if (Assumption)
146    return assumeSymNE(State, Sym, zero, zero);
147  else
148    return assumeSymEQ(State, Sym, zero, zero);
149}
150
151const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state,
152                                                  NonLoc Cond,
153                                                  bool Assumption) {
154
155  // We cannot reason about SymSymExprs, and can only reason about some
156  // SymIntExprs.
157  if (!canReasonAbout(Cond)) {
158    // Just add the constraint to the expression without trying to simplify.
159    SymbolRef sym = Cond.getAsSymExpr();
160    return assumeAuxForSymbol(state, sym, Assumption);
161  }
162
163  BasicValueFactory &BasicVals = state->getBasicVals();
164  SymbolManager &SymMgr = state->getSymbolManager();
165
166  switch (Cond.getSubKind()) {
167  default:
168    llvm_unreachable("'Assume' not implemented for this NonLoc");
169
170  case nonloc::SymbolValKind: {
171    nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
172    SymbolRef sym = SV.getSymbol();
173    return assumeAuxForSymbol(state, sym, Assumption);
174  }
175
176  case nonloc::SymExprValKind: {
177    nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
178
179    SymbolRef sym = V.getSymbolicExpression();
180    assert(sym);
181
182    // We can only simplify expressions whose RHS is an integer.
183    const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
184    if (!SE)
185      return assumeAuxForSymbol(state, sym, Assumption);
186
187    BinaryOperator::Opcode op = SE->getOpcode();
188    // Implicitly compare non-comparison expressions to 0.
189    if (!BinaryOperator::isComparisonOp(op)) {
190      QualType T = SymMgr.getType(SE);
191      const llvm::APSInt &zero = BasicVals.getValue(0, T);
192      op = (Assumption ? BO_NE : BO_EQ);
193      return assumeSymRel(state, SE, op, zero);
194    }
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  case nonloc::ConcreteIntKind: {
204    bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
205    bool isFeasible = b ? Assumption : !Assumption;
206    return isFeasible ? state : NULL;
207  }
208
209  case nonloc::LocAsIntegerKind:
210    return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
211                     Assumption);
212  } // end switch
213}
214
215static llvm::APSInt computeAdjustment(const SymExpr *LHS,
216                                      SymbolRef &Sym) {
217  llvm::APSInt DefaultAdjustment;
218  DefaultAdjustment = 0;
219
220  // First check if the LHS is a simple symbol reference.
221  if (isa<SymbolData>(LHS))
222    return DefaultAdjustment;
223
224  // Next, see if it's a "($sym+constant1)" expression.
225  const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
226
227  // We cannot simplify "($sym1+$sym2)".
228  if (!SE)
229    return DefaultAdjustment;
230
231  // Get the constant out of the expression "($sym+constant1)" or
232  // "<expr>+constant1".
233  Sym = SE->getLHS();
234  switch (SE->getOpcode()) {
235  case BO_Add:
236    return SE->getRHS();
237    break;
238  case BO_Sub:
239    return -SE->getRHS();
240    break;
241  default:
242    // We cannot simplify non-additive operators.
243    return DefaultAdjustment;
244  }
245
246  return DefaultAdjustment;
247}
248
249const ProgramState *SimpleConstraintManager::assumeSymRel(const ProgramState *state,
250                                                     const SymExpr *LHS,
251                                                     BinaryOperator::Opcode op,
252                                                     const llvm::APSInt& Int) {
253  assert(BinaryOperator::isComparisonOp(op) &&
254         "Non-comparison ops should be rewritten as comparisons to zero.");
255
256  // We only handle simple comparisons of the form "$sym == constant"
257  // or "($sym+constant1) == constant2".
258  // The adjustment is "constant1" in the above expression. It's used to
259  // "slide" the solution range around for modular arithmetic. For example,
260  // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
261  // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
262  // the subclasses of SimpleConstraintManager to handle the adjustment.
263  SymbolRef Sym = LHS;
264  llvm::APSInt Adjustment = computeAdjustment(LHS, Sym);
265
266  // FIXME: This next section is a hack. It silently converts the integers to
267  // be of the same type as the symbol, which is not always correct. Really the
268  // comparisons should be performed using the Int's type, then mapped back to
269  // the symbol's range of values.
270  ProgramStateManager &StateMgr = state->getStateManager();
271  ASTContext &Ctx = StateMgr.getContext();
272
273  QualType T = Sym->getType(Ctx);
274  assert(T->isIntegerType() || Loc::isLocType(T));
275  unsigned bitwidth = Ctx.getTypeSize(T);
276  bool isSymUnsigned
277    = T->isUnsignedIntegerOrEnumerationType() || Loc::isLocType(T);
278
279  // Convert the adjustment.
280  Adjustment.setIsUnsigned(isSymUnsigned);
281  Adjustment = Adjustment.extOrTrunc(bitwidth);
282
283  // Convert the right-hand side integer.
284  llvm::APSInt ConvertedInt(Int, isSymUnsigned);
285  ConvertedInt = ConvertedInt.extOrTrunc(bitwidth);
286
287  switch (op) {
288  default:
289    // No logic yet for other operators.  assume the constraint is feasible.
290    return state;
291
292  case BO_EQ:
293    return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);
294
295  case BO_NE:
296    return assumeSymNE(state, Sym, ConvertedInt, Adjustment);
297
298  case BO_GT:
299    return assumeSymGT(state, Sym, ConvertedInt, Adjustment);
300
301  case BO_GE:
302    return assumeSymGE(state, Sym, ConvertedInt, Adjustment);
303
304  case BO_LT:
305    return assumeSymLT(state, Sym, ConvertedInt, Adjustment);
306
307  case BO_LE:
308    return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
309  } // end switch
310}
311
312} // end of namespace ento
313
314} // end of namespace clang
315