SimpleConstraintManager.cpp revision 78114a58f8cf5e9b948e82448b2f0904f5b6c19e 
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  Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
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    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
53      if (SSE->getOpcode() == BO_EQ || SSE->getOpcode() == BO_NE)
54        return true;
55    }
56
57    return false;
58  }
59
60  return true;
61}
62
63ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
64                                               DefinedSVal Cond,
65                                               bool Assumption) {
66  if (Optional<NonLoc> NV = Cond.getAs<NonLoc>())
67    return assume(state, *NV, Assumption);
68  return assume(state, Cond.castAs<Loc>(), Assumption);
69}
70
71ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond,
72                                               bool assumption) {
73  state = assumeAux(state, cond, assumption);
74  if (NotifyAssumeClients && SU)
75    return SU->processAssume(state, cond, assumption);
76  return state;
77}
78
79ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
80                                                  Loc Cond, bool Assumption) {
81  switch (Cond.getSubKind()) {
82  default:
83    assert (false && "'Assume' not implemented for this Loc.");
84    return state;
85
86  case loc::MemRegionKind: {
87    // FIXME: Should this go into the storemanager?
88
89    const MemRegion *R = Cond.castAs<loc::MemRegionVal>().getRegion();
90    const SubRegion *SubR = dyn_cast<SubRegion>(R);
91
92    while (SubR) {
93      // FIXME: now we only find the first symbolic region.
94      if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
95        const llvm::APSInt &zero = getBasicVals().getZeroWithPtrWidth();
96        if (Assumption)
97          return assumeSymNE(state, SymR->getSymbol(), zero, zero);
98        else
99          return assumeSymEQ(state, SymR->getSymbol(), zero, zero);
100      }
101      SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
102    }
103
104    // FALL-THROUGH.
105  }
106
107  case loc::GotoLabelKind:
108    return Assumption ? state : NULL;
109
110  case loc::ConcreteIntKind: {
111    bool b = Cond.castAs<loc::ConcreteInt>().getValue() != 0;
112    bool isFeasible = b ? Assumption : !Assumption;
113    return isFeasible ? state : NULL;
114  }
115  } // end switch
116}
117
118ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
119                                               NonLoc cond,
120                                               bool assumption) {
121  state = assumeAux(state, cond, assumption);
122  if (NotifyAssumeClients && SU)
123    return SU->processAssume(state, cond, assumption);
124  return state;
125}
126
127static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
128  // FIXME: This should probably be part of BinaryOperator, since this isn't
129  // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.)
130  switch (op) {
131  default:
132    llvm_unreachable("Invalid opcode.");
133  case BO_LT: return BO_GE;
134  case BO_GT: return BO_LE;
135  case BO_LE: return BO_GT;
136  case BO_GE: return BO_LT;
137  case BO_EQ: return BO_NE;
138  case BO_NE: return BO_EQ;
139  }
140}
141
142
143ProgramStateRef
144SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
145                                            SymbolRef Sym, bool Assumption) {
146  BasicValueFactory &BVF = getBasicVals();
147  QualType T = Sym->getType();
148
149  // None of the constraint solvers currently support non-integer types.
150  if (!T->isIntegerType())
151    return State;
152
153  const llvm::APSInt &zero = BVF.getValue(0, T);
154  if (Assumption)
155    return assumeSymNE(State, Sym, zero, zero);
156  else
157    return assumeSymEQ(State, Sym, zero, zero);
158}
159
160ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
161                                                  NonLoc Cond,
162                                                  bool Assumption) {
163
164  // We cannot reason about SymSymExprs, and can only reason about some
165  // SymIntExprs.
166  if (!canReasonAbout(Cond)) {
167    // Just add the constraint to the expression without trying to simplify.
168    SymbolRef sym = Cond.getAsSymExpr();
169    return assumeAuxForSymbol(state, sym, Assumption);
170  }
171
172  switch (Cond.getSubKind()) {
173  default:
174    llvm_unreachable("'Assume' not implemented for this NonLoc");
175
176  case nonloc::SymbolValKind: {
177    nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>();
178    SymbolRef sym = SV.getSymbol();
179    assert(sym);
180
181    // Handle SymbolData.
182    if (!SV.isExpression()) {
183      return assumeAuxForSymbol(state, sym, Assumption);
184
185    // Handle symbolic expression.
186    } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym)) {
187      // We can only simplify expressions whose RHS is an integer.
188
189      BinaryOperator::Opcode op = SE->getOpcode();
190      if (BinaryOperator::isComparisonOp(op)) {
191        if (!Assumption)
192          op = NegateComparison(op);
193
194        return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
195      }
196
197    } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) {
198      BinaryOperator::Opcode Op = SSE->getOpcode();
199
200      // Translate "a != b" to "(b - a) != 0".
201      // We invert the order of the operands as a heuristic for how loop
202      // conditions are usually written ("begin != end") as compared to length
203      // calculations ("end - begin"). The more correct thing to do would be to
204      // canonicalize "a - b" and "b - a", which would allow us to treat
205      // "a != b" and "b != a" the same.
206      if (BinaryOperator::isEqualityOp(Op)) {
207        SymbolManager &SymMgr = getSymbolManager();
208
209        assert(Loc::isLocType(SSE->getLHS()->getType()));
210        assert(Loc::isLocType(SSE->getRHS()->getType()));
211        QualType DiffTy = SymMgr.getContext().getPointerDiffType();
212        SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
213                                                     SSE->getLHS(), DiffTy);
214
215        Assumption ^= (SSE->getOpcode() == BO_EQ);
216        return assumeAuxForSymbol(state, Subtraction, Assumption);
217      }
218    }
219
220    // If we get here, there's nothing else we can do but treat the symbol as
221    // opaque.
222    return assumeAuxForSymbol(state, sym, Assumption);
223  }
224
225  case nonloc::ConcreteIntKind: {
226    bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0;
227    bool isFeasible = b ? Assumption : !Assumption;
228    return isFeasible ? state : NULL;
229  }
230
231  case nonloc::LocAsIntegerKind:
232    return assumeAux(state, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
233                     Assumption);
234  } // end switch
235}
236
237static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
238  // Is it a "($sym+constant1)" expression?
239  if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
240    BinaryOperator::Opcode Op = SE->getOpcode();
241    if (Op == BO_Add || Op == BO_Sub) {
242      Sym = SE->getLHS();
243      Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
244
245      // Don't forget to negate the adjustment if it's being subtracted.
246      // This should happen /after/ promotion, in case the value being
247      // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
248      if (Op == BO_Sub)
249        Adjustment = -Adjustment;
250    }
251  }
252}
253
254ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state,
255                                                     const SymExpr *LHS,
256                                                     BinaryOperator::Opcode op,
257                                                     const llvm::APSInt& Int) {
258  assert(BinaryOperator::isComparisonOp(op) &&
259         "Non-comparison ops should be rewritten as comparisons to zero.");
260
261  // Get the type used for calculating wraparound.
262  BasicValueFactory &BVF = getBasicVals();
263  APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
264
265  // We only handle simple comparisons of the form "$sym == constant"
266  // or "($sym+constant1) == constant2".
267  // The adjustment is "constant1" in the above expression. It's used to
268  // "slide" the solution range around for modular arithmetic. For example,
269  // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
270  // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
271  // the subclasses of SimpleConstraintManager to handle the adjustment.
272  SymbolRef Sym = LHS;
273  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
274  computeAdjustment(Sym, Adjustment);
275
276  // Convert the right-hand side integer as necessary.
277  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
278  llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
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