Coverage Report

Created: 2019-07-24 05:18

/Users/buildslave/jenkins/workspace/clang-stage2-coverage-R/llvm/tools/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
0
32
0
    if (Ty->isRealFloatingType())
33
0
      return Solver->getFloatSort(BitWidth);
34
0
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
0
46
0
    case UO_Not:
47
0
      return Solver->mkBVNot(Exp);
48
0
49
0
    case UO_LNot:
50
0
      return Solver->mkNot(Exp);
51
0
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
0
65
0
    case UO_LNot:
66
0
      return fromUnOp(Solver, Op, Exp);
67
0
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
0
98
0
    switch (Op) {
99
0
    // Multiplicative operators
100
0
    case BO_Mul:
101
0
      return Solver->mkBVMul(LHS, RHS);
102
0
103
0
    case BO_Div:
104
0
      return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);
105
0
106
0
    case BO_Rem:
107
0
      return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);
108
0
109
0
      // Additive operators
110
0
    case BO_Add:
111
0
      return Solver->mkBVAdd(LHS, RHS);
112
0
113
0
    case BO_Sub:
114
0
      return Solver->mkBVSub(LHS, RHS);
115
0
116
0
      // Bitwise shift operators
117
0
    case BO_Shl:
118
0
      return Solver->mkBVShl(LHS, RHS);
119
0
120
0
    case BO_Shr:
121
0
      return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);
122
0
123
0
      // Relational operators
124
0
    case BO_LT:
125
0
      return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);
126
0
127
0
    case BO_GT:
128
0
      return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);
129
0
130
0
    case BO_LE:
131
0
      return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);
132
0
133
0
    case BO_GE:
134
0
      return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);
135
0
136
0
      // Equality operators
137
0
    case BO_EQ:
138
0
      return Solver->mkEqual(LHS, RHS);
139
0
140
0
    case BO_NE:
141
0
      return fromUnOp(Solver, UO_LNot,
142
0
                      fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned));
143
0
144
0
      // Bitwise operators
145
0
    case BO_And:
146
0
      return Solver->mkBVAnd(LHS, RHS);
147
0
148
0
    case BO_Xor:
149
0
      return Solver->mkBVXor(LHS, RHS);
150
0
151
0
    case BO_Or:
152
0
      return Solver->mkBVOr(LHS, RHS);
153
0
154
0
      // Logical operators
155
0
    case BO_LAnd:
156
0
      return Solver->mkAnd(LHS, RHS);
157
0
158
0
    case BO_LOr:
159
0
      return Solver->mkOr(LHS, RHS);
160
0
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
0
208
0
    switch (Op) {
209
0
    // Multiplicative operators
210
0
    case BO_Mul:
211
0
      return Solver->mkFPMul(LHS, RHS);
212
0
213
0
    case BO_Div:
214
0
      return Solver->mkFPDiv(LHS, RHS);
215
0
216
0
    case BO_Rem:
217
0
      return Solver->mkFPRem(LHS, RHS);
218
0
219
0
      // Additive operators
220
0
    case BO_Add:
221
0
      return Solver->mkFPAdd(LHS, RHS);
222
0
223
0
    case BO_Sub:
224
0
      return Solver->mkFPSub(LHS, RHS);
225
0
226
0
      // Relational operators
227
0
    case BO_LT:
228
0
      return Solver->mkFPLt(LHS, RHS);
229
0
230
0
    case BO_GT:
231
0
      return Solver->mkFPGt(LHS, RHS);
232
0
233
0
    case BO_LE:
234
0
      return Solver->mkFPLe(LHS, RHS);
235
0
236
0
    case BO_GE:
237
0
      return Solver->mkFPGe(LHS, RHS);
238
0
239
0
      // Equality operators
240
0
    case BO_EQ:
241
0
      return Solver->mkFPEqual(LHS, RHS);
242
0
243
0
    case BO_NE:
244
0
      return fromFloatUnOp(Solver, UO_LNot,
245
0
                           fromFloatBinOp(Solver, LHS, BO_EQ, RHS));
246
0
247
0
      // Logical operators
248
0
    case BO_LAnd:
249
0
    case BO_LOr:
250
0
      return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false);
251
0
252
0
    default:;
253
0
    }
254
0
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
0
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
0
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
0
283
0
      if (ToBitWidth < FromBitWidth)
