Coverage Report

Created: 2020-11-28 09:00

/Users/buildslave/jenkins/workspace/coverage/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
Line
Count
Source (jump to first uncovered line)
1
//== SMTConv.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 set of functions to create SMT expressions
10
//
11
//===----------------------------------------------------------------------===//
12
13
#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
14
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
15
16
#include "clang/AST/Expr.h"
17
#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
18
#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
19
#include "llvm/Support/SMTAPI.h"
20
21
namespace clang {
22
namespace ento {
23
24
class SMTConv {
25
public:
26
  // Returns an appropriate sort, given a QualType and it's bit width.
27
  static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,
28
0
                                        const QualType &Ty, unsigned BitWidth) {
29
0
    if (Ty->isBooleanType())
30
0
      return Solver->getBoolSort();
31
32
0
    if (Ty->isRealFloatingType())
33
0
      return Solver->getFloatSort(BitWidth);
34
35
0
    return Solver->getBitvectorSort(BitWidth);
36
0
  }
37
38
  /// Constructs an SMTSolverRef from an unary operator.
39
  static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver,
40
                                          const UnaryOperator::Opcode Op,
41
0
                                          const llvm::SMTExprRef &Exp) {
42
0
    switch (Op) {
43
0
    case UO_Minus:
44
0
      return Solver->mkBVNeg(Exp);
45
46
0
    case UO_Not:
47
0
      return Solver->mkBVNot(Exp);
48
49
0
    case UO_LNot:
50
0
      return Solver->mkNot(Exp);
51
52
0
    default:;
53
0
    }
54
0
    llvm_unreachable("Unimplemented opcode");
55
0
  }
56
57
  /// Constructs an SMTSolverRef from a floating-point unary operator.
58
  static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver,
59
                                               const UnaryOperator::Opcode Op,
60
0
                                               const llvm::SMTExprRef &Exp) {
61
0
    switch (Op) {
62
0
    case UO_Minus:
63
0
      return Solver->mkFPNeg(Exp);
64
65
0
    case UO_LNot:
66
0
      return fromUnOp(Solver, Op, Exp);
67
68
0
    default:;
69
0
    }
70
0
    llvm_unreachable("Unimplemented opcode");
71
0
  }
72
73
  /// Construct an SMTSolverRef from a n-ary binary operator.
74
  static inline llvm::SMTExprRef
75
  fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op,
76
0
             const std::vector<llvm::SMTExprRef> &ASTs) {
77
0
    assert(!ASTs.empty());
78
0
79
0
    if (Op != BO_LAnd && Op != BO_LOr)
80
0
      llvm_unreachable("Unimplemented opcode");
81
0
82
0
    llvm::SMTExprRef res = ASTs.front();
83
0
    for (std::size_t i = 1; i < ASTs.size(); ++i)
84
0
      res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])
85
0
                            : Solver->mkOr(res, ASTs[i]);
86
0
    return res;
87
0
  }
88
89
  /// Construct an SMTSolverRef from a binary operator.
90
  static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver,
91
                                           const llvm::SMTExprRef &LHS,
92
                                           const BinaryOperator::Opcode Op,
93
                                           const llvm::SMTExprRef &RHS,
94
0
                                           bool isSigned) {
95
0
    assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
96
0
           "AST's must have the same sort!");
97
98
0
    switch (Op) {
99
    // Multiplicative operators
100
0
    case BO_Mul:
101
0
      return Solver->mkBVMul(LHS, RHS);
102
103
0
    case BO_Div:
104
0
      return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);
105
106
0
    case BO_Rem:
107
0
      return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);
108
109
      // Additive operators
110
0
    case BO_Add:
111
0
      return Solver->mkBVAdd(LHS, RHS);
112
113
0
    case BO_Sub:
114
0
      return Solver->mkBVSub(LHS, RHS);
115
116
      // Bitwise shift operators
117
0
    case BO_Shl:
118
0
      return Solver->mkBVShl(LHS, RHS);
119
120
0
    case BO_Shr:
121
0
      return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);
122
123
      // Relational operators
124
0
    case BO_LT:
125
0
      return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);
126
127
0
    case BO_GT:
