summaryrefslogtreecommitdiff
path: root/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
blob: a76a2da001b54417e79248bcc68dde177f33db4e (about) (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
//== SimpleConstraintManager.cpp --------------------------------*- C++ -*--==//
//
//                     The LLVM Compiler Infrastructure
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
//
//  This file defines SimpleConstraintManager, a class that holds code shared
//  between BasicConstraintManager and RangeConstraintManager.
//
//===----------------------------------------------------------------------===//

#include "SimpleConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"

namespace clang {

namespace ento {

SimpleConstraintManager::~SimpleConstraintManager() {}

bool SimpleConstraintManager::canReasonAbout(SVal X) const {
  nonloc::SymbolVal *SymVal = dyn_cast<nonloc::SymbolVal>(&X);
  if (SymVal && SymVal->isExpression()) {
    const SymExpr *SE = SymVal->getSymbol();

    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
      switch (SIE->getOpcode()) {
          // We don't reason yet about bitwise-constraints on symbolic values.
        case BO_And:
        case BO_Or:
        case BO_Xor:
          return false;
        // We don't reason yet about these arithmetic constraints on
        // symbolic values.
        case BO_Mul:
        case BO_Div:
        case BO_Rem:
        case BO_Shl:
        case BO_Shr:
          return false;
        // All other cases.
        default:
          return true;
      }
    }

    return false;
  }

  return true;
}

ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
                                               DefinedSVal Cond,
                                               bool Assumption) {
  if (isa<NonLoc>(Cond))
    return assume(state, cast<NonLoc>(Cond), Assumption);
  else
    return assume(state, cast<Loc>(Cond), Assumption);
}

ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state, Loc cond,
                                               bool assumption) {
  state = assumeAux(state, cond, assumption);
  return SU.processAssume(state, cond, assumption);
}

ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
                                                  Loc Cond, bool Assumption) {

  BasicValueFactory &BasicVals = state->getBasicVals();

  switch (Cond.getSubKind()) {
  default:
    assert (false && "'Assume' not implemented for this Loc.");
    return state;

  case loc::MemRegionKind: {
    // FIXME: Should this go into the storemanager?

    const MemRegion *R = cast<loc::MemRegionVal>(Cond).getRegion();
    const SubRegion *SubR = dyn_cast<SubRegion>(R);

    while (SubR) {
      // FIXME: now we only find the first symbolic region.
      if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
        const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth();
        if (Assumption)
          return assumeSymNE(state, SymR->getSymbol(), zero, zero);
        else
          return assumeSymEQ(state, SymR->getSymbol(), zero, zero);
      }
      SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
    }

    // FALL-THROUGH.
  }

  case loc::GotoLabelKind:
    return Assumption ? state : NULL;

  case loc::ConcreteIntKind: {
    bool b = cast<loc::ConcreteInt>(Cond).getValue() != 0;
    bool isFeasible = b ? Assumption : !Assumption;
    return isFeasible ? state : NULL;
  }
  } // end switch
}

ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
                                               NonLoc cond,
                                               bool assumption) {
  state = assumeAux(state, cond, assumption);
  return SU.processAssume(state, cond, assumption);
}

static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
  // FIXME: This should probably be part of BinaryOperator, since this isn't
  // the only place it's used. (This code was copied from SimpleSValBuilder.cpp.)
  switch (op) {
  default:
    llvm_unreachable("Invalid opcode.");
  case BO_LT: return BO_GE;
  case BO_GT: return BO_LE;
  case BO_LE: return BO_GT;
  case BO_GE: return BO_LT;
  case BO_EQ: return BO_NE;
  case BO_NE: return BO_EQ;
  }
}


