SMTConv.h Source File (original) (raw)

13#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H

14#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H

19#include "llvm/Support/SMTAPI.h"

22namespace ento {

25public:

27 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,

28 const QualType &Ty, unsigned BitWidth) {

30 return Solver->getBoolSort();

33 return Solver->getFloatSort(BitWidth);

35 return Solver->getBitvectorSort(BitWidth);

36 }

39 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver,

41 const llvm::SMTExprRef &Exp) {

42 switch (Op) {

43 case UO_Minus:

44 return Solver->mkBVNeg(Exp);

46 case UO_Not:

47 return Solver->mkBVNot(Exp);

49 case UO_LNot:

50 return Solver->mkNot(Exp);

52 default:;

53 }

54 llvm_unreachable("Unimplemented opcode");

55 }

58 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver,

60 const llvm::SMTExprRef &Exp) {

61 switch (Op) {

62 case UO_Minus:

63 return Solver->mkFPNeg(Exp);

65 case UO_LNot:

66 return fromUnOp(Solver, Op, Exp);

68 default:;

69 }

70 llvm_unreachable("Unimplemented opcode");

71 }

74 static inline llvm::SMTExprRef

76 const std::vectorllvm::SMTExprRef &ASTs) {

77 assert(!ASTs.empty());

79 if (Op != BO_LAnd && Op != BO_LOr)

80 llvm_unreachable("Unimplemented opcode");

82 llvm::SMTExprRef res = ASTs.front();

83 for (std::size_t i = 1; i < ASTs.size(); ++i)

84 res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])

85 : Solver->mkOr(res, ASTs[i]);

86 return res;

87 }

90 static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver,

91 const llvm::SMTExprRef &LHS,

93 const llvm::SMTExprRef &RHS,

94 bool isSigned) {

95 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&

96 "AST's must have the same sort!");

98 switch (Op) {

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

110 case BO_Add:

111 return Solver->mkBVAdd(LHS, RHS);

112

113 case BO_Sub:

114 return Solver->mkBVSub(LHS, RHS);

115

116

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

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

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

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

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

167

168 static inline llvm::SMTExprRef

171 const llvm::APFloat::fltCategory &RHS) {

172 switch (Op) {

173

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:

193

194 default:;

195 }

196

197 llvm_unreachable("Unimplemented opcode");

198 }

199

200

201 static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver,

202 const llvm::SMTExprRef &LHS,

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

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

220 case BO_Add:

221 return Solver->mkFPAdd(LHS, RHS);

222

223 case BO_Sub:

224 return Solver->mkFPSub(LHS, RHS);

225

226

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

240 case BO_EQ:

241 return Solver->mkFPEqual(LHS, RHS);

242

243 case BO_NE:

246

247

248 case BO_LAnd:

249 case BO_LOr:

250 return fromBinOp(Solver, LHS, Op, RHS, false);

251

252 default:;

253 }

254

255 llvm_unreachable("Unimplemented opcode");

256 }

257

258

259

260 static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver,

261 const llvm::SMTExprRef &Exp,

262 QualType ToTy, uint64_t ToBitWidth,

264 uint64_t FromBitWidth) {

270

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)

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

287 return Exp;

288 }

289

291 if (ToBitWidth != FromBitWidth)

292 return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));

293

294 return Exp;

295 }

296

298 llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);

300 ? Solver->mkSBVtoFP(Exp, Sort)

301 : Solver->mkUBVtoFP(Exp, Sort);

302 }

303

306 ? Solver->mkFPtoSBV(Exp, ToBitWidth)

307 : Solver->mkFPtoUBV(Exp, ToBitWidth);

308

309 llvm_unreachable("Unsupported explicit type cast!");

310 }

311

312

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) {

318 return TargetType.convert(V);

319 }

320

321

322 static inline llvm::SMTExprRef

326 const uint64_t BitWidth = Ctx.getTypeSize(Ty);

327

329 llvm::raw_svector_ostream OS(Str);

331 return Solver->mkSymbol(Str.c_str(), mkSort(Solver, Ty, BitWidth));

332 }

333

334

335 static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,

337 const llvm::SMTExprRef &Exp,

339 return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,

340 Ctx.getTypeSize(FromTy));

341 }

342

343

344

345 static inline llvm::SMTExprRef

347 const llvm::SMTExprRef &LHS, QualType LTy,

350 llvm::SMTExprRef NewLHS = LHS;

351 llvm::SMTExprRef NewRHS = RHS;

353

354

355 if (RetTy) {

356

357

358

361 *RetTy = Ctx.BoolTy;

362 } else {

363 *RetTy = LTy;

364 }

365

366

367

369 *RetTy = Ctx.getPointerDiffType();

370 }

371 }

372

375 : fromBinOp(Solver, NewLHS, Op, NewRHS,

377 }

378

379

380

381 static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver,

384 bool *hasComparison,

388