128
0
      return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);
129
130
0
    case BO_LE:
131
0
      return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);
132
133
0
    case BO_GE:
134
0
      return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);
135
136
      // Equality operators
137
0
    case BO_EQ:
138
0
      return Solver->mkEqual(LHS, RHS);
139
140
0
    case BO_NE:
141
0
      return fromUnOp(Solver, UO_LNot,
142
0
                      fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned));
143
144
      // Bitwise operators
145
0
    case BO_And:
146
0
      return Solver->mkBVAnd(LHS, RHS);
147
148
0
    case BO_Xor:
149
0
      return Solver->mkBVXor(LHS, RHS);
150
151
0
    case BO_Or:
152
0
      return Solver->mkBVOr(LHS, RHS);
153
154
      // Logical operators
155
0
    case BO_LAnd:
156
0
      return Solver->mkAnd(LHS, RHS);
157
158
0
    case BO_LOr:
159
0
      return Solver->mkOr(LHS, RHS);
160
161
0
    default:;
162
0
    }
163
0
    llvm_unreachable("Unimplemented opcode");
164
0
  }
165
166
  /// Construct an SMTSolverRef from a special floating-point binary
167
  /// operator.
168
  static inline llvm::SMTExprRef
169
  fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS,
170
                        const BinaryOperator::Opcode Op,
171
0
                        const llvm::APFloat::fltCategory &RHS) {
172
0
    switch (Op) {
173
0
    // Equality operators
174
0
    case BO_EQ:
175
0
      switch (RHS) {
176
0
      case llvm::APFloat::fcInfinity:
177
0
        return Solver->mkFPIsInfinite(LHS);
178
0
179
0
      case llvm::APFloat::fcNaN:
180
0
        return Solver->mkFPIsNaN(LHS);
181
0
182
0
      case llvm::APFloat::fcNormal:
183
0
        return Solver->mkFPIsNormal(LHS);
184
0
185
0
      case llvm::APFloat::fcZero:
186
0
        return Solver->mkFPIsZero(LHS);
187
0
      }
188
0
      break;
189
0
190
0
    case BO_NE:
191
0
      return fromFloatUnOp(Solver, UO_LNot,
192
0
                           fromFloatSpecialBinOp(Solver, LHS, BO_EQ, RHS));
193
0
194
0
    default:;
195
0
    }
196
0
197
0
    llvm_unreachable("Unimplemented opcode");
198
0
  }
199
200
  /// Construct an SMTSolverRef from a floating-point binary operator.
201
  static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver,
202
                                                const llvm::SMTExprRef &LHS,
203
                                                const BinaryOperator::Opcode Op,
204
0
                                                const llvm::SMTExprRef &RHS) {
205
0
    assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
206
0
           "AST's must have the same sort!");
207
208
0
    switch (Op) {
209
    // Multiplicative operators
210
0
    case BO_Mul:
211
0
      return Solver->mkFPMul(LHS, RHS);
212
213
0
    case BO_Div:
214
0
      return Solver->mkFPDiv(LHS, RHS);
215
216
0
    case BO_Rem:
217
0
      return Solver->mkFPRem(LHS, RHS);
218
219
      // Additive operators
220
0
    case BO_Add:
221
0
      return Solver->mkFPAdd(LHS, RHS);
222
223
0
    case BO_Sub:
224
0
      return Solver->mkFPSub(LHS, RHS);
225
226
      // Relational operators
227
0
    case BO_LT:
228
0
      return Solver->mkFPLt(LHS, RHS);
229
230
0
    case BO_GT:
231
0
      return Solver->mkFPGt(LHS, RHS);
232
233
0
    case BO_LE:
234
0
      return Solver->mkFPLe(LHS, RHS);
235
236
0
    case BO_GE:
237
0
      return Solver->mkFPGe(LHS, RHS);
238
239
      // Equality operators
240
0
    case BO_EQ:
241
0
      return Solver->mkFPEqual(LHS, RHS);
242
243
0
    case BO_NE:
244
0
      return fromFloatUnOp(Solver, UO_LNot,
245
0
                           fromFloatBinOp(Solver, LHS, BO_EQ, RHS));
246
247
      // Logical operators
248
0
    case BO_LAnd:
249
0
    case BO_LOr:
250
0
      return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false);