ProgramStateRef SimpleConstraintManager::assumeAuxForSymbol(
                                              ProgramStateRef State,
                                              SymbolRef Sym,
                                              bool Assumption) {
  QualType T =  State->getSymbolManager().getType(Sym);
  const llvm::APSInt &zero = State->getBasicVals().getValue(0, T);
  if (Assumption)
    return assumeSymNE(State, Sym, zero, zero);
  else
    return assumeSymEQ(State, Sym, zero, zero);
}

ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
                                                  NonLoc Cond,
                                                  bool Assumption) {

  // We cannot reason about SymSymExprs, and can only reason about some
  // SymIntExprs.
  if (!canReasonAbout(Cond)) {
    // Just add the constraint to the expression without trying to simplify.
    SymbolRef sym = Cond.getAsSymExpr();
    return assumeAuxForSymbol(state, sym, Assumption);
  }

  BasicValueFactory &BasicVals = state->getBasicVals();
  SymbolManager &SymMgr = state->getSymbolManager();

  switch (Cond.getSubKind()) {
  default:
    llvm_unreachable("'Assume' not implemented for this NonLoc");

  case nonloc::SymbolValKind: {
    nonloc::SymbolVal& SV = cast<nonloc::SymbolVal>(Cond);
    SymbolRef sym = SV.getSymbol();
    assert(sym);

    // Handle SymbolData.
    if (!SV.isExpression()) {
      return assumeAuxForSymbol(state, sym, Assumption);

    // Handle symbolic expression.
    } else {
      // We can only simplify expressions whose RHS is an integer.
      const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
      if (!SE)
        return assumeAuxForSymbol(state, sym, Assumption);

      BinaryOperator::Opcode op = SE->getOpcode();
      // Implicitly compare non-comparison expressions to 0.
      if (!BinaryOperator::isComparisonOp(op)) {
        QualType T = SymMgr.getType(SE);
        const llvm::APSInt &zero = BasicVals.getValue(0, T);
        op = (Assumption ? BO_NE : BO_EQ);
        return assumeSymRel(state, SE, op, zero);
      }
      // From here on out, op is the real comparison we'll be testing.
      if (!Assumption)
        op = NegateComparison(op);

      return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
    }
  }

  case nonloc::ConcreteIntKind: {
    bool b = cast<nonloc::ConcreteInt>(Cond).getValue() != 0;
    bool isFeasible = b ? Assumption : !Assumption;
    return isFeasible ? state : NULL;
  }

  case nonloc::LocAsIntegerKind:
    return assumeAux(state, cast<nonloc::LocAsInteger>(Cond).getLoc(),
                     Assumption);
  } // end switch
}

static llvm::APSInt computeAdjustment(const SymExpr *LHS,
                                      SymbolRef &Sym) {
  llvm::APSInt DefaultAdjustment;
  DefaultAdjustment = 0;

  // First check if the LHS is a simple symbol reference.
  if (isa<SymbolData>(LHS))
    return DefaultAdjustment;

  // Next, see if it's a "($sym+constant1)" expression.
  const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);

  // We cannot simplify "($sym1+$sym2)".
  if (!SE)
    return DefaultAdjustment;

  // Get the constant out of the expression "($sym+constant1)" or
  // "<expr>+constant1".
  Sym = SE->getLHS();
  switch (SE->getOpcode()) {
  case BO_Add:
    return SE->getRHS();
  case BO_Sub:
    return -SE->getRHS();
  default:
    // We cannot simplify non-additive operators.
    return DefaultAdjustment;
  }
}

ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state,
                                                     const SymExpr *LHS,
                                                     BinaryOperator::Opcode op,
                                                     const llvm::APSInt& Int) {
  assert(BinaryOperator::isComparisonOp(op) &&
         "Non-comparison ops should be rewritten as comparisons to zero.");

  // We only handle simple comparisons of the form "$sym == constant"
  // or "($sym+constant1) == constant2".
  // The adjustment is "constant1" in the above expression. It's used to
  // "slide" the solution range around for modular arithmetic. For example,
  // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
  // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
  // the subclasses of SimpleConstraintManager to handle the adjustment.
  SymbolRef Sym = LHS;
  llvm::APSInt Adjustment = computeAdjustment(LHS, Sym);

  // FIXME: This next section is a hack. It silently converts the integers to
  // be of the same type as the symbol, which is not always correct. Really the
  // comparisons should be performed using the Int's type, then mapped back to
  // the symbol's range of values.
  ProgramStateManager &StateMgr = state->getStateManager();
  ASTContext &Ctx = StateMgr.getContext();

  QualType T = Sym->getType(Ctx);
  assert(T->isIntegerType() || Loc::isLocType(T));
  unsigned bitwidth = Ctx.getTypeSize(T);
  bool isSymUnsigned 
    = T->isUnsignedIntegerOrEnumerationType() || Loc::isLocType(T);

  // Convert the adjustment.
  Adjustment.setIsUnsigned(isSymUnsigned);
  Adjustment = Adjustment.extOrTrunc(bitwidth);

  // Convert the right-hand side integer.
  llvm::APSInt ConvertedInt(Int, isSymUnsigned);
  ConvertedInt = ConvertedInt.extOrTrunc(bitwidth);

  switch (op) {
  default:
    // No logic yet for other operators.  assume the constraint is feasible.
    return state;

  case BO_EQ:
    return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);

  case BO_NE:
    return assumeSymNE(state, Sym, ConvertedInt, Adjustment);

  case BO_GT:
    return assumeSymGT(state, Sym, ConvertedInt, Adjustment);

  case BO_GE:
    return assumeSymGE(state, Sym, ConvertedInt, Adjustment);

  case BO_LT:
    return assumeSymLT(state, Sym, ConvertedInt, Adjustment);

  case BO_LE:
    return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
  } // end switch
}

} // end of namespace ento

} // end of namespace clang