[analyzer] Moved non solver specific code from Z3ConstraintManager to SMTConstraintManager

[mikhail.ramalho]

Summary

This patch moves a lot of code from Z3ConstraintManager to SMTConstraintManager, leaving only the necessary:

• canReasonAbout which returns if a Solver can handle a given SVal (should be moved to SMTSolver in the future).
• removeDeadBindings, assumeExpr and print: methods that need to use ConstraintZ3Ty, can probably be moved to SMTConstraintManager in the future.

The patch creates a new file, SMTConstraintManager.cpp with the moved code. Conceptually, this is move in the right direction and needs further improvements: SMTConstraintManager still does a lot of things that are not required by a ConstraintManager.

We ought to move the unrelated to SMTSolver and remove everything that's not related to a ConstraintManager. In particular, we could remove addRangeConstraints and isModelFeasible, and make the refutation manager create an Z3Solver directly.

[george.karpenkov]

OK but let's not do too many refactorings.

[mikhail.ramalho]

Return addStateConstraints to SMTConstraintManager, as the SMT API shouldn't know about ProgramStateRefs

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

 //  every SMT solver specific class.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
 
 namespace clang {
 namespace ento {
 
 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
+  SMTSolverRef &Solver;
 
 public:
-  SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
-      : SimpleConstraintManager(SE, SB) {}
+  SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
+                       SMTSolverRef &S)
+      : SimpleConstraintManager(SE, SB), Solver(S) {}
   virtual ~SMTConstraintManager() = default;
 
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from SimpleConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
+                            bool Assumption) override;
+
+  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
+                                          const llvm::APSInt &From,
+                                          const llvm::APSInt &To,
+                                          bool InRange) override;
+
+  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
+                                       bool Assumption) override;
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from ConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
+
+  const llvm::APSInt *getSymVal(ProgramStateRef State,
+                                SymbolRef Sym) const override;
+
   /// Converts the ranged constraints of a set of symbols to SMT
   ///
   /// \param CR The set of constraints.
-  virtual void addRangeConstraints(clang::ento::ConstraintRangeTy CR) = 0;
+  void addRangeConstraints(clang::ento::ConstraintRangeTy CR);
 
   /// Checks if the added constraints are satisfiable
-  virtual clang::ento::ConditionTruthVal isModelFeasible() = 0;
+  clang::ento::ConditionTruthVal isModelFeasible();
 
   /// Dumps SMT formula