251
252
0
    default:;
253
0
    }
254
255
0
    llvm_unreachable("Unimplemented opcode");
256
0
  }
257
258
  /// Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy,
259
  /// and their bit widths.
260
  static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver,
261
                                          const llvm::SMTExprRef &Exp,
262
                                          QualType ToTy, uint64_t ToBitWidth,
263
                                          QualType FromTy,
264
0
                                          uint64_t FromBitWidth) {
265
0
    if ((FromTy->isIntegralOrEnumerationType() &&
266
0
         ToTy->isIntegralOrEnumerationType()) ||
267
0
        (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
268
0
        (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
269
0
        (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
270
271
0
      if (FromTy->isBooleanType()) {
272
0
        assert(ToBitWidth > 0 && "BitWidth must be positive!");
273
0
        return Solver->mkIte(
274
0
            Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth),
275
0
            Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth));
276
0
      }
277
278
0
      if (ToBitWidth > FromBitWidth)
279
0
        return FromTy->isSignedIntegerOrEnumerationType()
280
0
                   ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
281
0
                   : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
282
283
0
      if (ToBitWidth < FromBitWidth)
284
0
        return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
285
286
      // Both are bitvectors with the same width, ignore the type cast
287
0
      return Exp;
288
0
    }
289
290
0
    if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
291
0
      if (ToBitWidth != FromBitWidth)
292
0
        return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
293
294
0
      return Exp;
295
0
    }
296
297
0
    if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
298
0
      llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
299
0
      return FromTy->isSignedIntegerOrEnumerationType()
300
0
                 ? Solver->mkSBVtoFP(Exp, Sort)
301
0
                 : Solver->mkUBVtoFP(Exp, Sort);
302
0
    }
303
304
0
    if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
305
0
      return ToTy->isSignedIntegerOrEnumerationType()
306
0
                 ? Solver->mkFPtoSBV(Exp, ToBitWidth)
307
0
                 : Solver->mkFPtoUBV(Exp, ToBitWidth);
308
309
0
    llvm_unreachable("Unsupported explicit type cast!");
310
0
  }
311
312
  // Callback function for doCast parameter on APSInt type.
313
  static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver,
314
                                        const llvm::APSInt &V, QualType ToTy,
315
                                        uint64_t ToWidth, QualType FromTy,
316
0
                                        uint64_t FromWidth) {
317
0
    APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
318
0
    return TargetType.convert(V);
319
0
  }
320
321
  /// Construct an SMTSolverRef from a SymbolData.
322
  static inline llvm::SMTExprRef
323
0
  fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) {
324
0
    const SymbolID ID = Sym->getSymbolID();
325
0
    const QualType Ty = Sym->getType();
326
0
    const uint64_t BitWidth = Ctx.getTypeSize(Ty);
327
328
0
    llvm::SmallString<16> Str;
329
0
    llvm::raw_svector_ostream OS(Str);
330
0
    OS << Sym->getKindStr() << ID;
331
0
    return Solver->mkSymbol(Str.c_str(), mkSort(Solver, Ty, BitWidth));
332
0
  }
333
334
  // Wrapper to generate SMTSolverRef from SymbolCast data.
335
  static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,
336
                                             ASTContext &Ctx,
337
                                             const llvm::SMTExprRef &Exp,
338
0
                                             QualType FromTy, QualType ToTy) {
339
0
    return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
340
0
                    Ctx.getTypeSize(FromTy));
341
0
  }
342
343
  // Wrapper to generate SMTSolverRef from unpacked binary symbolic
344
  // expression. Sets the RetTy parameter. See getSMTSolverRef().
345
  static inline llvm::SMTExprRef
346
  getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
347
             const llvm::SMTExprRef &LHS, QualType LTy,
348
             BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS,
