Coverage Report

Created: 2019-07-24 05:18

/Users/buildslave/jenkins/workspace/clang-stage2-coverage-R/llvm/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
Line
Count
Source (jump to first uncovered line)
1
//== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
2
//
3
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4
// See https://llvm.org/LICENSE.txt for license information.
5
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6
//
7
//===----------------------------------------------------------------------===//
8
//
9
//  This file defines a SMT generic API, which will be the base class for
10
//  every SMT solver specific class.
11
//
12
//===----------------------------------------------------------------------===//
13
14
#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
15
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
16
17
#include "clang/Basic/JsonSupport.h"
18
#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
19
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
20
21
typedef llvm::ImmutableSet<
22
    std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
23
    ConstraintSMTType;
24
REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType)
25
26
namespace clang {
27
namespace ento {
28
29
class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
30
  mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
31
32
public:
33
  SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
34
0
      : SimpleConstraintManager(SE, SB) {}
35
0
  virtual ~SMTConstraintManager() = default;
36
37
  //===------------------------------------------------------------------===//
38
  // Implementation for interface from SimpleConstraintManager.
39
  //===------------------------------------------------------------------===//
40
41
  ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
42
0
                            bool Assumption) override {
43
0
    ASTContext &Ctx = getBasicVals().getContext();
44
0
45
0
    QualType RetTy;
46
0
    bool hasComparison;
47
0
48
0
    llvm::SMTExprRef Exp =
49
0
        SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
50
0
51
0
    // Create zero comparison for implicit boolean cast, with reversed
52
0
    // assumption
53
0
    if (!hasComparison && !RetTy->isBooleanType())
54
0
      return assumeExpr(
55
0
          State, Sym,
56
0
          SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
57
0
58
0
    return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
59
0
  }
60
61
  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
62
                                          const llvm::APSInt &From,
63
                                          const llvm::APSInt &To,
64
0
                                          bool InRange) override {
65
0
    ASTContext &Ctx = getBasicVals().getContext();
66
0
    return assumeExpr(
67
0
        State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
68
0
  }
69
70
  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
71
0
                                       bool Assumption) override {
72
0
    // Skip anything that is unsupported
73
0
    return State;
74
0
  }
75
76
  //===------------------------------------------------------------------===//
77
  // Implementation for interface from ConstraintManager.
78
  //===------------------------------------------------------------------===//
79
80
0
  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
81
0
    ASTContext &Ctx = getBasicVals().getContext();
82
0
83
0
    QualType RetTy;
84
0
    // The expression may be casted, so we cannot call getZ3DataExpr() directly
85
0
    llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
86
0
    llvm::SMTExprRef Exp =
87
0
        SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
88
0
89
0
    // Negate the constraint
90
0
    llvm::SMTExprRef NotExp =
91
0
        SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
92
0
93
0
    ConditionTruthVal isSat = checkModel(State, Sym, Exp);
94
0
    ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
95
0
96
0
    // Zero is the only possible solution
97
0
    if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
98
0
      return true;
99
0
100
0
    // Zero is not a solution
101
0
    if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
102
0
      return false;
103
0
104
0
    // Zero may be a solution
105
0
    return ConditionTruthVal();
106
0
  }
107
108
  const llvm::APSInt *getSymVal(ProgramStateRef State,
109
0
                                SymbolRef Sym) const override {
110
0
    BasicValueFactory &BVF = getBasicVals();
111
0
    ASTContext &Ctx = BVF.getContext();
112
0
113
0
    if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
114
0
      QualType Ty = Sym->getType();
115
0
      assert(!Ty->isRealFloatingType());
116
0
      llvm::APSInt Value(Ctx.getTypeSize(Ty),
117
0
                         !Ty->isSignedIntegerOrEnumerationType());
118
0
119
0
      // TODO: this should call checkModel so we can use the cache, however,
120
0
      // this method tries to get the interpretation (the actual value) from
121
0
      // the solver, which is currently not cached.
122
0
123
0
      llvm::SMTExprRef Exp =
124
0
          SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
125
0
126
0
      Solver->reset();
127
0
      addStateConstraints(State);
128
0
129
0
      // Constraints are unsatisfiable
130
0
      Optional<bool> isSat = Solver->check();
131
0
      if (!isSat.hasValue() || !isSat.getValue())
132
0
        return nullptr;
133
0
134
0
      // Model does not assign interpretation
135
0
      if (!Solver->getInterpretation(Exp, Value))
136
0
        return nullptr;
137
0
138
0
      // A value has been obtained, check if it is the only value
139
0
      llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
140
0
          Solver, Exp, BO_NE,
141
0
          Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
142
0
                              : Solver->mkBitvector(Value, Value.getBitWidth()),
143
0
          /*isSigned=*/false);
