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
14using 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
26namespace {
27
28/// Configuration class for Z3
29class Z3Config {
30 friend class Z3Context;
31
32 Z3_config Config = Z3_mk_config();
33
34public:
35 Z3Config() = default;
36 Z3Config(const Z3Config &) = delete;
37 Z3Config(Z3Config &&) = default;
38 Z3Config &operator=(Z3Config &) = delete;
39 Z3Config &operator=(Z3Config &&) = default;
40 ~Z3Config() { Z3_del_config(Config); }
41}; // end class Z3Config
42
43// Function used to report errors
44void 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
50class Z3Context {
51public:
52 Z3Config Config;
53 Z3_context Context;
54
55 Z3Context() {
56 Context = Z3_mk_context_rc(Config.Config);
57 // The error function is set here because the context is the first 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
74class Z3Sort : public SMTSort {
75 friend class Z3Solver;
76
77 Z3Context &Context;
78
79 Z3_sort Sort;
80
81public:
82 /// Default constructor, mainly used by make_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
145static const Z3Sort &toZ3Sort(const SMTSort &S) {
146 return static_cast<const Z3Sort &>(S);
147}
148
149class Z3Expr : public SMTExpr {
150 friend class Z3Solver;
151
152 Z3Context &Context;
153
154 Z3_ast AST;
155
156public:
157 Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
158 Z3_inc_ref(Context.Context, AST);
159 }
160
161 /// Override implicit copy constructor for correct reference counting.
162 Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
163 Z3_inc_ref(Context.Context, AST);
164 }
165
166 /// Override implicit copy assignment constructor for correct 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
202static const Z3Expr &toZ3Expr(const SMTExpr &E) {
203 return static_cast<const Z3Expr &>(E);
204}
205
206class Z3Model {
207 friend class Z3Solver;
208
209 Z3Context &Context;
210
211 Z3_model Model;
212
213public:
214 Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) {
215 Z3_model_inc_ref(Context.Context, Model);
216 }
217
218 Z3Model(const Z3Model &Other) = delete;
219 Z3Model(Z3Model &&Other) = delete;
220 Z3Model &operator=(Z3Model &Other) = delete;
221 Z3Model &operator=(Z3Model &&Other) = delete;
222
223 ~Z3Model() {
224 if (Model)
225 Z3_model_dec_ref(Context.Context, Model);
226 }
227
228 void print(raw_ostream &OS) const {
229 OS << Z3_model_to_string(Context.Context, Model);
230 }
231
232 LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
233}; // end class Z3Model
234
235/// Get the corresponding IEEE floating-point type for a given bitwidth.
236static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
237 switch (BitWidth) {
238 default:
239 llvm_unreachable("Unsupported floating-point semantics!");
240 break;
241 case 16:
242 return llvm::APFloat::IEEEhalf();
243 case 32:
244 return llvm::APFloat::IEEEsingle();
245 case 64:
246 return llvm::APFloat::IEEEdouble();
247 case 128:
248 return llvm::APFloat::IEEEquad();
249 }
250}
251
252// Determine whether two float semantics are equivalent
253static bool areEquivalent(const llvm::fltSemantics &LHS,
254 const llvm::fltSemantics &RHS) {
255 return (llvm::APFloat::semanticsPrecision(LHS) ==
256 llvm::APFloat::semanticsPrecision(RHS)) &&
257 (llvm::APFloat::semanticsMinExponent(LHS) ==
258 llvm::APFloat::semanticsMinExponent(RHS)) &&
259 (llvm::APFloat::semanticsMaxExponent(LHS) ==
260 llvm::APFloat::semanticsMaxExponent(RHS)) &&
261 (llvm::APFloat::semanticsSizeInBits(LHS) ==
262 llvm::APFloat::semanticsSizeInBits(RHS));
263}
264
265class Z3Solver : public SMTSolver {
266 friend class Z3ConstraintManager;
267
268 Z3Context Context;
269
270 Z3_solver Solver = [this] {
271 Z3_solver S = Z3_mk_simple_solver(Context.Context);
272 Z3_solver_inc_ref(Context.Context, S);
273 return S;
274 }();
275
276 Z3_params Params = [this] {
277 Z3_params P = Z3_mk_params(Context.Context);
278 Z3_params_inc_ref(Context.Context, P);
279 return P;
280 }();
281
282 // Cache Sorts
283 std::set<Z3Sort> CachedSorts;
284
285 // Cache Exprs
286 std::set<Z3Expr> CachedExprs;
287
288public:
289 Z3Solver() = default;
290 Z3Solver(const Z3Solver &Other) = delete;
291 Z3Solver(Z3Solver &&Other) = delete;
292 Z3Solver &operator=(Z3Solver &Other) = delete;
293 Z3Solver &operator=(Z3Solver &&Other) = delete;
294
295 ~Z3Solver() override {
296 Z3_params_dec_ref(Context.Context, Params);
297 Z3_solver_dec_ref(Context.Context, Solver);
298 }
299
300 void addConstraint(const SMTExprRef &Exp) const override {
301 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
302 }
303
304 // Given an SMTSort, adds/retrives it from the cache and 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
926class Z3Statistics final : public SMTSolverStatistics {
927public:
928 double getDouble(StringRef Key) const override {
929 auto It = DoubleValues.find(Key.str());
930 assert(It != DoubleValues.end());
931 return It->second;
932 };
933 unsigned getUnsigned(StringRef Key) const override {
934 auto It = UnsignedValues.find(Key.str());
935 if (It == UnsignedValues.end())
936 return 0;
937 return It->second;
938 };
939
940 void print(raw_ostream &OS) const override {
941 for (auto const &[K, V] : UnsignedValues) {
942 OS << K << ": " << V << '\n';
943 }
944 for (auto const &[K, V] : DoubleValues) {
945 write_double(OS << K << ": ", V, FloatStyle::Fixed);
946 OS << '\n';
947 }
948 }
949
950private:
951 friend class Z3Solver;
952 std::unordered_map<std::string, unsigned> UnsignedValues;
953 std::unordered_map<std::string, double> DoubleValues;
954};
955
956std::unique_ptr<SMTSolverStatistics> Z3Solver::getStatistics() const {
957 auto const &C = Context.Context;
958 Z3_stats S = Z3_solver_get_statistics(C, Solver);
959 Z3_stats_inc_ref(C, S);
960 auto StatsGuard = llvm::make_scope_exit([&C, &S] { Z3_stats_dec_ref(C, S); });
961 Z3Statistics Result;
962
963 unsigned NumKeys = Z3_stats_size(C, S);
964 for (unsigned Idx = 0; Idx < NumKeys; ++Idx) {
965 const char *Key = Z3_stats_get_key(C, S, Idx);
966 if (Z3_stats_is_uint(C, S, Idx)) {
967 auto Value = Z3_stats_get_uint_value(C, S, Idx);
968 Result.UnsignedValues.try_emplace(Key, Value);
969 } else {
970 assert(Z3_stats_is_double(C, S, Idx));
971 auto Value = Z3_stats_get_double_value(C, S, Idx);
972 Result.DoubleValues.try_emplace(Key, Value);
973 }
974 }
975 return std::make_unique<Z3Statistics>(std::move(Result));
976}
977
978} // end anonymous namespace
979
980#endif
981
982llvm::SMTSolverRef llvm::CreateZ3Solver() {
983#if LLVM_WITH_Z3
984 return std::make_unique<Z3Solver>();
985#else
986 llvm::report_fatal_error(reason: "LLVM was not compiled with Z3 support, rebuild "
987 "with -DLLVM_ENABLE_Z3_SOLVER=ON",
988 gen_crash_diag: false);
989 return nullptr;
990#endif
991}
992
993#if !defined(NDEBUG) || defined(LLVM_ENABLE_DUMP)
994LLVM_DUMP_METHOD void SMTSort::dump() const { print(llvm::errs()); }
995LLVM_DUMP_METHOD void SMTExpr::dump() const { print(llvm::errs()); }
996LLVM_DUMP_METHOD void SMTSolver::dump() const { print(llvm::errs()); }
997LLVM_DUMP_METHOD void SMTSolverStatistics::dump() const { print(llvm::errs()); }
998#endif
999