[analyzer] Moved all CSA code from the SMT API to a new header, `SMTConv.h`. NFC.

[mikhail.ramalho]

Summary

With this patch, the SMT backend is almost completely detached from the CSA.

Unfortunate consequence is that we missed the ConditionTruthVal from the CSA and had to use Optional<bool>.

The Z3 solver implementation is still in the same file as the Z3ConstraintManager, in lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp though, but except for that, the SMT API can be moved to anywhere in the codebase.

[george.karpenkov]

Makes sense. Another approach would have been to add state to SMTConv and have it reference the solver, but your way also works.

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"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 
 namespace clang {
 namespace ento {
 
 template <typename ConstraintSMT, typename SMTExprTy>
 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
   SMTSolverRef &Solver;
 
public:
 
   ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
                             bool Assumption) override {
     ASTContext &Ctx = getBasicVals().getContext();
 
     QualType RetTy;
     bool hasComparison;
 
-    SMTExprRef Exp = Solver->getExpr(Ctx, Sym, &RetTy, &hasComparison);
+    SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
 
     // Create zero comparison for implicit boolean cast, with reversed
     // assumption
     if (!hasComparison && !RetTy->isBooleanType())
-      return assumeExpr(State, Sym,
-                        Solver->getZeroExpr(Ctx, Exp, RetTy, !Assumption));
+      return assumeExpr(
+          State, Sym,
+          SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
 
     return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
   }
 
   ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
                                           const llvm::APSInt &From,
                                           const llvm::APSInt &To,
                                           bool InRange) override {
     ASTContext &Ctx = getBasicVals().getContext();
-    return assumeExpr(State, Sym,
-                      Solver->getRangeExpr(Ctx, Sym, From, To, InRange));
+    return assumeExpr(
+        State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
   }
 
   ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
                                        bool Assumption) override {
     // Skip anything that is unsupported
     return State;
   }
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//
 
   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override {
     ASTContext &Ctx = getBasicVals().getContext();
 
     QualType RetTy;
     // The expression may be casted, so we cannot call getZ3DataExpr() directly
-    SMTExprRef VarExp = Solver->getExpr(Ctx, Sym, &RetTy);
+    SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
     SMTExprRef Exp =
-        Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true);
+        SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
 
     // Negate the constraint
     SMTExprRef NotExp =
-        Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false);
+        SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
 
     Solver->reset();
     addStateConstraints(State);
 
     Solver->push();
     Solver->addConstraint(Exp);
-    ConditionTruthVal isSat = Solver->check();
+
+    Optional<bool> isSat = Solver->check();
+    if (!isSat.hasValue())
+      return ConditionTruthVal();
 
     Solver->pop();
     Solver->addConstraint(NotExp);
-    ConditionTruthVal isNotSat = Solver->check();
+
+    Optional<bool> isNotSat = Solver->check();
+    if (!isNotSat.hasValue())
+      return ConditionTruthVal();
 
     // Zero is the only possible solution
-    if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
+    if (isSat.getValue() && !isNotSat.getValue())
       return true;
 
     // Zero is not a solution
-    if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
+    if (!isSat.getValue() && isNotSat.getValue())
       return false;
 
     // Zero may be a solution
     return ConditionTruthVal();
   }
 
   const llvm::APSInt *getSymVal(ProgramStateRef State,
                                 SymbolRef Sym) const override {
     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 =
-          Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
+          SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
 
       Solver->reset();
       addStateConstraints(State);
 
       // Constraints are unsatisfiable
-      ConditionTruthVal isSat = Solver->check();
-      if (!isSat.isConstrainedTrue())
+      Optional<bool> isSat = Solver->check();
+      if (!isSat.hasValue() || !isSat.getValue())
         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,
+      SMTExprRef NotExp = SMTConv::fromBinOp(
+          Solver, Exp, BO_NE,
           Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue())
                               : Solver->fromAPSInt(Value),
           false);
 
       Solver->addConstraint(NotExp);
 
-      ConditionTruthVal isNotSat = Solver->check();
-      if (isNotSat.isConstrainedTrue())
+      Optional<bool> isNotSat = Solver->check();
+      if (!isSat.hasValue() || isNotSat.getValue())
         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();
if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
         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) = Solver->fixAPSInt(Ctx, *LHS);
-      std::tie(ConvertedRHS, RTy) = Solver->fixAPSInt(Ctx, *RHS);
-      Solver->doIntTypeConversion<llvm::APSInt, &SMTSolver::castAPSInt>(
-          Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
+      std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
+      std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
+      SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
+          Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
       return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
     }
 
     llvm_unreachable("Unsupported expression to get symbol value!");
   }
 
   ProgramStateRef removeDeadBindings(ProgramStateRef State,
                                      SymbolReaper &SymReaper) override {
protected:
   }
 
   // Generate and check a Z3 model, using the given constraint.
   ConditionTruthVal checkModel(ProgramStateRef State,
                                const SMTExprRef &Exp) const {
     Solver->reset();
     Solver->addConstraint(Exp);
     addStateConstraints(State);
-    return Solver->check();
-  }
 
