Back to home page

EIC code displayed by LXR
 
 

    

File indexing completed on 2026-05-10 08:37:09 

0001 //== SMTConv.h --------------------------------------------------*- C++ -*--==//
0002 //
0003 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
0004 // See https://llvm.org/LICENSE.txt for license information.
0005 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
0006 //
0007 //===----------------------------------------------------------------------===//
0008 //
0009 //  This file defines a set of functions to create SMT expressions
0010 //
0011 //===----------------------------------------------------------------------===//
0012 
0013 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
0014 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
0015 
0016 #include "clang/AST/Expr.h"
0017 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
0018 #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
0019 #include "llvm/Support/SMTAPI.h"
0020 
0021 namespace clang {
0022 namespace ento {
0023 
0024 class SMTConv {
0025 public:
0026   // Returns an appropriate sort, given a QualType and it's bit width.
0027   static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,
0028                                         const QualType &Ty, unsigned BitWidth) {
0029     if (Ty->isBooleanType())
0030       return Solver->getBoolSort();
0031 
0032     if (Ty->isRealFloatingType())
0033       return Solver->getFloatSort(BitWidth);
0034 
0035     return Solver->getBitvectorSort(BitWidth);
0036   }
0037 
0038   /// Constructs an SMTSolverRef from an unary operator.
0039   static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver,
0040                                           const UnaryOperator::Opcode Op,
0041                                           const llvm::SMTExprRef &Exp) {
0042     switch (Op) {
0043     case UO_Minus:
0044       return Solver->mkBVNeg(Exp);
0045 
0046     case UO_Not:
0047       return Solver->mkBVNot(Exp);
0048 
0049     case UO_LNot:
0050       return Solver->mkNot(Exp);
0051 
0052     default:;
0053     }
0054     llvm_unreachable("Unimplemented opcode");
0055   }
0056 
0057   /// Constructs an SMTSolverRef from a floating-point unary operator.
0058   static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver,
0059                                                const UnaryOperator::Opcode Op,
0060                                                const llvm::SMTExprRef &Exp) {
0061     switch (Op) {
0062     case UO_Minus:
0063       return Solver->mkFPNeg(Exp);
0064 
0065     case UO_LNot:
0066       return fromUnOp(Solver, Op, Exp);
0067 
0068     default:;
0069     }
0070     llvm_unreachable("Unimplemented opcode");
0071   }
0072 
0073   /// Construct an SMTSolverRef from a n-ary binary operator.
0074   static inline llvm::SMTExprRef
0075   fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op,
0076              const std::vector<llvm::SMTExprRef> &ASTs) {
0077     assert(!ASTs.empty());
0078 
0079     if (Op != BO_LAnd && Op != BO_LOr)
0080       llvm_unreachable("Unimplemented opcode");
0081 
0082     llvm::SMTExprRef res = ASTs.front();
0083     for (std::size_t i = 1; i < ASTs.size(); ++i)
0084       res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])
0085                             : Solver->mkOr(res, ASTs[i]);
0086     return res;
0087   }
0088 
0089   /// Construct an SMTSolverRef from a binary operator.
0090   static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver,
0091                                            const llvm::SMTExprRef &LHS,
0092                                            const BinaryOperator::Opcode Op,
0093                                            const llvm::SMTExprRef &RHS,
0094                                            bool isSigned) {
0095     assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
0096            "AST's must have the same sort!");
0097 
0098     switch (Op) {
0099     // Multiplicative operators
0100     case BO_Mul:
0101       return Solver->mkBVMul(LHS, RHS);
0102 
0103     case BO_Div:
0104       return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);
0105 
0106     case BO_Rem:
0107       return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);
0108 
0109       // Additive operators
0110     case BO_Add:
0111       return Solver->mkBVAdd(LHS, RHS);
0112 
0113     case BO_Sub:
0114       return Solver->mkBVSub(LHS, RHS);
0115 
0116       // Bitwise shift operators
0117     case BO_Shl:
0118       return Solver->mkBVShl(LHS, RHS);
0119 
0120     case BO_Shr:
0121       return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);
0122 
0123       // Relational operators
0124     case BO_LT:
0125       return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);
0126 
0127     case BO_GT:
0128       return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);
0129 
0130     case BO_LE:
0131       return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);
0132 
0133     case BO_GE:
0134       return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);
0135 
0136       // Equality operators
0137     case BO_EQ:
0138       return Solver->mkEqual(LHS, RHS);
0139 
0140     case BO_NE:
0141       return fromUnOp(Solver, UO_LNot,
0142                       fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned));
0143 
0144       // Bitwise operators
0145     case BO_And:
0146       return Solver->mkBVAnd(LHS, RHS);
0147 
0148     case BO_Xor:
0149       return Solver->mkBVXor(LHS, RHS);
0150 
0151     case BO_Or:
0152       return Solver->mkBVOr(LHS, RHS);
0153 
0154       // Logical operators
0155     case BO_LAnd:
0156       return Solver->mkAnd(LHS, RHS);
0157 
0158     case BO_LOr:
0159       return Solver->mkOr(LHS, RHS);
0160 
0161     default:;
0162     }
0163     llvm_unreachable("Unimplemented opcode");
0164   }
0165 
0166   /// Construct an SMTSolverRef from a special floating-point binary
0167   /// operator.
0168   static inline llvm::SMTExprRef
0169   fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS,
0170                         const BinaryOperator::Opcode Op,
0171                         const llvm::APFloat::fltCategory &RHS) {
0172     switch (Op) {
0173     // Equality operators
0174     case BO_EQ:
0175       switch (RHS) {
0176       case llvm::APFloat::fcInfinity:
0177         return Solver->mkFPIsInfinite(LHS);
0178 
0179       case llvm::APFloat::fcNaN:
0180         return Solver->mkFPIsNaN(LHS);
0181 
0182       case llvm::APFloat::fcNormal:
0183         return Solver->mkFPIsNormal(LHS);
0184 
0185       case llvm::APFloat::fcZero:
0186         return Solver->mkFPIsZero(LHS);
0187       }
0188       break;
0189 
0190     case BO_NE:
0191       return fromFloatUnOp(Solver, UO_LNot,
0192                            fromFloatSpecialBinOp(Solver, LHS, BO_EQ, RHS));
0193 
0194     default:;
0195     }
0196 
0197     llvm_unreachable("Unimplemented opcode");
0198   }
0199 
0200   /// Construct an SMTSolverRef from a floating-point binary operator.
0201   static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver,
0202                                                 const llvm::SMTExprRef &LHS,
0203                                                 const BinaryOperator::Opcode Op,
0204                                                 const llvm::SMTExprRef &RHS) {
0205     assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
0206            "AST's must have the same sort!");
0207 
0208     switch (Op) {
0209     // Multiplicative operators
0210     case BO_Mul:
0211       return Solver->mkFPMul(LHS, RHS);
0212 
0213     case BO_Div:
0214       return Solver->mkFPDiv(LHS, RHS);
0215 
0216     case BO_Rem:
0217       return Solver->mkFPRem(LHS, RHS);
0218 
0219       // Additive operators
0220     case BO_Add:
0221       return Solver->mkFPAdd(LHS, RHS);
0222 
0223     case BO_Sub:
0224       return Solver->mkFPSub(LHS, RHS);
0225 
0226       // Relational operators
0227     case BO_LT:
0228       return Solver->mkFPLt(LHS, RHS);
0229 
0230     case BO_GT:
0231       return Solver->mkFPGt(LHS, RHS);
0232 
0233     case BO_LE:
0234       return Solver->mkFPLe(LHS, RHS);
0235 
0236     case BO_GE:
0237       return Solver->mkFPGe(LHS, RHS);
0238 
0239       // Equality operators
0240     case BO_EQ:
0241       return Solver->mkFPEqual(LHS, RHS);
0242 
0243     case BO_NE:
0244       return fromFloatUnOp(Solver, UO_LNot,
0245                            fromFloatBinOp(Solver, LHS, BO_EQ, RHS));
0246 
0247       // Logical operators
0248     case BO_LAnd:
0249     case BO_LOr:
0250       return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false);
0251 
0252     default:;
0253     }
0254 
0255     llvm_unreachable("Unimplemented opcode");
0256   }
0257 
0258   /// Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy,
0259   /// and their bit widths.
0260   static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver,
0261                                           const llvm::SMTExprRef &Exp,
0262                                           QualType ToTy, uint64_t ToBitWidth,
0263                                           QualType FromTy,
0264                                           uint64_t FromBitWidth) {
0265     if ((FromTy->isIntegralOrEnumerationType() &&
0266          ToTy->isIntegralOrEnumerationType()) ||
0267         (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
0268         (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
0269         (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
0270 
0271       if (FromTy->isBooleanType()) {
0272         assert(ToBitWidth > 0 && "BitWidth must be positive!");
0273         return Solver->mkIte(
0274             Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth),
0275             Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth));
0276       }
0277 
0278       if (ToBitWidth > FromBitWidth)
0279         return FromTy->isSignedIntegerOrEnumerationType()
0280                    ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
0281                    : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
0282 
0283       if (ToBitWidth < FromBitWidth)
0284         return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
0285 
0286       // Both are bitvectors with the same width, ignore the type cast
0287       return Exp;
0288     }
0289 
0290     if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
0291       if (ToBitWidth != FromBitWidth)
0292         return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
0293 
0294       return Exp;
0295     }
0296 
0297     if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
0298       llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
0299       return FromTy->isSignedIntegerOrEnumerationType()
0300                  ? Solver->mkSBVtoFP(Exp, Sort)
0301                  : Solver->mkUBVtoFP(Exp, Sort);
0302     }
0303 
0304     if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
0305       return ToTy->isSignedIntegerOrEnumerationType()
0306                  ? Solver->mkFPtoSBV(Exp, ToBitWidth)
0307                  : Solver->mkFPtoUBV(Exp, ToBitWidth);
0308 
0309     llvm_unreachable("Unsupported explicit type cast!");
0310   }
0311 
0312   // Callback function for doCast parameter on APSInt type.
0313   static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver,
0314                                         const llvm::APSInt &V, QualType ToTy,
0315                                         uint64_t ToWidth, QualType FromTy,
0316                                         uint64_t FromWidth) {
0317     APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
0318     return TargetType.convert(V);
0319   }
0320 
0321   /// Construct an SMTSolverRef from a SymbolData.
0322   static inline llvm::SMTExprRef
0323   fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) {
0324     const SymbolID ID = Sym->getSymbolID();
0325     const QualType Ty = Sym->getType();
0326     const uint64_t BitWidth = Ctx.getTypeSize(Ty);
0327 
0328     llvm::SmallString<16> Str;
0329     llvm::raw_svector_ostream OS(Str);
0330     OS << Sym->getKindStr() << ID;
0331     return Solver->mkSymbol(Str.c_str(), mkSort(Solver, Ty, BitWidth));
0332   }
0333 
0334   // Wrapper to generate SMTSolverRef from SymbolCast data.
0335   static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,
0336                                              ASTContext &Ctx,
0337                                              const llvm::SMTExprRef &Exp,
0338                                              QualType FromTy, QualType ToTy) {
0339     return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
0340                     Ctx.getTypeSize(FromTy));
0341   }
0342 
0343   // Wrapper to generate SMTSolverRef from unpacked binary symbolic
0344   // expression. Sets the RetTy parameter. See getSMTSolverRef().
0345   static inline llvm::SMTExprRef
0346   getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
0347              const llvm::SMTExprRef &LHS, QualType LTy,
0348              BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS,
0349              QualType RTy, QualType *RetTy) {
0350     llvm::SMTExprRef NewLHS = LHS;
0351     llvm::SMTExprRef NewRHS = RHS;
0352     doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
0353 
0354     // Update the return type parameter if the output type has changed.
0355     if (RetTy) {
0356       // A boolean result can be represented as an integer type in C/C++, but at
0357       // this point we only care about the SMT sorts. Set it as a boolean type
0358       // to avoid subsequent SMT errors.
0359       if (BinaryOperator::isComparisonOp(Op) ||
0360           BinaryOperator::isLogicalOp(Op)) {
0361         *RetTy = Ctx.BoolTy;
0362       } else {
0363         *RetTy = LTy;
0364       }
0365 
0366       // If the two operands are pointers and the operation is a subtraction,
0367       // the result is of type ptrdiff_t, which is signed
0368       if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) {
0369         *RetTy = Ctx.getPointerDiffType();
0370       }
0371     }
0372 
0373     return LTy->isRealFloatingType()
0374                ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS)
0375                : fromBinOp(Solver, NewLHS, Op, NewRHS,
0376                            LTy->isSignedIntegerOrEnumerationType());
0377   }
0378 
0379   // Wrapper to generate SMTSolverRef from BinarySymExpr.
0380   // Sets the hasComparison and RetTy parameters. See getSMTSolverRef().
0381   static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver,
0382                                                ASTContext &Ctx,
0383                                                const BinarySymExpr *BSE,
0384                                                bool *hasComparison,
0385                                                QualType *RetTy) {
0386     QualType LTy, RTy;
0387     BinaryOperator::Opcode Op = BSE->getOpcode();
0388 
0389     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
0390       llvm::SMTExprRef LHS =
0391           getSymExpr(Solver, Ctx, SIE->getLHS(), &LTy, hasComparison);
0392       llvm::APSInt NewRInt;
0393       std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
0394       llvm::SMTExprRef RHS =
0395           Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
0396       return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
0397     }
0398 
0399     if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
0400       llvm::APSInt NewLInt;
0401       std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
0402       llvm::SMTExprRef LHS =
0403           Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
0404       llvm::SMTExprRef RHS =
0405           getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
0406       return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
0407     }
0408 
0409     if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
0410       llvm::SMTExprRef LHS =
0411           getSymExpr(Solver, Ctx, SSM->getLHS(), &LTy, hasComparison);
0412       llvm::SMTExprRef RHS =
0413           getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
0414       return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
0415     }
0416 
0417     llvm_unreachable("Unsupported BinarySymExpr type!");
0418   }
0419 
0420   // Recursive implementation to unpack and generate symbolic expression.
0421   // Sets the hasComparison and RetTy parameters. See getExpr().
0422   static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
0423                                             ASTContext &Ctx, SymbolRef Sym,
0424                                             QualType *RetTy,
0425                                             bool *hasComparison) {
0426     if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
0427       if (RetTy)
0428         *RetTy = Sym->getType();
0429 
0430       return fromData(Solver, Ctx, SD);
0431     }
0432 
0433     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
0434       if (RetTy)
0435         *RetTy = Sym->getType();
0436 
0437       QualType FromTy;
0438       llvm::SMTExprRef Exp =
0439           getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
0440 
0441       // Casting an expression with a comparison invalidates it. Note that this
0442       // must occur after the recursive call above.
0443       // e.g. (signed char) (x > 0)
0444       if (hasComparison)
0445         *hasComparison = false;
0446       return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
0447     }
0448 
0449     if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
0450       if (RetTy)
0451         *RetTy = Sym->getType();
0452 
0453       QualType OperandTy;
0454       llvm::SMTExprRef OperandExp =
0455           getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
0456       llvm::SMTExprRef UnaryExp =
0457           OperandTy->isRealFloatingType()
0458               ? fromFloatUnOp(Solver, USE->getOpcode(), OperandExp)
0459               : fromUnOp(Solver, USE->getOpcode(), OperandExp);
0460 
0461       // Currently, without the `support-symbolic-integer-casts=true` option,
0462       // we do not emit `SymbolCast`s for implicit casts.
0463       // One such implicit cast is missing if the operand of the unary operator
0464       // has a different type than the unary itself.
0465       if (Ctx.getTypeSize(OperandTy) != Ctx.getTypeSize(Sym->getType())) {
0466         if (hasComparison)
0467           *hasComparison = false;
0468         return getCastExpr(Solver, Ctx, UnaryExp, OperandTy, Sym->getType());
0469       }
0470       return UnaryExp;
0471     }
0472 
0473     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
0474       llvm::SMTExprRef Exp =
0475           getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
0476       // Set the hasComparison parameter, in post-order traversal order.
0477       if (hasComparison)
0478         *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
0479       return Exp;
0480     }
0481 
0482     llvm_unreachable("Unsupported SymbolRef type!");
0483   }
0484 
0485   // Generate an SMTSolverRef that represents the given symbolic expression.
0486   // Sets the hasComparison parameter if the expression has a comparison
0487   // operator. Sets the RetTy parameter to the final return type after
0488   // promotions and casts.
0489   static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
0490                                          ASTContext &Ctx, SymbolRef Sym,
0491                                          QualType *RetTy = nullptr,
0492                                          bool *hasComparison = nullptr) {
0493     if (hasComparison) {
0494       *hasComparison = false;
0495     }
0496 
0497     return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
0498   }
0499 
0500   // Generate an SMTSolverRef that compares the expression to zero.
0501   static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver,
0502                                              ASTContext &Ctx,
0503                                              const llvm::SMTExprRef &Exp,
0504                                              QualType Ty, bool Assumption) {
0505     if (Ty->isRealFloatingType()) {
0506       llvm::APFloat Zero =
0507           llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
0508       return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
0509                             Solver->mkFloat(Zero));
0510     }
0511 
0512     if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
0513         Ty->isBlockPointerType() || Ty->isReferenceType()) {
0514 
0515       // Skip explicit comparison for boolean types
0516       bool isSigned = Ty->isSignedIntegerOrEnumerationType();
0517       if (Ty->isBooleanType())
0518         return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
0519 
0520       return fromBinOp(
0521           Solver, Exp, Assumption ? BO_EQ : BO_NE,
0522           Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)),
0523           isSigned);
0524     }
0525 
0526     llvm_unreachable("Unsupported type for zero value!");
0527   }
0528 
0529   // Wrapper to generate SMTSolverRef from a range. If From == To, an
0530   // equality will be created instead.
0531   static inline llvm::SMTExprRef
0532   getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
0533                const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) {
0534     // Convert lower bound
0535     QualType FromTy;
0536     llvm::APSInt NewFromInt;
0537     std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
0538     llvm::SMTExprRef FromExp =
0539         Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
0540 
0541     // Convert symbol
0542     QualType SymTy;
0543     llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
0544 
0545     // Construct single (in)equality
0546     if (From == To)
0547       return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
0548                         FromExp, FromTy, /*RetTy=*/nullptr);
0549 
0550     QualType ToTy;
0551     llvm::APSInt NewToInt;
0552     std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
0553     llvm::SMTExprRef ToExp =
0554         Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
0555     assert(FromTy == ToTy && "Range values have different types!");
0556 
0557     // Construct two (in)equalities, and a logical and/or
0558     llvm::SMTExprRef LHS =
0559         getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
0560                    FromTy, /*RetTy=*/nullptr);
0561     llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
0562                                       InRange ? BO_LE : BO_GT, ToExp, ToTy,
0563                                       /*RetTy=*/nullptr);
0564 
0565     return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
0566                      SymTy->isSignedIntegerOrEnumerationType());
0567   }
0568 
0569   // Recover the QualType of an APSInt.
0570   // TODO: Refactor to put elsewhere
0571   static inline QualType getAPSIntType(ASTContext &Ctx,
0572                                        const llvm::APSInt &Int) {
0573     return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
0574   }
0575 
0576   // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
0577   static inline std::pair<llvm::APSInt, QualType>
0578   fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) {
0579     llvm::APSInt NewInt;
0580 
0581     // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
0582     // but the former is not available in Clang. Instead, extend the APSInt
0583     // directly.
0584     if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) {
0585       NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
0586     } else
0587       NewInt = Int;
0588 
0589     return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
0590   }
0591 
0592   // Perform implicit type conversion on binary symbolic expressions.
0593   // May modify all input parameters.
0594   // TODO: Refactor to use built-in conversion functions
0595   static inline void doTypeConversion(llvm::SMTSolverRef &Solver,
0596                                       ASTContext &Ctx, llvm::SMTExprRef &LHS,
0597                                       llvm::SMTExprRef &RHS, QualType &LTy,
0598                                       QualType &RTy) {
0599     assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
0600 
0601     // Perform type conversion
0602     if ((LTy->isIntegralOrEnumerationType() &&
0603          RTy->isIntegralOrEnumerationType()) &&
0604         (LTy->isArithmeticType() && RTy->isArithmeticType())) {
0605       SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(
0606           Solver, Ctx, LHS, LTy, RHS, RTy);
0607       return;
0608     }
0609 
0610     if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
0611       SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
0612           Solver, Ctx, LHS, LTy, RHS, RTy);
0613       return;
0614     }
0615 
0616     if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
0617         (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
0618         (LTy->isReferenceType() || RTy->isReferenceType())) {
0619       // TODO: Refactor to Sema::FindCompositePointerType(), and
0620       // Sema::CheckCompareOperands().
0621 
0622       uint64_t LBitWidth = Ctx.getTypeSize(LTy);
0623       uint64_t RBitWidth = Ctx.getTypeSize(RTy);
0624 
0625       // Cast the non-pointer type to the pointer type.
0626       // TODO: Be more strict about this.
0627       if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
0628           (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
0629           (LTy->isReferenceType() ^ RTy->isReferenceType())) {
0630         if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
0631             LTy->isReferenceType()) {
0632           LHS = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
0633           LTy = RTy;
0634         } else {
0635           RHS = fromCast(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
0636           RTy = LTy;
0637         }
0638       }
0639 
0640       // Cast the void pointer type to the non-void pointer type.
0641       // For void types, this assumes that the casted value is equal to the
0642       // value of the original pointer, and does not account for alignment
0643       // requirements.
0644       if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
0645         assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
0646                "Pointer types have different bitwidths!");
0647         if (RTy->isVoidPointerType())
0648           RTy = LTy;
0649         else
0650           LTy = RTy;
0651       }
0652 
0653       if (LTy == RTy)
0654         return;
0655     }
0656 
0657     // Fallback: for the solver, assume that these types don't really matter
0658     if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
0659         (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
0660       LTy = RTy;
0661       return;
0662     }
0663 
0664     // TODO: Refine behavior for invalid type casts
0665   }
0666 
0667   // Perform implicit integer type conversion.
0668   // May modify all input parameters.
0669   // TODO: Refactor to use Sema::handleIntegerConversion()
0670   template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
0671                                     QualType, uint64_t, QualType, uint64_t)>
0672   static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver,
0673                                          ASTContext &Ctx, T &LHS, QualType &LTy,
0674                                          T &RHS, QualType &RTy) {
0675     uint64_t LBitWidth = Ctx.getTypeSize(LTy);
0676     uint64_t RBitWidth = Ctx.getTypeSize(RTy);
0677 
0678     assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
0679     // Always perform integer promotion before checking type equality.
0680     // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
0681     if (Ctx.isPromotableIntegerType(LTy)) {
0682       QualType NewTy = Ctx.getPromotedIntegerType(LTy);
0683       uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
0684       LHS = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
0685       LTy = NewTy;
0686       LBitWidth = NewBitWidth;
0687     }
0688     if (Ctx.isPromotableIntegerType(RTy)) {
0689       QualType NewTy = Ctx.getPromotedIntegerType(RTy);
0690       uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
0691       RHS = (*doCast)(Solver, RHS, NewTy, NewBitWidth, RTy, RBitWidth);
0692       RTy = NewTy;
0693       RBitWidth = NewBitWidth;
0694     }
0695 
0696     if (LTy == RTy)
0697       return;
0698 
0699     // Perform integer type conversion
0700     // Note: Safe to skip updating bitwidth because this must terminate
0701     bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
0702     bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
0703 
0704     int order = Ctx.getIntegerTypeOrder(LTy, RTy);
0705     if (isLSignedTy == isRSignedTy) {
0706       // Same signedness; use the higher-ranked type
0707       if (order == 1) {
0708         RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
0709         RTy = LTy;
0710       } else {
0711         LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
0712         LTy = RTy;
0713       }
0714     } else if (order != (isLSignedTy ? 1 : -1)) {
0715       // The unsigned type has greater than or equal rank to the
0716       // signed type, so use the unsigned type
0717       if (isRSignedTy) {
0718         RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
0719         RTy = LTy;
0720       } else {
0721         LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
0722         LTy = RTy;
0723       }
0724     } else if (LBitWidth != RBitWidth) {
0725       // The two types are different widths; if we are here, that
0726       // means the signed type is larger than the unsigned type, so
0727       // use the signed type.
0728       if (isLSignedTy) {
0729         RHS = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
0730         RTy = LTy;
0731       } else {
0732         LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
0733         LTy = RTy;
0734       }
0735     } else {
0736       // The signed type is higher-ranked than the unsigned type,
0737       // but isn't actually any bigger (like unsigned int and long
0738       // on most 32-bit systems).  Use the unsigned type corresponding
0739       // to the signed type.
0740       QualType NewTy =
0741           Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
0742       RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
0743       RTy = NewTy;
0744       LHS = (doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
0745       LTy = NewTy;
0746     }
0747   }
0748 
0749   // Perform implicit floating-point type conversion.
0750   // May modify all input parameters.
0751   // TODO: Refactor to use Sema::handleFloatConversion()
0752   template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
0753                                     QualType, uint64_t, QualType, uint64_t)>
0754   static inline void
0755   doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
0756                         QualType &LTy, T &RHS, QualType &RTy) {
0757     uint64_t LBitWidth = Ctx.getTypeSize(LTy);
0758     uint64_t RBitWidth = Ctx.getTypeSize(RTy);
0759 
0760     // Perform float-point type promotion
0761     if (!LTy->isRealFloatingType()) {
0762       LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
0763       LTy = RTy;
0764       LBitWidth = RBitWidth;
0765     }
0766     if (!RTy->isRealFloatingType()) {
0767       RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
0768       RTy = LTy;
0769       RBitWidth = LBitWidth;
0770     }
0771 
0772     if (LTy == RTy)
0773       return;
0774 
0775     // If we have two real floating types, convert the smaller operand to the
0776     // bigger result
0777     // Note: Safe to skip updating bitwidth because this must terminate
0778     int order = Ctx.getFloatingTypeOrder(LTy, RTy);
0779     if (order > 0) {
0780       RHS = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
0781       RTy = LTy;
0782     } else if (order == 0) {
0783       LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
0784       LTy = RTy;
0785     } else {
0786       llvm_unreachable("Unsupported floating-point type cast!");
0787     }
0788   }
0789 };
0790 } // namespace ento
0791 } // namespace clang
0792 
0793 #endif
[ Source navigation ] [ Diff markup ] [ Identifier search ] [ general search ]

This page was automatically generated by the 2.3.7 LXR engine.

The LXR team
Valid CSS 2.1! Valid HTML 4.01!