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