349
0
             QualType RTy, QualType *RetTy) {
350
0
    llvm::SMTExprRef NewLHS = LHS;
351
0
    llvm::SMTExprRef NewRHS = RHS;
352
0
    doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
353
354
    // Update the return type parameter if the output type has changed.
355
0
    if (RetTy) {
356
      // A boolean result can be represented as an integer type in C/C++, but at
357
      // this point we only care about the SMT sorts. Set it as a boolean type
358
      // to avoid subsequent SMT errors.
359
0
      if (BinaryOperator::isComparisonOp(Op) ||
360
0
          BinaryOperator::isLogicalOp(Op)) {
361
0
        *RetTy = Ctx.BoolTy;
362
0
      } else {
363
0
        *RetTy = LTy;
364
0
      }
365
366
      // If the two operands are pointers and the operation is a subtraction,
367
      // the result is of type ptrdiff_t, which is signed
368
0
      if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) {
369
0
        *RetTy = Ctx.getPointerDiffType();
370
0
      }
371
0
    }
372
373
0
    return LTy->isRealFloatingType()
374
0
               ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS)
375
0
               : fromBinOp(Solver, NewLHS, Op, NewRHS,
376
0
                           LTy->isSignedIntegerOrEnumerationType());
377
0
  }
378
379
  // Wrapper to generate SMTSolverRef from BinarySymExpr.
380
  // Sets the hasComparison and RetTy parameters. See getSMTSolverRef().
381
  static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver,
382
                                               ASTContext &Ctx,
383
                                               const BinarySymExpr *BSE,
384
                                               bool *hasComparison,
385
0
                                               QualType *RetTy) {
386
0
    QualType LTy, RTy;
387
0
    BinaryOperator::Opcode Op = BSE->getOpcode();
388
389
0
    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
390
0
      llvm::SMTExprRef LHS =
391
0
          getSymExpr(Solver, Ctx, SIE->getLHS(), &LTy, hasComparison);
392
0
      llvm::APSInt NewRInt;
393
0
      std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
394
0
      llvm::SMTExprRef RHS =
395
0
          Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
396
0
      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
397
0
    }
398
399
0
    if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
400
0
      llvm::APSInt NewLInt;
401
0
      std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
402
0
      llvm::SMTExprRef LHS =
403
0
          Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
404
0
      llvm::SMTExprRef RHS =
405
0
          getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
406
0
      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
407
0
    }
408
409
0
    if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
410
0
      llvm::SMTExprRef LHS =
411
0
          getSymExpr(Solver, Ctx, SSM->getLHS(), &LTy, hasComparison);
412
0
      llvm::SMTExprRef RHS =
413
0
          getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
414
0
      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
415
0
    }
416
417
0
    llvm_unreachable("Unsupported BinarySymExpr type!");
418
0
  }
419
420
  // Recursive implementation to unpack and generate symbolic expression.
421
  // Sets the hasComparison and RetTy parameters. See getExpr().
422
  static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
423
                                            ASTContext &Ctx, SymbolRef Sym,
424
                                            QualType *RetTy,
425
0
                                            bool *hasComparison) {
426
0
    if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
427
0
      if (RetTy)
428
0
        *RetTy = Sym->getType();
429
430
0
      return fromData(Solver, Ctx, SD);
431
0
    }
432
433
0
    if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
434
0
      if (RetTy)
435
0
        *RetTy = Sym->getType();
436
437
0
      QualType FromTy;
438
0
      llvm::SMTExprRef Exp =
439
0
          getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
440
441
      // Casting an expression with a comparison invalidates it. Note that this
442
      // must occur after the recursive call above.
443
      // e.g. (signed char) (x > 0)
444
0
      if (hasComparison)
445
0
        *hasComparison = false;
446
0
      return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
447
0
    }
448
449
0
    if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
450
0
      llvm::SMTExprRef Exp =
451
0
          getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
452
      // Set the hasComparison parameter, in post-order traversal order.
453
0
      if (hasComparison)
454
0
        *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
455
0
      return Exp;
456
0
    }
457
458
0
    llvm_unreachable("Unsupported SymbolRef type!");
459
0
  }
460
461
  // Generate an SMTSolverRef that represents the given symbolic expression.
462
  // Sets the hasComparison parameter if the expression has a comparison
463
  // operator. Sets the RetTy parameter to the final return type after
464
  // promotions and casts.
