[analyzer] Update SMT API documentation and methods

[mikhail.ramalho]

Summary

Update the documentation of all the classes introduced with the new generic SMT API, most of them were referencing Z3 and how previous operations were being done (like including the context as parameter in a few methods).

Renamed the following methods, so it's clear that the operate on bitvectors:
*mkSignExt -> mkBVSignExt
*mkZeroExt -> mkBVZeroExt
*mkExtract -> mkBVExtract
*mkConcat -> mkBVConcat

Removed the unecessary methods:

• getDataExpr: it was an one line method that called fromData
• mkBitvector(const llvm::APSInt Int): it was not being used anywhere

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

public:
 
   const llvm::APSInt *getSymVal(ProgramStateRef State,
                                 SymbolRef Sym) const override;
 
   /// Dumps SMT formula
   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;
 

cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTContext.h

 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONTEXT_H
 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONTEXT_H
 
 namespace clang {
 namespace ento {
 
+/// Generic base class for SMT contexts
 class SMTContext {
 public:
   SMTContext() = default;
   virtual ~SMTContext() = default;
 };
 
 } // namespace ento
 } // namespace clang
 
 #endif

cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h

 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H
 
 #include "clang/Basic/TargetInfo.h"
 #include "llvm/ADT/FoldingSet.h"
 
 namespace clang {
 namespace ento {
 
+/// Generic base class for SMT exprs
 class SMTExpr {
 public:
   SMTExpr() = default;
   virtual ~SMTExpr() = default;
 
   bool operator<(const SMTExpr &Other) const {
     llvm::FoldingSetNodeID ID1, ID2;
     Profile(ID1);
friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {
     return LHS.equal_to(RHS);
   }
 
   virtual void print(raw_ostream &OS) const = 0;
 
   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 
 protected:
+  /// Query the SMT solver and returns true if two sorts are equal (same kind
+  /// and bit width). This does not check if the two sorts are the same objects.
   virtual bool equal_to(SMTExpr const &other) const = 0;
 };
 
+/// Shared pointer for SMTExprs, used by SMTSolver API.
 using SMTExprRef = std::shared_ptr<SMTExpr>;
 
 } // namespace ento
 } // namespace clang
 
 #endif

cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.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"
 
 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
+/// straight from clang's AST, through the from* methods.
 class SMTSolver {
 public:
   SMTSolver() = default;
   virtual ~SMTSolver() = default;
 
   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 
-  // Return an appropriate floating-point sort for the given bitwidth.
+  // Returns an appropriate floating-point sort for the given bitwidth.
   SMTSortRef getFloatSort(unsigned BitWidth) {
     switch (BitWidth) {
     case 16:
       return getFloat16Sort();
     case 32:
       return getFloat32Sort();
     case 64:
       return getFloat64Sort();
     case 128:
       return getFloat128Sort();
     default:;
     }
     llvm_unreachable("Unsupported floating-point bitwidth!");
   }
 
-  // Return an appropriate sort, given a QualType
+  // 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);
   }
 
-  /// Construct a Z3Expr from a unary operator, given a Z3_context.
+  /// 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");
   }
 
-  /// Construct a Z3Expr from a floating-point unary operator, given a
-  /// Z3_context.
+  /// 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 a Z3Expr from a n-ary binary operator.
+  /// 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 a Z3Expr from a binary operator, given a Z3_context.
+  /// 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 a Z3Expr from a special floating-point binary operator, given
-  /// a Z3_context.
+  /// 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:
case BO_NE:
       return fromFloatUnOp(UO_LNot, fromFloatSpecialBinOp(LHS, BO_EQ, RHS));
 
     default:;
     }
 
     llvm_unreachable("Unimplemented opcode");
   }
 
-  /// Construct a Z3Expr from a floating-point binary operator, given a
-  /// Z3_context.
+  /// 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:
case BO_LOr:
       return fromBinOp(LHS, Op, RHS, false);
 
     default:;
     }
 
     llvm_unreachable("Unimplemented opcode");
   }
 
-  /// Construct a Z3Expr from a SymbolCast, given a Z3_context.
+  /// 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()
-                   ? mkSignExt(ToBitWidth - FromBitWidth, Exp)
-                   : mkZeroExt(ToBitWidth - FromBitWidth, Exp);
+                   ? mkBVSignExt(ToBitWidth - FromBitWidth, Exp)
+                   : mkBVZeroExt(ToBitWidth - FromBitWidth, Exp);
 
       if (ToBitWidth < FromBitWidth)
