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_ex(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) : SMTSort(), 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 &Copy)
86  : SMTSort(), Context(Copy.Context), Sort(Copy.Sort) {
87  Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
88  }
89 
90  /// Provide move constructor
91  Z3Sort(Z3Sort &&Move) : SMTSort(), Context(Move.Context), Sort(nullptr) {
92  *this = std::move(Move);
93  }
94 
95  /// Provide move assignment constructor
96  Z3Sort &operator=(Z3Sort &&Move) {
97  if (this != &Move) {
98  if (Sort)
99  Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
100  Sort = Move.Sort;
101  Move.Sort = nullptr;
102  }
103  return *this;
104  }
105 
106  ~Z3Sort() {
107  if (Sort)
108  Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
109  }
110 
111  bool isBitvectorSortImpl() const override {
112  return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
113  }
114 
115  bool isFloatSortImpl() const override {
116  return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
117  }
118 
119  bool isBooleanSortImpl() const override {
120  return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);
121  }
122 
123  unsigned getBitvectorSortSizeImpl() const override {
124  return Z3_get_bv_sort_size(Context.Context, Sort);
125  }
126 
127  unsigned getFloatSortSizeImpl() const override {
128  return Z3_fpa_get_ebits(Context.Context, Sort) +
129  Z3_fpa_get_sbits(Context.Context, Sort);
130  }
131 
132  bool equal_to(SMTSort const &Other) const override {
133  return Z3_is_eq_sort(Context.Context, Sort,
134  static_cast<const Z3Sort &>(Other).Sort);
135  }
136 
137  Z3Sort &operator=(const Z3Sort &Move) {
138  Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Move.Sort));
139  Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
140  Sort = Move.Sort;
141  return *this;
142  }
143 
144  void print(raw_ostream &OS) const override {
145  OS << Z3_sort_to_string(Context.Context, Sort);
146  }
147 }; // end class Z3Sort
148 
149 static const Z3Sort &toZ3Sort(const SMTSort &S) {
150  return static_cast<const Z3Sort &>(S);
151 }
152 
153 class Z3Expr : public SMTExpr {
154  friend class Z3Solver;
155 
156  Z3Context &Context;
157 
158  Z3_ast AST;
159 
160 public:
161  Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
162  Z3_inc_ref(Context.Context, AST);
163  }
164 
165  /// Override implicit copy constructor for correct reference counting.
166  Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
167  Z3_inc_ref(Context.Context, AST);
168  }
169 
170  /// Provide move constructor
171  Z3Expr(Z3Expr &&Move) : SMTExpr(), Context(Move.Context), AST(nullptr) {
172  *this = std::move(Move);
173  }
174 
175  /// Provide move assignment constructor
176  Z3Expr &operator=(Z3Expr &&Move) {
177  if (this != &Move) {
178  if (AST)
179  Z3_dec_ref(Context.Context, AST);
180  AST = Move.AST;
181  Move.AST = nullptr;
182  }
183  return *this;
184  }
185 
186  ~Z3Expr() {
187  if (AST)
188  Z3_dec_ref(Context.Context, AST);
189  }
190 
191  void Profile(llvm::FoldingSetNodeID &ID) const override {
192  ID.AddInteger(Z3_get_ast_hash(Context.Context, AST));
193  }
194 
195  /// Comparison of AST equality, not model equivalence.
196  bool equal_to(SMTExpr const &Other) const override {
197  assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
198  Z3_get_sort(Context.Context,
199  static_cast<const Z3Expr &>(Other).AST)) &&
200  "AST's must have the same sort");
201  return Z3_is_eq_ast(Context.Context, AST,
202  static_cast<const Z3Expr &>(Other).AST);
203  }
204 
205  /// Override implicit move constructor for correct reference counting.
206  Z3Expr &operator=(const Z3Expr &Move) {
207  Z3_inc_ref(Context.Context, Move.AST);
208  Z3_dec_ref(Context.Context, AST);
209  AST = Move.AST;
210  return *this;
211  }
212 
213  void print(raw_ostream &OS) const override {
214  OS << Z3_ast_to_string(Context.Context, AST);
215  }
216 }; // end class Z3Expr
217 
218 static const Z3Expr &toZ3Expr(const SMTExpr &E) {
219  return static_cast<const Z3Expr &>(E);
220 }
221 
222 class Z3Model {
223  friend class Z3Solver;
224 
225  Z3Context &Context;
226 
227  Z3_model Model;
228 
229 public:
230  Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) {
231  assert(C.Context != nullptr);
232  Z3_model_inc_ref(Context.Context, Model);
233  }
234 
235  /// Override implicit copy constructor for correct reference counting.
236  Z3Model(const Z3Model &Copy) : Context(Copy.Context), Model(Copy.Model) {
237  Z3_model_inc_ref(Context.Context, Model);
238  }
239 
240  /// Provide move constructor
241  Z3Model(Z3Model &&Move) : Context(Move.Context), Model(nullptr) {
242  *this = std::move(Move);
243  }
244 
245  /// Provide move assignment constructor
246  Z3Model &operator=(Z3Model &&Move) {
247  if (this != &Move) {
248  if (Model)
249  Z3_model_dec_ref(Context.Context, Model);
250  Model = Move.Model;
251  Move.Model = nullptr;
252  }
253  return *this;
254  }
255 
256  ~Z3Model() {
257  if (Model)
258  Z3_model_dec_ref(Context.Context, Model);
259  }
260 
261  void print(raw_ostream &OS) const {
262  OS << Z3_model_to_string(Context.Context, Model);
263  }
264 
265  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
266 }; // end class Z3Model
267 
268 /// Get the corresponding IEEE floating-point type for a given bitwidth.
269 static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
270  switch (BitWidth) {
271  default:
272  llvm_unreachable("Unsupported floating-point semantics!");
273  break;
274  case 16:
275  return llvm::APFloat::IEEEhalf();
276  case 32:
277  return llvm::APFloat::IEEEsingle();
278  case 64:
279  return llvm::APFloat::IEEEdouble();
280  case 128:
281  return llvm::APFloat::IEEEquad();
282  }
283 }
284 
285 // Determine whether two float semantics are equivalent
286 static bool areEquivalent(const llvm::fltSemantics &LHS,
287  const llvm::fltSemantics &RHS) {
288  return (llvm::APFloat::semanticsPrecision(LHS) ==
289  llvm::APFloat::semanticsPrecision(RHS)) &&
290  (llvm::APFloat::semanticsMinExponent(LHS) ==
291  llvm::APFloat::semanticsMinExponent(RHS)) &&
292  (llvm::APFloat::semanticsMaxExponent(LHS) ==
293  llvm::APFloat::semanticsMaxExponent(RHS)) &&
294  (llvm::APFloat::semanticsSizeInBits(LHS) ==
295  llvm::APFloat::semanticsSizeInBits(RHS));
296 }
297 
298 } // end anonymous namespace
299 
300 typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
301 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, ConstraintZ3Ty)
302 
303 namespace {
304 
305 class Z3Solver : public SMTSolver {
306  friend class Z3ConstraintManager;
307 
308  Z3Context Context;
309 
310  Z3_solver Solver;
311 
312 public:
313  Z3Solver() : SMTSolver(), Solver(Z3_mk_simple_solver(Context.Context)) {
314  Z3_solver_inc_ref(Context.Context, Solver);
315  }
316 
317  /// Override implicit copy constructor for correct reference counting.
318  Z3Solver(const Z3Solver &Copy)
319  : SMTSolver(), Context(Copy.Context), Solver(Copy.Solver) {
320  Z3_solver_inc_ref(Context.Context, Solver);
321  }
322 
323  /// Provide move constructor
324  Z3Solver(Z3Solver &&Move)
325  : SMTSolver(), Context(Move.Context), Solver(nullptr) {
326  *this = std::move(Move);
327  }
328 
329  /// Provide move assignment constructor
330  Z3Solver &operator=(Z3Solver &&Move) {
331  if (this != &Move) {
332  if (Solver)
333  Z3_solver_dec_ref(Context.Context, Solver);
334  Solver = Move.Solver;
335  Move.Solver = nullptr;
336  }
337  return *this;
338  }
339 
340  ~Z3Solver() {
341  if (Solver)
342  Z3_solver_dec_ref(Context.Context, Solver);
343  }
344 
345  void addConstraint(const SMTExprRef &Exp) const override {
346  Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
347  }
348 
349  SMTSortRef getBoolSort() override {
350  return std::make_shared<Z3Sort>(Context, Z3_mk_bool_sort(Context.Context));
351  }
352 
353  SMTSortRef getBitvectorSort(unsigned BitWidth) override {
354  return std::make_shared<Z3Sort>(Context,
355  Z3_mk_bv_sort(Context.Context, BitWidth));
356  }
357 
358  SMTSortRef getSort(const SMTExprRef &Exp) override {
359  return std::make_shared<Z3Sort>(
360  Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST));
361  }
362 
363  SMTSortRef getFloat16Sort() override {
364  return std::make_shared<Z3Sort>(Context,
365  Z3_mk_fpa_sort_16(Context.Context));
366  }
367 
368  SMTSortRef getFloat32Sort() override {
369  return std::make_shared<Z3Sort>(Context,
370  Z3_mk_fpa_sort_32(Context.Context));
371  }
372 
373  SMTSortRef getFloat64Sort() override {
374  return std::make_shared<Z3Sort>(Context,
375  Z3_mk_fpa_sort_64(Context.Context));
376  }
377 
378  SMTSortRef getFloat128Sort() override {
379  return std::make_shared<Z3Sort>(Context,
380  Z3_mk_fpa_sort_128(Context.Context));
381  }
382 
383  SMTExprRef newExprRef(const SMTExpr &E) const override {
384  return std::make_shared<Z3Expr>(toZ3Expr(E));
385  }
386 
387  SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {
388  return newExprRef(
389  Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
390  }
391 
392  SMTExprRef mkBVNot(const SMTExprRef &Exp) override {
393  return newExprRef(
394  Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
395  }
396 
397  SMTExprRef mkNot(const SMTExprRef &Exp) override {
398  return newExprRef(
399  Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
400  }
401 
402  SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
403  return newExprRef(
404  Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
405  toZ3Expr(*RHS).AST)));
406  }
407 
408  SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
409  return newExprRef(
410  Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
411  toZ3Expr(*RHS).AST)));
412  }
413 
414  SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
415  return newExprRef(
416  Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
417  toZ3Expr(*RHS).AST)));
418  }
419 
420  SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
421  return newExprRef(
422  Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
423  toZ3Expr(*RHS).AST)));
424  }
425 
426  SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
427  return newExprRef(
428  Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
429  toZ3Expr(*RHS).AST)));
430  }
431 
432  SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
433  return newExprRef(
434  Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
435  toZ3Expr(*RHS).AST)));
436  }
437 
438  SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
439  return newExprRef(
440  Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
441  toZ3Expr(*RHS).AST)));
442  }
443 
444  SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
445  return newExprRef(
446  Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
447  toZ3Expr(*RHS).AST)));
448  }
449 
450  SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
451  return newExprRef(
452  Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
453  toZ3Expr(*RHS).AST)));
454  }
455 
456  SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
457  return newExprRef(
458  Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
459  toZ3Expr(*RHS).AST)));
460  }
461 
462  SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
463  return newExprRef(
464  Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
465  toZ3Expr(*RHS).AST)));
466  }
467 
468  SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
469  return newExprRef(
470  Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
471  toZ3Expr(*RHS).AST)));
472  }
473 
474  SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
475  return newExprRef(
476  Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
477  toZ3Expr(*RHS).AST)));
478  }
479 
480  SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
481  return newExprRef(
482  Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
483  toZ3Expr(*RHS).AST)));
484  }
485 
486  SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
487  return newExprRef(
488  Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
489  toZ3Expr(*RHS).AST)));
490  }
491 
492  SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
493  return newExprRef(
494  Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
495  toZ3Expr(*RHS).AST)));
496  }
497 
498  SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
499  return newExprRef(
500  Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
501  toZ3Expr(*RHS).AST)));
502  }
503 
504  SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
505  return newExprRef(
506  Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
507  toZ3Expr(*RHS).AST)));
508  }
509 
510  SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
511  return newExprRef(
512  Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
513  toZ3Expr(*RHS).AST)));
514  }
515 
516  SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
517  return newExprRef(
518  Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
519  toZ3Expr(*RHS).AST)));
520  }
521 
522  SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
523  return newExprRef(
524  Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
525  toZ3Expr(*RHS).AST)));
526  }
527 
528  SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
529  Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
530  return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));
531  }
532 
533  SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
534  Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
535  return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));
536  }
537 
538  SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
539  return newExprRef(
540  Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
541  toZ3Expr(*RHS).AST)));
542  }
543 
544  SMTExprRef mkFPNeg(const SMTExprRef &Exp) override {
545  return newExprRef(
546  Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
547  }
548 
549  SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override {
550  return newExprRef(Z3Expr(
551  Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
552  }
553 
554  SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override {
555  return newExprRef(
556  Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
557  }
558 
559  SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override {
560  return newExprRef(Z3Expr(
561  Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
562  }
563 
564  SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {
565  return newExprRef(Z3Expr(
566  Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
567  }
568 
569  SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
570  SMTExprRef RoundingMode = getFloatRoundingMode();
571  return newExprRef(
572  Z3Expr(Context,
573  Z3_mk_fpa_mul(Context.Context, toZ3Expr(*LHS).AST,
574  toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
575  }
576 
577  SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
578  SMTExprRef RoundingMode = getFloatRoundingMode();
579  return newExprRef(
580  Z3Expr(Context,
581  Z3_mk_fpa_div(Context.Context, toZ3Expr(*LHS).AST,
582  toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
583  }
584 
585  SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
586  return newExprRef(
587  Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
588  toZ3Expr(*RHS).AST)));
589  }
590 
591  SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
592  SMTExprRef RoundingMode = getFloatRoundingMode();
593  return newExprRef(
594  Z3Expr(Context,
595  Z3_mk_fpa_add(Context.Context, toZ3Expr(*LHS).AST,
596  toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
597  }
598 
599  SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
600  SMTExprRef RoundingMode = getFloatRoundingMode();
601  return newExprRef(
602  Z3Expr(Context,
603  Z3_mk_fpa_sub(Context.Context, toZ3Expr(*LHS).AST,
604  toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
605  }
606 
607  SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
608  return newExprRef(
609  Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
610  toZ3Expr(*RHS).AST)));
611  }
612 
613  SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
614  return newExprRef(
615  Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
616  toZ3Expr(*RHS).AST)));
617  }
618 
619  SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
620  return newExprRef(
621  Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
622  toZ3Expr(*RHS).AST)));
623  }
624 
625  SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
626  return newExprRef(
627  Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
628  toZ3Expr(*RHS).AST)));
629  }
630 
631  SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
632  return newExprRef(
633  Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
634  toZ3Expr(*RHS).AST)));
635  }
636 
637  SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
638  const SMTExprRef &F) override {
639  return newExprRef(
640  Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
641  toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
642  }
643 
644  SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {
645  return newExprRef(Z3Expr(
646  Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
647  }
648 
649  SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {
650  return newExprRef(Z3Expr(
651  Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
652  }
653 
654  SMTExprRef mkBVExtract(unsigned High, unsigned Low,
655  const SMTExprRef &Exp) override {
656  return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,
657  toZ3Expr(*Exp).AST)));
658  }
659 
660  SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
661  return newExprRef(
662  Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
663  toZ3Expr(*RHS).AST)));
664  }
665 
666  SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
667  SMTExprRef RoundingMode = getFloatRoundingMode();
668  return newExprRef(Z3Expr(
669  Context,
670  Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
671  toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
672  }
673 
674  SMTExprRef mkFPtoSBV(const SMTExprRef &From, const SMTSortRef &To) override {
675  SMTExprRef RoundingMode = getFloatRoundingMode();
676  return newExprRef(Z3Expr(
677  Context,
678  Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
679  toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
680  }
681 
682  SMTExprRef mkFPtoUBV(const SMTExprRef &From, const SMTSortRef &To) override {
683  SMTExprRef RoundingMode = getFloatRoundingMode();
684  return newExprRef(Z3Expr(
685  Context,
686  Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
687  toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
688  }
689 
690  SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) override {
691  SMTExprRef RoundingMode = getFloatRoundingMode();
692  return newExprRef(Z3Expr(
693  Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
694  toZ3Expr(*From).AST, ToWidth)));
695  }
696 
697  SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) override {
698  SMTExprRef RoundingMode = getFloatRoundingMode();
699  return newExprRef(Z3Expr(
700  Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
701  toZ3Expr(*From).AST, ToWidth)));
702  }
703 
704  SMTExprRef mkBoolean(const bool b) override {
705  return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
706  : Z3_mk_false(Context.Context)));
707  }
708 
709  SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {
710  const SMTSortRef Sort = getBitvectorSort(BitWidth);
711  return newExprRef(
712  Z3Expr(Context, Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
713  toZ3Sort(*Sort).Sort)));
714  }
715 
716  SMTExprRef mkFloat(const llvm::APFloat Float) override {
717  SMTSortRef Sort =
718  getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
719 
720  llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
721  SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth());
722  return newExprRef(Z3Expr(
723  Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
724  toZ3Sort(*Sort).Sort)));
725  }
726 
727  SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {
728  return newExprRef(
729  Z3Expr(Context, Z3_mk_const(Context.Context,
730  Z3_mk_string_symbol(Context.Context, Name),
731  toZ3Sort(*Sort).Sort)));
732  }
733 
734  llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
735  bool isUnsigned) override {
736  return llvm::APSInt(llvm::APInt(
737  BitWidth, Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
738  10));
739  }
740 
741  bool getBoolean(const SMTExprRef &Exp) override {
742  return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
743  }
744 
745  SMTExprRef getFloatRoundingMode() override {
746  // TODO: Don't assume nearest ties to even rounding mode
747  return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
748  }
749 
750  SMTExprRef fromBoolean(const bool Bool) override {
751  Z3_ast AST =
752  Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context);
753  return newExprRef(Z3Expr(Context, AST));
754  }
755 
756  SMTExprRef fromAPFloat(const llvm::APFloat &Float) override {
757  SMTSortRef Sort =
758  getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
759 
760  llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
761  SMTExprRef Z3Int = fromAPSInt(Int);
762  return newExprRef(Z3Expr(
763  Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
764  toZ3Sort(*Sort).Sort)));
765  }
766 
767  SMTExprRef fromAPSInt(const llvm::APSInt &Int) override {
768  SMTSortRef Sort = getBitvectorSort(Int.getBitWidth());
769  Z3_ast AST = Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
770  toZ3Sort(*Sort).Sort);
771  return newExprRef(Z3Expr(Context, AST));
772  }
773 
774  SMTExprRef fromInt(const char *Int, uint64_t BitWidth) override {
775  SMTSortRef Sort = getBitvectorSort(BitWidth);
776  Z3_ast AST = Z3_mk_numeral(Context.Context, Int, toZ3Sort(*Sort).Sort);
777  return newExprRef(Z3Expr(Context, AST));
778  }
779 
780  bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
781  llvm::APFloat &Float, bool useSemantics) {
782  assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");
783 
784  llvm::APSInt Int(Sort->getFloatSortSize(), true);
785  const llvm::fltSemantics &Semantics =
786  getFloatSemantics(Sort->getFloatSortSize());
787  SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());
788  if (!toAPSInt(BVSort, AST, Int, true)) {
789  return false;
790  }
791 
792  if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
793  assert(false && "Floating-point types don't match!");
794  return false;
795  }
796 
797  Float = llvm::APFloat(Semantics, Int);
798  return true;
799  }
800 
801  bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,
802  llvm::APSInt &Int, bool useSemantics) {
803  if (Sort->isBitvectorSort()) {
804  if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {
805  assert(false && "Bitvector types don't match!");
806  return false;
807  }
808 
809  // FIXME: This function is also used to retrieve floating-point values,
810  // which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything
811  // between 1 and 64 bits long, which is the reason we have this weird
812  // guard. In the future, we need proper calls in the backend to retrieve
813  // floating-points and its special values (NaN, +/-infinity, +/-zero),
814  // then we can drop this weird condition.
815  if (Sort->getBitvectorSortSize() <= 64 ||
816  Sort->getBitvectorSortSize() == 128) {
817  Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
818  return true;
819  }
820 
821  assert(false && "Bitwidth not supported!");
822  return false;
823  }
824 
825  if (Sort->isBooleanSort()) {
826  if (useSemantics && Int.getBitWidth() < 1) {
827  assert(false && "Boolean type doesn't match!");
828  return false;
829  }
830 
831  Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),
832  Int.isUnsigned());
833  return true;
834  }
835 
836  llvm_unreachable("Unsupported sort to integer!");
837  }
838 
839  bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
840  Z3Model Model = getModel();
841  Z3_func_decl Func = Z3_get_app_decl(
842  Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
843  if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
844  return false;
845 
846  SMTExprRef Assign = newExprRef(
847  Z3Expr(Context,
848  Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
849  SMTSortRef Sort = getSort(Assign);
850  return toAPSInt(Sort, Assign, Int, true);
851  }
852 
853  bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
854  Z3Model Model = getModel();
855  Z3_func_decl Func = Z3_get_app_decl(
856  Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
857  if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
858  return false;
859 
860  SMTExprRef Assign = newExprRef(
861  Z3Expr(Context,
862  Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
863  SMTSortRef Sort = getSort(Assign);
864  return toAPFloat(Sort, Assign, Float, true);
865  }
866 
867  Optional<bool> check() const override {
868  Z3_lbool res = Z3_solver_check(Context.Context, Solver);
869  if (res == Z3_L_TRUE)
870  return true;
871 
872  if (res == Z3_L_FALSE)
873  return false;
874 
875  return Optional<bool>();
876  }
877 
878  void push() override { return Z3_solver_push(Context.Context, Solver); }
879 
880  void pop(unsigned NumStates = 1) override {
881  assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
882  return Z3_solver_pop(Context.Context, Solver, NumStates);
883  }
884 
885  /// Get a model from the solver. Caller should check the model is
886  /// satisfiable.
887  Z3Model getModel() {
888  return Z3Model(Context, Z3_solver_get_model(Context.Context, Solver));
889  }
890 
891  /// Reset the solver and remove all constraints.
892  void reset() const 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 class Z3ConstraintManager : public SMTConstraintManager<ConstraintZ3, Z3Expr> {
900  SMTSolverRef Solver = CreateZ3Solver();
901 
902 public:
903  Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
904  : SMTConstraintManager(SE, SB, Solver) {}
905 
906  bool canReasonAbout(SVal X) const override {
907  const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
908 
909  Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
910  if (!SymVal)
911  return true;
912 
913  const SymExpr *Sym = SymVal->getSymbol();
914  QualType Ty = Sym->getType();
915 
916  // Complex types are not modeled
917  if (Ty->isComplexType() || Ty->isComplexIntegerType())
918  return false;
919 
920  // Non-IEEE 754 floating-point types are not modeled
921  if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
922  (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
923  &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
924  return false;
925 
926  if (isa<SymbolData>(Sym))
927  return true;
928 
929  SValBuilder &SVB = getSValBuilder();
930 
931  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
932  return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
933 
934  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
935  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
936  return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
937 
938  if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
939  return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
940 
941  if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
942  return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
943  canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
944  }
945 
946  llvm_unreachable("Unsupported expression to reason about!");
947  }
948 }; // end class Z3ConstraintManager
949 
950 } // end anonymous namespace
951 
952 #endif
953 
955 #if CLANG_ANALYZER_WITH_Z3
956  return llvm::make_unique<Z3Solver>();
957 #else
958  llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
959  "with -DCLANG_ANALYZER_BUILD_Z3=ON",
960  false);
961  return nullptr;
962 #endif
963 }
964 
965 std::unique_ptr<ConstraintManager>
967 #if CLANG_ANALYZER_WITH_Z3
968  return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
969 #else
970  llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
971  "with -DCLANG_ANALYZER_BUILD_Z3=ON",
972  false);
973  return nullptr;
974 #endif
975 }
A (possibly-)qualified type.
Definition: Type.h:642
std::shared_ptr< SMTSort > SMTSortRef
Shared pointer for SMTSorts, used by SMTSolver API.
Definition: SMTSort.h:86
bool isSpecificBuiltinType(unsigned K) const
Test for a particular builtin type.
Definition: Type.h:6371
static void dump(llvm::raw_ostream &OS, StringRef FunctionName, ArrayRef< CounterExpression > Expressions, ArrayRef< CounterMappingRegion > Regions)
std::unique_ptr< ConstraintManager > CreateZ3ConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine)
bool isComplexType() const
isComplexType() does not include complex integers (a GCC extension).
Definition: Type.cpp:473
const llvm::fltSemantics & getLongDoubleFormat() const
Definition: TargetInfo.h:575
Exposes information about the current target.
Definition: TargetInfo.h:54
#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:304
X
Add a minimal nested name specifier fixit hint to allow lookup of a tag name from an outer enclosing ...
Definition: SemaDecl.cpp:13824
Defines the clang::TargetInfo interface.
bool isComplexIntegerType() const
Definition: Type.cpp:479
std::shared_ptr< SMTExpr > SMTExprRef
Shared pointer for SMTExprs, used by SMTSolver API.
Definition: SMTExpr.h:57