llvm/lib/Support/Z3Solver.cpp

   1 //== Z3Solver.cpp -----------------------------------------------*- C++ -*--==//
   2 //
   3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
   4 // See https://llvm.org/LICENSE.txt for license information.
   5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
   6 //
   7 //===----------------------------------------------------------------------===//
   8
   9 #include "llvm/ADT/SmallString.h"
  10 #include "llvm/ADT/Twine.h"
  11 #include "llvm/Config/config.h"
  12 #include "llvm/Support/SMTAPI.h"
  13 #include <set>
  14
  15 using namespace llvm;
  16
  17 #if LLVM_WITH_Z3
  18
  19 #include <z3.h>
  20
  21 namespace {
  22
  23 /// Configuration class for Z3
  24 class Z3Config {
  25   friend class Z3Context;
  26
  27   Z3_config Config;
  28
  29 public:
  30   Z3Config() : Config(Z3_mk_config()) {
  31     // Enable model finding
  32     Z3_set_param_value(Config, "model", "true");
  33     // Disable proof generation
  34     Z3_set_param_value(Config, "proof", "false");
  35     // Set timeout to 15000ms = 15s
  36     Z3_set_param_value(Config, "timeout", "15000");
  37   }
  38
  39   ~Z3Config() { Z3_del_config(Config); }
  40 }; // end class Z3Config
  41
  42 // Function used to report errors
  43 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
  44   llvm::report_fatal_error("Z3 error: " +
  45                            llvm::Twine(Z3_get_error_msg(Context, Error)));
  46 }
  47
  48 /// Wrapper for Z3 context
  49 class Z3Context {
  50 public:
  51   Z3_context Context;
  52
  53   Z3Context() {
  54     Context = Z3_mk_context_rc(Z3Config().Config);
  55     // The error function is set here because the context is the first object
  56     // created by the backend
  57     Z3_set_error_handler(Context, Z3ErrorHandler);
  58   }
  59
  60   virtual ~Z3Context() {
  61     Z3_del_context(Context);
  62     Context = nullptr;
  63   }
  64 }; // end class Z3Context
  65
  66 /// Wrapper for Z3 Sort
  67 class Z3Sort : public SMTSort {
  68   friend class Z3Solver;
  69
  70   Z3Context &Context;
  71
  72   Z3_sort Sort;
  73
  74 public:
  75   /// Default constructor, mainly used by make_shared
  76   Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {
  77     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
  78   }
  79
  80   /// Override implicit copy constructor for correct reference counting.
  81   Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {
  82     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
  83   }
  84
  85   /// Override implicit copy assignment constructor for correct reference
  86   /// counting.
  87   Z3Sort &operator=(const Z3Sort &Other) {
  88     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Other.Sort));
  89     Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
  90     Sort = Other.Sort;
  91     return *this;
  92   }
  93
  94   Z3Sort(Z3Sort &&Other) = delete;
  95   Z3Sort &operator=(Z3Sort &&Other) = delete;
  96
  97   ~Z3Sort() {
  98     if (Sort)
  99       Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
 100   }
 101
 102   void Profile(llvm::FoldingSetNodeID &ID) const override {
 103     ID.AddInteger(
 104         Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort)));
 105   }
 106
 107   bool isBitvectorSortImpl() const override {
 108     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
 109   }
 110
 111   bool isFloatSortImpl() const override {
 112     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
 113   }
 114
 115   bool isBooleanSortImpl() const override {
 116     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);
 117   }
 118
 119   unsigned getBitvectorSortSizeImpl() const override {
 120     return Z3_get_bv_sort_size(Context.Context, Sort);
 121   }
 122
 123   unsigned getFloatSortSizeImpl() const override {
 124     return Z3_fpa_get_ebits(Context.Context, Sort) +
 125            Z3_fpa_get_sbits(Context.Context, Sort);
 126   }
 127
 128   bool equal_to(SMTSort const &Other) const override {
 129     return Z3_is_eq_sort(Context.Context, Sort,
 130                          static_cast<const Z3Sort &>(Other).Sort);
 131   }
 132
 133   void print(raw_ostream &OS) const override {
 134     OS << Z3_sort_to_string(Context.Context, Sort);
 135   }
 136 }; // end class Z3Sort
 137
 138 static const Z3Sort &toZ3Sort(const SMTSort &S) {
 139   return static_cast<const Z3Sort &>(S);
 140 }
 141
 142 class Z3Expr : public SMTExpr {
 143   friend class Z3Solver;
 144
 145   Z3Context &Context;
 146
 147   Z3_ast AST;
 148
 149 public:
 150   Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
 151     Z3_inc_ref(Context.Context, AST);
 152   }
 153
 154   /// Override implicit copy constructor for correct reference counting.
 155   Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
 156     Z3_inc_ref(Context.Context, AST);
 157   }
 158
 159   /// Override implicit copy assignment constructor for correct reference
 160   /// counting.
 161   Z3Expr &operator=(const Z3Expr &Other) {
 162     Z3_inc_ref(Context.Context, Other.AST);
 163     Z3_dec_ref(Context.Context, AST);
 164     AST = Other.AST;
 165     return *this;
 166   }
 167
 168   Z3Expr(Z3Expr &&Other) = delete;
 169   Z3Expr &operator=(Z3Expr &&Other) = delete;
 170
 171   ~Z3Expr() {
 172     if (AST)
 173       Z3_dec_ref(Context.Context, AST);
 174   }
 175
 176   void Profile(llvm::FoldingSetNodeID &ID) const override {
 177     ID.AddInteger(Z3_get_ast_id(Context.Context, AST));
 178   }
 179
 180   /// Comparison of AST equality, not model equivalence.
 181   bool equal_to(SMTExpr const &Other) const override {
 182     assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
 183                          Z3_get_sort(Context.Context,
 184                                      static_cast<const Z3Expr &>(Other).AST)) &&
 185            "AST's must have the same sort");
 186     return Z3_is_eq_ast(Context.Context, AST,
 187                         static_cast<const Z3Expr &>(Other).AST);
 188   }
 189
 190   void print(raw_ostream &OS) const override {
 191     OS << Z3_ast_to_string(Context.Context, AST);
 192   }
 193 }; // end class Z3Expr
 194
 195 static const Z3Expr &toZ3Expr(const SMTExpr &E) {
 196   return static_cast<const Z3Expr &>(E);
 197 }
 198
 199 class Z3Model {
 200   friend class Z3Solver;
 201
 202   Z3Context &Context;
 203
 204   Z3_model Model;
 205
 206 public:
 207   Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) {
 208     Z3_model_inc_ref(Context.Context, Model);
 209   }
 210
 211   Z3Model(const Z3Model &Other) = delete;
 212   Z3Model(Z3Model &&Other) = delete;
 213   Z3Model &operator=(Z3Model &Other) = delete;
 214   Z3Model &operator=(Z3Model &&Other) = delete;
 215
 216   ~Z3Model() {
 217     if (Model)
 218       Z3_model_dec_ref(Context.Context, Model);
 219   }
 220
 221   void print(raw_ostream &OS) const {
 222     OS << Z3_model_to_string(Context.Context, Model);
 223   }
 224
 225   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 226 }; // end class Z3Model
 227
 228 /// Get the corresponding IEEE floating-point type for a given bitwidth.
 229 static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
 230   switch (BitWidth) {
 231   default:
 232     llvm_unreachable("Unsupported floating-point semantics!");
 233     break;
 234   case 16:
 235     return llvm::APFloat::IEEEhalf();
 236   case 32:
 237     return llvm::APFloat::IEEEsingle();
 238   case 64:
 239     return llvm::APFloat::IEEEdouble();
 240   case 128:
 241     return llvm::APFloat::IEEEquad();
 242   }
 243 }
 244
 245 // Determine whether two float semantics are equivalent
 246 static bool areEquivalent(const llvm::fltSemantics &LHS,
 247                           const llvm::fltSemantics &RHS) {
 248   return (llvm::APFloat::semanticsPrecision(LHS) ==
 249           llvm::APFloat::semanticsPrecision(RHS)) &&
 250          (llvm::APFloat::semanticsMinExponent(LHS) ==
 251           llvm::APFloat::semanticsMinExponent(RHS)) &&
 252          (llvm::APFloat::semanticsMaxExponent(LHS) ==
 253           llvm::APFloat::semanticsMaxExponent(RHS)) &&
 254          (llvm::APFloat::semanticsSizeInBits(LHS) ==
 255           llvm::APFloat::semanticsSizeInBits(RHS));
 256 }
 257
 258 class Z3Solver : public SMTSolver {
 259   friend class Z3ConstraintManager;
 260
 261   Z3Context Context;
 262
 263   Z3_solver Solver;
 264
 265   // Cache Sorts
 266   std::set<Z3Sort> CachedSorts;
 267
 268   // Cache Exprs
 269   std::set<Z3Expr> CachedExprs;
 270
 271 public:
 272   Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
 273     Z3_solver_inc_ref(Context.Context, Solver);
 274   }
 275
 276   Z3Solver(const Z3Solver &Other) = delete;
 277   Z3Solver(Z3Solver &&Other) = delete;
 278   Z3Solver &operator=(Z3Solver &Other) = delete;
 279   Z3Solver &operator=(Z3Solver &&Other) = delete;
 280
 281   ~Z3Solver() {
 282     if (Solver)
 283       Z3_solver_dec_ref(Context.Context, Solver);
 284   }
 285
 286   void addConstraint(const SMTExprRef &Exp) const override {
 287     Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
 288   }
 289
 290   // Given an SMTSort, adds/retrives it from the cache and returns
 291   // an SMTSortRef to the SMTSort in the cache
 292   SMTSortRef newSortRef(const SMTSort &Sort) {
 293     auto It = CachedSorts.insert(toZ3Sort(Sort));
 294     return &(*It.first);
 295   }
 296
 297   // Given an SMTExpr, adds/retrives it from the cache and returns
 298   // an SMTExprRef to the SMTExpr in the cache
 299   SMTExprRef newExprRef(const SMTExpr &Exp) {
 300     auto It = CachedExprs.insert(toZ3Expr(Exp));
 301     return &(*It.first);
 302   }
 303
 304   SMTSortRef getBoolSort() override {
 305     return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));
 306   }
 307
 308   SMTSortRef getBitvectorSort(unsigned BitWidth) override {
 309     return newSortRef(
 310         Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));
 311   }
 312
 313   SMTSortRef getSort(const SMTExprRef &Exp) override {
 314     return newSortRef(
 315         Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
 316   }
 317
 318   SMTSortRef getFloat16Sort() override {
 319     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));
 320   }
 321
 322   SMTSortRef getFloat32Sort() override {
 323     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));
 324   }
 325
 326   SMTSortRef getFloat64Sort() override {
 327     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));
 328   }
 329
 330   SMTSortRef getFloat128Sort() override {
 331     return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));
 332   }
 333
 334   SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {
 335     return newExprRef(
 336         Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
 337   }
 338
 339   SMTExprRef mkBVNot(const SMTExprRef &Exp) override {
 340     return newExprRef(
 341         Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
 342   }
 343
 344   SMTExprRef mkNot(const SMTExprRef &Exp) override {
 345     return newExprRef(
 346         Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
 347   }
 348
 349   SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 350     return newExprRef(
 351         Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
 352                                     toZ3Expr(*RHS).AST)));
 353   }
 354
 355   SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 356     return newExprRef(
 357         Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
 358                                     toZ3Expr(*RHS).AST)));
 359   }
 360
 361   SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 362     return newExprRef(
 363         Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
 364                                     toZ3Expr(*RHS).AST)));
 365   }
 366
 367   SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 368     return newExprRef(
 369         Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
 370                                      toZ3Expr(*RHS).AST)));
 371   }
 372
 373   SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 374     return newExprRef(
 375         Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
 376                                      toZ3Expr(*RHS).AST)));
 377   }
 378
 379   SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 380     return newExprRef(
 381         Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
 382                                      toZ3Expr(*RHS).AST)));
 383   }
 384
 385   SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 386     return newExprRef(
 387         Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
 388                                      toZ3Expr(*RHS).AST)));
 389   }
 390
 391   SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 392     return newExprRef(
 393         Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
 394                                     toZ3Expr(*RHS).AST)));
 395   }
 396
 397   SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 398     return newExprRef(
 399         Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
 400                                      toZ3Expr(*RHS).AST)));
 401   }
 402
 403   SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 404     return newExprRef(
 405         Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
 406                                      toZ3Expr(*RHS).AST)));
 407   }
 408
 409   SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 410     return newExprRef(
 411         Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
 412                                     toZ3Expr(*RHS).AST)));
 413   }
 414
 415   SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 416     return newExprRef(
 417         Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
 418                                    toZ3Expr(*RHS).AST)));
 419   }
 420
 421   SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 422     return newExprRef(
 423         Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
 424                                     toZ3Expr(*RHS).AST)));
 425   }
 426
 427   SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 428     return newExprRef(
 429         Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
 430                                     toZ3Expr(*RHS).AST)));
 431   }
 432
 433   SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 434     return newExprRef(
 435         Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
 436                                     toZ3Expr(*RHS).AST)));
 437   }
 438
 439   SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 440     return newExprRef(
 441         Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
 442                                     toZ3Expr(*RHS).AST)));
 443   }
 444
 445   SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 446     return newExprRef(
 447         Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
 448                                     toZ3Expr(*RHS).AST)));
 449   }
 450
 451   SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 452     return newExprRef(
 453         Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
 454                                     toZ3Expr(*RHS).AST)));
 455   }
 456
 457   SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 458     return newExprRef(
 459         Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
 460                                     toZ3Expr(*RHS).AST)));
 461   }
 462
 463   SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 464     return newExprRef(
 465         Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
 466                                     toZ3Expr(*RHS).AST)));
 467   }
 468
 469   SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 470     return newExprRef(
 471         Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
 472                                     toZ3Expr(*RHS).AST)));
 473   }
 474
 475   SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 476     Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
 477     return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));
 478   }
 479
 480   SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 481     Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
 482     return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));
 483   }
 484
 485   SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 486     return newExprRef(
 487         Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
 488                                  toZ3Expr(*RHS).AST)));
 489   }
 490
 491   SMTExprRef mkFPNeg(const SMTExprRef &Exp) override {
 492     return newExprRef(
 493         Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
 494   }
 495
 496   SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override {
 497     return newExprRef(Z3Expr(
 498         Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
 499   }
 500
 501   SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override {
 502     return newExprRef(
 503         Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
 504   }
 505
 506   SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override {
 507     return newExprRef(Z3Expr(
 508         Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
 509   }
 510
 511   SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {
 512     return newExprRef(Z3Expr(
 513         Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
 514   }
 515
 516   SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 517     SMTExprRef RoundingMode = getFloatRoundingMode();
 518     return newExprRef(
 519         Z3Expr(Context,
 520                Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,
 521                              toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
 522   }
 523
 524   SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 525     SMTExprRef RoundingMode = getFloatRoundingMode();
 526     return newExprRef(
 527         Z3Expr(Context,
 528                Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,
 529                              toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
 530   }
 531
 532   SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 533     return newExprRef(
 534         Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
 535                                       toZ3Expr(*RHS).AST)));
 536   }
 537
 538   SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 539     SMTExprRef RoundingMode = getFloatRoundingMode();
 540     return newExprRef(
 541         Z3Expr(Context,
 542                Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,
 543                              toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
 544   }
 545
 546   SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 547     SMTExprRef RoundingMode = getFloatRoundingMode();
 548     return newExprRef(
 549         Z3Expr(Context,
 550                Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,
 551                              toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
 552   }
 553
 554   SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 555     return newExprRef(
 556         Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
 557                                      toZ3Expr(*RHS).AST)));
 558   }
 559
 560   SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 561     return newExprRef(
 562         Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
 563                                      toZ3Expr(*RHS).AST)));
 564   }
 565
 566   SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 567     return newExprRef(
 568         Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
 569                                       toZ3Expr(*RHS).AST)));
 570   }
 571
 572   SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 573     return newExprRef(
 574         Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
 575                                       toZ3Expr(*RHS).AST)));
 576   }
 577
 578   SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 579     return newExprRef(
 580         Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
 581                                      toZ3Expr(*RHS).AST)));
 582   }
 583
 584   SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
 585                    const SMTExprRef &F) override {
 586     return newExprRef(
 587         Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
 588                                   toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
 589   }
 590
 591   SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {
 592     return newExprRef(Z3Expr(
 593         Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
 594   }
 595
 596   SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {
 597     return newExprRef(Z3Expr(
 598         Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
 599   }
 600
 601   SMTExprRef mkBVExtract(unsigned High, unsigned Low,
 602                          const SMTExprRef &Exp) override {
 603     return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,
 604                                                     toZ3Expr(*Exp).AST)));
 605   }
 606
 607   /// Creates a predicate that checks for overflow in a bitvector addition
 608   /// operation
 609   SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
 610                                bool isSigned) override {
 611     return newExprRef(Z3Expr(
 612         Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
 613                                          toZ3Expr(*RHS).AST, isSigned)));
 614   }
 615
 616   /// Creates a predicate that checks for underflow in a signed bitvector
 617   /// addition operation
 618   SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS,
 619                                 const SMTExprRef &RHS) override {
 620     return newExprRef(Z3Expr(
 621         Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
 622                                           toZ3Expr(*RHS).AST)));
 623   }
 624
 625   /// Creates a predicate that checks for overflow in a signed bitvector
 626   /// subtraction operation
 627   SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS,
 628                                const SMTExprRef &RHS) override {
 629     return newExprRef(Z3Expr(
 630         Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
 631                                          toZ3Expr(*RHS).AST)));
 632   }
 633
 634   /// Creates a predicate that checks for underflow in a bitvector subtraction
 635   /// operation
 636   SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
 637                                 bool isSigned) override {
 638     return newExprRef(Z3Expr(
 639         Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
 640                                           toZ3Expr(*RHS).AST, isSigned)));
 641   }
 642
 643   /// Creates a predicate that checks for overflow in a signed bitvector
 644   /// division/modulus operation
 645   SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS,
 646                                 const SMTExprRef &RHS) override {
 647     return newExprRef(Z3Expr(
 648         Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
 649                                           toZ3Expr(*RHS).AST)));
 650   }
 651
 652   /// Creates a predicate that checks for overflow in a bitvector negation
 653   /// operation
 654   SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) override {
 655     return newExprRef(Z3Expr(
 656         Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST)));
 657   }
 658
 659   /// Creates a predicate that checks for overflow in a bitvector multiplication
 660   /// operation
 661   SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
 662                                bool isSigned) override {
 663     return newExprRef(Z3Expr(
 664         Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
 665                                          toZ3Expr(*RHS).AST, isSigned)));
 666   }
 667
 668   /// Creates a predicate that checks for underflow in a signed bitvector
 669   /// multiplication operation
 670   SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS,
 671                                 const SMTExprRef &RHS) override {
 672     return newExprRef(Z3Expr(
 673         Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
 674                                           toZ3Expr(*RHS).AST)));
 675   }
 676
 677   SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
 678     return newExprRef(
 679         Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
 680                                      toZ3Expr(*RHS).AST)));
 681   }
 682
 683   SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
 684     SMTExprRef RoundingMode = getFloatRoundingMode();
 685     return newExprRef(Z3Expr(
 686         Context,
 687         Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
 688                               toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
 689   }
 690
 691   SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
 692     SMTExprRef RoundingMode = getFloatRoundingMode();
 693     return newExprRef(Z3Expr(
 694         Context,
 695         Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
 696                                toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
 697   }
 698
 699   SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
 700     SMTExprRef RoundingMode = getFloatRoundingMode();
 701     return newExprRef(Z3Expr(
 702         Context,
 703         Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
 704                                  toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
 705   }
 706
 707   SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) override {
 708     SMTExprRef RoundingMode = getFloatRoundingMode();
 709     return newExprRef(Z3Expr(
 710         Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
 711                                   toZ3Expr(*From).AST, ToWidth)));
 712   }
 713
 714   SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) override {
 715     SMTExprRef RoundingMode = getFloatRoundingMode();
 716     return newExprRef(Z3Expr(
 717         Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
 718                                   toZ3Expr(*From).AST, ToWidth)));
 719   }
 720
 721   SMTExprRef mkBoolean(const bool b) override {
 722     return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
 723                                         : Z3_mk_false(Context.Context)));
 724   }
 725
 726   SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {
 727     const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;
 728
 729     // Slow path, when 64 bits are not enough.
 730     if (LLVM_UNLIKELY(Int.getBitWidth() > 64u)) {
 731       SmallString<40> Buffer;
 732       Int.toString(Buffer, 10);
 733       return newExprRef(Z3Expr(
 734           Context, Z3_mk_numeral(Context.Context, Buffer.c_str(), Z3Sort)));
 735     }
 736
 737     const int64_t BitReprAsSigned = Int.getExtValue();
 738     const uint64_t BitReprAsUnsigned =
 739         reinterpret_cast<const uint64_t &>(BitReprAsSigned);
 740
 741     Z3_ast Literal =
 742         Int.isSigned()
 743             ? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort)
 744             : Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort);
 745     return newExprRef(Z3Expr(Context, Literal));
 746   }
 747
 748   SMTExprRef mkFloat(const llvm::APFloat Float) override {
 749     SMTSortRef Sort =
 750         getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
 751
 752     llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
 753     SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth());
 754     return newExprRef(Z3Expr(
 755         Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
 756                                     toZ3Sort(*Sort).Sort)));
 757   }
 758
 759   SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {
 760     return newExprRef(
 761         Z3Expr(Context, Z3_mk_const(Context.Context,
 762                                     Z3_mk_string_symbol(Context.Context, Name),
 763                                     toZ3Sort(*Sort).Sort)));
 764   }
 765
 766   llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
 767                             bool isUnsigned) override {
 768     return llvm::APSInt(
 769         llvm::APInt(BitWidth,
 770                     Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
 771                     10),
 772         isUnsigned);
 773   }
 774
 775   bool getBoolean(const SMTExprRef &Exp) override {
 776     return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
 777   }
 778
 779   SMTExprRef getFloatRoundingMode() override {
 780     // TODO: Don't assume nearest ties to even rounding mode
 781     return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
 782   }
 783
 784   bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
 785                  llvm::APFloat &Float, bool useSemantics) {
 786     assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");
 787
 788     llvm::APSInt Int(Sort->getFloatSortSize(), true);
 789     const llvm::fltSemantics &Semantics =
 790         getFloatSemantics(Sort->getFloatSortSize());
 791     SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());
 792     if (!toAPSInt(BVSort, AST, Int, true)) {
 793       return false;
 794     }
 795
 796     if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
 797       assert(false && "Floating-point types don't match!");
 798       return false;
 799     }
 800
 801     Float = llvm::APFloat(Semantics, Int);
 802     return true;
 803   }
 804
 805   bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,
 806                 llvm::APSInt &Int, bool useSemantics) {
 807     if (Sort->isBitvectorSort()) {
 808       if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {
 809         assert(false && "Bitvector types don't match!");
 810         return false;
 811       }
 812
 813       // FIXME: This function is also used to retrieve floating-point values,
 814       // which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything
 815       // between 1 and 64 bits long, which is the reason we have this weird
 816       // guard. In the future, we need proper calls in the backend to retrieve
 817       // floating-points and its special values (NaN, +/-infinity, +/-zero),
 818       // then we can drop this weird condition.
 819       if (Sort->getBitvectorSortSize() <= 64 ||
 820           Sort->getBitvectorSortSize() == 128) {
 821         Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
 822         return true;
 823       }
 824
 825       assert(false && "Bitwidth not supported!");
 826       return false;
 827     }
 828
 829     if (Sort->isBooleanSort()) {
 830       if (useSemantics && Int.getBitWidth() < 1) {
 831         assert(false && "Boolean type doesn't match!");
 832         return false;
 833       }
 834
 835       Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),
 836                          Int.isUnsigned());
 837       return true;
 838     }
 839
 840     llvm_unreachable("Unsupported sort to integer!");
 841   }
 842
 843   bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
 844     Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
 845     Z3_func_decl Func = Z3_get_app_decl(
 846         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
 847     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
 848       return false;
 849
 850     SMTExprRef Assign = newExprRef(
 851         Z3Expr(Context,
 852                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
 853     SMTSortRef Sort = getSort(Assign);
 854     return toAPSInt(Sort, Assign, Int, true);
 855   }
 856
 857   bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
 858     Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
 859     Z3_func_decl Func = Z3_get_app_decl(
 860         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
 861     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
 862       return false;
 863
 864     SMTExprRef Assign = newExprRef(
 865         Z3Expr(Context,
 866                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
 867     SMTSortRef Sort = getSort(Assign);
 868     return toAPFloat(Sort, Assign, Float, true);
 869   }
 870
 871   Optional<bool> check() const override {
 872     Z3_lbool res = Z3_solver_check(Context.Context, Solver);
 873     if (res == Z3_L_TRUE)
 874       return true;
 875
 876     if (res == Z3_L_FALSE)
 877       return false;
 878
 879     return Optional<bool>();
 880   }
 881
 882   void push() override { return Z3_solver_push(Context.Context, Solver); }
 883
 884   void pop(unsigned NumStates = 1) override {
 885     assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
 886     return Z3_solver_pop(Context.Context, Solver, NumStates);
 887   }
 888
 889   bool isFPSupported() override { return true; }
 890
 891   /// Reset the solver and remove all constraints.
 892   void reset() override { Z3_solver_reset(Context.Context, Solver); }
 893
 894   void print(raw_ostream &OS) const override {
 895     OS << Z3_solver_to_string(Context.Context, Solver);
 896   }
 897 }; // end class Z3Solver
 898
 899 } // end anonymous namespace
 900
 901 #endif
 902
 903 llvm::SMTSolverRef llvm::CreateZ3Solver() {
 904 #if LLVM_WITH_Z3
 905   return std::make_unique<Z3Solver>();
 906 #else
 907   llvm::report_fatal_error("LLVM was not compiled with Z3 support, rebuild "
 908                            "with -DLLVM_ENABLE_Z3_SOLVER=ON",
 909                            false);
 910   return nullptr;
 911 #endif
 912 }
 913
 914 LLVM_DUMP_METHOD void SMTSort::dump() const { print(llvm::errs()); }
 915 LLVM_DUMP_METHOD void SMTExpr::dump() const { print(llvm::errs()); }
 916 LLVM_DUMP_METHOD void SMTSolver::dump() const { print(llvm::errs()); }