-        return mkExtract(ToBitWidth - 1, 0, Exp);
+        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));
public:
   // 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 a Z3Expr that represents the given symbolic expression.
+  // 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 a Z3Expr that compares the expression to zero.
+  // 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() ||
       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 getZ3Expr().
+  // 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 getDataExpr(Ctx, SD->getSymbolID(), 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 =
if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
       if (hasComparison)
         *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
       return Exp;
     }
 
     llvm_unreachable("Unsupported SymbolRef type!");
   }
 
-  // Wrapper to generate Z3Expr from SymbolData.
-  SMTExprRef getDataExpr(ASTContext &Ctx, const SymbolID ID, QualType Ty) {
-    return fromData(ID, Ty, Ctx.getTypeSize(Ty));
-  }
-
-  // Wrapper to generate Z3Expr from SymbolCast.
+  // 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 Z3Expr from BinarySymExpr.
-  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
+  // 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;
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 Z3Expr from unpacked binary symbolic expression.
-  // Sets the RetTy parameter. See getZ3Expr().
+  // 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 Z3 type. Set it as a boolean type to
-      // avoid subsequent Z3 errors.
+      // 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 Z3Expr from a range. If From == To, an equality will
-  // be created instead.
+  // 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);
+                        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.
void doFloatTypeConversion(ASTContext &Ctx, T &LHS, QualType &LTy, T &RHS,
     } else if (order == 0) {
       LHS = (this->*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
       LTy = RTy;
     } else {
       llvm_unreachable("Unsupported floating-point type cast!");
     }
   }
 
-  // Return a boolean sort.
+  // Returns a boolean sort.
   virtual SMTSortRef getBoolSort() = 0;
 
-  // Return an appropriate bitvector sort for the given bitwidth.
+  // Returns an appropriate bitvector sort for the given bitwidth.
   virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
 
-  // Return a floating-point sort of width 16
+  // Returns a floating-point sort of width 16
   virtual SMTSortRef getFloat16Sort() = 0;
 
-  // Return a floating-point sort of width 32
+  // Returns a floating-point sort of width 32
   virtual SMTSortRef getFloat32Sort() = 0;
 
-  // Return a floating-point sort of width 64
+  // Returns a floating-point sort of width 64
   virtual SMTSortRef getFloat64Sort() = 0;
 
-  // Return a floating-point sort of width 128
+  // Returns a floating-point sort of width 128
   virtual SMTSortRef getFloat128Sort() = 0;
 
-  // Return an appropriate sort for the given AST.
+  // Returns an appropriate sort for the given AST.
   virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
 
-  // Return a new SMTExprRef from an SMTExpr
+  // Returns a new SMTExprRef from an SMTExpr
   virtual SMTExprRef newExprRef(const SMTExpr &E) const = 0;
 
-  /// Given a constraint, add it to the solver
+  /// Given a constraint, adds it to the solver
   virtual void addConstraint(const SMTExprRef &Exp) const = 0;
 
-  /// Create a bitvector addition operation
+  /// Creates a bitvector addition operation
   virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector subtraction operation
+  /// Creates a bitvector subtraction operation
   virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector multiplication operation
+  /// Creates a bitvector multiplication operation
   virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector signed modulus operation
+  /// Creates a bitvector signed modulus operation
   virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector unsigned modulus operation
+  /// Creates a bitvector unsigned modulus operation
   virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector signed division operation
+  /// Creates a bitvector signed division operation
   virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector unsigned division operation
+  /// Creates a bitvector unsigned division operation
   virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector logical shift left operation
+  /// Creates a bitvector logical shift left operation
   virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector arithmetic shift right operation
+  /// Creates a bitvector arithmetic shift right operation
   virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector logical shift right operation
+  /// Creates a bitvector logical shift right operation
   virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector negation operation
+  /// Creates a bitvector negation operation
   virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
 
-  /// Create a bitvector not operation
+  /// Creates a bitvector not operation
   virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
 
-  /// Create a bitvector xor operation
+  /// Creates a bitvector xor operation
   virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector or operation
