SimpleConstraintManager.cpp revision 47cbd0f3892c7965cf16a58393f9f17a22d4d4d9 
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  if (NotifyAssumeClients)
71    return SU.processAssume(state, cond, assumption);
72  return state;
73}
74
75ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
76                                                  Loc Cond, bool Assumption) {
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 = getBasicVals().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
138SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
139                                            SymbolRef Sym, bool Assumption) {
140  BasicValueFactory &BVF = getBasicVals();
141  QualType T = Sym->getType(BVF.getContext());
142
143  // None of the constraint solvers currently support non-integer types.
144  if (!T->isIntegerType())
145    return State;
146
147  const llvm::APSInt &zero = BVF.getValue(0, T);
148  if (Assumption)
149    return assumeSymNE(State, Sym, zero, zero);
150  else
151    return assumeSymEQ(State, Sym, zero, zero);
152}
153
154ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
155                                                  NonLoc Cond,
156                                                  bool Assumption) {
157
158  // We cannot reason about SymSymExprs, and can only reason about some
159  // SymIntExprs.
160  if (!canReasonAbout(Cond)) {
161    // Just add the constraint to the expression without trying to simplify.
162    SymbolRef sym = Cond.getAsSymExpr();
163    return assumeAuxForSymbol(state, sym, Assumption);
164  }
165
166  BasicValueFactory &BasicVals = getBasicVals();
167
168  switch (Cond.getSubKind()) {
169  default:
170    llvm_unreachable("'Assume' not implemented for this NonLoc");
171
172  case nonloc::SymbolValKind: {
173    nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
174    SymbolRef sym = SV.getSymbol();
175    assert(sym);
176
177    // Handle SymbolData.
178    if (!SV.isExpression()) {
179      return assumeAuxForSymbol(state, sym, Assumption);
180
181    // Handle symbolic expression.
182    } else {
183      // We can only simplify expressions whose RHS is an integer.
184      const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
185      if (!SE)
186        return assumeAuxForSymbol(state, sym, Assumption);
187
188      BinaryOperator::Opcode op = SE->getOpcode();
189      // Implicitly compare non-comparison expressions to 0.
190      if (!BinaryOperator::isComparisonOp(op)) {
191        QualType T = SE->getType(BasicVals.getContext());
192        const llvm::APSInt &zero = BasicVals.getValue(0, T);
193        op = (Assumption ? BO_NE : BO_EQ);
194        return assumeSymRel(state, SE, op, zero);
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
204  case nonloc::ConcreteIntKind: {
205    bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
206    bool isFeasible = b ? Assumption : !Assumption;
207    return isFeasible ? state : NULL;
208  }
209
210  case nonloc::LocAsIntegerKind:
211    return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
212                     Assumption);
213  } // end switch
214}
215
216static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
217  // Is it a "($sym+constant1)" expression?
218  if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
219    BinaryOperator::Opcode Op = SE->getOpcode();
220    if (Op == BO_Add || Op == BO_Sub) {
221      Sym = SE->getLHS();
222      Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
223
224      // Don't forget to negate the adjustment if it's being subtracted.
225      // This should happen /after/ promotion, in case the value being
226      // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
227      if (Op == BO_Sub)
228        Adjustment = -Adjustment;
229    }
230  }
231}
232
233ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state,
234                                                     const SymExpr *LHS,
235                                                     BinaryOperator::Opcode op,
236                                                     const llvm::APSInt& Int) {
237  assert(BinaryOperator::isComparisonOp(op) &&
238         "Non-comparison ops should be rewritten as comparisons to zero.");
239
240  BasicValueFactory &BVF = getBasicVals();
241  ASTContext &Ctx = BVF.getContext();
242
243  // Get the type used for calculating wraparound.
244  APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType(Ctx));
245
246  // We only handle simple comparisons of the form "$sym == constant"
247  // or "($sym+constant1) == constant2".
248  // The adjustment is "constant1" in the above expression. It's used to
249  // "slide" the solution range around for modular arithmetic. For example,
250  // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
251  // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
252  // the subclasses of SimpleConstraintManager to handle the adjustment.
253  SymbolRef Sym = LHS;
254  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
255  computeAdjustment(Sym, Adjustment);
256
257  // Convert the right-hand side integer as necessary.
258  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
259  llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
260
261  switch (op) {
262  default:
263    // No logic yet for other operators.  assume the constraint is feasible.
264    return state;
265
266  case BO_EQ:
267    return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);
268
269  case BO_NE:
270    return assumeSymNE(state, Sym, ConvertedInt, Adjustment);
271
272  case BO_GT:
273    return assumeSymGT(state, Sym, ConvertedInt, Adjustment);
274
275  case BO_GE:
276    return assumeSymGE(state, Sym, ConvertedInt, Adjustment);
277
278  case BO_LT:
279    return assumeSymLT(state, Sym, ConvertedInt, Adjustment);
280
281  case BO_LE:
282    return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
283  } // end switch
284}
285
286} // end of namespace ento
287
288} // end of namespace clang
289