clang  15.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 UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
450  if (RetTy)
451  *RetTy = Sym->getType();
452 
453  QualType OperandTy;
454  llvm::SMTExprRef OperandExp =
455  getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
456  llvm::SMTExprRef UnaryExp =
457  fromUnOp(Solver, USE->getOpcode(), OperandExp);
458 
459  // Currently, without the `support-symbolic-integer-casts=true` option,
460  // we do not emit `SymbolCast`s for implicit casts.
461  // One such implicit cast is missing if the operand of the unary operator
462  // has a different type than the unary itself.
463  if (Ctx.getTypeSize(OperandTy) != Ctx.getTypeSize(Sym->getType())) {
464  if (hasComparison)
465  *hasComparison = false;
466  return getCastExpr(Solver, Ctx, UnaryExp, OperandTy, Sym->getType());
467  }
468  return UnaryExp;
469  }
470 
471  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
472  llvm::SMTExprRef Exp =
473  getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
474  // Set the hasComparison parameter, in post-order traversal order.
475  if (hasComparison)
476  *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
477  return Exp;
478  }
479 
480  llvm_unreachable("Unsupported SymbolRef type!");
481  }
482 
483  // Generate an SMTSolverRef that represents the given symbolic expression.
484  // Sets the hasComparison parameter if the expression has a comparison
485  // operator. Sets the RetTy parameter to the final return type after
486  // promotions and casts.
487  static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
488  ASTContext &Ctx, SymbolRef Sym,
489  QualType *RetTy = nullptr,
490  bool *hasComparison = nullptr) {
491  if (hasComparison) {
492  *hasComparison = false;
493  }
494 
495  return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
496  }
497 
498  // Generate an SMTSolverRef that compares the expression to zero.
499  static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver,
500  ASTContext &Ctx,
501  const llvm::SMTExprRef &Exp,
502  QualType Ty, bool Assumption) {
503  if (Ty->isRealFloatingType()) {
504  llvm::APFloat Zero =
505  llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
506  return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
507  Solver->mkFloat(Zero));
508  }
509 
510  if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
511  Ty->isBlockPointerType() || Ty->isReferenceType()) {
512 
513  // Skip explicit comparison for boolean types
514  bool isSigned = Ty->isSignedIntegerOrEnumerationType();
515  if (Ty->isBooleanType())
516  return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
517 
518  return fromBinOp(
519  Solver, Exp, Assumption ? BO_EQ : BO_NE,
520  Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
521  isSigned);
522  }
523 
524  llvm_unreachable("Unsupported type for zero value!");
525  }
526 
527  // Wrapper to generate SMTSolverRef from a range. If From == To, an
528  // equality will be created instead.
529  static inline llvm::SMTExprRef
530  getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
531  const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) {
532  // Convert lower bound
533  QualType FromTy;
534  llvm::APSInt NewFromInt;
535  std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
536  llvm::SMTExprRef FromExp =
537  Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
538 
539  // Convert symbol
540  QualType SymTy;
541  llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
542 
543  // Construct single (in)equality
544  if (From == To)
545  return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
546  FromExp, FromTy, /*RetTy=*/nullptr);
547 
548  QualType ToTy;
549  llvm::APSInt NewToInt;
550  std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
551  llvm::SMTExprRef ToExp =
552  Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
553  assert(FromTy == ToTy && "Range values have different types!");
554 
555  // Construct two (in)equalities, and a logical and/or
556  llvm::SMTExprRef LHS =
557  getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
558  FromTy, /*RetTy=*/nullptr);
559  llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
560  InRange ? BO_LE : BO_GT, ToExp, ToTy,
561  /*RetTy=*/nullptr);
562 
563  return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
565  }
566 
567  // Recover the QualType of an APSInt.
568  // TODO: Refactor to put elsewhere
569  static inline QualType getAPSIntType(ASTContext &Ctx,
570  const llvm::APSInt &Int) {
571  return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
572  }
573 
574  // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
575  static inline std::pair<llvm::APSInt, QualType>
576  fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) {
577  llvm::APSInt NewInt;
578 
579  // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
580  // but the former is not available in Clang. Instead, extend the APSInt
581  // directly.
582  if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) {
583  NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
584  } else
585  NewInt = Int;
586 
587  return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
588  }
589 
590  // Perform implicit type conversion on binary symbolic expressions.
591  // May modify all input parameters.
592  // TODO: Refactor to use built-in conversion functions
593  static inline void doTypeConversion(llvm::SMTSolverRef &Solver,
594  ASTContext &Ctx, llvm::SMTExprRef &LHS,
595  llvm::SMTExprRef &RHS, QualType &LTy,
596  QualType &RTy) {
597  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
598 
599  // Perform type conversion
600  if ((LTy->isIntegralOrEnumerationType() &&
601  RTy->isIntegralOrEnumerationType()) &&
602  (LTy->isArithmeticType() && RTy->isArithmeticType())) {
603  SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(
604  Solver, Ctx, LHS, LTy, RHS, RTy);
605  return;
606  }
607 
608  if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
609  SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
610  Solver, Ctx, LHS, LTy, RHS, RTy);
611  return;
612  }
613 
614  if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
615  (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
616  (LTy->isReferenceType() || RTy->isReferenceType())) {
617  // TODO: Refactor to Sema::FindCompositePointerType(), and
618  // Sema::CheckCompareOperands().
619 
620  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
621  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
622 
623  // Cast the non-pointer type to the pointer type.
624  // TODO: Be more strict about this.
625  if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
626  (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
627  (LTy->isReferenceType() ^ RTy->isReferenceType())) {
628  if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
629  LTy->isReferenceType()) {
630  LHS = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
631  LTy = RTy;
632  } else {
633  RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
634  RTy = LTy;
635  }
636  }
637 
638  // Cast the void pointer type to the non-void pointer type.
639  // For void types, this assumes that the casted value is equal to the
640  // value of the original pointer, and does not account for alignment
641  // requirements.
642  if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
643  assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
644  "Pointer types have different bitwidths!");
645  if (RTy->isVoidPointerType())
646  RTy = LTy;
647  else
648  LTy = RTy;
649  }
650 
651  if (LTy == RTy)
652  return;
653  }
654 
655  // Fallback: for the solver, assume that these types don't really matter
656  if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
658  LTy = RTy;
659  return;
660  }
661 
662  // TODO: Refine behavior for invalid type casts
663  }
664 
665  // Perform implicit integer type conversion.
666  // May modify all input parameters.
667  // TODO: Refactor to use Sema::handleIntegerConversion()
668  template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
670  static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver,
671  ASTContext &Ctx, T &LHS, QualType &LTy,
672  T &RHS, QualType &RTy) {
673  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
674  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
675 
676  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
677  // Always perform integer promotion before checking type equality.
678  // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
679  if (LTy->isPromotableIntegerType()) {
680  QualType NewTy = Ctx.getPromotedIntegerType(LTy);
681  uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
682  LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
683  LTy = NewTy;
684  LBitWidth = NewBitWidth;
685  }
686  if (RTy->isPromotableIntegerType()) {
687  QualType NewTy = Ctx.getPromotedIntegerType(RTy);
688  uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
689  RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);
690  RTy = NewTy;
691  RBitWidth = NewBitWidth;
692  }
693 
694  if (LTy == RTy)
695  return;
696 
697  // Perform integer type conversion
698  // Note: Safe to skip updating bitwidth because this must terminate
699  bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
700  bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
701 
702  int order = Ctx.getIntegerTypeOrder(LTy, RTy);
703  if (isLSignedTy == isRSignedTy) {
704  // Same signedness; use the higher-ranked type
705  if (order == 1) {
706  RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
707  RTy = LTy;
708  } else {
709  LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
710  LTy = RTy;
711  }
712  } else if (order != (isLSignedTy ? 1 : -1)) {
713  // The unsigned type has greater than or equal rank to the
714  // signed type, so use the unsigned type
715  if (isRSignedTy) {
716  RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
717  RTy = LTy;
718  } else {
719  LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
720  LTy = RTy;
721  }
722  } else if (LBitWidth != RBitWidth) {
723  // The two types are different widths; if we are here, that
724  // means the signed type is larger than the unsigned type, so
725  // use the signed type.
726  if (isLSignedTy) {
727  RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
728  RTy = LTy;
729  } else {
730  LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
731  LTy = RTy;
732  }
733  } else {
734  // The signed type is higher-ranked than the unsigned type,
735  // but isn't actually any bigger (like unsigned int and long
736  // on most 32-bit systems). Use the unsigned type corresponding
737  // to the signed type.
738  QualType NewTy =
739  Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
740  RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
741  RTy = NewTy;
742  LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
743  LTy = NewTy;
744  }
745  }
746 
747  // Perform implicit floating-point type conversion.
748  // May modify all input parameters.
749  // TODO: Refactor to use Sema::handleFloatConversion()
750  template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
752  static inline void
753  doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
754  QualType &LTy, T &RHS, QualType &RTy) {
755  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
756  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
757 
758  // Perform float-point type promotion
759  if (!LTy->isRealFloatingType()) {
760  LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
761  LTy = RTy;
762  LBitWidth = RBitWidth;
763  }
764  if (!RTy->isRealFloatingType()) {
765  RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
766  RTy = LTy;
767  RBitWidth = LBitWidth;
768  }
769 
770  if (LTy == RTy)
771  return;
772 
773  // If we have two real floating types, convert the smaller operand to the
774  // bigger result
775  // Note: Safe to skip updating bitwidth because this must terminate
776  int order = Ctx.getFloatingTypeOrder(LTy, RTy);
777  if (order > 0) {
778  RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
779  RTy = LTy;
780  } else if (order == 0) {
781  LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
782  LTy = RTy;
783  } else {
784  llvm_unreachable("Unsupported floating-point type cast!");
785  }
786  }
787 };
788 } // namespace ento
789 } // namespace clang
790 
791 #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:7053
clang::ento::SMTConv::doFloatTypeConversion
static void doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy)
Definition: SMTConv.h:753
clang::Type::isBlockPointerType
bool isBlockPointerType() const
Definition: Type.h:6815
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:569
clang::BinaryOperator::isLogicalOp
bool isLogicalOp() const
Definition: Expr.h:3950
clang::QualType
A (possibly-)qualified type.
Definition: Type.h:731
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:6598
clang::ento::BinarySymExpr
Represents a symbolic expression involving a binary operator.
Definition: SymbolManager.h:377
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:2137
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:530
clang::ento::SMTConv::getZeroExpr
static llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType Ty, bool Assumption)
Definition: SMTConv.h:499
clang::Type::isPromotableIntegerType
bool isPromotableIntegerType() const
More type predicates useful for type checking/promotion.
Definition: Type.cpp:2780
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:278
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
uint64_t
unsigned long uint64_t
Definition: hlsl_basic_types.h:24
size_t
__SIZE_TYPE__ size_t
The unsigned integer type of the result of the sizeof operator.
Definition: opencl-c-base.h:118
APSInt
llvm::APSInt APSInt
Definition: ByteCodeEmitter.cpp:19
clang::Type::isReferenceType
bool isReferenceType() const
Definition: Type.h:6819
V
#define V(N, I)
Definition: ASTContext.h:3176
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:2039
clang::ento::SymExpr::getType
virtual QualType getType() const =0
clang::Type::isNullPtrType
bool isNullPtrType() const
Definition: Type.h:7121
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:208
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:6866
clang::ento::SymExpr
Symbolic value.
Definition: SymExpr.h:29
clang::ento::BinarySymExpr::getOpcode
BinaryOperator::Opcode getOpcode() const
Definition: SymbolManager.h:396
clang::ASTContext::getTypeSize
uint64_t getTypeSize(QualType T) const
Return the size of the specified (complete) type T, in bits.
Definition: ASTContext.h:2285
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:670
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:11752
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:6981
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:6935
clang::ASTContext::getCorrespondingUnsignedType
QualType getCorrespondingUnsignedType(QualType T) const
Definition: ASTContext.cpp:10719
clang::Type::isArithmeticType
bool isArithmeticType() const
Definition: Type.cpp:2152
clang::ento::BinarySymExprImpl
Template implementation for all binary symbolic expressions.
Definition: SymbolManager.h:424
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:796
clang::BinaryOperator::isComparisonOp
bool isComparisonOp() const
Definition: Expr.h:3917
clang::ento::UnarySymExpr
Represents a symbolic expression involving a unary operator.
Definition: SymbolManager.h:328
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:133
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:7212
clang::Builtin::ID
ID
Definition: Builtins.h:52
clang
Definition: CalledOnceCheck.h:17
clang::Type::isAnyPointerType
bool isAnyPointerType() const
Definition: Type.h:6811
clang::ento::SymbolData
A symbol representing data which can be stored in a memory location (region).
Definition: SymExpr.h:117
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:5891
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:487
clang::ento::SMTConv::fixAPSInt
static std::pair< llvm::APSInt, QualType > fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int)
Definition: SMTConv.h:576
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:1097
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:593
clang::Type::isIntegralOrEnumerationType
bool isIntegralOrEnumerationType() const
Determine whether this type is an integral or enumeration type.
Definition: Type.h:7199
clang::ento::ObjKind::OS
@ OS
Indicates that the tracking object is a descendant of a referenced-counted OSObject,...