+  /// Creates a bitvector or operation
   virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector and operation
+  /// Creates a bitvector and operation
   virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector unsigned less-than operation
+  /// Creates a bitvector unsigned less-than operation
   virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector signed less-than operation
+  /// Creates a bitvector signed less-than operation
   virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector unsigned greater-than operation
+  /// Creates a bitvector unsigned greater-than operation
   virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector signed greater-than operation
+  /// Creates a bitvector signed greater-than operation
   virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector unsigned less-equal-than operation
+  /// Creates a bitvector unsigned less-equal-than operation
   virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector signed less-equal-than operation
+  /// Creates a bitvector signed less-equal-than operation
   virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector unsigned greater-equal-than operation
+  /// Creates a bitvector unsigned greater-equal-than operation
   virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a bitvector signed greater-equal-than operation
+  /// Creates a bitvector signed greater-equal-than operation
   virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
-  /// Create a boolean not operation
+  /// Creates a boolean not operation
   virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
 
-  /// Create a bitvector equality operation
+  /// Creates a boolean equality operation
   virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a boolean and operation
   virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a boolean or operation
   virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a boolean ite operation
   virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
                            const SMTExprRef &F) = 0;
 
-  virtual SMTExprRef mkSignExt(unsigned i, const SMTExprRef &Exp) = 0;
+  /// Creates a bitvector sign extension operation
+  virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;
 
-  virtual SMTExprRef mkZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
+  /// Creates a bitvector zero extension operation
+  virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
 
-  virtual SMTExprRef mkExtract(unsigned High, unsigned Low,
+  /// Creates a bitvector extract operation
+  virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
                                  const SMTExprRef &Exp) = 0;
 
-  virtual SMTExprRef mkConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
+  /// Creates a bitvector concat operation
+  virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS,
+                                const SMTExprRef &RHS) = 0;
 
+  /// Creates a floating-point negation operation
   virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;
 
+  /// Creates a floating-point isInfinite operation
   virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;
 
+  /// Creates a floating-point isNaN operation
   virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;
 
+  /// Creates a floating-point isNormal operation
   virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;
 
+  /// Creates a floating-point isZero operation
   virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;
 
+  /// Creates a floating-point multiplication operation
   virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a floating-point division operation
   virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a floating-point remainder operation
   virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a floating-point addition operation
   virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a floating-point subtraction operation
   virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a floating-point less-than operation
   virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a floating-point greater-than operation
   virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a floating-point less-than-or-equal operation
   virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a floating-point greater-than-or-equal operation
   virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
 
+  /// Creates a floating-point equality operation
   virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
                                const SMTExprRef &RHS) = 0;
 
+  /// Creates a floating-point conversion from floatint-point to floating-point
+  /// operation
   virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
 
+  /// Creates a floating-point conversion from floatint-point to signed
+  /// bitvector operation
   virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From,
                                const SMTSortRef &To) = 0;
 
+  /// Creates a floating-point conversion from floatint-point to unsigned
+  /// bitvector operation
   virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From,
                                const SMTSortRef &To) = 0;
 
+  /// Creates a floating-point conversion from signed bitvector to
+  /// floatint-point operation
   virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0;
 
+  /// Creates a floating-point conversion from unsigned bitvector to
+  /// floatint-point operation
   virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0;
 
+  /// Creates a new symbol, given a name and a sort
   virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
 
-  // Return an appropriate floating-point rounding mode.
+  // Returns an appropriate floating-point rounding mode.
   virtual SMTExprRef getFloatRoundingMode() = 0;
 
+  // If the a model is available, returns the value of a given bitvector symbol
   virtual const llvm::APSInt getBitvector(const SMTExprRef &Exp) = 0;
 
+  // If the a model is available, returns the value of a given boolean symbol
   virtual bool getBoolean(const SMTExprRef &Exp) = 0;
 
-  /// Construct a const SMTExprRef &From a boolean.
+  /// Constructs an SMTExprRef from a boolean.
   virtual SMTExprRef mkBoolean(const bool b) = 0;
 
-  /// Construct a const SMTExprRef &From a finite APFloat.
+  /// Constructs an SMTExprRef from a finite APFloat.
   virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
 
