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