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()); } 996