-  LLVM_DUMP_METHOD virtual void dump() const = 0;
+  LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
+
+protected:
+  //===------------------------------------------------------------------===//
+  // Internal implementation.
+  //===------------------------------------------------------------------===//
+
+  // Check whether a new model is satisfiable, and update the program state.
+  virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
+                                     const SMTExprRef &Exp) = 0;
+
+  /// Given a program state, construct the logical conjunction and add it to
+  /// the solver
+  virtual void addStateConstraints(ProgramStateRef State) const = 0;
+
+  // Generate and check a Z3 model, using the given constraint.
+  ConditionTruthVal checkModel(ProgramStateRef State,
+                               const SMTExprRef &Exp) const;
+
+  // Generate a Z3Expr 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.
+  SMTExprRef getExpr(SymbolRef Sym, QualType *RetTy = nullptr,
+                     bool *hasComparison = nullptr) const;
+
+  // Generate a Z3Expr that takes the logical not of an expression.
+  SMTExprRef getNotExpr(const SMTExprRef &Exp) const;
+
+  // Generate a Z3Expr that compares the expression to zero.
+  SMTExprRef getZeroExpr(const SMTExprRef &Exp, QualType RetTy,
+                         bool Assumption) const;
+
+  // Recursive implementation to unpack and generate symbolic expression.
+  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
+  SMTExprRef getSymExpr(SymbolRef Sym, QualType *RetTy,
+                        bool *hasComparison) const;
+
+  // Wrapper to generate Z3Expr from SymbolData.
+  SMTExprRef getDataExpr(const SymbolID ID, QualType Ty) const;
+
+  // Wrapper to generate Z3Expr from SymbolCast.
+  SMTExprRef getCastExpr(const SMTExprRef &Exp, QualType FromTy,
+                         QualType Ty) const;
+
+  // Wrapper to generate Z3Expr from BinarySymExpr.
+  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
+  SMTExprRef getSymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
+                           QualType *RetTy) const;
+
+  // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
+  // Sets the RetTy parameter. See getZ3Expr().
+  SMTExprRef getBinExpr(const SMTExprRef &LHS, QualType LTy,
+                        BinaryOperator::Opcode Op, const SMTExprRef &RHS,
+                        QualType RTy, QualType *RetTy) const;
+
+  // Wrapper to generate Z3Expr from a range. If From == To, an equality will
+  // be created instead.
+  SMTExprRef getRangeExpr(SymbolRef Sym, const llvm::APSInt &From,
+                          const llvm::APSInt &To, bool InRange);
+
+  //===------------------------------------------------------------------===//
+  // Helper functions.
+  //===------------------------------------------------------------------===//
+
+  // Recover the QualType of an APSInt.
+  // TODO: Refactor to put elsewhere
+  QualType getAPSIntType(const llvm::APSInt &Int) const;
+
+  // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
+  std::pair<llvm::APSInt, QualType> fixAPSInt(const llvm::APSInt &Int) const;
+
+  // Perform implicit type conversion on binary symbolic expressions.
+  // May modify all input parameters.
+  // TODO: Refactor to use built-in conversion functions
+  void doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS, QualType &LTy,
+                        QualType &RTy) const;
+
+  // Perform implicit integer type conversion.
+  // May modify all input parameters.
+  // TODO: Refactor to use Sema::handleIntegerConversion()
+  template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t,
+                                               QualType, uint64_t)>
+  void doIntTypeConversion(T &LHS, QualType &LTy, T &RHS, QualType &RTy) const {
+    ASTContext &Ctx = getBasicVals().getContext();
+    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.
+    // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
+    if (LTy->isPromotableIntegerType()) {
+      QualType NewTy = Ctx.getPromotedIntegerType(LTy);
+      uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
+      LHS = ((*Solver).*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);
+      LTy = NewTy;
+      LBitWidth = NewBitWidth;
+    }
+    if (RTy->isPromotableIntegerType()) {
+      QualType NewTy = Ctx.getPromotedIntegerType(RTy);
+      uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
+      RHS = ((*Solver).*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth);
+      RTy = NewTy;
+      RBitWidth = NewBitWidth;
+    }
+
+    if (LTy == RTy)
+      return;
+
+    // Perform integer type conversion
+    // Note: Safe to skip updating bitwidth because this must terminate
+    bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
+    bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
+
+    int order = Ctx.getIntegerTypeOrder(LTy, RTy);
+    if (isLSignedTy == isRSignedTy) {
+      // Same signedness; use the higher-ranked type
+      if (order == 1) {
+        RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+        RTy = LTy;
+      } else {
+        LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+        LTy = RTy;
+      }
+    } else if (order != (isLSignedTy ? 1 : -1)) {
+      // The unsigned type has greater than or equal rank to the
+      // signed type, so use the unsigned type
+      if (isRSignedTy) {
+        RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+        RTy = LTy;
+      } else {
+        LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+        LTy = RTy;
+      }
+    } else if (LBitWidth != RBitWidth) {
+      // The two types are different widths; if we are here, that
+      // means the signed type is larger than the unsigned type, so
+      // use the signed type.
+      if (isLSignedTy) {
+        RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+        RTy = LTy;
+      } else {
+        LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+        LTy = RTy;
+      }
+    } else {
+      // The signed type is higher-ranked than the unsigned type,
+      // but isn't actually any bigger (like unsigned int and long
+      // on most 32-bit systems).  Use the unsigned type corresponding
+      // to the signed type.
+      QualType NewTy =
+          Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
+      RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+      RTy = NewTy;
+      LHS = ((*Solver).*doCast)(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 (SMTSolver::*doCast)(const T &, QualType, uint64_t,
+                                               QualType, uint64_t)>
+  void doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
+                             QualType &RTy) const {
+    ASTContext &Ctx = getBasicVals().getContext();
+
+    uint64_t LBitWidth = Ctx.getTypeSize(LTy);
+    uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+
+    // Perform float-point type promotion
+    if (!LTy->isRealFloatingType()) {
+      LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+      LTy = RTy;
+      LBitWidth = RBitWidth;
+    }
+    if (!RTy->isRealFloatingType()) {
+      RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+      RTy = LTy;
+      RBitWidth = LBitWidth;
+    }
+
+    if (LTy == RTy)
+      return;
+
+    // If we have two real floating types, convert the smaller operand to the
+    // bigger result
+    // Note: Safe to skip updating bitwidth because this must terminate
+    int order = Ctx.getFloatingTypeOrder(LTy, RTy);
+    if (order > 0) {
+      RHS = ((*Solver).*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
+      RTy = LTy;
+    } else if (order == 0) {
+      LHS = ((*Solver).*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
+      LTy = RTy;
+    } else {
+      llvm_unreachable("Unsupported floating-point type cast!");
+    }
+  }
 }; // end class SMTConstraintManager
 
 } // namespace ento
 } // namespace clang
 
 #endif

lib/StaticAnalyzer/Core/CMakeLists.txt

add_clang_library(clangStaticAnalyzerCore
   ProgramState.cpp
   RangeConstraintManager.cpp
   RangedConstraintManager.cpp
   RegionStore.cpp
   SValBuilder.cpp
   SVals.cpp
   SimpleConstraintManager.cpp
   SimpleSValBuilder.cpp
+  SMTConstraintManager.cpp
   Store.cpp
   SubEngine.cpp
   SymbolManager.cpp
   WorkList.cpp
   Z3ConstraintManager.cpp
 
   LINK_LIBS
   clangAST

lib/StaticAnalyzer/Core/SMTConstraintManager.cpp

+//== SMTConstraintManager.cpp -----------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
+#include "clang/Basic/TargetInfo.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+
+using namespace clang;
+using namespace ento;
+
+void SMTConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
+  Solver->reset();
+
+  for (const auto &I : CR) {
+    SymbolRef Sym = I.first;
+
+    SMTExprRef Constraints = Solver->fromBoolean(false);
+    for (const auto &Range : I.second) {
+      SMTExprRef SymRange =
+          getRangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true);
+
+      // FIXME: the last argument (isSigned) is not used when generating the
+      // or expression, as both arguments are booleans
+      Constraints =
+          Solver->fromBinOp(Constraints, BO_LOr, SymRange, /*IsSigned=*/true);
+    }
+    Solver->addConstraint(Constraints);
+  }
+}
+
+clang::ento::ConditionTruthVal SMTConstraintManager::isModelFeasible() {
+  return Solver->check();
+}
+
+ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State,
+                                                SymbolRef Sym,
+                                                bool Assumption) {
+  QualType RetTy;
+  bool hasComparison;
+
+  SMTExprRef Exp = getExpr(Sym, &RetTy, &hasComparison);
+  // Create zero comparison for implicit boolean cast, with reversed assumption
+  if (!hasComparison && !RetTy->isBooleanType())
+    return assumeExpr(State, Sym, getZeroExpr(Exp, RetTy, !Assumption));
+
+  return assumeExpr(State, Sym, Assumption ? Exp : getNotExpr(Exp));
+}
+
+ProgramStateRef SMTConstraintManager::assumeSymInclusiveRange(
+    ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+    const llvm::APSInt &To, bool InRange) {
+  return assumeExpr(State, Sym, getRangeExpr(Sym, From, To, InRange));
+}
+
+ProgramStateRef
+SMTConstraintManager::assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
+                                           bool Assumption) {
+  // Skip anything that is unsupported
+  return State;
+}
+
+ConditionTruthVal SMTConstraintManager::checkNull(ProgramStateRef State,
+                                                  SymbolRef Sym) {
+  QualType RetTy;
+  // The expression may be casted, so we cannot call getZ3DataExpr() directly
+  SMTExprRef VarExp = getExpr(Sym, &RetTy);
+  SMTExprRef Exp = getZeroExpr(VarExp, RetTy, true);
+
+  // Negate the constraint
+  SMTExprRef NotExp = getZeroExpr(VarExp, RetTy, false);
+
+  Solver->reset();
+  addStateConstraints(State);
+
+  Solver->push();
+  Solver->addConstraint(Exp);
+  ConditionTruthVal isSat = Solver->check();
+
+  Solver->pop();
+  Solver->addConstraint(NotExp);
+  ConditionTruthVal isNotSat = Solver->check();
+
+  // Zero is the only possible solution
+  if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
+    return true;
+
+  // Zero is not a solution
+  if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
+    return false;
+
+  // Zero may be a solution
+  return ConditionTruthVal();
+}
+
+const llvm::APSInt *SMTConstraintManager::getSymVal(ProgramStateRef State,
+                                                    SymbolRef Sym) const {
+  BasicValueFactory &BVF = getBasicVals();
+  ASTContext &Ctx = BVF.getContext();
+
+  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
+    QualType Ty = Sym->getType();
+    assert(!Ty->isRealFloatingType());
+    llvm::APSInt Value(Ctx.getTypeSize(Ty),
+                       !Ty->isSignedIntegerOrEnumerationType());
+
+    SMTExprRef Exp = getDataExpr(SD->getSymbolID(), Ty);
+
+    Solver->reset();
+    addStateConstraints(State);
+
+    // Constraints are unsatisfiable
+    ConditionTruthVal isSat = Solver->check();
+    if (!isSat.isConstrainedTrue())
+      return nullptr;
+
+    // Model does not assign interpretation
+    if (!Solver->getInterpretation(Exp, Value))
+      return nullptr;
+
+    // A value has been obtained, check if it is the only value
+    SMTExprRef NotExp = Solver->fromBinOp(
+        Exp, BO_NE,
+        Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
+                            : Solver->fromAPSInt(Value),
+        false);
+
+    Solver->addConstraint(NotExp);
+
+    ConditionTruthVal isNotSat = Solver->check();
+    if (isNotSat.isConstrainedTrue())
+      return nullptr;
+
+    // This is the only solution, store it
+    return &BVF.getValue(Value);
+  }
+
+  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
+    SymbolRef CastSym = SC->getOperand();
+    QualType CastTy = SC->getType();
+    // Skip the void type
+    if (CastTy->isVoidType())
+      return nullptr;
+
+    const llvm::APSInt *Value;
+    if (!(Value = getSymVal(State, CastSym)))
+      return nullptr;
+    return &BVF.Convert(SC->getType(), *Value);
+  }
+
+  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+    const llvm::APSInt *LHS, *RHS;
+    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
+      LHS = getSymVal(State, SIE->getLHS());
+      RHS = &SIE->getRHS();
+    } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
+      LHS = &ISE->getLHS();
+      RHS = getSymVal(State, ISE->getRHS());
+    } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
+      // Early termination to avoid expensive call
+      LHS = getSymVal(State, SSM->getLHS());
+      RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
+    } else {
+      llvm_unreachable("Unsupported binary expression to get symbol value!");
+    }
+
+    if (!LHS || !RHS)
+      return nullptr;
+
+    llvm::APSInt ConvertedLHS, ConvertedRHS;
+    QualType LTy, RTy;
+    std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS);
+    std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS);
+    doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
+        ConvertedLHS, LTy, ConvertedRHS, RTy);
+    return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
+  }
+
+  llvm_unreachable("Unsupported expression to get symbol value!");
+}
+
+//===------------------------------------------------------------------===//
+// Internal implementation.
+//===------------------------------------------------------------------===//
+
+ConditionTruthVal
+SMTConstraintManager::checkModel(ProgramStateRef State,
+                                 const SMTExprRef &Exp) const {
+  Solver->reset();
+  Solver->addConstraint(Exp);
+  addStateConstraints(State);
+  return Solver->check();
+}
+
+SMTExprRef SMTConstraintManager::getExpr(SymbolRef Sym, QualType *RetTy,
+                                         bool *hasComparison) const {
+  if (hasComparison) {
+    *hasComparison = false;
+  }
+
+  return getSymExpr(Sym, RetTy, hasComparison);
+}
+
+SMTExprRef SMTConstraintManager::getNotExpr(const SMTExprRef &Exp) const {
+  return Solver->fromUnOp(UO_LNot, Exp);
+}
+
+SMTExprRef SMTConstraintManager::getZeroExpr(const SMTExprRef &Exp, QualType Ty,
+                                             bool Assumption) const {
+  ASTContext &Ctx = getBasicVals().getContext();
+  if (Ty->isRealFloatingType()) {
+    llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
+    return Solver->fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
+                                  Solver->fromAPFloat(Zero));
+  }
+
+  if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
+      Ty->isBlockPointerType() || Ty->isReferenceType()) {
+
+    // Skip explicit comparison for boolean types
+    bool isSigned = Ty->isSignedIntegerOrEnumerationType();
+    if (Ty->isBooleanType())
+      return Assumption ? getNotExpr(Exp) : Exp;
+
+    return Solver->fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
+                             Solver->fromInt("0", Ctx.getTypeSize(Ty)),
+                             isSigned);
+  }
+
+  llvm_unreachable("Unsupported type for zero value!");
+}
+
+SMTExprRef SMTConstraintManager::getSymExpr(SymbolRef Sym, QualType *RetTy,
+                                            bool *hasComparison) const {
+  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
+    if (RetTy)
+      *RetTy = Sym->getType();
+
+    return getDataExpr(SD->getSymbolID(), Sym->getType());
+  }
+
+  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
+    if (RetTy)
+      *RetTy = Sym->getType();
+
+    QualType FromTy;
+    SMTExprRef Exp = getSymExpr(SC->getOperand(), &FromTy, hasComparison);
+    // Casting an expression with a comparison invalidates it. Note that this
+    // must occur after the recursive call above.
+    // e.g. (signed char) (x > 0)
+    if (hasComparison)
+      *hasComparison = false;
+    return getCastExpr(Exp, FromTy, Sym->getType());
+  }
+
+  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+    SMTExprRef Exp = getSymBinExpr(BSE, hasComparison, RetTy);
+    // Set the hasComparison parameter, in post-order traversal order.
+    if (hasComparison)
+      *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
+    return Exp;
+  }
+
+  llvm_unreachable("Unsupported SymbolRef type!");
+}
+
+SMTExprRef SMTConstraintManager::getDataExpr(const SymbolID ID,
+                                             QualType Ty) const {
+  ASTContext &Ctx = getBasicVals().getContext();
+  return Solver->fromData(ID, Ty, Ctx.getTypeSize(Ty));
+}
+
+SMTExprRef SMTConstraintManager::getCastExpr(const SMTExprRef &Exp,
+                                             QualType FromTy,
+                                             QualType ToTy) const {
+  ASTContext &Ctx = getBasicVals().getContext();
+  return Solver->fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
+                          Ctx.getTypeSize(FromTy));
+}
+
+SMTExprRef SMTConstraintManager::getSymBinExpr(const BinarySymExpr *BSE,
+                                               bool *hasComparison,
+                                               QualType *RetTy) const {
+  QualType LTy, RTy;
+  BinaryOperator::Opcode Op = BSE->getOpcode();
+
+  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
+    SMTExprRef LHS = getSymExpr(SIE->getLHS(), &LTy, hasComparison);
+    llvm::APSInt NewRInt;
+    std::tie(NewRInt, RTy) = fixAPSInt(SIE->getRHS());
+    SMTExprRef RHS = Solver->fromAPSInt(NewRInt);
+    return getBinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
+  }
+
+  if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
+    llvm::APSInt NewLInt;
+    std::tie(NewLInt, LTy) = fixAPSInt(ISE->getLHS());
+    SMTExprRef LHS = Solver->fromAPSInt(NewLInt);
+    SMTExprRef RHS = getSymExpr(ISE->getRHS(), &RTy, hasComparison);
+    return getBinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
+  }
+
+  if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
+    SMTExprRef LHS = getSymExpr(SSM->getLHS(), &LTy, hasComparison);
+    SMTExprRef RHS = getSymExpr(SSM->getRHS(), &RTy, hasComparison);
+    return getBinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
+  }
+
+  llvm_unreachable("Unsupported BinarySymExpr type!");
+}
+
+SMTExprRef SMTConstraintManager::getBinExpr(const SMTExprRef &LHS, QualType LTy,
+                                            BinaryOperator::Opcode Op,
+                                            const SMTExprRef &RHS, QualType RTy,
+                                            QualType *RetTy) const {
+  SMTExprRef NewLHS = LHS;
+  SMTExprRef NewRHS = RHS;
+  doTypeConversion(NewLHS, NewRHS, LTy, RTy);
+
+  // Update the return type parameter if the output type has changed.
+  if (RetTy) {
+    // A boolean result can be represented as an integer type in C/C++, but at
+    // this point we only care about the Z3 type. Set it as a boolean type to
+    // avoid subsequent Z3 errors.
+    if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) {
+      ASTContext &Ctx = getBasicVals().getContext();
+      *RetTy = Ctx.BoolTy;
+    } else {
+      *RetTy = LTy;
+    }
+
+    // If the two operands are pointers and the operation is a subtraction, the
+    // result is of type ptrdiff_t, which is signed
+    if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) {
+      *RetTy = getBasicVals().getContext().getPointerDiffType();
+    }
+  }
+
+  return LTy->isRealFloatingType()
+             ? Solver->fromFloatBinOp(NewLHS, Op, NewRHS)
+             : Solver->fromBinOp(NewLHS, Op, NewRHS,
+                                 LTy->isSignedIntegerOrEnumerationType());
+}
+
+SMTExprRef SMTConstraintManager::getRangeExpr(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(From);
+  SMTExprRef FromExp = Solver->fromAPSInt(NewFromInt);
+
+  // Convert symbol
+  QualType SymTy;
+  SMTExprRef Exp = getExpr(Sym, &SymTy);
+
+  // Construct single (in)equality
+  if (From == To)
+    return getBinExpr(Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp, FromTy,
+                      /*RetTy=*/nullptr);
+
+  QualType ToTy;
+  llvm::APSInt NewToInt;
+  std::tie(NewToInt, ToTy) = fixAPSInt(To);
+  SMTExprRef ToExp = Solver->fromAPSInt(NewToInt);
+  assert(FromTy == ToTy && "Range values have different types!");
+
+  // Construct two (in)equalities, and a logical and/or
+  SMTExprRef LHS = getBinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
+                              FromTy, /*RetTy=*/nullptr);
+  SMTExprRef RHS = getBinExpr(Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
+                              /*RetTy=*/nullptr);
+
+  return Solver->fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+                           SymTy->isSignedIntegerOrEnumerationType());
+}
+
+//===------------------------------------------------------------------===//
+// Helper functions.
+//===------------------------------------------------------------------===//
+
+QualType SMTConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
+  ASTContext &Ctx = getBasicVals().getContext();
+  return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
+}
+
+std::pair<llvm::APSInt, QualType>
+SMTConstraintManager::fixAPSInt(const llvm::APSInt &Int) const {
+  llvm::APSInt NewInt;
+
+  // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
+  // but the former is not available in Clang. Instead, extend the APSInt
+  // directly.
+  if (Int.getBitWidth() == 1 && getAPSIntType(Int).isNull()) {
+    ASTContext &Ctx = getBasicVals().getContext();
+    NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
+  } else
+    NewInt = Int;
+
+  return std::make_pair(NewInt, getAPSIntType(NewInt));
+}
+
+void SMTConstraintManager::doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS,
+                                            QualType &LTy,
+                                            QualType &RTy) const {
+  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
+
+  ASTContext &Ctx = getBasicVals().getContext();
+
+  // Perform type conversion
+  if ((LTy->isIntegralOrEnumerationType() &&
+       RTy->isIntegralOrEnumerationType()) &&
+      (LTy->isArithmeticType() && RTy->isArithmeticType())) {
+    doIntTypeConversion<SMTExprRef, &SMTSolver::fromCast>(LHS, LTy, RHS, RTy);
+    return;
+  }
+
+  if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
+    doFloatTypeConversion<SMTExprRef, &SMTSolver::fromCast>(LHS, LTy, RHS, RTy);
+    return;
+  }
+
+  if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
+      (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
+      (LTy->isReferenceType() || RTy->isReferenceType())) {
+    // TODO: Refactor to Sema::FindCompositePointerType(), and
+    // Sema::CheckCompareOperands().
+
+    uint64_t LBitWidth = Ctx.getTypeSize(LTy);
+    uint64_t RBitWidth = Ctx.getTypeSize(RTy);
+
+    // Cast the non-pointer type to the pointer type.
+    // TODO: Be more strict about this.
+    if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
+        (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
+        (LTy->isReferenceType() ^ RTy->isReferenceType())) {
+      if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
+          LTy->isReferenceType()) {
+        LHS = Solver->fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
+        LTy = RTy;
+      } else {
+        RHS = Solver->fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
+        RTy = LTy;
+      }
+    }
+
+    // Cast the void pointer type to the non-void pointer type.
+    // For void types, this assumes that the casted value is equal to the value
+    // of the original pointer, and does not account for alignment requirements.
+    if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
+      assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
+             "Pointer types have different bitwidths!");
+      if (RTy->isVoidPointerType())
+        RTy = LTy;
+      else
+        LTy = RTy;
+    }
+
+    if (LTy == RTy)
+      return;
+  }
+
+  // Fallback: for the solver, assume that these types don't really matter
+  if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
+      (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
+    LTy = RTy;
+    return;
+  }
+
+  // TODO: Refine behavior for invalid type casts
+}

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

 
 class Z3Solver : public SMTSolver {
   friend class Z3ConstraintManager;
 
   Z3Context Context;
 
   Z3_solver Solver;
 
+public:
   Z3Solver() : SMTSolver(), Solver(Z3_mk_simple_solver(Context.Context)) {
     Z3_solver_inc_ref(Context.Context, Solver);
   }
 
-public:
   /// 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)
public:
   void reset() const 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 {
-  mutable Z3Solver Solver;
+  SMTSolverRef Solver = std::make_shared<Z3Solver>();
 
 public:
   Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
-      : SMTConstraintManager(SE, SB) {}
-
-  //===------------------------------------------------------------------===//
-  // Implementation for Refutation.
-  //===------------------------------------------------------------------===//
-
-  void addRangeConstraints(clang::ento::ConstraintRangeTy CR) override;
-
-  ConditionTruthVal isModelFeasible() override;
-
-  LLVM_DUMP_METHOD void dump() const override;
-
-  //===------------------------------------------------------------------===//
-  // Implementation for interface from ConstraintManager.
-  //===------------------------------------------------------------------===//
-
-  bool canReasonAbout(SVal X) const override;
-
-  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
-
-  const llvm::APSInt *getSymVal(ProgramStateRef State,
-                                SymbolRef Sym) const override;
-
-  ProgramStateRef removeDeadBindings(ProgramStateRef St,
-                                     SymbolReaper &SymReaper) override;
-
-  void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
-             const char *sep) override;
-
-  //===------------------------------------------------------------------===//
-  // Implementation for interface from SimpleConstraintManager.
-  //===------------------------------------------------------------------===//
-
-  ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
-                            bool Assumption) override;
-
-  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
-                                          const llvm::APSInt &From,
-                                          const llvm::APSInt &To,
-                                          bool InRange) override;
-
-  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
-                                       bool Assumption) override;
-
-private:
-  //===------------------------------------------------------------------===//
-  // Internal implementation.
-  //===------------------------------------------------------------------===//
-
-  /// Given a program state, construct the logical conjunction and add it to
-  /// the solver
-  void addStateConstraints(ProgramStateRef State) const;
-
-  // Check whether a new model is satisfiable, and update the program state.
-  ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym,
-                               const SMTExprRef &Exp);
-
-  // Generate and check a Z3 model, using the given constraint.
-  ConditionTruthVal checkZ3Model(ProgramStateRef State,
-                                 const SMTExprRef &Exp) const;
-
-  // Generate a Z3Expr 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.
-  SMTExprRef getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,
-                       bool *hasComparison = nullptr) const;
-
-  // Generate a Z3Expr that takes the logical not of an expression.
-  SMTExprRef getZ3NotExpr(const SMTExprRef &Exp) const;
-
-  // Generate a Z3Expr that compares the expression to zero.
-  SMTExprRef getZ3ZeroExpr(const SMTExprRef &Exp, QualType RetTy,
-                           bool Assumption) const;
-
-  // Recursive implementation to unpack and generate symbolic expression.
-  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
-  SMTExprRef getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
-                          bool *hasComparison) const;
-
-  // Wrapper to generate Z3Expr from SymbolData.
-  SMTExprRef getZ3DataExpr(const SymbolID ID, QualType Ty) const;
-
-  // Wrapper to generate Z3Expr from SymbolCast.
-  SMTExprRef getZ3CastExpr(const SMTExprRef &Exp, QualType FromTy,
-                           QualType Ty) const;
-
-  // Wrapper to generate Z3Expr from BinarySymExpr.
-  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
-  SMTExprRef getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
-                             QualType *RetTy) const;
-
-  // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
-  // Sets the RetTy parameter. See getZ3Expr().
-  SMTExprRef getZ3BinExpr(const SMTExprRef &LHS, QualType LTy,
-                          BinaryOperator::Opcode Op, const SMTExprRef &RHS,
-                          QualType RTy, QualType *RetTy) const;
-
-  // Wrapper to generate Z3Expr from a range. If From == To, an equality will
-  // be created instead.
-  SMTExprRef getZ3RangeExpr(SymbolRef Sym, const llvm::APSInt &From,
-                            const llvm::APSInt &To, bool InRange);
-
-  //===------------------------------------------------------------------===//
-  // Helper functions.
-  //===------------------------------------------------------------------===//
-
-  // Recover the QualType of an APSInt.
-  // TODO: Refactor to put elsewhere
-  QualType getAPSIntType(const llvm::APSInt &Int) const;
-
-  // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
-  std::pair<llvm::APSInt, QualType> fixAPSInt(const llvm::APSInt &Int) const;
-
-  // Perform implicit type conversion on binary symbolic expressions.
-  // May modify all input parameters.
-  // TODO: Refactor to use built-in conversion functions
-  void doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS, QualType &LTy,
-                        QualType &RTy) const;
-
-  // Perform implicit integer type conversion.
-  // May modify all input parameters.
-  // TODO: Refactor to use Sema::handleIntegerConversion()
-  template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t,
-                                               QualType, uint64_t)>
-  void doIntTypeConversion(T &LHS, QualType &LTy, T &RHS, QualType &RTy) const;
-
-  // Perform implicit floating-point type conversion.
-  // May modify all input parameters.
-  // TODO: Refactor to use Sema::handleFloatConversion()
-  template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t,
-                                               QualType, uint64_t)>
-  void doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
-                             QualType &RTy) const;
-}; // end class Z3ConstraintManager
-
-} // end anonymous namespace
+      : SMTConstraintManager(SE, SB, Solver) {}
 
