13 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
14 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
19 #include "llvm/Support/SMTAPI.h"
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);
39 static inline llvm::SMTExprRef
fromUnOp(llvm::SMTSolverRef &Solver,
41 const llvm::SMTExprRef &Exp) {
44 return Solver->mkBVNeg(Exp);
47 return Solver->mkBVNot(Exp);
50 return Solver->mkNot(Exp);
54 llvm_unreachable(
"Unimplemented opcode");
58 static inline llvm::SMTExprRef
fromFloatUnOp(llvm::SMTSolverRef &Solver,
60 const llvm::SMTExprRef &Exp) {
63 return Solver->mkFPNeg(Exp);
70 llvm_unreachable(
"Unimplemented opcode");
74 static inline llvm::SMTExprRef
76 const std::vector<llvm::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();
84 res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])
85 : Solver->mkOr(res, ASTs[i]);
90 static inline llvm::SMTExprRef
fromBinOp(llvm::SMTSolverRef &Solver,
91 const llvm::SMTExprRef &LHS,
93 const llvm::SMTExprRef &RHS,
95 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
96 "AST's must have the same sort!");
101 return Solver->mkBVMul(LHS, RHS);
104 return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);
107 return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);
111 return Solver->mkBVAdd(LHS, RHS);
114 return Solver->mkBVSub(LHS, RHS);
118 return Solver->mkBVShl(LHS, RHS);
121 return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);
125 return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);
128 return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);
131 return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);
134 return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);
138 return Solver->mkEqual(LHS, RHS);
142 fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned));
146 return Solver->mkBVAnd(LHS, RHS);
149 return Solver->mkBVXor(LHS, RHS);
152 return Solver->mkBVOr(LHS, RHS);
156 return Solver->mkAnd(LHS, RHS);
159 return Solver->mkOr(LHS, RHS);
163 llvm_unreachable(
"Unimplemented opcode");
168 static inline llvm::SMTExprRef
171 const llvm::APFloat::fltCategory &RHS) {
176 case llvm::APFloat::fcInfinity:
177 return Solver->mkFPIsInfinite(LHS);
179 case llvm::APFloat::fcNaN:
180 return Solver->mkFPIsNaN(LHS);
182 case llvm::APFloat::fcNormal:
183 return Solver->mkFPIsNormal(LHS);
185 case llvm::APFloat::fcZero:
186 return Solver->mkFPIsZero(LHS);
197 llvm_unreachable(
"Unimplemented opcode");
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!");
211 return Solver->mkFPMul(LHS, RHS);
214 return Solver->mkFPDiv(LHS, RHS);
217 return Solver->mkFPRem(LHS, RHS);
221 return Solver->mkFPAdd(LHS, RHS);
224 return Solver->mkFPSub(LHS, RHS);
228 return Solver->mkFPLt(LHS, RHS);
231 return Solver->mkFPGt(LHS, RHS);
234 return Solver->mkFPLe(LHS, RHS);
237 return Solver->mkFPGe(LHS, RHS);
241 return Solver->mkFPEqual(LHS, RHS);
250 return fromBinOp(Solver, LHS, Op, RHS,
false);
255 llvm_unreachable(
"Unimplemented opcode");
260 static inline llvm::SMTExprRef
fromCast(llvm::SMTSolverRef &Solver,
261 const llvm::SMTExprRef &Exp,
272 assert(ToBitWidth > 0 &&
"BitWidth must be positive!");
273 return Solver->mkIte(
274 Exp, Solver->mkBitvector(
llvm::APSInt(
"1"), ToBitWidth),
278 if (ToBitWidth > FromBitWidth)
280 ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
281 : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
283 if (ToBitWidth < FromBitWidth)
284 return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
291 if (ToBitWidth != FromBitWidth)
292 return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
298 llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
300 ? Solver->mkSBVtoFP(Exp, Sort)
301 : Solver->mkUBVtoFP(Exp, Sort);
306 ? Solver->mkFPtoSBV(Exp, ToBitWidth)
307 : Solver->mkFPtoUBV(Exp, ToBitWidth);
309 llvm_unreachable(
"Unsupported explicit type cast!");
322 static inline llvm::SMTExprRef
329 llvm::raw_svector_ostream
OS(Str);
331 return Solver->mkSymbol(Str.c_str(),
mkSort(Solver, Ty, BitWidth));
335 static inline llvm::SMTExprRef
getCastExpr(llvm::SMTSolverRef &Solver,
337 const llvm::SMTExprRef &Exp,
345 static inline llvm::SMTExprRef
347 const llvm::SMTExprRef &LHS,
QualType LTy,
350 llvm::SMTExprRef NewLHS = LHS;
351 llvm::SMTExprRef NewRHS = RHS;
389 if (
const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
390 llvm::SMTExprRef LHS =
391 getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison);
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);
399 if (
const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
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);
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);
417 llvm_unreachable(
"Unsupported BinarySymExpr type!");
422 static inline llvm::SMTExprRef
getSymExpr(llvm::SMTSolverRef &Solver,
425 bool *hasComparison) {
426 if (
const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
433 if (
const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
438 llvm::SMTExprRef Exp =
439 getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
445 *hasComparison =
false;
449 if (
const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
454 llvm::SMTExprRef OperandExp =
455 getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
456 llvm::SMTExprRef UnaryExp =
457 fromUnOp(Solver, USE->getOpcode(), OperandExp);
465 *hasComparison =
false;
471 if (
const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
472 llvm::SMTExprRef Exp =
480 llvm_unreachable(
"Unsupported SymbolRef type!");
487 static inline llvm::SMTExprRef
getExpr(llvm::SMTSolverRef &Solver,
490 bool *hasComparison =
nullptr) {
492 *hasComparison =
false;
495 return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
499 static inline llvm::SMTExprRef
getZeroExpr(llvm::SMTSolverRef &Solver,
501 const llvm::SMTExprRef &Exp,
507 Solver->mkFloat(
Zero));
516 return Assumption ?
fromUnOp(Solver, UO_LNot, Exp) : Exp;
519 Solver, Exp, Assumption ? BO_EQ : BO_NE,
524 llvm_unreachable(
"Unsupported type for zero value!");
529 static inline llvm::SMTExprRef
535 std::tie(NewFromInt, FromTy) =
fixAPSInt(Ctx, From);
536 llvm::SMTExprRef FromExp =
537 Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
541 llvm::SMTExprRef Exp =
getExpr(Solver, Ctx, Sym, &SymTy);
546 FromExp, FromTy,
nullptr);
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!");
556 llvm::SMTExprRef LHS =
559 llvm::SMTExprRef RHS =
getBinExpr(Solver, Ctx, Exp, SymTy,
560 InRange ? BO_LE : BO_GT, ToExp, ToTy,
575 static inline std::pair<llvm::APSInt, QualType>
582 if (Int.getBitWidth() == 1 &&
getAPSIntType(Ctx, Int).isNull()) {
595 llvm::SMTExprRef &RHS,
QualType <y,
597 assert(!LTy.
isNull() && !RTy.
isNull() &&
"Input type is null!");
603 SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(
604 Solver, Ctx, LHS, LTy, RHS, RTy);
609 SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
610 Solver, Ctx, LHS, LTy, RHS, RTy);
630 LHS =
fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
633 RHS =
fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
644 "Pointer types have different bitwidths!");
668 template <
typename T, T (*doCast)(llvm::SMTSolverRef &Solver,
const T &,
676 assert(!LTy.
isNull() && !RTy.
isNull() &&
"Input type is null!");
682 LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
684 LBitWidth = NewBitWidth;
689 RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);
691 RBitWidth = NewBitWidth;
703 if (isLSignedTy == isRSignedTy) {
706 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
709 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
712 }
else if (order != (isLSignedTy ? 1 : -1)) {
716 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
719 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
722 }
else if (LBitWidth != RBitWidth) {
727 RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
730 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
740 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
742 LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
750 template <
typename T, T (*doCast)(llvm::SMTSolverRef &Solver,
const T &,
760 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
762 LBitWidth = RBitWidth;
765 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
767 RBitWidth = LBitWidth;
778 RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
780 }
else if (order == 0) {
781 LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
784 llvm_unreachable(
"Unsupported floating-point type cast!");