[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–835

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–835

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.

clang/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;
+  SMTSolverRef Solver;
 
 public:
   SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
-                       SMTSolverRef &S)
+                       SMTSolverRef S)
       : SimpleConstraintManager(SE, SB), Solver(S) {}
   virtual ~SMTConstraintManager() = default;
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from SimpleConstraintManager.
   //===------------------------------------------------------------------===//
 
   ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,

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

 #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
 
 namespace clang {
 namespace ento {
 
 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();
 
     if (Ty->isRealFloatingType())
       return Solver->getFloatSort(BitWidth);
 
     return Solver->getBitvectorSort(BitWidth);
   }
 
   /// 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) {
     case UO_Minus:
       return Solver->mkBVNeg(Exp);
 
     case UO_Not:
       return Solver->mkBVNot(Exp);
 
     case UO_LNot:
       return Solver->mkNot(Exp);
 
     default:;
     }
     llvm_unreachable("Unimplemented opcode");
   }
 
   /// 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) {
     case UO_Minus:
       return Solver->mkFPNeg(Exp);
 
     case UO_LNot:
       return fromUnOp(Solver, Op, Exp);
 
     default:;
     }
     llvm_unreachable("Unimplemented opcode");
   }
 
   /// 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<SMTExprRef> &ASTs) {
     assert(!ASTs.empty());
 
     if (Op != BO_LAnd && Op != BO_LOr)
       llvm_unreachable("Unimplemented opcode");
 
     SMTExprRef res = ASTs.front();
     for (std::size_t i = 1; i < ASTs.size(); ++i)
       res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])
                             : Solver->mkOr(res, ASTs[i]);
     return res;
   }
 
   /// 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) &&
            "AST's must have the same sort!");
 
     switch (Op) {
     // Multiplicative operators
     case BO_Mul:
static inline SMTExprRef fromBinOp(SMTSolverRef Solver, const SMTExprRef &LHS,
 
     default:;
     }
     llvm_unreachable("Unimplemented opcode");
   }
 
   /// 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) {
     // Equality operators
     case BO_EQ:
       switch (RHS) {
       case llvm::APFloat::fcInfinity:
         return Solver->mkFPIsInfinite(LHS);
fromFloatSpecialBinOp(SMTSolverRef Solver, const SMTExprRef &LHS,
 
     default:;
     }
 
     llvm_unreachable("Unimplemented opcode");
   }
 
   /// 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) {
     assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
            "AST's must have the same sort!");
 
     switch (Op) {
     // Multiplicative operators
static inline SMTExprRef fromFloatBinOp(SMTSolverRef Solver,
     default:;
     }
 
     llvm_unreachable("Unimplemented opcode");
   }
 
   /// 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() &&
          ToTy->isIntegralOrEnumerationType()) ||
         (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
         (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
         (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
 
if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
       return ToTy->isSignedIntegerOrEnumerationType()
                  ? Solver->mkFPtoSBV(Exp, ToBitWidth)
                  : Solver->mkFPtoUBV(Exp, ToBitWidth);
 
     llvm_unreachable("Unsupported explicit type cast!");
   }
 
   // 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) {
     APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
     return TargetType.convert(V);
   }
 
   /// 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,
                     Ctx.getTypeSize(FromTy));
   }
 
   // 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,
                                       QualType *RetTy) {
     SMTExprRef NewLHS = LHS;
     SMTExprRef NewRHS = RHS;
     doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
 
static inline SMTExprRef getBinExpr(SMTSolverRef Solver, ASTContext &Ctx,
     return LTy->isRealFloatingType()
                ? fromFloatBinOp(Solver, NewLHS, Op, NewRHS)
                : fromBinOp(Solver, NewLHS, Op, NewRHS,
                            LTy->isSignedIntegerOrEnumerationType());
   }
 
   // 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;
     BinaryOperator::Opcode Op = BSE->getOpcode();
 
     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
       SMTExprRef LHS =
           getSymExpr(Solver, Ctx, SIE->getLHS(), &LTy, hasComparison);
if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
       return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
     }
 
     llvm_unreachable("Unsupported BinarySymExpr type!");
   }
 
   // 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<SymbolData>(Sym)) {
       if (RetTy)
         *RetTy = Sym->getType();
 
       return fromData(Solver, SD->getSymbolID(), Sym->getType(),
                       Ctx.getTypeSize(Sym->getType()));
static inline SMTExprRef getSymExpr(SMTSolverRef Solver, ASTContext &Ctx,
 
     llvm_unreachable("Unsupported SymbolRef type!");
   }
 
   // Generate an SMTExprRef 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.
-  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) {
       *hasComparison = false;
     }
 
     return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
   }
 
   // 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) {
 
     if (Ty->isRealFloatingType()) {
       llvm::APFloat Zero =
           llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
       return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
                             Solver->mkFloat(Zero));
if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
           isSigned);
     }
 
     llvm_unreachable("Unsupported type for zero value!");
   }
 
   // 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
     QualType FromTy;
     llvm::APSInt NewFromInt;
     std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
     SMTExprRef FromExp =
         Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
if (Int.getBitWidth() == 1 && getAPSIntType(Ctx, Int).isNull()) {
       NewInt = Int;
 
     return std::make_pair(NewInt, getAPSIntType(Ctx, NewInt));
   }
 
   // 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 &LTy, QualType &RTy) {
     assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
 
     // Perform type conversion
     if ((LTy->isIntegralOrEnumerationType() &&
          RTy->isIntegralOrEnumerationType()) &&
         (LTy->isArithmeticType() && RTy->isArithmeticType())) {
static inline void doTypeConversion(SMTSolverRef Solver, ASTContext &Ctx,
     }
 
     // TODO: Refine behavior for invalid type casts
   }
 
   // Perform implicit integer type conversion.
   // May modify all input parameters.
   // TODO: Refactor to use Sema::handleIntegerConversion()
-  template <typename T, T (*doCast)(SMTSolverRef &Solver, const T &, QualType,
+  template <typename T, T (*doCast)(SMTSolverRef Solver, const T &, QualType,
                                     uint64_t, QualType, uint64_t)>
-  static inline void doIntTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx,
+  static inline void doIntTypeConversion(SMTSolverRef Solver, ASTContext &Ctx,
                                          T &LHS, QualType &LTy, T &RHS,
                                          QualType &RTy) {
 
     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.
if (isLSignedTy == isRSignedTy) {
       LHS = (doCast)(Solver, 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 <typename T, T (*doCast)(SMTSolverRef &Solver, const T &, QualType,
+  template <typename T, T (*doCast)(SMTSolverRef Solver, const T &, QualType,
                                     uint64_t, QualType, uint64_t)>
-  static inline void
-  doFloatTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
-                        QualType &LTy, T &RHS, QualType &RTy) {
+  static inline void doFloatTypeConversion(SMTSolverRef Solver, ASTContext &Ctx,
+                                           T &LHS, QualType &LTy, T &RHS,
+                                           QualType &RTy) {
 
     uint64_t LBitWidth = Ctx.getTypeSize(LTy);
     uint64_t RBitWidth = Ctx.getTypeSize(RTy);
 
     // Perform float-point type promotion
     if (!LTy->isRealFloatingType()) {
       LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
       LTy = RTy;
if (order > 0) {
       llvm_unreachable("Unsupported floating-point type cast!");
     }
   }
 };
 } // namespace ento
 } // namespace clang
 
 #endif
 No newline at end of file

clang/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(),
+                                                 CreateZ3Solver());
 }