284
0
        return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
285
0
286
0
      // Both are bitvectors with the same width, ignore the type cast
287
0
      return Exp;
288
0
    }
289
0
290
0
    if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
291
0
      if (ToBitWidth != FromBitWidth)
292
0
        return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
293
0
294
0
      return Exp;
295
0
    }
296
0
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
0
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
0
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 fromData(llvm::SMTSolverRef &Solver,
323
                                          const SymbolID ID, const QualType &Ty,
324
0
                                          uint64_t BitWidth) {
325
0
    llvm::Twine Name = "$" + llvm::Twine(ID);
326
0
    return Solver->mkSymbol(Name.str().c_str(), mkSort(Solver, Ty, BitWidth));
327
0
  }
328
329
  // Wrapper to generate SMTSolverRef from SymbolCast data.
330
  static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,
331
                                             ASTContext &Ctx,
332
                                             const llvm::SMTExprRef &Exp,
333
0
                                             QualType FromTy, QualType ToTy) {
334
0
    return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
335
0
                    Ctx.getTypeSize(FromTy));
336
0
  }
337
338
  // Wrapper to generate SMTSolverRef from unpacked binary symbolic
339
  // expression. Sets the RetTy parameter. See getSMTSolverRef().
340
  static inline llvm::SMTExprRef
341
  getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
342
             const llvm::SMTExprRef &LHS, QualType LTy,
343
             BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS,
344
0
             QualType RTy, QualType *RetTy) {
345
0
    llvm::SMTExprRef NewLHS = LHS;
346
0
    llvm::SMTExprRef NewRHS = RHS;
347
0
    doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
348
0
349
0
    // Update the return type parameter if the output type has changed.
350
0
    if (RetTy) {
351
0
      // A boolean result can be represented as an integer type in C/C++, but at
352
0
      // this point we only care about the SMT sorts. Set it as a boolean type
353
0
      // to avoid subsequent SMT errors.
354
0
      if (BinaryOperator::isComparisonOp(Op) ||
355
0
          BinaryOperator::isLogicalOp(Op)) {
356
0
        *RetTy = Ctx.BoolTy;
357
0
      } else {
358
0
        *RetTy = LTy;
359
0
      }
360
0
361
0
      // If the two operands are pointers and the operation is a subtraction,
362
0
      // the result is of type ptrdiff_t, which is signed
363
0
      if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) {
364
0
        *RetTy = Ctx.getPointerDiffType();
365
0
      }
366
0
    }
367
0
368
0
    return LTy->isRealFloatingType()
369
0
               ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS)
370
0
               : fromBinOp(Solver, NewLHS, Op, NewRHS,
371
0
                           LTy->isSignedIntegerOrEnumerationType());
372
0
  }
373
374
  // Wrapper to generate SMTSolverRef from BinarySymExpr.
375
  // Sets the hasComparison and RetTy parameters. See getSMTSolverRef().
376
  static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver,
377
                                               ASTContext &Ctx,
378
                                               const BinarySymExpr *BSE,
379
                                               bool *hasComparison,
380
0
                                               QualType *RetTy) {
381
0
    QualType LTy, RTy;
382
0
    BinaryOperator::Opcode Op = BSE->getOpcode();
383
0
384
0
    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
385
0
      llvm::SMTExprRef LHS =
386
0
          getSymExpr(Solver, Ctx, SIE->getLHS(), &LTy, hasComparison);
387
0
      llvm::APSInt NewRInt;
388
0
      std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
389
0
      llvm::SMTExprRef RHS =
390
0
          Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
391
0
      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
392
0
    }
393
0
394
0
    if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
395
0
      llvm::APSInt NewLInt;
396
0
      std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
397
0
      llvm::SMTExprRef LHS =
398
0
          Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
399
0
      llvm::SMTExprRef RHS =
400
0
          getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
401
0
      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
402
0
    }
403
0
404
0
    if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
405
0
      llvm::SMTExprRef LHS =
406
0
          getSymExpr(Solver, Ctx, SSM->getLHS(), &LTy, hasComparison);
407
0
      llvm::SMTExprRef RHS =
408
0
          getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
409
0
      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
410
0
    }
411
0
412
0
    llvm_unreachable("Unsupported BinarySymExpr type!");
413
0
  }