-void Z3ConstraintManager::addStateConstraints(ProgramStateRef State) const {
+  void addStateConstraints(ProgramStateRef State) const override {
     // TODO: Don't add all the constraints, only the relevant ones
     ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
     ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
 
     // Construct the logical AND of all the constraints
     if (I != IE) {
       std::vector<SMTExprRef> ASTs;
 
-    while (I != IE)
-      ASTs.push_back(Solver.newExprRef(Z3Expr(I++->second)));
-
-    Solver.addConstraint(Solver.fromNBinOp(BO_LAnd, ASTs));
-  }
+      SMTExprRef Constraint = Solver->newExprRef(I++->second);
+      while (I != IE) {
+        Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));
       }
 
-ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State,
-                                               SymbolRef Sym, bool Assumption) {
-  QualType RetTy;
-  bool hasComparison;
-
-  SMTExprRef Exp = getZ3Expr(Sym, &RetTy, &hasComparison);
-  // Create zero comparison for implicit boolean cast, with reversed assumption
-  if (!hasComparison && !RetTy->isBooleanType())
-    return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption));
-
-  return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));
+      Solver->addConstraint(Constraint);
     }
-
-ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
-    ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-    const llvm::APSInt &To, bool InRange) {
-  return assumeZ3Expr(State, Sym, getZ3RangeExpr(Sym, From, To, InRange));
   }
 
-ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
-                                                          SymbolRef Sym,
-                                                          bool Assumption) {
-  // Skip anything that is unsupported
-  return State;
-}
-
-bool Z3ConstraintManager::canReasonAbout(SVal X) const {
+  bool canReasonAbout(SVal X) const override {
     const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
 
     Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
     if (!SymVal)
       return true;
 
     const SymExpr *Sym = SymVal->getSymbol();
     QualType Ty = Sym->getType();
 
     // Complex types are not modeled
     if (Ty->isComplexType() || Ty->isComplexIntegerType())
       return false;
 
     // Non-IEEE 754 floating-point types are not modeled
     if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
          (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
           &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
       return false;
 
     if (isa<SymbolData>(Sym))
       return true;
 
     SValBuilder &SVB = getSValBuilder();
 
     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
       return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
 
     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
         return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
 
       if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
         return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
 
       if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
         return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
                canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
     }
 
     llvm_unreachable("Unsupported expression to reason about!");
   }
 
-ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State,
-                                                 SymbolRef Sym) {
-  QualType RetTy;
-  // The expression may be casted, so we cannot call getZ3DataExpr() directly
-  SMTExprRef VarExp = getZ3Expr(Sym, &RetTy);
-  SMTExprRef Exp = getZ3ZeroExpr(VarExp, RetTy, true);
-
-  // Negate the constraint
-  SMTExprRef NotExp = getZ3ZeroExpr(VarExp, RetTy, false);
-
-  Solver.reset();
-  addStateConstraints(State);
-
-  Solver.push();
-  Solver.addConstraint(Exp);
-  ConditionTruthVal isSat = Solver.check();
-
-  Solver.pop();
-  Solver.addConstraint(NotExp);
-  ConditionTruthVal isNotSat = Solver.check();
-
-  // Zero is the only possible solution
-  if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
-    return true;
-
-  // Zero is not a solution
-  if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
-    return false;
-
-  // Zero may be a solution
-  return ConditionTruthVal();
-}
-
-const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
-                                                   SymbolRef Sym) const {
-  BasicValueFactory &BVF = getBasicVals();
-  ASTContext &Ctx = BVF.getContext();
-
-  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
-    QualType Ty = Sym->getType();
-    assert(!Ty->isRealFloatingType());
-    llvm::APSInt Value(Ctx.getTypeSize(Ty),
-                       !Ty->isSignedIntegerOrEnumerationType());
-
-    SMTExprRef Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
-
-    Solver.reset();
-    addStateConstraints(State);
-
-    // Constraints are unsatisfiable
-    ConditionTruthVal isSat = Solver.check();
-    if (!isSat.isConstrainedTrue())
-      return nullptr;
-
-    // Model does not assign interpretation
-    if (!Solver.getInterpretation(Exp, Value))
-      return nullptr;
-
-    // A value has been obtained, check if it is the only value
-    SMTExprRef NotExp = Solver.fromBinOp(
-        Exp, BO_NE,
-        Ty->isBooleanType() ? Solver.fromBoolean(Value.getBoolValue())
-                            : Solver.fromAPSInt(Value),
-        false);
-
-    Solver.addConstraint(NotExp);
-
-    ConditionTruthVal isNotSat = Solver.check();
-    if (isNotSat.isConstrainedTrue())
-      return nullptr;
-
-    // This is the only solution, store it
-    return &BVF.getValue(Value);
-  } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
-    SymbolRef CastSym = SC->getOperand();
-    QualType CastTy = SC->getType();
-    // Skip the void type
-    if (CastTy->isVoidType())
-      return nullptr;
-
-    const llvm::APSInt *Value;
-    if (!(Value = getSymVal(State, CastSym)))
-      return nullptr;
-    return &BVF.Convert(SC->getType(), *Value);
-  } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
-    const llvm::APSInt *LHS, *RHS;
-    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
-      LHS = getSymVal(State, SIE->getLHS());
-      RHS = &SIE->getRHS();
-    } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
-      LHS = &ISE->getLHS();
-      RHS = getSymVal(State, ISE->getRHS());
-    } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
-      // Early termination to avoid expensive call
-      LHS = getSymVal(State, SSM->getLHS());
-      RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
-    } else {
-      llvm_unreachable("Unsupported binary expression to get symbol value!");
-    }
-
-    if (!LHS || !RHS)
-      return nullptr;
-
-    llvm::APSInt ConvertedLHS, ConvertedRHS;
-    QualType LTy, RTy;
-    std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS);
-    std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS);
-    doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
-        ConvertedLHS, LTy, ConvertedRHS, RTy);
-    return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
-  }
-
-  llvm_unreachable("Unsupported expression to get symbol value!");
-}
-
-ProgramStateRef
-Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
-                                        SymbolReaper &SymReaper) {
+  ProgramStateRef removeDeadBindings(ProgramStateRef State,
+                                     SymbolReaper &SymReaper) override {
     ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
     ConstraintZ3Ty::Factory &CZFactory = State->get_context<ConstraintZ3>();
 
     for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
       if (SymReaper.maybeDead(I->first))
         CZ = CZFactory.remove(CZ, *I);
     }
 
     return State->set<ConstraintZ3>(CZ);
   }
 
