Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -27,11 +27,11 @@ namespace ento { class SMTConstraintManager : public clang::ento::SimpleConstraintManager { - SMTSolverRef &Solver; + SMTSolverRef Solver; public: SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB, - SMTSolverRef &S) + SMTSolverRef S) : SimpleConstraintManager(SE, SB), Solver(S) {} virtual ~SMTConstraintManager() = default; Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h @@ -25,7 +25,7 @@ class SMTConv { public: // Returns an appropriate sort, given a QualType and it's bit width. - static inline SMTSortRef mkSort(SMTSolverRef &Solver, const QualType &Ty, + static inline SMTSortRef mkSort(SMTSolverRef Solver, const QualType &Ty, unsigned BitWidth) { if (Ty->isBooleanType()) return Solver->getBoolSort(); @@ -37,7 +37,7 @@ } /// Constructs an SMTExprRef from an unary operator. - static inline SMTExprRef fromUnOp(SMTSolverRef &Solver, + static inline SMTExprRef fromUnOp(SMTSolverRef Solver, const UnaryOperator::Opcode Op, const SMTExprRef &Exp) { switch (Op) { @@ -56,7 +56,7 @@ } /// Constructs an SMTExprRef from a floating-point unary operator. - static inline SMTExprRef fromFloatUnOp(SMTSolverRef &Solver, + static inline SMTExprRef fromFloatUnOp(SMTSolverRef Solver, const UnaryOperator::Opcode Op, const SMTExprRef &Exp) { switch (Op) { @@ -72,7 +72,7 @@ } /// Construct an SMTExprRef from a n-ary binary operator. - static inline SMTExprRef fromNBinOp(SMTSolverRef &Solver, + static inline SMTExprRef fromNBinOp(SMTSolverRef Solver, const BinaryOperator::Opcode Op, const std::vector &ASTs) { assert(!ASTs.empty()); @@ -88,8 +88,7 @@ } /// Construct an SMTExprRef from a binary operator. - static inline SMTExprRef fromBinOp(SMTSolverRef &Solver, - const SMTExprRef &LHS, + 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) && @@ -165,7 +164,7 @@ /// Construct an SMTExprRef from a special floating-point binary operator. static inline SMTExprRef - fromFloatSpecialBinOp(SMTSolverRef &Solver, const SMTExprRef &LHS, + fromFloatSpecialBinOp(SMTSolverRef Solver, const SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::APFloat::fltCategory &RHS) { switch (Op) { @@ -197,7 +196,7 @@ } /// Construct an SMTExprRef from a floating-point binary operator. - static inline SMTExprRef fromFloatBinOp(SMTSolverRef &Solver, + static inline SMTExprRef fromFloatBinOp(SMTSolverRef Solver, const SMTExprRef &LHS, const BinaryOperator::Opcode Op, const SMTExprRef &RHS) { @@ -256,7 +255,7 @@ /// Construct an SMTExprRef from a QualType FromTy to a QualType ToTy, and /// their bit widths. - static inline SMTExprRef fromCast(SMTSolverRef &Solver, const SMTExprRef &Exp, + static inline SMTExprRef fromCast(SMTSolverRef Solver, const SMTExprRef &Exp, QualType ToTy, uint64_t ToBitWidth, QualType FromTy, uint64_t FromBitWidth) { if ((FromTy->isIntegralOrEnumerationType() && @@ -307,7 +306,7 @@ } // Callback function for doCast parameter on APSInt type. - static inline llvm::APSInt castAPSInt(SMTSolverRef &Solver, + static inline llvm::APSInt castAPSInt(SMTSolverRef Solver, const llvm::APSInt &V, QualType ToTy, uint64_t ToWidth, QualType FromTy, uint64_t FromWidth) { @@ -316,14 +315,14 @@ } /// Construct an SMTExprRef from a SymbolData. - static inline SMTExprRef fromData(SMTSolverRef &Solver, const SymbolID ID, + 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, + static inline SMTExprRef getCastExpr(SMTSolverRef Solver, ASTContext &Ctx, const SMTExprRef &Exp, QualType FromTy, QualType ToTy) { return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy, @@ -332,7 +331,7 @@ // Wrapper to generate SMTExprRef from unpacked binary symbolic expression. // Sets the RetTy parameter. See getSMTExprRef(). - static inline SMTExprRef getBinExpr(SMTSolverRef &Solver, ASTContext &Ctx, + static inline SMTExprRef getBinExpr(SMTSolverRef Solver, ASTContext &Ctx, const SMTExprRef &LHS, QualType LTy, BinaryOperator::Opcode Op, const SMTExprRef &RHS, QualType RTy, @@ -368,7 +367,7 @@ // Wrapper to generate SMTExprRef from BinarySymExpr. // Sets the hasComparison and RetTy parameters. See getSMTExprRef(). - static inline SMTExprRef getSymBinExpr(SMTSolverRef &Solver, ASTContext &Ctx, + static inline SMTExprRef getSymBinExpr(SMTSolverRef Solver, ASTContext &Ctx, const BinarySymExpr *BSE, bool *hasComparison, QualType *RetTy) { QualType LTy, RTy; @@ -405,7 +404,7 @@ // Recursive implementation to unpack and generate symbolic expression. // Sets the hasComparison and RetTy parameters. See getExpr(). - static inline SMTExprRef getSymExpr(SMTSolverRef &Solver, ASTContext &Ctx, + static inline SMTExprRef getSymExpr(SMTSolverRef Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy, bool *hasComparison) { if (const SymbolData *SD = dyn_cast(Sym)) { @@ -447,7 +446,7 @@ // 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, + static inline SMTExprRef getExpr(SMTSolverRef Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy = nullptr, bool *hasComparison = nullptr) { if (hasComparison) { @@ -458,7 +457,7 @@ } // Generate an SMTExprRef that compares the expression to zero. - static inline SMTExprRef getZeroExpr(SMTSolverRef &Solver, ASTContext &Ctx, + static inline SMTExprRef getZeroExpr(SMTSolverRef Solver, ASTContext &Ctx, const SMTExprRef &Exp, QualType Ty, bool Assumption) { @@ -488,7 +487,7 @@ // Wrapper to generate SMTExprRef from a range. If From == To, an equality // will be created instead. - static inline SMTExprRef getRangeExpr(SMTSolverRef &Solver, ASTContext &Ctx, + static inline SMTExprRef getRangeExpr(SMTSolverRef Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) { // Convert lower bound @@ -551,7 +550,7 @@ // 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, + 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!"); @@ -625,9 +624,9 @@ // 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, + static inline void doIntTypeConversion(SMTSolverRef Solver, ASTContext &Ctx, T &LHS, QualType <y, T &RHS, QualType &RTy) { @@ -708,11 +707,11 @@ // 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) { + 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); Index: clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -815,14 +815,6 @@ } }; // end class Z3Solver -class Z3ConstraintManager : public SMTConstraintManager { - SMTSolverRef Solver = CreateZ3Solver(); - -public: - Z3ConstraintManager(SubEngine *SE, SValBuilder &SB) - : SMTConstraintManager(SE, SB, Solver) {} -}; // end class Z3ConstraintManager - } // end anonymous namespace #endif @@ -840,12 +832,6 @@ std::unique_ptr ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) { -#if CLANG_ANALYZER_WITH_Z3 - return llvm::make_unique(Eng, StMgr.getSValBuilder()); -#else - llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild " - "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON", - false); - return nullptr; -#endif + return llvm::make_unique(Eng, StMgr.getSValBuilder(), + CreateZ3Solver()); }