-  /// Construct a const SMTExprRef &From an APSInt.
+  /// Constructs an SMTExprRef from an APSInt and its bit width
   virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
 
-  SMTExprRef mkBitvector(const llvm::APSInt Int) {
-    return mkBitvector(Int, Int.getBitWidth());
-  }
-
   /// Given an expression, extract the value of this operand in the model.
   virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
 
   /// Given an expression extract the value of this operand in the model.
   virtual bool getInterpretation(const SMTExprRef &Exp,
                                  llvm::APFloat &Float) = 0;
 
-  /// Construct a Z3Expr from a boolean, given a Z3_context.
+  /// Construct an SMTExprRef value from a boolean.
   virtual SMTExprRef fromBoolean(const bool Bool) = 0;
-  /// Construct a Z3Expr from a finite APFloat, given a Z3_context.
+
+  /// Construct an SMTExprRef value from a finite APFloat.
   virtual SMTExprRef fromAPFloat(const llvm::APFloat &Float) = 0;
 
-  /// Construct a Z3Expr from an APSInt, given a Z3_context.
+  /// Construct an SMTExprRef value from an APSInt.
   virtual SMTExprRef fromAPSInt(const llvm::APSInt &Int) = 0;
 
-  /// Construct a Z3Expr from an integer, given a Z3_context.
+  /// Construct an SMTExprRef value from an integer.
   virtual SMTExprRef fromInt(const char *Int, uint64_t BitWidth) = 0;
 
-  /// Construct a const SMTExprRef &From a SymbolData, given a SMT_context.
+  /// 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;
 
   /// 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();
 
 } // namespace ento
 } // namespace clang
 
 #endif

cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h

 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H
 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H
 
 #include "clang/Basic/TargetInfo.h"
 
 namespace clang {
 namespace ento {
 
+/// Generic base class for SMT sorts
 class SMTSort {
 public:
   SMTSort() = default;
   virtual ~SMTSort() = default;
 
+  /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
   virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
+
+  /// Returns true if the sort is a floating-point, calls isFloatSortImpl().
   virtual bool isFloatSort() const { return isFloatSortImpl(); }
+
+  /// Returns true if the sort is a boolean, calls isBooleanSortImpl().
   virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
 
+  /// Returns the bitvector size, fails if the sort is not a bitvector
+  /// Calls getBitvectorSortSizeImpl().
   virtual unsigned getBitvectorSortSize() const {
     assert(isBitvectorSort() && "Not a bitvector sort!");
     unsigned Size = getBitvectorSortSizeImpl();
     assert(Size && "Size is zero!");
     return Size;
   };
 
+  /// Returns the floating-point size, fails if the sort is not a floating-point
+  /// Calls getFloatSortSizeImpl().
   virtual unsigned getFloatSortSize() const {
     assert(isFloatSort() && "Not a floating-point sort!");
     unsigned Size = getFloatSortSizeImpl();
     assert(Size && "Size is zero!");
     return Size;
   };
 
   friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) {
     return LHS.equal_to(RHS);
   }
 
   virtual void print(raw_ostream &OS) const = 0;
 
   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
 
 protected:
+  /// Query the SMT solver and returns true if two sorts are equal (same kind
+  /// and bit width). This does not check if the two sorts are the same objects.
   virtual bool equal_to(SMTSort const &other) const = 0;
 
+  /// Query the SMT solver and checks if a sort is bitvector.
   virtual bool isBitvectorSortImpl() const = 0;
 
+  /// Query the SMT solver and checks if a sort is floating-point.
   virtual bool isFloatSortImpl() const = 0;
 
+  /// Query the SMT solver and checks if a sort is boolean.
   virtual bool isBooleanSortImpl() const = 0;
 
+  /// Query the SMT solver and returns the sort bit width.
   virtual unsigned getBitvectorSortSizeImpl() const = 0;
 
+  /// Query the SMT solver and returns the sort bit width.
   virtual unsigned getFloatSortSizeImpl() const = 0;
 };
 
+/// Shared pointer for SMTSorts, used by SMTSolver API.
 using SMTSortRef = std::shared_ptr<SMTSort>;
 
 } // namespace ento
 } // namespace clang
 
 #endif

cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp

ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State,
 
   SMTExprRef Exp = Solver->getExpr(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,
-                    Assumption ? Exp : Solver->fromUnOp(UO_LNot, Exp));
+  return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
 }
 
 ProgramStateRef SMTConstraintManager::assumeSymInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, bool InRange) {
   ASTContext &Ctx = getBasicVals().getContext();
   return assumeExpr(State, Sym,
                     Solver->getRangeExpr(Ctx, 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) {
   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 Exp = Solver->getZeroExpr(Ctx, VarExp, RetTy, true);
+  SMTExprRef Exp = Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/true);
 
   // Negate the constraint
-  SMTExprRef NotExp = Solver->getZeroExpr(Ctx, VarExp, RetTy, false);
+  SMTExprRef NotExp =
+      Solver->getZeroExpr(Ctx, VarExp, RetTy, /*Assumption=*/false);
 
   Solver->reset();
   addStateConstraints(State);
 
   Solver->push();
   Solver->addConstraint(Exp);
   ConditionTruthVal isSat = Solver->check();
 
const llvm::APSInt *SMTConstraintManager::getSymVal(ProgramStateRef State,
   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->getDataExpr(Ctx, SD->getSymbolID(), Ty);
+    SMTExprRef Exp =
+        Solver->fromData(SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
 
     Solver->reset();
     addStateConstraints(State);
 
     // Constraints are unsatisfiable
     ConditionTruthVal isSat = Solver->check();
     if (!isSat.isConstrainedTrue())
       return nullptr;

cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

 using namespace ento;
 
 #if CLANG_ANALYZER_WITH_Z3
 
 #include <z3.h>
 
 namespace {
 
+/// Configuration class for Z3
 class Z3Config {
   friend class Z3Context;
 
   Z3_config Config;
 
 public:
   Z3Config() : Config(Z3_mk_config()) {
     // Enable model finding
     Z3_set_param_value(Config, "model", "true");
     // Disable proof generation
     Z3_set_param_value(Config, "proof", "false");
     // Set timeout to 15000ms = 15s
     Z3_set_param_value(Config, "timeout", "15000");
   }
 
   ~Z3Config() { Z3_del_config(Config); }
 }; // end class Z3Config
 
+// Function used to report errors
 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
   llvm::report_fatal_error("Z3 error: " +
                            llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
 }
 
+/// Wrapper for Z3 context
 class Z3Context : public SMTContext {
 public:
   Z3_context Context;
 
   Z3Context() : SMTContext() {
     Context = Z3_mk_context_rc(Z3Config().Config);
+    // The error function is set here because the context is the first object
+    // created by the backend
     Z3_set_error_handler(Context, Z3ErrorHandler);
   }
 
   virtual ~Z3Context() {
     Z3_del_context(Context);
     Context = nullptr;
   }
 }; // end class Z3Context
 
+/// Wrapper for Z3 Sort
 class Z3Sort : public SMTSort {
   friend class Z3Solver;
 
   Z3Context &Context;
 
   Z3_sort Sort;
 
 public:
+  /// Default constructor, mainly used by make_shared
   Z3Sort(Z3Context &C, Z3_sort ZS) : SMTSort(), Context(C), Sort(ZS) {
     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
   }
 
   /// Override implicit copy constructor for correct reference counting.
   Z3Sort(const Z3Sort &Copy)
       : SMTSort(), Context(Copy.Context), Sort(Copy.Sort) {
     Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
public:
 
   SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
                    const SMTExprRef &F) override {
     return newExprRef(
         Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
                                   toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
   }
 
-  SMTExprRef mkSignExt(unsigned i, const SMTExprRef &Exp) override {
+  SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {
     return newExprRef(Z3Expr(
         Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
   }
 
-  SMTExprRef mkZeroExt(unsigned i, const SMTExprRef &Exp) override {
+  SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {
     return newExprRef(Z3Expr(
         Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
   }
 
-  SMTExprRef mkExtract(unsigned High, unsigned Low,
+  SMTExprRef mkBVExtract(unsigned High, unsigned Low,
                          const SMTExprRef &Exp) override {
     return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,
                                                     toZ3Expr(*Exp).AST)));
   }
 
-  SMTExprRef mkConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
+  SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
     return newExprRef(
         Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
                                      toZ3Expr(*RHS).AST)));
   }
 
   SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
     SMTExprRef RoundingMode = getFloatRoundingMode();
     return newExprRef(Z3Expr(
const llvm::APSInt getBitvector(const SMTExprRef &Exp) override {
     return llvm::APSInt(
         Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST));
   }
 
   bool getBoolean(const SMTExprRef &Exp) override {
     return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
   }
 
-  // Return an appropriate floating-point rounding mode.
   SMTExprRef getFloatRoundingMode() override {
     // TODO: Don't assume nearest ties to even rounding mode
     return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
   }
 
-  /// Construct a Z3Expr from a SymbolData, given a Z3_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));
   }
 
-  /// Construct a Z3Expr from a boolean, given a Z3_context.
   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));
   }
 
-  /// Construct a Z3Expr from a finite APFloat, given a Z3_context.
   SMTExprRef fromAPFloat(const llvm::APFloat &Float) override {
     SMTSortRef Sort =
         getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
 
     llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
     SMTExprRef Z3Int = fromAPSInt(Int);
     return newExprRef(Z3Expr(
         Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
                                     toZ3Sort(*Sort).Sort)));
   }
 
-  /// Construct a Z3Expr from an APSInt, given a Z3_context.
   SMTExprRef fromAPSInt(const llvm::APSInt &Int) override {
     SMTSortRef Sort = getBitvectorSort(Int.getBitWidth());
     Z3_ast AST = Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
                                toZ3Sort(*Sort).Sort);
     return newExprRef(Z3Expr(Context, AST));
   }
 
-  /// Construct a Z3Expr from an integer, given a Z3_context.
   SMTExprRef fromInt(const char *Int, uint64_t BitWidth) override {
     SMTSortRef Sort = getBitvectorSort(BitWidth);
     Z3_ast AST = Z3_mk_numeral(Context.Context, Int, toZ3Sort(*Sort).Sort);
     return newExprRef(Z3Expr(Context, AST));
   }
 
   bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
                  llvm::APFloat &Float, bool useSemantics) {
if (Sort->isBitvectorSort()) {
       // type, which isn't compatible with a unsigned long type, even if they
       // are the same size.
       Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST,
                             reinterpret_cast<__uint64 *>(&Value[0]));
       if (Sort->getBitvectorSortSize() <= 64) {
         Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]),
                            Int.isUnsigned());
       } else if (Sort->getBitvectorSortSize() == 128) {
-        SMTExprRef ASTHigh = mkExtract(127, 64, AST);
+        SMTExprRef ASTHigh = mkBVExtract(127, 64, AST);
         Z3_get_numeral_uint64(Context.Context, toZ3Expr(*AST).AST,
                               reinterpret_cast<__uint64 *>(&Value[1]));
         Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value),
                            Int.isUnsigned());
       } else {
         assert(false && "Bitwidth not supported!");
         return false;
       }