+    Optional<bool> res = Solver->check();
+    if (!res.hasValue())
+      return ConditionTruthVal();
+
+    return ConditionTruthVal(res.getValue());
+  }
 }; // end class SMTConstraintManager
 
 } // namespace ento
 } // namespace clang
 
 #endif

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

+//== SMTConv.h --------------------------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines a set of functions to create SMT expressions
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONV_H
+
+#include "clang/AST/Expr.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.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,
+                                  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,
+                                    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,
+                                         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,
+                                      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,
+                                     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:
+      return Solver->mkBVMul(LHS, RHS);
+
+    case BO_Div:
+      return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS);
+
+    case BO_Rem:
+      return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS);
+
+      // Additive operators
+    case BO_Add:
+      return Solver->mkBVAdd(LHS, RHS);
+
+    case BO_Sub:
+      return Solver->mkBVSub(LHS, RHS);
+
+      // Bitwise shift operators
+    case BO_Shl:
+      return Solver->mkBVShl(LHS, RHS);
+
+    case BO_Shr:
+      return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS);
+
+      // Relational operators
+    case BO_LT:
+      return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS);
+
+    case BO_GT:
+      return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS);
+
+    case BO_LE:
+      return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS);
+
+    case BO_GE:
+      return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS);
+
+      // Equality operators
+    case BO_EQ:
+      return Solver->mkEqual(LHS, RHS);
+
+    case BO_NE:
+      return fromUnOp(Solver, UO_LNot,
+                      fromBinOp(Solver, LHS, BO_EQ, RHS, isSigned));
+
+      // Bitwise operators
+    case BO_And:
+      return Solver->mkBVAnd(LHS, RHS);
+
+    case BO_Xor:
+      return Solver->mkBVXor(LHS, RHS);
+
+    case BO_Or:
+      return Solver->mkBVOr(LHS, RHS);
+
+      // Logical operators
+    case BO_LAnd:
+      return Solver->mkAnd(LHS, RHS);
+
+    case BO_LOr:
+      return Solver->mkOr(LHS, RHS);
+
+    default:;
+    }
+    llvm_unreachable("Unimplemented opcode");
+  }
+
+  /// Construct an SMTExprRef from a special floating-point binary operator.
+  static inline SMTExprRef
+  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);
+
+      case llvm::APFloat::fcNaN:
+        return Solver->mkFPIsNaN(LHS);
+
+      case llvm::APFloat::fcNormal:
+        return Solver->mkFPIsNormal(LHS);
+
+      case llvm::APFloat::fcZero:
+        return Solver->mkFPIsZero(LHS);
+      }
+      break;
+
+    case BO_NE:
+      return fromFloatUnOp(Solver, UO_LNot,
+                           fromFloatSpecialBinOp(Solver, LHS, BO_EQ, RHS));
+
+    default:;
+    }
+
+    llvm_unreachable("Unimplemented opcode");
+  }
+
+  /// Construct an SMTExprRef from a floating-point binary operator.
+  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
+    case BO_Mul:
+      return Solver->mkFPMul(LHS, RHS);
+
+    case BO_Div:
+      return Solver->mkFPDiv(LHS, RHS);
+
+    case BO_Rem:
+      return Solver->mkFPRem(LHS, RHS);
+
+      // Additive operators
+    case BO_Add:
+      return Solver->mkFPAdd(LHS, RHS);
+
+    case BO_Sub:
+      return Solver->mkFPSub(LHS, RHS);
+
+      // Relational operators
+    case BO_LT:
+      return Solver->mkFPLt(LHS, RHS);
+
+    case BO_GT:
+      return Solver->mkFPGt(LHS, RHS);
+
+    case BO_LE:
+      return Solver->mkFPLe(LHS, RHS);
+
+    case BO_GE:
+      return Solver->mkFPGe(LHS, RHS);
+
+      // Equality operators
+    case BO_EQ:
+      return Solver->mkFPEqual(LHS, RHS);
+
+    case BO_NE:
+      return fromFloatUnOp(Solver, UO_LNot,
+                           fromFloatBinOp(Solver, LHS, BO_EQ, RHS));
+
+      // Logical operators
+    case BO_LAnd:
+    case BO_LOr:
+      return fromBinOp(Solver, LHS, Op, RHS, false);
+
+    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,
+                                    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->isBooleanType()) {
+        assert(ToBitWidth > 0 && "BitWidth must be positive!");
+        return Solver->mkIte(
+            Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth),
+            Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth));
+      }
+
+      if (ToBitWidth > FromBitWidth)
+        return FromTy->isSignedIntegerOrEnumerationType()
+                   ? Solver->mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
+                   : Solver->mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
+
+      if (ToBitWidth < FromBitWidth)
+        return Solver->mkBVExtract(ToBitWidth - 1, 0, Exp);
+
+      // Both are bitvectors with the same width, ignore the type cast
+      return Exp;
+    }
+
+    if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
+      if (ToBitWidth != FromBitWidth)
+        return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth));
+
+      return Exp;
+    }
+
+    if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
+      SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
+      return FromTy->isSignedIntegerOrEnumerationType()
+                 ? Solver->mkFPtoSBV(Exp, Sort)
+                 : Solver->mkFPtoUBV(Exp, Sort);
+    }
+
+    if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
+      return ToTy->isSignedIntegerOrEnumerationType()
+                 ? Solver->mkSBVtoFP(Exp, ToBitWidth)
+                 : Solver->mkUBVtoFP(Exp, ToBitWidth);
+
+    llvm_unreachable("Unsupported explicit type cast!");
+  }
+
+  // Callback function for doCast parameter on APSInt type.
+  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,
+                                    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,
+                                       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,
+                                      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);
+
+    // 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 SMT sorts. Set it as a boolean type
+      // to avoid subsequent SMT errors.
+      if (BinaryOperator::isComparisonOp(Op) ||
+          BinaryOperator::isLogicalOp(Op)) {
+        *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 = Ctx.getPointerDiffType();
+      }
+    }
+
+    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,
+                                         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);
+      llvm::APSInt NewRInt;
+      std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
+      SMTExprRef RHS = Solver->fromAPSInt(NewRInt);
+      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
+    }
+
+    if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
+      llvm::APSInt NewLInt;
+      std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
+      SMTExprRef LHS = Solver->fromAPSInt(NewLInt);
+      SMTExprRef RHS =
+          getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
+      return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
+    }
+
+    if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
+      SMTExprRef LHS =
+          getSymExpr(Solver, Ctx, SSM->getLHS(), &LTy, hasComparison);
+      SMTExprRef RHS =
+          getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
+      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,
+                                      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()));
+    }
+
+    if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
+      if (RetTy)
+        *RetTy = Sym->getType();
+
+      QualType FromTy;
+      SMTExprRef Exp =
+          getSymExpr(Solver, Ctx, 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(Solver, Ctx, Exp, FromTy, Sym->getType());
+    }
+
+    if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
+      SMTExprRef Exp = getSymBinExpr(Solver, Ctx, 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!");
+  }
+
+  // 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,
+                                   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,
+                                       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->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 ? fromUnOp(Solver, UO_LNot, Exp) : Exp;
+
+      return fromBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE,
+                       Solver->fromInt("0", Ctx.getTypeSize(Ty)), 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,
+                                        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->fromAPSInt(NewFromInt);
+
+    // Convert symbol
+    QualType SymTy;
+    SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
+
+    // Construct single (in)equality
+    if (From == To)
+      return getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE,
+                        FromExp, FromTy, /*RetTy=*/nullptr);
+
+    QualType ToTy;
+    llvm::APSInt NewToInt;
+    std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, 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(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
+                   FromTy, /*RetTy=*/nullptr);
+    SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
+                                InRange ? BO_LE : BO_GT, ToExp, ToTy,
+                                /*RetTy=*/nullptr);
+
+    return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+                     SymTy->isSignedIntegerOrEnumerationType());
+  }
+
+  // Recover the QualType of an APSInt.
+  // TODO: Refactor to put elsewhere
+  static inline QualType getAPSIntType(ASTContext &Ctx,
+                                       const llvm::APSInt &Int) {
+    return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
+  }
+
+  // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
+  static inline std::pair<llvm::APSInt, QualType>
+  fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int) {
+    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(Ctx, Int).isNull()) {
+      NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
+    } else
+      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,
+                                      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())) {
+      SMTConv::doIntTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, LHS, LTy,
+                                                          RHS, RTy);
+      return;
+    }
+
+    if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
+      SMTConv::doFloatTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, 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 = fromCast(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
+          LTy = RTy;
+        } else {
+          RHS = fromCast(Solver, 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
+  }
+
+  // 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,
+                                    uint64_t, QualType, uint64_t)>
+  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.
+    // 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 = (*doCast)(Solver, LHS, NewTy, NewBitWidth, LTy, LBitWidth);
+      LTy = NewTy;
+      LBitWidth = NewBitWidth;
+    }
+    if (RTy->isPromotableIntegerType()) {
+      QualType NewTy = Ctx.getPromotedIntegerType(RTy);
+      uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
+      RHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
+        RTy = LTy;
+      } else {
+        LHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
+        RTy = LTy;
+      } else {
+        LHS = (*doCast)(Solver, 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 = (doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
+        RTy = LTy;
+      } else {
+        LHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
+      RTy = NewTy;
+      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,
+                                    uint64_t, QualType, uint64_t)>
+  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;
+      LBitWidth = RBitWidth;
+    }
+    if (!RTy->isRealFloatingType()) {
+      RHS = (*doCast)(Solver, 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 = (*doCast)(Solver, RHS, LTy, LBitWidth, RTy, RBitWidth);
+      RTy = LTy;
+    } else if (order == 0) {
+      LHS = (*doCast)(Solver, LHS, RTy, RBitWidth, LTy, LBitWidth);
+      LTy = RTy;
+    } else {
+      llvm_unreachable("Unsupported floating-point type cast!");
+    }
+  }
+};
+} // namespace ento
+} // namespace clang
+
+#endif
 No newline at end of file

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

 //  This file defines a SMT generic Solver API, which will be the base class
 //  for every SMT solver specific class.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
 
