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