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