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