clang: include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h Source File (original) (raw)
1
2
3
4
5
6
7
8
9
10
11
12
13#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
14#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
15
19#include "llvm/Support/SMTAPI.h"
20
22namespace ento {
23
25public:
26
27 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,
28 const QualType &Ty, unsigned BitWidth) {
30 return Solver->getBoolSort();
31
33 return Solver->getFloatSort(BitWidth);
34
35 return Solver->getBitvectorSort(BitWidth);
36 }
37
38
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);
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
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);
64
65 case UO_LNot:
66 return fromUnOp(Solver, Op, Exp);
67
68 default:;
69 }
70 llvm_unreachable("Unimplemented opcode");
71 }
72
73
74 static inline llvm::SMTExprRef
76 const std::vectorllvm::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
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!");
97
98 switch (Op) {
99
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(), <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(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(), <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
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 <y,
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 <y, 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 <y, 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 <y, 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