144
0
145
0
      Solver->addConstraint(NotExp);
146
0
147
0
      Optional<bool> isNotSat = Solver->check();
148
0
      if (!isSat.hasValue() || isNotSat.getValue())
149
0
        return nullptr;
150
0
151
0
      // This is the only solution, store it
152
0
      return &BVF.getValue(Value);
153
0
    }
154
0
155
0
    if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
156
0
      SymbolRef CastSym = SC->getOperand();
157
0
      QualType CastTy = SC->getType();
158
0
      // Skip the void type
159
0
      if (CastTy->isVoidType())
160
0
        return nullptr;
161
0
162
0
      const llvm::APSInt *Value;
163
0
      if (!(Value = getSymVal(State, CastSym)))
164
0
        return nullptr;
165
0
      return &BVF.Convert(SC->getType(), *Value);
166
0
    }
167
0
168
0
    if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
169
0
      const llvm::APSInt *LHS, *RHS;
170
0
      if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
171
0
        LHS = getSymVal(State, SIE->getLHS());
172
0
        RHS = &SIE->getRHS();
173
0
      } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
174
0
        LHS = &ISE->getLHS();
175
0
        RHS = getSymVal(State, ISE->getRHS());
176
0
      } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
177
0
        // Early termination to avoid expensive call
178
0
        LHS = getSymVal(State, SSM->getLHS());
179
0
        RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
180
0
      } else {
181
0
        llvm_unreachable("Unsupported binary expression to get symbol value!");
182
0
      }
183
0
184
0
      if (!LHS || !RHS)
185
0
        return nullptr;
186
0
187
0
      llvm::APSInt ConvertedLHS, ConvertedRHS;
188
0
      QualType LTy, RTy;
189
0
      std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
190
0
      std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
191
0
      SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
192
0
          Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
193
0
      return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
194
0
    }
195
0
196
0
    llvm_unreachable("Unsupported expression to get symbol value!");
197
0
  }
198
199
  ProgramStateRef removeDeadBindings(ProgramStateRef State,
200
0
                                     SymbolReaper &SymReaper) override {
201
0
    auto CZ = State->get<ConstraintSMT>();
202
0
    auto &CZFactory = State->get_context<ConstraintSMT>();
203
0
204
0
    for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
205
0
      if (SymReaper.isDead(I->first))
206
0
        CZ = CZFactory.remove(CZ, *I);
207
0
    }
208
0
209
0
    return State->set<ConstraintSMT>(CZ);
210
0
  }
211
212
  void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
213
0
                 unsigned int Space = 0, bool IsDot = false) const override {
214
0
    ConstraintSMTType Constraints = State->get<ConstraintSMT>();
215
0
216
0
    Indent(Out, Space, IsDot) << "\"constraints\": ";
217
0
    if (Constraints.isEmpty()) {
218
0
      Out << "null," << NL;
219
0
      return;
220
0
    }
221
0
222
0
    ++Space;
223
0
    Out << '[' << NL;
224
0
    for (ConstraintSMTType::iterator I = Constraints.begin();
225
0
         I != Constraints.end(); ++I) {
226
0
      Indent(Out, Space, IsDot)
227
0
          << "{ \"symbol\": \"" << I->first << "\", \"range\": \"";
228
0
      I->second->print(Out);
229
0
      Out << "\" }";
230
0
231
0
      if (std::next(I) != Constraints.end())
232
0
        Out << ',';
233
0
      Out << NL;
234
0
    }
235
0
236
0
    --Space;
237
0
    Indent(Out, Space, IsDot) << "],";
238
0
  }
