1 //== SMTConv.h --------------------------------------------------*- C++ -*--==//
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
7 //===----------------------------------------------------------------------===//
9 // This file defines a set of functions to create SMT expressions
11 //===----------------------------------------------------------------------===//
13 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
14 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
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"
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();
32 if (Ty->isRealFloatingType())
33 return Solver->getFloatSort(BitWidth);
35 return Solver->getBitvectorSort(BitWidth);
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) {
44 return Solver->mkBVNeg(Exp);
47 return Solver->mkBVNot(Exp);
50 return Solver->mkNot(Exp);
54 llvm_unreachable("Unimplemented opcode");
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) {
63 return Solver->mkFPNeg(Exp);
66 return fromUnOp(Solver, Op, Exp);
70 llvm_unreachable("Unimplemented opcode");
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());
79 if (Op != BO_LAnd && Op != BO_LOr)
80 llvm_unreachable("Unimplemented opcode");
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]);
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,
95 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
96 "AST's must have the same sort!");
99 // Multiplicative operators
101 return Solver->mkBVMul(LHS, RHS);
104 return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);
107 return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);
109 // Additive operators
111 return Solver->mkBVAdd(LHS, RHS);
114 return Solver->mkBVSub(LHS, RHS);
116 // Bitwise shift operators
118 return Solver->mkBVShl(LHS, RHS);
121 return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);
123 // Relational operators
125 return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);
128 return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);
131 return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);
134 return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);
136 // Equality operators
138 return Solver->mkEqual(LHS, RHS);
141 return fromUnOp(Solver, UO_LNot,
142 fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned));
146 return Solver->mkBVAnd(LHS, RHS);
149 return Solver->mkBVXor(LHS, RHS);
152 return Solver->mkBVOr(LHS, RHS);
156 return Solver->mkAnd(LHS, RHS);
159 return Solver->mkOr(LHS, RHS);
163 llvm_unreachable("Unimplemented opcode");
166 /// Construct an SMTSolverRef from a special floating-point binary
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) {
173 // Equality operators
176 case llvm::APFloat::fcInfinity:
177 return Solver->mkFPIsInfinite(LHS);
179 case llvm::APFloat::fcNaN:
180 return Solver->mkFPIsNaN(LHS);
182 case llvm::APFloat::fcNormal:
183 return Solver->mkFPIsNormal(LHS);
185 case llvm::APFloat::fcZero:
186 return Solver->mkFPIsZero(LHS);
191 return fromFloatUnOp(Solver, UO_LNot,
192 fromFloatSpecialBinOp(Solver, LHS, BO_EQ, RHS));
197 llvm_unreachable("Unimplemented opcode");
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!");
209 // Multiplicative operators
211 return Solver->mkFPMul(LHS, RHS);
214 return Solver->mkFPDiv(LHS, RHS);
217 return Solver->mkFPRem(LHS, RHS);
219 // Additive operators
221 return Solver->mkFPAdd(LHS, RHS);
224 return Solver->mkFPSub(LHS, RHS);
226 // Relational operators
228 return Solver->mkFPLt(LHS, RHS);
231 return Solver->mkFPGt(LHS, RHS);
234 return Solver->mkFPLe(LHS, RHS);
237 return Solver->mkFPGe(LHS, RHS);
239 // Equality operators
241 return Solver->mkFPEqual(LHS, RHS);
244 return fromFloatUnOp(Solver, UO_LNot,
245 fromFloatBinOp(Solver, LHS, BO_EQ, RHS));
250 return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false);
255 llvm_unreachable("Unimplemented opcode");
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,
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())) {
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));
278 if (ToBitWidth > FromBitWidth)
279 return FromTy->isSignedIntegerOrEnumerationType()
280 ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
281 : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
283 if (ToBitWidth < FromBitWidth)
284 return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
286 // Both are bitvectors with the same width, ignore the type cast
290 if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
291 if (ToBitWidth != FromBitWidth)
292 return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
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);
304 if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
305 return ToTy->isSignedIntegerOrEnumerationType()
306 ? Solver->mkFPtoSBV(Exp, ToBitWidth)
307 : Solver->mkFPtoUBV(Exp, ToBitWidth);
309 llvm_unreachable("Unsupported explicit type cast!");
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);
321 /// Construct an SMTSolverRef from a SymbolData.
322 static inline llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver,
323 const SymbolID ID, const QualType &Ty,
325 llvm::Twine Name = "$" + llvm::Twine(ID);
326 return Solver->mkSymbol(Name.str().c_str(), mkSort(Solver, Ty, BitWidth));
329 // Wrapper to generate SMTSolverRef from SymbolCast data.
330 static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,
332 const llvm::SMTExprRef &Exp,
333 QualType FromTy, QualType ToTy) {
334 return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
335 Ctx.getTypeSize(FromTy));
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);
349 // Update the return type parameter if the output type has changed.
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)) {
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();
368 return LTy->isRealFloatingType()
369 ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS)
370 : fromBinOp(Solver, NewLHS, Op, NewRHS,
371 LTy->isSignedIntegerOrEnumerationType());
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,
378 const BinarySymExpr *BSE,
382 BinaryOperator::Opcode Op = BSE->getOpcode();
384 if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
385 llvm::SMTExprRef LHS =
386 getSymExpr(Solver, Ctx, SIE->getLHS(), <y, 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);
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);
404 if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
405 llvm::SMTExprRef LHS =
406 getSymExpr(Solver, Ctx, SSM->getLHS(), <y, hasComparison);
407 llvm::SMTExprRef RHS =
408 getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
409 return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
412 llvm_unreachable("Unsupported BinarySymExpr type!");
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,
420 bool *hasComparison) {
421 if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
423 *RetTy = Sym->getType();
425 return fromData(Solver, SD->getSymbolID(), Sym->getType(),
426 Ctx.getTypeSize(Sym->getType()));
429 if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
431 *RetTy = Sym->getType();
434 llvm::SMTExprRef Exp =
435 getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
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)
441 *hasComparison = false;
442 return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
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.
450 *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
454 llvm_unreachable("Unsupported SymbolRef type!");
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) {
466 *hasComparison = false;
469 return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
472 // Generate an SMTSolverRef that compares the expression to zero.
473 static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver,
475 const llvm::SMTExprRef &Exp,
476 QualType Ty, bool Assumption) {
477 if (Ty->isRealFloatingType()) {
479 llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
480 return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
481 Solver->mkFloat(Zero));
484 if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
485 Ty->isBlockPointerType() || Ty->isReferenceType()) {
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;
493 Solver, Exp, Assumption ? BO_EQ : BO_NE,
494 Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
498 llvm_unreachable("Unsupported type for zero value!");
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
508 llvm::APSInt NewFromInt;
509 std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
510 llvm::SMTExprRef FromExp =
511 Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
515 llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
517 // Construct single (in)equality
519 return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
520 FromExp, FromTy, /*RetTy=*/nullptr);
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!");
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,
537 return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
538 SymTy->isSignedIntegerOrEnumerationType());
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());
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) {
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
556 if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) {
557 NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
561 return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
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 <y,
571 assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
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);
582 if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
583 SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
584 Solver, Ctx, LHS, LTy, RHS, RTy);
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().
594 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
595 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
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);
607 RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
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
616 if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
617 assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
618 "Pointer types have different bitwidths!");
619 if (RTy->isVoidPointerType())
629 // Fallback: for the solver, assume that these types don't really matter
630 if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
631 (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
636 // TODO: Refine behavior for invalid type casts
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 <y,
646 T &RHS, QualType &RTy) {
647 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
648 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
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);
658 LBitWidth = NewBitWidth;
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);
665 RBitWidth = NewBitWidth;
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();
676 int order = Ctx.getIntegerTypeOrder(LTy, RTy);
677 if (isLSignedTy == isRSignedTy) {
678 // Same signedness; use the higher-ranked type
680 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
683 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
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
690 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
693 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
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.
701 RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
704 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
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.
713 Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
714 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
716 LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
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)>
727 doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
728 QualType <y, T &RHS, QualType &RTy) {
729 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
730 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
732 // Perform float-point type promotion
733 if (!LTy->isRealFloatingType()) {
734 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
736 LBitWidth = RBitWidth;
738 if (!RTy->isRealFloatingType()) {
739 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
741 RBitWidth = LBitWidth;
747 // If we have two real floating types, convert the smaller operand to the
749 // Note: Safe to skip updating bitwidth because this must terminate
750 int order = Ctx.getFloatingTypeOrder(LTy, RTy);
752 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
754 } else if (order == 0) {
755 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
758 llvm_unreachable("Unsupported floating-point type cast!");