LLVM  10.0.0svn
Z3Solver.cpp
Go to the documentation of this file.
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) ==
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 
888 #if LLVM_WITH_Z3
889  return llvm::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 
uint64_t CallInst * C
static const fltSemantics & IEEEquad() LLVM_READNONE
Definition: APFloat.cpp:161
raw_ostream & errs()
This returns a reference to a raw_ostream for standard error.
virtual unsigned getFloatSortSize() const
Returns the floating-point size, fails if the sort is not a floating-point Calls getFloatSortSizeImpl...
Definition: SMTAPI.h:51
LLVMContext & Context
LLVM_ATTRIBUTE_NORETURN void report_fatal_error(Error Err, bool gen_crash_diag=true)
Report a serious error, calling any installed error handler.
Definition: Error.cpp:139
This class represents lattice values for constants.
Definition: AllocatorList.h:23
#define LLVM_DUMP_METHOD
Mark debug helper function definitions like dump() that should not be stripped from debug builds...
Definition: Compiler.h:473
amdgpu Simplify well known AMD library false FunctionCallee Value const Twine & Name
F(f)
const fltSemantics & getSemantics() const
Definition: APFloat.h:1165
LLVM_DUMP_METHOD void dump() const
Definition: Z3Solver.cpp:898
uint64_t High
Generic base class for SMT exprs.
Definition: SMTAPI.h:100
unsigned getBitWidth() const
Return the number of bits in the APInt.
Definition: APInt.h:1508
Twine - A lightweight data structure for efficiently representing the concatenation of temporary valu...
Definition: Twine.h:80
void AddInteger(signed I)
Definition: FoldingSet.cpp:60
static ExponentType semanticsMaxExponent(const fltSemantics &)
Definition: APFloat.cpp:194
ELFYAML::ELF_STO Other
Definition: ELFYAML.cpp:877
Generic base class for SMT Solvers.
Definition: SMTAPI.h:136
static unsigned int semanticsSizeInBits(const fltSemantics &)
Definition: APFloat.cpp:201
static const fltSemantics & IEEEdouble() LLVM_READNONE
Definition: APFloat.cpp:158
static ExponentType semanticsMinExponent(const fltSemantics &)
Definition: APFloat.cpp:198
FoldingSetNodeID - This class is used to gather all the unique data bits of a node.
Definition: FoldingSet.h:305
virtual bool isBooleanSort() const
Returns true if the sort is a boolean, calls isBooleanSortImpl().
Definition: SMTAPI.h:38
void dump(const SparseBitVector< ElementSize > &LHS, raw_ostream &out)
static GCRegistry::Add< CoreCLRGC > E("coreclr", "CoreCLR-compatible GC")
static void print(raw_ostream &Out, object::Archive::Kind Kind, T Val)
LLVM_DUMP_METHOD void dump() const
Definition: Z3Solver.cpp:899
#define llvm_unreachable(msg)
Marks that the current location is not supposed to be reachable.
static const fltSemantics & IEEEsingle() LLVM_READNONE
Definition: APFloat.cpp:155
BlockVerifier::State From
static const fltSemantics & IEEEhalf() LLVM_READNONE
Definition: APFloat.cpp:152
static unsigned int semanticsPrecision(const fltSemantics &)
Definition: APFloat.cpp:190
bool isUnsigned() const
Definition: APSInt.h:77
Class for arbitrary precision integers.
Definition: APInt.h:69
virtual bool isBitvectorSort() const
Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
Definition: SMTAPI.h:32
virtual bool isFloatSort() const
Returns true if the sort is a floating-point, calls isFloatSortImpl().
Definition: SMTAPI.h:35
LLVM_DUMP_METHOD void dump() const
Definition: Z3Solver.cpp:900
virtual unsigned getBitvectorSortSize() const
Returns the bitvector size, fails if the sort is not a bitvector Calls getBitvectorSortSizeImpl().
Definition: SMTAPI.h:42
Generic base class for SMT sorts.
Definition: SMTAPI.h:26
assert(ImpDefSCC.getReg()==AMDGPU::SCC &&ImpDefSCC.isDef())
SMTSolverRef CreateZ3Solver()
Convenience method to create and Z3Solver object.
Definition: Z3Solver.cpp:887
void toString(SmallVectorImpl< char > &Str, unsigned Radix=10) const
toString - Append this APSInt to the specified SmallString.
Definition: APSInt.h:82
Lightweight error class with error context and mandatory checking.
Definition: Error.h:157
This class implements an extremely fast bulk output stream that can only output to a stream...
Definition: raw_ostream.h:45
APInt bitcastToAPInt() const
Definition: APFloat.h:1104
std::shared_ptr< SMTSolver > SMTSolverRef
Shared pointer for SMTSolvers.
Definition: SMTAPI.h:440
constexpr char Args[]
Key for Kernel::Metadata::mArgs.