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"
17 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
18 #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.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 fromData(llvm::SMTSolverRef &Solver,
323                                           const SymbolID ID, const QualType &Ty,
324                                           uint64_t BitWidth) {
325     llvm::Twine Name = "$" + llvm::Twine(ID);
326     return Solver->mkSymbol(Name.str().c_str(), mkSort(Solver, Ty, BitWidth));
327   }
328 
329   // Wrapper to generate SMTSolverRef from SymbolCast data.
330   static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,
331                                              ASTContext &Ctx,
332                                              const llvm::SMTExprRef &Exp,
333                                              QualType FromTy, QualType ToTy) {
334     return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
335                     Ctx.getTypeSize(FromTy));
336   }
337 
338   // Wrapper to generate SMTSolverRef from unpacked binary symbolic
339   // expression. Sets the RetTy parameter. See getSMTSolverRef().
340   static inline llvm::SMTExprRef
341   getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
342              const llvm::SMTExprRef &LHS, QualType LTy,
343              BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS,
344              QualType RTy, QualType *RetTy) {
345     llvm::SMTExprRef NewLHS = LHS;
346     llvm::SMTExprRef NewRHS = RHS;
347     doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
348 
349     // Update the return type parameter if the output type has changed.
350     if (RetTy) {
351       // A boolean result can be represented as an integer type in C/C++, but at
352       // this point we only care about the SMT sorts. Set it as a boolean type
353       // to avoid subsequent SMT errors.
354       if (BinaryOperator::isComparisonOp(Op) ||
355           BinaryOperator::isLogicalOp(Op)) {
356         *RetTy = Ctx.BoolTy;
357       } else {
358         *RetTy = LTy;
359       }
360 
361       // If the two operands are pointers and the operation is a subtraction,
362       // the result is of type ptrdiff_t, which is signed
363       if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) {
364         *RetTy = Ctx.getPointerDiffType();
365       }
366     }
367 
368     return LTy->isRealFloatingType()
369                ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS)
370                : fromBinOp(Solver, NewLHS, Op, NewRHS,
371                            LTy->isSignedIntegerOrEnumerationType());
372   }
373 
374   // Wrapper to generate SMTSolverRef from BinarySymExpr.
375   // Sets the hasComparison and RetTy parameters. See getSMTSolverRef().
376   static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver,
377                                                ASTContext &Ctx,
378                                                const BinarySymExpr *BSE,
379                                                bool *hasComparison,
380                                                QualType *RetTy) {
381     QualType LTy, RTy;
382     BinaryOperator::Opcode Op = BSE->getOpcode();
383 
384     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
385       llvm::SMTExprRef LHS =
386           getSymExpr(Solver, Ctx, SIE->getLHS(), &LTy, hasComparison);
387       llvm::APSInt NewRInt;
388       std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
389       llvm::SMTExprRef RHS =
390           Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
391       return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
392     }
393 
394     if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
395       llvm::APSInt NewLInt;
396       std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
397       llvm::SMTExprRef LHS =
398           Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
399       llvm::SMTExprRef RHS =
400           getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
401       return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
402     }
403 
404     if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
405       llvm::SMTExprRef LHS =
406           getSymExpr(Solver, Ctx, SSM->getLHS(), &LTy, hasComparison);
407       llvm::SMTExprRef RHS =
408           getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
409       return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
410     }
411 
412     llvm_unreachable("Unsupported BinarySymExpr type!");
413   }
414 
415   // Recursive implementation to unpack and generate symbolic expression.
416   // Sets the hasComparison and RetTy parameters. See getExpr().
417   static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
418                                             ASTContext &Ctx, SymbolRef Sym,
419                                             QualType *RetTy,
420                                             bool *hasComparison) {
421     if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
422       if (RetTy)
423         *RetTy = Sym->getType();
424 
425       return fromData(Solver, SD->getSymbolID(), Sym->getType(),
426                       Ctx.getTypeSize(Sym->getType()));
427     }
428 
429     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
430       if (RetTy)
431         *RetTy = Sym->getType();
432 
433       QualType FromTy;
434       llvm::SMTExprRef Exp =
435           getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
436 
437       // Casting an expression with a comparison invalidates it. Note that this
438       // must occur after the recursive call above.
439       // e.g. (signed char) (x > 0)
440       if (hasComparison)
441         *hasComparison = false;
442       return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
443     }
444 
445     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
446       llvm::SMTExprRef Exp =
447           getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
448       // Set the hasComparison parameter, in post-order traversal order.
449       if (hasComparison)
450         *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
451       return Exp;
452     }
453 
454     llvm_unreachable("Unsupported SymbolRef type!");
455   }
456 
457   // Generate an SMTSolverRef that represents the given symbolic expression.
458   // Sets the hasComparison parameter if the expression has a comparison
459   // operator. Sets the RetTy parameter to the final return type after
460   // promotions and casts.
461   static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
462                                          ASTContext &Ctx, SymbolRef Sym,
463                                          QualType *RetTy = nullptr,
464                                          bool *hasComparison = nullptr) {
465     if (hasComparison) {
466       *hasComparison = false;
467     }
468 
469     return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
470   }
471 
472   // Generate an SMTSolverRef that compares the expression to zero.
473   static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver,
474                                              ASTContext &Ctx,
475                                              const llvm::SMTExprRef &Exp,
476                                              QualType Ty, bool Assumption) {
477     if (Ty->isRealFloatingType()) {
478       llvm::APFloat Zero =
479           llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
480       return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
481                             Solver->mkFloat(Zero));
482     }
483 
484     if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
485         Ty->isBlockPointerType() || Ty->isReferenceType()) {
486 
487       // Skip explicit comparison for boolean types
488       bool isSigned = Ty->isSignedIntegerOrEnumerationType();
489       if (Ty->isBooleanType())
490         return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
491 
492       return fromBinOp(
493           Solver, Exp, Assumption ? BO_EQ : BO_NE,
494           Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
495           isSigned);
496     }
497 
498     llvm_unreachable("Unsupported type for zero value!");
499   }
500 
501   // Wrapper to generate SMTSolverRef from a range. If From == To, an
502   // equality will be created instead.
503   static inline llvm::SMTExprRef
504   getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
505                const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) {
506     // Convert lower bound
507     QualType FromTy;
508     llvm::APSInt NewFromInt;
509     std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
510     llvm::SMTExprRef FromExp =
511         Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
512 
513     // Convert symbol
514     QualType SymTy;
515     llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
516 
517     // Construct single (in)equality
518     if (From == To)
519       return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
520                         FromExp, FromTy, /*RetTy=*/nullptr);
521 
522     QualType ToTy;
523     llvm::APSInt NewToInt;
524     std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
525     llvm::SMTExprRef ToExp =
526         Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
527     assert(FromTy == ToTy && "Range values have different types!");
528 
529     // Construct two (in)equalities, and a logical and/or
530     llvm::SMTExprRef LHS =
531         getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
532                    FromTy, /*RetTy=*/nullptr);
533     llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
534                                       InRange ? BO_LE : BO_GT, ToExp, ToTy,
535                                       /*RetTy=*/nullptr);
536 
537     return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
538                      SymTy->isSignedIntegerOrEnumerationType());
539   }
540 
541   // Recover the QualType of an APSInt.
542   // TODO: Refactor to put elsewhere
543   static inline QualType getAPSIntType(ASTContext &Ctx,
544                                        const llvm::APSInt &Int) {
545     return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
546   }
547 
548   // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
549   static inline std::pair<llvm::APSInt, QualType>
550   fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) {
551     llvm::APSInt NewInt;
552 
553     // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
554     // but the former is not available in Clang. Instead, extend the APSInt
555     // directly.
556     if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) {
557       NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
558     } else
559       NewInt = Int;
560 
561     return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
562   }
563 
564   // Perform implicit type conversion on binary symbolic expressions.
565   // May modify all input parameters.
566   // TODO: Refactor to use built-in conversion functions
567   static inline void doTypeConversion(llvm::SMTSolverRef &Solver,
568                                       ASTContext &Ctx, llvm::SMTExprRef &LHS,
569                                       llvm::SMTExprRef &RHS, QualType &LTy,
570                                       QualType &RTy) {
571     assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
572 
573     // Perform type conversion
574     if ((LTy->isIntegralOrEnumerationType() &&
575          RTy->isIntegralOrEnumerationType()) &&
576         (LTy->isArithmeticType() && RTy->isArithmeticType())) {
577       SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(
578           Solver, Ctx, LHS, LTy, RHS, RTy);
579       return;
580     }
581 
582     if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
583       SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
584           Solver, Ctx, LHS, LTy, RHS, RTy);
585       return;
586     }
587 
588     if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
589         (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
590         (LTy->isReferenceType() || RTy->isReferenceType())) {
591       // TODO: Refactor to Sema::FindCompositePointerType(), and
592       // Sema::CheckCompareOperands().
593 
594       uint64_t LBitWidth = Ctx.getTypeSize(LTy);
595       uint64_t RBitWidth = Ctx.getTypeSize(RTy);
596 
597       // Cast the non-pointer type to the pointer type.
598       // TODO: Be more strict about this.
599       if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
600           (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
601           (LTy->isReferenceType() ^ RTy->isReferenceType())) {
602         if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
603             LTy->isReferenceType()) {
604           LHS = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
605           LTy = RTy;
606         } else {
607           RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
608           RTy = LTy;
609         }
610       }
611 
612       // Cast the void pointer type to the non-void pointer type.
613       // For void types, this assumes that the casted value is equal to the
614       // value of the original pointer, and does not account for alignment
615       // requirements.
616       if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
617         assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
618                "Pointer types have different bitwidths!");
619         if (RTy->isVoidPointerType())
620           RTy = LTy;
621         else
622           LTy = RTy;
623       }
624 
625       if (LTy == RTy)
626         return;
627     }
628 
629     // Fallback: for the solver, assume that these types don't really matter
630     if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
631         (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
632       LTy = RTy;
633       return;
634     }
635 
636     // TODO: Refine behavior for invalid type casts
637   }
638 
639   // Perform implicit integer type conversion.
640   // May modify all input parameters.
641   // TODO: Refactor to use Sema::handleIntegerConversion()
642   template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
643                                     QualType, uint64_t, QualType, uint64_t)>
644   static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver,
645                                          ASTContext &Ctx, T &LHS, QualType &LTy,
646                                          T &RHS, QualType &RTy) {
647     uint64_t LBitWidth = Ctx.getTypeSize(LTy);
648     uint64_t RBitWidth = Ctx.getTypeSize(RTy);
649 
650     assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
651     // Always perform integer promotion before checking type equality.
652     // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
653     if (LTy->isPromotableIntegerType()) {
654       QualType NewTy = Ctx.getPromotedIntegerType(LTy);
655       uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
656       LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
657       LTy = NewTy;
658       LBitWidth = NewBitWidth;
659     }
660     if (RTy->isPromotableIntegerType()) {
661       QualType NewTy = Ctx.getPromotedIntegerType(RTy);
662       uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
663       RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);
664       RTy = NewTy;
665       RBitWidth = NewBitWidth;
666     }
667 
668     if (LTy == RTy)
669       return;
670 
671     // Perform integer type conversion
672     // Note: Safe to skip updating bitwidth because this must terminate
673     bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
674     bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
675 
676     int order = Ctx.getIntegerTypeOrder(LTy, RTy);
677     if (isLSignedTy == isRSignedTy) {
678       // Same signedness; use the higher-ranked type
679       if (order == 1) {
680         RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
681         RTy = LTy;
682       } else {
683         LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
684         LTy = RTy;
685       }
686     } else if (order != (isLSignedTy ? 1 : -1)) {
687       // The unsigned type has greater than or equal rank to the
688       // signed type, so use the unsigned type
689       if (isRSignedTy) {
690         RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
691         RTy = LTy;
692       } else {
693         LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
694         LTy = RTy;
695       }
696     } else if (LBitWidth != RBitWidth) {
697       // The two types are different widths; if we are here, that
698       // means the signed type is larger than the unsigned type, so
699       // use the signed type.
700       if (isLSignedTy) {
701         RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
702         RTy = LTy;
703       } else {
704         LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
705         LTy = RTy;
706       }
707     } else {
708       // The signed type is higher-ranked than the unsigned type,
709       // but isn't actually any bigger (like unsigned int and long
710       // on most 32-bit systems).  Use the unsigned type corresponding
711       // to the signed type.
712       QualType NewTy =
713           Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
714       RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
715       RTy = NewTy;
716       LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
717       LTy = NewTy;
718     }
719   }
720 
721   // Perform implicit floating-point type conversion.
722   // May modify all input parameters.
723   // TODO: Refactor to use Sema::handleFloatConversion()
724   template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
725                                     QualType, uint64_t, QualType, uint64_t)>
726   static inline void
727   doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
728                         QualType &LTy, T &RHS, QualType &RTy) {
729     uint64_t LBitWidth = Ctx.getTypeSize(LTy);
730     uint64_t RBitWidth = Ctx.getTypeSize(RTy);
731 
732     // Perform float-point type promotion
733     if (!LTy->isRealFloatingType()) {
734       LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
735       LTy = RTy;
736       LBitWidth = RBitWidth;
737     }
738     if (!RTy->isRealFloatingType()) {
739       RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
740       RTy = LTy;
741       RBitWidth = LBitWidth;
742     }
743 
744     if (LTy == RTy)
745       return;
746 
747     // If we have two real floating types, convert the smaller operand to the
748     // bigger result
749     // Note: Safe to skip updating bitwidth because this must terminate
750     int order = Ctx.getFloatingTypeOrder(LTy, RTy);
751     if (order > 0) {
752       RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
753       RTy = LTy;
754     } else if (order == 0) {
755       LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
756       LTy = RTy;
757     } else {
758       llvm_unreachable("Unsupported floating-point type cast!");
759     }
760   }
761 };
762 } // namespace ento
763 } // namespace clang
764 
765 #endif
766