contrib/llvm/tools/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

   1 //== Z3ConstraintManager.cpp --------------------------------*- 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 #include "clang/Basic/TargetInfo.h"
  11 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
  12 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
  13 #include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
  14
  15 #include "clang/Config/config.h"
  16
  17 using namespace clang;
  18 using namespace ento;
  19
  20 #if CLANG_ANALYZER_WITH_Z3
  21
  22 #include <z3.h>
  23
  24 // Forward declarations
  25 namespace {
  26 class Z3Expr;
  27 class ConstraintZ3 {};
  28 } // end anonymous namespace
  29
  30 typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
  31
  32 // Expansion of REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, Z3SetPair)
  33 namespace clang {
  34 namespace ento {
  35 template <>
  36 struct ProgramStateTrait<ConstraintZ3>
  37     : public ProgramStatePartialTrait<ConstraintZ3Ty> {
  38   static void *GDMIndex() {
  39     static int Index;
  40     return &Index;
  41   }
  42 };
  43 } // end namespace ento
  44 } // end namespace clang
  45
  46 namespace {
  47
  48 class Z3Config {
  49   friend class Z3Context;
  50
  51   Z3_config Config;
  52
  53 public:
  54   Z3Config() : Config(Z3_mk_config()) {
  55     // Enable model finding
  56     Z3_set_param_value(Config, "model", "true");
  57     // Disable proof generation
  58     Z3_set_param_value(Config, "proof", "false");
  59     // Set timeout to 15000ms = 15s
  60     Z3_set_param_value(Config, "timeout", "15000");
  61   }
  62
  63   ~Z3Config() { Z3_del_config(Config); }
  64 }; // end class Z3Config
  65
  66 class Z3Context {
  67   Z3_context ZC_P;
  68
  69 public:
  70   static Z3_context ZC;
  71
  72   Z3Context() : ZC_P(Z3_mk_context_rc(Z3Config().Config)) { ZC = ZC_P; }
  73
  74   ~Z3Context() {
  75     Z3_del_context(ZC);
  76     Z3_finalize_memory();
  77     ZC_P = nullptr;
  78   }
  79 }; // end class Z3Context
  80
  81 class Z3Sort {
  82   friend class Z3Expr;
  83
  84   Z3_sort Sort;
  85
  86   Z3Sort() : Sort(nullptr) {}
  87   Z3Sort(Z3_sort ZS) : Sort(ZS) {
  88     Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
  89   }
  90
  91 public:
  92   /// Override implicit copy constructor for correct reference counting.
  93   Z3Sort(const Z3Sort &Copy) : Sort(Copy.Sort) {
  94     Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
  95   }
  96
  97   /// Provide move constructor
  98   Z3Sort(Z3Sort &&Move) : Sort(nullptr) { *this = std::move(Move); }
  99
 100   /// Provide move assignment constructor
 101   Z3Sort &operator=(Z3Sort &&Move) {
 102     if (this != &Move) {
 103       if (Sort)
 104         Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
 105       Sort = Move.Sort;
 106       Move.Sort = nullptr;
 107     }
 108     return *this;
 109   }
 110
 111   ~Z3Sort() {
 112     if (Sort)
 113       Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
 114   }
 115
 116   // Return a boolean sort.
 117   static Z3Sort getBoolSort() { return Z3Sort(Z3_mk_bool_sort(Z3Context::ZC)); }
 118
 119   // Return an appropriate bitvector sort for the given bitwidth.
 120   static Z3Sort getBitvectorSort(unsigned BitWidth) {
 121     return Z3Sort(Z3_mk_bv_sort(Z3Context::ZC, BitWidth));
 122   }
 123
 124   // Return an appropriate floating-point sort for the given bitwidth.
 125   static Z3Sort getFloatSort(unsigned BitWidth) {
 126     Z3_sort Sort;
 127
 128     switch (BitWidth) {
 129     default:
 130       llvm_unreachable("Unsupported floating-point bitwidth!");
 131       break;
 132     case 16:
 133       Sort = Z3_mk_fpa_sort_16(Z3Context::ZC);
 134       break;
 135     case 32:
 136       Sort = Z3_mk_fpa_sort_32(Z3Context::ZC);
 137       break;
 138     case 64:
 139       Sort = Z3_mk_fpa_sort_64(Z3Context::ZC);
 140       break;
 141     case 128:
 142       Sort = Z3_mk_fpa_sort_128(Z3Context::ZC);
 143       break;
 144     }
 145     return Z3Sort(Sort);
 146   }
 147
 148   // Return an appropriate sort for the given AST.
 149   static Z3Sort getSort(Z3_ast AST) {
 150     return Z3Sort(Z3_get_sort(Z3Context::ZC, AST));
 151   }
 152
 153   Z3_sort_kind getSortKind() const {
 154     return Z3_get_sort_kind(Z3Context::ZC, Sort);
 155   }
 156
 157   unsigned getBitvectorSortSize() const {
 158     assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!");
 159     return Z3_get_bv_sort_size(Z3Context::ZC, Sort);
 160   }
 161
 162   unsigned getFloatSortSize() const {
 163     assert(getSortKind() == Z3_FLOATING_POINT_SORT &&
 164            "Not a floating-point sort!");
 165     return Z3_fpa_get_ebits(Z3Context::ZC, Sort) +
 166            Z3_fpa_get_sbits(Z3Context::ZC, Sort);
 167   }
 168
 169   bool operator==(const Z3Sort &Other) const {
 170     return Z3_is_eq_sort(Z3Context::ZC, Sort, Other.Sort);
 171   }
 172
 173   Z3Sort &operator=(const Z3Sort &Move) {
 174     Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Move.Sort));
 175     Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
 176     Sort = Move.Sort;
 177     return *this;
 178   }
 179
 180   void print(raw_ostream &OS) const {
 181     OS << Z3_sort_to_string(Z3Context::ZC, Sort);
 182   }
 183
 184   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 185 }; // end class Z3Sort
 186
 187 class Z3Expr {
 188   friend class Z3Model;
 189   friend class Z3Solver;
 190
 191   Z3_ast AST;
 192
 193   Z3Expr(Z3_ast ZA) : AST(ZA) { Z3_inc_ref(Z3Context::ZC, AST); }
 194
 195   // Return an appropriate floating-point rounding mode.
 196   static Z3Expr getFloatRoundingMode() {
 197     // TODO: Don't assume nearest ties to even rounding mode
 198     return Z3Expr(Z3_mk_fpa_rne(Z3Context::ZC));
 199   }
 200
 201   // Determine whether two float semantics are equivalent
 202   static bool areEquivalent(const llvm::fltSemantics &LHS,
 203                             const llvm::fltSemantics &RHS) {
 204     return (llvm::APFloat::semanticsPrecision(LHS) ==
 205             llvm::APFloat::semanticsPrecision(RHS)) &&
 206            (llvm::APFloat::semanticsMinExponent(LHS) ==
 207             llvm::APFloat::semanticsMinExponent(RHS)) &&
 208            (llvm::APFloat::semanticsMaxExponent(LHS) ==
 209             llvm::APFloat::semanticsMaxExponent(RHS)) &&
 210            (llvm::APFloat::semanticsSizeInBits(LHS) ==
 211             llvm::APFloat::semanticsSizeInBits(RHS));
 212   }
 213
 214 public:
 215   /// Override implicit copy constructor for correct reference counting.
 216   Z3Expr(const Z3Expr &Copy) : AST(Copy.AST) { Z3_inc_ref(Z3Context::ZC, AST); }
 217
 218   /// Provide move constructor
 219   Z3Expr(Z3Expr &&Move) : AST(nullptr) { *this = std::move(Move); }
 220
 221   /// Provide move assignment constructor
 222   Z3Expr &operator=(Z3Expr &&Move) {
 223     if (this != &Move) {
 224       if (AST)
 225         Z3_dec_ref(Z3Context::ZC, AST);
 226       AST = Move.AST;
 227       Move.AST = nullptr;
 228     }
 229     return *this;
 230   }
 231
 232   ~Z3Expr() {
 233     if (AST)
 234       Z3_dec_ref(Z3Context::ZC, AST);
 235   }
 236
 237   /// Get the corresponding IEEE floating-point type for a given bitwidth.
 238   static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
 239     switch (BitWidth) {
 240     default:
 241       llvm_unreachable("Unsupported floating-point semantics!");
 242       break;
 243     case 16:
 244       return llvm::APFloat::IEEEhalf();
 245     case 32:
 246       return llvm::APFloat::IEEEsingle();
 247     case 64:
 248       return llvm::APFloat::IEEEdouble();
 249     case 128:
 250       return llvm::APFloat::IEEEquad();
 251     }
 252   }
 253
 254   /// Construct a Z3Expr from a unary operator, given a Z3_context.
 255   static Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) {
 256     Z3_ast AST;
 257
 258     switch (Op) {
 259     default:
 260       llvm_unreachable("Unimplemented opcode");
 261       break;
 262
 263     case UO_Minus:
 264       AST = Z3_mk_bvneg(Z3Context::ZC, Exp.AST);
 265       break;
 266
 267     case UO_Not:
 268       AST = Z3_mk_bvnot(Z3Context::ZC, Exp.AST);
 269       break;
 270
 271     case UO_LNot:
 272       AST = Z3_mk_not(Z3Context::ZC, Exp.AST);
 273       break;
 274     }
 275
 276     return Z3Expr(AST);
 277   }
 278
 279   /// Construct a Z3Expr from a floating-point unary operator, given a
 280   /// Z3_context.
 281   static Z3Expr fromFloatUnOp(const UnaryOperator::Opcode Op,
 282                               const Z3Expr &Exp) {
 283     Z3_ast AST;
 284
 285     switch (Op) {
 286     default:
 287       llvm_unreachable("Unimplemented opcode");
 288       break;
 289
 290     case UO_Minus:
 291       AST = Z3_mk_fpa_neg(Z3Context::ZC, Exp.AST);
 292       break;
 293
 294     case UO_LNot:
 295       return Z3Expr::fromUnOp(Op, Exp);
 296     }
 297
 298     return Z3Expr(AST);
 299   }
 300
 301   /// Construct a Z3Expr from a n-ary binary operator.
 302   static Z3Expr fromNBinOp(const BinaryOperator::Opcode Op,
 303                            const std::vector<Z3_ast> &ASTs) {
 304     Z3_ast AST;
 305
 306     switch (Op) {
 307     default:
 308       llvm_unreachable("Unimplemented opcode");
 309       break;
 310
 311     case BO_LAnd:
 312       AST = Z3_mk_and(Z3Context::ZC, ASTs.size(), ASTs.data());
 313       break;
 314
 315     case BO_LOr:
 316       AST = Z3_mk_or(Z3Context::ZC, ASTs.size(), ASTs.data());
 317       break;
 318     }
 319
 320     return Z3Expr(AST);
 321   }
 322
 323   /// Construct a Z3Expr from a binary operator, given a Z3_context.
 324   static Z3Expr fromBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op,
 325                           const Z3Expr &RHS, bool isSigned) {
 326     Z3_ast AST;
 327
 328     assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
 329            "AST's must have the same sort!");
 330
 331     switch (Op) {
 332     default:
 333       llvm_unreachable("Unimplemented opcode");
 334       break;
 335
 336     // Multiplicative operators
 337     case BO_Mul:
 338       AST = Z3_mk_bvmul(Z3Context::ZC, LHS.AST, RHS.AST);
 339       break;
 340     case BO_Div:
 341       AST = isSigned ? Z3_mk_bvsdiv(Z3Context::ZC, LHS.AST, RHS.AST)
 342                      : Z3_mk_bvudiv(Z3Context::ZC, LHS.AST, RHS.AST);
 343       break;
 344     case BO_Rem:
 345       AST = isSigned ? Z3_mk_bvsrem(Z3Context::ZC, LHS.AST, RHS.AST)
 346                      : Z3_mk_bvurem(Z3Context::ZC, LHS.AST, RHS.AST);
 347       break;
 348
 349     // Additive operators
 350     case BO_Add:
 351       AST = Z3_mk_bvadd(Z3Context::ZC, LHS.AST, RHS.AST);
 352       break;
 353     case BO_Sub:
 354       AST = Z3_mk_bvsub(Z3Context::ZC, LHS.AST, RHS.AST);
 355       break;
 356
 357     // Bitwise shift operators
 358     case BO_Shl:
 359       AST = Z3_mk_bvshl(Z3Context::ZC, LHS.AST, RHS.AST);
 360       break;
 361     case BO_Shr:
 362       AST = isSigned ? Z3_mk_bvashr(Z3Context::ZC, LHS.AST, RHS.AST)
 363                      : Z3_mk_bvlshr(Z3Context::ZC, LHS.AST, RHS.AST);
 364       break;
 365
 366     // Relational operators
 367     case BO_LT:
 368       AST = isSigned ? Z3_mk_bvslt(Z3Context::ZC, LHS.AST, RHS.AST)
 369                      : Z3_mk_bvult(Z3Context::ZC, LHS.AST, RHS.AST);
 370       break;
 371     case BO_GT:
 372       AST = isSigned ? Z3_mk_bvsgt(Z3Context::ZC, LHS.AST, RHS.AST)
 373                      : Z3_mk_bvugt(Z3Context::ZC, LHS.AST, RHS.AST);
 374       break;
 375     case BO_LE:
 376       AST = isSigned ? Z3_mk_bvsle(Z3Context::ZC, LHS.AST, RHS.AST)
 377                      : Z3_mk_bvule(Z3Context::ZC, LHS.AST, RHS.AST);
 378       break;
 379     case BO_GE:
 380       AST = isSigned ? Z3_mk_bvsge(Z3Context::ZC, LHS.AST, RHS.AST)
 381                      : Z3_mk_bvuge(Z3Context::ZC, LHS.AST, RHS.AST);
 382       break;
 383
 384     // Equality operators
 385     case BO_EQ:
 386       AST = Z3_mk_eq(Z3Context::ZC, LHS.AST, RHS.AST);
 387       break;
 388     case BO_NE:
 389       return Z3Expr::fromUnOp(UO_LNot,
 390                               Z3Expr::fromBinOp(LHS, BO_EQ, RHS, isSigned));
 391       break;
 392
 393     // Bitwise operators
 394     case BO_And:
 395       AST = Z3_mk_bvand(Z3Context::ZC, LHS.AST, RHS.AST);
 396       break;
 397     case BO_Xor:
 398       AST = Z3_mk_bvxor(Z3Context::ZC, LHS.AST, RHS.AST);
 399       break;
 400     case BO_Or:
 401       AST = Z3_mk_bvor(Z3Context::ZC, LHS.AST, RHS.AST);
 402       break;
 403
 404     // Logical operators
 405     case BO_LAnd:
 406     case BO_LOr: {
 407       std::vector<Z3_ast> Args = {LHS.AST, RHS.AST};
 408       return Z3Expr::fromNBinOp(Op, Args);
 409     }
 410     }
 411
 412     return Z3Expr(AST);
 413   }
 414
 415   /// Construct a Z3Expr from a special floating-point binary operator, given
 416   /// a Z3_context.
 417   static Z3Expr fromFloatSpecialBinOp(const Z3Expr &LHS,
 418                                       const BinaryOperator::Opcode Op,
 419                                       const llvm::APFloat::fltCategory &RHS) {
 420     Z3_ast AST;
 421
 422     switch (Op) {
 423     default:
 424       llvm_unreachable("Unimplemented opcode");
 425       break;
 426
 427     // Equality operators
 428     case BO_EQ:
 429       switch (RHS) {
 430       case llvm::APFloat::fcInfinity:
 431         AST = Z3_mk_fpa_is_infinite(Z3Context::ZC, LHS.AST);
 432         break;
 433       case llvm::APFloat::fcNaN:
 434         AST = Z3_mk_fpa_is_nan(Z3Context::ZC, LHS.AST);
 435         break;
 436       case llvm::APFloat::fcNormal:
 437         AST = Z3_mk_fpa_is_normal(Z3Context::ZC, LHS.AST);
 438         break;
 439       case llvm::APFloat::fcZero:
 440         AST = Z3_mk_fpa_is_zero(Z3Context::ZC, LHS.AST);
 441         break;
 442       }
 443       break;
 444     case BO_NE:
 445       return Z3Expr::fromFloatUnOp(
 446           UO_LNot, Z3Expr::fromFloatSpecialBinOp(LHS, BO_EQ, RHS));
 447       break;
 448     }
 449
 450     return Z3Expr(AST);
 451   }
 452
 453   /// Construct a Z3Expr from a floating-point binary operator, given a
 454   /// Z3_context.
 455   static Z3Expr fromFloatBinOp(const Z3Expr &LHS,
 456                                const BinaryOperator::Opcode Op,
 457                                const Z3Expr &RHS) {
 458     Z3_ast AST;
 459
 460     assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
 461            "AST's must have the same sort!");
 462
 463     switch (Op) {
 464     default:
 465       llvm_unreachable("Unimplemented opcode");
 466       break;
 467
 468     // Multiplicative operators
 469     case BO_Mul: {
 470       Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
 471       AST = Z3_mk_fpa_mul(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
 472       break;
 473     }
 474     case BO_Div: {
 475       Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
 476       AST = Z3_mk_fpa_div(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
 477       break;
 478     }
 479     case BO_Rem:
 480       AST = Z3_mk_fpa_rem(Z3Context::ZC, LHS.AST, RHS.AST);
 481       break;
 482
 483     // Additive operators
 484     case BO_Add: {
 485       Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
 486       AST = Z3_mk_fpa_add(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
 487       break;
 488     }
 489     case BO_Sub: {
 490       Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
 491       AST = Z3_mk_fpa_sub(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
 492       break;
 493     }
 494
 495     // Relational operators
 496     case BO_LT:
 497       AST = Z3_mk_fpa_lt(Z3Context::ZC, LHS.AST, RHS.AST);
 498       break;
 499     case BO_GT:
 500       AST = Z3_mk_fpa_gt(Z3Context::ZC, LHS.AST, RHS.AST);
 501       break;
 502     case BO_LE:
 503       AST = Z3_mk_fpa_leq(Z3Context::ZC, LHS.AST, RHS.AST);
 504       break;
 505     case BO_GE:
 506       AST = Z3_mk_fpa_geq(Z3Context::ZC, LHS.AST, RHS.AST);
 507       break;
 508
 509     // Equality operators
 510     case BO_EQ:
 511       AST = Z3_mk_fpa_eq(Z3Context::ZC, LHS.AST, RHS.AST);
 512       break;
 513     case BO_NE:
 514       return Z3Expr::fromFloatUnOp(UO_LNot,
 515                                    Z3Expr::fromFloatBinOp(LHS, BO_EQ, RHS));
 516       break;
 517
 518     // Logical operators
 519     case BO_LAnd:
 520     case BO_LOr:
 521       return Z3Expr::fromBinOp(LHS, Op, RHS, false);
 522     }
 523
 524     return Z3Expr(AST);
 525   }
 526
 527   /// Construct a Z3Expr from a SymbolData, given a Z3_context.
 528   static Z3Expr fromData(const SymbolID ID, bool isBool, bool isFloat,
 529                          uint64_t BitWidth) {
 530     llvm::Twine Name = "$" + llvm::Twine(ID);
 531
 532     Z3Sort Sort;
 533     if (isBool)
 534       Sort = Z3Sort::getBoolSort();
 535     else if (isFloat)
 536       Sort = Z3Sort::getFloatSort(BitWidth);
 537     else
 538       Sort = Z3Sort::getBitvectorSort(BitWidth);
 539
 540     Z3_symbol Symbol = Z3_mk_string_symbol(Z3Context::ZC, Name.str().c_str());
 541     Z3_ast AST = Z3_mk_const(Z3Context::ZC, Symbol, Sort.Sort);
 542     return Z3Expr(AST);
 543   }
 544
 545   /// Construct a Z3Expr from a SymbolCast, given a Z3_context.
 546   static Z3Expr fromCast(const Z3Expr &Exp, QualType ToTy, uint64_t ToBitWidth,
 547                          QualType FromTy, uint64_t FromBitWidth) {
 548     Z3_ast AST;
 549
 550     if ((FromTy->isIntegralOrEnumerationType() &&
 551          ToTy->isIntegralOrEnumerationType()) ||
 552         (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
 553         (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
 554         (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
 555       // Special case: Z3 boolean type is distinct from bitvector type, so
 556       // must use if-then-else expression instead of direct cast
 557       if (FromTy->isBooleanType()) {
 558         assert(ToBitWidth > 0 && "BitWidth must be positive!");
 559         Z3Expr Zero = Z3Expr::fromInt("0", ToBitWidth);
 560         Z3Expr One = Z3Expr::fromInt("1", ToBitWidth);
 561         AST = Z3_mk_ite(Z3Context::ZC, Exp.AST, One.AST, Zero.AST);
 562       } else if (ToBitWidth > FromBitWidth) {
 563         AST = FromTy->isSignedIntegerOrEnumerationType()
 564                   ? Z3_mk_sign_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,
 565                                    Exp.AST)
 566                   : Z3_mk_zero_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,
 567                                    Exp.AST);
 568       } else if (ToBitWidth < FromBitWidth) {
 569         AST = Z3_mk_extract(Z3Context::ZC, ToBitWidth - 1, 0, Exp.AST);
 570       } else {
 571         // Both are bitvectors with the same width, ignore the type cast
 572         return Exp;
 573       }
 574     } else if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
 575       if (ToBitWidth != FromBitWidth) {
 576         Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
 577         Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
 578         AST = Z3_mk_fpa_to_fp_float(Z3Context::ZC, RoundingMode.AST, Exp.AST,
 579                                     Sort.Sort);
 580       } else {
 581         return Exp;
 582       }
 583     } else if (FromTy->isIntegralOrEnumerationType() &&
 584                ToTy->isRealFloatingType()) {
 585       Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
 586       Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
 587       AST = FromTy->isSignedIntegerOrEnumerationType()
 588                 ? Z3_mk_fpa_to_fp_signed(Z3Context::ZC, RoundingMode.AST,
 589                                          Exp.AST, Sort.Sort)
 590                 : Z3_mk_fpa_to_fp_unsigned(Z3Context::ZC, RoundingMode.AST,
 591                                            Exp.AST, Sort.Sort);
 592     } else if (FromTy->isRealFloatingType() &&
 593                ToTy->isIntegralOrEnumerationType()) {
 594       Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
 595       AST = ToTy->isSignedIntegerOrEnumerationType()
 596                 ? Z3_mk_fpa_to_sbv(Z3Context::ZC, RoundingMode.AST, Exp.AST,
 597                                    ToBitWidth)
 598                 : Z3_mk_fpa_to_ubv(Z3Context::ZC, RoundingMode.AST, Exp.AST,
 599                                    ToBitWidth);
 600     } else {
 601       llvm_unreachable("Unsupported explicit type cast!");
 602     }
 603
 604     return Z3Expr(AST);
 605   }
 606
 607   /// Construct a Z3Expr from a boolean, given a Z3_context.
 608   static Z3Expr fromBoolean(const bool Bool) {
 609     Z3_ast AST = Bool ? Z3_mk_true(Z3Context::ZC) : Z3_mk_false(Z3Context::ZC);
 610     return Z3Expr(AST);
 611   }
 612
 613   /// Construct a Z3Expr from a finite APFloat, given a Z3_context.
 614   static Z3Expr fromAPFloat(const llvm::APFloat &Float) {
 615     Z3_ast AST;
 616     Z3Sort Sort = Z3Sort::getFloatSort(
 617         llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
 618
 619     llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true);
 620     Z3Expr Z3Int = Z3Expr::fromAPSInt(Int);
 621     AST = Z3_mk_fpa_to_fp_bv(Z3Context::ZC, Z3Int.AST, Sort.Sort);
 622
 623     return Z3Expr(AST);
 624   }
 625
 626   /// Construct a Z3Expr from an APSInt, given a Z3_context.
 627   static Z3Expr fromAPSInt(const llvm::APSInt &Int) {
 628     Z3Sort Sort = Z3Sort::getBitvectorSort(Int.getBitWidth());
 629     Z3_ast AST =
 630         Z3_mk_numeral(Z3Context::ZC, Int.toString(10).c_str(), Sort.Sort);
 631     return Z3Expr(AST);
 632   }
 633
 634   /// Construct a Z3Expr from an integer, given a Z3_context.
 635   static Z3Expr fromInt(const char *Int, uint64_t BitWidth) {
 636     Z3Sort Sort = Z3Sort::getBitvectorSort(BitWidth);
 637     Z3_ast AST = Z3_mk_numeral(Z3Context::ZC, Int, Sort.Sort);
 638     return Z3Expr(AST);
 639   }
 640
 641   /// Construct an APFloat from a Z3Expr, given the AST representation
 642   static bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST,
 643                         llvm::APFloat &Float, bool useSemantics = true) {
 644     assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT &&
 645            "Unsupported sort to floating-point!");
 646
 647     llvm::APSInt Int(Sort.getFloatSortSize(), true);
 648     const llvm::fltSemantics &Semantics =
 649         Z3Expr::getFloatSemantics(Sort.getFloatSortSize());
 650     Z3Sort BVSort = Z3Sort::getBitvectorSort(Sort.getFloatSortSize());
 651     if (!Z3Expr::toAPSInt(BVSort, AST, Int, true)) {
 652       return false;
 653     }
 654
 655     if (useSemantics &&
 656         !Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) {
 657       assert(false && "Floating-point types don't match!");
 658       return false;
 659     }
 660
 661     Float = llvm::APFloat(Semantics, Int);
 662     return true;
 663   }
 664
 665   /// Construct an APSInt from a Z3Expr, given the AST representation
 666   static bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int,
 667                        bool useSemantics = true) {
 668     switch (Sort.getSortKind()) {
 669     default:
 670       llvm_unreachable("Unsupported sort to integer!");
 671     case Z3_BV_SORT: {
 672       if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) {
 673         assert(false && "Bitvector types don't match!");
 674         return false;
 675       }
 676
 677       uint64_t Value[2];
 678       // Force cast because Z3 defines __uint64 to be a unsigned long long
 679       // type, which isn't compatible with a unsigned long type, even if they
 680       // are the same size.
 681       Z3_get_numeral_uint64(Z3Context::ZC, AST,
 682                             reinterpret_cast<__uint64 *>(&Value[0]));
 683       if (Sort.getBitvectorSortSize() <= 64) {
 684         Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true);
 685       } else if (Sort.getBitvectorSortSize() == 128) {
 686         Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST));
 687         Z3_get_numeral_uint64(Z3Context::ZC, AST,
 688                               reinterpret_cast<__uint64 *>(&Value[1]));
 689         Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true);
 690       } else {
 691         assert(false && "Bitwidth not supported!");
 692         return false;
 693       }
 694       return true;
 695     }
 696     case Z3_BOOL_SORT:
 697       if (useSemantics && Int.getBitWidth() < 1) {
 698         assert(false && "Boolean type doesn't match!");
 699         return false;
 700       }
 701       Int = llvm::APSInt(
 702           llvm::APInt(Int.getBitWidth(),
 703                       Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1
 704                                                                          : 0),
 705           true);
 706       return true;
 707     }
 708   }
 709
 710   void Profile(llvm::FoldingSetNodeID &ID) const {
 711     ID.AddInteger(Z3_get_ast_hash(Z3Context::ZC, AST));
 712   }
 713
 714   bool operator<(const Z3Expr &Other) const {
 715     llvm::FoldingSetNodeID ID1, ID2;
 716     Profile(ID1);
 717     Other.Profile(ID2);
 718     return ID1 < ID2;
 719   }
 720
 721   /// Comparison of AST equality, not model equivalence.
 722   bool operator==(const Z3Expr &Other) const {
 723     assert(Z3_is_eq_sort(Z3Context::ZC, Z3_get_sort(Z3Context::ZC, AST),
 724                          Z3_get_sort(Z3Context::ZC, Other.AST)) &&
 725            "AST's must have the same sort");
 726     return Z3_is_eq_ast(Z3Context::ZC, AST, Other.AST);
 727   }
 728
 729   /// Override implicit move constructor for correct reference counting.
 730   Z3Expr &operator=(const Z3Expr &Move) {
 731     Z3_inc_ref(Z3Context::ZC, Move.AST);
 732     Z3_dec_ref(Z3Context::ZC, AST);
 733     AST = Move.AST;
 734     return *this;
 735   }
 736
 737   void print(raw_ostream &OS) const {
 738     OS << Z3_ast_to_string(Z3Context::ZC, AST);
 739   }
 740
 741   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 742 }; // end class Z3Expr
 743
 744 class Z3Model {
 745   Z3_model Model;
 746
 747 public:
 748   Z3Model(Z3_model ZM) : Model(ZM) { Z3_model_inc_ref(Z3Context::ZC, Model); }
 749
 750   /// Override implicit copy constructor for correct reference counting.
 751   Z3Model(const Z3Model &Copy) : Model(Copy.Model) {
 752     Z3_model_inc_ref(Z3Context::ZC, Model);
 753   }
 754
 755   /// Provide move constructor
 756   Z3Model(Z3Model &&Move) : Model(nullptr) { *this = std::move(Move); }
 757
 758   /// Provide move assignment constructor
 759   Z3Model &operator=(Z3Model &&Move) {
 760     if (this != &Move) {
 761       if (Model)
 762         Z3_model_dec_ref(Z3Context::ZC, Model);
 763       Model = Move.Model;
 764       Move.Model = nullptr;
 765     }
 766     return *this;
 767   }
 768
 769   ~Z3Model() {
 770     if (Model)
 771       Z3_model_dec_ref(Z3Context::ZC, Model);
 772   }
 773
 774   /// Given an expression, extract the value of this operand in the model.
 775   bool getInterpretation(const Z3Expr &Exp, llvm::APSInt &Int) const {
 776     Z3_func_decl Func =
 777         Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
 778     if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
 779       return false;
 780
 781     Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
 782     Z3Sort Sort = Z3Sort::getSort(Assign);
 783     return Z3Expr::toAPSInt(Sort, Assign, Int, true);
 784   }
 785
 786   /// Given an expression, extract the value of this operand in the model.
 787   bool getInterpretation(const Z3Expr &Exp, llvm::APFloat &Float) const {
 788     Z3_func_decl Func =
 789         Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
 790     if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
 791       return false;
 792
 793     Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
 794     Z3Sort Sort = Z3Sort::getSort(Assign);
 795     return Z3Expr::toAPFloat(Sort, Assign, Float, true);
 796   }
 797
 798   void print(raw_ostream &OS) const {
 799     OS << Z3_model_to_string(Z3Context::ZC, Model);
 800   }
 801
 802   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 803 }; // end class Z3Model
 804
 805 class Z3Solver {
 806   friend class Z3ConstraintManager;
 807
 808   Z3_solver Solver;
 809
 810   Z3Solver(Z3_solver ZS) : Solver(ZS) {
 811     Z3_solver_inc_ref(Z3Context::ZC, Solver);
 812   }
 813
 814 public:
 815   /// Override implicit copy constructor for correct reference counting.
 816   Z3Solver(const Z3Solver &Copy) : Solver(Copy.Solver) {
 817     Z3_solver_inc_ref(Z3Context::ZC, Solver);
 818   }
 819
 820   /// Provide move constructor
 821   Z3Solver(Z3Solver &&Move) : Solver(nullptr) { *this = std::move(Move); }
 822
 823   /// Provide move assignment constructor
 824   Z3Solver &operator=(Z3Solver &&Move) {
 825     if (this != &Move) {
 826       if (Solver)
 827         Z3_solver_dec_ref(Z3Context::ZC, Solver);
 828       Solver = Move.Solver;
 829       Move.Solver = nullptr;
 830     }
 831     return *this;
 832   }
 833
 834   ~Z3Solver() {
 835     if (Solver)
 836       Z3_solver_dec_ref(Z3Context::ZC, Solver);
 837   }
 838
 839   /// Given a constraint, add it to the solver
 840   void addConstraint(const Z3Expr &Exp) {
 841     Z3_solver_assert(Z3Context::ZC, Solver, Exp.AST);
 842   }
 843
 844   /// Given a program state, construct the logical conjunction and add it to
 845   /// the solver
 846   void addStateConstraints(ProgramStateRef State) {
 847     // TODO: Don't add all the constraints, only the relevant ones
 848     ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
 849     ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
 850
 851     // Construct the logical AND of all the constraints
 852     if (I != IE) {
 853       std::vector<Z3_ast> ASTs;
 854
 855       while (I != IE)
 856         ASTs.push_back(I++->second.AST);
 857
 858       Z3Expr Conj = Z3Expr::fromNBinOp(BO_LAnd, ASTs);
 859       addConstraint(Conj);
 860     }
 861   }
 862
 863   /// Check if the constraints are satisfiable
 864   Z3_lbool check() { return Z3_solver_check(Z3Context::ZC, Solver); }
 865
 866   /// Push the current solver state
 867   void push() { return Z3_solver_push(Z3Context::ZC, Solver); }
 868
 869   /// Pop the previous solver state
 870   void pop(unsigned NumStates = 1) {
 871     assert(Z3_solver_get_num_scopes(Z3Context::ZC, Solver) >= NumStates);
 872     return Z3_solver_pop(Z3Context::ZC, Solver, NumStates);
 873   }
 874
 875   /// Get a model from the solver. Caller should check the model is
 876   /// satisfiable.
 877   Z3Model getModel() {
 878     return Z3Model(Z3_solver_get_model(Z3Context::ZC, Solver));
 879   }
 880
 881   /// Reset the solver and remove all constraints.
 882   void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
 883 }; // end class Z3Solver
 884
 885 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
 886   llvm::report_fatal_error("Z3 error: " +
 887                            llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
 888 }
 889
 890 class Z3ConstraintManager : public SimpleConstraintManager {
 891   Z3Context Context;
 892   mutable Z3Solver Solver;
 893
 894 public:
 895   Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
 896       : SimpleConstraintManager(SE, SB),
 897         Solver(Z3_mk_simple_solver(Z3Context::ZC)) {
 898     Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler);
 899   }
 900
 901   //===------------------------------------------------------------------===//
 902   // Implementation for interface from ConstraintManager.
 903   //===------------------------------------------------------------------===//
 904
 905   bool canReasonAbout(SVal X) const override;
 906
 907   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
 908
 909   const llvm::APSInt *getSymVal(ProgramStateRef State,
 910                                 SymbolRef Sym) const override;
 911
 912   ProgramStateRef removeDeadBindings(ProgramStateRef St,
 913                                      SymbolReaper &SymReaper) override;
 914
 915   void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
 916              const char *sep) override;
 917
 918   //===------------------------------------------------------------------===//
 919   // Implementation for interface from SimpleConstraintManager.
 920   //===------------------------------------------------------------------===//
 921
 922   ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
 923                             bool Assumption) override;
 924
 925   ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
 926                                           const llvm::APSInt &From,
 927                                           const llvm::APSInt &To,
 928                                           bool InRange) override;
 929
 930   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
 931                                        bool Assumption) override;
 932
 933 private:
 934   //===------------------------------------------------------------------===//
 935   // Internal implementation.
 936   //===------------------------------------------------------------------===//
 937
 938   // Check whether a new model is satisfiable, and update the program state.
 939   ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym,
 940                                const Z3Expr &Exp);
 941
 942   // Generate and check a Z3 model, using the given constraint.
 943   Z3_lbool checkZ3Model(ProgramStateRef State, const Z3Expr &Exp) const;
 944
 945   // Generate a Z3Expr that represents the given symbolic expression.
 946   // Sets the hasComparison parameter if the expression has a comparison
 947   // operator.
 948   // Sets the RetTy parameter to the final return type after promotions and
 949   // casts.
 950   Z3Expr getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,
 951                    bool *hasComparison = nullptr) const;
 952
 953   // Generate a Z3Expr that takes the logical not of an expression.
 954   Z3Expr getZ3NotExpr(const Z3Expr &Exp) const;
 955
 956   // Generate a Z3Expr that compares the expression to zero.
 957   Z3Expr getZ3ZeroExpr(const Z3Expr &Exp, QualType RetTy,
 958                        bool Assumption) const;
 959
 960   // Recursive implementation to unpack and generate symbolic expression.
 961   // Sets the hasComparison and RetTy parameters. See getZ3Expr().
 962   Z3Expr getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
 963                       bool *hasComparison) const;
 964
 965   // Wrapper to generate Z3Expr from SymbolData.
 966   Z3Expr getZ3DataExpr(const SymbolID ID, QualType Ty) const;
 967
 968   // Wrapper to generate Z3Expr from SymbolCast.
 969   Z3Expr getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, QualType Ty) const;
 970
 971   // Wrapper to generate Z3Expr from BinarySymExpr.
 972   // Sets the hasComparison and RetTy parameters. See getZ3Expr().
 973   Z3Expr getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
 974                          QualType *RetTy) const;
 975
 976   // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
 977   // Sets the RetTy parameter. See getZ3Expr().
 978   Z3Expr getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
 979                       BinaryOperator::Opcode Op, const Z3Expr &RHS,
 980                       QualType RTy, QualType *RetTy) const;
 981
 982   //===------------------------------------------------------------------===//
 983   // Helper functions.
 984   //===------------------------------------------------------------------===//
 985
 986   // Recover the QualType of an APSInt.
 987   // TODO: Refactor to put elsewhere
 988   QualType getAPSIntType(const llvm::APSInt &Int) const;
 989
 990   // Perform implicit type conversion on binary symbolic expressions.
 991   // May modify all input parameters.
 992   // TODO: Refactor to use built-in conversion functions
 993   void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType &LTy,
 994                         QualType &RTy) const;
 995
 996   // Perform implicit integer type conversion.
 997   // May modify all input parameters.
 998   // TODO: Refactor to use Sema::handleIntegerConversion()
 999   template <typename T,
