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