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