if (Sort->isBooleanSort()) {
       Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),
                          Int.isUnsigned());
       return true;
     }
 
     llvm_unreachable("Unsupported sort to integer!");
   }
 
-  /// Given an expression and a model, extract the value of this operand in
-  /// the model.
   bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
     Z3Model Model = getModel();
     Z3_func_decl Func = Z3_get_app_decl(
         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
       return false;
 
     SMTExprRef Assign = newExprRef(
         Z3Expr(Context,
                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
     SMTSortRef Sort = getSort(Assign);
     return toAPSInt(Sort, Assign, Int, true);
   }
 
-  /// Given an expression and a model, extract the value of this operand in
-  /// the model.
   bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
     Z3Model Model = getModel();
     Z3_func_decl Func = Z3_get_app_decl(
         Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
     if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
       return false;
 
     SMTExprRef Assign = newExprRef(
         Z3Expr(Context,
                Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
     SMTSortRef Sort = getSort(Assign);
     return toAPFloat(Sort, Assign, Float, true);
   }
 
-  /// Check if the constraints are satisfiable
   ConditionTruthVal 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();
   }
 
-  /// Push the current solver state
   void push() override { return Z3_solver_push(Context.Context, Solver); }
 
-  /// Pop the previous solver state
   void pop(unsigned NumStates = 1) override {
     assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
     return Z3_solver_pop(Context.Context, Solver, NumStates);
   }
 
   /// Get a model from the solver. Caller should check the model is
   /// satisfiable.
   Z3Model getModel() {