r337921 - [analyzer] Moved code from SMTConstraintManager to SMTSolver
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 25 05:49:37 PDT 2018
Author: mramalho
Date: Wed Jul 25 05:49:37 2018
New Revision: 337921
URL: http://llvm.org/viewvc/llvm-project?rev=337921&view=rev
Log:
[analyzer] Moved code from SMTConstraintManager to SMTSolver
Summary:
This is the second part of D49668, and moves all the code that's not specific to a ConstraintManager to SMTSolver.
No functional change intended.
Reviewers: NoQ, george.karpenkov
Reviewed By: george.karpenkov
Subscribers: xazax.hun, szepet, a.sidorin
Differential Revision: https://reviews.llvm.org/D49767
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=337921&r1=337920&r2=337921&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Jul 25 05:49:37 2018
@@ -81,189 +81,6 @@ protected:
// Generate and check a Z3 model, using the given constraint.
ConditionTruthVal checkModel(ProgramStateRef State,
const SMTExprRef &Exp) const;
-
- // Generate a Z3Expr 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(SymbolRef Sym, QualType *RetTy = nullptr,
- bool *hasComparison = nullptr) const;
-
- // Generate a Z3Expr that takes the logical not of an expression.
- SMTExprRef getNotExpr(const SMTExprRef &Exp) const;
-
- // Generate a Z3Expr that compares the expression to zero.
- SMTExprRef getZeroExpr(const SMTExprRef &Exp, QualType RetTy,
- bool Assumption) const;
-
- // Recursive implementation to unpack and generate symbolic expression.
- // Sets the hasComparison and RetTy parameters. See getZ3Expr().
- SMTExprRef getSymExpr(SymbolRef Sym, QualType *RetTy,
- bool *hasComparison) const;
-
- // Wrapper to generate Z3Expr from SymbolData.
- SMTExprRef getDataExpr(const SymbolID ID, QualType Ty) const;
-
- // Wrapper to generate Z3Expr from SymbolCast.
- SMTExprRef getCastExpr(const SMTExprRef &Exp, QualType FromTy,
- QualType Ty) const;
-
- // Wrapper to generate Z3Expr from BinarySymExpr.
- // Sets the hasComparison and RetTy parameters. See getZ3Expr().
- SMTExprRef getSymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
- QualType *RetTy) const;
-
- // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
- // Sets the RetTy parameter. See getZ3Expr().
- SMTExprRef getBinExpr(const SMTExprRef &LHS, QualType LTy,
- BinaryOperator::Opcode Op, const SMTExprRef &RHS,
- QualType RTy, QualType *RetTy) const;
-
- // Wrapper to generate Z3Expr from a range. If From == To, an equality will
- // be created instead.
- SMTExprRef getRangeExpr(SymbolRef Sym, const llvm::APSInt &From,
- const llvm::APSInt &To, bool InRange);
-
- //===------------------------------------------------------------------===//
- // Helper functions.
- //===------------------------------------------------------------------===//
-
- // Recover the QualType of an APSInt.
- // TODO: Refactor to put elsewhere
- QualType getAPSIntType(const llvm::APSInt &Int) const;
-
- // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
- std::pair<llvm::APSInt, QualType> fixAPSInt(const llvm::APSInt &Int) const;
-
- // Perform implicit type conversion on binary symbolic expressions.
- // May modify all input parameters.
- // TODO: Refactor to use built-in conversion functions
- void doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS, QualType <y,
- QualType &RTy) const;
-
- // 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(T &LHS, QualType <y, T &RHS, QualType &RTy) const {
- ASTContext &Ctx = getBasicVals().getContext();
- 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 = ((*Solver).*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 = ((*Solver).*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 = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else {
- LHS = ((*Solver).*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 = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else {
- LHS = ((*Solver).*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 = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else {
- LHS = ((*Solver).*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 = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = NewTy;
- LHS = ((*Solver).*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(T &LHS, QualType <y, T &RHS,
- QualType &RTy) const {
- ASTContext &Ctx = getBasicVals().getContext();
-
- uint64_t LBitWidth = Ctx.getTypeSize(LTy);
- uint64_t RBitWidth = Ctx.getTypeSize(RTy);
-
- // Perform float-point type promotion
- if (!LTy->isRealFloatingType()) {
- LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
- LBitWidth = RBitWidth;
- }
- if (!RTy->isRealFloatingType()) {
- RHS = ((*Solver).*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 = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
- RTy = LTy;
- } else if (order == 0) {
- LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
- } else {
- llvm_unreachable("Unsupported floating-point type cast!");
- }
- }
}; // end class SMTConstraintManager
} // namespace ento
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=337921&r1=337920&r2=337921&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Wed Jul 25 05:49:37 2018
@@ -318,6 +318,420 @@ public:
return TargetType.convert(V);
}
+ // Generate a Z3Expr 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 a Z3Expr 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 getZ3Expr().
+ SMTExprRef getSymExpr(ASTContext &Ctx, SymbolRef Sym, QualType *RetTy,
+ bool *hasComparison) {
+ if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
+ if (RetTy)
+ *RetTy = Sym->getType();
+
+ return getDataExpr(Ctx, SD->getSymbolID(), 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 Z3Expr from SymbolData.
+ SMTExprRef getDataExpr(ASTContext &Ctx, const SymbolID ID, QualType Ty) {
+ return fromData(ID, Ty, Ctx.getTypeSize(Ty));
+ }
+
+ // Wrapper to generate Z3Expr from SymbolCast.
+ 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 Z3Expr from BinarySymExpr.
+ // Sets the hasComparison and RetTy parameters. See getZ3Expr().
+ 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 Z3Expr from unpacked binary symbolic expression.
+ // Sets the RetTy parameter. See getZ3Expr().
+ 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 Z3 type. Set it as a boolean type to
+ // avoid subsequent Z3 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 Z3Expr 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!");
+ }
+ }
+
// Return a boolean sort.
virtual SMTSortRef getBoolSort() = 0;
Modified: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp?rev=337921&r1=337920&r2=337921&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp Wed Jul 25 05:49:37 2018
@@ -16,6 +16,7 @@ using namespace clang;
using namespace ento;
void SMTConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
+ ASTContext &Ctx = getBasicVals().getContext();
Solver->reset();
for (const auto &I : CR) {
@@ -23,8 +24,8 @@ void SMTConstraintManager::addRangeConst
SMTExprRef Constraints = Solver->fromBoolean(false);
for (const auto &Range : I.second) {
- SMTExprRef SymRange =
- getRangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true);
+ SMTExprRef SymRange = Solver->getRangeExpr(Ctx, Sym, Range.From(),
+ Range.To(), /*InRange=*/true);
// FIXME: the last argument (isSigned) is not used when generating the
// or expression, as both arguments are booleans
@@ -42,21 +43,28 @@ clang::ento::ConditionTruthVal SMTConstr
ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State,
SymbolRef Sym,
bool Assumption) {
+ ASTContext &Ctx = getBasicVals().getContext();
+
QualType RetTy;
bool hasComparison;
- SMTExprRef Exp = getExpr(Sym, &RetTy, &hasComparison);
+ SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison);
+
// Create zero comparison for implicit boolean cast, with reversed assumption
if (!hasComparison && !RetTy->isBooleanType())
- return assumeExpr(State, Sym, getZeroExpr(Exp, RetTy, !Assumption));
+ return assumeExpr(State, Sym,
+ Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption));
- return assumeExpr(State, Sym, Assumption ? Exp : getNotExpr(Exp));
+ return assumeExpr(State, Sym,
+ Assumption ? Exp : Solver->fromUnOp(UO_LNot, Exp));
}
ProgramStateRef SMTConstraintManager::assumeSymInclusiveRange(
ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
const llvm::APSInt &To, bool InRange) {
- return assumeExpr(State, Sym, getRangeExpr(Sym, From, To, InRange));
+ ASTContext &Ctx = getBasicVals().getContext();
+ return assumeExpr(State, Sym,
+ Solver->getRangeExpr(Ctx, Sym, From, To, InRange));
}
ProgramStateRef
@@ -68,13 +76,15 @@ SMTConstraintManager::assumeSymUnsupport
ConditionTruthVal SMTConstraintManager::checkNull(ProgramStateRef State,
SymbolRef Sym) {
+ ASTContext &Ctx = getBasicVals().getContext();
+
QualType RetTy;
// The expression may be casted, so we cannot call getZ3DataExpr() directly
- SMTExprRef VarExp = getExpr(Sym, &RetTy);
- SMTExprRef Exp = getZeroExpr(VarExp, RetTy, true);
+ SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy);
+ SMTExprRef Exp = Solver->getZeroExpr(Ctx, VarExp, RetTy, true);
// Negate the constraint
- SMTExprRef NotExp = getZeroExpr(VarExp, RetTy, false);
+ SMTExprRef NotExp = Solver->getZeroExpr(Ctx, VarExp, RetTy, false);
Solver->reset();
addStateConstraints(State);
@@ -110,7 +120,7 @@ const llvm::APSInt *SMTConstraintManager
llvm::APSInt Value(Ctx.getTypeSize(Ty),
!Ty->isSignedIntegerOrEnumerationType());
- SMTExprRef Exp = getDataExpr(SD->getSymbolID(), Ty);
+ SMTExprRef Exp = Solver->getDataExpr(Ctx, SD->getSymbolID(), Ty);
Solver->reset();
addStateConstraints(State);
@@ -175,20 +185,16 @@ const llvm::APSInt *SMTConstraintManager
llvm::APSInt ConvertedLHS, ConvertedRHS;
QualType LTy, RTy;
- std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS);
- std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS);
- doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
- ConvertedLHS, LTy, ConvertedRHS, RTy);
+ std::tie(ConvertedLHS, LTy) = Solver->fixAPSInt(Ctx, *LHS);
+ std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS);
+ Solver->doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
+ Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
}
llvm_unreachable("Unsupported expression to get symbol value!");
}
-//===------------------------------------------------------------------===//
-// Internal implementation.
-//===------------------------------------------------------------------===//
-
ConditionTruthVal
SMTConstraintManager::checkModel(ProgramStateRef State,
const SMTExprRef &Exp) const {
@@ -197,283 +203,3 @@ SMTConstraintManager::checkModel(Program
addStateConstraints(State);
return Solver->check();
}
-
-SMTExprRef SMTConstraintManager::getExpr(SymbolRef Sym, QualType *RetTy,
- bool *hasComparison) const {
- if (hasComparison) {
- *hasComparison = false;
- }
-
- return getSymExpr(Sym, RetTy, hasComparison);
-}
-
-SMTExprRef SMTConstraintManager::getNotExpr(const SMTExprRef &Exp) const {
- return Solver->fromUnOp(UO_LNot, Exp);
-}
-
-SMTExprRef SMTConstraintManager::getZeroExpr(const SMTExprRef &Exp, QualType Ty,
- bool Assumption) const {
- ASTContext &Ctx = getBasicVals().getContext();
- if (Ty->isRealFloatingType()) {
- llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
- return Solver->fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
- Solver->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 ? getNotExpr(Exp) : Exp;
-
- return Solver->fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
- Solver->fromInt("0", Ctx.getTypeSize(Ty)),
- isSigned);
- }
-
- llvm_unreachable("Unsupported type for zero value!");
-}
-
-SMTExprRef SMTConstraintManager::getSymExpr(SymbolRef Sym, QualType *RetTy,
- bool *hasComparison) const {
- if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
- if (RetTy)
- *RetTy = Sym->getType();
-
- return getDataExpr(SD->getSymbolID(), Sym->getType());
- }
-
- if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
- if (RetTy)
- *RetTy = Sym->getType();
-
- QualType FromTy;
- SMTExprRef Exp = getSymExpr(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(Exp, FromTy, Sym->getType());
- }
-
- if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
- SMTExprRef Exp = getSymBinExpr(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!");
-}
-
-SMTExprRef SMTConstraintManager::getDataExpr(const SymbolID ID,
- QualType Ty) const {
- ASTContext &Ctx = getBasicVals().getContext();
- return Solver->fromData(ID, Ty, Ctx.getTypeSize(Ty));
-}
-
-SMTExprRef SMTConstraintManager::getCastExpr(const SMTExprRef &Exp,
- QualType FromTy,
- QualType ToTy) const {
- ASTContext &Ctx = getBasicVals().getContext();
- return Solver->fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
- Ctx.getTypeSize(FromTy));
-}
-
-SMTExprRef SMTConstraintManager::getSymBinExpr(const BinarySymExpr *BSE,
- bool *hasComparison,
- QualType *RetTy) const {
- QualType LTy, RTy;
- BinaryOperator::Opcode Op = BSE->getOpcode();
-
- if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
- SMTExprRef LHS = getSymExpr(SIE->getLHS(), <y, hasComparison);
- llvm::APSInt NewRInt;
- std::tie(NewRInt, RTy) = fixAPSInt(SIE->getRHS());
- SMTExprRef RHS = Solver->fromAPSInt(NewRInt);
- return getBinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
- }
-
- if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
- llvm::APSInt NewLInt;
- std::tie(NewLInt, LTy) = fixAPSInt(ISE->getLHS());
- SMTExprRef LHS = Solver->fromAPSInt(NewLInt);
- SMTExprRef RHS = getSymExpr(ISE->getRHS(), &RTy, hasComparison);
- return getBinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
- }
-
- if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
- SMTExprRef LHS = getSymExpr(SSM->getLHS(), <y, hasComparison);
- SMTExprRef RHS = getSymExpr(SSM->getRHS(), &RTy, hasComparison);
- return getBinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
- }
-
- llvm_unreachable("Unsupported BinarySymExpr type!");
-}
-
-SMTExprRef SMTConstraintManager::getBinExpr(const SMTExprRef &LHS, QualType LTy,
- BinaryOperator::Opcode Op,
- const SMTExprRef &RHS, QualType RTy,
- QualType *RetTy) const {
- SMTExprRef NewLHS = LHS;
- SMTExprRef NewRHS = RHS;
- doTypeConversion(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 Z3 type. Set it as a boolean type to
- // avoid subsequent Z3 errors.
- if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) {
- ASTContext &Ctx = getBasicVals().getContext();
- *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 = getBasicVals().getContext().getPointerDiffType();
- }
- }
-
- return LTy->isRealFloatingType()
- ? Solver->fromFloatBinOp(NewLHS, Op, NewRHS)
- : Solver->fromBinOp(NewLHS, Op, NewRHS,
- LTy->isSignedIntegerOrEnumerationType());
-}
-
-SMTExprRef SMTConstraintManager::getRangeExpr(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(From);
- SMTExprRef FromExp = Solver->fromAPSInt(NewFromInt);
-
- // Convert symbol
- QualType SymTy;
- SMTExprRef Exp = getExpr(Sym, &SymTy);
-
- // Construct single (in)equality
- if (From == To)
- return getBinExpr(Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp, FromTy,
- /*RetTy=*/nullptr);
-
- QualType ToTy;
- llvm::APSInt NewToInt;
- std::tie(NewToInt, ToTy) = fixAPSInt(To);
- SMTExprRef ToExp = Solver->fromAPSInt(NewToInt);
- assert(FromTy == ToTy && "Range values have different types!");
-
- // Construct two (in)equalities, and a logical and/or
- SMTExprRef LHS = getBinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
- FromTy, /*RetTy=*/nullptr);
- SMTExprRef RHS = getBinExpr(Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
- /*RetTy=*/nullptr);
-
- return Solver->fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
- SymTy->isSignedIntegerOrEnumerationType());
-}
-
-//===------------------------------------------------------------------===//
-// Helper functions.
-//===------------------------------------------------------------------===//
-
-QualType SMTConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
- ASTContext &Ctx = getBasicVals().getContext();
- return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
-}
-
-std::pair<llvm::APSInt, QualType>
-SMTConstraintManager::fixAPSInt(const llvm::APSInt &Int) const {
- 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(Int).isNull()) {
- ASTContext &Ctx = getBasicVals().getContext();
- NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
- } else
- NewInt = Int;
-
- return std::make_pair(NewInt, getAPSIntType(NewInt));
-}
-
-void SMTConstraintManager::doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS,
- QualType <y,
- QualType &RTy) const {
- assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
-
- ASTContext &Ctx = getBasicVals().getContext();
-
- // Perform type conversion
- if ((LTy->isIntegralOrEnumerationType() &&
- RTy->isIntegralOrEnumerationType()) &&
- (LTy->isArithmeticType() && RTy->isArithmeticType())) {
- doIntTypeConversion<SMTExprRef, &SMTSolver::fromCast>(LHS, LTy, RHS, RTy);
- return;
- }
-
- if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
- doFloatTypeConversion<SMTExprRef, &SMTSolver::fromCast>(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 = Solver->fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
- LTy = RTy;
- } else {
- RHS = Solver->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
-}
More information about the cfe-commits
mailing list