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