13#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
14#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
19#include "llvm/Support/SMTAPI.h"
29 static inline llvm::SMTSortRef
mkSort(llvm::SMTSolverRef &Solver,
30 const QualType &Ty,
unsigned BitWidth) {
32 return Solver->getBoolSort();
35 return Solver->getFloatSort(BitWidth);
37 return Solver->getBitvectorSort(BitWidth);
41 static inline llvm::SMTExprRef
fromUnOp(llvm::SMTSolverRef &Solver,
43 const llvm::SMTExprRef &Exp) {
46 return Solver->mkBVNeg(Exp);
49 return Solver->mkBVNot(Exp);
52 return Solver->mkNot(Exp);
56 llvm_unreachable(
"Unimplemented opcode");
60 static inline llvm::SMTExprRef
fromFloatUnOp(llvm::SMTSolverRef &Solver,
62 const llvm::SMTExprRef &Exp) {
65 return Solver->mkFPNeg(Exp);
72 llvm_unreachable(
"Unimplemented opcode");
76 static inline llvm::SMTExprRef
78 const std::vector<llvm::SMTExprRef> &ASTs) {
79 assert(!ASTs.empty());
81 if (Op != BO_LAnd && Op != BO_LOr)
82 llvm_unreachable(
"Unimplemented opcode");
84 llvm::SMTExprRef res = ASTs.front();
85 for (std::size_t i = 1; i < ASTs.size(); ++i)
86 res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])
87 : Solver->mkOr(res, ASTs[i]);
92 static inline llvm::SMTExprRef
fromBinOp(llvm::SMTSolverRef &Solver,
93 const llvm::SMTExprRef &LHS,
95 const llvm::SMTExprRef &RHS,
97 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
98 "AST's must have the same sort!");
103 return Solver->mkBVMul(LHS, RHS);
106 return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);
109 return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);
113 return Solver->mkBVAdd(LHS, RHS);
116 return Solver->mkBVSub(LHS, RHS);
120 return Solver->mkBVShl(LHS, RHS);
123 return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);
127 return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);
130 return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);
133 return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);
136 return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);
140 return Solver->mkEqual(LHS, RHS);
144 fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned));
148 return Solver->mkBVAnd(LHS, RHS);
151 return Solver->mkBVXor(LHS, RHS);
154 return Solver->mkBVOr(LHS, RHS);
158 return Solver->mkAnd(LHS, RHS);
161 return Solver->mkOr(LHS, RHS);
165 llvm_unreachable(
"Unimplemented opcode");
170 static inline llvm::SMTExprRef
173 const llvm::APFloat::fltCategory &RHS) {
178 case llvm::APFloat::fcInfinity:
179 return Solver->mkFPIsInfinite(LHS);
181 case llvm::APFloat::fcNaN:
182 return Solver->mkFPIsNaN(LHS);
184 case llvm::APFloat::fcNormal:
185 return Solver->mkFPIsNormal(LHS);
187 case llvm::APFloat::fcZero:
188 return Solver->mkFPIsZero(LHS);
199 llvm_unreachable(
"Unimplemented opcode");
204 const llvm::SMTExprRef &LHS,
206 const llvm::SMTExprRef &RHS) {
207 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
208 "AST's must have the same sort!");
213 return Solver->mkFPMul(LHS, RHS);
216 return Solver->mkFPDiv(LHS, RHS);
219 return Solver->mkFPRem(LHS, RHS);
223 return Solver->mkFPAdd(LHS, RHS);
226 return Solver->mkFPSub(LHS, RHS);
230 return Solver->mkFPLt(LHS, RHS);
233 return Solver->mkFPGt(LHS, RHS);
236 return Solver->mkFPLe(LHS, RHS);
239 return Solver->mkFPGe(LHS, RHS);
243 return Solver->mkFPEqual(LHS, RHS);
252 return fromBinOp(Solver, LHS, Op, RHS,
false);
257 llvm_unreachable(
"Unimplemented opcode");
262 static inline llvm::SMTExprRef
fromCast(llvm::SMTSolverRef &Solver,
263 const llvm::SMTExprRef &Exp,
266 uint64_t FromBitWidth) {
274 assert(ToBitWidth > 0 &&
"BitWidth must be positive!");
275 return Solver->mkIte(
276 Exp, Solver->mkBitvector(llvm::APSInt(
"1"), ToBitWidth),
277 Solver->mkBitvector(llvm::APSInt(
"0"), ToBitWidth));
280 if (ToBitWidth > FromBitWidth)
282 ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
283 : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
285 if (ToBitWidth < FromBitWidth)
286 return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
293 if (ToBitWidth != FromBitWidth)
294 return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
300 llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
302 ? Solver->mkSBVtoFP(Exp, Sort)
303 : Solver->mkUBVtoFP(Exp, Sort);
308 ? Solver->mkFPtoSBV(Exp, ToBitWidth)
309 : Solver->mkFPtoUBV(Exp, ToBitWidth);
311 llvm_unreachable(
"Unsupported explicit type cast!");
315 static inline llvm::APSInt
castAPSInt(llvm::SMTSolverRef &Solver,
318 uint64_t FromWidth) {
324 static inline llvm::SMTExprRef
328 const uint64_t BitWidth = Ctx.getTypeSize(Ty);
331 llvm::raw_svector_ostream
OS(Str);
333 return Solver->mkSymbol(Str.c_str(),
mkSort(Solver, Ty, BitWidth));
337 static inline llvm::SMTExprRef
getCastExpr(llvm::SMTSolverRef &Solver,
339 const llvm::SMTExprRef &Exp,
341 return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
342 Ctx.getTypeSize(FromTy));
347 static inline llvm::SMTExprRef
349 const llvm::SMTExprRef &LHS,
QualType LTy,
352 llvm::SMTExprRef NewLHS = LHS;
353 llvm::SMTExprRef NewRHS = RHS;
371 *RetTy = Ctx.getPointerDiffType();
391 if (
const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
392 llvm::SMTExprRef LHS =
393 getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison);
394 llvm::APSInt NewRInt;
395 std::tie(NewRInt, RTy) =
fixAPSInt(Ctx, SIE->getRHS());
396 llvm::SMTExprRef RHS =
397 Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
398 return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
401 if (
const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
402 llvm::APSInt NewLInt;
403 std::tie(NewLInt, LTy) =
fixAPSInt(Ctx, ISE->getLHS());
404 llvm::SMTExprRef LHS =
405 Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
406 llvm::SMTExprRef RHS =
407 getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
408 return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
411 if (
const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
412 llvm::SMTExprRef LHS =
413 getSymExpr(Solver, Ctx, SSM->getLHS(), <y, hasComparison);
414 llvm::SMTExprRef RHS =
415 getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
416 return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
419 llvm_unreachable(
"Unsupported BinarySymExpr type!");
424 static inline llvm::SMTExprRef
getSymExpr(llvm::SMTSolverRef &Solver,
427 bool *hasComparison) {
428 if (
const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
435 if (
const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
440 llvm::SMTExprRef Exp =
441 getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
447 *hasComparison =
false;
451 if (
const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
456 llvm::SMTExprRef OperandExp =
457 getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
458 llvm::SMTExprRef UnaryExp =
461 :
fromUnOp(Solver, USE->getOpcode(), OperandExp);
467 if (Ctx.getTypeSize(OperandTy) != Ctx.getTypeSize(Sym->
getType())) {
469 *hasComparison =
false;
475 if (
const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
476 llvm::SMTExprRef Exp =
484 llvm_unreachable(
"Unsupported SymbolRef type!");
491 static inline llvm::SMTExprRef
getExpr(llvm::SMTSolverRef &Solver,
494 bool *hasComparison =
nullptr) {
496 *hasComparison =
false;
499 return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
503 static inline llvm::SMTExprRef
getZeroExpr(llvm::SMTSolverRef &Solver,
505 const llvm::SMTExprRef &Exp,
509 llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
511 Solver->mkFloat(
Zero));
520 return Assumption ?
fromUnOp(Solver, UO_LNot, Exp) : Exp;
523 Solver, Exp, Assumption ? BO_EQ : BO_NE,
524 Solver->mkBitvector(llvm::APSInt(
"0"), Ctx.getTypeSize(Ty)),
528 llvm_unreachable(
"Unsupported type for zero value!");
533 static inline llvm::SMTExprRef
535 const llvm::APSInt &From,
const llvm::APSInt &To,
bool InRange) {
538 llvm::APSInt NewFromInt;
539 std::tie(NewFromInt, FromTy) =
fixAPSInt(Ctx, From);
540 llvm::SMTExprRef FromExp =
541 Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
545 llvm::SMTExprRef Exp =
getExpr(Solver, Ctx, Sym, &SymTy);
549 return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
550 FromExp, FromTy,
nullptr);
553 llvm::APSInt NewToInt;
554 std::tie(NewToInt, ToTy) =
fixAPSInt(Ctx, To);
555 llvm::SMTExprRef ToExp =
556 Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
557 assert(FromTy == ToTy &&
"Range values have different types!");
560 llvm::SMTExprRef LHS =
561 getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
563 llvm::SMTExprRef RHS =
getBinExpr(Solver, Ctx, Exp, SymTy,
564 InRange ? BO_LE : BO_GT, ToExp, ToTy,
567 return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
574 const llvm::APSInt &Int) {
576 Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
582 unsigned CharTypeSize = Ctx.getTypeSize(Ctx.CharTy);
583 unsigned Pow2DestWidth =
584 std::max(llvm::bit_ceil(Int.getBitWidth()), CharTypeSize);
585 return Ctx.getIntTypeForBitwidth(Pow2DestWidth, Int.isSigned());
589 static inline std::pair<llvm::APSInt, QualType>
592 unsigned APSIntBitwidth = Int.getBitWidth();
598 if (APSIntBitwidth == 1 && Ty.
isNull())
599 return {Int.extend(Ctx.getTypeSize(Ctx.BoolTy)),
601 else if (APSIntBitwidth == 1 && !Ty.
isNull())
602 return {Int.extend(Ctx.getTypeSize(
getAPSIntType(Ctx, Int))),
604 if (llvm::isPowerOf2_32(APSIntBitwidth) || Ty.
isNull())
606 return {Int.extend(Ctx.getTypeSize(Ty)), Ty};
614 llvm::SMTExprRef &RHS,
QualType <y,
616 assert(!LTy.
isNull() && !RTy.
isNull() &&
"Input type is null!");
622 SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(
623 Solver, Ctx, LHS, LTy, RHS, RTy);
628 SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
629 Solver, Ctx, LHS, LTy, RHS, RTy);
639 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
640 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
649 LHS =
fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
652 RHS =
fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
662 assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
663 "Pointer types have different bitwidths!");
687 template <
typename T,
T (*doCast)(llvm::SMTSolverRef &Solver,
const T &,
692 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
693 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
695 assert(!LTy.
isNull() && !RTy.
isNull() &&
"Input type is null!");
698 if (Ctx.isPromotableIntegerType(LTy)) {
699 QualType NewTy = Ctx.getPromotedIntegerType(LTy);
700 uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
701 LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
703 LBitWidth = NewBitWidth;
705 if (Ctx.isPromotableIntegerType(RTy)) {
706 QualType NewTy = Ctx.getPromotedIntegerType(RTy);
707 uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
708 RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);
710 RBitWidth = NewBitWidth;
721 int order = Ctx.getIntegerTypeOrder(LTy, RTy);
722 if (isLSignedTy == isRSignedTy) {
725 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
728 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
731 }
else if (order != (isLSignedTy ? 1 : -1)) {
735 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
738 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
741 }
else if (LBitWidth != RBitWidth) {
746 RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
749 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
758 Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
759 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
761 LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
769 template <
typename T,
T (*doCast)(llvm::SMTSolverRef &Solver,
const T &,
774 uint64_t LBitWidth = Ctx.getTypeSize(LTy);
775 uint64_t RBitWidth = Ctx.getTypeSize(RTy);
779 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
781 LBitWidth = RBitWidth;
784 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
786 RBitWidth = LBitWidth;
795 int order = Ctx.getFloatingTypeOrder(LTy, RTy);
797 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
799 }
else if (order == 0) {
800 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
803 llvm_unreachable(
"Unsupported floating-point type cast!");
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