465
  static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
466
                                         ASTContext &Ctx, SymbolRef Sym,
467
                                         QualType *RetTy = nullptr,
468
0
                                         bool *hasComparison = nullptr) {
469
0
    if (hasComparison) {
470
0
      *hasComparison = false;
471
0
    }
472
473
0
    return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
474
0
  }
475
476
  // Generate an SMTSolverRef that compares the expression to zero.
477
  static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver,
478
                                             ASTContext &Ctx,
479
                                             const llvm::SMTExprRef &Exp,
480
0
                                             QualType Ty, bool Assumption) {
481
0
    if (Ty->isRealFloatingType()) {
482
0
      llvm::APFloat Zero =
483
0
          llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
484
0
      return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
485
0
                            Solver->mkFloat(Zero));
486
0
    }
487
488
0
    if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
489
0
        Ty->isBlockPointerType() || Ty->isReferenceType()) {
490
491
      // Skip explicit comparison for boolean types
492
0
      bool isSigned = Ty->isSignedIntegerOrEnumerationType();
493
0
      if (Ty->isBooleanType())
494
0
        return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
495
496
0
      return fromBinOp(
497
0
          Solver, Exp, Assumption ? BO_EQ : BO_NE,
498
0
          Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
499
0
          isSigned);
500
0
    }
501
502
0
    llvm_unreachable("Unsupported type for zero value!");
503
0
  }
Unexecuted instantiation: clang::ento::SMTConv::getZeroExpr(std::__1::shared_ptr<llvm::SMTSolver>&, clang::ASTContext&, llvm::SMTExpr const* const&, clang::QualType, bool)
Unexecuted instantiation: clang::ento::SMTConv::getZeroExpr(std::__1::shared_ptr<llvm::SMTSolver>&, clang::ASTContext&, llvm::SMTExpr const* const&, clang::QualType, bool)
504
505
  // Wrapper to generate SMTSolverRef from a range. If From == To, an
506
  // equality will be created instead.
507
  static inline llvm::SMTExprRef
508
  getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
509
0
               const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) {
510
    // Convert lower bound
511
0
    QualType FromTy;
512
0
    llvm::APSInt NewFromInt;
513
0
    std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
514
0
    llvm::SMTExprRef FromExp =
515
0
        Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
516
517
    // Convert symbol
518
0
    QualType SymTy;
519
0
    llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
520
521
    // Construct single (in)equality
522
0
    if (From == To)
523
0
      return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
524
0
                        FromExp, FromTy, /*RetTy=*/nullptr);
525
526
0
    QualType ToTy;
527
0
    llvm::APSInt NewToInt;
528
0
    std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
529
0
    llvm::SMTExprRef ToExp =
530
0
        Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
531
0
    assert(FromTy == ToTy && "Range values have different types!");
532
533
    // Construct two (in)equalities, and a logical and/or
534
0
    llvm::SMTExprRef LHS =
535
0
        getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
536
0
                   FromTy, /*RetTy=*/nullptr);
537
0
    llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
538
0
                                      InRange ? BO_LE : BO_GT, ToExp, ToTy,
539
0
                                      /*RetTy=*/nullptr);
540
541
0
    return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
542
0
                     SymTy->isSignedIntegerOrEnumerationType());
543
0
  }
544
545
  // Recover the QualType of an APSInt.
546
  // TODO: Refactor to put elsewhere
547
  static inline QualType getAPSIntType(ASTContext &Ctx,
548
0
                                       const llvm::APSInt &Int) {
549
0
    return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
550
0
  }
551
552
  // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
553
  static inline std::pair<llvm::APSInt, QualType>
554
0
  fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) {
555
0
    llvm::APSInt NewInt;
556
557
    // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
558
    // but the former is not available in Clang. Instead, extend the APSInt
559
    // directly.
560
0
    if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) {
561
0
      NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
562
0
    } else
563
0
      NewInt = Int;
564
565
0
    return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
566
0
  }
567
568
  // Perform implicit type conversion on binary symbolic expressions.
569
  // May modify all input parameters.
570
  // TODO: Refactor to use built-in conversion functions