414
415
  // Recursive implementation to unpack and generate symbolic expression.
416
  // Sets the hasComparison and RetTy parameters. See getExpr().
417
  static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
418
                                            ASTContext &Ctx, SymbolRef Sym,
419
                                            QualType *RetTy,
420
0
                                            bool *hasComparison) {
421
0
    if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
422
0
      if (RetTy)
423
0
        *RetTy = Sym->getType();
424
0
425
0
      return fromData(Solver, SD->getSymbolID(), Sym->getType(),
426
0
                      Ctx.getTypeSize(Sym->getType()));
427
0
    }
428
0
429
0
    if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
430
0
      if (RetTy)
431
0
        *RetTy = Sym->getType();
432
0
433
0
      QualType FromTy;
434
0
      llvm::SMTExprRef Exp =
435
0
          getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
436
0
437
0
      // Casting an expression with a comparison invalidates it. Note that this
438
0
      // must occur after the recursive call above.
439
0
      // e.g. (signed char) (x > 0)
440
0
      if (hasComparison)
441
0
        *hasComparison = false;
442
0
      return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
443
0
    }
444
0
445
0
    if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
446
0
      llvm::SMTExprRef Exp =
447
0
          getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
448
0
      // Set the hasComparison parameter, in post-order traversal order.
449
0
      if (hasComparison)
450
0
        *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
451
0
      return Exp;
452
0
    }
453
0
454
0
    llvm_unreachable("Unsupported SymbolRef type!");
455
0
  }
456
457
  // Generate an SMTSolverRef that represents the given symbolic expression.
458
  // Sets the hasComparison parameter if the expression has a comparison
459
  // operator. Sets the RetTy parameter to the final return type after
460
  // promotions and casts.
461
  static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
462
                                         ASTContext &Ctx, SymbolRef Sym,
463
                                         QualType *RetTy = nullptr,
464
0
                                         bool *hasComparison = nullptr) {
465
0
    if (hasComparison) {
466
0
      *hasComparison = false;
467
0
    }
468
0
469
0
    return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
470
0
  }
471
472
  // Generate an SMTSolverRef that compares the expression to zero.
473
  static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver,
474
                                             ASTContext &Ctx,
475
                                             const llvm::SMTExprRef &Exp,
476
0
                                             QualType Ty, bool Assumption) {
477
0
    if (Ty->isRealFloatingType()) {
478
0
      llvm::APFloat Zero =
479
0
          llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
480
0
      return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
481
0
                            Solver->mkFloat(Zero));
482
0
    }
483
0
484
0
    if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
485
0
        Ty->isBlockPointerType() || Ty->isReferenceType()) {
486
0
487
0
      // Skip explicit comparison for boolean types
488
0
      bool isSigned = Ty->isSignedIntegerOrEnumerationType();
489
0
      if (Ty->isBooleanType())
490
0
        return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
491
0
492
0
      return fromBinOp(
493
0
          Solver, Exp, Assumption ? BO_EQ : BO_NE,
494
0
          Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
495
0
          isSigned);
496
0
    }
497
0
498
0
    llvm_unreachable("Unsupported type for zero value!");
499
0
  }
500
501
  // Wrapper to generate SMTSolverRef from a range. If From == To, an
502
  // equality will be created instead.
503
  static inline llvm::SMTExprRef
504
  getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
505
0
               const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) {
506
0
    // Convert lower bound
507
0
    QualType FromTy;
508
0
    llvm::APSInt NewFromInt;
509
0
    std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
510
0
    llvm::SMTExprRef FromExp =
511
0
        Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
512
0
513
0
    // Convert symbol
514
0
    QualType SymTy;
515
0
    llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
516
0
517
0
    // Construct single (in)equality
518
0
    if (From == To)
519
0
      return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
520
0
                        FromExp, FromTy, /*RetTy=*/nullptr);
521
0
522
0
    QualType ToTy;
523
0
    llvm::APSInt NewToInt;
524
0
    std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
525
0
    llvm::SMTExprRef ToExp =
526
0
        Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
527
0
    assert(FromTy == ToTy && "Range values have different types!");
528
0
529
0
    // Construct two (in)equalities, and a logical and/or
530
0
    llvm::SMTExprRef LHS =
531
0
        getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
532
0
                   FromTy, /*RetTy=*/nullptr);
533
0
    llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
