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