Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -16,7 +16,7 @@ #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" namespace clang { namespace ento { @@ -42,13 +42,14 @@ QualType RetTy; bool hasComparison; - SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison); + SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); // Create zero comparison for implicit boolean cast, with reversed // assumption if (!hasComparison && !RetTy->isBooleanType()) - return assumeExpr(State, Sym, - Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption)); + return assumeExpr( + State, Sym, + SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption)); return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp)); } @@ -58,8 +59,8 @@ const llvm::APSInt &To, bool InRange) override { ASTContext &Ctx = getBasicVals().getContext(); - return assumeExpr(State, Sym, - Solver->getRangeExpr(Ctx, Sym, From, To, InRange)); + return assumeExpr( + State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange)); } ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, @@ -77,31 +78,37 @@ QualType RetTy; // The expression may be casted, so we cannot call getZ3DataExpr() directly - SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy); + SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); SMTExprRef Exp = - Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true); + SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true); // Negate the constraint SMTExprRef NotExp = - Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false); + SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false); Solver->reset(); addStateConstraints(State); Solver->push(); Solver->addConstraint(Exp); - ConditionTruthVal isSat = Solver->check(); + + Optional isSat = Solver->check(); + if (!isSat.hasValue()) + return ConditionTruthVal(); Solver->pop(); Solver->addConstraint(NotExp); - ConditionTruthVal isNotSat = Solver->check(); + + Optional isNotSat = Solver->check(); + if (!isNotSat.hasValue()) + return ConditionTruthVal(); // Zero is the only possible solution - if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse()) + if (isSat.getValue() && !isNotSat.getValue()) return true; // Zero is not a solution - if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue()) + if (!isSat.getValue() && isNotSat.getValue()) return false; // Zero may be a solution @@ -120,14 +127,14 @@ !Ty->isSignedIntegerOrEnumerationType()); SMTExprRef Exp = - Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty)); + SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty)); Solver->reset(); addStateConstraints(State); // Constraints are unsatisfiable - ConditionTruthVal isSat = Solver->check(); - if (!isSat.isConstrainedTrue()) + Optional isSat = Solver->check(); + if (!isSat.hasValue() || !isSat.getValue()) return nullptr; // Model does not assign interpretation @@ -135,16 +142,16 @@ return nullptr; // A value has been obtained, check if it is the only value - SMTExprRef NotExp = Solver->fromBinOp( - Exp, BO_NE, + SMTExprRef NotExp = SMTConv::fromBinOp( + Solver, Exp, BO_NE, Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue()) : Solver->fromAPSInt(Value), false); Solver->addConstraint(NotExp); - ConditionTruthVal isNotSat = Solver->check(); - if (isNotSat.isConstrainedTrue()) + Optional isNotSat = Solver->check(); + if (!isSat.hasValue() || isNotSat.getValue()) return nullptr; // This is the only solution, store it @@ -185,10 +192,10 @@ llvm::APSInt ConvertedLHS, ConvertedRHS; QualType LTy, RTy; - std::tie(ConvertedLHS, LTy) = Solver->fixAPSInt(Ctx, *LHS); - std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS); - Solver->doIntTypeConversion( - Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy); + std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS); + std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS); + SMTConv::doIntTypeConversion( + Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy); return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS); } @@ -262,9 +269,13 @@ Solver->reset(); Solver->addConstraint(Exp); addStateConstraints(State); - return Solver->check(); - } + Optional res = Solver->check(); + if (!res.hasValue()) + return ConditionTruthVal(); + + return ConditionTruthVal(res.getValue()); + } }; // end class SMTConstraintManager } // namespace ento Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h @@ -0,0 +1,750 @@ +//== SMTConv.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 set of functions to create SMT expressions +// +//===----------------------------------------------------------------------===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H + +#include "clang/AST/Expr.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h" + +namespace clang { +namespace ento { + +class SMTConv { +public: + // Returns an appropriate sort, given a QualType and it's bit width. + static inline SMTSortRef mkSort(SMTSolverRef &Solver, const QualType &Ty, + unsigned BitWidth) { + if (Ty->isBooleanType()) + return Solver->getBoolSort(); + + if (Ty->isRealFloatingType()) + return Solver->getFloatSort(BitWidth); + + return Solver->getBitvectorSort(BitWidth); + } + + /// Constructs an SMTExprRef from an unary operator. + static inline SMTExprRef fromUnOp(SMTSolverRef &Solver, + const UnaryOperator::Opcode Op, + const SMTExprRef &Exp) { + switch (Op) { + case UO_Minus: + return Solver->mkBVNeg(Exp); + + case UO_Not: + return Solver->mkBVNot(Exp); + + case UO_LNot: + return Solver->mkNot(Exp); + + default:; + } + llvm_unreachable("Unimplemented opcode"); + } + + /// Constructs an SMTExprRef from a floating-point unary operator. + static inline SMTExprRef fromFloatUnOp(SMTSolverRef &Solver, + const UnaryOperator::Opcode Op, + const SMTExprRef &Exp) { + switch (Op) { + case UO_Minus: + return Solver->mkFPNeg(Exp); + + case UO_LNot: + return fromUnOp(Solver, Op, Exp); + + default:; + } + llvm_unreachable("Unimplemented opcode"); + } + + /// Construct an SMTExprRef from a n-ary binary operator. + static inline SMTExprRef fromNBinOp(SMTSolverRef &Solver, + const BinaryOperator::Opcode Op, + const std::vector &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) ? Solver->mkAnd(res, ASTs[i]) + : Solver->mkOr(res, ASTs[i]); + return res; + } + + /// Construct an SMTExprRef from a binary operator. + static inline SMTExprRef fromBinOp(SMTSolverRef &Solver, + const SMTExprRef &LHS, + const BinaryOperator::Opcode Op, + const SMTExprRef &RHS, bool isSigned) { + assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && + "AST's must have the same sort!"); + + switch (Op) { + // Multiplicative operators + case BO_Mul: + return Solver->mkBVMul(LHS, RHS); + + case BO_Div: + return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS); + + case BO_Rem: + return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS); + + // Additive operators + case BO_Add: + return Solver->mkBVAdd(LHS, RHS); + + case BO_Sub: + return Solver->mkBVSub(LHS, RHS); + + // Bitwise shift operators + case BO_Shl: + return Solver->mkBVShl(LHS, RHS); + + case BO_Shr: + return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS); + + // Relational operators + case BO_LT: + return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS); + + case BO_GT: + return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS); + + case BO_LE: + return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS); + + case BO_GE: + return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS); + + // Equality operators + case BO_EQ: + return Solver->mkEqual(LHS, RHS); + + case BO_NE: + return fromUnOp(Solver, UO_LNot, + fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned)); + + // Bitwise operators + case BO_And: + return Solver->mkBVAnd(LHS, RHS); + + case BO_Xor: + return Solver->mkBVXor(LHS, RHS); + + case BO_Or: + return Solver->mkBVOr(LHS, RHS); + + // Logical operators + case BO_LAnd: + return Solver->mkAnd(LHS, RHS); + + case BO_LOr: + return Solver->mkOr(LHS, RHS); + + default:; + } + llvm_unreachable("Unimplemented opcode"); + } + + /// Construct an SMTExprRef from a special floating-point binary operator. + static inline SMTExprRef + fromFloatSpecialBinOp(SMTSolverRef &Solver, 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 Solver->mkFPIsInfinite(LHS); + + case llvm::APFloat::fcNaN: + return Solver->mkFPIsNaN(LHS); + + case llvm::APFloat::fcNormal: + return Solver->mkFPIsNormal(LHS); + + case llvm::APFloat::fcZero: + return Solver->mkFPIsZero(LHS); + } + break; + + case BO_NE: + return fromFloatUnOp(Solver, UO_LNot, + fromFloatSpecialBinOp(Solver, LHS, BO_EQ, RHS)); + + default:; + } + + llvm_unreachable("Unimplemented opcode"); + } + + /// Construct an SMTExprRef from a floating-point binary operator. + static inline SMTExprRef fromFloatBinOp(SMTSolverRef &Solver, + const SMTExprRef &LHS, + const BinaryOperator::Opcode Op, + const SMTExprRef &RHS) { + assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && + "AST's must have the same sort!"); + + switch (Op) { + // Multiplicative operators + case BO_Mul: + return Solver->mkFPMul(LHS, RHS); + + case BO_Div: + return Solver->mkFPDiv(LHS, RHS); + + case BO_Rem: + return Solver->mkFPRem(LHS, RHS); + + // Additive operators + case BO_Add: + return Solver->mkFPAdd(LHS, RHS); + + case BO_Sub: + return Solver->mkFPSub(LHS, RHS); + + // Relational operators + case BO_LT: + return Solver->mkFPLt(LHS, RHS); + + case BO_GT: + return Solver->mkFPGt(LHS, RHS); + + case BO_LE: + return Solver->mkFPLe(LHS, RHS); + + case BO_GE: + return Solver->mkFPGe(LHS, RHS); + + // Equality operators + case BO_EQ: + return Solver->mkFPEqual(LHS, RHS); + + case BO_NE: + return fromFloatUnOp(Solver, UO_LNot, + fromFloatBinOp(Solver, LHS, BO_EQ, RHS)); + + // Logical operators + case BO_LAnd: + case BO_LOr: + return fromBinOp(Solver, LHS, Op, RHS, false); + + default:; + } + + llvm_unreachable("Unimplemented opcode"); + } + + /// Construct an SMTExprRef from a QualType FromTy to a QualType ToTy, and + /// their bit widths. + static inline SMTExprRef fromCast(SMTSolverRef &Solver, 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 Solver->mkIte( + Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth), + Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth)); + } + + if (ToBitWidth > FromBitWidth) + return FromTy->isSignedIntegerOrEnumerationType() + ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp) + : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp); + + if (ToBitWidth < FromBitWidth) + return Solver->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 Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth)); + + return Exp; + } + + if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) { + SMTSortRef Sort = Solver->getFloatSort(ToBitWidth); + return FromTy->isSignedIntegerOrEnumerationType() + ? Solver->mkFPtoSBV(Exp, Sort) + : Solver->mkFPtoUBV(Exp, Sort); + } + + if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType()) + return ToTy->isSignedIntegerOrEnumerationType() + ? Solver->mkSBVtoFP(Exp, ToBitWidth) + : Solver->mkUBVtoFP(Exp, ToBitWidth); + + llvm_unreachable("Unsupported explicit type cast!"); + } + + // Callback function for doCast parameter on APSInt type. + static inline llvm::APSInt castAPSInt(SMTSolverRef &Solver, + const llvm::APSInt &V, QualType ToTy, + uint64_t ToWidth, QualType FromTy, + uint64_t FromWidth) { + APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType()); + return TargetType.convert(V); + } + + /// Construct an SMTExprRef from a SymbolData. + static inline SMTExprRef fromData(SMTSolverRef &Solver, const SymbolID ID, + const QualType &Ty, uint64_t BitWidth) { + llvm::Twine Name = "$" + llvm::Twine(ID); + return Solver->mkSymbol(Name.str().c_str(), mkSort(Solver, Ty, BitWidth)); + } + + // Wrapper to generate SMTExprRef from SymbolCast data. + static inline SMTExprRef getCastExpr(SMTSolverRef &Solver, ASTContext &Ctx, + const SMTExprRef &Exp, QualType FromTy, + QualType ToTy) { + return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy, + Ctx.getTypeSize(FromTy)); + } + + // Wrapper to generate SMTExprRef from unpacked binary symbolic expression. + // Sets the RetTy parameter. See getSMTExprRef(). + static inline SMTExprRef getBinExpr(SMTSolverRef &Solver, ASTContext &Ctx, + const SMTExprRef &LHS, QualType LTy, + BinaryOperator::Opcode Op, + const SMTExprRef &RHS, QualType RTy, + QualType *RetTy) { + SMTExprRef NewLHS = LHS; + SMTExprRef NewRHS = RHS; + doTypeConversion(Solver, 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(Solver, NewLHS, Op, NewRHS) + : fromBinOp(Solver, NewLHS, Op, NewRHS, + LTy->isSignedIntegerOrEnumerationType()); + } + + // Wrapper to generate SMTExprRef from BinarySymExpr. + // Sets the hasComparison and RetTy parameters. See getSMTExprRef(). + static inline SMTExprRef getSymBinExpr(SMTSolverRef &Solver, ASTContext &Ctx, + const BinarySymExpr *BSE, + bool *hasComparison, QualType *RetTy) { + QualType LTy, RTy; + BinaryOperator::Opcode Op = BSE->getOpcode(); + + if (const SymIntExpr *SIE = dyn_cast(BSE)) { + SMTExprRef LHS = + getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison); + llvm::APSInt NewRInt; + std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS()); + SMTExprRef RHS = Solver->fromAPSInt(NewRInt); + return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); + } + + if (const IntSymExpr *ISE = dyn_cast(BSE)) { + llvm::APSInt NewLInt; + std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS()); + SMTExprRef LHS = Solver->fromAPSInt(NewLInt); + SMTExprRef RHS = + getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison); + return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); + } + + if (const SymSymExpr *SSM = dyn_cast(BSE)) { + SMTExprRef LHS = + getSymExpr(Solver, Ctx, SSM->getLHS(), <y, hasComparison); + SMTExprRef RHS = + getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison); + return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); + } + + llvm_unreachable("Unsupported BinarySymExpr type!"); + } + + // Recursive implementation to unpack and generate symbolic expression. + // Sets the hasComparison and RetTy parameters. See getExpr(). + static inline SMTExprRef getSymExpr(SMTSolverRef &Solver, ASTContext &Ctx, + SymbolRef Sym, QualType *RetTy, + bool *hasComparison) { + if (const SymbolData *SD = dyn_cast(Sym)) { + if (RetTy) + *RetTy = Sym->getType(); + + return fromData(Solver, SD->getSymbolID(), Sym->getType(), + Ctx.getTypeSize(Sym->getType())); + } + + if (const SymbolCast *SC = dyn_cast(Sym)) { + if (RetTy) + *RetTy = Sym->getType(); + + QualType FromTy; + SMTExprRef Exp = + getSymExpr(Solver, 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(Solver, Ctx, Exp, FromTy, Sym->getType()); + } + + if (const BinarySymExpr *BSE = dyn_cast(Sym)) { + SMTExprRef Exp = getSymBinExpr(Solver, 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!"); + } + + // 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. + static inline SMTExprRef getExpr(SMTSolverRef &Solver, ASTContext &Ctx, + SymbolRef Sym, QualType *RetTy = nullptr, + bool *hasComparison = nullptr) { + if (hasComparison) { + *hasComparison = false; + } + + return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison); + } + + // Generate an SMTExprRef that compares the expression to zero. + static inline SMTExprRef getZeroExpr(SMTSolverRef &Solver, ASTContext &Ctx, + const SMTExprRef &Exp, QualType Ty, + bool Assumption) { + + if (Ty->isRealFloatingType()) { + llvm::APFloat Zero = + llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty)); + return fromFloatBinOp(Solver, 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 ? fromUnOp(Solver, UO_LNot, Exp) : Exp; + + return fromBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE, + Solver->fromInt("0", Ctx.getTypeSize(Ty)), isSigned); + } + + llvm_unreachable("Unsupported type for zero value!"); + } + + // Wrapper to generate SMTExprRef from a range. If From == To, an equality + // will be created instead. + static inline SMTExprRef getRangeExpr(SMTSolverRef &Solver, 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 = Solver->fromAPSInt(NewFromInt); + + // Convert symbol + QualType SymTy; + SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy); + + // Construct single (in)equality + if (From == To) + return getBinExpr(Solver, 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 = Solver->fromAPSInt(NewToInt); + assert(FromTy == ToTy && "Range values have different types!"); + + // Construct two (in)equalities, and a logical and/or + SMTExprRef LHS = + getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp, + FromTy, /*RetTy=*/nullptr); + SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy, + InRange ? BO_LE : BO_GT, ToExp, ToTy, + /*RetTy=*/nullptr); + + return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS, + SymTy->isSignedIntegerOrEnumerationType()); + } + + // Recover the QualType of an APSInt. + // TODO: Refactor to put elsewhere + static inline 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. + static inline std::pair + 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 + static inline void doTypeConversion(SMTSolverRef &Solver, 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())) { + SMTConv::doIntTypeConversion(Solver, Ctx, LHS, LTy, + RHS, RTy); + return; + } + + if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) { + SMTConv::doFloatTypeConversion(Solver, 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(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth); + LTy = RTy; + } else { + RHS = fromCast(Solver, 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 + static inline void doIntTypeConversion(SMTSolverRef &Solver, 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 = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth); + LTy = NewTy; + LBitWidth = NewBitWidth; + } + if (RTy->isPromotableIntegerType()) { + QualType NewTy = Ctx.getPromotedIntegerType(RTy); + uint64_t NewBitWidth = Ctx.getTypeSize(NewTy); + RHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = LTy; + } else { + LHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = LTy; + } else { + LHS = (*doCast)(Solver, 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 = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = LTy; + } else { + LHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = NewTy; + LHS = (doCast)(Solver, 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 + static inline void + doFloatTypeConversion(SMTSolverRef &Solver, 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 = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth); + LTy = RTy; + LBitWidth = RBitWidth; + } + if (!RTy->isRealFloatingType()) { + RHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth); + RTy = LTy; + } else if (order == 0) { + LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth); + LTy = RTy; + } else { + llvm_unreachable("Unsupported floating-point type cast!"); + } + } +}; +} // namespace ento +} // namespace clang + +#endif \ No newline at end of file Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h @@ -15,12 +15,9 @@ #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" +#include "llvm/ADT/APSInt.h" namespace clang { namespace ento { @@ -53,683 +50,6 @@ 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 &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(Sym)) { - if (RetTy) - *RetTy = Sym->getType(); - - return fromData(SD->getSymbolID(), Sym->getType(), - Ctx.getTypeSize(Sym->getType())); - } - - if (const SymbolCast *SC = dyn_cast(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(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(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(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(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 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(Ctx, LHS, LTy, RHS, - RTy); - return; - } - - if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) { - doFloatTypeConversion(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 - 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 - 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; @@ -965,12 +285,8 @@ /// 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; + virtual Optional check() const = 0; /// Push the current solver state virtual void push() = 0; @@ -988,7 +304,7 @@ using SMTSolverRef = std::shared_ptr; /// Convenience method to create and Z3Solver object -std::unique_ptr CreateZ3Solver(); +SMTSolverRef CreateZ3Solver(); } // namespace ento } // namespace clang Index: cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp =================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -42,10 +42,10 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" #include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/None.h" #include "llvm/ADT/Optional.h" @@ -2504,7 +2504,7 @@ VisitNode(EndPathNode, nullptr, BRC, BR); // Create a refutation manager - std::unique_ptr RefutationSolver = CreateZ3Solver(); + SMTSolverRef RefutationSolver = CreateZ3Solver(); ASTContext &Ctx = BRC.getASTContext(); // Add constraints to the solver @@ -2514,15 +2514,19 @@ SMTExprRef Constraints = RefutationSolver->fromBoolean(false); for (const auto &Range : I.second) { Constraints = RefutationSolver->mkOr( - Constraints, - RefutationSolver->getRangeExpr(Ctx, Sym, Range.From(), Range.To(), - /*InRange=*/true)); + Constraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym, + Range.From(), Range.To(), + /*InRange=*/true)); } RefutationSolver->addConstraint(Constraints); } // And check for satisfiability - if (RefutationSolver->check().isConstrainedFalse()) + Optional isSat = RefutationSolver->check(); + if (!isSat.hasValue()) + return; + + if (!isSat.getValue()) BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext()); } Index: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -11,9 +11,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" #include "clang/Config/config.h" @@ -749,12 +747,6 @@ return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context))); } - SMTExprRef fromData(const SymbolID ID, const QualType &Ty, - uint64_t BitWidth) override { - llvm::Twine Name = "$" + llvm::Twine(ID); - return mkSymbol(Name.str().c_str(), mkSort(Ty, BitWidth)); - } - SMTExprRef fromBoolean(const bool Bool) override { Z3_ast AST = Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context); @@ -872,7 +864,7 @@ return toAPFloat(Sort, Assign, Float, true); } - ConditionTruthVal check() const override { + Optional check() const override { Z3_lbool res = Z3_solver_check(Context.Context, Solver); if (res == Z3_L_TRUE) return true; @@ -880,7 +872,7 @@ if (res == Z3_L_FALSE) return false; - return ConditionTruthVal(); + return Optional(); } void push() override { return Z3_solver_push(Context.Context, Solver); } @@ -959,7 +951,7 @@ #endif -std::unique_ptr clang::ento::CreateZ3Solver() { +SMTSolverRef clang::ento::CreateZ3Solver() { #if CLANG_ANALYZER_WITH_Z3 return llvm::make_unique(); #else