106f32e7eSjoerg //== SMTConv.h --------------------------------------------------*- C++ -*--==// 206f32e7eSjoerg // 306f32e7eSjoerg // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. 406f32e7eSjoerg // See https://llvm.org/LICENSE.txt for license information. 506f32e7eSjoerg // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception 606f32e7eSjoerg // 706f32e7eSjoerg //===----------------------------------------------------------------------===// 806f32e7eSjoerg // 906f32e7eSjoerg // This file defines a set of functions to create SMT expressions 1006f32e7eSjoerg // 1106f32e7eSjoerg //===----------------------------------------------------------------------===// 1206f32e7eSjoerg 1306f32e7eSjoerg #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H 1406f32e7eSjoerg #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H 1506f32e7eSjoerg 1606f32e7eSjoerg #include "clang/AST/Expr.h" 1706f32e7eSjoerg #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" 1806f32e7eSjoerg #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" 1906f32e7eSjoerg #include "llvm/Support/SMTAPI.h" 2006f32e7eSjoerg 2106f32e7eSjoerg namespace clang { 2206f32e7eSjoerg namespace ento { 2306f32e7eSjoerg 2406f32e7eSjoerg class SMTConv { 2506f32e7eSjoerg public: 2606f32e7eSjoerg // Returns an appropriate sort, given a QualType and it's bit width. mkSort(llvm::SMTSolverRef & Solver,const QualType & Ty,unsigned BitWidth)2706f32e7eSjoerg static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, 2806f32e7eSjoerg const QualType &Ty, unsigned BitWidth) { 2906f32e7eSjoerg if (Ty->isBooleanType()) 3006f32e7eSjoerg return Solver->getBoolSort(); 3106f32e7eSjoerg 3206f32e7eSjoerg if (Ty->isRealFloatingType()) 3306f32e7eSjoerg return Solver->getFloatSort(BitWidth); 3406f32e7eSjoerg 3506f32e7eSjoerg return Solver->getBitvectorSort(BitWidth); 3606f32e7eSjoerg } 3706f32e7eSjoerg 3806f32e7eSjoerg /// Constructs an SMTSolverRef from an unary operator. fromUnOp(llvm::SMTSolverRef & Solver,const UnaryOperator::Opcode Op,const llvm::SMTExprRef & Exp)3906f32e7eSjoerg static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, 4006f32e7eSjoerg const UnaryOperator::Opcode Op, 4106f32e7eSjoerg const llvm::SMTExprRef &Exp) { 4206f32e7eSjoerg switch (Op) { 4306f32e7eSjoerg case UO_Minus: 4406f32e7eSjoerg return Solver->mkBVNeg(Exp); 4506f32e7eSjoerg 4606f32e7eSjoerg case UO_Not: 4706f32e7eSjoerg return Solver->mkBVNot(Exp); 4806f32e7eSjoerg 4906f32e7eSjoerg case UO_LNot: 5006f32e7eSjoerg return Solver->mkNot(Exp); 5106f32e7eSjoerg 5206f32e7eSjoerg default:; 5306f32e7eSjoerg } 5406f32e7eSjoerg llvm_unreachable("Unimplemented opcode"); 5506f32e7eSjoerg } 5606f32e7eSjoerg 5706f32e7eSjoerg /// Constructs an SMTSolverRef from a floating-point unary operator. fromFloatUnOp(llvm::SMTSolverRef & Solver,const UnaryOperator::Opcode Op,const llvm::SMTExprRef & Exp)5806f32e7eSjoerg static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, 5906f32e7eSjoerg const UnaryOperator::Opcode Op, 6006f32e7eSjoerg const llvm::SMTExprRef &Exp) { 6106f32e7eSjoerg switch (Op) { 6206f32e7eSjoerg case UO_Minus: 6306f32e7eSjoerg return Solver->mkFPNeg(Exp); 6406f32e7eSjoerg 6506f32e7eSjoerg case UO_LNot: 6606f32e7eSjoerg return fromUnOp(Solver, Op, Exp); 6706f32e7eSjoerg 6806f32e7eSjoerg default:; 6906f32e7eSjoerg } 7006f32e7eSjoerg llvm_unreachable("Unimplemented opcode"); 7106f32e7eSjoerg } 7206f32e7eSjoerg 7306f32e7eSjoerg /// Construct an SMTSolverRef from a n-ary binary operator. 7406f32e7eSjoerg static inline llvm::SMTExprRef fromNBinOp(llvm::SMTSolverRef & Solver,const BinaryOperator::Opcode Op,const std::vector<llvm::SMTExprRef> & ASTs)7506f32e7eSjoerg fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op, 7606f32e7eSjoerg const std::vector<llvm::SMTExprRef> &ASTs) { 7706f32e7eSjoerg assert(!ASTs.empty()); 7806f32e7eSjoerg 7906f32e7eSjoerg if (Op != BO_LAnd && Op != BO_LOr) 8006f32e7eSjoerg llvm_unreachable("Unimplemented opcode"); 8106f32e7eSjoerg 8206f32e7eSjoerg llvm::SMTExprRef res = ASTs.front(); 8306f32e7eSjoerg for (std::size_t i = 1; i < ASTs.size(); ++i) 8406f32e7eSjoerg res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i]) 8506f32e7eSjoerg : Solver->mkOr(res, ASTs[i]); 8606f32e7eSjoerg return res; 8706f32e7eSjoerg } 8806f32e7eSjoerg 8906f32e7eSjoerg /// Construct an SMTSolverRef from a binary operator. fromBinOp(llvm::SMTSolverRef & Solver,const llvm::SMTExprRef & LHS,const BinaryOperator::Opcode Op,const llvm::SMTExprRef & RHS,bool isSigned)9006f32e7eSjoerg static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, 9106f32e7eSjoerg const llvm::SMTExprRef &LHS, 9206f32e7eSjoerg const BinaryOperator::Opcode Op, 9306f32e7eSjoerg const llvm::SMTExprRef &RHS, 9406f32e7eSjoerg bool isSigned) { 9506f32e7eSjoerg assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && 9606f32e7eSjoerg "AST's must have the same sort!"); 9706f32e7eSjoerg 9806f32e7eSjoerg switch (Op) { 9906f32e7eSjoerg // Multiplicative operators 10006f32e7eSjoerg case BO_Mul: 10106f32e7eSjoerg return Solver->mkBVMul(LHS, RHS); 10206f32e7eSjoerg 10306f32e7eSjoerg case BO_Div: 10406f32e7eSjoerg return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS); 10506f32e7eSjoerg 10606f32e7eSjoerg case BO_Rem: 10706f32e7eSjoerg return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS); 10806f32e7eSjoerg 10906f32e7eSjoerg // Additive operators 11006f32e7eSjoerg case BO_Add: 11106f32e7eSjoerg return Solver->mkBVAdd(LHS, RHS); 11206f32e7eSjoerg 11306f32e7eSjoerg case BO_Sub: 11406f32e7eSjoerg return Solver->mkBVSub(LHS, RHS); 11506f32e7eSjoerg 11606f32e7eSjoerg // Bitwise shift operators 11706f32e7eSjoerg case BO_Shl: 11806f32e7eSjoerg return Solver->mkBVShl(LHS, RHS); 11906f32e7eSjoerg 12006f32e7eSjoerg case BO_Shr: 12106f32e7eSjoerg return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS); 12206f32e7eSjoerg 12306f32e7eSjoerg // Relational operators 12406f32e7eSjoerg case BO_LT: 12506f32e7eSjoerg return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS); 12606f32e7eSjoerg 12706f32e7eSjoerg case BO_GT: 12806f32e7eSjoerg return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS); 12906f32e7eSjoerg 13006f32e7eSjoerg case BO_LE: 13106f32e7eSjoerg return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS); 13206f32e7eSjoerg 13306f32e7eSjoerg case BO_GE: 13406f32e7eSjoerg return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS); 13506f32e7eSjoerg 13606f32e7eSjoerg // Equality operators 13706f32e7eSjoerg case BO_EQ: 13806f32e7eSjoerg return Solver->mkEqual(LHS, RHS); 13906f32e7eSjoerg 14006f32e7eSjoerg case BO_NE: 14106f32e7eSjoerg return fromUnOp(Solver, UO_LNot, 14206f32e7eSjoerg fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned)); 14306f32e7eSjoerg 14406f32e7eSjoerg // Bitwise operators 14506f32e7eSjoerg case BO_And: 14606f32e7eSjoerg return Solver->mkBVAnd(LHS, RHS); 14706f32e7eSjoerg 14806f32e7eSjoerg case BO_Xor: 14906f32e7eSjoerg return Solver->mkBVXor(LHS, RHS); 15006f32e7eSjoerg 15106f32e7eSjoerg case BO_Or: 15206f32e7eSjoerg return Solver->mkBVOr(LHS, RHS); 15306f32e7eSjoerg 15406f32e7eSjoerg // Logical operators 15506f32e7eSjoerg case BO_LAnd: 15606f32e7eSjoerg return Solver->mkAnd(LHS, RHS); 15706f32e7eSjoerg 15806f32e7eSjoerg case BO_LOr: 15906f32e7eSjoerg return Solver->mkOr(LHS, RHS); 16006f32e7eSjoerg 16106f32e7eSjoerg default:; 16206f32e7eSjoerg } 16306f32e7eSjoerg llvm_unreachable("Unimplemented opcode"); 16406f32e7eSjoerg } 16506f32e7eSjoerg 16606f32e7eSjoerg /// Construct an SMTSolverRef from a special floating-point binary 16706f32e7eSjoerg /// operator. 16806f32e7eSjoerg static inline llvm::SMTExprRef fromFloatSpecialBinOp(llvm::SMTSolverRef & Solver,const llvm::SMTExprRef & LHS,const BinaryOperator::Opcode Op,const llvm::APFloat::fltCategory & RHS)16906f32e7eSjoerg fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, 17006f32e7eSjoerg const BinaryOperator::Opcode Op, 17106f32e7eSjoerg const llvm::APFloat::fltCategory &RHS) { 17206f32e7eSjoerg switch (Op) { 17306f32e7eSjoerg // Equality operators 17406f32e7eSjoerg case BO_EQ: 17506f32e7eSjoerg switch (RHS) { 17606f32e7eSjoerg case llvm::APFloat::fcInfinity: 17706f32e7eSjoerg return Solver->mkFPIsInfinite(LHS); 17806f32e7eSjoerg 17906f32e7eSjoerg case llvm::APFloat::fcNaN: 18006f32e7eSjoerg return Solver->mkFPIsNaN(LHS); 18106f32e7eSjoerg 18206f32e7eSjoerg case llvm::APFloat::fcNormal: 18306f32e7eSjoerg return Solver->mkFPIsNormal(LHS); 18406f32e7eSjoerg 18506f32e7eSjoerg case llvm::APFloat::fcZero: 18606f32e7eSjoerg return Solver->mkFPIsZero(LHS); 18706f32e7eSjoerg } 18806f32e7eSjoerg break; 18906f32e7eSjoerg 19006f32e7eSjoerg case BO_NE: 19106f32e7eSjoerg return fromFloatUnOp(Solver, UO_LNot, 19206f32e7eSjoerg fromFloatSpecialBinOp(Solver, LHS, BO_EQ, RHS)); 19306f32e7eSjoerg 19406f32e7eSjoerg default:; 19506f32e7eSjoerg } 19606f32e7eSjoerg 19706f32e7eSjoerg llvm_unreachable("Unimplemented opcode"); 19806f32e7eSjoerg } 19906f32e7eSjoerg 20006f32e7eSjoerg /// Construct an SMTSolverRef from a floating-point binary operator. fromFloatBinOp(llvm::SMTSolverRef & Solver,const llvm::SMTExprRef & LHS,const BinaryOperator::Opcode Op,const llvm::SMTExprRef & RHS)20106f32e7eSjoerg static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver, 20206f32e7eSjoerg const llvm::SMTExprRef &LHS, 20306f32e7eSjoerg const BinaryOperator::Opcode Op, 20406f32e7eSjoerg const llvm::SMTExprRef &RHS) { 20506f32e7eSjoerg assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && 20606f32e7eSjoerg "AST's must have the same sort!"); 20706f32e7eSjoerg 20806f32e7eSjoerg switch (Op) { 20906f32e7eSjoerg // Multiplicative operators 21006f32e7eSjoerg case BO_Mul: 21106f32e7eSjoerg return Solver->mkFPMul(LHS, RHS); 21206f32e7eSjoerg 21306f32e7eSjoerg case BO_Div: 21406f32e7eSjoerg return Solver->mkFPDiv(LHS, RHS); 21506f32e7eSjoerg 21606f32e7eSjoerg case BO_Rem: 21706f32e7eSjoerg return Solver->mkFPRem(LHS, RHS); 21806f32e7eSjoerg 21906f32e7eSjoerg // Additive operators 22006f32e7eSjoerg case BO_Add: 22106f32e7eSjoerg return Solver->mkFPAdd(LHS, RHS); 22206f32e7eSjoerg 22306f32e7eSjoerg case BO_Sub: 22406f32e7eSjoerg return Solver->mkFPSub(LHS, RHS); 22506f32e7eSjoerg 22606f32e7eSjoerg // Relational operators 22706f32e7eSjoerg case BO_LT: 22806f32e7eSjoerg return Solver->mkFPLt(LHS, RHS); 22906f32e7eSjoerg 23006f32e7eSjoerg case BO_GT: 23106f32e7eSjoerg return Solver->mkFPGt(LHS, RHS); 23206f32e7eSjoerg 23306f32e7eSjoerg case BO_LE: 23406f32e7eSjoerg return Solver->mkFPLe(LHS, RHS); 23506f32e7eSjoerg 23606f32e7eSjoerg case BO_GE: 23706f32e7eSjoerg return Solver->mkFPGe(LHS, RHS); 23806f32e7eSjoerg 23906f32e7eSjoerg // Equality operators 24006f32e7eSjoerg case BO_EQ: 24106f32e7eSjoerg return Solver->mkFPEqual(LHS, RHS); 24206f32e7eSjoerg 24306f32e7eSjoerg case BO_NE: 24406f32e7eSjoerg return fromFloatUnOp(Solver, UO_LNot, 24506f32e7eSjoerg fromFloatBinOp(Solver, LHS, BO_EQ, RHS)); 24606f32e7eSjoerg 24706f32e7eSjoerg // Logical operators 24806f32e7eSjoerg case BO_LAnd: 24906f32e7eSjoerg case BO_LOr: 25006f32e7eSjoerg return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false); 25106f32e7eSjoerg 25206f32e7eSjoerg default:; 25306f32e7eSjoerg } 25406f32e7eSjoerg 25506f32e7eSjoerg llvm_unreachable("Unimplemented opcode"); 25606f32e7eSjoerg } 25706f32e7eSjoerg 25806f32e7eSjoerg /// Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy, 25906f32e7eSjoerg /// and their bit widths. fromCast(llvm::SMTSolverRef & Solver,const llvm::SMTExprRef & Exp,QualType ToTy,uint64_t ToBitWidth,QualType FromTy,uint64_t FromBitWidth)26006f32e7eSjoerg static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver, 26106f32e7eSjoerg const llvm::SMTExprRef &Exp, 26206f32e7eSjoerg QualType ToTy, uint64_t ToBitWidth, 26306f32e7eSjoerg QualType FromTy, 26406f32e7eSjoerg uint64_t FromBitWidth) { 26506f32e7eSjoerg if ((FromTy->isIntegralOrEnumerationType() && 26606f32e7eSjoerg ToTy->isIntegralOrEnumerationType()) || 26706f32e7eSjoerg (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) || 26806f32e7eSjoerg (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) || 26906f32e7eSjoerg (FromTy->isReferenceType() ^ ToTy->isReferenceType())) { 27006f32e7eSjoerg 27106f32e7eSjoerg if (FromTy->isBooleanType()) { 27206f32e7eSjoerg assert(ToBitWidth > 0 && "BitWidth must be positive!"); 27306f32e7eSjoerg return Solver->mkIte( 27406f32e7eSjoerg Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth), 27506f32e7eSjoerg Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth)); 27606f32e7eSjoerg } 27706f32e7eSjoerg 27806f32e7eSjoerg if (ToBitWidth > FromBitWidth) 27906f32e7eSjoerg return FromTy->isSignedIntegerOrEnumerationType() 28006f32e7eSjoerg ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp) 28106f32e7eSjoerg : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp); 28206f32e7eSjoerg 28306f32e7eSjoerg if (ToBitWidth < FromBitWidth) 28406f32e7eSjoerg return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp); 28506f32e7eSjoerg 28606f32e7eSjoerg // Both are bitvectors with the same width, ignore the type cast 28706f32e7eSjoerg return Exp; 28806f32e7eSjoerg } 28906f32e7eSjoerg 29006f32e7eSjoerg if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) { 29106f32e7eSjoerg if (ToBitWidth != FromBitWidth) 29206f32e7eSjoerg return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth)); 29306f32e7eSjoerg 29406f32e7eSjoerg return Exp; 29506f32e7eSjoerg } 29606f32e7eSjoerg 29706f32e7eSjoerg if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) { 29806f32e7eSjoerg llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth); 29906f32e7eSjoerg return FromTy->isSignedIntegerOrEnumerationType() 30006f32e7eSjoerg ? Solver->mkSBVtoFP(Exp, Sort) 30106f32e7eSjoerg : Solver->mkUBVtoFP(Exp, Sort); 30206f32e7eSjoerg } 30306f32e7eSjoerg 30406f32e7eSjoerg if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType()) 30506f32e7eSjoerg return ToTy->isSignedIntegerOrEnumerationType() 30606f32e7eSjoerg ? Solver->mkFPtoSBV(Exp, ToBitWidth) 30706f32e7eSjoerg : Solver->mkFPtoUBV(Exp, ToBitWidth); 30806f32e7eSjoerg 30906f32e7eSjoerg llvm_unreachable("Unsupported explicit type cast!"); 31006f32e7eSjoerg } 31106f32e7eSjoerg 31206f32e7eSjoerg // Callback function for doCast parameter on APSInt type. castAPSInt(llvm::SMTSolverRef & Solver,const llvm::APSInt & V,QualType ToTy,uint64_t ToWidth,QualType FromTy,uint64_t FromWidth)31306f32e7eSjoerg static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver, 31406f32e7eSjoerg const llvm::APSInt &V, QualType ToTy, 31506f32e7eSjoerg uint64_t ToWidth, QualType FromTy, 31606f32e7eSjoerg uint64_t FromWidth) { 31706f32e7eSjoerg APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType()); 31806f32e7eSjoerg return TargetType.convert(V); 31906f32e7eSjoerg } 32006f32e7eSjoerg 32106f32e7eSjoerg /// Construct an SMTSolverRef from a SymbolData. 322*13fbcb42Sjoerg static inline llvm::SMTExprRef fromData(llvm::SMTSolverRef & Solver,ASTContext & Ctx,const SymbolData * Sym)323*13fbcb42Sjoerg fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) { 324*13fbcb42Sjoerg const SymbolID ID = Sym->getSymbolID(); 325*13fbcb42Sjoerg const QualType Ty = Sym->getType(); 326*13fbcb42Sjoerg const uint64_t BitWidth = Ctx.getTypeSize(Ty); 327*13fbcb42Sjoerg 328*13fbcb42Sjoerg llvm::SmallString<16> Str; 329*13fbcb42Sjoerg llvm::raw_svector_ostream OS(Str); 330*13fbcb42Sjoerg OS << Sym->getKindStr() << ID; 331*13fbcb42Sjoerg return Solver->mkSymbol(Str.c_str(), mkSort(Solver, Ty, BitWidth)); 33206f32e7eSjoerg } 33306f32e7eSjoerg 33406f32e7eSjoerg // Wrapper to generate SMTSolverRef from SymbolCast data. getCastExpr(llvm::SMTSolverRef & Solver,ASTContext & Ctx,const llvm::SMTExprRef & Exp,QualType FromTy,QualType ToTy)33506f32e7eSjoerg static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver, 33606f32e7eSjoerg ASTContext &Ctx, 33706f32e7eSjoerg const llvm::SMTExprRef &Exp, 33806f32e7eSjoerg QualType FromTy, QualType ToTy) { 33906f32e7eSjoerg return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy, 34006f32e7eSjoerg Ctx.getTypeSize(FromTy)); 34106f32e7eSjoerg } 34206f32e7eSjoerg 34306f32e7eSjoerg // Wrapper to generate SMTSolverRef from unpacked binary symbolic 34406f32e7eSjoerg // expression. Sets the RetTy parameter. See getSMTSolverRef(). 34506f32e7eSjoerg static inline 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)34606f32e7eSjoerg getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, 34706f32e7eSjoerg const llvm::SMTExprRef &LHS, QualType LTy, 34806f32e7eSjoerg BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, 34906f32e7eSjoerg QualType RTy, QualType *RetTy) { 35006f32e7eSjoerg llvm::SMTExprRef NewLHS = LHS; 35106f32e7eSjoerg llvm::SMTExprRef NewRHS = RHS; 35206f32e7eSjoerg doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy); 35306f32e7eSjoerg 35406f32e7eSjoerg // Update the return type parameter if the output type has changed. 35506f32e7eSjoerg if (RetTy) { 35606f32e7eSjoerg // A boolean result can be represented as an integer type in C/C++, but at 35706f32e7eSjoerg // this point we only care about the SMT sorts. Set it as a boolean type 35806f32e7eSjoerg // to avoid subsequent SMT errors. 35906f32e7eSjoerg if (BinaryOperator::isComparisonOp(Op) || 36006f32e7eSjoerg BinaryOperator::isLogicalOp(Op)) { 36106f32e7eSjoerg *RetTy = Ctx.BoolTy; 36206f32e7eSjoerg } else { 36306f32e7eSjoerg *RetTy = LTy; 36406f32e7eSjoerg } 36506f32e7eSjoerg 36606f32e7eSjoerg // If the two operands are pointers and the operation is a subtraction, 36706f32e7eSjoerg // the result is of type ptrdiff_t, which is signed 36806f32e7eSjoerg if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) { 36906f32e7eSjoerg *RetTy = Ctx.getPointerDiffType(); 37006f32e7eSjoerg } 37106f32e7eSjoerg } 37206f32e7eSjoerg 37306f32e7eSjoerg return LTy->isRealFloatingType() 37406f32e7eSjoerg ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS) 37506f32e7eSjoerg : fromBinOp(Solver, NewLHS, Op, NewRHS, 37606f32e7eSjoerg LTy->isSignedIntegerOrEnumerationType()); 37706f32e7eSjoerg } 37806f32e7eSjoerg 37906f32e7eSjoerg // Wrapper to generate SMTSolverRef from BinarySymExpr. 38006f32e7eSjoerg // Sets the hasComparison and RetTy parameters. See getSMTSolverRef(). getSymBinExpr(llvm::SMTSolverRef & Solver,ASTContext & Ctx,const BinarySymExpr * BSE,bool * hasComparison,QualType * RetTy)38106f32e7eSjoerg static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver, 38206f32e7eSjoerg ASTContext &Ctx, 38306f32e7eSjoerg const BinarySymExpr *BSE, 38406f32e7eSjoerg bool *hasComparison, 38506f32e7eSjoerg QualType *RetTy) { 38606f32e7eSjoerg QualType LTy, RTy; 38706f32e7eSjoerg BinaryOperator::Opcode Op = BSE->getOpcode(); 38806f32e7eSjoerg 38906f32e7eSjoerg if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) { 39006f32e7eSjoerg llvm::SMTExprRef LHS = 39106f32e7eSjoerg getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison); 39206f32e7eSjoerg llvm::APSInt NewRInt; 39306f32e7eSjoerg std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS()); 39406f32e7eSjoerg llvm::SMTExprRef RHS = 39506f32e7eSjoerg Solver->mkBitvector(NewRInt, NewRInt.getBitWidth()); 39606f32e7eSjoerg return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); 39706f32e7eSjoerg } 39806f32e7eSjoerg 39906f32e7eSjoerg if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) { 40006f32e7eSjoerg llvm::APSInt NewLInt; 40106f32e7eSjoerg std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS()); 40206f32e7eSjoerg llvm::SMTExprRef LHS = 40306f32e7eSjoerg Solver->mkBitvector(NewLInt, NewLInt.getBitWidth()); 40406f32e7eSjoerg llvm::SMTExprRef RHS = 40506f32e7eSjoerg getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison); 40606f32e7eSjoerg return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); 40706f32e7eSjoerg } 40806f32e7eSjoerg 40906f32e7eSjoerg if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) { 41006f32e7eSjoerg llvm::SMTExprRef LHS = 41106f32e7eSjoerg getSymExpr(Solver, Ctx, SSM->getLHS(), <y, hasComparison); 41206f32e7eSjoerg llvm::SMTExprRef RHS = 41306f32e7eSjoerg getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison); 41406f32e7eSjoerg return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); 41506f32e7eSjoerg } 41606f32e7eSjoerg 41706f32e7eSjoerg llvm_unreachable("Unsupported BinarySymExpr type!"); 41806f32e7eSjoerg } 41906f32e7eSjoerg 42006f32e7eSjoerg // Recursive implementation to unpack and generate symbolic expression. 42106f32e7eSjoerg // Sets the hasComparison and RetTy parameters. See getExpr(). getSymExpr(llvm::SMTSolverRef & Solver,ASTContext & Ctx,SymbolRef Sym,QualType * RetTy,bool * hasComparison)42206f32e7eSjoerg static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver, 42306f32e7eSjoerg ASTContext &Ctx, SymbolRef Sym, 42406f32e7eSjoerg QualType *RetTy, 42506f32e7eSjoerg bool *hasComparison) { 42606f32e7eSjoerg if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) { 42706f32e7eSjoerg if (RetTy) 42806f32e7eSjoerg *RetTy = Sym->getType(); 42906f32e7eSjoerg 430*13fbcb42Sjoerg return fromData(Solver, Ctx, SD); 43106f32e7eSjoerg } 43206f32e7eSjoerg 43306f32e7eSjoerg if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) { 43406f32e7eSjoerg if (RetTy) 43506f32e7eSjoerg *RetTy = Sym->getType(); 43606f32e7eSjoerg 43706f32e7eSjoerg QualType FromTy; 43806f32e7eSjoerg llvm::SMTExprRef Exp = 43906f32e7eSjoerg getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison); 44006f32e7eSjoerg 44106f32e7eSjoerg // Casting an expression with a comparison invalidates it. Note that this 44206f32e7eSjoerg // must occur after the recursive call above. 44306f32e7eSjoerg // e.g. (signed char) (x > 0) 44406f32e7eSjoerg if (hasComparison) 44506f32e7eSjoerg *hasComparison = false; 44606f32e7eSjoerg return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType()); 44706f32e7eSjoerg } 44806f32e7eSjoerg 44906f32e7eSjoerg if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) { 45006f32e7eSjoerg llvm::SMTExprRef Exp = 45106f32e7eSjoerg getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy); 45206f32e7eSjoerg // Set the hasComparison parameter, in post-order traversal order. 45306f32e7eSjoerg if (hasComparison) 45406f32e7eSjoerg *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode()); 45506f32e7eSjoerg return Exp; 45606f32e7eSjoerg } 45706f32e7eSjoerg 45806f32e7eSjoerg llvm_unreachable("Unsupported SymbolRef type!"); 45906f32e7eSjoerg } 46006f32e7eSjoerg 46106f32e7eSjoerg // Generate an SMTSolverRef that represents the given symbolic expression. 46206f32e7eSjoerg // Sets the hasComparison parameter if the expression has a comparison 46306f32e7eSjoerg // operator. Sets the RetTy parameter to the final return type after 46406f32e7eSjoerg // promotions and casts. 46506f32e7eSjoerg static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, 46606f32e7eSjoerg ASTContext &Ctx, SymbolRef Sym, 46706f32e7eSjoerg QualType *RetTy = nullptr, 46806f32e7eSjoerg bool *hasComparison = nullptr) { 46906f32e7eSjoerg if (hasComparison) { 47006f32e7eSjoerg *hasComparison = false; 47106f32e7eSjoerg } 47206f32e7eSjoerg 47306f32e7eSjoerg return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison); 47406f32e7eSjoerg } 47506f32e7eSjoerg 47606f32e7eSjoerg // Generate an SMTSolverRef that compares the expression to zero. getZeroExpr(llvm::SMTSolverRef & Solver,ASTContext & Ctx,const llvm::SMTExprRef & Exp,QualType Ty,bool Assumption)47706f32e7eSjoerg static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, 47806f32e7eSjoerg ASTContext &Ctx, 47906f32e7eSjoerg const llvm::SMTExprRef &Exp, 48006f32e7eSjoerg QualType Ty, bool Assumption) { 48106f32e7eSjoerg if (Ty->isRealFloatingType()) { 48206f32e7eSjoerg llvm::APFloat Zero = 48306f32e7eSjoerg llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty)); 48406f32e7eSjoerg return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE, 48506f32e7eSjoerg Solver->mkFloat(Zero)); 48606f32e7eSjoerg } 48706f32e7eSjoerg 48806f32e7eSjoerg if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() || 48906f32e7eSjoerg Ty->isBlockPointerType() || Ty->isReferenceType()) { 49006f32e7eSjoerg 49106f32e7eSjoerg // Skip explicit comparison for boolean types 49206f32e7eSjoerg bool isSigned = Ty->isSignedIntegerOrEnumerationType(); 49306f32e7eSjoerg if (Ty->isBooleanType()) 49406f32e7eSjoerg return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp; 49506f32e7eSjoerg 49606f32e7eSjoerg return fromBinOp( 49706f32e7eSjoerg Solver, Exp, Assumption ? BO_EQ : BO_NE, 49806f32e7eSjoerg Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)), 49906f32e7eSjoerg isSigned); 50006f32e7eSjoerg } 50106f32e7eSjoerg 50206f32e7eSjoerg llvm_unreachable("Unsupported type for zero value!"); 50306f32e7eSjoerg } 50406f32e7eSjoerg 50506f32e7eSjoerg // Wrapper to generate SMTSolverRef from a range. If From == To, an 50606f32e7eSjoerg // equality will be created instead. 50706f32e7eSjoerg static inline llvm::SMTExprRef getRangeExpr(llvm::SMTSolverRef & Solver,ASTContext & Ctx,SymbolRef Sym,const llvm::APSInt & From,const llvm::APSInt & To,bool InRange)50806f32e7eSjoerg getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, 50906f32e7eSjoerg const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) { 51006f32e7eSjoerg // Convert lower bound 51106f32e7eSjoerg QualType FromTy; 51206f32e7eSjoerg llvm::APSInt NewFromInt; 51306f32e7eSjoerg std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From); 51406f32e7eSjoerg llvm::SMTExprRef FromExp = 51506f32e7eSjoerg Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth()); 51606f32e7eSjoerg 51706f32e7eSjoerg // Convert symbol 51806f32e7eSjoerg QualType SymTy; 51906f32e7eSjoerg llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy); 52006f32e7eSjoerg 52106f32e7eSjoerg // Construct single (in)equality 52206f32e7eSjoerg if (From == To) 52306f32e7eSjoerg return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE, 52406f32e7eSjoerg FromExp, FromTy, /*RetTy=*/nullptr); 52506f32e7eSjoerg 52606f32e7eSjoerg QualType ToTy; 52706f32e7eSjoerg llvm::APSInt NewToInt; 52806f32e7eSjoerg std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To); 52906f32e7eSjoerg llvm::SMTExprRef ToExp = 53006f32e7eSjoerg Solver->mkBitvector(NewToInt, NewToInt.getBitWidth()); 53106f32e7eSjoerg assert(FromTy == ToTy && "Range values have different types!"); 53206f32e7eSjoerg 53306f32e7eSjoerg // Construct two (in)equalities, and a logical and/or 53406f32e7eSjoerg llvm::SMTExprRef LHS = 53506f32e7eSjoerg getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp, 53606f32e7eSjoerg FromTy, /*RetTy=*/nullptr); 53706f32e7eSjoerg llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy, 53806f32e7eSjoerg InRange ? BO_LE : BO_GT, ToExp, ToTy, 53906f32e7eSjoerg /*RetTy=*/nullptr); 54006f32e7eSjoerg 54106f32e7eSjoerg return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS, 54206f32e7eSjoerg SymTy->isSignedIntegerOrEnumerationType()); 54306f32e7eSjoerg } 54406f32e7eSjoerg 54506f32e7eSjoerg // Recover the QualType of an APSInt. 54606f32e7eSjoerg // TODO: Refactor to put elsewhere getAPSIntType(ASTContext & Ctx,const llvm::APSInt & Int)54706f32e7eSjoerg static inline QualType getAPSIntType(ASTContext &Ctx, 54806f32e7eSjoerg const llvm::APSInt &Int) { 54906f32e7eSjoerg return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned()); 55006f32e7eSjoerg } 55106f32e7eSjoerg 55206f32e7eSjoerg // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1. 55306f32e7eSjoerg static inline std::pair<llvm::APSInt, QualType> fixAPSInt(ASTContext & Ctx,const llvm::APSInt & Int)55406f32e7eSjoerg fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) { 55506f32e7eSjoerg llvm::APSInt NewInt; 55606f32e7eSjoerg 55706f32e7eSjoerg // FIXME: This should be a cast from a 1-bit integer type to a boolean type, 55806f32e7eSjoerg // but the former is not available in Clang. Instead, extend the APSInt 55906f32e7eSjoerg // directly. 56006f32e7eSjoerg if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) { 56106f32e7eSjoerg NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy)); 56206f32e7eSjoerg } else 56306f32e7eSjoerg NewInt = Int; 56406f32e7eSjoerg 56506f32e7eSjoerg return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt)); 56606f32e7eSjoerg } 56706f32e7eSjoerg 56806f32e7eSjoerg // Perform implicit type conversion on binary symbolic expressions. 56906f32e7eSjoerg // May modify all input parameters. 57006f32e7eSjoerg // TODO: Refactor to use built-in conversion functions doTypeConversion(llvm::SMTSolverRef & Solver,ASTContext & Ctx,llvm::SMTExprRef & LHS,llvm::SMTExprRef & RHS,QualType & LTy,QualType & RTy)57106f32e7eSjoerg static inline void doTypeConversion(llvm::SMTSolverRef &Solver, 57206f32e7eSjoerg ASTContext &Ctx, llvm::SMTExprRef &LHS, 57306f32e7eSjoerg llvm::SMTExprRef &RHS, QualType <y, 57406f32e7eSjoerg QualType &RTy) { 57506f32e7eSjoerg assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!"); 57606f32e7eSjoerg 57706f32e7eSjoerg // Perform type conversion 57806f32e7eSjoerg if ((LTy->isIntegralOrEnumerationType() && 57906f32e7eSjoerg RTy->isIntegralOrEnumerationType()) && 58006f32e7eSjoerg (LTy->isArithmeticType() && RTy->isArithmeticType())) { 58106f32e7eSjoerg SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>( 58206f32e7eSjoerg Solver, Ctx, LHS, LTy, RHS, RTy); 58306f32e7eSjoerg return; 58406f32e7eSjoerg } 58506f32e7eSjoerg 58606f32e7eSjoerg if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) { 58706f32e7eSjoerg SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>( 58806f32e7eSjoerg Solver, Ctx, LHS, LTy, RHS, RTy); 58906f32e7eSjoerg return; 59006f32e7eSjoerg } 59106f32e7eSjoerg 59206f32e7eSjoerg if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) || 59306f32e7eSjoerg (LTy->isBlockPointerType() || RTy->isBlockPointerType()) || 59406f32e7eSjoerg (LTy->isReferenceType() || RTy->isReferenceType())) { 59506f32e7eSjoerg // TODO: Refactor to Sema::FindCompositePointerType(), and 59606f32e7eSjoerg // Sema::CheckCompareOperands(). 59706f32e7eSjoerg 59806f32e7eSjoerg uint64_t LBitWidth = Ctx.getTypeSize(LTy); 59906f32e7eSjoerg uint64_t RBitWidth = Ctx.getTypeSize(RTy); 60006f32e7eSjoerg 60106f32e7eSjoerg // Cast the non-pointer type to the pointer type. 60206f32e7eSjoerg // TODO: Be more strict about this. 60306f32e7eSjoerg if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) || 60406f32e7eSjoerg (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) || 60506f32e7eSjoerg (LTy->isReferenceType() ^ RTy->isReferenceType())) { 60606f32e7eSjoerg if (LTy->isNullPtrType() || LTy->isBlockPointerType() || 60706f32e7eSjoerg LTy->isReferenceType()) { 60806f32e7eSjoerg LHS = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth); 60906f32e7eSjoerg LTy = RTy; 61006f32e7eSjoerg } else { 61106f32e7eSjoerg RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); 61206f32e7eSjoerg RTy = LTy; 61306f32e7eSjoerg } 61406f32e7eSjoerg } 61506f32e7eSjoerg 61606f32e7eSjoerg // Cast the void pointer type to the non-void pointer type. 61706f32e7eSjoerg // For void types, this assumes that the casted value is equal to the 61806f32e7eSjoerg // value of the original pointer, and does not account for alignment 61906f32e7eSjoerg // requirements. 62006f32e7eSjoerg if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) { 62106f32e7eSjoerg assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) && 62206f32e7eSjoerg "Pointer types have different bitwidths!"); 62306f32e7eSjoerg if (RTy->isVoidPointerType()) 62406f32e7eSjoerg RTy = LTy; 62506f32e7eSjoerg else 62606f32e7eSjoerg LTy = RTy; 62706f32e7eSjoerg } 62806f32e7eSjoerg 62906f32e7eSjoerg if (LTy == RTy) 63006f32e7eSjoerg return; 63106f32e7eSjoerg } 63206f32e7eSjoerg 63306f32e7eSjoerg // Fallback: for the solver, assume that these types don't really matter 63406f32e7eSjoerg if ((LTy.getCanonicalType() == RTy.getCanonicalType()) || 63506f32e7eSjoerg (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) { 63606f32e7eSjoerg LTy = RTy; 63706f32e7eSjoerg return; 63806f32e7eSjoerg } 63906f32e7eSjoerg 64006f32e7eSjoerg // TODO: Refine behavior for invalid type casts 64106f32e7eSjoerg } 64206f32e7eSjoerg 64306f32e7eSjoerg // Perform implicit integer type conversion. 64406f32e7eSjoerg // May modify all input parameters. 64506f32e7eSjoerg // TODO: Refactor to use Sema::handleIntegerConversion() 64606f32e7eSjoerg template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &, 64706f32e7eSjoerg QualType, uint64_t, QualType, uint64_t)> doIntTypeConversion(llvm::SMTSolverRef & Solver,ASTContext & Ctx,T & LHS,QualType & LTy,T & RHS,QualType & RTy)64806f32e7eSjoerg static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver, 64906f32e7eSjoerg ASTContext &Ctx, T &LHS, QualType <y, 65006f32e7eSjoerg T &RHS, QualType &RTy) { 65106f32e7eSjoerg uint64_t LBitWidth = Ctx.getTypeSize(LTy); 65206f32e7eSjoerg uint64_t RBitWidth = Ctx.getTypeSize(RTy); 65306f32e7eSjoerg 65406f32e7eSjoerg assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!"); 65506f32e7eSjoerg // Always perform integer promotion before checking type equality. 65606f32e7eSjoerg // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion 65706f32e7eSjoerg if (LTy->isPromotableIntegerType()) { 65806f32e7eSjoerg QualType NewTy = Ctx.getPromotedIntegerType(LTy); 65906f32e7eSjoerg uint64_t NewBitWidth = Ctx.getTypeSize(NewTy); 66006f32e7eSjoerg LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth); 66106f32e7eSjoerg LTy = NewTy; 66206f32e7eSjoerg LBitWidth = NewBitWidth; 66306f32e7eSjoerg } 66406f32e7eSjoerg if (RTy->isPromotableIntegerType()) { 66506f32e7eSjoerg QualType NewTy = Ctx.getPromotedIntegerType(RTy); 66606f32e7eSjoerg uint64_t NewBitWidth = Ctx.getTypeSize(NewTy); 66706f32e7eSjoerg RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth); 66806f32e7eSjoerg RTy = NewTy; 66906f32e7eSjoerg RBitWidth = NewBitWidth; 67006f32e7eSjoerg } 67106f32e7eSjoerg 67206f32e7eSjoerg if (LTy == RTy) 67306f32e7eSjoerg return; 67406f32e7eSjoerg 67506f32e7eSjoerg // Perform integer type conversion 67606f32e7eSjoerg // Note: Safe to skip updating bitwidth because this must terminate 67706f32e7eSjoerg bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType(); 67806f32e7eSjoerg bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType(); 67906f32e7eSjoerg 68006f32e7eSjoerg int order = Ctx.getIntegerTypeOrder(LTy, RTy); 68106f32e7eSjoerg if (isLSignedTy == isRSignedTy) { 68206f32e7eSjoerg // Same signedness; use the higher-ranked type 68306f32e7eSjoerg if (order == 1) { 68406f32e7eSjoerg RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); 68506f32e7eSjoerg RTy = LTy; 68606f32e7eSjoerg } else { 68706f32e7eSjoerg LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth); 68806f32e7eSjoerg LTy = RTy; 68906f32e7eSjoerg } 69006f32e7eSjoerg } else if (order != (isLSignedTy ? 1 : -1)) { 69106f32e7eSjoerg // The unsigned type has greater than or equal rank to the 69206f32e7eSjoerg // signed type, so use the unsigned type 69306f32e7eSjoerg if (isRSignedTy) { 69406f32e7eSjoerg RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); 69506f32e7eSjoerg RTy = LTy; 69606f32e7eSjoerg } else { 69706f32e7eSjoerg LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth); 69806f32e7eSjoerg LTy = RTy; 69906f32e7eSjoerg } 70006f32e7eSjoerg } else if (LBitWidth != RBitWidth) { 70106f32e7eSjoerg // The two types are different widths; if we are here, that 70206f32e7eSjoerg // means the signed type is larger than the unsigned type, so 70306f32e7eSjoerg // use the signed type. 70406f32e7eSjoerg if (isLSignedTy) { 70506f32e7eSjoerg RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); 70606f32e7eSjoerg RTy = LTy; 70706f32e7eSjoerg } else { 70806f32e7eSjoerg LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth); 70906f32e7eSjoerg LTy = RTy; 71006f32e7eSjoerg } 71106f32e7eSjoerg } else { 71206f32e7eSjoerg // The signed type is higher-ranked than the unsigned type, 71306f32e7eSjoerg // but isn't actually any bigger (like unsigned int and long 71406f32e7eSjoerg // on most 32-bit systems). Use the unsigned type corresponding 71506f32e7eSjoerg // to the signed type. 71606f32e7eSjoerg QualType NewTy = 71706f32e7eSjoerg Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy); 71806f32e7eSjoerg RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); 71906f32e7eSjoerg RTy = NewTy; 72006f32e7eSjoerg LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth); 72106f32e7eSjoerg LTy = NewTy; 72206f32e7eSjoerg } 72306f32e7eSjoerg } 72406f32e7eSjoerg 72506f32e7eSjoerg // Perform implicit floating-point type conversion. 72606f32e7eSjoerg // May modify all input parameters. 72706f32e7eSjoerg // TODO: Refactor to use Sema::handleFloatConversion() 72806f32e7eSjoerg template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &, 72906f32e7eSjoerg QualType, uint64_t, QualType, uint64_t)> 73006f32e7eSjoerg static inline void doFloatTypeConversion(llvm::SMTSolverRef & Solver,ASTContext & Ctx,T & LHS,QualType & LTy,T & RHS,QualType & RTy)73106f32e7eSjoerg doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, 73206f32e7eSjoerg QualType <y, T &RHS, QualType &RTy) { 73306f32e7eSjoerg uint64_t LBitWidth = Ctx.getTypeSize(LTy); 73406f32e7eSjoerg uint64_t RBitWidth = Ctx.getTypeSize(RTy); 73506f32e7eSjoerg 73606f32e7eSjoerg // Perform float-point type promotion 73706f32e7eSjoerg if (!LTy->isRealFloatingType()) { 73806f32e7eSjoerg LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth); 73906f32e7eSjoerg LTy = RTy; 74006f32e7eSjoerg LBitWidth = RBitWidth; 74106f32e7eSjoerg } 74206f32e7eSjoerg if (!RTy->isRealFloatingType()) { 74306f32e7eSjoerg RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); 74406f32e7eSjoerg RTy = LTy; 74506f32e7eSjoerg RBitWidth = LBitWidth; 74606f32e7eSjoerg } 74706f32e7eSjoerg 74806f32e7eSjoerg if (LTy == RTy) 74906f32e7eSjoerg return; 75006f32e7eSjoerg 75106f32e7eSjoerg // If we have two real floating types, convert the smaller operand to the 75206f32e7eSjoerg // bigger result 75306f32e7eSjoerg // Note: Safe to skip updating bitwidth because this must terminate 75406f32e7eSjoerg int order = Ctx.getFloatingTypeOrder(LTy, RTy); 75506f32e7eSjoerg if (order > 0) { 75606f32e7eSjoerg RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); 75706f32e7eSjoerg RTy = LTy; 75806f32e7eSjoerg } else if (order == 0) { 75906f32e7eSjoerg LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth); 76006f32e7eSjoerg LTy = RTy; 76106f32e7eSjoerg } else { 76206f32e7eSjoerg llvm_unreachable("Unsupported floating-point type cast!"); 76306f32e7eSjoerg } 76406f32e7eSjoerg } 76506f32e7eSjoerg }; 76606f32e7eSjoerg } // namespace ento 76706f32e7eSjoerg } // namespace clang 76806f32e7eSjoerg 76906f32e7eSjoerg #endif 770