clang  6.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 
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]), true);
685  } else if (Sort.getBitvectorSortSize() == 128) {
686  Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST));
687  Z3_get_numeral_uint64(Z3Context::ZC, AST,
688  reinterpret_cast<__uint64 *>(&Value[1]));
689  Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true);
690  } else {
691  assert(false && "Bitwidth not supported!");
692  return false;
693  }
694  return true;
695  }
696  case Z3_BOOL_SORT:
697  if (useSemantics && Int.getBitWidth() < 1) {
698  assert(false && "Boolean type doesn't match!");
699  return false;
700  }
701  Int = llvm::APSInt(
702  llvm::APInt(Int.getBitWidth(),
703  Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1
704  : 0),
705  true);
706  return true;
707  }
708  }
709 
710  void Profile(llvm::FoldingSetNodeID &ID) const {
711  ID.AddInteger(Z3_get_ast_hash(Z3Context::ZC, AST));
712  }
713 
714  bool operator<(const Z3Expr &Other) const {
715  llvm::FoldingSetNodeID ID1, ID2;
716  Profile(ID1);
717  Other.Profile(ID2);
718  return ID1 < ID2;
719  }
720 
721  /// Comparison of AST equality, not model equivalence.
722  bool operator==(const Z3Expr &Other) const {
723  assert(Z3_is_eq_sort(Z3Context::ZC, Z3_get_sort(Z3Context::ZC, AST),
724  Z3_get_sort(Z3Context::ZC, Other.AST)) &&
725  "AST's must have the same sort");
726  return Z3_is_eq_ast(Z3Context::ZC, AST, Other.AST);
727  }
728 
729  /// Override implicit move constructor for correct reference counting.
730  Z3Expr &operator=(const Z3Expr &Move) {
731  Z3_inc_ref(Z3Context::ZC, Move.AST);
732  Z3_dec_ref(Z3Context::ZC, AST);
733  AST = Move.AST;
734  return *this;
735  }
736 
737  void print(raw_ostream &OS) const {
738  OS << Z3_ast_to_string(Z3Context::ZC, AST);
739  }
740 
741  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
742 }; // end class Z3Expr
743 
744 class Z3Model {
745  Z3_model Model;
746 
747 public:
748  Z3Model(Z3_model ZM) : Model(ZM) { Z3_model_inc_ref(Z3Context::ZC, Model); }
749 
750  /// Override implicit copy constructor for correct reference counting.
751  Z3Model(const Z3Model &Copy) : Model(Copy.Model) {
752  Z3_model_inc_ref(Z3Context::ZC, Model);
753  }
754 
755  /// Provide move constructor
756  Z3Model(Z3Model &&Move) : Model(nullptr) { *this = std::move(Move); }
757 
758  /// Provide move assignment constructor
759  Z3Model &operator=(Z3Model &&Move) {
760  if (this != &Move) {
761  if (Model)
762  Z3_model_dec_ref(Z3Context::ZC, Model);
763  Model = Move.Model;
764  Move.Model = nullptr;
765  }
766  return *this;
767  }
768 
769  ~Z3Model() {
770  if (Model)
771  Z3_model_dec_ref(Z3Context::ZC, Model);
772  }
773 
774  /// Given an expression, extract the value of this operand in the model.
775  bool getInterpretation(const Z3Expr &Exp, llvm::APSInt &Int) const {
776  Z3_func_decl Func =
777  Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
778  if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
779  return false;
780 
781  Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
782  Z3Sort Sort = Z3Sort::getSort(Assign);
783  return Z3Expr::toAPSInt(Sort, Assign, Int, true);
784  }
785 
786  /// Given an expression, extract the value of this operand in the model.
787  bool getInterpretation(const Z3Expr &Exp, llvm::APFloat &Float) const {
788  Z3_func_decl Func =
789  Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
790  if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
791  return false;
792 
793  Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model, Func);
794  Z3Sort Sort = Z3Sort::getSort(Assign);
795  return Z3Expr::toAPFloat(Sort, Assign, Float, true);
796  }
797 
798  void print(raw_ostream &OS) const {
799  OS << Z3_model_to_string(Z3Context::ZC, Model);
800  }
801 
802  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
803 }; // end class Z3Model
804 
805 class Z3Solver {
806  friend class Z3ConstraintManager;
807 
808  Z3_solver Solver;
809 
810  Z3Solver(Z3_solver ZS) : Solver(ZS) {
811  Z3_solver_inc_ref(Z3Context::ZC, Solver);
812  }
813 
814 public:
815  /// Override implicit copy constructor for correct reference counting.
816  Z3Solver(const Z3Solver &Copy) : Solver(Copy.Solver) {
817  Z3_solver_inc_ref(Z3Context::ZC, Solver);
818  }
819 
820  /// Provide move constructor
821  Z3Solver(Z3Solver &&Move) : Solver(nullptr) { *this = std::move(Move); }
822 
823  /// Provide move assignment constructor
824  Z3Solver &operator=(Z3Solver &&Move) {
825  if (this != &Move) {
826  if (Solver)
827  Z3_solver_dec_ref(Z3Context::ZC, Solver);
828  Solver = Move.Solver;
829  Move.Solver = nullptr;
830  }
831  return *this;
832  }
833 
834  ~Z3Solver() {
835  if (Solver)
836  Z3_solver_dec_ref(Z3Context::ZC, Solver);
837  }
838 
839  /// Given a constraint, add it to the solver
840  void addConstraint(const Z3Expr &Exp) {
841  Z3_solver_assert(Z3Context::ZC, Solver, Exp.AST);
842  }
843 
844  /// Given a program state, construct the logical conjunction and add it to
845  /// the solver
846  void addStateConstraints(ProgramStateRef State) {
847  // TODO: Don't add all the constraints, only the relevant ones
848  ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
849  ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
850 
851  // Construct the logical AND of all the constraints
852  if (I != IE) {
853  std::vector<Z3_ast> ASTs;
854 
855  while (I != IE)
856  ASTs.push_back(I++->second.AST);
857 
858  Z3Expr Conj = Z3Expr::fromNBinOp(BO_LAnd, ASTs);
859  addConstraint(Conj);
860  }
861  }
862 
863  /// Check if the constraints are satisfiable
864  Z3_lbool check() { return Z3_solver_check(Z3Context::ZC, Solver); }
865 
866  /// Push the current solver state
867  void push() { return Z3_solver_push(Z3Context::ZC, Solver); }
868 
869  /// Pop the previous solver state
870  void pop(unsigned NumStates = 1) {
871  assert(Z3_solver_get_num_scopes(Z3Context::ZC, Solver) >= NumStates);
872  return Z3_solver_pop(Z3Context::ZC, Solver, NumStates);
873  }
874 
875  /// Get a model from the solver. Caller should check the model is
876  /// satisfiable.
877  Z3Model getModel() {
878  return Z3Model(Z3_solver_get_model(Z3Context::ZC, Solver));
879  }
880 
881  /// Reset the solver and remove all constraints.
882  void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
883 }; // end class Z3Solver
884 
885 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
886  llvm::report_fatal_error("Z3 error: " +
887  llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
888 }
889 
890 class Z3ConstraintManager : public SimpleConstraintManager {
891  Z3Context Context;
892  mutable Z3Solver Solver;
893 
894 public:
895  Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
896  : SimpleConstraintManager(SE, SB),
897  Solver(Z3_mk_simple_solver(Z3Context::ZC)) {
898  Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler);
899  }
900 
901  //===------------------------------------------------------------------===//
902  // Implementation for interface from ConstraintManager.
903  //===------------------------------------------------------------------===//
904 
905  bool canReasonAbout(SVal X) const override;
906 
907  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
908 
909  const llvm::APSInt *getSymVal(ProgramStateRef State,
910  SymbolRef Sym) const override;
911 
912  ProgramStateRef removeDeadBindings(ProgramStateRef St,
913  SymbolReaper &SymReaper) override;
914 
915  void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
916  const char *sep) override;
917 
918  //===------------------------------------------------------------------===//
919  // Implementation for interface from SimpleConstraintManager.
920  //===------------------------------------------------------------------===//
921 
923  bool Assumption) override;
924 
925  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
926  const llvm::APSInt &From,
927  const llvm::APSInt &To,
928  bool InRange) override;
929 
930  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
931  bool Assumption) override;
932 
933 private:
934  //===------------------------------------------------------------------===//
935  // Internal implementation.
936  //===------------------------------------------------------------------===//
937 
938  // Check whether a new model is satisfiable, and update the program state.
939  ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym,
940  const Z3Expr &Exp);
941 
942  // Generate and check a Z3 model, using the given constraint.
943  Z3_lbool checkZ3Model(ProgramStateRef State, const Z3Expr &Exp) const;
944 
945  // Generate a Z3Expr that represents the given symbolic expression.
946  // Sets the hasComparison parameter if the expression has a comparison
947  // operator.
948  // Sets the RetTy parameter to the final return type after promotions and
949  // casts.
950  Z3Expr getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,
951  bool *hasComparison = nullptr) const;
952 
953  // Generate a Z3Expr that takes the logical not of an expression.
954  Z3Expr getZ3NotExpr(const Z3Expr &Exp) const;
955 
956  // Generate a Z3Expr that compares the expression to zero.
957  Z3Expr getZ3ZeroExpr(const Z3Expr &Exp, QualType RetTy,
958  bool Assumption) const;
959 
960  // Recursive implementation to unpack and generate symbolic expression.
961  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
962  Z3Expr getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
963  bool *hasComparison) const;
964 
965  // Wrapper to generate Z3Expr from SymbolData.
966  Z3Expr getZ3DataExpr(const SymbolID ID, QualType Ty) const;
967 
968  // Wrapper to generate Z3Expr from SymbolCast.
969  Z3Expr getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, QualType Ty) const;
970 
971  // Wrapper to generate Z3Expr from BinarySymExpr.
972  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
973  Z3Expr getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
974  QualType *RetTy) const;
975 
976  // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
977  // Sets the RetTy parameter. See getZ3Expr().
978  Z3Expr getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
979  BinaryOperator::Opcode Op, const Z3Expr &RHS,
980  QualType RTy, QualType *RetTy) const;
981 
982  //===------------------------------------------------------------------===//
983  // Helper functions.
984  //===------------------------------------------------------------------===//
985 
986  // Recover the QualType of an APSInt.
987  // TODO: Refactor to put elsewhere
988  QualType getAPSIntType(const llvm::APSInt &Int) const;
989 
990  // Perform implicit type conversion on binary symbolic expressions.
991  // May modify all input parameters.
992  // TODO: Refactor to use built-in conversion functions
993  void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType &LTy,
994  QualType &RTy) const;
995 
996  // Perform implicit integer type conversion.
997  // May modify all input parameters.
998  // TODO: Refactor to use Sema::handleIntegerConversion()
999  template <typename T,
1000  T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1001  void doIntTypeConversion(T &LHS, QualType &LTy, T &RHS, QualType &RTy) const;
1002 
1003  // Perform implicit floating-point type conversion.
1004  // May modify all input parameters.
1005  // TODO: Refactor to use Sema::handleFloatConversion()
1006  template <typename T,
1007  T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1008  void doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
1009  QualType &RTy) const;
1010 
1011  // Callback function for doCast parameter on APSInt type.
1012  static llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy,
1013  uint64_t ToWidth, QualType FromTy,
1014  uint64_t FromWidth);
1015 }; // end class Z3ConstraintManager
1016 
1017 Z3_context Z3Context::ZC;
1018 
1019 } // end anonymous namespace
1020 
1021 ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State,
1022  SymbolRef Sym, bool Assumption) {
1023  QualType RetTy;
1024  bool hasComparison;
1025 
1026  Z3Expr Exp = getZ3Expr(Sym, &RetTy, &hasComparison);
1027  // Create zero comparison for implicit boolean cast, with reversed assumption
1028  if (!hasComparison && !RetTy->isBooleanType())
1029  return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption));
1030 
1031  return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));
1032 }
1033 
1034 ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
1035  ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
1036  const llvm::APSInt &To, bool InRange) {
1037  QualType RetTy;
1038  // The expression may be casted, so we cannot call getZ3DataExpr() directly
1039  Z3Expr Exp = getZ3Expr(Sym, &RetTy);
1040 
1041  assert((getAPSIntType(From) == getAPSIntType(To)) &&
1042  "Range values have different types!");
1043  QualType RTy = getAPSIntType(From);
1044  bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
1045  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
1046  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
1047 
1048  // Construct single (in)equality
1049  if (From == To)
1050  return assumeZ3Expr(State, Sym,
1051  getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
1052  FromExp, RTy, nullptr));
1053 
1054  // Construct two (in)equalities, and a logical and/or
1055  Z3Expr LHS =
1056  getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
1057  Z3Expr RHS =
1058  getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
1059  return assumeZ3Expr(
1060  State, Sym,
1061  Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
1062 }
1063 
1064 ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
1065  SymbolRef Sym,
1066  bool Assumption) {
1067  // Skip anything that is unsupported
1068  return State;
1069 }
1070 
1071 bool Z3ConstraintManager::canReasonAbout(SVal X) const {
1072  const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
1073 
1075  if (!SymVal)
1076  return true;
1077 
1078  const SymExpr *Sym = SymVal->getSymbol();
1079  do {
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  break;
1094  } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
1095  Sym = SC->getOperand();
1096  } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1097  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
1098  Sym = SIE->getLHS();
1099  } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
1100  Sym = ISE->getRHS();
1101  } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
1102  return canReasonAbout(nonloc::SymbolVal(SSM->getLHS())) &&
1103  canReasonAbout(nonloc::SymbolVal(SSM->getRHS()));
1104  } else {
1105  llvm_unreachable("Unsupported binary expression to reason about!");
1106  }
1107  } else {
1108  llvm_unreachable("Unsupported expression to reason about!");
1109  }
1110  } while (Sym);
1111 
1112  return true;
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 &BV = getBasicVals();
1149  ASTContext &Ctx = BV.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 &BV.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 &BV.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 = *LHS, ConvertedRHS = *RHS;
1215  QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
1216  doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
1217  ConvertedLHS, LTy, ConvertedRHS, RTy);
1218  return BV.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
1219  }
1220 
1221  llvm_unreachable("Unsupported expression to get symbol value!");
1222 }
1223 
1225 Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
1226  SymbolReaper &SymReaper) {
1227  ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
1228  ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
1229 
1230  for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
1231  if (SymReaper.maybeDead(I->first))
1232  CZ = CZFactory.remove(CZ, *I);
1233  }
1234 
1235  return State->set<ConstraintZ3>(CZ);
1236 }
1237 
1238 //===------------------------------------------------------------------===//
1239 // Internal implementation.
1240 //===------------------------------------------------------------------===//
1241 
1242 ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State,
1243  SymbolRef Sym,
1244  const Z3Expr &Exp) {
1245  // Check the model, avoid simplifying AST to save time
1246  if (checkZ3Model(State, Exp) == Z3_L_TRUE)
1247  return State->add<ConstraintZ3>(std::make_pair(Sym, Exp));
1248 
1249  return nullptr;
1250 }
1251 
1252 Z3_lbool Z3ConstraintManager::checkZ3Model(ProgramStateRef State,
1253  const Z3Expr &Exp) const {
1254  Solver.reset();
1255  Solver.addConstraint(Exp);
1256  Solver.addStateConstraints(State);
1257  return Solver.check();
1258 }
1259 
1260 Z3Expr Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy,
1261  bool *hasComparison) const {
1262  if (hasComparison) {
1263  *hasComparison = false;
1264  }
1265 
1266  return getZ3SymExpr(Sym, RetTy, hasComparison);
1267 }
1268 
1269 Z3Expr Z3ConstraintManager::getZ3NotExpr(const Z3Expr &Exp) const {
1270  return Z3Expr::fromUnOp(UO_LNot, Exp);
1271 }
1272 
1273 Z3Expr Z3ConstraintManager::getZ3ZeroExpr(const Z3Expr &Exp, QualType Ty,
1274  bool Assumption) const {
1275  ASTContext &Ctx = getBasicVals().getContext();
1276  if (Ty->isRealFloatingType()) {
1277  llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
1278  return Z3Expr::fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
1279  Z3Expr::fromAPFloat(Zero));
1280  } else if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
1281  Ty->isBlockPointerType() || Ty->isReferenceType()) {
1282  bool isSigned = Ty->isSignedIntegerOrEnumerationType();
1283  // Skip explicit comparison for boolean types
1284  if (Ty->isBooleanType())
1285  return Assumption ? getZ3NotExpr(Exp) : Exp;
1286  return Z3Expr::fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
1287  Z3Expr::fromInt("0", Ctx.getTypeSize(Ty)),
1288  isSigned);
1289  }
1290 
1291  llvm_unreachable("Unsupported type for zero value!");
1292 }
1293 
1294 Z3Expr Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
1295  bool *hasComparison) const {
1296  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
1297  if (RetTy)
1298  *RetTy = Sym->getType();
1299 
1300  return getZ3DataExpr(SD->getSymbolID(), Sym->getType());
1301  } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
1302  if (RetTy)
1303  *RetTy = Sym->getType();
1304 
1305  QualType FromTy;
1306  Z3Expr Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison);
1307  // Casting an expression with a comparison invalidates it. Note that this
1308  // must occur after the recursive call above.
1309  // e.g. (signed char) (x > 0)
1310  if (hasComparison)
1311  *hasComparison = false;
1312  return getZ3CastExpr(Exp, FromTy, Sym->getType());
1313  } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
1314  Z3Expr Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy);
1315  // Set the hasComparison parameter, in post-order traversal order.
1316  if (hasComparison)
1317  *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
1318  return Exp;
1319  }
1320 
1321  llvm_unreachable("Unsupported SymbolRef type!");
1322 }
1323 
1324 Z3Expr Z3ConstraintManager::getZ3DataExpr(const SymbolID ID,
1325  QualType Ty) const {
1326  ASTContext &Ctx = getBasicVals().getContext();
1327  return Z3Expr::fromData(ID, Ty->isBooleanType(), Ty->isRealFloatingType(),
1328  Ctx.getTypeSize(Ty));
1329 }
1330 
1331 Z3Expr Z3ConstraintManager::getZ3CastExpr(const Z3Expr &Exp, QualType FromTy,
1332  QualType ToTy) const {
1333  ASTContext &Ctx = getBasicVals().getContext();
1334  return Z3Expr::fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
1335  Ctx.getTypeSize(FromTy));
1336 }
1337 
1338 Z3Expr Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
1339  bool *hasComparison,
1340  QualType *RetTy) const {
1341  QualType LTy, RTy;
1342  BinaryOperator::Opcode Op = BSE->getOpcode();
1343 
1344  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
1345  RTy = getAPSIntType(SIE->getRHS());
1346  Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), &LTy, hasComparison);
1347  Z3Expr RHS = Z3Expr::fromAPSInt(SIE->getRHS());
1348  return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1349  } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
1350  LTy = getAPSIntType(ISE->getLHS());
1351  Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS());
1352  Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
1353  return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1354  } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
1355  Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), &LTy, hasComparison);
1356  Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
1357  return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
1358  } else {
1359  llvm_unreachable("Unsupported BinarySymExpr type!");
1360  }
1361 }
1362 
1363 Z3Expr Z3ConstraintManager::getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
1365  const Z3Expr &RHS, QualType RTy,
1366  QualType *RetTy) const {
1367  Z3Expr NewLHS = LHS;
1368  Z3Expr NewRHS = RHS;
1369  doTypeConversion(NewLHS, NewRHS, LTy, RTy);
1370  // Update the return type parameter if the output type has changed.
1371  if (RetTy) {
1372  // A boolean result can be represented as an integer type in C/C++, but at
1373  // this point we only care about the Z3 type. Set it as a boolean type to
1374  // avoid subsequent Z3 errors.
1376  ASTContext &Ctx = getBasicVals().getContext();
1377  *RetTy = Ctx.BoolTy;
1378  } else {
1379  *RetTy = LTy;
1380  }
1381 
1382  // If the two operands are pointers and the operation is a subtraction, the
1383  // result is of type ptrdiff_t, which is signed
1384  if (LTy->isAnyPointerType() && LTy == RTy && Op == BO_Sub) {
1385  ASTContext &Ctx = getBasicVals().getContext();
1386  *RetTy = Ctx.getIntTypeForBitwidth(Ctx.getTypeSize(LTy), true);
1387  }
1388  }
1389 
1390  return LTy->isRealFloatingType()
1391  ? Z3Expr::fromFloatBinOp(NewLHS, Op, NewRHS)
1392  : Z3Expr::fromBinOp(NewLHS, Op, NewRHS,
1393  LTy->isSignedIntegerOrEnumerationType());
1394 }
1395 
1396 //===------------------------------------------------------------------===//
1397 // Helper functions.
1398 //===------------------------------------------------------------------===//
1399 
1400 QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
1401  ASTContext &Ctx = getBasicVals().getContext();
1402  return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
1403 }
1404 
1405 void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
1406  QualType &LTy, QualType &RTy) const {
1407  ASTContext &Ctx = getBasicVals().getContext();
1408 
1409  // Perform type conversion
1410  if (LTy->isIntegralOrEnumerationType() &&
1411  RTy->isIntegralOrEnumerationType()) {
1412  if (LTy->isArithmeticType() && RTy->isArithmeticType())
1413  return doIntTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
1414  } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
1415  return doFloatTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
1416  } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
1417  (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
1418  (LTy->isReferenceType() || RTy->isReferenceType())) {
1419  // TODO: Refactor to Sema::FindCompositePointerType(), and
1420  // Sema::CheckCompareOperands().
1421 
1422  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1423  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1424 
1425  // Cast the non-pointer type to the pointer type.
1426  // TODO: Be more strict about this.
1427  if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
1428  (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
1429  (LTy->isReferenceType() ^ RTy->isReferenceType())) {
1430  if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
1431  LTy->isReferenceType()) {
1432  LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
1433  LTy = RTy;
1434  } else {
1435  RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
1436  RTy = LTy;
1437  }
1438  }
1439 
1440  // Cast the void pointer type to the non-void pointer type.
1441  // For void types, this assumes that the casted value is equal to the value
1442  // of the original pointer, and does not account for alignment requirements.
1443  if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
1444  assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
1445  "Pointer types have different bitwidths!");
1446  if (RTy->isVoidPointerType())
1447  RTy = LTy;
1448  else
1449  LTy = RTy;
1450  }
1451 
1452  if (LTy == RTy)
1453  return;
1454  }
1455 
1456  // Fallback: for the solver, assume that these types don't really matter
1457  if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
1458  (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
1459  LTy = RTy;
1460  return;
1461  }
1462 
1463  // TODO: Refine behavior for invalid type casts
1464 }
1465 
1466 template <typename T,
1467  T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1468 void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType &LTy, T &RHS,
1469  QualType &RTy) const {
1470  ASTContext &Ctx = getBasicVals().getContext();
1471 
1472  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1473  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1474 
1475  // Always perform integer promotion before checking type equality.
1476  // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
1477  if (LTy->isPromotableIntegerType()) {
1478  QualType NewTy = Ctx.getPromotedIntegerType(LTy);
1479  uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
1480  LHS = (*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);
1481  LTy = NewTy;
1482  LBitWidth = NewBitWidth;
1483  }
1484  if (RTy->isPromotableIntegerType()) {
1485  QualType NewTy = Ctx.getPromotedIntegerType(RTy);
1486  uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
1487  RHS = (*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth);
1488  RTy = NewTy;
1489  RBitWidth = NewBitWidth;
1490  }
1491 
1492  if (LTy == RTy)
1493  return;
1494 
1495  // Perform integer type conversion
1496  // Note: Safe to skip updating bitwidth because this must terminate
1497  bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
1498  bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
1499 
1500  int order = Ctx.getIntegerTypeOrder(LTy, RTy);
1501  if (isLSignedTy == isRSignedTy) {
1502  // Same signedness; use the higher-ranked type
1503  if (order == 1) {
1504  RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1505  RTy = LTy;
1506  } else {
1507  LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1508  LTy = RTy;
1509  }
1510  } else if (order != (isLSignedTy ? 1 : -1)) {
1511  // The unsigned type has greater than or equal rank to the
1512  // signed type, so use the unsigned type
1513  if (isRSignedTy) {
1514  RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1515  RTy = LTy;
1516  } else {
1517  LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1518  LTy = RTy;
1519  }
1520  } else if (LBitWidth != RBitWidth) {
1521  // The two types are different widths; if we are here, that
1522  // means the signed type is larger than the unsigned type, so
1523  // use the signed type.
1524  if (isLSignedTy) {
1525  RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1526  RTy = LTy;
1527  } else {
1528  LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1529  LTy = RTy;
1530  }
1531  } else {
1532  // The signed type is higher-ranked than the unsigned type,
1533  // but isn't actually any bigger (like unsigned int and long
1534  // on most 32-bit systems). Use the unsigned type corresponding
1535  // to the signed type.
1536  QualType NewTy = Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
1537  RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1538  RTy = NewTy;
1539  LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1540  LTy = NewTy;
1541  }
1542 }
1543 
1544 template <typename T,
1545  T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
1546 void Z3ConstraintManager::doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
1547  QualType &RTy) const {
1548  ASTContext &Ctx = getBasicVals().getContext();
1549 
1550  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
1551  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
1552 
1553  // Perform float-point type promotion
1554  if (!LTy->isRealFloatingType()) {
1555  LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
1556  LTy = RTy;
1557  LBitWidth = RBitWidth;
1558  }
1559  if (!RTy->isRealFloatingType()) {
1560  RHS = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
1561  RTy = LTy;
1562  RBitWidth = LBitWidth;
1563  }
1564 
1565  if (LTy == RTy)
1566  return;
1567 
1568  // If we have two real floating types, convert the smaller operand to the
1569  // bigger result
1570  // Note: Safe to skip updating bitwidth because this must terminate
1571  int order = Ctx.getFloatingTypeOrder(LTy, RTy);
1572  if (order > 0) {
1573  RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
1574  RTy = LTy;
1575  } else if (order == 0) {
1576  LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
1577  LTy = RTy;
1578  } else {
1579  llvm_unreachable("Unsupported floating-point type cast!");
1580  }
1581 }
1582 
1583 llvm::APSInt Z3ConstraintManager::castAPSInt(const llvm::APSInt &V,
1584  QualType ToTy, uint64_t ToWidth,
1585  QualType FromTy,
1586  uint64_t FromWidth) {
1587  APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
1588  return TargetType.convert(V);
1589 }
1590 
1591 //==------------------------------------------------------------------------==/
1592 // Pretty-printing.
1593 //==------------------------------------------------------------------------==/
1594 
1595 void Z3ConstraintManager::print(ProgramStateRef St, raw_ostream &OS,
1596  const char *nl, const char *sep) {
1597 
1598  ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
1599 
1600  OS << nl << sep << "Constraints:";
1601  for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
1602  OS << nl << ' ' << I->first << " : ";
1603  I->second.print(OS);
1604  }
1605  OS << nl;
1606 }
1607 
1608 #endif
1609 
1610 std::unique_ptr<ConstraintManager>
1612 #if CLANG_ANALYZER_WITH_Z3
1613  return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
1614 #else
1615  llvm::report_fatal_error("Clang was not compiled with Z3 support!", false);
1616  return nullptr;
1617 #endif
1618 }
A (possibly-)qualified type.
Definition: Type.h:653
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:5952
bool operator==(CanQual< T > x, CanQual< U > y)
bool isArithmeticType() const
Definition: Type.cpp:1908
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:1893
bool isLogicalOp() const
Definition: Expr.h:3106
unsigned SymbolID
Definition: SymExpr.h:110
QualType getCorrespondingUnsignedType(QualType T) const
Symbolic value.
Definition: SymExpr.h:29
Holds long-lived AST nodes (such as types and decls) that can be referred to throughout the semantic ...
Definition: ASTContext.h:149
LineState State
bool isReferenceType() const
Definition: Type.h:5956
bool isSpecificBuiltinType(unsigned K) const
Test for a particular builtin type.
Definition: Type.h:6138
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:6221
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:2381
bool isComplexType() const
isComplexType() does not include complex integers (a GCC extension).
Definition: Type.cpp:438
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:422
Exposes information about the current target.
Definition: TargetInfo.h:54
const FunctionProtoType * T
bool isNullPtrType() const
Definition: Type.h:6184
Represents a cast expression.
Optional< T > getAs() const
Convert to the specified SVal type, returning None if this SVal is not of the desired type...
Definition: SVals.h:100
bool isVoidPointerType() const
Definition: Type.cpp:426
bool isComparisonOp() const
Definition: Expr.h:3076
QualType getCanonicalType() const
Definition: Type.h:5759
SVal - This represents a symbolic expression, which can be either an L-value or an R-value...
Definition: SVals.h:63
bool isSignedIntegerOrEnumerationType() const
Determines whether this is an integer type that is signed or an enumeration types whose underlying ty...
Definition: Type.cpp:1816
Represents a symbolic expression like 3 - &#39;x&#39;.
bool isObjCObjectPointerType() const
Definition: Type.h:6041
bool isAnyPointerType() const
Definition: Type.h:5948
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.
bool isBooleanType() const
Definition: Type.h:6234
Represents symbolic expression.
Definition: SVals.h:327
uint64_t getTypeSize(QualType T) const
Return the size of the specified (complete) type T, in bits.
Definition: ASTContext.h:2007
X
Add a minimal nested name specifier fixit hint to allow lookup of a tag name from an outer enclosing ...
Definition: SemaDecl.cpp:13008
BinaryOperator::Opcode getOpcode() const
bool isVoidType() const
Definition: Type.h:6171
Defines the clang::TargetInfo interface.
bool isComplexIntegerType() const
Definition: Type.cpp:444
CanQualType BoolTy
Definition: ASTContext.h:997
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:113
QualType getIntTypeForBitwidth(unsigned DestWidth, unsigned Signed) const
getIntTypeForBitwidth - sets integer QualTy according to specified details: bitwidth, signed/unsigned.