-void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
-  Solver.reset();
-
-  for (const auto &I : CR) {
-    SymbolRef Sym = I.first;
-
-    SMTExprRef Constraints = Solver.fromBoolean(false);
-    for (const auto &Range : I.second) {
-      SMTExprRef SymRange =
-          getZ3RangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true);
-
-      // FIXME: the last argument (isSigned) is not used when generating the
-      // or expression, as both arguments are booleans
-      Constraints =
-          Solver.fromBinOp(Constraints, BO_LOr, SymRange, /*IsSigned=*/true);
-    }
-    Solver.addConstraint(Constraints);
-  }
-}
-
-clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() {
-  return Solver.check();
-}
-
-LLVM_DUMP_METHOD void Z3ConstraintManager::dump() const { Solver.dump(); }
-
-//===------------------------------------------------------------------===//
-// Internal implementation.
-//===------------------------------------------------------------------===//
-
-ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State,
-                                                  SymbolRef Sym,
-                                                  const SMTExprRef &Exp) {
+  ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
+                             const SMTExprRef &Exp) override {
     // Check the model, avoid simplifying AST to save time
-  if (checkZ3Model(State, Exp).isConstrainedTrue())
+    if (checkModel(State, Exp).isConstrainedTrue())
       return State->add<ConstraintZ3>(std::make_pair(Sym, toZ3Expr(*Exp)));
 
     return nullptr;
   }
 
