[analyzer] Cleanup constructors in the Z3 backend

[mikhail.ramalho]

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.

[george.karpenkov]

I'm OK with the change; not sure why you've decided to remove a creator for a model (it should probably have a different name though)

clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

80 ↗

(On Diff #175577)

TBH I have no idea what calling SMTSort with no argument does.
Same as not doing anything?

859 ↗

(On Diff #175577)

Should this be removed?

[mikhail.ramalho]

clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

80 ↗

(On Diff #175577)

If there is no call to the base class constructor, the compiler will insert a call to the base class with no argument.

But yeah, the SMTSort constructor doesn't initialize anything.

859 ↗

(On Diff #175577)

Yep, the getModel method is not part of the API, it's Z3 specific. No point in keeping it around.

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

class Z3Sort : public SMTSort {
   friend class Z3Solver;
 
   Z3Context &Context;
 
   Z3_sort Sort;
 
 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<Z3_ast>(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<Z3_ast>(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<Z3_ast>(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<Z3_ast>(Other.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<Z3_ast>(Sort));
   }
 
   bool isBitvectorSortImpl() const override {
     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
   }
return Z3_fpa_get_ebits(Context.Context, Sort) +
            Z3_fpa_get_sbits(Context.Context, Sort);
   }
 
   bool equal_to(SMTSort const &Other) const override {
     return Z3_is_eq_sort(Context.Context, Sort,
                          static_cast<const Z3Sort &>(Other).Sort);
   }
 
-  Z3Sort &operator=(const Z3Sort &Move) {
-    Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Move.Sort));
-    Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
-    Sort = Move.Sort;
-    return *this;
-  }
-
   void print(raw_ostream &OS) const override {
     OS << Z3_sort_to_string(Context.Context, Sort);
   }
 }; // end class Z3Sort
 
 static const Z3Sort &toZ3Sort(const SMTSort &S) {
   return static_cast<const Z3Sort &>(S);
 }
Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
     Z3_inc_ref(Context.Context, AST);
   }
 
   /// Override implicit copy constructor for correct reference counting.
   Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
     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);
+    AST = Other.AST;
     return *this;
   }
 
+  Z3Expr(Z3Expr &&Other) = delete;
+  Z3Expr &operator=(Z3Expr &&Other) = delete;
+
   ~Z3Expr() {
     if (AST)
       Z3_dec_ref(Context.Context, AST);
   }
 
   void Profile(llvm::FoldingSetNodeID &ID) const override {
     ID.AddInteger(Z3_get_ast_hash(Context.Context, AST));
   }
 
   /// Comparison of AST equality, not model equivalence.
   bool equal_to(SMTExpr const &Other) const override {
     assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
                          Z3_get_sort(Context.Context,
                                      static_cast<const Z3Expr &>(Other).AST)) &&
            "AST's must have the same sort");
     return Z3_is_eq_ast(Context.Context, AST,
                         static_cast<const Z3Expr &>(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);
   }
 }; // end class Z3Expr
 
 static const Z3Expr &toZ3Expr(const SMTExpr &E) {
   return static_cast<const Z3Expr &>(E);
 }
 
 class Z3Model {
   friend class Z3Solver;
 
   Z3Context &Context;
 
   Z3_model Model;
 
 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)
       Z3_model_dec_ref(Context.Context, Model);
   }
 
   void print(raw_ostream &OS) const {
     OS << Z3_model_to_string(Context.Context, Model);

 class Z3Solver : public SMTSolver {
   friend class Z3ConstraintManager;
 
   Z3Context Context;
 
   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)
       Z3_solver_dec_ref(Context.Context, Solver);
   }
 
   void addConstraint(const SMTExprRef &Exp) const override {
     Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
if (Sort->isBooleanSort()) {
                          Int.isUnsigned());
       return true;
     }
 
     llvm_unreachable("Unsupported sort to integer!");
   }
 
   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)
       return false;
 
     SMTExprRef Assign = newExprRef(
         Z3Expr(Context,
                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
     SMTSortRef Sort = getSort(Assign);
     return toAPSInt(Sort, Assign, Int, true);
   }
 
   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)
       return false;
 
     SMTExprRef Assign = newExprRef(
         Z3Expr(Context,
                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
public:
 
   void push() override { return Z3_solver_push(Context.Context, Solver); }
 
   void pop(unsigned NumStates = 1) override {
     assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
     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.
   void reset() override { Z3_solver_reset(Context.Context, Solver); }
 
   void print(raw_ostream &OS) const override {
     OS << Z3_solver_to_string(Context.Context, Solver);
   }