clang  14.0.0git
SMTConv.h
Go to the documentation of this file.
1 //== SMTConv.h --------------------------------------------------*- C++ -*--==//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 //
9 // This file defines a set of functions to create SMT expressions
10 //
11 //===----------------------------------------------------------------------===//
12 
13 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
14 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
15 
16 #include "clang/AST/Expr.h"
19 #include "llvm/Support/SMTAPI.h"
20 
21 namespace clang {
22 namespace ento {
23 
24 class SMTConv {
25 public:
26  // Returns an appropriate sort, given a QualType and it's bit width.
27  static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,
28  const QualType &Ty, unsigned BitWidth) {
29  if (Ty->isBooleanType())
30  return Solver->getBoolSort();
31 
32  if (Ty->isRealFloatingType())
33  return Solver->getFloatSort(BitWidth);
34 
35  return Solver->getBitvectorSort(BitWidth);
36  }
37 
38  /// Constructs an SMTSolverRef from an unary operator.
39  static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver,
40  const UnaryOperator::Opcode Op,
41  const llvm::SMTExprRef &Exp) {
42  switch (Op) {
43  case UO_Minus:
44  return Solver->mkBVNeg(Exp);
45 
46  case UO_Not:
47  return Solver->mkBVNot(Exp);
48 
49  case UO_LNot:
50  return Solver->mkNot(Exp);
51 
52  default:;
53  }
54  llvm_unreachable("Unimplemented opcode");
55  }
56 
57  /// Constructs an SMTSolverRef from a floating-point unary operator.
58  static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver,
59  const UnaryOperator::Opcode Op,
60  const llvm::SMTExprRef &Exp) {
61  switch (Op) {
62  case UO_Minus:
63  return Solver->mkFPNeg(Exp);
64 
65  case UO_LNot:
66  return fromUnOp(Solver, Op, Exp);
67 
68  default:;
69  }
70  llvm_unreachable("Unimplemented opcode");
71  }
72 
73  /// Construct an SMTSolverRef from a n-ary binary operator.
74  static inline llvm::SMTExprRef
75  fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op,
76  const std::vector<llvm::SMTExprRef> &ASTs) {
77  assert(!ASTs.empty());
78 
79  if (Op != BO_LAnd && Op != BO_LOr)
80  llvm_unreachable("Unimplemented opcode");
81 
82  llvm::SMTExprRef res = ASTs.front();
83  for (std::size_t i = 1; i < ASTs.size(); ++i)
84  res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])
85  : Solver->mkOr(res, ASTs[i]);
86  return res;
87  }
88 
89  /// Construct an SMTSolverRef from a binary operator.
90  static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver,
91  const llvm::SMTExprRef &LHS,
92  const BinaryOperator::Opcode Op,
93  const llvm::SMTExprRef &RHS,
94  bool isSigned) {
95  assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
96  "AST's must have the same sort!");
97 
98  switch (Op) {
99  // Multiplicative operators
100  case BO_Mul:
101  return Solver->mkBVMul(LHS, RHS);
102 
103  case BO_Div:
104  return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);
105 
106  case BO_Rem:
107  return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);
108 
109  // Additive operators
110  case BO_Add:
111  return Solver->mkBVAdd(LHS, RHS);
112 
113  case BO_Sub:
114  return Solver->mkBVSub(LHS, RHS);
115 
116  // Bitwise shift operators
117  case BO_Shl:
118  return Solver->mkBVShl(LHS, RHS);
119 
120  case BO_Shr:
121  return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);
122 
123  // Relational operators
124  case BO_LT:
125  return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);
126 
127  case BO_GT:
128  return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);
129 
130  case BO_LE:
131  return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);
132 
133  case BO_GE:
134  return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);
135 
136  // Equality operators
137  case BO_EQ:
138  return Solver->mkEqual(LHS, RHS);
139 
140  case BO_NE:
141  return fromUnOp(Solver, UO_LNot,
142  fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned));
143 
144  // Bitwise operators
145  case BO_And:
146  return Solver->mkBVAnd(LHS, RHS);
147 
148  case BO_Xor:
149  return Solver->mkBVXor(LHS, RHS);
150 
151  case BO_Or:
152  return Solver->mkBVOr(LHS, RHS);
153 
154  // Logical operators
155  case BO_LAnd:
156  return Solver->mkAnd(LHS, RHS);
157 
158  case BO_LOr:
159  return Solver->mkOr(LHS, RHS);
160 
161  default:;
162  }
163  llvm_unreachable("Unimplemented opcode");
164  }
165 
166  /// Construct an SMTSolverRef from a special floating-point binary
167  /// operator.
168  static inline llvm::SMTExprRef
169  fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS,
170  const BinaryOperator::Opcode Op,
171  const llvm::APFloat::fltCategory &RHS) {
172  switch (Op) {
173  // Equality operators
174  case BO_EQ:
175  switch (RHS) {
176  case llvm::APFloat::fcInfinity:
177  return Solver->mkFPIsInfinite(LHS);
178 
179  case llvm::APFloat::fcNaN:
180  return Solver->mkFPIsNaN(LHS);
181 
182  case llvm::APFloat::fcNormal:
183  return Solver->mkFPIsNormal(LHS);
184 
185  case llvm::APFloat::fcZero:
186  return Solver->mkFPIsZero(LHS);
187  }
188  break;
189 
190  case BO_NE:
191  return fromFloatUnOp(Solver, UO_LNot,
192  fromFloatSpecialBinOp(Solver, LHS, BO_EQ, RHS));
193 
194  default:;
195  }
196 
197  llvm_unreachable("Unimplemented opcode");
198  }
199 
200  /// Construct an SMTSolverRef from a floating-point binary operator.
201  static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver,
202  const llvm::SMTExprRef &LHS,
203  const BinaryOperator::Opcode Op,
204  const llvm::SMTExprRef &RHS) {
205  assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
206  "AST's must have the same sort!");
207 
208  switch (Op) {
209  // Multiplicative operators
210  case BO_Mul:
211  return Solver->mkFPMul(LHS, RHS);
212 
213  case BO_Div:
214  return Solver->mkFPDiv(LHS, RHS);
215 
216  case BO_Rem:
217  return Solver->mkFPRem(LHS, RHS);
218 
219  // Additive operators
220  case BO_Add:
221  return Solver->mkFPAdd(LHS, RHS);
222 
223  case BO_Sub:
224  return Solver->mkFPSub(LHS, RHS);
225 
226  // Relational operators
227  case BO_LT:
228  return Solver->mkFPLt(LHS, RHS);
229 
230  case BO_GT:
231  return Solver->mkFPGt(LHS, RHS);
232 
233  case BO_LE:
234  return Solver->mkFPLe(LHS, RHS);
235 
236  case BO_GE:
237  return Solver->mkFPGe(LHS, RHS);
238 
239  // Equality operators
240  case BO_EQ:
241  return Solver->mkFPEqual(LHS, RHS);
242 
243  case BO_NE:
244  return fromFloatUnOp(Solver, UO_LNot,
245  fromFloatBinOp(Solver, LHS, BO_EQ, RHS));
246 
247  // Logical operators
248  case BO_LAnd:
249  case BO_LOr:
250  return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false);
251 
252  default:;
253  }
254 
255  llvm_unreachable("Unimplemented opcode");
256  }
257 
258  /// Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy,
259  /// and their bit widths.
260  static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver,
261  const llvm::SMTExprRef &Exp,
262  QualType ToTy, uint64_t ToBitWidth,
263  QualType FromTy,
264  uint64_t FromBitWidth) {
265  if ((FromTy->isIntegralOrEnumerationType() &&
266  ToTy->isIntegralOrEnumerationType()) ||
267  (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
268  (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
269  (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
270 
271  if (FromTy->isBooleanType()) {
272  assert(ToBitWidth > 0 && "BitWidth must be positive!");
273  return Solver->mkIte(
274  Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth),
275  Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth));
276  }
277 
278  if (ToBitWidth > FromBitWidth)
279  return FromTy->isSignedIntegerOrEnumerationType()
280  ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
281  : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
282 
283  if (ToBitWidth < FromBitWidth)
284  return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
285 
286  // Both are bitvectors with the same width, ignore the type cast
287  return Exp;
288  }
289 
290  if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
291  if (ToBitWidth != FromBitWidth)
292  return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
293 
294  return Exp;
295  }
296 
297  if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
298  llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
299  return FromTy->isSignedIntegerOrEnumerationType()
300  ? Solver->mkSBVtoFP(Exp, Sort)
301  : Solver->mkUBVtoFP(Exp, Sort);
302  }
303 
304  if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
305  return ToTy->isSignedIntegerOrEnumerationType()
306  ? Solver->mkFPtoSBV(Exp, ToBitWidth)
307  : Solver->mkFPtoUBV(Exp, ToBitWidth);
308 
309  llvm_unreachable("Unsupported explicit type cast!");
310  }
311 
312  // Callback function for doCast parameter on APSInt type.
313  static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver,
314  const llvm::APSInt &V, QualType ToTy,
315  uint64_t ToWidth, QualType FromTy,
316  uint64_t FromWidth) {
317  APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
318  return TargetType.convert(V);
319  }
320 
321  /// Construct an SMTSolverRef from a SymbolData.
322  static inline llvm::SMTExprRef
323  fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) {
324  const SymbolID ID = Sym->getSymbolID();
325  const QualType Ty = Sym->getType();
326  const uint64_t BitWidth = Ctx.getTypeSize(Ty);
327 
329  llvm::raw_svector_ostream OS(Str);
330  OS << Sym->getKindStr() << ID;
331  return Solver->mkSymbol(Str.c_str(), mkSort(Solver, Ty, BitWidth));
332  }
333 
334  // Wrapper to generate SMTSolverRef from SymbolCast data.
335  static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,
336  ASTContext &Ctx,
337  const llvm::SMTExprRef &Exp,
338  QualType FromTy, QualType ToTy) {
339  return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
340  Ctx.getTypeSize(FromTy));
341  }
342 
343  // Wrapper to generate SMTSolverRef from unpacked binary symbolic
344  // expression. Sets the RetTy parameter. See getSMTSolverRef().
345  static inline llvm::SMTExprRef
346  getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
347  const llvm::SMTExprRef &LHS, QualType LTy,
348  BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS,
349  QualType RTy, QualType *RetTy) {
350  llvm::SMTExprRef NewLHS = LHS;
351  llvm::SMTExprRef NewRHS = RHS;
352  doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
353 
354  // Update the return type parameter if the output type has changed.
355  if (RetTy) {
356  // A boolean result can be represented as an integer type in C/C++, but at
357  // this point we only care about the SMT sorts. Set it as a boolean type
358  // to avoid subsequent SMT errors.
361  *RetTy = Ctx.BoolTy;
362  } else {
363  *RetTy = LTy;
364  }
365 
366  // If the two operands are pointers and the operation is a subtraction,
367  // the result is of type ptrdiff_t, which is signed
368  if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) {
369  *RetTy = Ctx.getPointerDiffType();
370  }
371  }
372 
373  return LTy->isRealFloatingType()
374  ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS)
375  : fromBinOp(Solver, NewLHS, Op, NewRHS,
377  }
378 
379  // Wrapper to generate SMTSolverRef from BinarySymExpr.
380  // Sets the hasComparison and RetTy parameters. See getSMTSolverRef().
381  static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver,
382  ASTContext &Ctx,
383  const BinarySymExpr *BSE,
384  bool *hasComparison,
385  QualType *RetTy) {
386  QualType LTy, RTy;
387  BinaryOperator::Opcode Op = BSE->getOpcode();
388 
389  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
390  llvm::SMTExprRef LHS =
391  getSymExpr(Solver, Ctx, SIE->getLHS(), &LTy, hasComparison);
392  llvm::APSInt NewRInt;
393  std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
394  llvm::SMTExprRef RHS =
395  Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
396  return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
397  }
398 
399  if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
400  llvm::APSInt NewLInt;
401  std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
402  llvm::SMTExprRef LHS =
403  Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
404  llvm::SMTExprRef RHS =
405  getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
406  return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
407  }
408 
409  if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
410  llvm::SMTExprRef LHS =
411  getSymExpr(Solver, Ctx, SSM->getLHS(), &LTy, hasComparison);
412  llvm::SMTExprRef RHS =
413  getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
414  return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
415  }
416 
417  llvm_unreachable("Unsupported BinarySymExpr type!");
418  }
419 
420  // Recursive implementation to unpack and generate symbolic expression.
421  // Sets the hasComparison and RetTy parameters. See getExpr().
422  static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
423  ASTContext &Ctx, SymbolRef Sym,
424  QualType *RetTy,
425  bool *hasComparison) {
426  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
427  if (RetTy)
428  *RetTy = Sym->getType();
429 
430  return fromData(Solver, Ctx, SD);
431  }
432 
433  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
434  if (RetTy)
435  *RetTy = Sym->getType();
436 
437  QualType FromTy;
438  llvm::SMTExprRef Exp =
439  getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
440 
441  // Casting an expression with a comparison invalidates it. Note that this
442  // must occur after the recursive call above.
443  // e.g. (signed char) (x > 0)
444  if (hasComparison)
445  *hasComparison = false;
446  return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
447  }
448 
449  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
450  llvm::SMTExprRef Exp =
451  getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
452  // Set the hasComparison parameter, in post-order traversal order.
453  if (hasComparison)
454  *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
455  return Exp;
456  }
457 
458  llvm_unreachable("Unsupported SymbolRef type!");
459  }
460 
461  // Generate an SMTSolverRef that represents the given symbolic expression.
462  // Sets the hasComparison parameter if the expression has a comparison
463  // operator. Sets the RetTy parameter to the final return type after
464  // promotions and casts.
465  static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
466  ASTContext &Ctx, SymbolRef Sym,
467  QualType *RetTy = nullptr,
468  bool *hasComparison = nullptr) {
469  if (hasComparison) {
470  *hasComparison = false;
471  }
472 
473  return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
474  }
475 
476  // Generate an SMTSolverRef that compares the expression to zero.
477  static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver,
478  ASTContext &Ctx,
479  const llvm::SMTExprRef &Exp,
480  QualType Ty, bool Assumption) {
481  if (Ty->isRealFloatingType()) {
482  llvm::APFloat Zero =
483  llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
484  return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
485  Solver->mkFloat(Zero));
486  }
487 
488  if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
489  Ty->isBlockPointerType() || Ty->isReferenceType()) {
490 
491  // Skip explicit comparison for boolean types
492  bool isSigned = Ty->isSignedIntegerOrEnumerationType();
493  if (Ty->isBooleanType())
494  return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
495 
496  return fromBinOp(
497  Solver, Exp, Assumption ? BO_EQ : BO_NE,
498  Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
499  isSigned);
500  }
501 
502  llvm_unreachable("Unsupported type for zero value!");
503  }
504 
505  // Wrapper to generate SMTSolverRef from a range. If From == To, an
506  // equality will be created instead.
507  static inline llvm::SMTExprRef
508  getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
509  const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) {
510  // Convert lower bound
511  QualType FromTy;
512  llvm::APSInt NewFromInt;
513  std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
514  llvm::SMTExprRef FromExp =
515  Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
516 
517  // Convert symbol
518  QualType SymTy;
519  llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
520 
521  // Construct single (in)equality
522  if (From == To)
523  return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
524  FromExp, FromTy, /*RetTy=*/nullptr);
525 
526  QualType ToTy;
527  llvm::APSInt NewToInt;
528  std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
529  llvm::SMTExprRef ToExp =
530  Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
531  assert(FromTy == ToTy && "Range values have different types!");
532 
533  // Construct two (in)equalities, and a logical and/or
534  llvm::SMTExprRef LHS =
535  getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
536  FromTy, /*RetTy=*/nullptr);
537  llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
538  InRange ? BO_LE : BO_GT, ToExp, ToTy,
539  /*RetTy=*/nullptr);
540 
541  return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
543  }
544 
545  // Recover the QualType of an APSInt.
546  // TODO: Refactor to put elsewhere
547  static inline QualType getAPSIntType(ASTContext &Ctx,
548  const llvm::APSInt &Int) {
549  return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
550  }
551 
552  // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
553  static inline std::pair<llvm::APSInt, QualType>
554  fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) {
555  llvm::APSInt NewInt;
556 
557  // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
558  // but the former is not available in Clang. Instead, extend the APSInt
559  // directly.
560  if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) {
561  NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
562  } else
563  NewInt = Int;
564 
565  return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
566  }
567 
568  // Perform implicit type conversion on binary symbolic expressions.
569  // May modify all input parameters.
570  // TODO: Refactor to use built-in conversion functions
571  static inline void doTypeConversion(llvm::SMTSolverRef &Solver,
572  ASTContext &Ctx, llvm::SMTExprRef &LHS,
573  llvm::SMTExprRef &RHS, QualType &LTy,
574  QualType &RTy) {
575  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
576 
577  // Perform type conversion
578  if ((LTy->isIntegralOrEnumerationType() &&
579  RTy->isIntegralOrEnumerationType()) &&
580  (LTy->isArithmeticType() && RTy->isArithmeticType())) {
581  SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(
582  Solver, Ctx, LHS, LTy, RHS, RTy);
583  return;
584  }
585 
586  if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
587  SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
588  Solver, Ctx, LHS, LTy, RHS, RTy);
589  return;
590  }
591 
592  if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
593  (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
594  (LTy->isReferenceType() || RTy->isReferenceType())) {
595  // TODO: Refactor to Sema::FindCompositePointerType(), and
596  // Sema::CheckCompareOperands().
597 
598  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
599  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
600 
601  // Cast the non-pointer type to the pointer type.
602  // TODO: Be more strict about this.
603  if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
604  (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
605  (LTy->isReferenceType() ^ RTy->isReferenceType())) {
606  if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
607  LTy->isReferenceType()) {
608  LHS = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
609  LTy = RTy;
610  } else {
611  RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
612  RTy = LTy;
613  }
614  }
615 
616  // Cast the void pointer type to the non-void pointer type.
617  // For void types, this assumes that the casted value is equal to the
618  // value of the original pointer, and does not account for alignment
619  // requirements.
620  if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
621  assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
622  "Pointer types have different bitwidths!");
623  if (RTy->isVoidPointerType())
624  RTy = LTy;
625  else
626  LTy = RTy;
627  }
628 
629  if (LTy == RTy)
630  return;
631  }
632 
633  // Fallback: for the solver, assume that these types don't really matter
634  if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
636  LTy = RTy;
637  return;
638  }
639 
640  // TODO: Refine behavior for invalid type casts
641  }
642 
643  // Perform implicit integer type conversion.
644  // May modify all input parameters.
645  // TODO: Refactor to use Sema::handleIntegerConversion()
646  template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
647  QualType, uint64_t, QualType, uint64_t)>
648  static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver,
649  ASTContext &Ctx, T &LHS, QualType &LTy,
650  T &RHS, QualType &RTy) {
651  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
652  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
653 
654  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
655  // Always perform integer promotion before checking type equality.
656  // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
657  if (LTy->isPromotableIntegerType()) {
658  QualType NewTy = Ctx.getPromotedIntegerType(LTy);
659  uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
660  LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
661  LTy = NewTy;
662  LBitWidth = NewBitWidth;
663  }
664  if (RTy->isPromotableIntegerType()) {
665  QualType NewTy = Ctx.getPromotedIntegerType(RTy);
666  uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
667  RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);
668  RTy = NewTy;
669  RBitWidth = NewBitWidth;
670  }
671 
672  if (LTy == RTy)
673  return;
674 
675  // Perform integer type conversion
676  // Note: Safe to skip updating bitwidth because this must terminate
677  bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
678  bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
679 
680  int order = Ctx.getIntegerTypeOrder(LTy, RTy);
681  if (isLSignedTy == isRSignedTy) {
682  // Same signedness; use the higher-ranked type
683  if (order == 1) {
684  RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
685  RTy = LTy;
686  } else {
687  LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
688  LTy = RTy;
689  }
690  } else if (order != (isLSignedTy ? 1 : -1)) {
691  // The unsigned type has greater than or equal rank to the
692  // signed type, so use the unsigned type
693  if (isRSignedTy) {
694  RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
695  RTy = LTy;
696  } else {
697  LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
698  LTy = RTy;
699  }
700  } else if (LBitWidth != RBitWidth) {
701  // The two types are different widths; if we are here, that
702  // means the signed type is larger than the unsigned type, so
703  // use the signed type.
704  if (isLSignedTy) {
705  RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
706  RTy = LTy;
707  } else {
708  LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
709  LTy = RTy;
710  }
711  } else {
712  // The signed type is higher-ranked than the unsigned type,
713  // but isn't actually any bigger (like unsigned int and long
714  // on most 32-bit systems). Use the unsigned type corresponding
715  // to the signed type.
716  QualType NewTy =
717  Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
718  RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
719  RTy = NewTy;
720  LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
721  LTy = NewTy;
722  }
723  }
724 
725  // Perform implicit floating-point type conversion.
726  // May modify all input parameters.
727  // TODO: Refactor to use Sema::handleFloatConversion()
728  template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
729  QualType, uint64_t, QualType, uint64_t)>
730  static inline void
731  doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
732  QualType &LTy, T &RHS, QualType &RTy) {
733  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
734  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
735 
736  // Perform float-point type promotion
737  if (!LTy->isRealFloatingType()) {
738  LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
739  LTy = RTy;
740  LBitWidth = RBitWidth;
741  }
742  if (!RTy->isRealFloatingType()) {
743  RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
744  RTy = LTy;
745  RBitWidth = LBitWidth;
746  }
747 
748  if (LTy == RTy)
749  return;
750 
751  // If we have two real floating types, convert the smaller operand to the
752  // bigger result
753  // Note: Safe to skip updating bitwidth because this must terminate
754  int order = Ctx.getFloatingTypeOrder(LTy, RTy);
755  if (order > 0) {
756  RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
757  RTy = LTy;
758  } else if (order == 0) {
759  LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
760  LTy = RTy;
761  } else {
762  llvm_unreachable("Unsupported floating-point type cast!");
763  }
764  }
765 };
766 } // namespace ento
767 } // namespace clang
768 
769 #endif
clang::ASTContext::getIntegerTypeOrder
int getIntegerTypeOrder(QualType LHS, QualType RHS) const
Return the highest ranked integer type, see C99 6.3.1.8p1.
Definition: ASTContext.cpp:6575
clang::ento::SMTConv::doFloatTypeConversion
static void doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy)
Definition: SMTConv.h:731
clang::Type::isBlockPointerType
bool isBlockPointerType() const
Definition: Type.h:6681
clang::Type::isVoidPointerType
bool isVoidPointerType() const
Definition: Type.cpp:589
clang::ento::SMTConv::getAPSIntType
static QualType getAPSIntType(ASTContext &Ctx, const llvm::APSInt &Int)
Definition: SMTConv.h:547
clang::BinaryOperator::isLogicalOp
bool isLogicalOp() const
Definition: Expr.h:3936
clang::QualType
A (possibly-)qualified type.
Definition: Type.h:673
clang::ASTContext::getFloatTypeSemantics
const llvm::fltSemantics & getFloatTypeSemantics(QualType T) const
Return the APFloat 'semantics' for the specified scalar floating point type.
Definition: ASTContext.cpp:1703
clang::QualType::getCanonicalType
QualType getCanonicalType() const
Definition: Type.h:6464
clang::ento::BinarySymExpr
Represents a symbolic expression involving a binary operator.
Definition: SymbolManager.h:313
clang::ento::SMTConv::getBinExpr
static llvm::SMTExprRef getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &LHS, QualType LTy, BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, QualType RTy, QualType *RetTy)
Definition: SMTConv.h:346
SymbolManager.h
clang::Type::isRealFloatingType
bool isRealFloatingType() const
Floating point categories.
Definition: Type.cpp:2113
clang::ento::SMTConv::mkSort
static llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, const QualType &Ty, unsigned BitWidth)
Definition: SMTConv.h:27
clang::ento::SMTConv
Definition: SMTConv.h:24
clang::ento::SMTConv::getRangeExpr
static llvm::SMTExprRef getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
Definition: SMTConv.h:508
clang::ento::SMTConv::getZeroExpr
static llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType Ty, bool Assumption)
Definition: SMTConv.h:477
clang::Type::isPromotableIntegerType
bool isPromotableIntegerType() const
More type predicates useful for type checking/promotion.
Definition: Type.cpp:2737
clang::ento::SMTConv::fromFloatBinOp
static llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS)
Construct an SMTSolverRef from a floating-point binary operator.
Definition: SMTConv.h:201
clang::ento::SymbolCast
Represents a cast expression.
Definition: SymbolManager.h:264
clang::ento::SMTConv::fromCast
static llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &Exp, QualType ToTy, uint64_t ToBitWidth, QualType FromTy, uint64_t FromBitWidth)
Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy, and their bit widths.
Definition: SMTConv.h:260
size_t
__SIZE_TYPE__ size_t
The unsigned integer type of the result of the sizeof operator.
Definition: opencl-c-base.h:102
APSInt
llvm::APSInt APSInt
Definition: ByteCodeEmitter.cpp:19
clang::Type::isReferenceType
bool isReferenceType() const
Definition: Type.h:6685
V
#define V(N, I)
Definition: ASTContext.h:3121
clang::ento::SMTConv::fromUnOp
static llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef &Exp)
Constructs an SMTSolverRef from an unary operator.
Definition: SMTConv.h:39
clang::Type::isSignedIntegerOrEnumerationType
bool isSignedIntegerOrEnumerationType() const
Determines whether this is an integer type that is signed or an enumeration types whose underlying ty...
Definition: Type.cpp:2025
clang::ento::SymExpr::getType
virtual QualType getType() const =0
clang::Type::isNullPtrType
bool isNullPtrType() const
Definition: Type.h:6981
clang::ento::SMTConv::getCastExpr
static llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType FromTy, QualType ToTy)
Definition: SMTConv.h:335
clang::ASTContext
Holds long-lived AST nodes (such as types and decls) that can be referred to throughout the semantic ...
Definition: ASTContext.h:212
clang::ASTContext::getFloatingTypeOrder
int getFloatingTypeOrder(QualType LHS, QualType RHS) const
Compare the rank of the two specified floating point types, ignoring the domain of the type (i....
Definition: ASTContext.cpp:6388
clang::ento::SymExpr
Symbolic value.
Definition: SymExpr.h:29
clang::ento::BinarySymExpr::getOpcode
BinaryOperator::Opcode getOpcode() const
Definition: SymbolManager.h:332
clang::ASTContext::getTypeSize
uint64_t getTypeSize(QualType T) const
Return the size of the specified (complete) type T, in bits.
Definition: ASTContext.h:2245
Expr.h
llvm::SmallString< 16 >
clang::ento::SMTConv::doIntTypeConversion
static void doIntTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy)
Definition: SMTConv.h:648
clang::interp::Zero
bool Zero(InterpState &S, CodePtr OpPC)
Definition: Interp.h:814
clang::ASTContext::getIntTypeForBitwidth
QualType getIntTypeForBitwidth(unsigned DestWidth, unsigned Signed) const
getIntTypeForBitwidth - sets integer QualTy according to specified details: bitwidth,...
Definition: ASTContext.cpp:11266
clang::ASTContext::getPromotedIntegerType
QualType getPromotedIntegerType(QualType PromotableType) const
Return the type that PromotableType will promote to: C99 6.3.1.1p2, assuming that PromotableType is a...
Definition: ASTContext.cpp:6503
clang::ento::APSIntType
A record of the "type" of an APSInt, used for conversions.
Definition: APSIntType.h:19
clang::interp::InRange
bool InRange(InterpState &S, CodePtr OpPC)
Definition: Interp.h:266
clang::ento::SymbolData::getKindStr
virtual StringRef getKindStr() const =0
Get a string representation of the kind of the region.
clang::Type::isObjCObjectPointerType
bool isObjCObjectPointerType() const
Definition: Type.h:6795
clang::ASTContext::getCorrespondingUnsignedType
QualType getCorrespondingUnsignedType(QualType T) const
Definition: ASTContext.cpp:10235
clang::Type::isArithmeticType
bool isArithmeticType() const
Definition: Type.cpp:2128
clang::ento::BinarySymExprImpl
Template implementation for all binary symbolic expressions.
Definition: SymbolManager.h:360
clang::ento::SMTConv::castAPSInt
static llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver, const llvm::APSInt &V, QualType ToTy, uint64_t ToWidth, QualType FromTy, uint64_t FromWidth)
Definition: SMTConv.h:313
clang::QualType::isNull
bool isNull() const
Return true if this QualType doesn't point to a type yet.
Definition: Type.h:738
clang::BinaryOperator::isComparisonOp
bool isComparisonOp() const
Definition: Expr.h:3903
clang::ento::SMTConv::fromBinOp
static llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, bool isSigned)
Construct an SMTSolverRef from a binary operator.
Definition: SMTConv.h:90
clang::UnaryOperatorKind
UnaryOperatorKind
Definition: OperationKinds.h:30
APSIntType.h
clang::ento::SMTConv::fromFloatSpecialBinOp
static llvm::SMTExprRef fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::APFloat::fltCategory &RHS)
Construct an SMTSolverRef from a special floating-point binary operator.
Definition: SMTConv.h:169
clang::BinaryOperatorKind
BinaryOperatorKind
Definition: OperationKinds.h:25
clang::ento::SymbolData::getSymbolID
SymbolID getSymbolID() const
Definition: SymExpr.h:132
clang::ento::SMTConv::fromNBinOp
static llvm::SMTExprRef fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op, const std::vector< llvm::SMTExprRef > &ASTs)
Construct an SMTSolverRef from a n-ary binary operator.
Definition: SMTConv.h:75
clang::Type::isBooleanType
bool isBooleanType() const
Definition: Type.h:7072
clang::Builtin::ID
ID
Definition: Builtins.h:48
clang
Definition: CalledOnceCheck.h:17
clang::Type::isAnyPointerType
bool isAnyPointerType() const
Definition: Type.h:6677
clang::ento::SymbolData
A symbol representing data which can be stored in a memory location (region).
Definition: SymExpr.h:116
clang::ento::APSIntType::convert
llvm::APSInt convert(const llvm::APSInt &Value) const LLVM_READONLY
Convert and return a new APSInt with the given value, but this type's bit width and signedness.
Definition: APSIntType.h:48
unsigned
clang::ASTContext::getPointerDiffType
QualType getPointerDiffType() const
Return the unique type for "ptrdiff_t" (C99 7.17) defined in <stddef.h>.
Definition: ASTContext.cpp:5756
clang::ento::SMTConv::getSymExpr
static llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy, bool *hasComparison)
Definition: SMTConv.h:422
clang::ento::SMTConv::fromFloatUnOp
static llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef &Exp)
Constructs an SMTSolverRef from a floating-point unary operator.
Definition: SMTConv.h:58
clang::ento::SMTConv::getExpr
static llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy=nullptr, bool *hasComparison=nullptr)
Definition: SMTConv.h:465
clang::ento::SMTConv::fixAPSInt
static std::pair< llvm::APSInt, QualType > fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int)
Definition: SMTConv.h:554
clang::ento::SMTConv::fromData
static llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym)
Construct an SMTSolverRef from a SymbolData.
Definition: SMTConv.h:323
clang::ASTContext::BoolTy
CanQualType BoolTy
Definition: ASTContext.h:1076
clang::ento::SMTConv::getSymBinExpr
static llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const BinarySymExpr *BSE, bool *hasComparison, QualType *RetTy)
Definition: SMTConv.h:381
clang::ento::SMTConv::doTypeConversion
static void doTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, llvm::SMTExprRef &LHS, llvm::SMTExprRef &RHS, QualType &LTy, QualType &RTy)
Definition: SMTConv.h:571
clang::Type::isIntegralOrEnumerationType
bool isIntegralOrEnumerationType() const
Determine whether this type is an integral or enumeration type.
Definition: Type.h:7059
clang::ento::ObjKind::OS
@ OS
Indicates that the tracking object is a descendant of a referenced-counted OSObject,...