clang  7.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"
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 // Forward declarations
25 namespace {
26 class Z3Expr;
27 class ConstraintZ3 {};
28 } // end anonymous namespace
29 
30 typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
31 
32 // Expansion of REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, Z3SetPair)
33 namespace clang {
34 namespace ento {
35 template <>
36 struct ProgramStateTrait<ConstraintZ3>
37  : public ProgramStatePartialTrait<ConstraintZ3Ty> {
38  static void *GDMIndex() {
39  static int Index;
40  return &Index;
41  }
42 };
43 } // end namespace ento
44 } // end namespace clang
45 
46 namespace {
47 
48 class Z3Config {
49  friend class Z3Context;
50 
51  Z3_config Config;
52 
53 public:
54  Z3Config() : Config(Z3_mk_config()) {
55  // Enable model finding
56  Z3_set_param_value(Config, "model", "true");
57  // Disable proof generation
58  Z3_set_param_value(Config, "proof", "false");
59  // Set timeout to 15000ms = 15s
60  Z3_set_param_value(Config, "timeout", "15000");
61  }
62 
63  ~Z3Config() { Z3_del_config(Config); }
64 }; // end class Z3Config
65 
66 class Z3Context {
67  Z3_context ZC_P;
68 
69 public:
70  static Z3_context ZC;
71 
72  Z3Context() : ZC_P(Z3_mk_context_rc(Z3Config().Config)) { ZC = ZC_P; }
73 
74  ~Z3Context() {
75  Z3_del_context(ZC);
76  Z3_finalize_memory();
77  ZC_P = nullptr;
78  }
79 }; // end class Z3Context
80 
81 class Z3Sort {
82  friend class Z3Expr;
83 
84  Z3_sort Sort;
85 
86  Z3Sort() : Sort(nullptr) {}
87  Z3Sort(Z3_sort ZS) : Sort(ZS) {
88  Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
89  }
90 
91 public:
92  /// Override implicit copy constructor for correct reference counting.
93  Z3Sort(const Z3Sort &Copy) : Sort(Copy.Sort) {
94  Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
95  }
96 
97  /// Provide move constructor
98  Z3Sort(Z3Sort &&Move) : Sort(nullptr) { *this = std::move(Move); }
99 
100  /// Provide move assignment constructor
101  Z3Sort &operator=(Z3Sort &&Move) {
102  if (this != &Move) {
103  if (Sort)
104  Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
105  Sort = Move.Sort;
106  Move.Sort = nullptr;
107  }
108  return *this;
109  }
110 
111  ~Z3Sort() {
112  if (Sort)
113  Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
114  }
115 
116  // Return a boolean sort.
117  static Z3Sort getBoolSort() { return Z3Sort(Z3_mk_bool_sort(Z3Context::ZC)); }
118 
119  // Return an appropriate bitvector sort for the given bitwidth.
120  static Z3Sort getBitvectorSort(unsigned BitWidth) {
121  return Z3Sort(Z3_mk_bv_sort(Z3Context::ZC, BitWidth));
122  }
123 
124  // Return an appropriate floating-point sort for the given bitwidth.
125  static Z3Sort getFloatSort(unsigned BitWidth) {
126  Z3_sort Sort;
127 
128  switch (BitWidth) {
129  default:
130  llvm_unreachable("Unsupported floating-point bitwidth!");
131  break;
132  case 16:
133  Sort = Z3_mk_fpa_sort_16(Z3Context::ZC);
134  break;
135  case 32:
136  Sort = Z3_mk_fpa_sort_32(Z3Context::ZC);
137  break;
138  case 64:
139  Sort = Z3_mk_fpa_sort_64(Z3Context::ZC);
140  break;
141  case 128:
142  Sort = Z3_mk_fpa_sort_128(Z3Context::ZC);
143  break;
144  }
145  return Z3Sort(Sort);
146  }
147 
148  // Return an appropriate sort for the given AST.
149  static Z3Sort getSort(Z3_ast AST) {
150  return Z3Sort(Z3_get_sort(Z3Context::ZC, AST));
151  }
152 
153  Z3_sort_kind getSortKind() const {
154  return Z3_get_sort_kind(Z3Context::ZC, Sort);
155  }
156 
157  unsigned getBitvectorSortSize() const {
158  assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!");
159  return Z3_get_bv_sort_size(Z3Context::ZC, Sort);
160  }
161 
162  unsigned getFloatSortSize() const {
163  assert(getSortKind() == Z3_FLOATING_POINT_SORT &&
164  "Not a floating-point sort!");
165  return Z3_fpa_get_ebits(Z3Context::ZC, Sort) +
166  Z3_fpa_get_sbits(Z3Context::ZC, Sort);
167  }
168 
169  bool operator==(const Z3Sort &Other) const {
170  return Z3_is_eq_sort(Z3Context::ZC, Sort, Other.Sort);
171  }
172 
173  Z3Sort &operator=(const Z3Sort &Move) {
174  Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Move.Sort));
175  Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
176  Sort = Move.Sort;
177  return *this;
178  }
179 
180  void print(raw_ostream &OS) const {
181  OS << Z3_sort_to_string(Z3Context::ZC, Sort);
182  }
183 
184  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
185 }; // end class Z3Sort
186 
187 class Z3Expr {
188  friend class Z3Model;
189  friend class Z3Solver;
190 
191  Z3_ast AST;
192 
193  Z3Expr(Z3_ast ZA) : AST(ZA) { Z3_inc_ref(Z3Context::ZC, AST); }
194 
195  // Return an appropriate floating-point rounding mode.
196  static Z3Expr getFloatRoundingMode() {
197  // TODO: Don't assume nearest ties to even rounding mode
198  return Z3Expr(Z3_mk_fpa_rne(Z3Context::ZC));
199  }
200 
201  // Determine whether two float semantics are equivalent
202  static bool areEquivalent(const llvm::fltSemantics &LHS,
203  const llvm::fltSemantics &RHS) {
204  return (llvm::APFloat::semanticsPrecision(LHS) ==
205  llvm::APFloat::semanticsPrecision(RHS)) &&
206  (llvm::APFloat::semanticsMinExponent(LHS) ==
207  llvm::APFloat::semanticsMinExponent(RHS)) &&
208  (llvm::APFloat::semanticsMaxExponent(LHS) ==
209  llvm::APFloat::semanticsMaxExponent(RHS)) &&
210  (llvm::APFloat::semanticsSizeInBits(LHS) ==
211  llvm::APFloat::semanticsSizeInBits(RHS));
212  }
213 
214 public:
215  /// Override implicit copy constructor for correct reference counting.
216  Z3Expr(const Z3Expr &Copy) : AST(Copy.AST) { Z3_inc_ref(Z3Context::ZC, AST); }
217 
218  /// Provide move constructor
219  Z3Expr(Z3Expr &&Move) : AST(nullptr) { *this = std::move(Move); }
220 
221  /// Provide move assignment constructor
222  Z3Expr &operator=(Z3Expr &&Move) {
223  if (this != &Move) {
224  if (AST)
225  Z3_dec_ref(Z3Context::ZC, AST);
226  AST = Move.AST;
227  Move.AST = nullptr;
228  }
229  return *this;
230  }
231 
232  ~Z3Expr() {
233  if (AST)
234  Z3_dec_ref(Z3Context::ZC, AST);
235  }
236 
237  /// Get the corresponding IEEE floating-point type for a given bitwidth.
238  static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
239  switch (BitWidth) {
240  default:
241  llvm_unreachable("Unsupported floating-point semantics!");
242  break;
243  case 16:
244  return llvm::APFloat::IEEEhalf();
245  case 32:
246  return llvm::APFloat::IEEEsingle();
247  case 64:
248  return llvm::APFloat::IEEEdouble();
249  case 128:
250  return llvm::APFloat::IEEEquad();
251  }
252  }
253 
254  /// Construct a Z3Expr from a unary operator, given a Z3_context.
255  static Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr &Exp) {
256  Z3_ast AST;
257 
258  switch (Op) {
259  default:
260  llvm_unreachable("Unimplemented opcode");
261  break;
262 
263  case UO_Minus:
264  AST = Z3_mk_bvneg(Z3Context::ZC, Exp.AST);
265  break;
266 
267  case UO_Not:
268  AST = Z3_mk_bvnot(Z3Context::ZC, Exp.AST);
269  break;
270 
271  case UO_LNot:
272  AST = Z3_mk_not(Z3Context::ZC, Exp.AST);
273  break;
274  }
275 
276  return Z3Expr(AST);
277  }
278 
279  /// Construct a Z3Expr from a floating-point unary operator, given a
280  /// Z3_context.
281  static Z3Expr fromFloatUnOp(const UnaryOperator::Opcode Op,
282  const Z3Expr &Exp) {
283  Z3_ast AST;
284 
285  switch (Op) {
286  default:
287  llvm_unreachable("Unimplemented opcode");
288  break;
289 
290  case UO_Minus:
291  AST = Z3_mk_fpa_neg(Z3Context::ZC, Exp.AST);
292  break;
293 
294  case UO_LNot:
295  return Z3Expr::fromUnOp(Op, Exp);
296  }
297 
298  return Z3Expr(AST);
299  }
300 
301  /// Construct a Z3Expr from a n-ary binary operator.
302  static Z3Expr fromNBinOp(const BinaryOperator::Opcode Op,
303  const std::vector<Z3_ast> &ASTs) {
304  Z3_ast AST;
305 
306  switch (Op) {
307  default:
308  llvm_unreachable("Unimplemented opcode");
309  break;
310 
311  case BO_LAnd:
312  AST = Z3_mk_and(Z3Context::ZC, ASTs.size(), ASTs.data());
313  break;
314 
315  case BO_LOr:
316  AST = Z3_mk_or(Z3Context::ZC, ASTs.size(), ASTs.data());
317  break;
318  }
319 
320  return Z3Expr(AST);
321  }
322 
323  /// Construct a Z3Expr from a binary operator, given a Z3_context.
324  static Z3Expr fromBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode Op,
325  const Z3Expr &RHS, bool isSigned) {
326  Z3_ast AST;
327 
328  assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
329  "AST's must have the same sort!");
330 
331  switch (Op) {
332  default:
333  llvm_unreachable("Unimplemented opcode");
334  break;
335 
336  // Multiplicative operators
337  case BO_Mul:
338  AST = Z3_mk_bvmul(Z3Context::ZC, LHS.AST, RHS.AST);
339  break;
340  case BO_Div:
341  AST = isSigned ? Z3_mk_bvsdiv(Z3Context::ZC, LHS.AST, RHS.AST)
342  : Z3_mk_bvudiv(Z3Context::ZC, LHS.AST, RHS.AST);
343  break;
344  case BO_Rem:
345  AST = isSigned ? Z3_mk_bvsrem(Z3Context::ZC, LHS.AST, RHS.AST)
346  : Z3_mk_bvurem(Z3Context::ZC, LHS.AST, RHS.AST);
347  break;
348 
349  // Additive operators
350  case BO_Add:
351  AST = Z3_mk_bvadd(Z3Context::ZC, LHS.AST, RHS.AST);
352  break;
353  case BO_Sub:
354  AST = Z3_mk_bvsub(Z3Context::ZC, LHS.AST, RHS.AST);
355  break;
356 
357  // Bitwise shift operators
358  case BO_Shl:
359  AST = Z3_mk_bvshl(Z3Context::ZC, LHS.AST, RHS.AST);
360  break;
361  case BO_Shr:
362  AST = isSigned ? Z3_mk_bvashr(Z3Context::ZC, LHS.AST, RHS.AST)
363  : Z3_mk_bvlshr(Z3Context::ZC, LHS.AST, RHS.AST);
364  break;
365 
366  // Relational operators
367  case BO_LT:
368  AST = isSigned ? Z3_mk_bvslt(Z3Context::ZC, LHS.AST, RHS.AST)
369  : Z3_mk_bvult(Z3Context::ZC, LHS.AST, RHS.AST);
370  break;
371  case BO_GT:
372  AST = isSigned ? Z3_mk_bvsgt(Z3Context::ZC, LHS.AST, RHS.AST)
373  : Z3_mk_bvugt(Z3Context::ZC, LHS.AST, RHS.AST);
374  break;
375  case BO_LE:
376  AST = isSigned ? Z3_mk_bvsle(Z3Context::ZC, LHS.AST, RHS.AST)
377  : Z3_mk_bvule(Z3Context::ZC, LHS.AST, RHS.AST);
378  break;
379  case BO_GE:
380  AST = isSigned ? Z3_mk_bvsge(Z3Context::ZC, LHS.AST, RHS.AST)
381  : Z3_mk_bvuge(Z3Context::ZC, LHS.AST, RHS.AST);
382  break;
383 
384  // Equality operators
385  case BO_EQ:
386  AST = Z3_mk_eq(Z3Context::ZC, LHS.AST, RHS.AST);
387  break;
388  case BO_NE:
389  return Z3Expr::fromUnOp(UO_LNot,
390  Z3Expr::fromBinOp(LHS, BO_EQ, RHS, isSigned));
391  break;
392 
393  // Bitwise operators
394  case BO_And:
395  AST = Z3_mk_bvand(Z3Context::ZC, LHS.AST, RHS.AST);
396  break;
397  case BO_Xor:
398  AST = Z3_mk_bvxor(Z3Context::ZC, LHS.AST, RHS.AST);
399  break;
400  case BO_Or:
401  AST = Z3_mk_bvor(Z3Context::ZC, LHS.AST, RHS.AST);
402  break;
403 
404  // Logical operators
405  case BO_LAnd:
406  case BO_LOr: {
407  std::vector<Z3_ast> Args = {LHS.AST, RHS.AST};
408  return Z3Expr::fromNBinOp(Op, Args);
409  }
410  }
411 
412  return Z3Expr(AST);
413  }
414 
415  /// Construct a Z3Expr from a special floating-point binary operator, given
416  /// a Z3_context.
417  static Z3Expr fromFloatSpecialBinOp(const Z3Expr &LHS,
418  const BinaryOperator::Opcode Op,
419  const llvm::APFloat::fltCategory &RHS) {
420  Z3_ast AST;
421 
422  switch (Op) {
423  default:
424  llvm_unreachable("Unimplemented opcode");
425  break;
426 
427  // Equality operators
428  case BO_EQ:
429  switch (RHS) {
430  case llvm::APFloat::fcInfinity:
431  AST = Z3_mk_fpa_is_infinite(Z3Context::ZC, LHS.AST);
432  break;
433  case llvm::APFloat::fcNaN:
434  AST = Z3_mk_fpa_is_nan(Z3Context::ZC, LHS.AST);
435  break;
436  case llvm::APFloat::fcNormal:
437  AST = Z3_mk_fpa_is_normal(Z3Context::ZC, LHS.AST);
438  break;
439  case llvm::APFloat::fcZero:
440  AST = Z3_mk_fpa_is_zero(Z3Context::ZC, LHS.AST);
441  break;
442  }
443  break;
444  case BO_NE:
445  return Z3Expr::fromFloatUnOp(
446  UO_LNot, Z3Expr::fromFloatSpecialBinOp(LHS, BO_EQ, RHS));
447  break;
448  }
449 
450  return Z3Expr(AST);
451  }
452 
453  /// Construct a Z3Expr from a floating-point binary operator, given a
454  /// Z3_context.
455  static Z3Expr fromFloatBinOp(const Z3Expr &LHS,
456  const BinaryOperator::Opcode Op,
457  const Z3Expr &RHS) {
458  Z3_ast AST;
459 
460  assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
461  "AST's must have the same sort!");
462 
463  switch (Op) {
464  default:
465  llvm_unreachable("Unimplemented opcode");
466  break;
467 
468  // Multiplicative operators
469  case BO_Mul: {
470  Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
471  AST = Z3_mk_fpa_mul(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
472  break;
473  }
474  case BO_Div: {
475  Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
476  AST = Z3_mk_fpa_div(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
477  break;
478  }
479  case BO_Rem:
480  AST = Z3_mk_fpa_rem(Z3Context::ZC, LHS.AST, RHS.AST);
481  break;
482 
483  // Additive operators
484  case BO_Add: {
485  Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
486  AST = Z3_mk_fpa_add(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
487  break;
488  }
489  case BO_Sub: {
490  Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
491  AST = Z3_mk_fpa_sub(Z3Context::ZC, RoundingMode.AST, LHS.AST, RHS.AST);
492  break;
493  }
494 
495  // Relational operators
496  case BO_LT:
497  AST = Z3_mk_fpa_lt(Z3Context::ZC, LHS.AST, RHS.AST);
498  break;
499  case BO_GT:
500  AST = Z3_mk_fpa_gt(Z3Context::ZC, LHS.AST, RHS.AST);
501  break;
502  case BO_LE:
503  AST = Z3_mk_fpa_leq(Z3Context::ZC, LHS.AST, RHS.AST);
504  break;
505  case BO_GE:
506  AST = Z3_mk_fpa_geq(Z3Context::ZC, LHS.AST, RHS.AST);
507  break;
508 
509  // Equality operators
510  case BO_EQ:
511  AST = Z3_mk_fpa_eq(Z3Context::ZC, LHS.AST, RHS.AST);
512  break;
513  case BO_NE:
514  return Z3Expr::fromFloatUnOp(UO_LNot,
515  Z3Expr::fromFloatBinOp(LHS, BO_EQ, RHS));
516  break;
517 
518  // Logical operators
519  case BO_LAnd:
520  case BO_LOr:
521  return Z3Expr::fromBinOp(LHS, Op, RHS, false);
522  }
523 
524  return Z3Expr(AST);
525  }
526 
527  /// Construct a Z3Expr from a SymbolData, given a Z3_context.
528  static Z3Expr fromData(const SymbolID ID, bool isBool, bool isFloat,
529  uint64_t BitWidth) {
530  llvm::Twine Name = "$" + llvm::Twine(ID);
531 
532  Z3Sort Sort;
533  if (isBool)
534  Sort = Z3Sort::getBoolSort();
535  else if (isFloat)
536  Sort = Z3Sort::getFloatSort(BitWidth);
537  else
538  Sort = Z3Sort::getBitvectorSort(BitWidth);
539 
540  Z3_symbol Symbol = Z3_mk_string_symbol(Z3Context::ZC, Name.str().c_str());
541  Z3_ast AST = Z3_mk_const(Z3Context::ZC, Symbol, Sort.Sort);
542  return Z3Expr(AST);
543  }
544 
545  /// Construct a Z3Expr from a SymbolCast, given a Z3_context.
546  static Z3Expr fromCast(const Z3Expr &Exp, QualType ToTy, uint64_t ToBitWidth,
547  QualType FromTy, uint64_t FromBitWidth) {
548  Z3_ast AST;
549 
550  if ((FromTy->isIntegralOrEnumerationType() &&
551  ToTy->isIntegralOrEnumerationType()) ||
552  (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
553  (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
554  (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
555  // Special case: Z3 boolean type is distinct from bitvector type, so
556  // must use if-then-else expression instead of direct cast
557  if (FromTy->isBooleanType()) {
558  assert(ToBitWidth > 0 && "BitWidth must be positive!");
559  Z3Expr Zero = Z3Expr::fromInt("0", ToBitWidth);
560  Z3Expr One = Z3Expr::fromInt("1", ToBitWidth);
561  AST = Z3_mk_ite(Z3Context::ZC, Exp.AST, One.AST, Zero.AST);
562  } else if (ToBitWidth > FromBitWidth) {
563  AST = FromTy->isSignedIntegerOrEnumerationType()
564  ? Z3_mk_sign_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,
565  Exp.AST)
566  : Z3_mk_zero_ext(Z3Context::ZC, ToBitWidth - FromBitWidth,
567  Exp.AST);
568  } else if (ToBitWidth < FromBitWidth) {
569  AST = Z3_mk_extract(Z3Context::ZC, ToBitWidth - 1, 0, Exp.AST);
570  } else {
571  // Both are bitvectors with the same width, ignore the type cast
572  return Exp;
573  }
574  } else if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
575  if (ToBitWidth != FromBitWidth) {
576  Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
577  Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
578  AST = Z3_mk_fpa_to_fp_float(Z3Context::ZC, RoundingMode.AST, Exp.AST,
579  Sort.Sort);
580  } else {
581  return Exp;
582  }
583  } else if (FromTy->isIntegralOrEnumerationType() &&
584  ToTy->isRealFloatingType()) {
585  Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
586  Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
587  AST = FromTy->isSignedIntegerOrEnumerationType()
588  ? Z3_mk_fpa_to_fp_signed(Z3Context::ZC, RoundingMode.AST,
589  Exp.AST, Sort.Sort)
590  : Z3_mk_fpa_to_fp_unsigned(Z3Context::ZC, RoundingMode.AST,
591  Exp.AST, Sort.Sort);
592  } else if (FromTy->isRealFloatingType() &&
593  ToTy->isIntegralOrEnumerationType()) {
594  Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
596  ? Z3_mk_fpa_to_sbv(Z3Context::ZC, RoundingMode.AST, Exp.AST,
597  ToBitWidth)
598  : Z3_mk_fpa_to_ubv(Z3Context::ZC, RoundingMode.AST, Exp.AST,
599  ToBitWidth);
600  } else {
601  llvm_unreachable("Unsupported explicit type cast!");
602  }
603 
604  return Z3Expr(AST);
605  }
606 
607  /// Construct a Z3Expr from a boolean, given a Z3_context.
608  static Z3Expr fromBoolean(const bool Bool) {
609  Z3_ast AST = Bool ? Z3_mk_true(Z3Context::ZC) : Z3_mk_false(Z3Context::ZC);
610  return Z3Expr(AST);
611  }
612 
613  /// Construct a Z3Expr from a finite APFloat, given a Z3_context.
614  static Z3Expr fromAPFloat(const llvm::APFloat &Float) {
615  Z3_ast AST;
616  Z3Sort Sort = Z3Sort::getFloatSort(
617  llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
618 
619  llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true);
620  Z3Expr Z3Int = Z3Expr::fromAPSInt(Int);
621  AST = Z3_mk_fpa_to_fp_bv(Z3Context::ZC, Z3Int.AST, Sort.Sort);
622 
623  return Z3Expr(AST);
624  }
625 
626  /// Construct a Z3Expr from an APSInt, given a Z3_context.
627  static Z3Expr fromAPSInt(const llvm::APSInt &Int) {
628  Z3Sort Sort = Z3Sort::getBitvectorSort(Int.getBitWidth());
629  Z3_ast AST =
630  Z3_mk_numeral(Z3Context::ZC, Int.toString(10).c_str(), Sort.Sort);
631  return Z3Expr(AST);
632  }
633 
634  /// Construct a Z3Expr from an integer, given a Z3_context.
635  static Z3Expr fromInt(const char *Int, uint64_t BitWidth) {
636  Z3Sort Sort = Z3Sort::getBitvectorSort(BitWidth);
637  Z3_ast AST = Z3_mk_numeral(Z3Context::ZC, Int, Sort.Sort);
638  return Z3Expr(AST);
639  }
640 
641  /// Construct an APFloat from a Z3Expr, given the AST representation
642  static bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST,
643  llvm::APFloat &Float, bool useSemantics = true) {
644  assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT &&
645  "Unsupported sort to floating-point!");
646 
647  llvm::APSInt Int(Sort.getFloatSortSize(), true);
648  const llvm::fltSemantics &Semantics =
649  Z3Expr::getFloatSemantics(Sort.getFloatSortSize());
650  Z3Sort BVSort = Z3Sort::getBitvectorSort(Sort.getFloatSortSize());
651  if (!Z3Expr::toAPSInt(BVSort, AST, Int, true)) {
652  return false;
653  }
654 
655  if (useSemantics &&
656  !Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) {
657  assert(false && "Floating-point types don't match!");
658  return false;
659  }
660 
661  Float = llvm::APFloat(Semantics, Int);
662  return true;
663  }
664 
665  /// Construct an APSInt from a Z3Expr, given the AST representation
666  static bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST, llvm::APSInt &Int,
667  bool useSemantics = true) {
668  switch (Sort.getSortKind()) {
669  default:
670  llvm_unreachable("Unsupported sort to integer!");
671  case Z3_BV_SORT: {
672  if (useSemantics && Int.getBitWidth() != Sort.getBitvectorSortSize()) {
673  assert(false && "Bitvector types don't match!");
674  return false;
675  }
676 
677  uint64_t Value[2];
678  // Force cast because Z3 defines __uint64 to be a unsigned long long
679  // type, which isn't compatible with a unsigned long type, even if they
680  // are the same size.
681  Z3_get_numeral_uint64(Z3Context::ZC, AST,
682  reinterpret_cast<__uint64 *>(&Value[0]));
683  if (Sort.getBitvectorSortSize() <= 64) {
684  Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]),
685  Int.isUnsigned());
686  } else if (Sort.getBitvectorSortSize() == 128) {
687  Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST));
688  Z3_get_numeral_uint64(Z3Context::ZC, AST,
689  reinterpret_cast<__uint64 *>(&Value[1]));
690  Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value),
691  Int.isUnsigned());
692  } else {
693  assert(false && "Bitwidth not supported!");
694  return false;
695  }
696  return true;
697  }
698  case Z3_BOOL_SORT:
699  if (useSemantics && Int.getBitWidth() < 1) {
700  assert(false && "Boolean type doesn't match!");
701  return false;
702  }
703  Int = llvm::APSInt(
704  llvm::APInt(Int.getBitWidth(),
705  Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1
706  : 0),
707  Int.isUnsigned());
708  return true;
709  }
710  }
711 
712  void Profile(llvm::FoldingSetNodeID &ID) const {
713  ID.AddInteger(Z3_get_ast_hash(Z3Context::ZC, AST));
714  }
715 
716  bool operator<(const Z3Expr &Other) const {
717  llvm::FoldingSetNodeID ID1, ID2;
718  Profile(ID1);
719  Other.Profile(ID2);
720  return ID1 < ID2;
721  }
722 
723  /// Comparison of AST equality, not model equivalence.
724  bool operator==(const Z3Expr &Other) const {
725  assert(Z3_is_eq_sort(Z3Context::ZC, Z3_get_sort(Z3Context::ZC, AST),
726  Z3_get_sort(Z3Context::ZC, Other.AST)) &&
727  "AST's must have the same sort");
728  return Z3_is_eq_ast(Z3Context::ZC, AST, Other.AST);
729  }
730 
731  /// Override implicit move constructor for correct reference counting.
732  Z3Expr &operator=(const Z3Expr &Move) {
733  Z3_inc_ref(Z3Context::ZC, Move.AST);
734  Z3_dec_ref(Z3Context::ZC, AST);
735  AST = Move.AST;
736  return *this;
737  }
738 
739  void print(raw_ostream &OS) const {
740  OS << Z3_ast_to_string(Z3Context::ZC, AST);
741  }
742 
743  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
744 }; // end class Z3Expr
745 
746 class Z3Model {
747  Z3_model Model;
748 
749 public:
750  Z3Model(Z3_model ZM) : Model(ZM) { Z3_model_inc_ref(Z3Context::ZC, Model); }
751 
752  /// Override implicit copy constructor for correct reference counting.
753  Z3Model(const Z3Model &Copy) : Model(Copy.Model) {
754  Z3_model_inc_ref(Z3Context::ZC, Model);
755  }
756 
757  /// Provide move constructor
758  Z3Model(Z3Model &&Move) : Model(nullptr) { *this = std::move(Move); }
759 
760  /// Provide move assignment constructor
761  Z3Model &operator=(Z3Model &&Move) {
762  if (this != &Move) {
763  if (Model)
764  Z3_model_dec_ref(Z3Context::ZC, Model);
765  Model = Move.Model;
766  Move.Model = nullptr;
767  }
768  return *this;
769  }
770 
771  ~Z3Model() {
772  if (Model)
773  Z3_model_dec_ref(Z3Context::ZC, Model);
774  }
775 
776  /// Given an expression, extract the value of this operand in the model.
777  bool getInterpretation(const Z3Expr &Exp, llvm::APSInt &Int) const {
778  Z3_func_decl Func =
779  Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
780  if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
781  return false;
782 
783  Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
784  Z3Sort Sort = Z3Sort::getSort(Assign);
785  return Z3Expr::toAPSInt(Sort, Assign, Int, true);
786  }
787 
788  /// Given an expression, extract the value of this operand in the model.
789  bool getInterpretation(const Z3Expr &Exp, llvm::APFloat &Float) const {
790  Z3_func_decl Func =
791  Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
792  if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
793  return false;
794 
795  Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
796  Z3Sort Sort = Z3Sort::getSort(Assign);
797  return Z3Expr::toAPFloat(Sort, Assign, Float, true);
798  }
799 
800  void print(raw_ostream &OS) const {
801  OS << Z3_model_to_string(Z3Context::ZC, Model);
802  }
803 
804  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
805 }; // end class Z3Model
806 
807 class Z3Solver {
808  friend class Z3ConstraintManager;
809 
810  Z3_solver Solver;
811 
812  Z3Solver(Z3_solver ZS) : Solver(ZS) {
813  Z3_solver_inc_ref(Z3Context::ZC, Solver);
814  }
815 
816 public:
817  /// Override implicit copy constructor for correct reference counting.
818  Z3Solver(const Z3Solver &Copy) : Solver(Copy.Solver) {
819  Z3_solver_inc_ref(Z3Context::ZC, Solver);
820  }
821 
822  /// Provide move constructor
823  Z3Solver(Z3Solver &&Move) : Solver(nullptr) { *this = std::move(Move); }
824 
825  /// Provide move assignment constructor
826  Z3Solver &operator=(Z3Solver &&Move) {
827  if (this != &Move) {
828  if (Solver)
829  Z3_solver_dec_ref(Z3Context::ZC, Solver);
830  Solver = Move.Solver;
831  Move.Solver = nullptr;
832  }
833  return *this;
834  }
835 
836  ~Z3Solver() {
837  if (Solver)
838  Z3_solver_dec_ref(Z3Context::ZC, Solver);
839  }
840 
841  /// Given a constraint, add it to the solver
842  void addConstraint(const Z3Expr &Exp) {
843  Z3_solver_assert(Z3Context::ZC, Solver, Exp.AST);
844  }
845 
846  /// Given a program state, construct the logical conjunction and add it to
847  /// the solver
848  void addStateConstraints(ProgramStateRef State) {
849  // TODO: Don't add all the constraints, only the relevant ones
850  ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
851  ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
852 
853  // Construct the logical AND of all the constraints
854  if (I != IE) {
855  std::vector<Z3_ast> ASTs;
856 
857  while (I != IE)
858  ASTs.push_back(I++->second.AST);
859 
860  Z3Expr Conj = Z3Expr::fromNBinOp(BO_LAnd, ASTs);
861  addConstraint(Conj);
862  }
863  }
864 
865  /// Check if the constraints are satisfiable
866  Z3_lbool check() { return Z3_solver_check(Z3Context::ZC, Solver); }
867 
868  /// Push the current solver state
869  void push() { return Z3_solver_push(Z3Context::ZC, Solver); }
870 
871  /// Pop the previous solver state
872  void pop(unsigned NumStates = 1) {
873  assert(Z3_solver_get_num_scopes(Z3Context::ZC, Solver) >= NumStates);
874  return Z3_solver_pop(Z3Context::ZC, Solver, NumStates);
875  }
876 
877  /// Get a model from the solver. Caller should check the model is
878  /// satisfiable.
879  Z3Model getModel() {
880  return Z3Model(Z3_solver_get_model(Z3Context::ZC, Solver));
881  }
882 
883  /// Reset the solver and remove all constraints.
884  void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
885 
886  void print(raw_ostream &OS) const {
887  OS << Z3_solver_to_string(Z3Context::ZC, Solver);
888  }
889 
890  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
891 }; // end class Z3Solver
892 
893 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
894  llvm::report_fatal_error("Z3 error: " +
895  llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
896 }
897 
898 class Z3ConstraintManager : public SMTConstraintManager {
899  Z3Context Context;
900  mutable Z3Solver Solver;
901 
902 public:
903  Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
904  : SMTConstraintManager(SE, SB),
905  Solver(Z3_mk_simple_solver(Z3Context::ZC)) {
906  Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler);
907  }
908  //===------------------------------------------------------------------===//
909  // Implementation for Refutation.
910  //===------------------------------------------------------------------===//
911 
912  void addRangeConstraints(clang::ento::ConstraintRangeTy CR) override;
913 
914  ConditionTruthVal isModelFeasible() override;
915 
916  LLVM_DUMP_METHOD void dump() const override;
917 
918  //===------------------------------------------------------------------===//
919  // Implementation for interface from ConstraintManager.
920  //===------------------------------------------------------------------===//
921 
922  bool canReasonAbout(SVal X) const override;
923 
924  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
925 
926  const llvm::APSInt *getSymVal(ProgramStateRef State,
927  SymbolRef Sym) const override;
928 
929  ProgramStateRef removeDeadBindings(ProgramStateRef St,
930  SymbolReaper &SymReaper) override;
931 
932  void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
933  const char *sep) override;
934 
935  //===------------------------------------------------------------------===//
936  // Implementation for interface from SimpleConstraintManager.
937  //===------------------------------------------------------------------===//
938 
940  bool Assumption) override;
941 
942  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
943  const llvm::APSInt &From,
944  const llvm::APSInt &To,
945  bool InRange) override;
946 
947  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
948  bool Assumption) override;
949 
950 private:
951  //===------------------------------------------------------------------===//
952  // Internal implementation.
953  //===------------------------------------------------------------------===//
954 
955  // Check whether a new model is satisfiable, and update the program state.
956  ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym,
957  const Z3Expr &Exp);
958 
959  // Generate and check a Z3 model, using the given constraint.
960  Z3_lbool checkZ3Model(ProgramStateRef State, const Z3Expr &Exp) const;
961 
962  // Generate a Z3Expr that represents the given symbolic expression.
963  // Sets the hasComparison parameter if the expression has a comparison
964  // operator.
965  // Sets the RetTy parameter to the final return type after promotions and
966  // casts.
967  Z3Expr getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,
968  bool *hasComparison = nullptr) const;
969 
970  // Generate a Z3Expr that takes the logical not of an expression.
971  Z3Expr getZ3NotExpr(const Z3Expr &Exp) const;
972 
973  // Generate a Z3Expr that compares the expression to zero.
974  Z3Expr getZ3ZeroExpr(const Z3Expr &Exp, QualType RetTy,
975  bool Assumption) const;
976 
977  // Recursive implementation to unpack and generate symbolic expression.
978  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
979  Z3Expr getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
980  bool *hasComparison) const;
981 
982  // Wrapper to generate Z3Expr from SymbolData.
983  Z3Expr getZ3DataExpr(const SymbolID ID, QualType Ty) const;
984 
985  // Wrapper to generate Z3Expr from SymbolCast.
986  Z3Expr getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, QualType Ty) const;
987 
988  // Wrapper to generate Z3Expr from BinarySymExpr.
989  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
990  Z3Expr getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
991  QualType *RetTy) const;
992 
993  // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
994  // Sets the RetTy parameter. See getZ3Expr().
995  Z3Expr getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
996  BinaryOperator::Opcode Op, const Z3Expr &RHS,
997  QualType RTy, QualType *RetTy) const;
998 
999  // Wrapper to generate Z3Expr from a range. If From == To, an equality will
1000  // be created instead.
1001  Z3Expr getZ3RangeExpr(SymbolRef Sym, const llvm::APSInt &From,
1002  const llvm::APSInt &To, bool InRange);
1003 
1004  //===------------------------------------------------------------------===//
1005  // Helper functions.
1006  //===------------------------------------------------------------------===//
1007 
1008  // Recover the QualType of an APSInt.
1009  // TODO: Refactor to put elsewhere
1010  QualType getAPSIntType(const llvm::APSInt &Int) const;
1011 
1012  // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
1013  std::pair<llvm::APSInt, QualType> fixAPSInt(const llvm::APSInt &Int) const;
1014 
1015  // Perform implicit type conversion on binary symbolic expressions.
1016  // May modify all input parameters.
1017  // TODO: Refactor to use built-in conversion functions
1018  void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType &LTy,
1019  QualType &RTy) const;
1020 
1021  // Perform implicit integer type conversion.
1022  // May modify all input parameters.
1023  // TODO: Refactor to use Sema::handleIntegerConversion()
1024  template <typename T,
1025  T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1026  void doIntTypeConversion(T &LHS, QualType &LTy, T &RHS, QualType &RTy) const;
1027 
1028  // Perform implicit floating-point type conversion.
1029  // May modify all input parameters.
1030  // TODO: Refactor to use Sema::handleFloatConversion()
1031  template <typename T,
1032  T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1033  void doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
1034  QualType &RTy) const;
1035 
1036  // Callback function for doCast parameter on APSInt type.
1037  static llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy,
1038  uint64_t ToWidth, QualType FromTy,
1039  uint64_t FromWidth);
1040 }; // end class Z3ConstraintManager
1041 
1042 Z3_context Z3Context::ZC;
1043 
1044 } // end anonymous namespace
1045 
1046 ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State,
1047  SymbolRef Sym, bool Assumption) {
1048  QualType RetTy;
1049  bool hasComparison;
1050 
1051  Z3Expr Exp = getZ3Expr(Sym, &RetTy, &hasComparison);
1052  // Create zero comparison for implicit boolean cast, with reversed assumption
1053  if (!hasComparison && !RetTy->isBooleanType())
1054  return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption));
1055 
1056  return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));
1057 }
1058 
1059 ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
1060  ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
1061  const llvm::APSInt &To, bool InRange) {
1062  return assumeZ3Expr(State, Sym, getZ3RangeExpr(Sym, From, To, InRange));
1063 }
1064 
1065 ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
1066  SymbolRef Sym,
1067  bool Assumption) {
1068  // Skip anything that is unsupported
1069  return State;
1070 }
1071 
1072 bool Z3ConstraintManager::canReasonAbout(SVal X) const {
1073  const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
1074 
1076  if (!SymVal)
1077  return true;
1078 
1079  const SymExpr *Sym = SymVal->getSymbol();
1080  QualType Ty = Sym->getType();
1081 
1082  // Complex types are not modeled
1083  if (Ty->isComplexType() || Ty->isComplexIntegerType())
1084  return false;
1085 
1086  // Non-IEEE 754 floating-point types are not modeled
1087  if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
1088  (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
1089  &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
1090  return false;
1091 
1092  if (isa<SymbolData>(Sym))
1093  return true;
1094 
1095  SValBuilder &SVB = getSValBuilder();
1096 
1097  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
1098  return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
1099 
1100  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1101  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
1102  return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
1103 
1104  if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
1105  return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
1106 
1107  if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
1108  return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
1109  canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
1110  }
1111 
1112  llvm_unreachable("Unsupported expression to reason about!");
1113 }
1114 
1115 ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State,
1116  SymbolRef Sym) {
1117  QualType RetTy;
1118  // The expression may be casted, so we cannot call getZ3DataExpr() directly
1119  Z3Expr VarExp = getZ3Expr(Sym, &RetTy);
1120  Z3Expr Exp = getZ3ZeroExpr(VarExp, RetTy, true);
1121  // Negate the constraint
1122  Z3Expr NotExp = getZ3ZeroExpr(VarExp, RetTy, false);
1123 
1124  Solver.reset();
1125  Solver.addStateConstraints(State);
1126 
1127  Solver.push();
1128  Solver.addConstraint(Exp);
1129  Z3_lbool isSat = Solver.check();
1130 
1131  Solver.pop();
1132  Solver.addConstraint(NotExp);
1133  Z3_lbool isNotSat = Solver.check();
1134 
1135  // Zero is the only possible solution
1136  if (isSat == Z3_L_TRUE && isNotSat == Z3_L_FALSE)
1137  return true;
1138  // Zero is not a solution
1139  else if (isSat == Z3_L_FALSE && isNotSat == Z3_L_TRUE)
1140  return false;
1141 
1142  // Zero may be a solution
1143  return ConditionTruthVal();
1144 }
1145 
1146 const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
1147  SymbolRef Sym) const {
1148  BasicValueFactory &BVF = getBasicVals();
1149  ASTContext &Ctx = BVF.getContext();
1150 
1151  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
1152  QualType Ty = Sym->getType();
1153  assert(!Ty->isRealFloatingType());
1154  llvm::APSInt Value(Ctx.getTypeSize(Ty),
1156 
1157  Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
1158 
1159  Solver.reset();
1160  Solver.addStateConstraints(State);
1161 
1162  // Constraints are unsatisfiable
1163  if (Solver.check() != Z3_L_TRUE)
1164  return nullptr;
1165 
1166  Z3Model Model = Solver.getModel();
1167  // Model does not assign interpretation
1168  if (!Model.getInterpretation(Exp, Value))
1169  return nullptr;
1170 
1171  // A value has been obtained, check if it is the only value
1172  Z3Expr NotExp = Z3Expr::fromBinOp(
1173  Exp, BO_NE,
1174  Ty->isBooleanType() ? Z3Expr::fromBoolean(Value.getBoolValue())
1175  : Z3Expr::fromAPSInt(Value),
1176  false);
1177 
1178  Solver.addConstraint(NotExp);
1179  if (Solver.check() == Z3_L_TRUE)
1180  return nullptr;
1181 
1182  // This is the only solution, store it
1183  return &BVF.getValue(Value);
1184  } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
1185  SymbolRef CastSym = SC->getOperand();
1186  QualType CastTy = SC->getType();
1187  // Skip the void type
1188  if (CastTy->isVoidType())
1189  return nullptr;
1190 
1191  const llvm::APSInt *Value;
1192  if (!(Value = getSymVal(State, CastSym)))
1193  return nullptr;
1194  return &BVF.Convert(SC->getType(), *Value);
1195  } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1196  const llvm::APSInt *LHS, *RHS;
1197  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
1198  LHS = getSymVal(State, SIE->getLHS());
1199  RHS = &SIE->getRHS();
1200  } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
1201  LHS = &ISE->getLHS();
1202  RHS = getSymVal(State, ISE->getRHS());
1203  } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
1204  // Early termination to avoid expensive call
1205  LHS = getSymVal(State, SSM->getLHS());
1206  RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
1207  } else {
1208  llvm_unreachable("Unsupported binary expression to get symbol value!");
1209  }
1210 
1211  if (!LHS || !RHS)
1212  return nullptr;
1213 
1214  llvm::APSInt ConvertedLHS, ConvertedRHS;
1215  QualType LTy, RTy;
1216  std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS);
1217  std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS);
1218  doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
1219  ConvertedLHS, LTy, ConvertedRHS, RTy);
1220  return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
1221  }
1222 
1223  llvm_unreachable("Unsupported expression to get symbol value!");
1224 }
1225 
1227 Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
1228  SymbolReaper &SymReaper) {
1229  ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
1230  ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
1231 
1232  for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
1233  if (SymReaper.maybeDead(I->first))
1234  CZ = CZFactory.remove(CZ, *I);
1235  }
1236 
1237  return State->set<ConstraintZ3>(CZ);
1238 }
1239 
1240 void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
1241  for (const auto &I : CR) {
1242  SymbolRef Sym = I.first;
1243 
1244  Z3Expr Constraints = Z3Expr::fromBoolean(false);
1245  for (const auto &Range : I.second) {
1246  Z3Expr SymRange =
1247  getZ3RangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true);
1248 
1249  // FIXME: the last argument (isSigned) is not used when generating the
1250  // or expression, as both arguments are booleans
1251  Constraints =
1252  Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, /*IsSigned=*/true);
1253  }
1254  Solver.addConstraint(Constraints);
1255  }
1256 }
1257 
1258 clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() {
1259  if (Solver.check() == Z3_L_FALSE)
1260  return false;
1261 
1262  return ConditionTruthVal();
1263 }
1264 
1265 LLVM_DUMP_METHOD void Z3ConstraintManager::dump() const
1266 {
1267  Solver.dump();
1268 }
1269 
1270 //===------------------------------------------------------------------===//
1271 // Internal implementation.
1272 //===------------------------------------------------------------------===//
1273 
1274 ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State,
1275  SymbolRef Sym,
1276  const Z3Expr &Exp) {
1277  // Check the model, avoid simplifying AST to save time
1278  if (checkZ3Model(State, Exp) == Z3_L_TRUE)
1279  return State->add<ConstraintZ3>(std::make_pair(Sym, Exp));
1280 
1281  return nullptr;
1282 }
1283 
1284 Z3_lbool Z3ConstraintManager::checkZ3Model(ProgramStateRef State,
1285  const Z3Expr &Exp) const {
1286  Solver.reset();
1287  Solver.addConstraint(Exp);
1288  Solver.addStateConstraints(State);
1289  return Solver.check();
1290 }
1291 
1292 Z3Expr Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy,
1293  bool *hasComparison) const {
1294  if (hasComparison) {
1295  *hasComparison = false;
1296  }
1297 
1298  return getZ3SymExpr(Sym, RetTy, hasComparison);
1299 }
1300 
1301 Z3Expr Z3ConstraintManager::getZ3NotExpr(const Z3Expr &Exp) const {
1302  return Z3Expr::fromUnOp(UO_LNot, Exp);
1303 }
1304 
1305 Z3Expr Z3ConstraintManager::getZ3ZeroExpr(const Z3Expr &Exp, QualType Ty,
1306  bool Assumption) const {
1307  ASTContext &Ctx = getBasicVals().getContext();
1308  if (Ty->isRealFloatingType()) {
1309  llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
1310  return Z3Expr::fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
1311  Z3Expr::fromAPFloat(Zero));
1312  } else if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
1313  Ty->isBlockPointerType() || Ty->isReferenceType()) {
1314  bool isSigned = Ty->isSignedIntegerOrEnumerationType();
1315  // Skip explicit comparison for boolean types
1316  if (Ty->isBooleanType())
1317  return Assumption ? getZ3NotExpr(Exp) : Exp;
1318  return Z3Expr::fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
1319  Z3Expr::fromInt("0", Ctx.getTypeSize(Ty)),
1320  isSigned);
1321  }
1322 
1323  llvm_unreachable("Unsupported type for zero value!");
1324 }
1325 
1326 Z3Expr Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
1327  bool *hasComparison) const {
1328  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
1329  if (RetTy)
1330  *RetTy = Sym->getType();
1331 
1332  return getZ3DataExpr(SD->getSymbolID(), Sym->getType());
1333  } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
1334  if (RetTy)
1335  *RetTy = Sym->getType();
1336 
1337  QualType FromTy;
1338  Z3Expr Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison);
1339  // Casting an expression with a comparison invalidates it. Note that this
1340  // must occur after the recursive call above.
1341  // e.g. (signed char) (x > 0)
1342  if (hasComparison)
1343  *hasComparison = false;
1344  return getZ3CastExpr(Exp, FromTy, Sym->getType());
1345  } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1346  Z3Expr Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy);
1347  // Set the hasComparison parameter, in post-order traversal order.
1348  if (hasComparison)
1349  *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
1350  return Exp;
1351  }
1352 
1353  llvm_unreachable("Unsupported SymbolRef type!");
1354 }
1355 
1356 Z3Expr Z3ConstraintManager::getZ3DataExpr(const SymbolID ID,
1357  QualType Ty) const {
1358  ASTContext &Ctx = getBasicVals().getContext();
1359  return Z3Expr::fromData(ID, Ty->isBooleanType(), Ty->isRealFloatingType(),
1360  Ctx.getTypeSize(Ty));
1361 }
1362 
1363 Z3Expr Z3ConstraintManager::getZ3CastExpr(const Z3Expr &Exp, QualType FromTy,
1364  QualType ToTy) const {
1365  ASTContext &Ctx = getBasicVals().getContext();
1366  return Z3Expr::fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
1367  Ctx.getTypeSize(FromTy));
1368 }
1369 
1370 Z3Expr Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
1371  bool *hasComparison,
1372  QualType *RetTy) const {
1373  QualType LTy, RTy;
1374  BinaryOperator::Opcode Op = BSE->getOpcode();
1375 
1376  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
1377  Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), &LTy, hasComparison);
1378  llvm::APSInt NewRInt;
1379  std::tie(NewRInt, RTy) = fixAPSInt(SIE->getRHS());
1380  Z3Expr RHS = Z3Expr::fromAPSInt(NewRInt);
1381  return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1382  } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
1383  llvm::APSInt NewLInt;
1384  std::tie(NewLInt, LTy) = fixAPSInt(ISE->getLHS());
1385  Z3Expr LHS = Z3Expr::fromAPSInt(NewLInt);
1386  Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
1387  return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1388  } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
1389  Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), &LTy, hasComparison);
1390  Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
1391  return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1392  } else {
1393  llvm_unreachable("Unsupported BinarySymExpr type!");
1394  }
1395 }
1396 
1397 Z3Expr Z3ConstraintManager::getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
1399  const Z3Expr &RHS, QualType RTy,
1400  QualType *RetTy) const {
1401  Z3Expr NewLHS = LHS;
1402  Z3Expr NewRHS = RHS;
1403  doTypeConversion(NewLHS, NewRHS, LTy, RTy);
1404  // Update the return type parameter if the output type has changed.
1405  if (RetTy) {
1406  // A boolean result can be represented as an integer type in C/C++, but at
1407  // this point we only care about the Z3 type. Set it as a boolean type to
1408  // avoid subsequent Z3 errors.
1410  ASTContext &Ctx = getBasicVals().getContext();
1411  *RetTy = Ctx.BoolTy;
1412  } else {
1413  *RetTy = LTy;
1414  }
1415 
1416  // If the two operands are pointers and the operation is a subtraction, the
1417  // result is of type ptrdiff_t, which is signed
1418  if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) {
1419  *RetTy = getBasicVals().getContext().getPointerDiffType();
1420  }
1421  }
1422 
1423  return LTy->isRealFloatingType()
1424  ? Z3Expr::fromFloatBinOp(NewLHS, Op, NewRHS)
1425  : Z3Expr::fromBinOp(NewLHS, Op, NewRHS,
1426  LTy->isSignedIntegerOrEnumerationType());
1427 }
1428 
1429 Z3Expr Z3ConstraintManager::getZ3RangeExpr(SymbolRef Sym,
1430  const llvm::APSInt &From,
1431  const llvm::APSInt &To,
1432  bool InRange) {
1433  // Convert lower bound
1434  QualType FromTy;
1435  llvm::APSInt NewFromInt;
1436  std::tie(NewFromInt, FromTy) = fixAPSInt(From);
1437  Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt);
1438 
1439  // Convert symbol
1440  QualType SymTy;
1441  Z3Expr Exp = getZ3Expr(Sym, &SymTy);
1442 
1443  // Construct single (in)equality
1444  if (From == To)
1445  return getZ3BinExpr(Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp, FromTy,
1446  /*RetTy=*/nullptr);
1447 
1448  QualType ToTy;
1449  llvm::APSInt NewToInt;
1450  std::tie(NewToInt, ToTy) = fixAPSInt(To);
1451  Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt);
1452  assert(FromTy == ToTy && "Range values have different types!");
1453 
1454  // Construct two (in)equalities, and a logical and/or
1455  Z3Expr LHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
1456  FromTy, /*RetTy=*/nullptr);
1457  Z3Expr RHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
1458  /*RetTy=*/nullptr);
1459 
1460  return Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
1462 }
1463 
1464 //===------------------------------------------------------------------===//
1465 // Helper functions.
1466 //===------------------------------------------------------------------===//
1467 
1468 QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
1469  ASTContext &Ctx = getBasicVals().getContext();
1470  return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
1471 }
1472 
1473 std::pair<llvm::APSInt, QualType>
1474 Z3ConstraintManager::fixAPSInt(const llvm::APSInt &Int) const {
1475  llvm::APSInt NewInt;
1476 
1477  // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
1478  // but the former is not available in Clang. Instead, extend the APSInt
1479  // directly.
1480  if (Int.getBitWidth() == 1 && getAPSIntType(Int).isNull()) {
1481  ASTContext &Ctx = getBasicVals().getContext();
1482  NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
1483  } else
1484  NewInt = Int;
1485 
1486  return std::make_pair(NewInt, getAPSIntType(NewInt));
1487 }
1488 
1489 void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
1490  QualType &LTy, QualType &RTy) const {
1491  ASTContext &Ctx = getBasicVals().getContext();
1492 
1493  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
1494  // Perform type conversion
1495  if (LTy->isIntegralOrEnumerationType() &&
1496  RTy->isIntegralOrEnumerationType()) {
1497  if (LTy->isArithmeticType() && RTy->isArithmeticType())
1498  return doIntTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
1499  } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
1500  return doFloatTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
1501  } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
1502  (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
1503  (LTy->isReferenceType() || RTy->isReferenceType())) {
1504  // TODO: Refactor to Sema::FindCompositePointerType(), and
1505  // Sema::CheckCompareOperands().
1506 
1507  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1508  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1509 
1510  // Cast the non-pointer type to the pointer type.
1511  // TODO: Be more strict about this.
1512  if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
1513  (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
1514  (LTy->isReferenceType() ^ RTy->isReferenceType())) {
1515  if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
1516  LTy->isReferenceType()) {
1517  LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
1518  LTy = RTy;
1519  } else {
1520  RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
1521  RTy = LTy;
1522  }
1523  }
1524 
1525  // Cast the void pointer type to the non-void pointer type.
1526  // For void types, this assumes that the casted value is equal to the value
1527  // of the original pointer, and does not account for alignment requirements.
1528  if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
1529  assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
1530  "Pointer types have different bitwidths!");
1531  if (RTy->isVoidPointerType())
1532  RTy = LTy;
1533  else
1534  LTy = RTy;
1535  }
1536 
1537  if (LTy == RTy)
1538  return;
1539  }
1540 
1541  // Fallback: for the solver, assume that these types don't really matter
1542  if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
1543  (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
1544  LTy = RTy;
1545  return;
1546  }
1547 
1548  // TODO: Refine behavior for invalid type casts
1549 }
1550 
1551 template <typename T,
1552  T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1553 void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType &LTy, T &RHS,
1554  QualType &RTy) const {
1555  ASTContext &Ctx = getBasicVals().getContext();
1556  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1557  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1558 
1559  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
1560  // Always perform integer promotion before checking type equality.
1561  // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
1562  if (LTy->isPromotableIntegerType()) {
1563  QualType NewTy = Ctx.getPromotedIntegerType(LTy);
1564  uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
1565  LHS = (*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);
1566  LTy = NewTy;
1567  LBitWidth = NewBitWidth;
1568  }
1569  if (RTy->isPromotableIntegerType()) {
1570  QualType NewTy = Ctx.getPromotedIntegerType(RTy);
1571  uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
1572  RHS = (*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth);
1573  RTy = NewTy;
1574  RBitWidth = NewBitWidth;
1575  }
1576 
1577  if (LTy == RTy)
1578  return;
1579 
1580  // Perform integer type conversion
1581  // Note: Safe to skip updating bitwidth because this must terminate
1582  bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
1583  bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
1584 
1585  int order = Ctx.getIntegerTypeOrder(LTy, RTy);
1586  if (isLSignedTy == isRSignedTy) {
1587  // Same signedness; use the higher-ranked type
1588  if (order == 1) {
1589  RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1590  RTy = LTy;
1591  } else {
1592  LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1593  LTy = RTy;
1594  }
1595  } else if (order != (isLSignedTy ? 1 : -1)) {
1596  // The unsigned type has greater than or equal rank to the
1597  // signed type, so use the unsigned type
1598  if (isRSignedTy) {
1599  RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1600  RTy = LTy;
1601  } else {
1602  LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1603  LTy = RTy;
1604  }
1605  } else if (LBitWidth != RBitWidth) {
1606  // The two types are different widths; if we are here, that
1607  // means the signed type is larger than the unsigned type, so
1608  // use the signed type.
1609  if (isLSignedTy) {
1610  RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1611  RTy = LTy;
1612  } else {
1613  LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1614  LTy = RTy;
1615  }
1616  } else {
1617  // The signed type is higher-ranked than the unsigned type,
1618  // but isn't actually any bigger (like unsigned int and long
1619  // on most 32-bit systems). Use the unsigned type corresponding
1620  // to the signed type.
1621  QualType NewTy = Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
1622  RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1623  RTy = NewTy;
1624  LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1625  LTy = NewTy;
1626  }
1627 }
1628 
1629 template <typename T,
1630  T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1631 void Z3ConstraintManager::doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
1632  QualType &RTy) const {
1633  ASTContext &Ctx = getBasicVals().getContext();
1634 
1635  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1636  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1637 
1638  // Perform float-point type promotion
1639  if (!LTy->isRealFloatingType()) {
1640  LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1641  LTy = RTy;
1642  LBitWidth = RBitWidth;
1643  }
1644  if (!RTy->isRealFloatingType()) {
1645  RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1646  RTy = LTy;
1647  RBitWidth = LBitWidth;
1648  }
1649 
1650  if (LTy == RTy)
1651  return;
1652 
1653  // If we have two real floating types, convert the smaller operand to the
1654  // bigger result
1655  // Note: Safe to skip updating bitwidth because this must terminate
1656  int order = Ctx.getFloatingTypeOrder(LTy, RTy);
1657  if (order > 0) {
1658  RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
1659  RTy = LTy;
1660  } else if (order == 0) {
1661  LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
1662  LTy = RTy;
1663  } else {
1664  llvm_unreachable("Unsupported floating-point type cast!");
1665  }
1666 }
1667 
1668 llvm::APSInt Z3ConstraintManager::castAPSInt(const llvm::APSInt &V,
1669  QualType ToTy, uint64_t ToWidth,
1670  QualType FromTy,
1671  uint64_t FromWidth) {
1672  APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
1673  return TargetType.convert(V);
1674 }
1675 
1676 //==------------------------------------------------------------------------==/
1677 // Pretty-printing.
1678 //==------------------------------------------------------------------------==/
1679 
1680 void Z3ConstraintManager::print(ProgramStateRef St, raw_ostream &OS,
1681  const char *nl, const char *sep) {
1682 
1683  ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
1684 
1685  OS << nl << sep << "Constraints:";
1686  for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
1687  OS << nl << ' ' << I->first << " : ";
1688  I->second.print(OS);
1689  }
1690  OS << nl;
1691 }
1692 
1693 #endif
1694 
1695 std::unique_ptr<ConstraintManager>
1697 #if CLANG_ANALYZER_WITH_Z3
1698  return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
1699 #else
1700  llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
1701  "with -DCLANG_ANALYZER_BUILD_Z3=ON",
1702  false);
1703  return nullptr;
1704 #endif
1705 }
const llvm::APSInt & From() const
A (possibly-)qualified type.
Definition: Type.h:655
int getIntegerTypeOrder(QualType LHS, QualType RHS) const
Return the highest ranked integer type, see C99 6.3.1.8p1.
bool isBlockPointerType() const
Definition: Type.h:6114
bool operator==(CanQual< T > x, CanQual< U > y)
bool isArithmeticType() const
Definition: Type.cpp:1946
bool maybeDead(SymbolRef sym)
If a symbol is known to be live, marks the symbol as live.
bool isRealFloatingType() const
Floating point categories.
Definition: Type.cpp:1931
bool isLogicalOp() const
Definition: Expr.h:3190
QualType getCorrespondingUnsignedType(QualType T) const
A Range represents the closed range [from, to].
llvm::ImmutableMap< SymbolRef, RangeSet > ConstraintRangeTy
Symbolic value.
Definition: SymExpr.h:30
SVal makeSymbolVal(SymbolRef Sym)
Make an SVal that represents the given symbol.
Definition: SValBuilder.h:373
Holds long-lived AST nodes (such as types and decls) that can be referred to throughout the semantic ...
Definition: ASTContext.h:150
LineState State
bool isReferenceType() const
Definition: Type.h:6118
bool isSpecificBuiltinType(unsigned K) const
Test for a particular builtin type.
Definition: Type.h:6300
i32 captured_struct **param SharedsTy A type which contains references the shared variables *param Shareds Context with the list of shared variables from the p *TaskFunction *param Data Additional data for task generation like final * state
bool isIntegralOrEnumerationType() const
Determine whether this type is an integral or enumeration type.
Definition: Type.h:6433
const llvm::APSInt & Convert(const llvm::APSInt &To, const llvm::APSInt &From)
Convert - Create a new persistent APSInt with the same value as &#39;From&#39; but with the bitwidth and sign...
BinaryOperatorKind
static void dump(llvm::raw_ostream &OS, StringRef FunctionName, ArrayRef< CounterExpression > Expressions, ArrayRef< CounterMappingRegion > Regions)
A record of the "type" of an APSInt, used for conversions.
Definition: APSIntType.h:20
std::unique_ptr< ConstraintManager > CreateZ3ConstraintManager(ProgramStateManager &statemgr, SubEngine *subengine)
Represents a symbolic expression like &#39;x&#39; + 3.
virtual QualType getType() const =0
bool isPromotableIntegerType() const
More type predicates useful for type checking/promotion.
Definition: Type.cpp:2448
bool isComplexType() const
isComplexType() does not include complex integers (a GCC extension).
Definition: Type.cpp:473
QualType getPromotedIntegerType(QualType PromotableType) const
Return the type that PromotableType will promote to: C99 6.3.1.1p2, assuming that PromotableType is a...
const llvm::fltSemantics & getLongDoubleFormat() const
Definition: TargetInfo.h:567
Exposes information about the current target.
Definition: TargetInfo.h:54
bool isNullPtrType() const
Definition: Type.h:6358
Represents a cast expression.
bool isNull() const
Return true if this QualType doesn&#39;t point to a type yet.
Definition: Type.h:720
Optional< T > getAs() const
Convert to the specified SVal type, returning None if this SVal is not of the desired type...
Definition: SVals.h:112
bool isVoidPointerType() const
Definition: Type.cpp:461
bool isComparisonOp() const
Definition: Expr.h:3160
QualType getCanonicalType() const
Definition: Type.h:5921
SVal - This represents a symbolic expression, which can be either an L-value or an R-value...
Definition: SVals.h:76
bool isSignedIntegerOrEnumerationType() const
Determines whether this is an integer type that is signed or an enumeration types whose underlying ty...
Definition: Type.cpp:1854
Represents a symbolic expression like 3 - &#39;x&#39;.
bool isObjCObjectPointerType() const
Definition: Type.h:6203
bool isAnyPointerType() const
Definition: Type.h:6110
A class responsible for cleaning up unused symbols.
const llvm::APSInt * evalAPSInt(BinaryOperator::Opcode Op, const llvm::APSInt &V1, const llvm::APSInt &V2)
bool operator<(DeclarationName LHS, DeclarationName RHS)
Ordering on two declaration names.
const llvm::fltSemantics & getFloatTypeSemantics(QualType T) const
Return the APFloat &#39;semantics&#39; for the specified scalar floating point type.
llvm::APSInt convert(const llvm::APSInt &Value) const LLVM_READONLY
Convert and return a new APSInt with the given value, but this type&#39;s bit width and signedness...
Definition: APSIntType.h:49
Dataflow Directional Tag Classes.
int getFloatingTypeOrder(QualType LHS, QualType RHS) const
Compare the rank of the two specified floating point types, ignoring the domain of the type (i...
UnaryOperatorKind
Represents a symbolic expression involving a binary operator.
const llvm::APSInt & To() const
bool isBooleanType() const
Definition: Type.h:6446
Represents symbolic expression that isn&#39;t a location.
Definition: SVals.h:347
uint64_t getTypeSize(QualType T) const
Return the size of the specified (complete) type T, in bits.
Definition: ASTContext.h:2046
X
Add a minimal nested name specifier fixit hint to allow lookup of a tag name from an outer enclosing ...
Definition: SemaDecl.cpp:13719
unsigned SymbolID
Definition: SymExpr.h:113
BinaryOperator::Opcode getOpcode() const
bool isVoidType() const
Definition: Type.h:6333
Defines the clang::TargetInfo interface.
bool isComplexIntegerType() const
Definition: Type.cpp:479
static llvm::ImmutableListFactory< const FieldRegion * > Factory
CanQualType BoolTy
Definition: ASTContext.h:999
Represents a symbolic expression like &#39;x&#39; + &#39;y&#39;.
A symbol representing data which can be stored in a memory location (region).
Definition: SymExpr.h:117
QualType getIntTypeForBitwidth(unsigned DestWidth, unsigned Signed) const
getIntTypeForBitwidth - sets integer QualTy according to specified details: bitwidth, signed/unsigned.