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 {
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   SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
607     return newExprRef(
608         Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
609                                      toZ3Expr(*RHS).AST)));
610   }
611 
612   SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
613     SMTExprRef RoundingMode = getFloatRoundingMode();
614     return newExprRef(Z3Expr(
615         Context,
616         Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
617                               toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
618   }
619 
620   SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
621     SMTExprRef RoundingMode = getFloatRoundingMode();
622     return newExprRef(Z3Expr(
623         Context,
624         Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
625                                toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
626   }
627 
628   SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
629     SMTExprRef RoundingMode = getFloatRoundingMode();
630     return newExprRef(Z3Expr(
631         Context,
632         Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
633                                  toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
634   }
635 
636   SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) override {
637     SMTExprRef RoundingMode = getFloatRoundingMode();
638     return newExprRef(Z3Expr(
639         Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
640                                   toZ3Expr(*From).AST, ToWidth)));
641   }
642 
643   SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) override {
644     SMTExprRef RoundingMode = getFloatRoundingMode();
645     return newExprRef(Z3Expr(
646         Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
647                                   toZ3Expr(*From).AST, ToWidth)));
648   }
649 
650   SMTExprRef mkBoolean(const bool b) override {
651     return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
652                                         : Z3_mk_false(Context.Context)));
653   }
654 
655   SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {
656     const SMTSortRef Sort = getBitvectorSort(BitWidth);
657     return newExprRef(
658         Z3Expr(Context, Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
659                                       toZ3Sort(*Sort).Sort)));
660   }
661 
662   SMTExprRef mkFloat(const llvm::APFloat Float) override {
663     SMTSortRef Sort =
664         getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
665 
666     llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
667     SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth());
668     return newExprRef(Z3Expr(
669         Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
670                                     toZ3Sort(*Sort).Sort)));
671   }
672 
673   SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {
674     return newExprRef(
675         Z3Expr(Context, Z3_mk_const(Context.Context,
676                                     Z3_mk_string_symbol(Context.Context, Name),
677                                     toZ3Sort(*Sort).Sort)));
678   }
679 
680   llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
681                             bool isUnsigned) override {
682     return llvm::APSInt(
683         llvm::APInt(BitWidth,
684                     Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
685                     10),
686         isUnsigned);
687   }
688 
689   bool getBoolean(const SMTExprRef &Exp) override {
690     return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
691   }
692 
693   SMTExprRef getFloatRoundingMode() override {
694     // TODO: Don't assume nearest ties to even rounding mode
695     return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
696   }
697 
698   bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
699                  llvm::APFloat &Float, bool useSemantics) {
700     assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");
701 
702     llvm::APSInt Int(Sort->getFloatSortSize(), true);
703     const llvm::fltSemantics &Semantics =
704         getFloatSemantics(Sort->getFloatSortSize());
705     SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());
706     if (!toAPSInt(BVSort, AST, Int, true)) {
707       return false;
708     }
709 
710     if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
711       assert(false && "Floating-point types don't match!");
712       return false;
713     }
714 
715     Float = llvm::APFloat(Semantics, Int);
716     return true;
717   }
718 
719   bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,
720                 llvm::APSInt &Int, bool useSemantics) {
721     if (Sort->isBitvectorSort()) {
722       if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {
723         assert(false && "Bitvector types don't match!");
724         return false;
725       }
726 
727       // FIXME: This function is also used to retrieve floating-point values,
728       // which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything
729       // between 1 and 64 bits long, which is the reason we have this weird
730       // guard. In the future, we need proper calls in the backend to retrieve
731       // floating-points and its special values (NaN, +/-infinity, +/-zero),
732       // then we can drop this weird condition.
733       if (Sort->getBitvectorSortSize() <= 64 ||
734           Sort->getBitvectorSortSize() == 128) {
735         Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
736         return true;
737       }
738 
739       assert(false && "Bitwidth not supported!");
740       return false;
741     }
742 
743     if (Sort->isBooleanSort()) {
744       if (useSemantics && Int.getBitWidth() < 1) {
745         assert(false && "Boolean type doesn't match!");
746         return false;
747       }
748 
749       Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),
750                          Int.isUnsigned());
751       return true;
752     }
753 
754     llvm_unreachable("Unsupported sort to integer!");
755   }
756 
757   bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
758     Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
759     Z3_func_decl Func = Z3_get_app_decl(
760         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
761     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
762       return false;
763 
764     SMTExprRef Assign = newExprRef(
765         Z3Expr(Context,
766                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
767     SMTSortRef Sort = getSort(Assign);
768     return toAPSInt(Sort, Assign, Int, true);
769   }
770 
771   bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
772     Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
773     Z3_func_decl Func = Z3_get_app_decl(
774         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
775     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
776       return false;
777 
778     SMTExprRef Assign = newExprRef(
779         Z3Expr(Context,
780                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
781     SMTSortRef Sort = getSort(Assign);
782     return toAPFloat(Sort, Assign, Float, true);
783   }
784 
785   Optional<bool> check() const override {
786     Z3_lbool res = Z3_solver_check(Context.Context, Solver);
787     if (res == Z3_L_TRUE)
788       return true;
789 
790     if (res == Z3_L_FALSE)
791       return false;
792 
793     return Optional<bool>();
794   }
795 
796   void push() override { return Z3_solver_push(Context.Context, Solver); }
797 
798   void pop(unsigned NumStates = 1) override {
799     assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
800     return Z3_solver_pop(Context.Context, Solver, NumStates);
801   }
802 
803   bool isFPSupported() override { return true; }
804 
805   /// Reset the solver and remove all constraints.
806   void reset() override { Z3_solver_reset(Context.Context, Solver); }
807 
808   void print(raw_ostream &OS) const override {
809     OS << Z3_solver_to_string(Context.Context, Solver);
810   }
811 }; // end class Z3Solver
812 
813 } // end anonymous namespace
814 
815 #endif
816 
817 llvm::SMTSolverRef llvm::CreateZ3Solver() {
818 #if LLVM_WITH_Z3
819   return llvm::make_unique<Z3Solver>();
820 #else
821   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
822                            "with -DLLVM_ENABLE_Z3_SOLVER=ON",
823                            false);
824   return nullptr;
825 #endif
826 }
827 
828 LLVM_DUMP_METHOD void SMTSort::dump() const { print(llvm::errs()); }
829 LLVM_DUMP_METHOD void SMTExpr::dump() const { print(llvm::errs()); }
830 LLVM_DUMP_METHOD void SMTSolver::dump() const { print(llvm::errs()); }
831 
832 
833