-ConditionTruthVal
-Z3ConstraintManager::checkZ3Model(ProgramStateRef State,
-                                  const SMTExprRef &Exp) const {
-  Solver.reset();
-  Solver.addConstraint(Exp);
-  addStateConstraints(State);
-  return Solver.check();
-}
-
-SMTExprRef Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy,
-                                          bool *hasComparison) const {
-  if (hasComparison) {
-    *hasComparison = false;
-  }
-
-  return getZ3SymExpr(Sym, RetTy, hasComparison);
-}
-
-SMTExprRef Z3ConstraintManager::getZ3NotExpr(const SMTExprRef &Exp) const {
-  return Solver.fromUnOp(UO_LNot, Exp);
-}
-
-SMTExprRef Z3ConstraintManager::getZ3ZeroExpr(const SMTExprRef &Exp,
-                                              QualType Ty,
-                                              bool Assumption) const {
-  ASTContext &Ctx = getBasicVals().getContext();
-  if (Ty->isRealFloatingType()) {
-    llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
-    return Solver.fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
-                                 Solver.fromAPFloat(Zero));
-  } else if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() ||
-             Ty->isBlockPointerType() || Ty->isReferenceType()) {
-    bool isSigned = Ty->isSignedIntegerOrEnumerationType();
-    // Skip explicit comparison for boolean types
-    if (Ty->isBooleanType())
-      return Assumption ? getZ3NotExpr(Exp) : Exp;
-    return Solver.fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
-                            Solver.fromInt("0", Ctx.getTypeSize(Ty)), isSigned);
-  }
-
-  llvm_unreachable("Unsupported type for zero value!");
-}
-
-SMTExprRef Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
-                                             bool *hasComparison) const {
-  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
-    if (RetTy)
-      *RetTy = Sym->getType();
-
-    return getZ3DataExpr(SD->getSymbolID(), Sym->getType());
-  } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
-    if (RetTy)
-      *RetTy = Sym->getType();
-
-    QualType FromTy;
-    SMTExprRef Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison);
-    // Casting an expression with a comparison invalidates it. Note that this
-    // must occur after the recursive call above.
-    // e.g. (signed char) (x > 0)
-    if (hasComparison)
-      *hasComparison = false;
-    return getZ3CastExpr(Exp, FromTy, Sym->getType());
-  } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
-    SMTExprRef Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy);
-    // Set the hasComparison parameter, in post-order traversal order.
-    if (hasComparison)
-      *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
-    return Exp;
-  }
-
-  llvm_unreachable("Unsupported SymbolRef type!");
-}
-
-SMTExprRef Z3ConstraintManager::getZ3DataExpr(const SymbolID ID,
-                                              QualType Ty) const {
-  ASTContext &Ctx = getBasicVals().getContext();
-  return Solver.fromData(ID, Ty, Ctx.getTypeSize(Ty));
-}
-
-SMTExprRef Z3ConstraintManager::getZ3CastExpr(const SMTExprRef &Exp,
-                                              QualType FromTy,
-                                              QualType ToTy) const {
-  ASTContext &Ctx = getBasicVals().getContext();
-  return Solver.fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
-                         Ctx.getTypeSize(FromTy));
-}
-
-SMTExprRef Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
-                                                bool *hasComparison,
-                                                QualType *RetTy) const {
-  QualType LTy, RTy;
-  BinaryOperator::Opcode Op = BSE->getOpcode();
-
-  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
-    SMTExprRef LHS = getZ3SymExpr(SIE->getLHS(), &LTy, hasComparison);
-    llvm::APSInt NewRInt;
-    std::tie(NewRInt, RTy) = fixAPSInt(SIE->getRHS());
-    SMTExprRef RHS = Solver.fromAPSInt(NewRInt);
-    return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
-  } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
-    llvm::APSInt NewLInt;
-    std::tie(NewLInt, LTy) = fixAPSInt(ISE->getLHS());
-    SMTExprRef LHS = Solver.fromAPSInt(NewLInt);
-    SMTExprRef RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
-    return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
-  } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
-    SMTExprRef LHS = getZ3SymExpr(SSM->getLHS(), &LTy, hasComparison);
-    SMTExprRef RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
-    return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
-  } else {
-    llvm_unreachable("Unsupported BinarySymExpr type!");
-  }
-}
-
-SMTExprRef Z3ConstraintManager::getZ3BinExpr(
-    const SMTExprRef &LHS, QualType LTy, BinaryOperator::Opcode Op,
-    const SMTExprRef &RHS, QualType RTy, QualType *RetTy) const {
-  SMTExprRef NewLHS = LHS;
-  SMTExprRef NewRHS = RHS;
-  doTypeConversion(NewLHS, NewRHS, LTy, RTy);
-  // Update the return type parameter if the output type has changed.
-  if (RetTy) {
-    // A boolean result can be represented as an integer type in C/C++, but at
-    // this point we only care about the Z3 type. Set it as a boolean type to
-    // avoid subsequent Z3 errors.
-    if (BinaryOperator::isComparisonOp(Op) || BinaryOperator::isLogicalOp(Op)) {
-      ASTContext &Ctx = getBasicVals().getContext();
-      *RetTy = Ctx.BoolTy;
-    } else {
-      *RetTy = LTy;
-    }
-
-    // If the two operands are pointers and the operation is a subtraction, the
-    // result is of type ptrdiff_t, which is signed
-    if (LTy->isAnyPointerType() && RTy->isAnyPointerType() && Op == BO_Sub) {
-      *RetTy = getBasicVals().getContext().getPointerDiffType();
-    }
-  }
-
-  return LTy->isRealFloatingType()
-             ? Solver.fromFloatBinOp(NewLHS, Op, NewRHS)
-             : Solver.fromBinOp(NewLHS, Op, NewRHS,
-                                LTy->isSignedIntegerOrEnumerationType());
-}
-
-SMTExprRef Z3ConstraintManager::getZ3RangeExpr(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(From);
-  SMTExprRef FromExp = Solver.fromAPSInt(NewFromInt);
-
-  // Convert symbol
-  QualType SymTy;
-  SMTExprRef Exp = getZ3Expr(Sym, &SymTy);
-
-  // Construct single (in)equality
-  if (From == To)
-    return getZ3BinExpr(Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp, FromTy,
-                        /*RetTy=*/nullptr);
-
-  QualType ToTy;
-  llvm::APSInt NewToInt;
-  std::tie(NewToInt, ToTy) = fixAPSInt(To);
-  SMTExprRef ToExp = Solver.fromAPSInt(NewToInt);
-  assert(FromTy == ToTy && "Range values have different types!");
-
-  // Construct two (in)equalities, and a logical and/or
-  SMTExprRef LHS = getZ3BinExpr(Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
-                                FromTy, /*RetTy=*/nullptr);
-  SMTExprRef RHS =
-      getZ3BinExpr(Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
-                   /*RetTy=*/nullptr);
-
-  return Solver.fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
-                          SymTy->isSignedIntegerOrEnumerationType());
-}
-
-//===------------------------------------------------------------------===//
-// Helper functions.
-//===------------------------------------------------------------------===//
-
-QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
-  ASTContext &Ctx = getBasicVals().getContext();
-  return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
-}
-
-std::pair<llvm::APSInt, QualType>
-Z3ConstraintManager::fixAPSInt(const llvm::APSInt &Int) const {
-  llvm::APSInt NewInt;
-
-  // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
-  // but the former is not available in Clang. Instead, extend the APSInt
-  // directly.
-  if (Int.getBitWidth() == 1 && getAPSIntType(Int).isNull()) {
-    ASTContext &Ctx = getBasicVals().getContext();
-    NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
-  } else
-    NewInt = Int;
-
-  return std::make_pair(NewInt, getAPSIntType(NewInt));
-}
-
-void Z3ConstraintManager::doTypeConversion(SMTExprRef &LHS, SMTExprRef &RHS,
-                                           QualType &LTy, QualType &RTy) const {
-  ASTContext &Ctx = getBasicVals().getContext();
-
-  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
-  // Perform type conversion
-  if (LTy->isIntegralOrEnumerationType() &&
-      RTy->isIntegralOrEnumerationType()) {
-    if (LTy->isArithmeticType() && RTy->isArithmeticType()) {
-      doIntTypeConversion<SMTExprRef, &Z3Solver::fromCast>(LHS, LTy, RHS, RTy);
-      return;
-    }
-  } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
-    doFloatTypeConversion<SMTExprRef, &Z3Solver::fromCast>(LHS, LTy, RHS, RTy);
-    return;
-  } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
-             (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
-             (LTy->isReferenceType() || RTy->isReferenceType())) {
-    // TODO: Refactor to Sema::FindCompositePointerType(), and
-    // Sema::CheckCompareOperands().
-
-    uint64_t LBitWidth = Ctx.getTypeSize(LTy);
-    uint64_t RBitWidth = Ctx.getTypeSize(RTy);
-
-    // Cast the non-pointer type to the pointer type.
-    // TODO: Be more strict about this.
-    if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
-        (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
-        (LTy->isReferenceType() ^ RTy->isReferenceType())) {
-      if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
-          LTy->isReferenceType()) {
-        LHS = Solver.fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
-        LTy = RTy;
-      } else {
-        RHS = Solver.fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
-        RTy = LTy;
-      }
-    }
-
-    // Cast the void pointer type to the non-void pointer type.
-    // For void types, this assumes that the casted value is equal to the value
-    // of the original pointer, and does not account for alignment requirements.
-    if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
-      assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
-             "Pointer types have different bitwidths!");
-      if (RTy->isVoidPointerType())
-        RTy = LTy;
-      else
-        LTy = RTy;
-    }
-
-    if (LTy == RTy)
-      return;
-  }
-
-  // Fallback: for the solver, assume that these types don't really matter
-  if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
-      (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType())) {
-    LTy = RTy;
-    return;
-  }
-
-  // TODO: Refine behavior for invalid type casts
-}
-
-template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t,
-                                             QualType, uint64_t)>
-void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType &LTy, T &RHS,
-                                              QualType &RTy) const {
-  ASTContext &Ctx = getBasicVals().getContext();
-  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.
-  // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
-  if (LTy->isPromotableIntegerType()) {
-    QualType NewTy = Ctx.getPromotedIntegerType(LTy);
-    uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
-    LHS = (Solver.*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);
-    LTy = NewTy;
-    LBitWidth = NewBitWidth;
-  }
-  if (RTy->isPromotableIntegerType()) {
-    QualType NewTy = Ctx.getPromotedIntegerType(RTy);
-    uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
-    RHS = (Solver.*doCast)(RHS, NewTy, NewBitWidth, RTy, RBitWidth);
-    RTy = NewTy;
-    RBitWidth = NewBitWidth;
-  }
-
-  if (LTy == RTy)
-    return;
-
-  // Perform integer type conversion
-  // Note: Safe to skip updating bitwidth because this must terminate
-  bool isLSignedTy = LTy->isSignedIntegerOrEnumerationType();
-  bool isRSignedTy = RTy->isSignedIntegerOrEnumerationType();
-
-  int order = Ctx.getIntegerTypeOrder(LTy, RTy);
-  if (isLSignedTy == isRSignedTy) {
-    // Same signedness; use the higher-ranked type
-    if (order == 1) {
-      RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
-      RTy = LTy;
-    } else {
-      LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
-      LTy = RTy;
-    }
-  } else if (order != (isLSignedTy ? 1 : -1)) {
-    // The unsigned type has greater than or equal rank to the
-    // signed type, so use the unsigned type
-    if (isRSignedTy) {
-      RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
-      RTy = LTy;
-    } else {
-      LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
-      LTy = RTy;
-    }
-  } else if (LBitWidth != RBitWidth) {
-    // The two types are different widths; if we are here, that
-    // means the signed type is larger than the unsigned type, so
-    // use the signed type.
-    if (isLSignedTy) {
-      RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
-      RTy = LTy;
-    } else {
-      LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
-      LTy = RTy;
-    }
-  } else {
-    // The signed type is higher-ranked than the unsigned type,
-    // but isn't actually any bigger (like unsigned int and long
-    // on most 32-bit systems).  Use the unsigned type corresponding
-    // to the signed type.
-    QualType NewTy = Ctx.getCorrespondingUnsignedType(isLSignedTy ? LTy : RTy);
-    RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
-    RTy = NewTy;
-    LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
-    LTy = NewTy;
-  }
-}
-
-template <typename T, T (SMTSolver::*doCast)(const T &, QualType, uint64_t,
-                                             QualType, uint64_t)>
-void Z3ConstraintManager::doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
-                                                QualType &RTy) const {
-  ASTContext &Ctx = getBasicVals().getContext();
-
-  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
-  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
-
-  // Perform float-point type promotion
-  if (!LTy->isRealFloatingType()) {
-    LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
-    LTy = RTy;
-    LBitWidth = RBitWidth;
-  }
-  if (!RTy->isRealFloatingType()) {
-    RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
-    RTy = LTy;
-    RBitWidth = LBitWidth;
-  }
-
-  if (LTy == RTy)
-    return;
-
-  // If we have two real floating types, convert the smaller operand to the
-  // bigger result
-  // Note: Safe to skip updating bitwidth because this must terminate
-  int order = Ctx.getFloatingTypeOrder(LTy, RTy);
-  if (order > 0) {
-    RHS = (Solver.*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
-    RTy = LTy;
-  } else if (order == 0) {
-    LHS = (Solver.*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
-    LTy = RTy;
-  } else {
-    llvm_unreachable("Unsupported floating-point type cast!");
-  }
-}
-
   //==------------------------------------------------------------------------==/
   // Pretty-printing.
   //==------------------------------------------------------------------------==/
 
-void Z3ConstraintManager::print(ProgramStateRef St, raw_ostream &OS,
-                                const char *nl, const char *sep) {
+  void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
+             const char *sep) override {
 
     ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
 
     OS << nl << sep << "Constraints:";
     for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E; ++I) {
       OS << nl << ' ' << I->first << " : ";
       I->second.print(OS);
     }
     OS << nl;
   }
+}; // end class Z3ConstraintManager
+
+} // end anonymous namespace
 
 #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_BUILD_Z3=ON",
                            false);
   return nullptr;
 #endif
 }