534
0
                                      InRange ? BO_LE : BO_GT, ToExp, ToTy,
535
0
                                      /*RetTy=*/nullptr);
536
0
537
0
    return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
538
0
                     SymTy->isSignedIntegerOrEnumerationType());
539
0
  }
540
541
  // Recover the QualType of an APSInt.
542
  // TODO: Refactor to put elsewhere
543
  static inline QualType getAPSIntType(ASTContext &Ctx,
544
0
                                       const llvm::APSInt &Int) {
545
0
    return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
546
0
  }
547
548
  // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
549
  static inline std::pair<llvm::APSInt, QualType>
550
0
  fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) {
551
0
    llvm::APSInt NewInt;
552
0
553
0
    // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
554
0
    // but the former is not available in Clang. Instead, extend the APSInt
555
0
    // directly.
556
0
    if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) {
557
0
      NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
558
0
    } else
559
0
      NewInt = Int;
560
0
561
0
    return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
562
0
  }
563
564
  // Perform implicit type conversion on binary symbolic expressions.
565
  // May modify all input parameters.
566
  // TODO: Refactor to use built-in conversion functions
567
  static inline void doTypeConversion(llvm::SMTSolverRef &Solver,
568
                                      ASTContext &Ctx, llvm::SMTExprRef &LHS,
569
                                      llvm::SMTExprRef &RHS, QualType &LTy,
570
0
                                      QualType &RTy) {
571
0
    assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
572
0
573
0
    // Perform type conversion
574
0
    if ((LTy->isIntegralOrEnumerationType() &&
575
0
         RTy->isIntegralOrEnumerationType()) &&
576
0
        (LTy->isArithmeticType() && RTy->isArithmeticType())) {
577
0
      SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(
578
0
          Solver, Ctx, LHS, LTy, RHS, RTy);
579
0
      return;
580
0
    }
581
0
582
0
    if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
583
0
      SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
584
0
          Solver, Ctx, LHS, LTy, RHS, RTy);
585
0
      return;
586
0
    }
587
0
588
0
    if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
589
0
        (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
590
0
        (LTy->isReferenceType() || RTy->isReferenceType())) {
591
0
      // TODO: Refactor to Sema::FindCompositePointerType(), and
592
0
      // Sema::CheckCompareOperands().
593
0
594
0
      uint64_t LBitWidth = Ctx.getTypeSize(LTy);
595
0
      uint64_t RBitWidth = Ctx.getTypeSize(RTy);
596
0
597
0
      // Cast the non-pointer type to the pointer type.
598
0
      // TODO: Be more strict about this.
599
0
      if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
600
0
          (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
601
0
          (LTy->isReferenceType() ^ RTy->isReferenceType())) {
602
0
        if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
603
0
            LTy->isReferenceType()) {
604
0
          LHS = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
605
0
          LTy = RTy;
606
0
        } else {
607
0
          RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
608
0
          RTy = LTy;
609
0
        }
610
0
      }
611
0
612
0
      // Cast the void pointer type to the non-void pointer type.
613
0
      // For void types, this assumes that the casted value is equal to the
614
0
      // value of the original pointer, and does not account for alignment
615
0
      // requirements.
616
0
      if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
617
0
        assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
618
0
               "Pointer types have different bitwidths!");
619
0
        if (RTy->isVoidPointerType())
620
0
          RTy = LTy;
621
0
        else
622
0
          LTy = RTy;
623
0
      }
624
0
625
0
      if (LTy == RTy)
626
0
        return;
627
0
    }
628
0
629
0
    // Fallback: for the solver, assume that these types don't really matter
630
0
    if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
631
0
        (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
632
0
      LTy = RTy;
633
0
      return;
634
0
    }
635
0
636
0
    // TODO: Refine behavior for invalid type casts
637
0
  }
638
639
  // Perform implicit integer type conversion.
640
  // May modify all input parameters.
641
  // TODO: Refactor to use Sema::handleIntegerConversion()
642
  template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
643
                                    QualType, uint64_t, QualType, uint64_t)>
644
  static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver,
645
                                         ASTContext &Ctx, T &LHS, QualType &LTy,
