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