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