-#include "clang/AST/Expr.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
+#include "llvm/ADT/APSInt.h"
 
 namespace clang {
 namespace ento {
 
 /// Generic base class for SMT Solvers
 ///
 /// This class is responsible for wrapping all sorts and expression generation,
 /// through the mk* methods. It also provides methods to create SMT expressions
case 64:
       return getFloat64Sort();
     case 128:
       return getFloat128Sort();
     default:;
     }
     llvm_unreachable("Unsupported floating-point bitwidth!");
   }
 
-  // Returns an appropriate sort, given a QualType and it's bit width.
-  SMTSortRef mkSort(const QualType &Ty, unsigned BitWidth) {
-    if (Ty->isBooleanType())
-      return getBoolSort();
-
-    if (Ty->isRealFloatingType())
-      return getFloatSort(BitWidth);
-
-    return getBitvectorSort(BitWidth);
-  }
-
-  /// Constructs an SMTExprRef from an unary operator.
-  SMTExprRef fromUnOp(const UnaryOperator::Opcode Op, const SMTExprRef &Exp) {
-    switch (Op) {
-    case UO_Minus:
-      return mkBVNeg(Exp);
-
-    case UO_Not:
-      return mkBVNot(Exp);
-
-    case UO_LNot:
-      return mkNot(Exp);
-
-    default:;
-    }
-    llvm_unreachable("Unimplemented opcode");
-  }
-
-  /// Constructs an SMTExprRef from a floating-point unary operator.
-  SMTExprRef fromFloatUnOp(const UnaryOperator::Opcode Op,
-                           const SMTExprRef &Exp) {
-    switch (Op) {
-    case UO_Minus:
-      return mkFPNeg(Exp);
-
-    case UO_LNot:
-      return fromUnOp(Op, Exp);
-
-    default:;
-    }
-    llvm_unreachable("Unimplemented opcode");
-  }
-
-  /// Construct an SMTExprRef from a n-ary binary operator.
-  SMTExprRef fromNBinOp(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) ? mkAnd(res, ASTs[i]) : mkOr(res, ASTs[i]);
-    return res;
-  }
-
-  /// Construct an SMTExprRef from a binary operator.
-  SMTExprRef fromBinOp(const SMTExprRef &LHS, const BinaryOperator::Opcode Op,
-                       const SMTExprRef &RHS, bool isSigned) {
-    assert(*getSort(LHS) == *getSort(RHS) && "AST's must have the same sort!");
-
-    switch (Op) {
-    // Multiplicative operators
-    case BO_Mul:
-      return mkBVMul(LHS, RHS);
-
-    case BO_Div:
-      return isSigned ? mkBVSDiv(LHS, RHS) : mkBVUDiv(LHS, RHS);
-
-    case BO_Rem:
-      return isSigned ? mkBVSRem(LHS, RHS) : mkBVURem(LHS, RHS);
-
-    // Additive operators
-    case BO_Add:
-      return mkBVAdd(LHS, RHS);
-
-    case BO_Sub:
-      return mkBVSub(LHS, RHS);
-
-    // Bitwise shift operators
-    case BO_Shl:
-      return mkBVShl(LHS, RHS);
-
-    case BO_Shr:
-      return isSigned ? mkBVAshr(LHS, RHS) : mkBVLshr(LHS, RHS);
-
-    // Relational operators
-    case BO_LT:
-      return isSigned ? mkBVSlt(LHS, RHS) : mkBVUlt(LHS, RHS);
-
-    case BO_GT:
-      return isSigned ? mkBVSgt(LHS, RHS) : mkBVUgt(LHS, RHS);
-
-    case BO_LE:
-      return isSigned ? mkBVSle(LHS, RHS) : mkBVUle(LHS, RHS);
-
-    case BO_GE:
-      return isSigned ? mkBVSge(LHS, RHS) : mkBVUge(LHS, RHS);
-
-    // Equality operators
-    case BO_EQ:
-      return mkEqual(LHS, RHS);
-
-    case BO_NE:
-      return fromUnOp(UO_LNot, fromBinOp(LHS, BO_EQ, RHS, isSigned));
-
-    // Bitwise operators
-    case BO_And:
-      return mkBVAnd(LHS, RHS);
-
-    case BO_Xor:
-      return mkBVXor(LHS, RHS);
-
-    case BO_Or:
-      return mkBVOr(LHS, RHS);
-
-    // Logical operators
-    case BO_LAnd:
-      return mkAnd(LHS, RHS);
-
-    case BO_LOr:
-      return mkOr(LHS, RHS);
-
-    default:;
-    }
-    llvm_unreachable("Unimplemented opcode");
-  }
-
-  /// Construct an SMTExprRef from a special floating-point binary operator.
-  SMTExprRef fromFloatSpecialBinOp(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 mkFPIsInfinite(LHS);
-
-      case llvm::APFloat::fcNaN:
-        return mkFPIsNaN(LHS);
-
-      case llvm::APFloat::fcNormal:
-        return mkFPIsNormal(LHS);
-
-      case llvm::APFloat::fcZero:
-        return mkFPIsZero(LHS);
-      }
-      break;
-
-    case BO_NE:
-      return fromFloatUnOp(UO_LNot, fromFloatSpecialBinOp(LHS, BO_EQ, RHS));
-
-    default:;
-    }
-
-    llvm_unreachable("Unimplemented opcode");
-  }
-
-  /// Construct an SMTExprRef from a floating-point binary operator.
-  SMTExprRef fromFloatBinOp(const SMTExprRef &LHS,
-                            const BinaryOperator::Opcode Op,
-                            const SMTExprRef &RHS) {
-    assert(*getSort(LHS) == *getSort(RHS) && "AST's must have the same sort!");
-
-    switch (Op) {
-    // Multiplicative operators
-    case BO_Mul:
-      return mkFPMul(LHS, RHS);
-
-    case BO_Div:
-      return mkFPDiv(LHS, RHS);
-
-    case BO_Rem:
-      return mkFPRem(LHS, RHS);
-
-      // Additive operators
-    case BO_Add:
-      return mkFPAdd(LHS, RHS);
-
-    case BO_Sub:
-      return mkFPSub(LHS, RHS);
-
-      // Relational operators
-    case BO_LT:
-      return mkFPLt(LHS, RHS);
-
-    case BO_GT:
-      return mkFPGt(LHS, RHS);
-
-    case BO_LE:
-      return mkFPLe(LHS, RHS);
-
-    case BO_GE:
-      return mkFPGe(LHS, RHS);
-
-      // Equality operators
-    case BO_EQ:
-      return mkFPEqual(LHS, RHS);
-
-    case BO_NE:
-      return fromFloatUnOp(UO_LNot, fromFloatBinOp(LHS, BO_EQ, RHS));
-
-      // Logical operators
-    case BO_LAnd:
-    case BO_LOr:
-      return fromBinOp(LHS, Op, RHS, false);
-
-    default:;
-    }
-
-    llvm_unreachable("Unimplemented opcode");
-  }
-
-  /// Construct an SMTExprRef from a QualType FromTy to a QualType ToTy, and
-  /// their bit widths.
-  SMTExprRef fromCast(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->isBooleanType()) {
-        assert(ToBitWidth > 0 && "BitWidth must be positive!");
-        return mkIte(Exp, mkBitvector(llvm::APSInt("1"), ToBitWidth),
-                     mkBitvector(llvm::APSInt("0"), ToBitWidth));
-      }
-
-      if (ToBitWidth > FromBitWidth)
-        return FromTy->isSignedIntegerOrEnumerationType()
-                   ? mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
-                   : mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
-
-      if (ToBitWidth < FromBitWidth)
-        return mkBVExtract(ToBitWidth - 1, 0, Exp);
-
-      // Both are bitvectors with the same width, ignore the type cast
-      return Exp;
-    }
-
-    if (FromTy->isRealFloatingType() && ToTy->isRealFloatingType()) {
-      if (ToBitWidth != FromBitWidth)
-        return mkFPtoFP(Exp, getFloatSort(ToBitWidth));
-
-      return Exp;
-    }
-
-    if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
-      SMTSortRef Sort = getFloatSort(ToBitWidth);
-      return FromTy->isSignedIntegerOrEnumerationType() ? mkFPtoSBV(Exp, Sort)
-                                                        : mkFPtoUBV(Exp, Sort);
-    }
-
-    if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType())
-      return ToTy->isSignedIntegerOrEnumerationType()
-                 ? mkSBVtoFP(Exp, ToBitWidth)
-                 : mkUBVtoFP(Exp, ToBitWidth);
-
-    llvm_unreachable("Unsupported explicit type cast!");
-  }
-
-  // Callback function for doCast parameter on APSInt type.
-  llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy,
-                          uint64_t ToWidth, QualType FromTy,
-                          uint64_t FromWidth) {
-    APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
-    return TargetType.convert(V);
-  }
-
-  // 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.
-  SMTExprRef getExpr(ASTContext &Ctx, SymbolRef Sym, QualType *RetTy = nullptr,
-                     bool *hasComparison = nullptr) {
-    if (hasComparison) {
-      *hasComparison = false;
-    }
-
-    return getSymExpr(Ctx, Sym, RetTy, hasComparison);
-  }
-
-  // Generate an SMTExprRef that compares the expression to zero.
-  SMTExprRef getZeroExpr(ASTContext &Ctx, const SMTExprRef &Exp, QualType Ty,
-                         bool Assumption) {
-
-    if (Ty->isRealFloatingType()) {
-      llvm::APFloat Zero =
-          llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
-      return fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE, 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 ? fromUnOp(UO_LNot, Exp) : Exp;
-
-      return fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
-                       fromInt("0", Ctx.getTypeSize(Ty)), isSigned);
-    }
-
-    llvm_unreachable("Unsupported type for zero value!");
-  }
-
-  // Recursive implementation to unpack and generate symbolic expression.
-  // Sets the hasComparison and RetTy parameters. See getExpr().
-  SMTExprRef getSymExpr(ASTContext &Ctx, SymbolRef Sym, QualType *RetTy,
-                        bool *hasComparison) {
-    if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
-      if (RetTy)
-        *RetTy = Sym->getType();
-
-      return fromData(SD->getSymbolID(), Sym->getType(),
-                      Ctx.getTypeSize(Sym->getType()));
-    }
-
-    if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
-      if (RetTy)
-        *RetTy = Sym->getType();
-
-      QualType FromTy;
-      SMTExprRef Exp =
-          getSymExpr(Ctx, 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(Ctx, Exp, FromTy, Sym->getType());
-    }
-
-    if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
-      SMTExprRef Exp = getSymBinExpr(Ctx, 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!");
-  }
-
-  // Wrapper to generate SMTExprRef from SymbolCast data.
-  SMTExprRef getCastExpr(ASTContext &Ctx, const SMTExprRef &Exp,
-                         QualType FromTy, QualType ToTy) {
-    return fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
-                    Ctx.getTypeSize(FromTy));
-  }
-
-  // Wrapper to generate SMTExprRef from BinarySymExpr.
-  // Sets the hasComparison and RetTy parameters. See getSMTExprRef().
-  SMTExprRef getSymBinExpr(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(Ctx, SIE->getLHS(), &LTy, hasComparison);
-      llvm::APSInt NewRInt;
-      std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
-      SMTExprRef RHS = fromAPSInt(NewRInt);
-      return getBinExpr(Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
-    }
-
-    if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
-      llvm::APSInt NewLInt;
-      std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
-      SMTExprRef LHS = fromAPSInt(NewLInt);
-      SMTExprRef RHS = getSymExpr(Ctx, ISE->getRHS(), &RTy, hasComparison);
-      return getBinExpr(Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
-    }
-
-    if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
-      SMTExprRef LHS = getSymExpr(Ctx, SSM->getLHS(), &LTy, hasComparison);
-      SMTExprRef RHS = getSymExpr(Ctx, SSM->getRHS(), &RTy, hasComparison);
-      return getBinExpr(Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
-    }
-
-    llvm_unreachable("Unsupported BinarySymExpr type!");
-  }
-
-  // Wrapper to generate SMTExprRef from unpacked binary symbolic expression.
-  // Sets the RetTy parameter. See getSMTExprRef().
-  SMTExprRef getBinExpr(ASTContext &Ctx, const SMTExprRef &LHS, QualType LTy,
-                        BinaryOperator::Opcode Op, const SMTExprRef &RHS,
-                        QualType RTy, QualType *RetTy) {
-    SMTExprRef NewLHS = LHS;
-    SMTExprRef NewRHS = RHS;
-    doTypeConversion(Ctx, 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 SMT sorts. Set it as a boolean type
-      // to avoid subsequent SMT errors.
-      if (BinaryOperator::isComparisonOp(Op) ||
-          BinaryOperator::isLogicalOp(Op)) {
-        *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 = Ctx.getPointerDiffType();
-      }
-    }
-
-    return LTy->isRealFloatingType()
-               ? fromFloatBinOp(NewLHS, Op, NewRHS)
-               : fromBinOp(NewLHS, Op, NewRHS,
-                           LTy->isSignedIntegerOrEnumerationType());
-  }
-
-  // Wrapper to generate SMTExprRef from a range. If From == To, an equality
-  // will be created instead.
-  SMTExprRef getRangeExpr(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 = fromAPSInt(NewFromInt);
-
-    // Convert symbol
-    QualType SymTy;
-    SMTExprRef Exp = getExpr(Ctx, Sym, &SymTy);
-
-    // Construct single (in)equality
-    if (From == To)
-      return getBinExpr(Ctx, Exp, SymTy, InRange ? BO_EQ : BO_NE, FromExp,
-                        FromTy, /*RetTy=*/nullptr);
-
-    QualType ToTy;
-    llvm::APSInt NewToInt;
-    std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
-    SMTExprRef ToExp = fromAPSInt(NewToInt);
-    assert(FromTy == ToTy && "Range values have different types!");
-
-    // Construct two (in)equalities, and a logical and/or
-    SMTExprRef LHS = getBinExpr(Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT,
-                                FromExp, FromTy, /*RetTy=*/nullptr);
-    SMTExprRef RHS =
-        getBinExpr(Ctx, Exp, SymTy, InRange ? BO_LE : BO_GT, ToExp, ToTy,
-                   /*RetTy=*/nullptr);
-
-    return fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
-                     SymTy->isSignedIntegerOrEnumerationType());
-  }
-
-  // Recover the QualType of an APSInt.
-  // TODO: Refactor to put elsewhere
-  QualType getAPSIntType(ASTContext &Ctx, const llvm::APSInt &Int) {
-    return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
-  }
-
-  // Get the QualTy for the input APSInt, and fix it if it has a bitwidth of 1.
-  std::pair<llvm::APSInt, QualType> fixAPSInt(ASTContext &Ctx,
-                                              const llvm::APSInt &Int) {
-    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(Ctx, Int).isNull()) {
-      NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
-    } else
-      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
-  void doTypeConversion(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())) {
-      doIntTypeConversion<SMTExprRef, &SMTSolver::fromCast>(Ctx, LHS, LTy, RHS,
-                                                            RTy);
-      return;
-    }
-
-    if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
-      doFloatTypeConversion<SMTExprRef, &SMTSolver::fromCast>(Ctx, 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 = fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
-          LTy = RTy;
-        } else {
-          RHS = 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
-  }
-
-  // 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(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.
-    // 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 = (this->*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 = (this->*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 = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
-        RTy = LTy;
-      } else {
-        LHS = (this->*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 = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
-        RTy = LTy;
-      } else {
-        LHS = (this->*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 = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
-        RTy = LTy;
-      } else {
-        LHS = (this->*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 = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
-      RTy = NewTy;
-      LHS = (this->*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(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 = (this->*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
-      LTy = RTy;
-      LBitWidth = RBitWidth;
-    }
-    if (!RTy->isRealFloatingType()) {
-      RHS = (this->*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 = (this->*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
-      RTy = LTy;
-    } else if (order == 0) {
-      LHS = (this->*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
-      LTy = RTy;
-    } else {
-      llvm_unreachable("Unsupported floating-point type cast!");
-    }
-  }
-
   // Returns a boolean sort.
   virtual SMTSortRef getBoolSort() = 0;
 
   // Returns an appropriate bitvector sort for the given bitwidth.
   virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
 
   // Returns a floating-point sort of width 16
   virtual SMTSortRef getFloat16Sort() = 0;
public:
   virtual SMTExprRef fromAPFloat(const llvm::APFloat &Float) = 0;
 
   /// Construct an SMTExprRef value from an APSInt.
   virtual SMTExprRef fromAPSInt(const llvm::APSInt &Int) = 0;
 
   /// Construct an SMTExprRef value from an integer.
   virtual SMTExprRef fromInt(const char *Int, uint64_t BitWidth) = 0;
 
-  /// Construct an SMTExprRef from a SymbolData.
-  virtual SMTExprRef fromData(const SymbolID ID, const QualType &Ty,
-                              uint64_t BitWidth) = 0;
-
   /// Check if the constraints are satisfiable
-  virtual ConditionTruthVal check() const = 0;
+  virtual Optional<bool> check() const = 0;
 
   /// Push the current solver state
   virtual void push() = 0;
 
   /// Pop the previous solver state
   virtual void pop(unsigned NumStates = 1) = 0;
 
   /// Reset the solver and remove all constraints.
   virtual void reset() const = 0;
 
   virtual void print(raw_ostream &OS) const = 0;
 };
 
 /// Shared pointer for SMTSolvers.
 using SMTSolverRef = std::shared_ptr<SMTSolver>;
 
 /// Convenience method to create and Z3Solver object
-std::unique_ptr<SMTSolver> CreateZ3Solver();
+SMTSolverRef CreateZ3Solver();
 
 } // namespace ento
 } // namespace clang
 
 #endif

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

 #include "clang/StaticAnalyzer/Core/BugReporter/PathDiagnostic.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExplodedGraph.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/None.h"
 #include "llvm/ADT/Optional.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/SmallPtrSet.h"
 #include "llvm/ADT/SmallString.h"
 #include "llvm/ADT/SmallVector.h"
 #include "llvm/ADT/StringExtras.h"
FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
     : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
 
 void FalsePositiveRefutationBRVisitor::finalizeVisitor(
     BugReporterContext &BRC, const ExplodedNode *EndPathNode, BugReport &BR) {
   // Collect new constraints
   VisitNode(EndPathNode, nullptr, BRC, BR);
 
   // Create a refutation manager
-  std::unique_ptr<SMTSolver> RefutationSolver = CreateZ3Solver();
+  SMTSolverRef RefutationSolver = CreateZ3Solver();
   ASTContext &Ctx = BRC.getASTContext();
 
   // Add constraints to the solver
   for (const auto &I : Constraints) {
     SymbolRef Sym = I.first;
 
     SMTExprRef Constraints = RefutationSolver->fromBoolean(false);
     for (const auto &Range : I.second) {
       Constraints = RefutationSolver->mkOr(
-          Constraints,
-          RefutationSolver->getRangeExpr(Ctx, Sym, Range.From(), Range.To(),
+          Constraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
+                                             Range.From(), Range.To(),
                                              /*InRange=*/true));
     }
     RefutationSolver->addConstraint(Constraints);
   }
 
   // And check for satisfiability
-  if (RefutationSolver->check().isConstrainedFalse())
+  Optional<bool> isSat = RefutationSolver->check();
+  if (!isSat.hasValue())
+    return;
+
+  if (!isSat.getValue())
     BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
 }
 
 std::shared_ptr<PathDiagnosticPiece>
 FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
                                             const ExplodedNode *PrevN,
                                             BugReporterContext &BRC,
                                             BugReport &BR) {

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

 //== Z3ConstraintManager.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/Basic/TargetInfo.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 
 #include "clang/Config/config.h"
 
 using namespace clang;
 using namespace ento;
 
 #if CLANG_ANALYZER_WITH_Z3
 
bool getBoolean(const SMTExprRef &Exp) override {
     return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
   }
 
   SMTExprRef getFloatRoundingMode() override {
     // TODO: Don't assume nearest ties to even rounding mode
     return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
   }
 
-  SMTExprRef fromData(const SymbolID ID, const QualType &Ty,
-                      uint64_t BitWidth) override {
-    llvm::Twine Name = "$" + llvm::Twine(ID);
-    return mkSymbol(Name.str().c_str(), mkSort(Ty, BitWidth));
-  }
-
   SMTExprRef fromBoolean(const bool Bool) override {
     Z3_ast AST =
         Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context);
     return newExprRef(Z3Expr(Context, AST));
   }
 
   SMTExprRef fromAPFloat(const llvm::APFloat &Float) override {
     SMTSortRef Sort =
bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
 
     SMTExprRef Assign = newExprRef(
         Z3Expr(Context,
                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
     SMTSortRef Sort = getSort(Assign);
     return toAPFloat(Sort, Assign, Float, true);
   }
 
-  ConditionTruthVal check() const override {
+  Optional<bool> check() const override {
     Z3_lbool res = Z3_solver_check(Context.Context, Solver);
     if (res == Z3_L_TRUE)
       return true;
 
     if (res == Z3_L_FALSE)
       return false;
 
-    return ConditionTruthVal();
+    return Optional<bool>();
   }
 
   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);
   }
bool canReasonAbout(SVal X) const override {
     llvm_unreachable("Unsupported expression to reason about!");
   }
 }; // end class Z3ConstraintManager
 
 } // end anonymous namespace
 
 #endif
 
-std::unique_ptr<SMTSolver> clang::ento::CreateZ3Solver() {
+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_BUILD_Z3=ON",
                            false);
   return nullptr;
 #endif