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