571
  static inline void doTypeConversion(llvm::SMTSolverRef &Solver,
572
                                      ASTContext &Ctx, llvm::SMTExprRef &LHS,
573
                                      llvm::SMTExprRef &RHS, QualType &LTy,
574
0
                                      QualType &RTy) {
575
0
    assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
576
577
    // Perform type conversion
578
0
    if ((LTy->isIntegralOrEnumerationType() &&
579
0
         RTy->isIntegralOrEnumerationType()) &&
580
0
        (LTy->isArithmeticType() && RTy->isArithmeticType())) {
581
0
      SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(
582
0
          Solver, Ctx, LHS, LTy, RHS, RTy);
583
0
      return;
584
0
    }
585
586
0
    if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
587
0
      SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
588
0
          Solver, Ctx, LHS, LTy, RHS, RTy);
589
0
      return;
590
0
    }
591
592
0
    if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
593
0
        (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
594
0
        (LTy->isReferenceType() || RTy->isReferenceType())) {
595
      // TODO: Refactor to Sema::FindCompositePointerType(), and
596
      // Sema::CheckCompareOperands().
597
598
0
      uint64_t LBitWidth = Ctx.getTypeSize(LTy);
599
0
      uint64_t RBitWidth = Ctx.getTypeSize(RTy);
600
601
      // Cast the non-pointer type to the pointer type.
602
      // TODO: Be more strict about this.
603
0
      if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
604
0
          (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
605
0
          (LTy->isReferenceType() ^ RTy->isReferenceType())) {
606
0
        if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
607
0
            LTy->isReferenceType()) {
608
0
          LHS = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
609
0
          LTy = RTy;
610
0
        } else {
611
0
          RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
612
0
          RTy = LTy;
613
0
        }
614
0
      }
615
616
      // Cast the void pointer type to the non-void pointer type.
617
      // For void types, this assumes that the casted value is equal to the
618
      // value of the original pointer, and does not account for alignment
619
      // requirements.
620
0
      if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
621
0
        assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
622
0
               "Pointer types have different bitwidths!");
623
0
        if (RTy->isVoidPointerType())
624
0
          RTy = LTy;
625
0
        else
626
0
          LTy = RTy;
627
0
      }
628
629
0
      if (LTy == RTy)
630
0
        return;
631
0
    }
632
633
    // Fallback: for the solver, assume that these types don't really matter
634
0
    if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
635
0
        (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
636
0
      LTy = RTy;
637
0
      return;
638
0
    }
639
640
    // TODO: Refine behavior for invalid type casts
641
0
  }
642
643
  // Perform implicit integer type conversion.
644
  // May modify all input parameters.
645
  // TODO: Refactor to use Sema::handleIntegerConversion()
646
  template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
647
                                    QualType, uint64_t, QualType, uint64_t)>
648
  static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver,
649
                                         ASTContext &Ctx, T &LHS, QualType &LTy,
650
0
                                         T &RHS, QualType &RTy) {
651
0
    uint64_t LBitWidth = Ctx.getTypeSize(LTy);
652
0
    uint64_t RBitWidth = Ctx.getTypeSize(RTy);
653
654
0
    assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
655
    // Always perform integer promotion before checking type equality.
656
    // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
657
0
    if (LTy->isPromotableIntegerType()) {
658
0
      QualType NewTy = Ctx.getPromotedIntegerType(LTy);
659
0
      uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
660
0
      LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
661
0
      LTy = NewTy;
662
0
      LBitWidth = NewBitWidth;
663
0
    }
664
0
    if (RTy->isPromotableIntegerType()) {
665
0
      QualType NewTy = Ctx.getPromotedIntegerType(RTy);
666
0
      uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
667
0
      RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);
668
0
      RTy = NewTy;
669
0
      RBitWidth = NewBitWidth;
670
0
    }
671
672
0
    if (LTy == RTy)
673
0
      return;
674
675
    // Perform integer type conversion
676
    // Note: Safe to skip updating bitwidth because this must terminate
677
0
    bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
678
0
    bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
679
680
0
    int order = Ctx.getIntegerTypeOrder(LTy, RTy);
