| //== SMTSolver.h ------------------------------------------------*- C++ -*--==// |
| // |
| // The LLVM Compiler Infrastructure |
| // |
| // This file is distributed under the University of Illinois Open Source |
| // License. See LICENSE.TXT for details. |
| // |
| //===----------------------------------------------------------------------===// |
| // |
| // This file defines a SMT generic Solver API, which will be the base class |
| // for every SMT solver specific class. |
| // |
| //===----------------------------------------------------------------------===// |
| |
| #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H |
| #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H |
| |
| #include "clang/AST/Expr.h" |
| #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" |
| #include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h" |
| #include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h" |
| #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" |
| #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" |
| |
| namespace clang { |
| namespace ento { |
| |
| /// Generic base class for SMT Solvers |
| /// |
| /// This class is responsible for wrapping all sorts and expression generation, |
| /// through the mk* methods. It also provides methods to create SMT expressions |
| /// straight from clang's AST, through the from* methods. |
| class SMTSolver { |
| public: |
| SMTSolver() = default; |
| virtual ~SMTSolver() = default; |
| |
| LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); } |
| |
| // Returns an appropriate floating-point sort for the given bitwidth. |
| SMTSortRef getFloatSort(unsigned BitWidth) { |
| switch (BitWidth) { |
| case 16: |
| return getFloat16Sort(); |
| case 32: |
| return getFloat32Sort(); |
| case 64: |
| return getFloat64Sort(); |
| case 128: |
| return getFloat128Sort(); |
| default:; |
| } |
| llvm_unreachable("Unsupported floating-point bitwidth!"); |
| } |
| |
| // Returns an appropriate sort, given a QualType and it's bit width. |
| SMTSortRef mkSort(const QualType &Ty, unsigned BitWidth) { |
| if (Ty->isBooleanType()) |
| return getBoolSort(); |
| |
| if (Ty->isRealFloatingType()) |
| return getFloatSort(BitWidth); |
| |
| return getBitvectorSort(BitWidth); |
| } |
| |
| /// Constructs an SMTExprRef from an unary operator. |
| SMTExprRef fromUnOp(const UnaryOperator::Opcode Op, const SMTExprRef &Exp) { |
| switch (Op) { |
| case UO_Minus: |
| return mkBVNeg(Exp); |
| |
| case UO_Not: |
| return mkBVNot(Exp); |
| |
| case UO_LNot: |
| return mkNot(Exp); |
| |
| default:; |
| } |
| llvm_unreachable("Unimplemented opcode"); |
| } |
| |
| /// Constructs an SMTExprRef from a floating-point unary operator. |
| SMTExprRef fromFloatUnOp(const UnaryOperator::Opcode Op, |
| const SMTExprRef &Exp) { |
| switch (Op) { |
| case UO_Minus: |
| return mkFPNeg(Exp); |
| |
| case UO_LNot: |
| return fromUnOp(Op, Exp); |
| |
| default:; |
| } |
| llvm_unreachable("Unimplemented opcode"); |
| } |
| |
| /// Construct an SMTExprRef from a n-ary binary operator. |
| SMTExprRef fromNBinOp(const BinaryOperator::Opcode Op, |
| const std::vector<SMTExprRef> &ASTs) { |
| assert(!ASTs.empty()); |
| |
| if (Op != BO_LAnd && Op != BO_LOr) |
| llvm_unreachable("Unimplemented opcode"); |
| |
| SMTExprRef res = ASTs.front(); |
| for (std::size_t i = 1; i < ASTs.size(); ++i) |
| res = (Op == BO_LAnd) ? mkAnd(res, ASTs[i]) : mkOr(res, ASTs[i]); |
| return res; |
| } |
| |
| /// Construct an SMTExprRef from a binary operator. |
| SMTExprRef fromBinOp(const SMTExprRef &LHS, const BinaryOperator::Opcode Op, |
| const SMTExprRef &RHS, bool isSigned) { |
| assert(*getSort(LHS) == *getSort(RHS) && "AST's must have the same sort!"); |
| |
| switch (Op) { |
| // Multiplicative operators |
| case BO_Mul: |
| return mkBVMul(LHS, RHS); |
| |
| case BO_Div: |
| return isSigned ? mkBVSDiv(LHS, RHS) : mkBVUDiv(LHS, RHS); |
| |
| case BO_Rem: |
| return isSigned ? mkBVSRem(LHS, RHS) : mkBVURem(LHS, RHS); |
| |
| // Additive operators |
| case BO_Add: |
| return mkBVAdd(LHS, RHS); |
| |
| case BO_Sub: |
| return mkBVSub(LHS, RHS); |
| |
| // Bitwise shift operators |
| case BO_Shl: |
| return mkBVShl(LHS, RHS); |
| |
| case BO_Shr: |
| return isSigned ? mkBVAshr(LHS, RHS) : mkBVLshr(LHS, RHS); |
| |
| // Relational operators |
| case BO_LT: |
| return isSigned ? mkBVSlt(LHS, RHS) : mkBVUlt(LHS, RHS); |
| |
| case BO_GT: |
| return isSigned ? mkBVSgt(LHS, RHS) : mkBVUgt(LHS, RHS); |
| |
| case BO_LE: |
| return isSigned ? mkBVSle(LHS, RHS) : mkBVUle(LHS, RHS); |
| |
| case BO_GE: |
| return isSigned ? mkBVSge(LHS, RHS) : mkBVUge(LHS, RHS); |
| |
| // Equality operators |
| case BO_EQ: |
| return mkEqual(LHS, RHS); |
| |
| case BO_NE: |
| return fromUnOp(UO_LNot, fromBinOp(LHS, BO_EQ, RHS, isSigned)); |
| |
| // Bitwise operators |
| case BO_And: |
| return mkBVAnd(LHS, RHS); |
| |
| case BO_Xor: |
| return mkBVXor(LHS, RHS); |
| |
| case BO_Or: |
| return mkBVOr(LHS, RHS); |
| |
| // Logical operators |
| case BO_LAnd: |
| return mkAnd(LHS, RHS); |
| |
| case BO_LOr: |
| return mkOr(LHS, RHS); |
| |
| default:; |
| } |
| llvm_unreachable("Unimplemented opcode"); |
| } |
| |
| /// Construct an SMTExprRef from a special floating-point binary operator. |
| SMTExprRef fromFloatSpecialBinOp(const SMTExprRef &LHS, |
| const BinaryOperator::Opcode Op, |
| const llvm::APFloat::fltCategory &RHS) { |
| switch (Op) { |
| // Equality operators |
| case BO_EQ: |
| switch (RHS) { |
| case llvm::APFloat::fcInfinity: |
| return mkFPIsInfinite(LHS); |
| |
| case llvm::APFloat::fcNaN: |
| return mkFPIsNaN(LHS); |
| |
| case llvm::APFloat::fcNormal: |
| return mkFPIsNormal(LHS); |
| |
| case llvm::APFloat::fcZero: |
| return mkFPIsZero(LHS); |
| } |
| break; |
| |
| case BO_NE: |
| return fromFloatUnOp(UO_LNot, fromFloatSpecialBinOp(LHS, BO_EQ, RHS)); |
| |
| default:; |
| } |
| |
| llvm_unreachable("Unimplemented opcode"); |
| } |
| |
| /// Construct an SMTExprRef from a floating-point binary operator. |
| SMTExprRef fromFloatBinOp(const SMTExprRef &LHS, |
| const BinaryOperator::Opcode Op, |
| const SMTExprRef &RHS) { |
| assert(*getSort(LHS) == *getSort(RHS) && "AST's must have the same sort!"); |
| |
| switch (Op) { |
| // Multiplicative operators |
| case BO_Mul: |
| return mkFPMul(LHS, RHS); |
| |
| case BO_Div: |
| return mkFPDiv(LHS, RHS); |
| |
| case BO_Rem: |
| return mkFPRem(LHS, RHS); |
| |
| // Additive operators |
| case BO_Add: |
| return mkFPAdd(LHS, RHS); |
| |
| case BO_Sub: |
| return mkFPSub(LHS, RHS); |
| |
| // Relational operators |
| case BO_LT: |
| return mkFPLt(LHS, RHS); |
| |
| case BO_GT: |
| return mkFPGt(LHS, RHS); |
| |
| case BO_LE: |
| return mkFPLe(LHS, RHS); |
| |
| case BO_GE: |
| return mkFPGe(LHS, RHS); |
| |
| // Equality operators |
| case BO_EQ: |
| return mkFPEqual(LHS, RHS); |
| |
| case BO_NE: |
| return fromFloatUnOp(UO_LNot, fromFloatBinOp(LHS, BO_EQ, RHS)); |
| |
| // Logical operators |
| case BO_LAnd: |
| case BO_LOr: |
| return fromBinOp(LHS, Op, RHS, false); |
| |
| default:; |
| } |
| |
| llvm_unreachable("Unimplemented opcode"); |
| } |
| |
| /// Construct an SMTExprRef from a QualType FromTy to a QualType ToTy, and |
| /// their bit widths. |
| SMTExprRef fromCast(const SMTExprRef &Exp, QualType ToTy, uint64_t ToBitWidth, |
| QualType FromTy, uint64_t FromBitWidth) { |
| if ((FromTy->isIntegralOrEnumerationType() && |
| ToTy->isIntegralOrEnumerationType()) || |
| (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) || |
| (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) || |
| (FromTy->isReferenceType() ^ ToTy->isReferenceType())) { |
| |
| if (FromTy->isBooleanType()) { |
| assert(ToBitWidth > 0 && "BitWidth must be positive!"); |
| return mkIte(Exp, mkBitvector(llvm::APSInt("1"), ToBitWidth), |
| mkBitvector(llvm::APSInt("0"), ToBitWidth)); |
| } |
| |
| if (ToBitWidth > FromBitWidth) |
| return FromTy->isSignedIntegerOrEnumerationType() |
| ? mkBVSignExt(ToBitWidth - FromBitWidth, Exp) |
| : mkBVZeroExt(ToBitWidth - FromBitWidth, Exp); |
| |
| if (ToBitWidth < FromBitWidth) |
| return mkBVExtract(ToBitWidth - 1, 0, Exp); |
| |
| // Both are bitvectors with the same width, ignore the type cast |
| return Exp; |
| } |
| |
| if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) { |
| if (ToBitWidth != FromBitWidth) |
| return mkFPtoFP(Exp, getFloatSort(ToBitWidth)); |
| |
| return Exp; |
| } |
| |
| if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) { |
| SMTSortRef Sort = getFloatSort(ToBitWidth); |
| return FromTy->isSignedIntegerOrEnumerationType() ? mkFPtoSBV(Exp, Sort) |
| : mkFPtoUBV(Exp, Sort); |
| } |
| |
| if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType()) |
| return ToTy->isSignedIntegerOrEnumerationType() |
| ? mkSBVtoFP(Exp, ToBitWidth) |
| : mkUBVtoFP(Exp, ToBitWidth); |
| |
| llvm_unreachable("Unsupported explicit type cast!"); |
| } |
| |
| // Callback function for doCast parameter on APSInt type. |
| llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy, |
| uint64_t ToWidth, QualType FromTy, |
| uint64_t FromWidth) { |
| APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType()); |
| return TargetType.convert(V); |
| } |
| |
| // Generate an SMTExprRef that represents the given symbolic expression. |
| // Sets the hasComparison parameter if the expression has a comparison |
| // operator. |
| // Sets the RetTy parameter to the final return type after promotions and |
| // casts. |
| SMTExprRef getExpr(ASTContext &Ctx, SymbolRef Sym, QualType *RetTy = nullptr, |
| bool *hasComparison = nullptr) { |
| if (hasComparison) { |
| *hasComparison = false; |
| } |
| |
| return getSymExpr(Ctx, Sym, RetTy, hasComparison); |
| } |
| |
| // Generate an SMTExprRef that compares the expression to zero. |
| SMTExprRef getZeroExpr(ASTContext &Ctx, const SMTExprRef &Exp, QualType Ty, |
| bool Assumption) { |
| |
| if (Ty->isRealFloatingType()) { |
| llvm::APFloat Zero = |
| llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty)); |
| return fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE, fromAPFloat(Zero)); |
| } |
| |
| if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() || |
| Ty->isBlockPointerType() || Ty->isReferenceType()) { |
| |
| // Skip explicit comparison for boolean types |
| bool isSigned = Ty->isSignedIntegerOrEnumerationType(); |
| if (Ty->isBooleanType()) |
| return Assumption ? fromUnOp(UO_LNot, Exp) : Exp; |
| |
| return fromBinOp(Exp, Assumption ? BO_EQ : BO_NE, |
| fromInt("0", Ctx.getTypeSize(Ty)), isSigned); |
| } |
| |
| llvm_unreachable("Unsupported type for zero value!"); |
| } |
| |
| // Recursive implementation to unpack and generate symbolic expression. |
| // Sets the hasComparison and RetTy parameters. See getExpr(). |
| SMTExprRef getSymExpr(ASTContext &Ctx, SymbolRef Sym, QualType *RetTy, |
| bool *hasComparison) { |
| if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) { |
| if (RetTy) |
| *RetTy = Sym->getType(); |
| |
| return fromData(SD->getSymbolID(), Sym->getType(), |
| Ctx.getTypeSize(Sym->getType())); |
| } |
| |
| if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) { |
| if (RetTy) |
| *RetTy = Sym->getType(); |
| |
| QualType FromTy; |
| SMTExprRef Exp = |
| getSymExpr(Ctx, SC->getOperand(), &FromTy, hasComparison); |
| // Casting an expression with a comparison invalidates it. Note that this |
| // must occur after the recursive call above. |
| // e.g. (signed char) (x > 0) |
| if (hasComparison) |
| *hasComparison = false; |
| return getCastExpr(Ctx, Exp, FromTy, Sym->getType()); |
| } |
| |
| if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) { |
| SMTExprRef Exp = getSymBinExpr(Ctx, BSE, hasComparison, RetTy); |
| // Set the hasComparison parameter, in post-order traversal order. |
| if (hasComparison) |
| *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode()); |
| return Exp; |
| } |
| |
| llvm_unreachable("Unsupported SymbolRef type!"); |
| } |
| |
| // Wrapper to generate SMTExprRef from SymbolCast data. |
| SMTExprRef getCastExpr(ASTContext &Ctx, const SMTExprRef &Exp, |
| QualType FromTy, QualType ToTy) { |
| return fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy, |
| Ctx.getTypeSize(FromTy)); |
| } |
| |
| // Wrapper to generate SMTExprRef from BinarySymExpr. |
| // Sets the hasComparison and RetTy parameters. See getSMTExprRef(). |
| SMTExprRef getSymBinExpr(ASTContext &Ctx, const BinarySymExpr *BSE, |
| bool *hasComparison, QualType *RetTy) { |
| QualType LTy, RTy; |
| BinaryOperator::Opcode Op = BSE->getOpcode(); |
| |
| if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) { |
| SMTExprRef LHS = getSymExpr(Ctx, SIE->getLHS(), <y, hasComparison); |
| llvm::APSInt NewRInt; |
| std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS()); |
| SMTExprRef RHS = fromAPSInt(NewRInt); |
| return getBinExpr(Ctx, LHS, LTy, Op, RHS, RTy, RetTy); |
| } |
| |
| if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) { |
| llvm::APSInt NewLInt; |
| std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS()); |
| SMTExprRef LHS = fromAPSInt(NewLInt); |
| SMTExprRef RHS = getSymExpr(Ctx, ISE->getRHS(), &RTy, hasComparison); |
| return getBinExpr(Ctx, LHS, LTy, Op, RHS, RTy, RetTy); |
| } |
| |
| if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) { |
| SMTExprRef LHS = getSymExpr(Ctx, SSM->getLHS(), <y, hasComparison); |
| SMTExprRef RHS = getSymExpr(Ctx, SSM->getRHS(), &RTy, hasComparison); |
| return getBinExpr(Ctx, LHS, LTy, Op, RHS, RTy, RetTy); |
| } |
| |
| llvm_unreachable("Unsupported BinarySymExpr type!"); |
| } |
| |
| // Wrapper to generate SMTExprRef from unpacked binary symbolic expression. |
| // Sets the RetTy parameter. See getSMTExprRef(). |
| SMTExprRef getBinExpr(ASTContext &Ctx, const SMTExprRef &LHS, QualType LTy, |
| BinaryOperator::Opcode Op, const SMTExprRef &RHS, |
| QualType RTy, QualType *RetTy) { |
| SMTExprRef NewLHS = LHS; |
| SMTExprRef NewRHS = RHS; |
| doTypeConversion(Ctx, NewLHS, NewRHS, LTy, RTy); |
| |
| // Update the return type parameter if the output type has changed. |
| if (RetTy) { |
| // A boolean result can be represented as an integer type in C/C++, but at |
| // this point we only care about the SMT sorts. Set it as a boolean type |
| // to avoid subsequent SMT errors. |
| if (BinaryOperator::isComparisonOp(Op) || |
| BinaryOperator::isLogicalOp(Op)) { |
| *RetTy = Ctx.BoolTy; |
| } else { |
| *RetTy = LTy; |
| } |
| |
| // If the two operands are pointers and the operation is a subtraction, |
| // the result is of type ptrdiff_t, which is signed |
| if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) { |
| *RetTy = Ctx.getPointerDiffType(); |
| } |
| } |
| |
| return LTy->isRealFloatingType() |
| ? fromFloatBinOp(NewLHS, Op, NewRHS) |
| : fromBinOp(NewLHS, Op, NewRHS, |
| LTy->isSignedIntegerOrEnumerationType()); |
| } |
| |
| // Wrapper to generate SMTExprRef from a range. If From == To, an equality |
| // will be created instead. |
| SMTExprRef getRangeExpr(ASTContext &Ctx, SymbolRef Sym, |
| const llvm::APSInt &From, const llvm::APSInt &To, |
| bool InRange) { |
| // Convert lower bound |
| QualType FromTy; |
| llvm::APSInt NewFromInt; |
| std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From); |
| SMTExprRef FromExp = fromAPSInt(NewFromInt); |
| |
| // Convert symbol |
| QualType SymTy; |
| SMTExprRef Exp = getExpr(Ctx, Sym, &SymTy); |
| |
| // Construct single (in)equality |
| if (From == To) |
| return getBinExpr(Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp, |
| FromTy, /*RetTy=*/nullptr); |
| |
| QualType ToTy; |
| llvm::APSInt NewToInt; |
| std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To); |
| SMTExprRef ToExp = fromAPSInt(NewToInt); |
| assert(FromTy == ToTy && "Range values have different types!"); |
| |
| // Construct two (in)equalities, and a logical and/or |
| SMTExprRef LHS = getBinExpr(Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, |
| FromExp, FromTy, /*RetTy=*/nullptr); |
| SMTExprRef RHS = |
| getBinExpr(Ctx, Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy, |
| /*RetTy=*/nullptr); |
| |
| return fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, |
| SymTy->isSignedIntegerOrEnumerationType()); |
| } |
| |
| // Recover the QualType of an APSInt. |
| // TODO: Refactor to put elsewhere |
| QualType getAPSIntType(ASTContext &Ctx, const llvm::APSInt &Int) { |
| return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned()); |
| } |
| |
| // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1. |
| std::pair<llvm::APSInt, QualType> fixAPSInt(ASTContext &Ctx, |
| const llvm::APSInt &Int) { |
| llvm::APSInt NewInt; |
| |
| // FIXME: This should be a cast from a 1-bit integer type to a boolean type, |
| // but the former is not available in Clang. Instead, extend the APSInt |
| // directly. |
| if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) { |
| NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy)); |
| } else |
| NewInt = Int; |
| |
| return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt)); |
| } |
| |
| // Perform implicit type conversion on binary symbolic expressions. |
| // May modify all input parameters. |
| // TODO: Refactor to use built-in conversion functions |
| void doTypeConversion(ASTContext &Ctx, SMTExprRef &LHS, SMTExprRef &RHS, |
| QualType <y, QualType &RTy) { |
| assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!"); |
| |
| // Perform type conversion |
| if ((LTy->isIntegralOrEnumerationType() && |
| RTy->isIntegralOrEnumerationType()) && |
| (LTy->isArithmeticType() && RTy->isArithmeticType())) { |
| doIntTypeConversion<SMTExprRef, &SMTSolver::fromCast>(Ctx, LHS, LTy, RHS, |
| RTy); |
| return; |
| } |
| |
| if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) { |
| doFloatTypeConversion<SMTExprRef, &SMTSolver::fromCast>(Ctx, LHS, LTy, |
| RHS, RTy); |
| return; |
| } |
| |
| if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) || |
| (LTy->isBlockPointerType() || RTy->isBlockPointerType()) || |
| (LTy->isReferenceType() || RTy->isReferenceType())) { |
| // TODO: Refactor to Sema::FindCompositePointerType(), and |
| // Sema::CheckCompareOperands(). |
| |
| uint64_t LBitWidth = Ctx.getTypeSize(LTy); |
| uint64_t RBitWidth = Ctx.getTypeSize(RTy); |
| |
| // Cast the non-pointer type to the pointer type. |
| // TODO: Be more strict about this. |
| if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) || |
| (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) || |
| (LTy->isReferenceType() ^ RTy->isReferenceType())) { |
| if (LTy->isNullPtrType() || LTy->isBlockPointerType() || |
| LTy->isReferenceType()) { |
| LHS = fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth); |
| LTy = RTy; |
| } else { |
| RHS = fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth); |
| RTy = LTy; |
| } |
| } |
| |
| // Cast the void pointer type to the non-void pointer type. |
| // For void types, this assumes that the casted value is equal to the |
| // value of the original pointer, and does not account for alignment |
| // requirements. |
| if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) { |
| assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) && |
| "Pointer types have different bitwidths!"); |
| if (RTy->isVoidPointerType()) |
| RTy = LTy; |
| else |
| LTy = RTy; |
| } |
| |
| if (LTy == RTy) |
| return; |
| } |
| |
| // Fallback: for the solver, assume that these types don't really matter |
| if ((LTy.getCanonicalType() == RTy.getCanonicalType()) || |
| (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) { |
| LTy = RTy; |
| return; |
| } |
| |
| // TODO: Refine behavior for invalid type casts |
| } |
| |
| // Perform implicit integer type conversion. |
| // May modify all input parameters. |
| // TODO: Refactor to use Sema::handleIntegerConversion() |
| template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t, |
| QualType, uint64_t)> |
| void doIntTypeConversion(ASTContext &Ctx, T &LHS, QualType <y, T &RHS, |
| QualType &RTy) { |
| |
| uint64_t LBitWidth = Ctx.getTypeSize(LTy); |
| uint64_t RBitWidth = Ctx.getTypeSize(RTy); |
| |
| assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!"); |
| // Always perform integer promotion before checking type equality. |
| // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion |
| if (LTy->isPromotableIntegerType()) { |
| QualType NewTy = Ctx.getPromotedIntegerType(LTy); |
| uint64_t NewBitWidth = Ctx.getTypeSize(NewTy); |
| LHS = (this->*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth); |
| LTy = NewTy; |
| LBitWidth = NewBitWidth; |
| } |
| if (RTy->isPromotableIntegerType()) { |
| QualType NewTy = Ctx.getPromotedIntegerType(RTy); |
| uint64_t NewBitWidth = Ctx.getTypeSize(NewTy); |
| RHS = (this->*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth); |
| RTy = NewTy; |
| RBitWidth = NewBitWidth; |
| } |
| |
| if (LTy == RTy) |
| return; |
| |
| // Perform integer type conversion |
| // Note: Safe to skip updating bitwidth because this must terminate |
| bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType(); |
| bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType(); |
| |
| int order = Ctx.getIntegerTypeOrder(LTy, RTy); |
| if (isLSignedTy == isRSignedTy) { |
| // Same signedness; use the higher-ranked type |
| if (order == 1) { |
| RHS = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); |
| RTy = LTy; |
| } else { |
| LHS = (this->*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); |
| LTy = RTy; |
| } |
| } else if (order != (isLSignedTy ? 1 : -1)) { |
| // The unsigned type has greater than or equal rank to the |
| // signed type, so use the unsigned type |
| if (isRSignedTy) { |
| RHS = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); |
| RTy = LTy; |
| } else { |
| LHS = (this->*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); |
| LTy = RTy; |
| } |
| } else if (LBitWidth != RBitWidth) { |
| // The two types are different widths; if we are here, that |
| // means the signed type is larger than the unsigned type, so |
| // use the signed type. |
| if (isLSignedTy) { |
| RHS = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); |
| RTy = LTy; |
| } else { |
| LHS = (this->*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); |
| LTy = RTy; |
| } |
| } else { |
| // The signed type is higher-ranked than the unsigned type, |
| // but isn't actually any bigger (like unsigned int and long |
| // on most 32-bit systems). Use the unsigned type corresponding |
| // to the signed type. |
| QualType NewTy = |
| Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy); |
| RHS = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); |
| RTy = NewTy; |
| LHS = (this->*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); |
| LTy = NewTy; |
| } |
| } |
| |
| // Perform implicit floating-point type conversion. |
| // May modify all input parameters. |
| // TODO: Refactor to use Sema::handleFloatConversion() |
| template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t, |
| QualType, uint64_t)> |
| void doFloatTypeConversion(ASTContext &Ctx, T &LHS, QualType <y, T &RHS, |
| QualType &RTy) { |
| |
| uint64_t LBitWidth = Ctx.getTypeSize(LTy); |
| uint64_t RBitWidth = Ctx.getTypeSize(RTy); |
| |
| // Perform float-point type promotion |
| if (!LTy->isRealFloatingType()) { |
| LHS = (this->*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); |
| LTy = RTy; |
| LBitWidth = RBitWidth; |
| } |
| if (!RTy->isRealFloatingType()) { |
| RHS = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); |
| RTy = LTy; |
| RBitWidth = LBitWidth; |
| } |
| |
| if (LTy == RTy) |
| return; |
| |
| // If we have two real floating types, convert the smaller operand to the |
| // bigger result |
| // Note: Safe to skip updating bitwidth because this must terminate |
| int order = Ctx.getFloatingTypeOrder(LTy, RTy); |
| if (order > 0) { |
| RHS = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth); |
| RTy = LTy; |
| } else if (order == 0) { |
| LHS = (this->*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth); |
| LTy = RTy; |
| } else { |
| llvm_unreachable("Unsupported floating-point type cast!"); |
| } |
| } |
| |
| // Returns a boolean sort. |
| virtual SMTSortRef getBoolSort() = 0; |
| |
| // Returns an appropriate bitvector sort for the given bitwidth. |
| virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0; |
| |
| // Returns a floating-point sort of width 16 |
| virtual SMTSortRef getFloat16Sort() = 0; |
| |
| // Returns a floating-point sort of width 32 |
| virtual SMTSortRef getFloat32Sort() = 0; |
| |
| // Returns a floating-point sort of width 64 |
| virtual SMTSortRef getFloat64Sort() = 0; |
| |
| // Returns a floating-point sort of width 128 |
| virtual SMTSortRef getFloat128Sort() = 0; |
| |
| // Returns an appropriate sort for the given AST. |
| virtual SMTSortRef getSort(const SMTExprRef &AST) = 0; |
| |
| // Returns a new SMTExprRef from an SMTExpr |
| virtual SMTExprRef newExprRef(const SMTExpr &E) const = 0; |
| |
| /// Given a constraint, adds it to the solver |
| virtual void addConstraint(const SMTExprRef &Exp) const = 0; |
| |
| /// Creates a bitvector addition operation |
| virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector subtraction operation |
| virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector multiplication operation |
| virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector signed modulus operation |
| virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector unsigned modulus operation |
| virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector signed division operation |
| virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector unsigned division operation |
| virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector logical shift left operation |
| virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector arithmetic shift right operation |
| virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector logical shift right operation |
| virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector negation operation |
| virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0; |
| |
| /// Creates a bitvector not operation |
| virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0; |
| |
| /// Creates a bitvector xor operation |
| virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector or operation |
| virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector and operation |
| virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector unsigned less-than operation |
| virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector signed less-than operation |
| virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector unsigned greater-than operation |
| virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector signed greater-than operation |
| virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector unsigned less-equal-than operation |
| virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector signed less-equal-than operation |
| virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector unsigned greater-equal-than operation |
| virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a bitvector signed greater-equal-than operation |
| virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a boolean not operation |
| virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0; |
| |
| /// Creates a boolean equality operation |
| virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a boolean and operation |
| virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a boolean or operation |
| virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a boolean ite operation |
| virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, |
| const SMTExprRef &F) = 0; |
| |
| /// Creates a bitvector sign extension operation |
| virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0; |
| |
| /// Creates a bitvector zero extension operation |
| virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0; |
| |
| /// Creates a bitvector extract operation |
| virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low, |
| const SMTExprRef &Exp) = 0; |
| |
| /// Creates a bitvector concat operation |
| virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS, |
| const SMTExprRef &RHS) = 0; |
| |
| /// Creates a floating-point negation operation |
| virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0; |
| |
| /// Creates a floating-point isInfinite operation |
| virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0; |
| |
| /// Creates a floating-point isNaN operation |
| virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0; |
| |
| /// Creates a floating-point isNormal operation |
| virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0; |
| |
| /// Creates a floating-point isZero operation |
| virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0; |
| |
| /// Creates a floating-point multiplication operation |
| virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a floating-point division operation |
| virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a floating-point remainder operation |
| virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a floating-point addition operation |
| virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a floating-point subtraction operation |
| virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a floating-point less-than operation |
| virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a floating-point greater-than operation |
| virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a floating-point less-than-or-equal operation |
| virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a floating-point greater-than-or-equal operation |
| virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| |
| /// Creates a floating-point equality operation |
| virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS, |
| const SMTExprRef &RHS) = 0; |
| |
| /// Creates a floating-point conversion from floatint-point to floating-point |
| /// operation |
| virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0; |
| |
| /// Creates a floating-point conversion from floatint-point to signed |
| /// bitvector operation |
| virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, |
| const SMTSortRef &To) = 0; |
| |
| /// Creates a floating-point conversion from floatint-point to unsigned |
| /// bitvector operation |
| virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, |
| const SMTSortRef &To) = 0; |
| |
| /// Creates a floating-point conversion from signed bitvector to |
| /// floatint-point operation |
| virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0; |
| |
| /// Creates a floating-point conversion from unsigned bitvector to |
| /// floatint-point operation |
| virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0; |
| |
| /// Creates a new symbol, given a name and a sort |
| virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0; |
| |
| // Returns an appropriate floating-point rounding mode. |
| virtual SMTExprRef getFloatRoundingMode() = 0; |
| |
| // If the a model is available, returns the value of a given bitvector symbol |
| virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, |
| bool isUnsigned) = 0; |
| |
| // If the a model is available, returns the value of a given boolean symbol |
| virtual bool getBoolean(const SMTExprRef &Exp) = 0; |
| |
| /// Constructs an SMTExprRef from a boolean. |
| virtual SMTExprRef mkBoolean(const bool b) = 0; |
| |
| /// Constructs an SMTExprRef from a finite APFloat. |
| virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0; |
| |
| /// Constructs an SMTExprRef from an APSInt and its bit width |
| virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0; |
| |
| /// Given an expression, extract the value of this operand in the model. |
| virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0; |
| |
| /// Given an expression extract the value of this operand in the model. |
| virtual bool getInterpretation(const SMTExprRef &Exp, |
| llvm::APFloat &Float) = 0; |
| |
| /// Construct an SMTExprRef value from a boolean. |
| virtual SMTExprRef fromBoolean(const bool Bool) = 0; |
| |
| /// Construct an SMTExprRef value from a finite APFloat. |
| virtual SMTExprRef fromAPFloat(const llvm::APFloat &Float) = 0; |
| |
| /// Construct an SMTExprRef value from an APSInt. |
| virtual SMTExprRef fromAPSInt(const llvm::APSInt &Int) = 0; |
| |
| /// Construct an SMTExprRef value from an integer. |
| virtual SMTExprRef fromInt(const char *Int, uint64_t BitWidth) = 0; |
| |
| /// Construct an SMTExprRef from a SymbolData. |
| virtual SMTExprRef fromData(const SymbolID ID, const QualType &Ty, |
| uint64_t BitWidth) = 0; |
| |
| /// Check if the constraints are satisfiable |
| virtual ConditionTruthVal check() const = 0; |
| |
| /// Push the current solver state |
| virtual void push() = 0; |
| |
| /// Pop the previous solver state |
| virtual void pop(unsigned NumStates = 1) = 0; |
| |
| /// Reset the solver and remove all constraints. |
| virtual void reset() const = 0; |
| |
| virtual void print(raw_ostream &OS) const = 0; |
| }; |
| |
| /// Shared pointer for SMTSolvers. |
| using SMTSolverRef = std::shared_ptr<SMTSolver>; |
| |
| /// Convenience method to create and Z3Solver object |
| std::unique_ptr<SMTSolver> CreateZ3Solver(); |
| |
| } // namespace ento |
| } // namespace clang |
| |
| #endif |