contrib/llvm/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

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