681
0
    if (isLSignedTy == isRSignedTy) {
682
      // Same signedness; use the higher-ranked type
683
0
      if (order == 1) {
684
0
        RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
685
0
        RTy = LTy;
686
0
      } else {
687
0
        LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
688
0
        LTy = RTy;
689
0
      }
690
0
    } else if (order != (isLSignedTy ? 1 : -1)) {
691
      // The unsigned type has greater than or equal rank to the
692
      // signed type, so use the unsigned type
693
0
      if (isRSignedTy) {
694
0
        RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
695
0
        RTy = LTy;
696
0
      } else {
697
0
        LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
698
0
        LTy = RTy;
699
0
      }
700
0
    } else if (LBitWidth != RBitWidth) {
701
      // The two types are different widths; if we are here, that
702
      // means the signed type is larger than the unsigned type, so
703
      // use the signed type.
704
0
      if (isLSignedTy) {
705
0
        RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
706
0
        RTy = LTy;
707
0
      } else {
708
0
        LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
709
0
        LTy = RTy;
710
0
      }
711
0
    } else {
712
      // The signed type is higher-ranked than the unsigned type,
713
      // but isn't actually any bigger (like unsigned int and long
714
      // on most 32-bit systems).  Use the unsigned type corresponding
715
      // to the signed type.
716
0
      QualType NewTy =
717
0
          Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
718
0
      RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
719
0
      RTy = NewTy;
720
0
      LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
721
0
      LTy = NewTy;
722
0
    }
723
0
  }
Unexecuted instantiation: void clang::ento::SMTConv::doIntTypeConversion<llvm::SMTExpr const*, &(clang::ento::SMTConv::fromCast(std::__1::shared_ptr<llvm::SMTSolver>&, llvm::SMTExpr const* const&, clang::QualType, unsigned long long, clang::QualType, unsigned long long))>(std::__1::shared_ptr<llvm::SMTSolver>&, clang::ASTContext&, llvm::SMTExpr const*&, clang::QualType&, llvm::SMTExpr const*&, clang::QualType&)
Unexecuted instantiation: void clang::ento::SMTConv::doIntTypeConversion<llvm::APSInt, &(clang::ento::SMTConv::castAPSInt(std::__1::shared_ptr<llvm::SMTSolver>&, llvm::APSInt const&, clang::QualType, unsigned long long, clang::QualType, unsigned long long))>(std::__1::shared_ptr<llvm::SMTSolver>&, clang::ASTContext&, llvm::APSInt&, clang::QualType&, llvm::APSInt&, clang::QualType&)
724
725
  // Perform implicit floating-point type conversion.
726
  // May modify all input parameters.
727
  // TODO: Refactor to use Sema::handleFloatConversion()
728
  template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
729
                                    QualType, uint64_t, QualType, uint64_t)>
730
  static inline void
731
  doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
732
0
                        QualType &LTy, T &RHS, QualType &RTy) {
733
0
    uint64_t LBitWidth = Ctx.getTypeSize(LTy);
734
0
    uint64_t RBitWidth = Ctx.getTypeSize(RTy);
735
736
    // Perform float-point type promotion
737
0
    if (!LTy->isRealFloatingType()) {
738
0
      LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
739
0
      LTy = RTy;
740
0
      LBitWidth = RBitWidth;
741
0
    }
742
0
    if (!RTy->isRealFloatingType()) {
743
0
      RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
744
0
      RTy = LTy;
745
0
      RBitWidth = LBitWidth;
746
0
    }
747
748
0
    if (LTy == RTy)
749
0
      return;
750
751
    // If we have two real floating types, convert the smaller operand to the
752
    // bigger result
753
    // Note: Safe to skip updating bitwidth because this must terminate
754
0
    int order = Ctx.getFloatingTypeOrder(LTy, RTy);
755
0
    if (order > 0) {
756
0
      RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
757
0
      RTy = LTy;
758
0
    } else if (order == 0) {
759
0
      LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
760
0
      LTy = RTy;
761
0
    } else {
762
0
      llvm_unreachable("Unsupported floating-point type cast!");
763
0
    }
764
0
  }
765
};
766
} // namespace ento
767
} // namespace clang
768
769
#endif