[analyzer] Got rid of the `Z3ConstraintManager` class

[mikhail.ramalho]

Summary

Now, instead of passing the reference to a shared_ptr, we pass the shared_ptr instead.

I've also removed the check if Z3 is present in CreateZ3ConstraintManager as this function already calls CreateZ3Solver that performs the exactly same check.

[mikhail.ramalho]

Moved CreateZ3Solver to SMTConstraintManager.

In the future, CreateZ3Solver should be renamed CreateSMTSolver to handle all backends.

[NoQ]

Makes perfect sense to me.

clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

834 ↗

(On Diff #176119)

Why are we even passing StMgr into this callback when it can be easily retrieved from Eng? :)

[mikhail.ramalho]

clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

834 ↗

(On Diff #176119)

I guess I simply copied it from RangeConstraintManager.cpp:311...

I can send another patch to remove the parameter from both functions. They are declared in ConstraintManager.h:200 and ConstraintManager.h:204.

include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

typedef llvm::ImmutableSet<
     std::pair<clang::ento::SymbolRef, const clang::ento::SMTExpr *>>
     ConstraintSMTTy;
 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy)
 
 namespace clang {
 namespace ento {
 
 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
-  SMTSolverRef &Solver;
+  mutable SMTSolverRef Solver = CreateZ3Solver();
 
 public:
-  SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
-                       SMTSolverRef &S)
-      : SimpleConstraintManager(SE, SB), Solver(S) {}
+  SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
+      : SimpleConstraintManager(SE, SB) {}
   virtual ~SMTConstraintManager() = default;
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from SimpleConstraintManager.
   //===------------------------------------------------------------------===//
 
   ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
                             bool Assumption) override {

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

public:
   /// 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);
   }
 }; // 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
 
 SMTSolverRef clang::ento::CreateZ3Solver() {
 #if CLANG_ANALYZER_WITH_Z3
   return llvm::make_unique<Z3Solver>();
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
                            "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
                            false);
   return nullptr;
 #endif
 }
 
 std::unique_ptr<ConstraintManager>
 ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
-#if CLANG_ANALYZER_WITH_Z3
-  return llvm::make_unique<Z3ConstraintManager>(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<SMTConstraintManager>(Eng, StMgr.getSValBuilder());
 }