239
240
  bool haveEqualConstraints(ProgramStateRef S1,
241
0
                            ProgramStateRef S2) const override {
242
0
    return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
243
0
  }
244
245
0
  bool canReasonAbout(SVal X) const override {
246
0
    const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
247
0
248
0
    Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
249
0
    if (!SymVal)
250
0
      return true;
251
0
252
0
    const SymExpr *Sym = SymVal->getSymbol();
253
0
    QualType Ty = Sym->getType();
254
0
255
0
    // Complex types are not modeled
256
0
    if (Ty->isComplexType() || Ty->isComplexIntegerType())
257
0
      return false;
258
0
259
0
    // Non-IEEE 754 floating-point types are not modeled
260
0
    if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
261
0
         (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
262
0
          &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
263
0
      return false;
264
0
265
0
    if (Ty->isRealFloatingType())
266
0
      return Solver->isFPSupported();
267
0
268
0
    if (isa<SymbolData>(Sym))
269
0
      return true;
270
0
271
0
    SValBuilder &SVB = getSValBuilder();
272
0
273
0
    if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
274
0
      return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
275
0
276
0
    if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
277
0
      if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
278
0
        return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
279
0
280
0
      if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
281
0
        return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
282
0
283
0
      if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
284
0
        return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
285
0
               canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
286
0
    }
287
0
288
0
    llvm_unreachable("Unsupported expression to reason about!");
289
0
  }
290
291
  /// Dumps SMT formula
292
0
  LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
293
294
protected:
295
  // Check whether a new model is satisfiable, and update the program state.
296
  virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
297
0
                                     const llvm::SMTExprRef &Exp) {
298
0
    // Check the model, avoid simplifying AST to save time
299
0
    if (checkModel(State, Sym, Exp).isConstrainedTrue())
300
0
      return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
301
0
302
0
    return nullptr;
303
0
  }
304
305
  /// Given a program state, construct the logical conjunction and add it to
306
  /// the solver
307
0
  virtual void addStateConstraints(ProgramStateRef State) const {
308
0
    // TODO: Don't add all the constraints, only the relevant ones
309
0
    auto CZ = State->get<ConstraintSMT>();
310
0
    auto I = CZ.begin(), IE = CZ.end();
311
0
312
0
    // Construct the logical AND of all the constraints
313
0
    if (I != IE) {
314
0
      std::vector<llvm::SMTExprRef> ASTs;
315
0
316
0
      llvm::SMTExprRef Constraint = I++->second;
317
0
      while (I != IE) {
318
0
        Constraint = Solver->mkAnd(Constraint, I++->second);
319
0
      }
320
0
321
0
      Solver->addConstraint(Constraint);
322
0
    }
323
0
  }
324
325
  // Generate and check a Z3 model, using the given constraint.
326
  ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
327
0
                               const llvm::SMTExprRef &Exp) const {
328
0
    ProgramStateRef NewState =
329
0
        State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
330
0
331
0
    llvm::FoldingSetNodeID ID;
332
0
    NewState->get<ConstraintSMT>().Profile(ID);
333
0
334
0
    unsigned hash = ID.ComputeHash();
335
0
    auto I = Cached.find(hash);
336
0
    if (I != Cached.end())
337
0
      return I->second;
338
0
339
0
    Solver->reset();
340
0
    addStateConstraints(NewState);
341
0
342
0
    Optional<bool> res = Solver->check();
343
0
    if (!res.hasValue())
344
0
      Cached[hash] = ConditionTruthVal();
345
0
    else
346
0
      Cached[hash] = ConditionTruthVal(res.getValue());
347
0
348
0
    return Cached[hash];
349
0
  }
350
351
  // Cache the result of an SMT query (true, false, unknown). The key is the
352
  // hash of the constraints in a state
353
  mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
354
}; // end class SMTConstraintManager
355
356
} // namespace ento
357
} // namespace clang
358
359
#endif