1000             T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1001   void doIntTypeConversion(T &LHS, QualType &LTy, T &RHS, QualType &RTy) const;
1002
1003   // Perform implicit floating-point type conversion.
1004   // May modify all input parameters.
1005   // TODO: Refactor to use Sema::handleFloatConversion()
1006   template <typename T,
1007             T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1008   void doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
1009                              QualType &RTy) const;
1010
1011   // Callback function for doCast parameter on APSInt type.
1012   static llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy,
1013                                  uint64_t ToWidth, QualType FromTy,
1014                                  uint64_t FromWidth);
1015 }; // end class Z3ConstraintManager
1016
1017 Z3_context Z3Context::ZC;
1018
1019 } // end anonymous namespace
1020
1021 ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State,
1022                                                SymbolRef Sym, bool Assumption) {
1023   QualType RetTy;
1024   bool hasComparison;
1025
1026   Z3Expr Exp = getZ3Expr(Sym, &RetTy, &hasComparison);
1027   // Create zero comparison for implicit boolean cast, with reversed assumption
1028   if (!hasComparison && !RetTy->isBooleanType())
1029     return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption));
1030
1031   return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));
1032 }
1033
1034 ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
1035     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
1036     const llvm::APSInt &To, bool InRange) {
1037   QualType RetTy;
1038   // The expression may be casted, so we cannot call getZ3DataExpr() directly
1039   Z3Expr Exp = getZ3Expr(Sym, &RetTy);
1040
1041   assert((getAPSIntType(From) == getAPSIntType(To)) &&
1042          "Range values have different types!");
1043   QualType RTy = getAPSIntType(From);
1044   bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
1045   Z3Expr FromExp = Z3Expr::fromAPSInt(From);
1046   Z3Expr ToExp = Z3Expr::fromAPSInt(To);
1047
1048   // Construct single (in)equality
1049   if (From == To)
1050     return assumeZ3Expr(State, Sym,
1051                         getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
1052                                      FromExp, RTy, nullptr));
1053
1054   // Construct two (in)equalities, and a logical and/or
1055   Z3Expr LHS =
1056       getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
1057   Z3Expr RHS =
1058       getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
1059   return assumeZ3Expr(
1060       State, Sym,
1061       Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
1062 }
1063
1064 ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
1065                                                           SymbolRef Sym,
1066                                                           bool Assumption) {
1067   // Skip anything that is unsupported
1068   return State;
1069 }
1070
1071 bool Z3ConstraintManager::canReasonAbout(SVal X) const {
1072   const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
1073
1074   Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
1075   if (!SymVal)
1076     return true;
1077
1078   const SymExpr *Sym = SymVal->getSymbol();
1079   do {
1080     QualType Ty = Sym->getType();
1081
1082     // Complex types are not modeled
1083     if (Ty->isComplexType() || Ty->isComplexIntegerType())
1084       return false;
1085
1086     // Non-IEEE 754 floating-point types are not modeled
1087     if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
1088          (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
1089           &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
1090       return false;
1091
1092     if (isa<SymbolData>(Sym)) {
1093       break;
1094     } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
1095       Sym = SC->getOperand();
1096     } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1097       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
1098         Sym = SIE->getLHS();
1099       } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
1100         Sym = ISE->getRHS();
1101       } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
1102         return canReasonAbout(nonloc::SymbolVal(SSM->getLHS())) &&
1103                canReasonAbout(nonloc::SymbolVal(SSM->getRHS()));
1104       } else {
1105         llvm_unreachable("Unsupported binary expression to reason about!");
1106       }
1107     } else {
1108       llvm_unreachable("Unsupported expression to reason about!");
1109     }
1110   } while (Sym);
1111
1112   return true;
1113 }
1114
1115 ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State,
1116                                                  SymbolRef Sym) {
1117   QualType RetTy;
1118   // The expression may be casted, so we cannot call getZ3DataExpr() directly
1119   Z3Expr VarExp = getZ3Expr(Sym, &RetTy);
1120   Z3Expr Exp = getZ3ZeroExpr(VarExp, RetTy, true);
1121   // Negate the constraint
1122   Z3Expr NotExp = getZ3ZeroExpr(VarExp, RetTy, false);
1123
1124   Solver.reset();
1125   Solver.addStateConstraints(State);
1126
1127   Solver.push();
1128   Solver.addConstraint(Exp);
1129   Z3_lbool isSat = Solver.check();
1130
1131   Solver.pop();
1132   Solver.addConstraint(NotExp);
1133   Z3_lbool isNotSat = Solver.check();
1134
1135   // Zero is the only possible solution
1136   if (isSat == Z3_L_TRUE && isNotSat == Z3_L_FALSE)
1137     return true;
1138   // Zero is not a solution
1139   else if (isSat == Z3_L_FALSE && isNotSat == Z3_L_TRUE)
1140     return false;
1141
1142   // Zero may be a solution
1143   return ConditionTruthVal();
1144 }
1145
1146 const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
1147                                                    SymbolRef Sym) const {
1148   BasicValueFactory &BV = getBasicVals();
1149   ASTContext &Ctx = BV.getContext();
1150
1151   if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
1152     QualType Ty = Sym->getType();
1153     assert(!Ty->isRealFloatingType());
1154     llvm::APSInt Value(Ctx.getTypeSize(Ty),
1155                        !Ty->isSignedIntegerOrEnumerationType());
1156
1157     Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
1158
1159     Solver.reset();
1160     Solver.addStateConstraints(State);
1161
1162     // Constraints are unsatisfiable
1163     if (Solver.check() != Z3_L_TRUE)
1164       return nullptr;
1165
1166     Z3Model Model = Solver.getModel();
1167     // Model does not assign interpretation
1168     if (!Model.getInterpretation(Exp, Value))
1169       return nullptr;
1170
1171     // A value has been obtained, check if it is the only value
1172     Z3Expr NotExp = Z3Expr::fromBinOp(
1173         Exp, BO_NE,
1174         Ty->isBooleanType() ? Z3Expr::fromBoolean(Value.getBoolValue())
1175                             : Z3Expr::fromAPSInt(Value),
1176         false);
1177
1178     Solver.addConstraint(NotExp);
1179     if (Solver.check() == Z3_L_TRUE)
1180       return nullptr;
1181
1182     // This is the only solution, store it
1183     return &BV.getValue(Value);
1184   } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
1185     SymbolRef CastSym = SC->getOperand();
1186     QualType CastTy = SC->getType();
1187     // Skip the void type
1188     if (CastTy->isVoidType())
1189       return nullptr;
1190
1191     const llvm::APSInt *Value;
1192     if (!(Value = getSymVal(State, CastSym)))
1193       return nullptr;
1194     return &BV.Convert(SC->getType(), *Value);
1195   } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1196     const llvm::APSInt *LHS, *RHS;
1197     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
1198       LHS = getSymVal(State, SIE->getLHS());
1199       RHS = &SIE->getRHS();
1200     } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
1201       LHS = &ISE->getLHS();
1202       RHS = getSymVal(State, ISE->getRHS());
1203     } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
1204       // Early termination to avoid expensive call
1205       LHS = getSymVal(State, SSM->getLHS());
1206       RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
1207     } else {
1208       llvm_unreachable("Unsupported binary expression to get symbol value!");
1209     }
1210
1211     if (!LHS || !RHS)
1212       return nullptr;
1213
1214     llvm::APSInt ConvertedLHS = *LHS, ConvertedRHS = *RHS;
1215     QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
1216     doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
1217         ConvertedLHS, LTy, ConvertedRHS, RTy);
1218     return BV.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
1219   }
1220
1221   llvm_unreachable("Unsupported expression to get symbol value!");
1222 }
1223
1224 ProgramStateRef
1225 Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
1226                                         SymbolReaper &SymReaper) {
1227   ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
1228   ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
1229
1230   for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
1231     if (SymReaper.maybeDead(I->first))
1232       CZ = CZFactory.remove(CZ, *I);
1233   }
1234
1235   return State->set<ConstraintZ3>(CZ);
1236 }
1237
1238 //===------------------------------------------------------------------===//
1239 // Internal implementation.
1240 //===------------------------------------------------------------------===//
1241
1242 ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State,
1243                                                   SymbolRef Sym,
1244                                                   const Z3Expr &Exp) {
1245   // Check the model, avoid simplifying AST to save time
1246   if (checkZ3Model(State, Exp) == Z3_L_TRUE)
1247     return State->add<ConstraintZ3>(std::make_pair(Sym, Exp));
1248
1249   return nullptr;
1250 }
1251
1252 Z3_lbool Z3ConstraintManager::checkZ3Model(ProgramStateRef State,
1253                                            const Z3Expr &Exp) const {
1254   Solver.reset();
1255   Solver.addConstraint(Exp);
1256   Solver.addStateConstraints(State);
1257   return Solver.check();
1258 }
1259
1260 Z3Expr Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy,
1261                                       bool *hasComparison) const {
1262   if (hasComparison) {
1263     *hasComparison = false;
1264   }
1265
1266   return getZ3SymExpr(Sym, RetTy, hasComparison);
1267 }
1268
1269 Z3Expr Z3ConstraintManager::getZ3NotExpr(const Z3Expr &Exp) const {
1270   return Z3Expr::fromUnOp(UO_LNot, Exp);
1271 }
1272
1273 Z3Expr Z3ConstraintManager::getZ3ZeroExpr(const Z3Expr &Exp, QualType Ty,
1274                                           bool Assumption) const {
1275   ASTContext &Ctx = getBasicVals().getContext();
1276   if (Ty->isRealFloatingType()) {
1277     llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
1278     return Z3Expr::fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
1279                                   Z3Expr::fromAPFloat(Zero));
1280   } else if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
1281              Ty->isBlockPointerType() || Ty->isReferenceType()) {
1282     bool isSigned = Ty->isSignedIntegerOrEnumerationType();
1283     // Skip explicit comparison for boolean types
1284     if (Ty->isBooleanType())
1285       return Assumption ? getZ3NotExpr(Exp) : Exp;
1286     return Z3Expr::fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
1287                              Z3Expr::fromInt("0", Ctx.getTypeSize(Ty)),
1288                              isSigned);
1289   }
1290
1291   llvm_unreachable("Unsupported type for zero value!");
1292 }
1293
1294 Z3Expr Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
1295                                          bool *hasComparison) const {
1296   if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
1297     if (RetTy)
1298       *RetTy = Sym->getType();
1299
1300     return getZ3DataExpr(SD->getSymbolID(), Sym->getType());
1301   } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
1302     if (RetTy)
1303       *RetTy = Sym->getType();
1304
1305     QualType FromTy;
1306     Z3Expr Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison);
1307     // Casting an expression with a comparison invalidates it. Note that this
1308     // must occur after the recursive call above.
1309     // e.g. (signed char) (x > 0)
1310     if (hasComparison)
1311       *hasComparison = false;
1312     return getZ3CastExpr(Exp, FromTy, Sym->getType());
1313   } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1314     Z3Expr Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy);
1315     // Set the hasComparison parameter, in post-order traversal order.
1316     if (hasComparison)
1317       *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
1318     return Exp;
1319   }
1320
1321   llvm_unreachable("Unsupported SymbolRef type!");
1322 }
1323
1324 Z3Expr Z3ConstraintManager::getZ3DataExpr(const SymbolID ID,
1325                                           QualType Ty) const {
1326   ASTContext &Ctx = getBasicVals().getContext();
1327   return Z3Expr::fromData(ID, Ty->isBooleanType(), Ty->isRealFloatingType(),
1328                           Ctx.getTypeSize(Ty));
1329 }
1330
1331 Z3Expr Z3ConstraintManager::getZ3CastExpr(const Z3Expr &Exp, QualType FromTy,
1332                                           QualType ToTy) const {
1333   ASTContext &Ctx = getBasicVals().getContext();
1334   return Z3Expr::fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
1335                           Ctx.getTypeSize(FromTy));
1336 }
1337
1338 Z3Expr Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
1339                                             bool *hasComparison,
1340                                             QualType *RetTy) const {
1341   QualType LTy, RTy;
1342   BinaryOperator::Opcode Op = BSE->getOpcode();
1343
1344   if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
1345     RTy = getAPSIntType(SIE->getRHS());
1346     Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), &LTy, hasComparison);
1347     Z3Expr RHS = Z3Expr::fromAPSInt(SIE->getRHS());
1348     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1349   } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
1350     LTy = getAPSIntType(ISE->getLHS());
1351     Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS());
1352     Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
1353     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1354   } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
1355     Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), &LTy, hasComparison);
1356     Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
1357     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1358   } else {
1359     llvm_unreachable("Unsupported BinarySymExpr type!");
1360   }
1361 }
1362
1363 Z3Expr Z3ConstraintManager::getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
1364                                          BinaryOperator::Opcode Op,
1365                                          const Z3Expr &RHS, QualType RTy,
1366                                          QualType *RetTy) const {
1367   Z3Expr NewLHS = LHS;
1368   Z3Expr NewRHS = RHS;
1369   doTypeConversion(NewLHS, NewRHS, LTy, RTy);
1370   // Update the return type parameter if the output type has changed.
1371   if (RetTy) {
1372     // A boolean result can be represented as an integer type in C/C++, but at
1373     // this point we only care about the Z3 type. Set it as a boolean type to
1374     // avoid subsequent Z3 errors.
1375     if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) {
1376       ASTContext &Ctx = getBasicVals().getContext();
1377       *RetTy = Ctx.BoolTy;
1378     } else {
1379       *RetTy = LTy;
1380     }
1381
1382     // If the two operands are pointers and the operation is a subtraction, the
1383     // result is of type ptrdiff_t, which is signed
1384     if (LTy->isAnyPointerType() && LTy == RTy && Op == BO_Sub) {
1385       ASTContext &Ctx = getBasicVals().getContext();
1386       *RetTy = Ctx.getIntTypeForBitwidth(Ctx.getTypeSize(LTy), true);
1387     }
1388   }
1389
1390   return LTy->isRealFloatingType()
1391              ? Z3Expr::fromFloatBinOp(NewLHS, Op, NewRHS)
1392              : Z3Expr::fromBinOp(NewLHS, Op, NewRHS,
1393                                  LTy->isSignedIntegerOrEnumerationType());
1394 }
1395
1396 //===------------------------------------------------------------------===//
1397 // Helper functions.
1398 //===------------------------------------------------------------------===//
1399
1400 QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
1401   ASTContext &Ctx = getBasicVals().getContext();
1402   return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
1403 }
1404
1405 void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
1406                                            QualType &LTy, QualType &RTy) const {
1407   ASTContext &Ctx = getBasicVals().getContext();
1408
1409   // Perform type conversion
1410   if (LTy->isIntegralOrEnumerationType() &&
1411       RTy->isIntegralOrEnumerationType()) {
1412     if (LTy->isArithmeticType() && RTy->isArithmeticType())
1413       return doIntTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
1414   } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
1415     return doFloatTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
1416   } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
1417              (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
1418              (LTy->isReferenceType() || RTy->isReferenceType())) {
1419     // TODO: Refactor to Sema::FindCompositePointerType(), and
1420     // Sema::CheckCompareOperands().
1421
1422     uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1423     uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1424
1425     // Cast the non-pointer type to the pointer type.
1426     // TODO: Be more strict about this.
1427     if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
1428         (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
1429         (LTy->isReferenceType() ^ RTy->isReferenceType())) {
1430       if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
1431           LTy->isReferenceType()) {
1432         LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
1433         LTy = RTy;
1434       } else {
1435         RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
1436         RTy = LTy;
1437       }
1438     }
1439
1440     // Cast the void pointer type to the non-void pointer type.
1441     // For void types, this assumes that the casted value is equal to the value
1442     // of the original pointer, and does not account for alignment requirements.
1443     if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
1444       assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
1445              "Pointer types have different bitwidths!");
1446       if (RTy->isVoidPointerType())
1447         RTy = LTy;
1448       else
1449         LTy = RTy;
1450     }
1451
1452     if (LTy == RTy)
1453       return;
1454   }
1455
1456   // Fallback: for the solver, assume that these types don't really matter
1457   if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
1458       (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
1459     LTy = RTy;
1460     return;
1461   }
1462
1463   // TODO: Refine behavior for invalid type casts
1464 }
1465
1466 template <typename T,
1467           T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1468 void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType &LTy, T &RHS,
1469                                               QualType &RTy) const {
1470   ASTContext &Ctx = getBasicVals().getContext();
1471
1472   uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1473   uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1474
1475   // Always perform integer promotion before checking type equality.
1476   // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
1477   if (LTy->isPromotableIntegerType()) {
1478     QualType NewTy = Ctx.getPromotedIntegerType(LTy);
1479     uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
1480     LHS = (*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);
1481     LTy = NewTy;
1482     LBitWidth = NewBitWidth;
1483   }
1484   if (RTy->isPromotableIntegerType()) {
1485     QualType NewTy = Ctx.getPromotedIntegerType(RTy);
1486     uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
1487     RHS = (*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth);
1488     RTy = NewTy;
1489     RBitWidth = NewBitWidth;
1490   }
1491
1492   if (LTy == RTy)
1493     return;
1494
1495   // Perform integer type conversion
1496   // Note: Safe to skip updating bitwidth because this must terminate
1497   bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
1498   bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
1499
1500   int order = Ctx.getIntegerTypeOrder(LTy, RTy);
1501   if (isLSignedTy == isRSignedTy) {
1502     // Same signedness; use the higher-ranked type
1503     if (order == 1) {
1504       RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1505       RTy = LTy;
1506     } else {
1507       LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1508       LTy = RTy;
1509     }
1510   } else if (order != (isLSignedTy ? 1 : -1)) {
1511     // The unsigned type has greater than or equal rank to the
1512     // signed type, so use the unsigned type
1513     if (isRSignedTy) {
1514       RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1515       RTy = LTy;
1516     } else {
1517       LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1518       LTy = RTy;
1519     }
1520   } else if (LBitWidth != RBitWidth) {
1521     // The two types are different widths; if we are here, that
1522     // means the signed type is larger than the unsigned type, so
1523     // use the signed type.
1524     if (isLSignedTy) {
1525       RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1526       RTy = LTy;
1527     } else {
1528       LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1529       LTy = RTy;
1530     }
1531   } else {
1532     // The signed type is higher-ranked than the unsigned type,
1533     // but isn't actually any bigger (like unsigned int and long
1534     // on most 32-bit systems).  Use the unsigned type corresponding
1535     // to the signed type.
1536     QualType NewTy = Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
1537     RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1538     RTy = NewTy;
1539     LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1540     LTy = NewTy;
1541   }
1542 }
1543
1544 template <typename T,
1545           T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1546 void Z3ConstraintManager::doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
1547                                                 QualType &RTy) const {
1548   ASTContext &Ctx = getBasicVals().getContext();
1549
1550   uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1551   uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1552
1553   // Perform float-point type promotion
1554   if (!LTy->isRealFloatingType()) {
1555     LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1556     LTy = RTy;
1557     LBitWidth = RBitWidth;
1558   }
1559   if (!RTy->isRealFloatingType()) {
1560     RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1561     RTy = LTy;
1562     RBitWidth = LBitWidth;
1563   }
1564
1565   if (LTy == RTy)
1566     return;
1567
1568   // If we have two real floating types, convert the smaller operand to the
1569   // bigger result
1570   // Note: Safe to skip updating bitwidth because this must terminate
1571   int order = Ctx.getFloatingTypeOrder(LTy, RTy);
1572   if (order > 0) {
1573     RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
1574     RTy = LTy;
1575   } else if (order == 0) {
1576     LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
1577     LTy = RTy;
1578   } else {
1579     llvm_unreachable("Unsupported floating-point type cast!");
1580   }
1581 }
1582
1583 llvm::APSInt Z3ConstraintManager::castAPSInt(const llvm::APSInt &V,
1584                                              QualType ToTy, uint64_t ToWidth,
1585                                              QualType FromTy,
1586                                              uint64_t FromWidth) {
1587   APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
1588   return TargetType.convert(V);
1589 }
1590
1591 //==------------------------------------------------------------------------==/
1592 // Pretty-printing.
1593 //==------------------------------------------------------------------------==/
1594
1595 void Z3ConstraintManager::print(ProgramStateRef St, raw_ostream &OS,
1596                                 const char *nl, const char *sep) {
1597
1598   ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
1599
1600   OS << nl << sep << "Constraints:";
1601   for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
1602     OS << nl << ' ' << I->first << " : ";
1603     I->second.print(OS);
1604   }
1605   OS << nl;
1606 }
1607
1608 #endif
1609
1610 std::unique_ptr<ConstraintManager>
1611 ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
1612 #if CLANG_ANALYZER_WITH_Z3
1613   return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
1614 #else
1615   llvm::report_fatal_error("Clang was not compiled with Z3 support!", false);
1616   return nullptr;
1617 #endif
1618 }