Coverage Report

Created: 2020-09-19 12:23

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