Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -16,27 +16,254 @@ #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h" namespace clang { namespace ento { class SMTConstraintManager : public clang::ento::SimpleConstraintManager { + SMTSolverRef &Solver; public: - SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB) - : SimpleConstraintManager(SE, SB) {} + SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB, + SMTSolverRef &S) + : SimpleConstraintManager(SE, SB), Solver(S) {} virtual ~SMTConstraintManager() = default; + //===------------------------------------------------------------------===// + // Implementation for interface from SimpleConstraintManager. + //===------------------------------------------------------------------===// + + ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym, + bool Assumption) override; + + ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, + const llvm::APSInt &From, + const llvm::APSInt &To, + bool InRange) override; + + ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, + bool Assumption) override; + + //===------------------------------------------------------------------===// + // Implementation for interface from ConstraintManager. + //===------------------------------------------------------------------===// + + ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override; + + const llvm::APSInt *getSymVal(ProgramStateRef State, + SymbolRef Sym) const override; + /// Converts the ranged constraints of a set of symbols to SMT /// /// \param CR The set of constraints. - virtual void addRangeConstraints(clang::ento::ConstraintRangeTy CR) = 0; + void addRangeConstraints(clang::ento::ConstraintRangeTy CR); /// Checks if the added constraints are satisfiable - virtual clang::ento::ConditionTruthVal isModelFeasible() = 0; + clang::ento::ConditionTruthVal isModelFeasible(); /// Dumps SMT formula - LLVM_DUMP_METHOD virtual void dump() const = 0; + LLVM_DUMP_METHOD void dump() const { Solver->dump(); } + +protected: + //===------------------------------------------------------------------===// + // Internal implementation. + //===------------------------------------------------------------------===// + + // Check whether a new model is satisfiable, and update the program state. + virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, + const SMTExprRef &Exp) = 0; + + /// Given a program state, construct the logical conjunction and add it to + /// the solver + virtual void addStateConstraints(ProgramStateRef State) const = 0; + + // 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 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 + 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 + 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 Index: lib/StaticAnalyzer/Core/CMakeLists.txt =================================================================== --- lib/StaticAnalyzer/Core/CMakeLists.txt +++ lib/StaticAnalyzer/Core/CMakeLists.txt @@ -48,6 +48,7 @@ SVals.cpp SimpleConstraintManager.cpp SimpleSValBuilder.cpp + SMTConstraintManager.cpp Store.cpp SubEngine.cpp SymbolManager.cpp Index: lib/StaticAnalyzer/Core/SMTConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/SMTConstraintManager.cpp +++ lib/StaticAnalyzer/Core/SMTConstraintManager.cpp @@ -0,0 +1,479 @@ +//== SMTConstraintManager.cpp -----------------------------------*- C++ -*--==// +// +// The LLVM Compiler Infrastructure +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" +#include "clang/Basic/TargetInfo.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" + +using namespace clang; +using namespace ento; + +void SMTConstraintManager::addRangeConstraints(ConstraintRangeTy CR) { + Solver->reset(); + + for (const auto &I : CR) { + SymbolRef Sym = I.first; + + SMTExprRef Constraints = Solver->fromBoolean(false); + for (const auto &Range : I.second) { + SMTExprRef SymRange = + getRangeExpr(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 + Constraints = + Solver->fromBinOp(Constraints, BO_LOr, SymRange, /*IsSigned=*/true); + } + Solver->addConstraint(Constraints); + } +} + +clang::ento::ConditionTruthVal SMTConstraintManager::isModelFeasible() { + return Solver->check(); +} + +ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State, + SymbolRef Sym, + bool Assumption) { + QualType RetTy; + bool hasComparison; + + SMTExprRef Exp = getExpr(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, Assumption ? Exp : getNotExpr(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)); +} + +ProgramStateRef +SMTConstraintManager::assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, + bool Assumption) { + // Skip anything that is unsupported + return State; +} + +ConditionTruthVal SMTConstraintManager::checkNull(ProgramStateRef State, + SymbolRef Sym) { + QualType RetTy; + // The expression may be casted, so we cannot call getZ3DataExpr() directly + SMTExprRef VarExp = getExpr(Sym, &RetTy); + SMTExprRef Exp = getZeroExpr(VarExp, RetTy, true); + + // Negate the constraint + SMTExprRef NotExp = getZeroExpr(VarExp, RetTy, false); + + Solver->reset(); + addStateConstraints(State); + + Solver->push(); + Solver->addConstraint(Exp); + ConditionTruthVal isSat = Solver->check(); + + Solver->pop(); + Solver->addConstraint(NotExp); + ConditionTruthVal isNotSat = Solver->check(); + + // Zero is the only possible solution + if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse()) + return true; + + // Zero is not a solution + if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue()) + return false; + + // Zero may be a solution + return ConditionTruthVal(); +} + +const llvm::APSInt *SMTConstraintManager::getSymVal(ProgramStateRef State, + SymbolRef Sym) const { + BasicValueFactory &BVF = getBasicVals(); + ASTContext &Ctx = BVF.getContext(); + + if (const SymbolData *SD = dyn_cast(Sym)) { + QualType Ty = Sym->getType(); + assert(!Ty->isRealFloatingType()); + llvm::APSInt Value(Ctx.getTypeSize(Ty), + !Ty->isSignedIntegerOrEnumerationType()); + + SMTExprRef Exp = getDataExpr(SD->getSymbolID(), Ty); + + Solver->reset(); + addStateConstraints(State); + + // Constraints are unsatisfiable + ConditionTruthVal isSat = Solver->check(); + if (!isSat.isConstrainedTrue()) + return nullptr; + + // Model does not assign interpretation + if (!Solver->getInterpretation(Exp, Value)) + return nullptr; + + // A value has been obtained, check if it is the only value + SMTExprRef NotExp = Solver->fromBinOp( + Exp, BO_NE, + Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue()) + : Solver->fromAPSInt(Value), + false); + + Solver->addConstraint(NotExp); + + ConditionTruthVal isNotSat = Solver->check(); + if (isNotSat.isConstrainedTrue()) + return nullptr; + + // This is the only solution, store it + return &BVF.getValue(Value); + } + + if (const SymbolCast *SC = dyn_cast(Sym)) { + SymbolRef CastSym = SC->getOperand(); + QualType CastTy = SC->getType(); + // Skip the void type + if (CastTy->isVoidType()) + return nullptr; + + const llvm::APSInt *Value; + if (!(Value = getSymVal(State, CastSym))) + return nullptr; + return &BVF.Convert(SC->getType(), *Value); + } + + if (const BinarySymExpr *BSE = dyn_cast(Sym)) { + const llvm::APSInt *LHS, *RHS; + if (const SymIntExpr *SIE = dyn_cast(BSE)) { + LHS = getSymVal(State, SIE->getLHS()); + RHS = &SIE->getRHS(); + } else if (const IntSymExpr *ISE = dyn_cast(BSE)) { + LHS = &ISE->getLHS(); + RHS = getSymVal(State, ISE->getRHS()); + } else if (const SymSymExpr *SSM = dyn_cast(BSE)) { + // Early termination to avoid expensive call + LHS = getSymVal(State, SSM->getLHS()); + RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr; + } else { + llvm_unreachable("Unsupported binary expression to get symbol value!"); + } + + if (!LHS || !RHS) + return nullptr; + + llvm::APSInt ConvertedLHS, ConvertedRHS; + QualType LTy, RTy; + std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS); + std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS); + doIntTypeConversion( + 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 { + Solver->reset(); + Solver->addConstraint(Exp); + 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(Sym)) { + if (RetTy) + *RetTy = Sym->getType(); + + return getDataExpr(SD->getSymbolID(), Sym->getType()); + } + + if (const SymbolCast *SC = dyn_cast(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(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(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(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(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 +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(LHS, LTy, RHS, RTy); + return; + } + + if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) { + doFloatTypeConversion(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 +} Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -320,11 +320,11 @@ Z3_solver Solver; +public: Z3Solver() : SMTSolver(), Solver(Z3_mk_simple_solver(Context.Context)) { Z3_solver_inc_ref(Context.Context, Solver); } -public: /// Override implicit copy constructor for correct reference counting. Z3Solver(const Z3Solver &Copy) : SMTSolver(), Context(Copy.Context), Solver(Copy.Solver) { @@ -932,807 +932,114 @@ }; // end class Z3Solver class Z3ConstraintManager : public SMTConstraintManager { - mutable Z3Solver Solver; + SMTSolverRef Solver = std::make_shared(); public: Z3ConstraintManager(SubEngine *SE, SValBuilder &SB) - : SMTConstraintManager(SE, SB) {} - - //===------------------------------------------------------------------===// - // Implementation for Refutation. - //===------------------------------------------------------------------===// - - void addRangeConstraints(clang::ento::ConstraintRangeTy CR) override; - - ConditionTruthVal isModelFeasible() override; - - LLVM_DUMP_METHOD void dump() const override; - - //===------------------------------------------------------------------===// - // Implementation for interface from ConstraintManager. - //===------------------------------------------------------------------===// - - bool canReasonAbout(SVal X) const override; - - ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override; - - const llvm::APSInt *getSymVal(ProgramStateRef State, - SymbolRef Sym) const override; - - ProgramStateRef removeDeadBindings(ProgramStateRef St, - SymbolReaper &SymReaper) override; - - void print(ProgramStateRef St, raw_ostream &Out, const char *nl, - const char *sep) override; - - //===------------------------------------------------------------------===// - // Implementation for interface from SimpleConstraintManager. - //===------------------------------------------------------------------===// - - ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym, - bool Assumption) override; - - ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, - const llvm::APSInt &From, - const llvm::APSInt &To, - bool InRange) override; - - ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, - bool Assumption) override; - -private: - //===------------------------------------------------------------------===// - // Internal implementation. - //===------------------------------------------------------------------===// - - /// Given a program state, construct the logical conjunction and add it to - /// the solver - void addStateConstraints(ProgramStateRef State) const; - - // Check whether a new model is satisfiable, and update the program state. - ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym, - const SMTExprRef &Exp); - - // Generate and check a Z3 model, using the given constraint. - ConditionTruthVal checkZ3Model(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 getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr, - bool *hasComparison = nullptr) const; - - // Generate a Z3Expr that takes the logical not of an expression. - SMTExprRef getZ3NotExpr(const SMTExprRef &Exp) const; - - // Generate a Z3Expr that compares the expression to zero. - SMTExprRef getZ3ZeroExpr(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 getZ3SymExpr(SymbolRef Sym, QualType *RetTy, - bool *hasComparison) const; - - // Wrapper to generate Z3Expr from SymbolData. - SMTExprRef getZ3DataExpr(const SymbolID ID, QualType Ty) const; - - // Wrapper to generate Z3Expr from SymbolCast. - SMTExprRef getZ3CastExpr(const SMTExprRef &Exp, QualType FromTy, - QualType Ty) const; - - // Wrapper to generate Z3Expr from BinarySymExpr. - // Sets the hasComparison and RetTy parameters. See getZ3Expr(). - SMTExprRef getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison, - QualType *RetTy) const; - - // Wrapper to generate Z3Expr from unpacked binary symbolic expression. - // Sets the RetTy parameter. See getZ3Expr(). - SMTExprRef getZ3BinExpr(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 getZ3RangeExpr(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 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 - void doIntTypeConversion(T &LHS, QualType <y, T &RHS, QualType &RTy) const; - - // Perform implicit floating-point type conversion. - // May modify all input parameters. - // TODO: Refactor to use Sema::handleFloatConversion() - template - void doFloatTypeConversion(T &LHS, QualType <y, T &RHS, - QualType &RTy) const; -}; // end class Z3ConstraintManager - -} // end anonymous namespace - -void Z3ConstraintManager::addStateConstraints(ProgramStateRef State) const { - // TODO: Don't add all the constraints, only the relevant ones - ConstraintZ3Ty CZ = State->get(); - ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end(); - - // Construct the logical AND of all the constraints - if (I != IE) { - std::vector ASTs; - - while (I != IE) - ASTs.push_back(Solver.newExprRef(Z3Expr(I++->second))); - - Solver.addConstraint(Solver.fromNBinOp(BO_LAnd, ASTs)); - } -} - -ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State, - SymbolRef Sym, bool Assumption) { - QualType RetTy; - bool hasComparison; - - SMTExprRef Exp = getZ3Expr(Sym, &RetTy, &hasComparison); - // Create zero comparison for implicit boolean cast, with reversed assumption - if (!hasComparison && !RetTy->isBooleanType()) - return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption)); - - return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp)); -} - -ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange( - ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, - const llvm::APSInt &To, bool InRange) { - return assumeZ3Expr(State, Sym, getZ3RangeExpr(Sym, From, To, InRange)); -} - -ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State, - SymbolRef Sym, - bool Assumption) { - // Skip anything that is unsupported - return State; -} - -bool Z3ConstraintManager::canReasonAbout(SVal X) const { - const TargetInfo &TI = getBasicVals().getContext().getTargetInfo(); - - Optional SymVal = X.getAs(); - if (!SymVal) - return true; - - const SymExpr *Sym = SymVal->getSymbol(); - QualType Ty = Sym->getType(); - - // Complex types are not modeled - if (Ty->isComplexType() || Ty->isComplexIntegerType()) - return false; - - // Non-IEEE 754 floating-point types are not modeled - if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) && - (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() || - &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble()))) - return false; - - if (isa(Sym)) - return true; - - SValBuilder &SVB = getSValBuilder(); - - if (const SymbolCast *SC = dyn_cast(Sym)) - return canReasonAbout(SVB.makeSymbolVal(SC->getOperand())); + : SMTConstraintManager(SE, SB, Solver) {} - if (const BinarySymExpr *BSE = dyn_cast(Sym)) { - if (const SymIntExpr *SIE = dyn_cast(BSE)) - return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS())); - - if (const IntSymExpr *ISE = dyn_cast(BSE)) - return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS())); + void addStateConstraints(ProgramStateRef State) const override { + // TODO: Don't add all the constraints, only the relevant ones + ConstraintZ3Ty CZ = State->get(); + ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end(); + + // Construct the logical AND of all the constraints + if (I != IE) { + std::vector ASTs; + + SMTExprRef Constraint = Solver->newExprRef(I++->second); + while (I != IE) { + Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second)); + } - if (const SymSymExpr *SSE = dyn_cast(BSE)) - return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) && - canReasonAbout(SVB.makeSymbolVal(SSE->getRHS())); + Solver->addConstraint(Constraint); + } } - llvm_unreachable("Unsupported expression to reason about!"); -} - -ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State, - SymbolRef Sym) { - QualType RetTy; - // The expression may be casted, so we cannot call getZ3DataExpr() directly - SMTExprRef VarExp = getZ3Expr(Sym, &RetTy); - SMTExprRef Exp = getZ3ZeroExpr(VarExp, RetTy, true); - - // Negate the constraint - SMTExprRef NotExp = getZ3ZeroExpr(VarExp, RetTy, false); - - Solver.reset(); - addStateConstraints(State); - - Solver.push(); - Solver.addConstraint(Exp); - ConditionTruthVal isSat = Solver.check(); - - Solver.pop(); - Solver.addConstraint(NotExp); - ConditionTruthVal isNotSat = Solver.check(); - - // Zero is the only possible solution - if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse()) - return true; - - // Zero is not a solution - if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue()) - return false; - - // Zero may be a solution - return ConditionTruthVal(); -} + bool canReasonAbout(SVal X) const override { + const TargetInfo &TI = getBasicVals().getContext().getTargetInfo(); -const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State, - SymbolRef Sym) const { - BasicValueFactory &BVF = getBasicVals(); - ASTContext &Ctx = BVF.getContext(); + Optional SymVal = X.getAs(); + if (!SymVal) + return true; - if (const SymbolData *SD = dyn_cast(Sym)) { + const SymExpr *Sym = SymVal->getSymbol(); QualType Ty = Sym->getType(); - assert(!Ty->isRealFloatingType()); - llvm::APSInt Value(Ctx.getTypeSize(Ty), - !Ty->isSignedIntegerOrEnumerationType()); - - SMTExprRef Exp = getZ3DataExpr(SD->getSymbolID(), Ty); - - Solver.reset(); - addStateConstraints(State); - - // Constraints are unsatisfiable - ConditionTruthVal isSat = Solver.check(); - if (!isSat.isConstrainedTrue()) - return nullptr; - - // Model does not assign interpretation - if (!Solver.getInterpretation(Exp, Value)) - return nullptr; - - // A value has been obtained, check if it is the only value - SMTExprRef NotExp = Solver.fromBinOp( - Exp, BO_NE, - Ty->isBooleanType() ? Solver.fromBoolean(Value.getBoolValue()) - : Solver.fromAPSInt(Value), - false); - - Solver.addConstraint(NotExp); - - ConditionTruthVal isNotSat = Solver.check(); - if (isNotSat.isConstrainedTrue()) - return nullptr; - - // This is the only solution, store it - return &BVF.getValue(Value); - } else if (const SymbolCast *SC = dyn_cast(Sym)) { - SymbolRef CastSym = SC->getOperand(); - QualType CastTy = SC->getType(); - // Skip the void type - if (CastTy->isVoidType()) - return nullptr; - - const llvm::APSInt *Value; - if (!(Value = getSymVal(State, CastSym))) - return nullptr; - return &BVF.Convert(SC->getType(), *Value); - } else if (const BinarySymExpr *BSE = dyn_cast(Sym)) { - const llvm::APSInt *LHS, *RHS; - if (const SymIntExpr *SIE = dyn_cast(BSE)) { - LHS = getSymVal(State, SIE->getLHS()); - RHS = &SIE->getRHS(); - } else if (const IntSymExpr *ISE = dyn_cast(BSE)) { - LHS = &ISE->getLHS(); - RHS = getSymVal(State, ISE->getRHS()); - } else if (const SymSymExpr *SSM = dyn_cast(BSE)) { - // Early termination to avoid expensive call - LHS = getSymVal(State, SSM->getLHS()); - RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr; - } else { - llvm_unreachable("Unsupported binary expression to get symbol value!"); - } - if (!LHS || !RHS) - return nullptr; + // Complex types are not modeled + if (Ty->isComplexType() || Ty->isComplexIntegerType()) + return false; - llvm::APSInt ConvertedLHS, ConvertedRHS; - QualType LTy, RTy; - std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS); - std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS); - doIntTypeConversion( - ConvertedLHS, LTy, ConvertedRHS, RTy); - return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS); - } + // Non-IEEE 754 floating-point types are not modeled + if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) && + (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() || + &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble()))) + return false; - llvm_unreachable("Unsupported expression to get symbol value!"); -} + if (isa(Sym)) + return true; -ProgramStateRef -Z3ConstraintManager::removeDeadBindings(ProgramStateRef State, - SymbolReaper &SymReaper) { - ConstraintZ3Ty CZ = State->get(); - ConstraintZ3Ty::Factory &CZFactory = State->get_context(); - - for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) { - if (SymReaper.maybeDead(I->first)) - CZ = CZFactory.remove(CZ, *I); - } + SValBuilder &SVB = getSValBuilder(); - return State->set(CZ); -} + if (const SymbolCast *SC = dyn_cast(Sym)) + return canReasonAbout(SVB.makeSymbolVal(SC->getOperand())); -void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) { - Solver.reset(); + if (const BinarySymExpr *BSE = dyn_cast(Sym)) { + if (const SymIntExpr *SIE = dyn_cast(BSE)) + return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS())); - for (const auto &I : CR) { - SymbolRef Sym = I.first; + if (const IntSymExpr *ISE = dyn_cast(BSE)) + return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS())); - SMTExprRef Constraints = Solver.fromBoolean(false); - for (const auto &Range : I.second) { - SMTExprRef SymRange = - getZ3RangeExpr(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 - Constraints = - Solver.fromBinOp(Constraints, BO_LOr, SymRange, /*IsSigned=*/true); + if (const SymSymExpr *SSE = dyn_cast(BSE)) + return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) && + canReasonAbout(SVB.makeSymbolVal(SSE->getRHS())); } - Solver.addConstraint(Constraints); - } -} - -clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() { - return Solver.check(); -} - -LLVM_DUMP_METHOD void Z3ConstraintManager::dump() const { Solver.dump(); } - -//===------------------------------------------------------------------===// -// Internal implementation. -//===------------------------------------------------------------------===// - -ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State, - SymbolRef Sym, - const SMTExprRef &Exp) { - // Check the model, avoid simplifying AST to save time - if (checkZ3Model(State, Exp).isConstrainedTrue()) - return State->add(std::make_pair(Sym, toZ3Expr(*Exp))); - - return nullptr; -} - -ConditionTruthVal -Z3ConstraintManager::checkZ3Model(ProgramStateRef State, - const SMTExprRef &Exp) const { - Solver.reset(); - Solver.addConstraint(Exp); - addStateConstraints(State); - return Solver.check(); -} - -SMTExprRef Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy, - bool *hasComparison) const { - if (hasComparison) { - *hasComparison = false; - } - - return getZ3SymExpr(Sym, RetTy, hasComparison); -} -SMTExprRef Z3ConstraintManager::getZ3NotExpr(const SMTExprRef &Exp) const { - return Solver.fromUnOp(UO_LNot, Exp); -} - -SMTExprRef Z3ConstraintManager::getZ3ZeroExpr(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)); - } else if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() || - Ty->isBlockPointerType() || Ty->isReferenceType()) { - bool isSigned = Ty->isSignedIntegerOrEnumerationType(); - // Skip explicit comparison for boolean types - if (Ty->isBooleanType()) - return Assumption ? getZ3NotExpr(Exp) : Exp; - return Solver.fromBinOp(Exp, Assumption ? BO_EQ : BO_NE, - Solver.fromInt("0", Ctx.getTypeSize(Ty)), isSigned); + llvm_unreachable("Unsupported expression to reason about!"); } - llvm_unreachable("Unsupported type for zero value!"); -} - -SMTExprRef Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy, - bool *hasComparison) const { - if (const SymbolData *SD = dyn_cast(Sym)) { - if (RetTy) - *RetTy = Sym->getType(); - - return getZ3DataExpr(SD->getSymbolID(), Sym->getType()); - } else if (const SymbolCast *SC = dyn_cast(Sym)) { - if (RetTy) - *RetTy = Sym->getType(); - - QualType FromTy; - SMTExprRef Exp = getZ3SymExpr(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 getZ3CastExpr(Exp, FromTy, Sym->getType()); - } else if (const BinarySymExpr *BSE = dyn_cast(Sym)) { - SMTExprRef Exp = getZ3SymBinExpr(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!"); -} + ProgramStateRef removeDeadBindings(ProgramStateRef State, + SymbolReaper &SymReaper) override { + ConstraintZ3Ty CZ = State->get(); + ConstraintZ3Ty::Factory &CZFactory = State->get_context(); -SMTExprRef Z3ConstraintManager::getZ3DataExpr(const SymbolID ID, - QualType Ty) const { - ASTContext &Ctx = getBasicVals().getContext(); - return Solver.fromData(ID, Ty, Ctx.getTypeSize(Ty)); -} - -SMTExprRef Z3ConstraintManager::getZ3CastExpr(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 Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE, - bool *hasComparison, - QualType *RetTy) const { - QualType LTy, RTy; - BinaryOperator::Opcode Op = BSE->getOpcode(); - - if (const SymIntExpr *SIE = dyn_cast(BSE)) { - SMTExprRef LHS = getZ3SymExpr(SIE->getLHS(), <y, hasComparison); - llvm::APSInt NewRInt; - std::tie(NewRInt, RTy) = fixAPSInt(SIE->getRHS()); - SMTExprRef RHS = Solver.fromAPSInt(NewRInt); - return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy); - } else if (const IntSymExpr *ISE = dyn_cast(BSE)) { - llvm::APSInt NewLInt; - std::tie(NewLInt, LTy) = fixAPSInt(ISE->getLHS()); - SMTExprRef LHS = Solver.fromAPSInt(NewLInt); - SMTExprRef RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison); - return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy); - } else if (const SymSymExpr *SSM = dyn_cast(BSE)) { - SMTExprRef LHS = getZ3SymExpr(SSM->getLHS(), <y, hasComparison); - SMTExprRef RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison); - return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy); - } else { - llvm_unreachable("Unsupported BinarySymExpr type!"); - } -} - -SMTExprRef Z3ConstraintManager::getZ3BinExpr( - 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; + for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) { + if (SymReaper.maybeDead(I->first)) + CZ = CZFactory.remove(CZ, *I); } - // 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 State->set(CZ); } - return LTy->isRealFloatingType() - ? Solver.fromFloatBinOp(NewLHS, Op, NewRHS) - : Solver.fromBinOp(NewLHS, Op, NewRHS, - LTy->isSignedIntegerOrEnumerationType()); -} - -SMTExprRef Z3ConstraintManager::getZ3RangeExpr(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 = getZ3Expr(Sym, &SymTy); - - // Construct single (in)equality - if (From == To) - return getZ3BinExpr(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 = getZ3BinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp, - FromTy, /*RetTy=*/nullptr); - SMTExprRef RHS = - getZ3BinExpr(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 Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const { - ASTContext &Ctx = getBasicVals().getContext(); - return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned()); -} - -std::pair -Z3ConstraintManager::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 Z3ConstraintManager::doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS, - QualType <y, QualType &RTy) const { - ASTContext &Ctx = getBasicVals().getContext(); - - assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!"); - // Perform type conversion - if (LTy->isIntegralOrEnumerationType() && - RTy->isIntegralOrEnumerationType()) { - if (LTy->isArithmeticType() && RTy->isArithmeticType()) { - doIntTypeConversion(LHS, LTy, RHS, RTy); - return; - } - } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) { - doFloatTypeConversion(LHS, LTy, RHS, RTy); - return; - } else 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; - } + ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, + const SMTExprRef &Exp) override { + // Check the model, avoid simplifying AST to save time + if (checkModel(State, Exp).isConstrainedTrue()) + return State->add(std::make_pair(Sym, toZ3Expr(*Exp))); - if (LTy == RTy) - return; + return nullptr; } - // Fallback: for the solver, assume that these types don't really matter - if ((LTy.getCanonicalType() == RTy.getCanonicalType()) || - (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) { - LTy = RTy; - return; - } + //==------------------------------------------------------------------------==/ + // Pretty-printing. + //==------------------------------------------------------------------------==/ - // TODO: Refine behavior for invalid type casts -} + void print(ProgramStateRef St, raw_ostream &OS, const char *nl, + const char *sep) override { -template -void Z3ConstraintManager::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; - } -} + ConstraintZ3Ty CZ = St->get(); -template -void Z3ConstraintManager::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!"); + OS << nl << sep << "Constraints:"; + for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) { + OS << nl << ' ' << I->first << " : "; + I->second.print(OS); + } + OS << nl; } -} - -//==------------------------------------------------------------------------==/ -// Pretty-printing. -//==------------------------------------------------------------------------==/ - -void Z3ConstraintManager::print(ProgramStateRef St, raw_ostream &OS, - const char *nl, const char *sep) { - - ConstraintZ3Ty CZ = St->get(); +}; // end class Z3ConstraintManager - OS << nl << sep << "Constraints:"; - for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) { - OS << nl << ' ' << I->first << " : "; - I->second.print(OS); - } - OS << nl; -} +} // end anonymous namespace #endif