389 if (const SymIntExpr *SIE = dyn_cast(BSE)) {

390 llvm::SMTExprRef LHS =

391 getSymExpr(Solver, Ctx, SIE->getLHS(), &LTy, 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(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(BSE)) {

410 llvm::SMTExprRef LHS =

411 getSymExpr(Solver, Ctx, SSM->getLHS(), &LTy, 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

421

422 static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,

425 bool *hasComparison) {

426 if (const SymbolData *SD = dyn_cast(Sym)) {

427 if (RetTy)

429

430 return fromData(Solver, Ctx, SD);

431 }

432

433 if (const SymbolCast *SC = dyn_cast(Sym)) {

434 if (RetTy)

436

438 llvm::SMTExprRef Exp =

439 getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);

440

441

442

443

444 if (hasComparison)

445 *hasComparison = false;

447 }

448

449 if (const UnarySymExpr *USE = dyn_cast(Sym)) {

450 if (RetTy)

452

454 llvm::SMTExprRef OperandExp =

455 getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);

456 llvm::SMTExprRef UnaryExp =

458 ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp)

459 : fromUnOp(Solver, USE->getOpcode(), OperandExp);

460

461

462

463

464

465 if (Ctx.getTypeSize(OperandTy) != Ctx.getTypeSize(Sym->getType())) {

466 if (hasComparison)

467 *hasComparison = false;

468 return getCastExpr(Solver, Ctx, UnaryExp, OperandTy, Sym->getType());

469 }

470 return UnaryExp;

471 }

472

473 if (const BinarySymExpr *BSE = dyn_cast(Sym)) {

474 llvm::SMTExprRef Exp =

475 getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);

476

477 if (hasComparison)

479 return Exp;

480 }

481

482 llvm_unreachable("Unsupported SymbolRef type!");

483 }

484

485

486

487

488

489 static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,

492 bool *hasComparison = nullptr) {

493 if (hasComparison) {

494 *hasComparison = false;

495 }

496

497 return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);

498 }

499

500

501 static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver,

503 const llvm::SMTExprRef &Exp,

504 QualType Ty, bool Assumption) {

506 llvm::APFloat Zero =

507 llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));

508 return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,

509 Solver->mkFloat(Zero));

510 }

511

514

515

518 return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;

519

521 Solver, Exp, Assumption ? BO_EQ : BO_NE,

522 Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),

523 isSigned);

524 }

525

526 llvm_unreachable("Unsupported type for zero value!");

527 }

528

529

530

531 static inline llvm::SMTExprRef

533 const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) {

534

536 llvm::APSInt NewFromInt;

537 std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);

538 llvm::SMTExprRef FromExp =

539 Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());

540

541

543 llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);

544

545

546 if (From == To)

547 return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,

548 FromExp, FromTy, nullptr);

549

551 llvm::APSInt NewToInt;

552 std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);

553 llvm::SMTExprRef ToExp =

554 Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());

555 assert(FromTy == ToTy && "Range values have different types!");

556

557

558 llvm::SMTExprRef LHS =

559 getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,

560 FromTy, nullptr);

561 llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,

562 InRange ? BO_LE : BO_GT, ToExp, ToTy,

563 nullptr);

564

565 return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,

567 }

568

569

570

572 const llvm::APSInt &Int) {

573 return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());

574 }

575

576

577 static inline std::pair<llvm::APSInt, QualType>

579 llvm::APSInt NewInt;

580

581

582

583

584 if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) {

585 NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));

586 } else

587 NewInt = Int;

588

589 return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));

590 }

591

592

593

594

596 ASTContext &Ctx, llvm::SMTExprRef &LHS,

597 llvm::SMTExprRef &RHS, QualType &LTy,

599 assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");

600

601

605 SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(

606 Solver, Ctx, LHS, LTy, RHS, RTy);

607 return;

608 }

609

611 SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(

612 Solver, Ctx, LHS, LTy, RHS, RTy);

613 return;

614 }

615

619

620

621

622 uint64_t LBitWidth = Ctx.getTypeSize(LTy);

623 uint64_t RBitWidth = Ctx.getTypeSize(RTy);

624

625

626

632 LHS = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

633 LTy = RTy;

634 } else {

635 RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

636 RTy = LTy;

637 }

638 }

639

640

641

642

643

645 assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&

646 "Pointer types have different bitwidths!");

648 RTy = LTy;

649 else

650 LTy = RTy;

651 }

652

653 if (LTy == RTy)

654 return;

655 }

656

657

660 LTy = RTy;

661 return;

662 }

663

664

665 }

666

667

668

669

670 template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,

675 uint64_t LBitWidth = Ctx.getTypeSize(LTy);

676 uint64_t RBitWidth = Ctx.getTypeSize(RTy);

677

678 assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");

679

680

681 if (Ctx.isPromotableIntegerType(LTy)) {

682 QualType NewTy = Ctx.getPromotedIntegerType(LTy);

683 uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);

684 LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);

685 LTy = NewTy;

686 LBitWidth = NewBitWidth;

687 }

688 if (Ctx.isPromotableIntegerType(RTy)) {

689 QualType NewTy = Ctx.getPromotedIntegerType(RTy);

690 uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);

691 RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);

692 RTy = NewTy;

693 RBitWidth = NewBitWidth;

694 }

695

696 if (LTy == RTy)

697 return;

698

699

700

703

