SimpleConstraintManager.cpp revision 1eb4433ac451dc16f4133a88af2d002ac26c58ef 
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/Analysis/PathSensitive/GRExprEngine.h"
17#include "clang/Analysis/PathSensitive/GRState.h"
18
19namespace clang {
20
21SimpleConstraintManager::~SimpleConstraintManager() {}
22
23bool SimpleConstraintManager::canReasonAbout(SVal X) const {
24  if (nonloc::SymExprVal *SymVal = dyn_cast<nonloc::SymExprVal>(&X)) {
25    const SymExpr *SE = SymVal->getSymbolicExpression();
26
27    if (isa<SymbolData>(SE))
28      return true;
29
30    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
31      switch (SIE->getOpcode()) {
32          // We don't reason yet about bitwise-constraints on symbolic values.
33        case BinaryOperator::And:
34        case BinaryOperator::Or:
35        case BinaryOperator::Xor:
36          return false;
37        // We don't reason yet about arithmetic constraints on symbolic values.
38        case BinaryOperator::Mul:
39        case BinaryOperator::Div:
40        case BinaryOperator::Rem:
41        case BinaryOperator::Add:
42        case BinaryOperator::Sub:
43        case BinaryOperator::Shl:
44        case BinaryOperator::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
58const GRState *SimpleConstraintManager::Assume(const GRState *state,
59                                               SVal Cond, bool Assumption) {
60  if (Cond.isUnknown()) {
61    return state;
62  }
63
64  if (isa<NonLoc>(Cond))
65    return Assume(state, cast<NonLoc>(Cond), Assumption);
66  else
67    return Assume(state, cast<Loc>(Cond), Assumption);
68}
69
70const GRState *SimpleConstraintManager::Assume(const GRState *state, Loc Cond,
71                                               bool Assumption) {
72
73  state = AssumeAux(state, Cond, Assumption);
74
75  // EvalAssume is used to call into the GRTransferFunction object to perform
76  // any checker-specific update of the state based on this assumption being
77  // true or false.
78  return state ? state->getTransferFuncs().EvalAssume(state, Cond, Assumption)
79               : NULL;
80}
81
82const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
83                                                  Loc Cond, bool Assumption) {
84
85  BasicValueFactory &BasicVals = state->getBasicVals();
86
87  switch (Cond.getSubKind()) {
88  default:
89    assert (false && "'Assume' not implemented for this Loc.");
90    return state;
91
92  case loc::MemRegionKind: {
93    // FIXME: Should this go into the storemanager?
94
95    const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion();
96    const SubRegion *SubR = dyn_cast<SubRegion>(R);
97
98    while (SubR) {
99      // FIXME: now we only find the first symbolic region.
100      if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
101        if (Assumption)
102          return AssumeSymNE(state, SymR->getSymbol(),
103                             BasicVals.getZeroWithPtrWidth());
104        else
105          return AssumeSymEQ(state, SymR->getSymbol(),
106                             BasicVals.getZeroWithPtrWidth());
107      }
108      SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
109    }
110
111    // FALL-THROUGH.
112  }
113
114  case loc::GotoLabelKind:
115    return Assumption ? state : NULL;
116
117  case loc::ConcreteIntKind: {
118    bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
119    bool isFeasible = b ? Assumption : !Assumption;
120    return isFeasible ? state : NULL;
121  }
122  } // end switch
123}
124
125const GRState *SimpleConstraintManager::Assume(const GRState *state,
126                                               NonLoc Cond,
127                                               bool Assumption) {
128
129  state = AssumeAux(state, Cond, Assumption);
130
131  // EvalAssume is used to call into the GRTransferFunction object to perform
132  // any checker-specific update of the state based on this assumption being
133  // true or false.
134  return state ? state->getTransferFuncs().EvalAssume(state, Cond, Assumption)
135               : NULL;
136}
137
138const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
139                                                  NonLoc Cond,
140                                                  bool Assumption) {
141
142  // We cannot reason about SymIntExpr and SymSymExpr.
143  if (!canReasonAbout(Cond)) {
144    // Just return the current state indicating that the path is feasible.
145    // This may be an over-approximation of what is possible.
146    return state;
147  }
148
149  BasicValueFactory &BasicVals = state->getBasicVals();
150  SymbolManager &SymMgr = state->getSymbolManager();
151
152  switch (Cond.getSubKind()) {
153  default:
154    assert(false && "'Assume' not implemented for this NonLoc");
155
156  case nonloc::SymbolValKind: {
157    nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
158    SymbolRef sym = SV.getSymbol();
159    QualType T =  SymMgr.getType(sym);
160    const llvm::APSInt &zero = BasicVals.getValue(0, T);
161
162    return Assumption ? AssumeSymNE(state, sym, zero)
163                      : AssumeSymEQ(state, sym, zero);
164  }
165
166  case nonloc::SymExprValKind: {
167    nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
168    if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression()))
169      return AssumeSymInt(state, Assumption, SE);
170
171    // For all other symbolic expressions, over-approximate and consider
172    // the constraint feasible.
173    return state;
174  }
175
176  case nonloc::ConcreteIntKind: {
177    bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
178    bool isFeasible = b ? Assumption : !Assumption;
179    return isFeasible ? state : NULL;
180  }
181
182  case nonloc::LocAsIntegerKind:
183    return AssumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
184                     Assumption);
185  } // end switch
186}
187
188const GRState *SimpleConstraintManager::AssumeSymInt(const GRState *state,
189                                                     bool Assumption,
190                                                     const SymIntExpr *SE) {
191
192
193  // Here we assume that LHS is a symbol.  This is consistent with the
194  // rest of the constraint manager logic.
195  SymbolRef Sym = cast<SymbolData>(SE->getLHS());
196  const llvm::APSInt &Int = SE->getRHS();
197
198  switch (SE->getOpcode()) {
199  default:
200    // No logic yet for other operators.  Assume the constraint is feasible.
201    return state;
202
203  case BinaryOperator::EQ:
204    return Assumption ? AssumeSymEQ(state, Sym, Int)
205                      : AssumeSymNE(state, Sym, Int);
206
207  case BinaryOperator::NE:
208    return Assumption ? AssumeSymNE(state, Sym, Int)
209                      : AssumeSymEQ(state, Sym, Int);
210  case BinaryOperator::GT:
211    return Assumption ? AssumeSymGT(state, Sym, Int)
212                      : AssumeSymLE(state, Sym, Int);
213
214  case BinaryOperator::GE:
215    return Assumption ? AssumeSymGE(state, Sym, Int)
216                      : AssumeSymLT(state, Sym, Int);
217
218  case BinaryOperator::LT:
219    return Assumption ? AssumeSymLT(state, Sym, Int)
220                      : AssumeSymGE(state, Sym, Int);
221
222  case BinaryOperator::LE:
223    return Assumption ? AssumeSymLE(state, Sym, Int)
224                      : AssumeSymGT(state, Sym, Int);
225  } // end switch
226}
227
228const GRState *SimpleConstraintManager::AssumeInBound(const GRState *state,
229                                                      SVal Idx,
230                                                      SVal UpperBound,
231                                                      bool Assumption) {
232
233  // Only support ConcreteInt for now.
234  if (!(isa<nonloc::ConcreteInt>(Idx) && isa<nonloc::ConcreteInt>(UpperBound)))
235    return state;
236
237  const llvm::APSInt& Zero = state->getBasicVals().getZeroWithPtrWidth(false);
238  llvm::APSInt IdxV = cast<nonloc::ConcreteInt>(Idx).getValue();
239  // IdxV might be too narrow.
240  if (IdxV.getBitWidth() < Zero.getBitWidth())
241    IdxV.extend(Zero.getBitWidth());
242  // UBV might be too narrow, too.
243  llvm::APSInt UBV = cast<nonloc::ConcreteInt>(UpperBound).getValue();
244  if (UBV.getBitWidth() < Zero.getBitWidth())
245    UBV.extend(Zero.getBitWidth());
246
247  bool InBound = (Zero <= IdxV) && (IdxV < UBV);
248  bool isFeasible = Assumption ? InBound : !InBound;
249  return isFeasible ? state : NULL;
250}
251
252}  // end of namespace clang
253