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