From: Mikhail R. Gadelha Date: Wed, 28 Nov 2018 17:22:49 +0000 (+0000) Subject: [analyzer] Cleanup constructors in the Z3 backend X-Git-Tag: llvmorg-8.0.0-rc1~3398 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=ad320ae3e241e125b030c4b431574a3e789141d8;p=platform%2Fupstream%2Fllvm.git [analyzer] Cleanup constructors in the Z3 backend Summary: Left only the constructors that are actually required, and marked the move constructors as deleted. They are not used anymore and we were never sure they've actually worked correctly. Reviewers: george.karpenkov, NoQ Reviewed By: george.karpenkov Subscribers: xazax.hun, baloghadamsoftware, szepet, a.sidorin, Szelethus, donat.nagy, dkrupp Differential Revision: https://reviews.llvm.org/D54974 llvm-svn: 347777 --- diff --git a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp index 61bba56..c4729f9 100644 --- a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ b/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -77,32 +77,27 @@ class Z3Sort : public SMTSort { public: /// Default constructor, mainly used by make_shared - Z3Sort(Z3Context &C, Z3_sort ZS) : SMTSort(), Context(C), Sort(ZS) { + Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) { Z3_inc_ref(Context.Context, reinterpret_cast(Sort)); } /// Override implicit copy constructor for correct reference counting. - Z3Sort(const Z3Sort &Copy) - : SMTSort(), Context(Copy.Context), Sort(Copy.Sort) { + Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) { Z3_inc_ref(Context.Context, reinterpret_cast(Sort)); } - /// Provide move constructor - Z3Sort(Z3Sort &&Move) : SMTSort(), Context(Move.Context), Sort(nullptr) { - *this = std::move(Move); - } - - /// Provide move assignment constructor - Z3Sort &operator=(Z3Sort &&Move) { - if (this != &Move) { - if (Sort) - Z3_dec_ref(Context.Context, reinterpret_cast(Sort)); - Sort = Move.Sort; - Move.Sort = nullptr; - } + /// Override implicit copy assignment constructor for correct reference + /// counting. + Z3Sort &operator=(const Z3Sort &Other) { + Z3_inc_ref(Context.Context, reinterpret_cast(Other.Sort)); + Z3_dec_ref(Context.Context, reinterpret_cast(Sort)); + Sort = Other.Sort; return *this; } + Z3Sort(Z3Sort &&Other) = delete; + Z3Sort &operator=(Z3Sort &&Other) = delete; + ~Z3Sort() { if (Sort) Z3_dec_ref(Context.Context, reinterpret_cast(Sort)); @@ -134,13 +129,6 @@ public: static_cast(Other).Sort); } - Z3Sort &operator=(const Z3Sort &Move) { - Z3_inc_ref(Context.Context, reinterpret_cast(Move.Sort)); - Z3_dec_ref(Context.Context, reinterpret_cast(Sort)); - Sort = Move.Sort; - return *this; - } - void print(raw_ostream &OS) const override { OS << Z3_sort_to_string(Context.Context, Sort); } @@ -167,22 +155,18 @@ public: Z3_inc_ref(Context.Context, AST); } - /// Provide move constructor - Z3Expr(Z3Expr &&Move) : SMTExpr(), Context(Move.Context), AST(nullptr) { - *this = std::move(Move); - } - - /// Provide move assignment constructor - Z3Expr &operator=(Z3Expr &&Move) { - if (this != &Move) { - if (AST) - Z3_dec_ref(Context.Context, AST); - AST = Move.AST; - Move.AST = nullptr; - } + /// Override implicit copy assignment constructor for correct reference + /// counting. + Z3Expr &operator=(const Z3Expr &Other) { + Z3_inc_ref(Context.Context, Other.AST); + Z3_dec_ref(Context.Context, AST); + AST = Other.AST; return *this; } + Z3Expr(Z3Expr &&Other) = delete; + Z3Expr &operator=(Z3Expr &&Other) = delete; + ~Z3Expr() { if (AST) Z3_dec_ref(Context.Context, AST); @@ -202,14 +186,6 @@ public: static_cast(Other).AST); } - /// Override implicit move constructor for correct reference counting. - Z3Expr &operator=(const Z3Expr &Move) { - Z3_inc_ref(Context.Context, Move.AST); - Z3_dec_ref(Context.Context, AST); - AST = Move.AST; - return *this; - } - void print(raw_ostream &OS) const override { OS << Z3_ast_to_string(Context.Context, AST); } @@ -228,30 +204,13 @@ class Z3Model { public: Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) { - assert(C.Context != nullptr); - Z3_model_inc_ref(Context.Context, Model); - } - - /// Override implicit copy constructor for correct reference counting. - Z3Model(const Z3Model &Copy) : Context(Copy.Context), Model(Copy.Model) { Z3_model_inc_ref(Context.Context, Model); } - /// Provide move constructor - Z3Model(Z3Model &&Move) : Context(Move.Context), Model(nullptr) { - *this = std::move(Move); - } - - /// Provide move assignment constructor - Z3Model &operator=(Z3Model &&Move) { - if (this != &Move) { - if (Model) - Z3_model_dec_ref(Context.Context, Model); - Model = Move.Model; - Move.Model = nullptr; - } - return *this; - } + Z3Model(const Z3Model &Other) = delete; + Z3Model(Z3Model &&Other) = delete; + Z3Model &operator=(Z3Model &Other) = delete; + Z3Model &operator=(Z3Model &&Other) = delete; ~Z3Model() { if (Model) @@ -310,32 +269,14 @@ class Z3Solver : public SMTSolver { Z3_solver Solver; public: - Z3Solver() : SMTSolver(), Solver(Z3_mk_simple_solver(Context.Context)) { + Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) { Z3_solver_inc_ref(Context.Context, Solver); } - /// Override implicit copy constructor for correct reference counting. - Z3Solver(const Z3Solver &Copy) - : SMTSolver(), Context(Copy.Context), Solver(Copy.Solver) { - Z3_solver_inc_ref(Context.Context, Solver); - } - - /// Provide move constructor - Z3Solver(Z3Solver &&Move) - : SMTSolver(), Context(Move.Context), Solver(nullptr) { - *this = std::move(Move); - } - - /// Provide move assignment constructor - Z3Solver &operator=(Z3Solver &&Move) { - if (this != &Move) { - if (Solver) - Z3_solver_dec_ref(Context.Context, Solver); - Solver = Move.Solver; - Move.Solver = nullptr; - } - return *this; - } + Z3Solver(const Z3Solver &Other) = delete; + Z3Solver(Z3Solver &&Other) = delete; + Z3Solver &operator=(Z3Solver &Other) = delete; + Z3Solver &operator=(Z3Solver &&Other) = delete; ~Z3Solver() { if (Solver) @@ -809,7 +750,7 @@ public: } bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override { - Z3Model Model = getModel(); + Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); Z3_func_decl Func = Z3_get_app_decl( Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE) @@ -823,7 +764,7 @@ public: } bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override { - Z3Model Model = getModel(); + Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); Z3_func_decl Func = Z3_get_app_decl( Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE) @@ -854,12 +795,6 @@ public: return Z3_solver_pop(Context.Context, Solver, NumStates); } - /// Get a model from the solver. Caller should check the model is - /// satisfiable. - Z3Model getModel() { - return Z3Model(Context, Z3_solver_get_model(Context.Context, Solver)); - } - bool isFPSupported() override { return true; } /// Reset the solver and remove all constraints.