704 int order = Ctx.getIntegerTypeOrder(LTy, RTy);

705 if (isLSignedTy == isRSignedTy) {

706

707 if (order == 1) {

708 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

709 RTy = LTy;

710 } else {

711 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

712 LTy = RTy;

713 }

714 } else if (order != (isLSignedTy ? 1 : -1)) {

715

716

717 if (isRSignedTy) {

718 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

719 RTy = LTy;

720 } else {

721 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

722 LTy = RTy;

723 }

724 } else if (LBitWidth != RBitWidth) {

725

726

727

728 if (isLSignedTy) {

729 RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

730 RTy = LTy;

731 } else {

732 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

733 LTy = RTy;

734 }

735 } else {

736

737

738

739

741 Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);

742 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

743 RTy = NewTy;

744 LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

745 LTy = NewTy;

746 }

747 }

748

749

750

751

752 template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,

754 static inline void

757 uint64_t LBitWidth = Ctx.getTypeSize(LTy);

758 uint64_t RBitWidth = Ctx.getTypeSize(RTy);

759

760

762 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

763 LTy = RTy;

764 LBitWidth = RBitWidth;

765 }

767 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

768 RTy = LTy;

769 RBitWidth = LBitWidth;

770 }

771

772 if (LTy == RTy)

773 return;

774

775

776

777

778 int order = Ctx.getFloatingTypeOrder(LTy, RTy);

779 if (order > 0) {

780 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);

781 RTy = LTy;

782 } else if (order == 0) {

783 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);

784 LTy = RTy;

785 } else {

786 llvm_unreachable("Unsupported floating-point type cast!");

787 }

788 }

789};

790}

791}

792

793#endif

Holds long-lived AST nodes (such as types and decls) that can be referred to throughout the semantic ...

bool isComparisonOp() const

A (possibly-)qualified type.

bool isNull() const

Return true if this QualType doesn't point to a type yet.

QualType getCanonicalType() const

bool isBlockPointerType() const

bool isBooleanType() const

bool isSignedIntegerOrEnumerationType() const

Determines whether this is an integer type that is signed or an enumeration types whose underlying ty...

bool isVoidPointerType() const

bool isArithmeticType() const

bool isReferenceType() const

bool isIntegralOrEnumerationType() const

Determine whether this type is an integral or enumeration type.

bool isObjCObjectPointerType() const

bool isRealFloatingType() const

Floating point categories.

bool isAnyPointerType() const

bool isNullPtrType() const

A record of the "type" of an APSInt, used for conversions.

llvm::APSInt convert(const llvm::APSInt &Value) const LLVM_READONLY

Convert and return a new APSInt with the given value, but this type's bit width and signedness.

Template implementation for all binary symbolic expressions.

Represents a symbolic expression involving a binary operator.

BinaryOperator::Opcode getOpcode() const

static llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, const QualType &Ty, unsigned BitWidth)

static llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS)

Construct an SMTSolverRef from a floating-point binary operator.

static QualType getAPSIntType(ASTContext &Ctx, const llvm::APSInt &Int)

static llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType Ty, bool Assumption)

static void doIntTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy)

static llvm::SMTExprRef getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)

static llvm::SMTExprRef fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op, const std::vector< llvm::SMTExprRef > &ASTs)

Construct an SMTSolverRef from a n-ary binary operator.

static llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy, bool *hasComparison)

static llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy=nullptr, bool *hasComparison=nullptr)

static void doTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, llvm::SMTExprRef &LHS, llvm::SMTExprRef &RHS, QualType &LTy, QualType &RTy)

static llvm::SMTExprRef fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::APFloat::fltCategory &RHS)

Construct an SMTSolverRef from a special floating-point binary operator.

static llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym)

Construct an SMTSolverRef from a SymbolData.

static void doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS, QualType &RTy)

static llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const BinarySymExpr *BSE, bool *hasComparison, QualType *RetTy)

static llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, bool isSigned)

Construct an SMTSolverRef from a binary operator.

static llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType FromTy, QualType ToTy)

static 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)

static std::pair< llvm::APSInt, QualType > fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int)

static llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &Exp, QualType ToTy, uint64_t ToBitWidth, QualType FromTy, uint64_t FromBitWidth)

Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy, and their bit widths.

static llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver, const llvm::APSInt &V, QualType ToTy, uint64_t ToWidth, QualType FromTy, uint64_t FromWidth)

static llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef &Exp)

Constructs an SMTSolverRef from a floating-point unary operator.

static llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, const UnaryOperator::Opcode Op, const llvm::SMTExprRef &Exp)

Constructs an SMTSolverRef from an unary operator.

virtual QualType getType() const =0

SymbolID getSymbolID() const

Get a unique identifier for this symbol.

Represents a cast expression.

A symbol representing data which can be stored in a memory location (region).

virtual StringRef getKindStr() const =0

Get a string representation of the kind of the region.

Represents a symbolic expression involving a unary operator.

@ OS

Indicates that the tracking object is a descendant of a referenced-counted OSObject,...

The JSON file list parser is used to communicate input to InstallAPI.

const FunctionProtoType * T