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