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