999 lines · 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-exception6//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 14using namespace llvm;15 16#if LLVM_WITH_Z317 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 26namespace {27 28/// Configuration class for Z329class Z3Config {30 friend class Z3Context;31 32 Z3_config Config = Z3_mk_config();33 34public: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 Z3Config42 43// Function used to report errors44void 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 context50class Z3Context {51public: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 object58 // created by the backend59 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 Z3Context72 73/// Wrapper for Z3 Sort74class Z3Sort : public SMTSort {75 friend class Z3Solver;76 77 Z3Context &Context;78 79 Z3_sort Sort;80 81public:82 /// Default constructor, mainly used by make_shared83 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 reference93 /// 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 Z3Sort144 145static const Z3Sort &toZ3Sort(const SMTSort &S) {146 return static_cast<const Z3Sort &>(S);147}148 149class Z3Expr : public SMTExpr {150 friend class Z3Solver;151 152 Z3Context &Context;153 154 Z3_ast AST;155 156public: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 reference167 /// 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 Z3Expr201 202static const Z3Expr &toZ3Expr(const SMTExpr &E) {203 return static_cast<const Z3Expr &>(E);204}205 206class Z3Model {207 friend class Z3Solver;208 209 Z3Context &Context;210 211 Z3_model Model;212 213public: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 Z3Model234 235/// Get the corresponding IEEE floating-point type for a given bitwidth.236static 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 equivalent253static 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 265class 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 Sorts283 std::set<Z3Sort> CachedSorts;284 285 // Cache Exprs286 std::set<Z3Expr> CachedExprs;287 288public: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 returns305 // an SMTSortRef to the SMTSort in the cache306 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 returns312 // an SMTExprRef to the SMTExpr in the cache313 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 addition622 /// operation623 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 bitvector631 /// addition operation632 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 bitvector640 /// subtraction operation641 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 subtraction649 /// operation650 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 bitvector658 /// division/modulus operation659 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 negation667 /// operation668 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 multiplication674 /// operation675 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 bitvector683 /// multiplication operation684 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 mode795 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 anything829 // between 1 and 64 bits long, which is the reason we have this weird830 // guard. In the future, we need proper calls in the backend to retrieve831 // 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 Z3Solver925 926class Z3Statistics final : public SMTSolverStatistics {927public: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 if (It == UnsignedValues.end())936 return 0;937 return It->second;938 };939 940 void print(raw_ostream &OS) const override {941 for (auto const &[K, V] : UnsignedValues) {942 OS << K << ": " << V << '\n';943 }944 for (auto const &[K, V] : DoubleValues) {945 write_double(OS << K << ": ", V, FloatStyle::Fixed);946 OS << '\n';947 }948 }949 950private:951 friend class Z3Solver;952 std::unordered_map<std::string, unsigned> UnsignedValues;953 std::unordered_map<std::string, double> DoubleValues;954};955 956std::unique_ptr<SMTSolverStatistics> Z3Solver::getStatistics() const {957 auto const &C = Context.Context;958 Z3_stats S = Z3_solver_get_statistics(C, Solver);959 Z3_stats_inc_ref(C, S);960 auto StatsGuard = llvm::make_scope_exit([&C, &S] { Z3_stats_dec_ref(C, S); });961 Z3Statistics Result;962 963 unsigned NumKeys = Z3_stats_size(C, S);964 for (unsigned Idx = 0; Idx < NumKeys; ++Idx) {965 const char *Key = Z3_stats_get_key(C, S, Idx);966 if (Z3_stats_is_uint(C, S, Idx)) {967 auto Value = Z3_stats_get_uint_value(C, S, Idx);968 Result.UnsignedValues.try_emplace(Key, Value);969 } else {970 assert(Z3_stats_is_double(C, S, Idx));971 auto Value = Z3_stats_get_double_value(C, S, Idx);972 Result.DoubleValues.try_emplace(Key, Value);973 }974 }975 return std::make_unique<Z3Statistics>(std::move(Result));976}977 978} // end anonymous namespace979 980#endif981 982llvm::SMTSolverRef llvm::CreateZ3Solver() {983#if LLVM_WITH_Z3984 return std::make_unique<Z3Solver>();985#else986 llvm::report_fatal_error("LLVM was not compiled with Z3 support, rebuild "987 "with -DLLVM_ENABLE_Z3_SOLVER=ON",988 false);989 return nullptr;990#endif991}992 993#if !defined(NDEBUG) || defined(LLVM_ENABLE_DUMP)994LLVM_DUMP_METHOD void SMTSort::dump() const { print(llvm::errs()); }995LLVM_DUMP_METHOD void SMTExpr::dump() const { print(llvm::errs()); }996LLVM_DUMP_METHOD void SMTSolver::dump() const { print(llvm::errs()); }997LLVM_DUMP_METHOD void SMTSolverStatistics::dump() const { print(llvm::errs()); }998#endif999