646
0
                                         T &RHS, QualType &RTy) {
647
0
    uint64_t LBitWidth = Ctx.getTypeSize(LTy);
648
0
    uint64_t RBitWidth = Ctx.getTypeSize(RTy);
649
0
650
0
    assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
651
0
    // Always perform integer promotion before checking type equality.
652
0
    // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
653
0
    if (LTy->isPromotableIntegerType()) {
654
0
      QualType NewTy = Ctx.getPromotedIntegerType(LTy);
655
0
      uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
656
0
      LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
657
0
      LTy = NewTy;
658
0
      LBitWidth = NewBitWidth;
659
0
    }
660
0
    if (RTy->isPromotableIntegerType()) {
661
0
      QualType NewTy = Ctx.getPromotedIntegerType(RTy);
662
0
      uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
663
0
      RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);
664
0
      RTy = NewTy;
665
0
      RBitWidth = NewBitWidth;
666
0
    }
667
0
668
0
    if (LTy == RTy)
669
0
      return;
670
0
671
0
    // Perform integer type conversion
672
0
    // Note: Safe to skip updating bitwidth because this must terminate
673
0
    bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
674
0
    bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
675
0
676
0
    int order = Ctx.getIntegerTypeOrder(LTy, RTy);
677
0
    if (isLSignedTy == isRSignedTy) {
678
0
      // Same signedness; use the higher-ranked type
679
0
      if (order == 1) {
680
0
        RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
681
0
        RTy = LTy;
682
0
      } else {
683
0
        LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
684
0
        LTy = RTy;
685
0
      }
686
0
    } else if (order != (isLSignedTy ? 1 : -1)) {
687
0
      // The unsigned type has greater than or equal rank to the
688
0
      // signed type, so use the unsigned type
689
0
      if (isRSignedTy) {
690
0
        RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
691
0
        RTy = LTy;
692
0
      } else {
693
0
        LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
694
0
        LTy = RTy;
695
0
      }
696
0
    } else if (LBitWidth != RBitWidth) {
697
0
      // The two types are different widths; if we are here, that
698
0
      // means the signed type is larger than the unsigned type, so
699
0
      // use the signed type.
700
0
      if (isLSignedTy) {
701
0
        RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
702
0
        RTy = LTy;
703
0
      } else {
704
0
        LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
705
0
        LTy = RTy;
706
0
      }
707
0
    } else {
708
0
      // The signed type is higher-ranked than the unsigned type,
709
0
      // but isn't actually any bigger (like unsigned int and long
710
0
      // on most 32-bit systems).  Use the unsigned type corresponding
711
0
      // to the signed type.
712
0
      QualType NewTy =
713
0
          Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
714
0
      RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
715
0
      RTy = NewTy;
716
0
      LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
717
0
      LTy = NewTy;
718
0
    }
719
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&)
720
721
  // Perform implicit floating-point type conversion.
722
  // May modify all input parameters.
723
  // TODO: Refactor to use Sema::handleFloatConversion()
724
  template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
725
                                    QualType, uint64_t, QualType, uint64_t)>
726
  static inline void
727
  doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
728
0
                        QualType &LTy, T &RHS, QualType &RTy) {
729
0
    uint64_t LBitWidth = Ctx.getTypeSize(LTy);
730
0
    uint64_t RBitWidth = Ctx.getTypeSize(RTy);
731
0
732
0
    // Perform float-point type promotion
733
0
    if (!LTy->isRealFloatingType()) {
734
0
      LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
735
0
      LTy = RTy;
736
0
      LBitWidth = RBitWidth;
737
0
    }
738
0
    if (!RTy->isRealFloatingType()) {
739
0
      RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
740
0
      RTy = LTy;
741
0
      RBitWidth = LBitWidth;
742
0
    }
743
0
744
0
    if (LTy == RTy)
745
0
      return;
746
0
747
0
    // If we have two real floating types, convert the smaller operand to the
748
0
    // bigger result
749
0
    // Note: Safe to skip updating bitwidth because this must terminate
750
0
    int order = Ctx.getFloatingTypeOrder(LTy, RTy);
751
0
    if (order > 0) {
752
0
      RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
753
0
      RTy = LTy;
754
0
    } else if (order == 0) {
755
0
      LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
756
0
      LTy = RTy;
757
0
    } else {
758
0
      llvm_unreachable("Unsupported floating-point type cast!");
759
0
    }
760
0
  }
761
};
762
} // namespace ento
763
} // namespace clang
764
765
#endif