xref: /freebsd/contrib/llvm-project/llvm/lib/Support/Z3Solver.cpp (revision 19fae0f66023a97a9b464b3beeeabb2081f575b3) 
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