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