r299463 - [analyzer] Add new Z3 constraint manager backend

Reid Kleckner via cfe-commits cfe-commits at lists.llvm.org
Wed Apr 5 10:25:21 PDT 2017


With the combination of your change and mine (
https://reviews.llvm.org/D31677), these tests are failing with this
pickling error:
http://lab.llvm.org:8011/builders/clang-cmake-armv7-a15-full/builds/5629/steps/ninja%20check%201/logs/stdio
cPickle.PicklingError: Can't pickle <class
'lit.TestingConfig.AnalyzerTest'>: attribute lookup
lit.TestingConfig.AnalyzerTest failed

Any idea what's up? Why does AnalyzerTest multiply inherit from object?
That seems unnecessary.

On Tue, Apr 4, 2017 at 12:52 PM, Dominic Chen via cfe-commits <
cfe-commits at lists.llvm.org> wrote:

> Author: ddcc
> Date: Tue Apr  4 14:52:25 2017
> New Revision: 299463
>
> URL: http://llvm.org/viewvc/llvm-project?rev=299463&view=rev
> Log:
> [analyzer] Add new Z3 constraint manager backend
>
> Summary: Implement new Z3 constraint manager backend.
>
> Reviewers: zaks.anna, dcoughlin, NoQ, xazax.hun
>
> Subscribers: mgorny, cfe-commits
>
> Differential Revision: https://reviews.llvm.org/D28952
>
> Added:
>     cfe/trunk/cmake/modules/FindZ3.cmake
>     cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
>     cfe/trunk/test/Analysis/unsupported-types.c
> Modified:
>     cfe/trunk/CMakeLists.txt
>     cfe/trunk/include/clang/Config/config.h.cmake
>     cfe/trunk/include/clang/StaticAnalyzer/Core/Analyses.def
>     cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/
> ConstraintManager.h
>     cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt
>     cfe/trunk/test/Analysis/expr-inspection.c
>     cfe/trunk/test/Analysis/lit.local.cfg
>     cfe/trunk/test/lit.cfg
>     cfe/trunk/test/lit.site.cfg.in
>
> Modified: cfe/trunk/CMakeLists.txt
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/CMakeLists.
> txt?rev=299463&r1=299462&r2=299463&view=diff
> ============================================================
> ==================
> --- cfe/trunk/CMakeLists.txt (original)
> +++ cfe/trunk/CMakeLists.txt Tue Apr  4 14:52:25 2017
> @@ -186,6 +186,8 @@ if (LIBXML2_FOUND)
>    set(CLANG_HAVE_LIBXML 1)
>  endif()
>
> +find_package(Z3 4.5)
> +
>  include(CheckIncludeFile)
>  check_include_file(sys/resource.h CLANG_HAVE_RLIMITS)
>
> @@ -330,10 +332,6 @@ if (APPLE)
>    endif()
>  endif()
>
> -configure_file(
> -  ${CLANG_SOURCE_DIR}/include/clang/Config/config.h.cmake
> -  ${CLANG_BINARY_DIR}/include/clang/Config/config.h)
> -
>  include(CMakeParseArguments)
>  include(AddClang)
>
> @@ -371,8 +369,19 @@ option(CLANG_BUILD_TOOLS
>  option(CLANG_ENABLE_ARCMT "Build ARCMT." ON)
>  option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON)
>
> -if (NOT CLANG_ENABLE_STATIC_ANALYZER AND CLANG_ENABLE_ARCMT)
> -  message(FATAL_ERROR "Cannot disable static analyzer while enabling
> ARCMT")
> +option(CLANG_ANALYZER_BUILD_Z3
> +  "Build the static analyzer with the Z3 constraint manager." OFF)
> +
> +if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR
> CLANG_ANALYZER_BUILD_Z3))
> +  message(FATAL_ERROR "Cannot disable static analyzer while enabling
> ARCMT or Z3")
> +endif()
> +
> +if(CLANG_ANALYZER_BUILD_Z3)
> +  if(Z3_FOUND)
> +    set(CLANG_ANALYZER_WITH_Z3 1)
> +  else()
> +    message(FATAL_ERROR "Cannot find Z3 header file or shared library")
> +  endif()
>  endif()
>
>  if(CLANG_ENABLE_ARCMT)
> @@ -687,3 +696,7 @@ endif()
>  if (LLVM_ADD_NATIVE_VISUALIZERS_TO_SOLUTION)
>    add_subdirectory(utils/ClangVisualizers)
>  endif()
> +
> +configure_file(
> +  ${CLANG_SOURCE_DIR}/include/clang/Config/config.h.cmake
> +  ${CLANG_BINARY_DIR}/include/clang/Config/config.h)
>
> Added: cfe/trunk/cmake/modules/FindZ3.cmake
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/cmake/
> modules/FindZ3.cmake?rev=299463&view=auto
> ============================================================
> ==================
> --- cfe/trunk/cmake/modules/FindZ3.cmake (added)
> +++ cfe/trunk/cmake/modules/FindZ3.cmake Tue Apr  4 14:52:25 2017
> @@ -0,0 +1,28 @@
> +find_path(Z3_INCLUDE_DIR NAMES z3.h
> +   PATH_SUFFIXES libz3
> +   )
> +
> +find_library(Z3_LIBRARIES NAMES z3 libz3
> +   )
> +
> +find_program(Z3_EXECUTABLE z3)
> +
> +if(Z3_INCLUDE_DIR AND Z3_EXECUTABLE)
> +    execute_process (COMMAND ${Z3_EXECUTABLE} -version
> +      OUTPUT_VARIABLE libz3_version_str
> +      ERROR_QUIET
> +      OUTPUT_STRIP_TRAILING_WHITESPACE)
> +
> +    string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1"
> +           Z3_VERSION_STRING "${libz3_version_str}")
> +    unset(libz3_version_str)
> +endif()
> +
> +# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
> +# all listed variables are TRUE
> +include(FindPackageHandleStandardArgs)
> +FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3
> +                                  REQUIRED_VARS Z3_LIBRARIES
> Z3_INCLUDE_DIR
> +                                  VERSION_VAR Z3_VERSION_STRING)
> +
> +mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)
>
> Modified: cfe/trunk/include/clang/Config/config.h.cmake
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/
> clang/Config/config.h.cmake?rev=299463&r1=299462&r2=299463&view=diff
> ============================================================
> ==================
> --- cfe/trunk/include/clang/Config/config.h.cmake (original)
> +++ cfe/trunk/include/clang/Config/config.h.cmake Tue Apr  4 14:52:25 2017
> @@ -38,6 +38,9 @@
>  /* Define if we have libxml2 */
>  #cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML}
>
> +/* Define if we have z3 and want to build it */
> +#cmakedefine CLANG_ANALYZER_WITH_Z3 ${CLANG_ANALYZER_WITH_Z3}
> +
>  /* Define if we have sys/resource.h (rlimits) */
>  #cmakedefine CLANG_HAVE_RLIMITS ${CLANG_HAVE_RLIMITS}
>
>
> Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/Analyses.def
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/
> clang/StaticAnalyzer/Core/Analyses.def?rev=299463&r1=
> 299462&r2=299463&view=diff
> ============================================================
> ==================
> --- cfe/trunk/include/clang/StaticAnalyzer/Core/Analyses.def (original)
> +++ cfe/trunk/include/clang/StaticAnalyzer/Core/Analyses.def Tue Apr  4
> 14:52:25 2017
> @@ -22,6 +22,7 @@ ANALYSIS_STORE(RegionStore, "region", "U
>  #endif
>
>  ANALYSIS_CONSTRAINTS(RangeConstraints, "range", "Use constraint tracking
> of concrete value ranges", CreateRangeConstraintManager)
> +ANALYSIS_CONSTRAINTS(Z3Constraints, "z3", "Use Z3 contraint solver",
> CreateZ3ConstraintManager)
>
>  #ifndef ANALYSIS_DIAGNOSTICS
>  #define ANALYSIS_DIAGNOSTICS(NAME, CMDFLAG, DESC, CREATEFN)
>
> Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/
> ConstraintManager.h
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/
> clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h?rev=
> 299463&r1=299462&r2=299463&view=diff
> ============================================================
> ==================
> --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
> (original)
> +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
> Tue Apr  4 14:52:25 2017
> @@ -184,6 +184,9 @@ std::unique_ptr<ConstraintManager>
>  CreateRangeConstraintManager(ProgramStateManager &statemgr,
>                               SubEngine *subengine);
>
> +std::unique_ptr<ConstraintManager>
> +CreateZ3ConstraintManager(ProgramStateManager &statemgr, SubEngine
> *subengine);
> +
>  } // end GR namespace
>
>  } // end clang namespace
>
> Modified: cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/
> StaticAnalyzer/Core/CMakeLists.txt?rev=299463&r1=
> 299462&r2=299463&view=diff
> ============================================================
> ==================
> --- cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt (original)
> +++ cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt Tue Apr  4 14:52:25
> 2017
> @@ -1,5 +1,12 @@
>  set(LLVM_LINK_COMPONENTS support)
>
> +# Link Z3 if the user wants to build it.
> +if(CLANG_ANALYZER_WITH_Z3)
> +  set(Z3_LINK_FILES ${Z3_LIBRARIES})
> +else()
> +  set(Z3_LINK_FILES "")
> +endif()
> +
>  add_clang_library(clangStaticAnalyzerCore
>    APSIntType.cpp
>    AnalysisManager.cpp
> @@ -43,6 +50,7 @@ add_clang_library(clangStaticAnalyzerCor
>    Store.cpp
>    SubEngine.cpp
>    SymbolManager.cpp
> +  Z3ConstraintManager.cpp
>
>    LINK_LIBS
>    clangAST
> @@ -50,4 +58,12 @@ add_clang_library(clangStaticAnalyzerCor
>    clangBasic
>    clangLex
>    clangRewrite
> +  ${Z3_LINK_FILES}
>    )
> +
> +if(CLANG_ANALYZER_WITH_Z3)
> +  target_include_directories(clangStaticAnalyzerCore SYSTEM
> +    PRIVATE
> +    ${Z3_INCLUDE_DIR}
> +    )
> +endif()
>
> Added: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/
> StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=299463&view=auto
> ============================================================
> ==================
> --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (added)
> +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Tue Apr  4
> 14:52:25 2017
> @@ -0,0 +1,1618 @@
> +//== 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/
> SimpleConstraintManager.h"
> +
> +#include "clang/Config/config.h"
> +
> +using namespace clang;
> +using namespace ento;
> +
> +#if CLANG_ANALYZER_WITH_Z3
> +
> +#include <z3.h>
> +
> +// Forward declarations
> +namespace {
> +class Z3Expr;
> +class ConstraintZ3 {};
> +} // end anonymous namespace
> +
> +typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
> +
> +// Expansion of REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, Z3SetPair)
> +namespace clang {
> +namespace ento {
> +template <>
> +struct ProgramStateTrait<ConstraintZ3>
> +    : public ProgramStatePartialTrait<ConstraintZ3Ty> {
> +  static void *GDMIndex() {
> +    static int Index;
> +    return &Index;
> +  }
> +};
> +} // end namespace ento
> +} // end namespace clang
> +
> +namespace {
> +
> +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
> +
> +class Z3Context {
> +  Z3_context ZC_P;
> +
> +public:
> +  static Z3_context ZC;
> +
> +  Z3Context() : ZC_P(Z3_mk_context_rc(Z3Config().Config)) { ZC = ZC_P; }
> +
> +  ~Z3Context() {
> +    Z3_del_context(ZC);
> +    Z3_finalize_memory();
> +    ZC_P = nullptr;
> +  }
> +}; // end class Z3Context
> +
> +class Z3Sort {
> +  friend class Z3Expr;
> +
> +  Z3_sort Sort;
> +
> +  Z3Sort() : Sort(nullptr) {}
> +  Z3Sort(Z3_sort ZS) : Sort(ZS) {
> +    Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
> +  }
> +
> +public:
> +  /// Override implicit copy constructor for correct reference counting.
> +  Z3Sort(const Z3Sort &Copy) : Sort(Copy.Sort) {
> +    Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
> +  }
> +
> +  /// Provide move constructor
> +  Z3Sort(Z3Sort &&Move) : Sort(nullptr) { *this = std::move(Move); }
> +
> +  /// Provide move assignment constructor
> +  Z3Sort &operator=(Z3Sort &&Move) {
> +    if (this != &Move) {
> +      if (Sort)
> +        Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
> +      Sort = Move.Sort;
> +      Move.Sort = nullptr;
> +    }
> +    return *this;
> +  }
> +
> +  ~Z3Sort() {
> +    if (Sort)
> +      Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
> +  }
> +
> +  // Return a boolean sort.
> +  static Z3Sort getBoolSort() { return Z3Sort(Z3_mk_bool_sort(Z3Context::ZC));
> }
> +
> +  // Return an appropriate bitvector sort for the given bitwidth.
> +  static Z3Sort getBitvectorSort(unsigned BitWidth) {
> +    return Z3Sort(Z3_mk_bv_sort(Z3Context::ZC, BitWidth));
> +  }
> +
> +  // Return an appropriate floating-point sort for the given bitwidth.
> +  static Z3Sort getFloatSort(unsigned BitWidth) {
> +    Z3_sort Sort;
> +
> +    switch (BitWidth) {
> +    default:
> +      llvm_unreachable("Unsupported floating-point bitwidth!");
> +      break;
> +    case 16:
> +      Sort = Z3_mk_fpa_sort_16(Z3Context::ZC);
> +      break;
> +    case 32:
> +      Sort = Z3_mk_fpa_sort_32(Z3Context::ZC);
> +      break;
> +    case 64:
> +      Sort = Z3_mk_fpa_sort_64(Z3Context::ZC);
> +      break;
> +    case 128:
> +      Sort = Z3_mk_fpa_sort_128(Z3Context::ZC);
> +      break;
> +    }
> +    return Z3Sort(Sort);
> +  }
> +
> +  // Return an appropriate sort for the given AST.
> +  static Z3Sort getSort(Z3_ast AST) {
> +    return Z3Sort(Z3_get_sort(Z3Context::ZC, AST));
> +  }
> +
> +  Z3_sort_kind getSortKind() const {
> +    return Z3_get_sort_kind(Z3Context::ZC, Sort);
> +  }
> +
> +  unsigned getBitvectorSortSize() const {
> +    assert(getSortKind() == Z3_BV_SORT && "Not a bitvector sort!");
> +    return Z3_get_bv_sort_size(Z3Context::ZC, Sort);
> +  }
> +
> +  unsigned getFloatSortSize() const {
> +    assert(getSortKind() == Z3_FLOATING_POINT_SORT &&
> +           "Not a floating-point sort!");
> +    return Z3_fpa_get_ebits(Z3Context::ZC, Sort) +
> +           Z3_fpa_get_sbits(Z3Context::ZC, Sort);
> +  }
> +
> +  bool operator==(const Z3Sort &Other) const {
> +    return Z3_is_eq_sort(Z3Context::ZC, Sort, Other.Sort);
> +  }
> +
> +  Z3Sort &operator=(const Z3Sort &Move) {
> +    Z3_inc_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Move.Sort));
> +    Z3_dec_ref(Z3Context::ZC, reinterpret_cast<Z3_ast>(Sort));
> +    Sort = Move.Sort;
> +    return *this;
> +  }
> +
> +  void print(raw_ostream &OS) const {
> +    OS << Z3_sort_to_string(Z3Context::ZC, Sort);
> +  }
> +
> +  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
> +}; // end class Z3Sort
> +
> +class Z3Expr {
> +  friend class Z3Model;
> +  friend class Z3Solver;
> +
> +  Z3_ast AST;
> +
> +  Z3Expr(Z3_ast ZA) : AST(ZA) { Z3_inc_ref(Z3Context::ZC, AST); }
> +
> +  // Return an appropriate floating-point rounding mode.
> +  static Z3Expr getFloatRoundingMode() {
> +    // TODO: Don't assume nearest ties to even rounding mode
> +    return Z3Expr(Z3_mk_fpa_rne(Z3Context::ZC));
> +  }
> +
> +  // Determine whether two float semantics are equivalent
> +  static bool areEquivalent(const llvm::fltSemantics &LHS,
> +                            const llvm::fltSemantics &RHS) {
> +    return (llvm::APFloat::semanticsPrecision(LHS) ==
> +            llvm::APFloat::semanticsPrecision(RHS)) &&
> +           (llvm::APFloat::semanticsMinExponent(LHS) ==
> +            llvm::APFloat::semanticsMinExponent(RHS)) &&
> +           (llvm::APFloat::semanticsMaxExponent(LHS) ==
> +            llvm::APFloat::semanticsMaxExponent(RHS)) &&
> +           (llvm::APFloat::semanticsSizeInBits(LHS) ==
> +            llvm::APFloat::semanticsSizeInBits(RHS));
> +  }
> +
> +public:
> +  /// Override implicit copy constructor for correct reference counting.
> +  Z3Expr(const Z3Expr &Copy) : AST(Copy.AST) { Z3_inc_ref(Z3Context::ZC,
> AST); }
> +
> +  /// Provide move constructor
> +  Z3Expr(Z3Expr &&Move) : AST(nullptr) { *this = std::move(Move); }
> +
> +  /// Provide move assignment constructor
> +  Z3Expr &operator=(Z3Expr &&Move) {
> +    if (this != &Move) {
> +      if (AST)
> +        Z3_dec_ref(Z3Context::ZC, AST);
> +      AST = Move.AST;
> +      Move.AST = nullptr;
> +    }
> +    return *this;
> +  }
> +
> +  ~Z3Expr() {
> +    if (AST)
> +      Z3_dec_ref(Z3Context::ZC, AST);
> +  }
> +
> +  /// Get the corresponding IEEE floating-point type for a given bitwidth.
> +  static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
> +    switch (BitWidth) {
> +    default:
> +      llvm_unreachable("Unsupported floating-point semantics!");
> +      break;
> +    case 16:
> +      return llvm::APFloat::IEEEhalf();
> +    case 32:
> +      return llvm::APFloat::IEEEsingle();
> +    case 64:
> +      return llvm::APFloat::IEEEdouble();
> +    case 128:
> +      return llvm::APFloat::IEEEquad();
> +    }
> +  }
> +
> +  /// Construct a Z3Expr from a unary operator, given a Z3_context.
> +  static Z3Expr fromUnOp(const UnaryOperator::Opcode Op, const Z3Expr
> &Exp) {
> +    Z3_ast AST;
> +
> +    switch (Op) {
> +    default:
> +      llvm_unreachable("Unimplemented opcode");
> +      break;
> +
> +    case UO_Minus:
> +      AST = Z3_mk_bvneg(Z3Context::ZC, Exp.AST);
> +      break;
> +
> +    case UO_Not:
> +      AST = Z3_mk_bvnot(Z3Context::ZC, Exp.AST);
> +      break;
> +
> +    case UO_LNot:
> +      AST = Z3_mk_not(Z3Context::ZC, Exp.AST);
> +      break;
> +    }
> +
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct a Z3Expr from a floating-point unary operator, given a
> +  /// Z3_context.
> +  static Z3Expr fromFloatUnOp(const UnaryOperator::Opcode Op,
> +                              const Z3Expr &Exp) {
> +    Z3_ast AST;
> +
> +    switch (Op) {
> +    default:
> +      llvm_unreachable("Unimplemented opcode");
> +      break;
> +
> +    case UO_Minus:
> +      AST = Z3_mk_fpa_neg(Z3Context::ZC, Exp.AST);
> +      break;
> +
> +    case UO_LNot:
> +      return Z3Expr::fromUnOp(Op, Exp);
> +    }
> +
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct a Z3Expr from a n-ary binary operator.
> +  static Z3Expr fromNBinOp(const BinaryOperator::Opcode Op,
> +                           const std::vector<Z3_ast> &ASTs) {
> +    Z3_ast AST;
> +
> +    switch (Op) {
> +    default:
> +      llvm_unreachable("Unimplemented opcode");
> +      break;
> +
> +    case BO_LAnd:
> +      AST = Z3_mk_and(Z3Context::ZC, ASTs.size(), ASTs.data());
> +      break;
> +
> +    case BO_LOr:
> +      AST = Z3_mk_or(Z3Context::ZC, ASTs.size(), ASTs.data());
> +      break;
> +    }
> +
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct a Z3Expr from a binary operator, given a Z3_context.
> +  static Z3Expr fromBinOp(const Z3Expr &LHS, const BinaryOperator::Opcode
> Op,
> +                          const Z3Expr &RHS, bool isSigned) {
> +    Z3_ast AST;
> +
> +    assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
> +           "AST's must have the same sort!");
> +
> +    switch (Op) {
> +    default:
> +      llvm_unreachable("Unimplemented opcode");
> +      break;
> +
> +    // Multiplicative operators
> +    case BO_Mul:
> +      AST = Z3_mk_bvmul(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_Div:
> +      AST = isSigned ? Z3_mk_bvsdiv(Z3Context::ZC, LHS.AST, RHS.AST)
> +                     : Z3_mk_bvudiv(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_Rem:
> +      AST = isSigned ? Z3_mk_bvsrem(Z3Context::ZC, LHS.AST, RHS.AST)
> +                     : Z3_mk_bvurem(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +
> +    // Additive operators
> +    case BO_Add:
> +      AST = Z3_mk_bvadd(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_Sub:
> +      AST = Z3_mk_bvsub(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +
> +    // Bitwise shift operators
> +    case BO_Shl:
> +      AST = Z3_mk_bvshl(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_Shr:
> +      AST = isSigned ? Z3_mk_bvashr(Z3Context::ZC, LHS.AST, RHS.AST)
> +                     : Z3_mk_bvlshr(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +
> +    // Relational operators
> +    case BO_LT:
> +      AST = isSigned ? Z3_mk_bvslt(Z3Context::ZC, LHS.AST, RHS.AST)
> +                     : Z3_mk_bvult(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_GT:
> +      AST = isSigned ? Z3_mk_bvsgt(Z3Context::ZC, LHS.AST, RHS.AST)
> +                     : Z3_mk_bvugt(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_LE:
> +      AST = isSigned ? Z3_mk_bvsle(Z3Context::ZC, LHS.AST, RHS.AST)
> +                     : Z3_mk_bvule(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_GE:
> +      AST = isSigned ? Z3_mk_bvsge(Z3Context::ZC, LHS.AST, RHS.AST)
> +                     : Z3_mk_bvuge(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +
> +    // Equality operators
> +    case BO_EQ:
> +      AST = Z3_mk_eq(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_NE:
> +      return Z3Expr::fromUnOp(UO_LNot,
> +                              Z3Expr::fromBinOp(LHS, BO_EQ, RHS,
> isSigned));
> +      break;
> +
> +    // Bitwise operators
> +    case BO_And:
> +      AST = Z3_mk_bvand(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_Xor:
> +      AST = Z3_mk_bvxor(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_Or:
> +      AST = Z3_mk_bvor(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +
> +    // Logical operators
> +    case BO_LAnd:
> +    case BO_LOr: {
> +      std::vector<Z3_ast> Args = {LHS.AST, RHS.AST};
> +      return Z3Expr::fromNBinOp(Op, Args);
> +    }
> +    }
> +
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct a Z3Expr from a special floating-point binary operator,
> given
> +  /// a Z3_context.
> +  static Z3Expr fromFloatSpecialBinOp(const Z3Expr &LHS,
> +                                      const BinaryOperator::Opcode Op,
> +                                      const llvm::APFloat::fltCategory
> &RHS) {
> +    Z3_ast AST;
> +
> +    switch (Op) {
> +    default:
> +      llvm_unreachable("Unimplemented opcode");
> +      break;
> +
> +    // Equality operators
> +    case BO_EQ:
> +      switch (RHS) {
> +      case llvm::APFloat::fcInfinity:
> +        AST = Z3_mk_fpa_is_infinite(Z3Context::ZC, LHS.AST);
> +        break;
> +      case llvm::APFloat::fcNaN:
> +        AST = Z3_mk_fpa_is_nan(Z3Context::ZC, LHS.AST);
> +        break;
> +      case llvm::APFloat::fcNormal:
> +        AST = Z3_mk_fpa_is_normal(Z3Context::ZC, LHS.AST);
> +        break;
> +      case llvm::APFloat::fcZero:
> +        AST = Z3_mk_fpa_is_zero(Z3Context::ZC, LHS.AST);
> +        break;
> +      }
> +      break;
> +    case BO_NE:
> +      return Z3Expr::fromFloatUnOp(
> +          UO_LNot, Z3Expr::fromFloatSpecialBinOp(LHS, BO_EQ, RHS));
> +      break;
> +    }
> +
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct a Z3Expr from a floating-point binary operator, given a
> +  /// Z3_context.
> +  static Z3Expr fromFloatBinOp(const Z3Expr &LHS,
> +                               const BinaryOperator::Opcode Op,
> +                               const Z3Expr &RHS) {
> +    Z3_ast AST;
> +
> +    assert(Z3Sort::getSort(LHS.AST) == Z3Sort::getSort(RHS.AST) &&
> +           "AST's must have the same sort!");
> +
> +    switch (Op) {
> +    default:
> +      llvm_unreachable("Unimplemented opcode");
> +      break;
> +
> +    // Multiplicative operators
> +    case BO_Mul: {
> +      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
> +      AST = Z3_mk_fpa_mul(Z3Context::ZC, RoundingMode.AST, LHS.AST,
> RHS.AST);
> +      break;
> +    }
> +    case BO_Div: {
> +      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
> +      AST = Z3_mk_fpa_div(Z3Context::ZC, RoundingMode.AST, LHS.AST,
> RHS.AST);
> +      break;
> +    }
> +    case BO_Rem:
> +      AST = Z3_mk_fpa_rem(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +
> +    // Additive operators
> +    case BO_Add: {
> +      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
> +      AST = Z3_mk_fpa_add(Z3Context::ZC, RoundingMode.AST, LHS.AST,
> RHS.AST);
> +      break;
> +    }
> +    case BO_Sub: {
> +      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
> +      AST = Z3_mk_fpa_sub(Z3Context::ZC, RoundingMode.AST, LHS.AST,
> RHS.AST);
> +      break;
> +    }
> +
> +    // Relational operators
> +    case BO_LT:
> +      AST = Z3_mk_fpa_lt(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_GT:
> +      AST = Z3_mk_fpa_gt(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_LE:
> +      AST = Z3_mk_fpa_leq(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_GE:
> +      AST = Z3_mk_fpa_geq(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +
> +    // Equality operators
> +    case BO_EQ:
> +      AST = Z3_mk_fpa_eq(Z3Context::ZC, LHS.AST, RHS.AST);
> +      break;
> +    case BO_NE:
> +      return Z3Expr::fromFloatUnOp(UO_LNot,
> +                                   Z3Expr::fromFloatBinOp(LHS, BO_EQ,
> RHS));
> +      break;
> +
> +    // Logical operators
> +    case BO_LAnd:
> +    case BO_LOr:
> +      return Z3Expr::fromBinOp(LHS, Op, RHS, false);
> +    }
> +
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct a Z3Expr from a SymbolData, given a Z3_context.
> +  static Z3Expr fromData(const SymbolID ID, bool isBool, bool isFloat,
> +                         uint64_t BitWidth) {
> +    llvm::Twine Name = "$" + llvm::Twine(ID);
> +
> +    Z3Sort Sort;
> +    if (isBool)
> +      Sort = Z3Sort::getBoolSort();
> +    else if (isFloat)
> +      Sort = Z3Sort::getFloatSort(BitWidth);
> +    else
> +      Sort = Z3Sort::getBitvectorSort(BitWidth);
> +
> +    Z3_symbol Symbol = Z3_mk_string_symbol(Z3Context::ZC,
> Name.str().c_str());
> +    Z3_ast AST = Z3_mk_const(Z3Context::ZC, Symbol, Sort.Sort);
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct a Z3Expr from a SymbolCast, given a Z3_context.
> +  static Z3Expr fromCast(const Z3Expr &Exp, QualType ToTy, uint64_t
> ToBitWidth,
> +                         QualType FromTy, uint64_t FromBitWidth) {
> +    Z3_ast AST;
> +
> +    if ((FromTy->isIntegralOrEnumerationType() &&
> +         ToTy->isIntegralOrEnumerationType()) ||
> +        (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
> +        (FromTy->isBlockPointerType() ^ ToTy->isBlockPointerType()) ||
> +        (FromTy->isReferenceType() ^ ToTy->isReferenceType())) {
> +      // Special case: Z3 boolean type is distinct from bitvector type, so
> +      // must use if-then-else expression instead of direct cast
> +      if (FromTy->isBooleanType()) {
> +        assert(ToBitWidth > 0 && "BitWidth must be positive!");
> +        Z3Expr Zero = Z3Expr::fromInt("0", ToBitWidth);
> +        Z3Expr One = Z3Expr::fromInt("1", ToBitWidth);
> +        AST = Z3_mk_ite(Z3Context::ZC, Exp.AST, One.AST, Zero.AST);
> +      } else if (ToBitWidth > FromBitWidth) {
> +        AST = FromTy->isSignedIntegerOrEnumerationType()
> +                  ? Z3_mk_sign_ext(Z3Context::ZC, ToBitWidth -
> FromBitWidth,
> +                                   Exp.AST)
> +                  : Z3_mk_zero_ext(Z3Context::ZC, ToBitWidth -
> FromBitWidth,
> +                                   Exp.AST);
> +      } else if (ToBitWidth < FromBitWidth) {
> +        AST = Z3_mk_extract(Z3Context::ZC, ToBitWidth - 1, 0, Exp.AST);
> +      } else {
> +        // Both are bitvectors with the same width, ignore the type cast
> +        return Exp;
> +      }
> +    } else if (FromTy->isRealFloatingType() &&
> ToTy->isRealFloatingType()) {
> +      if (ToBitWidth != FromBitWidth) {
> +        Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
> +        Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
> +        AST = Z3_mk_fpa_to_fp_float(Z3Context::ZC, RoundingMode.AST,
> Exp.AST,
> +                                    Sort.Sort);
> +      } else {
> +        return Exp;
> +      }
> +    } else if (FromTy->isIntegralOrEnumerationType() &&
> +               ToTy->isRealFloatingType()) {
> +      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
> +      Z3Sort Sort = Z3Sort::getFloatSort(ToBitWidth);
> +      AST = FromTy->isSignedIntegerOrEnumerationType()
> +                ? Z3_mk_fpa_to_fp_signed(Z3Context::ZC, RoundingMode.AST,
> +                                         Exp.AST, Sort.Sort)
> +                : Z3_mk_fpa_to_fp_unsigned(Z3Context::ZC,
> RoundingMode.AST,
> +                                           Exp.AST, Sort.Sort);
> +    } else if (FromTy->isRealFloatingType() &&
> +               ToTy->isIntegralOrEnumerationType()) {
> +      Z3Expr RoundingMode = Z3Expr::getFloatRoundingMode();
> +      AST = ToTy->isSignedIntegerOrEnumerationType()
> +                ? Z3_mk_fpa_to_sbv(Z3Context::ZC, RoundingMode.AST,
> Exp.AST,
> +                                   ToBitWidth)
> +                : Z3_mk_fpa_to_ubv(Z3Context::ZC, RoundingMode.AST,
> Exp.AST,
> +                                   ToBitWidth);
> +    } else {
> +      llvm_unreachable("Unsupported explicit type cast!");
> +    }
> +
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct a Z3Expr from a boolean, given a Z3_context.
> +  static Z3Expr fromBoolean(const bool Bool) {
> +    Z3_ast AST = Bool ? Z3_mk_true(Z3Context::ZC) :
> Z3_mk_false(Z3Context::ZC);
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct a Z3Expr from a finite APFloat, given a Z3_context.
> +  static Z3Expr fromAPFloat(const llvm::APFloat &Float) {
> +    Z3_ast AST;
> +    Z3Sort Sort = Z3Sort::getFloatSort(
> +        llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
> +
> +    llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), true);
> +    Z3Expr Z3Int = Z3Expr::fromAPSInt(Int);
> +    AST = Z3_mk_fpa_to_fp_bv(Z3Context::ZC, Z3Int.AST, Sort.Sort);
> +
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct a Z3Expr from an APSInt, given a Z3_context.
> +  static Z3Expr fromAPSInt(const llvm::APSInt &Int) {
> +    Z3Sort Sort = Z3Sort::getBitvectorSort(Int.getBitWidth());
> +    Z3_ast AST =
> +        Z3_mk_numeral(Z3Context::ZC, Int.toString(10).c_str(), Sort.Sort);
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct a Z3Expr from an integer, given a Z3_context.
> +  static Z3Expr fromInt(const char *Int, uint64_t BitWidth) {
> +    Z3Sort Sort = Z3Sort::getBitvectorSort(BitWidth);
> +    Z3_ast AST = Z3_mk_numeral(Z3Context::ZC, Int, Sort.Sort);
> +    return Z3Expr(AST);
> +  }
> +
> +  /// Construct an APFloat from a Z3Expr, given the AST representation
> +  static bool toAPFloat(const Z3Sort &Sort, const Z3_ast &AST,
> +                        llvm::APFloat &Float, bool useSemantics = true) {
> +    assert(Sort.getSortKind() == Z3_FLOATING_POINT_SORT &&
> +           "Unsupported sort to floating-point!");
> +
> +    llvm::APSInt Int(Sort.getFloatSortSize(), true);
> +    const llvm::fltSemantics &Semantics =
> +        Z3Expr::getFloatSemantics(Sort.getFloatSortSize());
> +    Z3Sort BVSort = Z3Sort::getBitvectorSort(Sort.getFloatSortSize());
> +    if (!Z3Expr::toAPSInt(BVSort, AST, Int, true)) {
> +      return false;
> +    }
> +
> +    if (useSemantics &&
> +        !Z3Expr::areEquivalent(Float.getSemantics(), Semantics)) {
> +      assert(false && "Floating-point types don't match!");
> +      return false;
> +    }
> +
> +    Float = llvm::APFloat(Semantics, Int);
> +    return true;
> +  }
> +
> +  /// Construct an APSInt from a Z3Expr, given the AST representation
> +  static bool toAPSInt(const Z3Sort &Sort, const Z3_ast &AST,
> llvm::APSInt &Int,
> +                       bool useSemantics = true) {
> +    switch (Sort.getSortKind()) {
> +    default:
> +      llvm_unreachable("Unsupported sort to integer!");
> +    case Z3_BV_SORT: {
> +      if (useSemantics && Int.getBitWidth() !=
> Sort.getBitvectorSortSize()) {
> +        assert(false && "Bitvector types don't match!");
> +        return false;
> +      }
> +
> +      uint64_t Value[2];
> +      // Force cast because Z3 defines __uint64 to be a unsigned long long
> +      // type, which isn't compatible with a unsigned long type, even if
> they
> +      // are the same size.
> +      Z3_get_numeral_uint64(Z3Context::ZC, AST,
> +                            reinterpret_cast<__uint64 *>(&Value[0]));
> +      if (Sort.getBitvectorSortSize() <= 64) {
> +        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]),
> true);
> +      } else if (Sort.getBitvectorSortSize() == 128) {
> +        Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64,
> AST));
> +        Z3_get_numeral_uint64(Z3Context::ZC, AST,
> +                              reinterpret_cast<__uint64 *>(&Value[1]));
> +        Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true);
> +      } else {
> +        assert(false && "Bitwidth not supported!");
> +        return false;
> +      }
> +      return true;
> +    }
> +    case Z3_BOOL_SORT:
> +      if (useSemantics && Int.getBitWidth() < 1) {
> +        assert(false && "Boolean type doesn't match!");
> +        return false;
> +      }
> +      Int = llvm::APSInt(
> +          llvm::APInt(Int.getBitWidth(),
> +                      Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE
> ? 1
> +
>  : 0),
> +          true);
> +      return true;
> +    }
> +  }
> +
> +  void Profile(llvm::FoldingSetNodeID &ID) const {
> +    ID.AddInteger(Z3_get_ast_hash(Z3Context::ZC, AST));
> +  }
> +
> +  bool operator<(const Z3Expr &Other) const {
> +    llvm::FoldingSetNodeID ID1, ID2;
> +    Profile(ID1);
> +    Other.Profile(ID2);
> +    return ID1 < ID2;
> +  }
> +
> +  /// Comparison of AST equality, not model equivalence.
> +  bool operator==(const Z3Expr &Other) const {
> +    assert(Z3_is_eq_sort(Z3Context::ZC, Z3_get_sort(Z3Context::ZC, AST),
> +                         Z3_get_sort(Z3Context::ZC, Other.AST)) &&
> +           "AST's must have the same sort");
> +    return Z3_is_eq_ast(Z3Context::ZC, AST, Other.AST);
> +  }
> +
> +  /// Override implicit move constructor for correct reference counting.
> +  Z3Expr &operator=(const Z3Expr &Move) {
> +    Z3_inc_ref(Z3Context::ZC, Move.AST);
> +    Z3_dec_ref(Z3Context::ZC, AST);
> +    AST = Move.AST;
> +    return *this;
> +  }
> +
> +  void print(raw_ostream &OS) const {
> +    OS << Z3_ast_to_string(Z3Context::ZC, AST);
> +  }
> +
> +  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
> +}; // end class Z3Expr
> +
> +class Z3Model {
> +  Z3_model Model;
> +
> +public:
> +  Z3Model(Z3_model ZM) : Model(ZM) { Z3_model_inc_ref(Z3Context::ZC,
> Model); }
> +
> +  /// Override implicit copy constructor for correct reference counting.
> +  Z3Model(const Z3Model &Copy) : Model(Copy.Model) {
> +    Z3_model_inc_ref(Z3Context::ZC, Model);
> +  }
> +
> +  /// Provide move constructor
> +  Z3Model(Z3Model &&Move) : Model(nullptr) { *this = std::move(Move); }
> +
> +  /// Provide move assignment constructor
> +  Z3Model &operator=(Z3Model &&Move) {
> +    if (this != &Move) {
> +      if (Model)
> +        Z3_model_dec_ref(Z3Context::ZC, Model);
> +      Model = Move.Model;
> +      Move.Model = nullptr;
> +    }
> +    return *this;
> +  }
> +
> +  ~Z3Model() {
> +    if (Model)
> +      Z3_model_dec_ref(Z3Context::ZC, Model);
> +  }
> +
> +  /// Given an expression, extract the value of this operand in the model.
> +  bool getInterpretation(const Z3Expr &Exp, llvm::APSInt &Int) const {
> +    Z3_func_decl Func =
> +        Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
> +    if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
> +      return false;
> +
> +    Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model,
> Func);
> +    Z3Sort Sort = Z3Sort::getSort(Assign);
> +    return Z3Expr::toAPSInt(Sort, Assign, Int, true);
> +  }
> +
> +  /// Given an expression, extract the value of this operand in the model.
> +  bool getInterpretation(const Z3Expr &Exp, llvm::APFloat &Float) const {
> +    Z3_func_decl Func =
> +        Z3_get_app_decl(Z3Context::ZC, Z3_to_app(Z3Context::ZC, Exp.AST));
> +    if (Z3_model_has_interp(Z3Context::ZC, Model, Func) != Z3_L_TRUE)
> +      return false;
> +
> +    Z3_ast Assign = Z3_model_get_const_interp(Z3Context::ZC, Model,
> Func);
> +    Z3Sort Sort = Z3Sort::getSort(Assign);
> +    return Z3Expr::toAPFloat(Sort, Assign, Float, true);
> +  }
> +
> +  void print(raw_ostream &OS) const {
> +    OS << Z3_model_to_string(Z3Context::ZC, Model);
> +  }
> +
> +  LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
> +}; // end class Z3Model
> +
> +class Z3Solver {
> +  friend class Z3ConstraintManager;
> +
> +  Z3_solver Solver;
> +
> +  Z3Solver(Z3_solver ZS) : Solver(ZS) {
> +    Z3_solver_inc_ref(Z3Context::ZC, Solver);
> +  }
> +
> +public:
> +  /// Override implicit copy constructor for correct reference counting.
> +  Z3Solver(const Z3Solver &Copy) : Solver(Copy.Solver) {
> +    Z3_solver_inc_ref(Z3Context::ZC, Solver);
> +  }
> +
> +  /// Provide move constructor
> +  Z3Solver(Z3Solver &&Move) : Solver(nullptr) { *this = std::move(Move); }
> +
> +  /// Provide move assignment constructor
> +  Z3Solver &operator=(Z3Solver &&Move) {
> +    if (this != &Move) {
> +      if (Solver)
> +        Z3_solver_dec_ref(Z3Context::ZC, Solver);
> +      Solver = Move.Solver;
> +      Move.Solver = nullptr;
> +    }
> +    return *this;
> +  }
> +
> +  ~Z3Solver() {
> +    if (Solver)
> +      Z3_solver_dec_ref(Z3Context::ZC, Solver);
> +  }
> +
> +  /// Given a constraint, add it to the solver
> +  void addConstraint(const Z3Expr &Exp) {
> +    Z3_solver_assert(Z3Context::ZC, Solver, Exp.AST);
> +  }
> +
> +  /// Given a program state, construct the logical conjunction and add it
> to
> +  /// the solver
> +  void addStateConstraints(ProgramStateRef State) {
> +    // TODO: Don't add all the constraints, only the relevant ones
> +    ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
> +    ConstraintZ3Ty::iterator I = CZ.begin(), IE = CZ.end();
> +
> +    // Construct the logical AND of all the constraints
> +    if (I != IE) {
> +      std::vector<Z3_ast> ASTs;
> +
> +      while (I != IE)
> +        ASTs.push_back(I++->second.AST);
> +
> +      Z3Expr Conj = Z3Expr::fromNBinOp(BO_LAnd, ASTs);
> +      addConstraint(Conj);
> +    }
> +  }
> +
> +  /// Check if the constraints are satisfiable
> +  Z3_lbool check() { return Z3_solver_check(Z3Context::ZC, Solver); }
> +
> +  /// Push the current solver state
> +  void push() { return Z3_solver_push(Z3Context::ZC, Solver); }
> +
> +  /// Pop the previous solver state
> +  void pop(unsigned NumStates = 1) {
> +    assert(Z3_solver_get_num_scopes(Z3Context::ZC, Solver) >= NumStates);
> +    return Z3_solver_pop(Z3Context::ZC, Solver, NumStates);
> +  }
> +
> +  /// Get a model from the solver. Caller should check the model is
> +  /// satisfiable.
> +  Z3Model getModel() {
> +    return Z3Model(Z3_solver_get_model(Z3Context::ZC, Solver));
> +  }
> +
> +  /// Reset the solver and remove all constraints.
> +  void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
> +}; // end class Z3Solver
> +
> +void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
> +  llvm::report_fatal_error("Z3 error: " +
> +                           llvm::Twine(Z3_get_error_msg_ex(Context,
> Error)));
> +}
> +
> +class Z3ConstraintManager : public SimpleConstraintManager {
> +  Z3Context Context;
> +  mutable Z3Solver Solver;
> +
> +public:
> +  Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
> +      : SimpleConstraintManager(SE, SB),
> +        Solver(Z3_mk_simple_solver(Z3Context::ZC)) {
> +    Z3_set_error_handler(Z3Context::ZC, Z3ErrorHandler);
> +  }
> +
> +  //===-------------------------------------------------------
> -----------===//
> +  // Implementation for interface from ConstraintManager.
> +  //===-------------------------------------------------------
> -----------===//
> +
> +  bool canReasonAbout(SVal X) const override;
> +
> +  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym)
> override;
> +
> +  const llvm::APSInt *getSymVal(ProgramStateRef State,
> +                                SymbolRef Sym) const override;
> +
> +  ProgramStateRef removeDeadBindings(ProgramStateRef St,
> +                                     SymbolReaper &SymReaper) override;
> +
> +  void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
> +             const char *sep) override;
> +
> +  //===-------------------------------------------------------
> -----------===//
> +  // Implementation for interface from SimpleConstraintManager.
> +  //===-------------------------------------------------------
> -----------===//
> +
> +  ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
> +                            bool Assumption) override;
> +
> +  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State,
> SymbolRef Sym,
> +                                          const llvm::APSInt &From,
> +                                          const llvm::APSInt &To,
> +                                          bool InRange) override;
> +
> +  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef
> Sym,
> +                                       bool Assumption) override;
> +
> +private:
> +  //===-------------------------------------------------------
> -----------===//
> +  // Internal implementation.
> +  //===-------------------------------------------------------
> -----------===//
> +
> +  // Check whether a new model is satisfiable, and update the program
> state.
> +  ProgramStateRef assumeZ3Expr(ProgramStateRef State, SymbolRef Sym,
> +                               const Z3Expr &Exp);
> +
> +  // Generate and check a Z3 model, using the given constraint.
> +  Z3_lbool checkZ3Model(ProgramStateRef State, const Z3Expr &Exp) const;
> +
> +  // Generate a Z3Expr that represents the given symbolic expression.
> +  // Sets the hasComparison parameter if the expression has a comparison
> +  // operator.
> +  // Sets the RetTy parameter to the final return type after promotions
> and
> +  // casts.
> +  Z3Expr getZ3Expr(SymbolRef Sym, QualType *RetTy = nullptr,
> +                   bool *hasComparison = nullptr) const;
> +
> +  // Generate a Z3Expr that takes the logical not of an expression.
> +  Z3Expr getZ3NotExpr(const Z3Expr &Exp) const;
> +
> +  // Generate a Z3Expr that compares the expression to zero.
> +  Z3Expr getZ3ZeroExpr(const Z3Expr &Exp, QualType RetTy,
> +                       bool Assumption) const;
> +
> +  // Recursive implementation to unpack and generate symbolic expression.
> +  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
> +  Z3Expr getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
> +                      bool *hasComparison) const;
> +
> +  // Wrapper to generate Z3Expr from SymbolData.
> +  Z3Expr getZ3DataExpr(const SymbolID ID, QualType Ty) const;
> +
> +  // Wrapper to generate Z3Expr from SymbolCast.
> +  Z3Expr getZ3CastExpr(const Z3Expr &Exp, QualType FromTy, QualType Ty)
> const;
> +
> +  // Wrapper to generate Z3Expr from BinarySymExpr.
> +  // Sets the hasComparison and RetTy parameters. See getZ3Expr().
> +  Z3Expr getZ3SymBinExpr(const BinarySymExpr *BSE, bool *hasComparison,
> +                         QualType *RetTy) const;
> +
> +  // Wrapper to generate Z3Expr from unpacked binary symbolic expression.
> +  // Sets the RetTy parameter. See getZ3Expr().
> +  Z3Expr getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
> +                      BinaryOperator::Opcode Op, const Z3Expr &RHS,
> +                      QualType RTy, QualType *RetTy) const;
> +
> +  //===-------------------------------------------------------
> -----------===//
> +  // Helper functions.
> +  //===-------------------------------------------------------
> -----------===//
> +
> +  // Recover the QualType of an APSInt.
> +  // TODO: Refactor to put elsewhere
> +  QualType getAPSIntType(const llvm::APSInt &Int) const;
> +
> +  // Perform implicit type conversion on binary symbolic expressions.
> +  // May modify all input parameters.
> +  // TODO: Refactor to use built-in conversion functions
> +  void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType &LTy,
> +                        QualType &RTy) const;
> +
> +  // Perform implicit integer type conversion.
> +  // May modify all input parameters.
> +  // TODO: Refactor to use Sema::handleIntegerConversion()
> +  template <typename T,
> +            T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
> +  void doIntTypeConversion(T &LHS, QualType &LTy, T &RHS, QualType &RTy)
> const;
> +
> +  // Perform implicit floating-point type conversion.
> +  // May modify all input parameters.
> +  // TODO: Refactor to use Sema::handleFloatConversion()
> +  template <typename T,
> +            T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
> +  void doFloatTypeConversion(T &LHS, QualType &LTy, T &RHS,
> +                             QualType &RTy) const;
> +
> +  // Callback function for doCast parameter on APSInt type.
> +  static llvm::APSInt castAPSInt(const llvm::APSInt &V, QualType ToTy,
> +                                 uint64_t ToWidth, QualType FromTy,
> +                                 uint64_t FromWidth);
> +}; // end class Z3ConstraintManager
> +
> +Z3_context Z3Context::ZC;
> +
> +} // end anonymous namespace
> +
> +ProgramStateRef Z3ConstraintManager::assumeSym(ProgramStateRef State,
> +                                               SymbolRef Sym, bool
> Assumption) {
> +  QualType RetTy;
> +  bool hasComparison;
> +
> +  Z3Expr Exp = getZ3Expr(Sym, &RetTy, &hasComparison);
> +  // Create zero comparison for implicit boolean cast, with reversed
> assumption
> +  if (!hasComparison && !RetTy->isBooleanType())
> +    return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy,
> !Assumption));
> +
> +  return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));
> +}
> +
> +ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
> +    ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
> +    const llvm::APSInt &To, bool InRange) {
> +  QualType RetTy;
> +  // The expression may be casted, so we cannot call getZ3DataExpr()
> directly
> +  Z3Expr Exp = getZ3Expr(Sym, &RetTy);
> +
> +  assert((getAPSIntType(From) == getAPSIntType(To)) &&
> +         "Range values have different types!");
> +  QualType RTy = getAPSIntType(From);
> +  bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
> +  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
> +  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
> +
> +  // Construct single (in)equality
> +  if (From == To)
> +    return assumeZ3Expr(State, Sym,
> +                        getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
> +                                     FromExp, RTy, nullptr));
> +
> +  // Construct two (in)equalities, and a logical and/or
> +  Z3Expr LHS =
> +      getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy,
> nullptr);
> +  Z3Expr RHS =
> +      getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy,
> nullptr);
> +  return assumeZ3Expr(
> +      State, Sym,
> +      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
> isSignedTy));
> +}
> +
> +ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef
> State,
> +                                                          SymbolRef Sym,
> +                                                          bool
> Assumption) {
> +  // Skip anything that is unsupported
> +  return State;
> +}
> +
> +bool Z3ConstraintManager::canReasonAbout(SVal X) const {
> +  const TargetInfo &TI = getBasicVals().getContext().getTargetInfo();
> +
> +  Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
> +  if (!SymVal)
> +    return true;
> +
> +  const SymExpr *Sym = SymVal->getSymbol();
> +  do {
> +    QualType Ty = Sym->getType();
> +
> +    // Complex types are not modeled
> +    if (Ty->isComplexType() || Ty->isComplexIntegerType())
> +      return false;
> +
> +    // Non-IEEE 754 floating-point types are not modeled
> +    if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
> +         (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended()
> ||
> +          &TI.getLongDoubleFormat() == &llvm::APFloat::
> PPCDoubleDouble())))
> +      return false;
> +
> +    if (isa<SymbolData>(Sym)) {
> +      break;
> +    } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
> +      Sym = SC->getOperand();
> +    } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
> +      if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
> +        Sym = SIE->getLHS();
> +      } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
> +        Sym = ISE->getRHS();
> +      } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
> +        return canReasonAbout(nonloc::SymbolVal(SSM->getLHS())) &&
> +               canReasonAbout(nonloc::SymbolVal(SSM->getRHS()));
> +      } else {
> +        llvm_unreachable("Unsupported binary expression to reason
> about!");
> +      }
> +    } else {
> +      llvm_unreachable("Unsupported expression to reason about!");
> +    }
> +  } while (Sym);
> +
> +  return true;
> +}
> +
> +ConditionTruthVal Z3ConstraintManager::checkNull(ProgramStateRef State,
> +                                                 SymbolRef Sym) {
> +  QualType RetTy;
> +  // The expression may be casted, so we cannot call getZ3DataExpr()
> directly
> +  Z3Expr VarExp = getZ3Expr(Sym, &RetTy);
> +  Z3Expr Exp = getZ3ZeroExpr(VarExp, RetTy, true);
> +  // Negate the constraint
> +  Z3Expr NotExp = getZ3ZeroExpr(VarExp, RetTy, false);
> +
> +  Solver.reset();
> +  Solver.addStateConstraints(State);
> +
> +  Solver.push();
> +  Solver.addConstraint(Exp);
> +  Z3_lbool isSat = Solver.check();
> +
> +  Solver.pop();
> +  Solver.addConstraint(NotExp);
> +  Z3_lbool isNotSat = Solver.check();
> +
> +  // Zero is the only possible solution
> +  if (isSat == Z3_L_TRUE && isNotSat == Z3_L_FALSE)
> +    return true;
> +  // Zero is not a solution
> +  else if (isSat == Z3_L_FALSE && isNotSat == Z3_L_TRUE)
> +    return false;
> +
> +  // Zero may be a solution
> +  return ConditionTruthVal();
> +}
> +
> +const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
> +                                                   SymbolRef Sym) const {
> +  BasicValueFactory &BV = getBasicVals();
> +  ASTContext &Ctx = BV.getContext();
> +
> +  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
> +    QualType Ty = Sym->getType();
> +    assert(!Ty->isRealFloatingType());
> +    llvm::APSInt Value(Ctx.getTypeSize(Ty),
> +                       !Ty->isSignedIntegerOrEnumerationType());
> +
> +    Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
> +
> +    Solver.reset();
> +    Solver.addStateConstraints(State);
> +
> +    // Constraints are unsatisfiable
> +    if (Solver.check() != Z3_L_TRUE)
> +      return nullptr;
> +
> +    Z3Model Model = Solver.getModel();
> +    // Model does not assign interpretation
> +    if (!Model.getInterpretation(Exp, Value))
> +      return nullptr;
> +
> +    // A value has been obtained, check if it is the only value
> +    Z3Expr NotExp = Z3Expr::fromBinOp(
> +        Exp, BO_NE,
> +        Ty->isBooleanType() ? Z3Expr::fromBoolean(Value.getBoolValue())
> +                            : Z3Expr::fromAPSInt(Value),
> +        false);
> +
> +    Solver.addConstraint(NotExp);
> +    if (Solver.check() == Z3_L_TRUE)
> +      return nullptr;
> +
> +    // This is the only solution, store it
> +    return &BV.getValue(Value);
> +  } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
> +    SymbolRef CastSym = SC->getOperand();
> +    QualType CastTy = SC->getType();
> +    // Skip the void type
> +    if (CastTy->isVoidType())
> +      return nullptr;
> +
> +    const llvm::APSInt *Value;
> +    if (!(Value = getSymVal(State, CastSym)))
> +      return nullptr;
> +    return &BV.Convert(SC->getType(), *Value);
> +  } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
> +    const llvm::APSInt *LHS, *RHS;
> +    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
> +      LHS = getSymVal(State, SIE->getLHS());
> +      RHS = &SIE->getRHS();
> +    } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
> +      LHS = &ISE->getLHS();
> +      RHS = getSymVal(State, ISE->getRHS());
> +    } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
> +      // Early termination to avoid expensive call
> +      LHS = getSymVal(State, SSM->getLHS());
> +      RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
> +    } else {
> +      llvm_unreachable("Unsupported binary expression to get symbol
> value!");
> +    }
> +
> +    if (!LHS || !RHS)
> +      return nullptr;
> +
> +    llvm::APSInt ConvertedLHS = *LHS, ConvertedRHS = *RHS;
> +    QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
> +    doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
> +        ConvertedLHS, LTy, ConvertedRHS, RTy);
> +    return BV.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
> +  }
> +
> +  llvm_unreachable("Unsupported expression to get symbol value!");
> +}
> +
> +ProgramStateRef
> +Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
> +                                        SymbolReaper &SymReaper) {
> +  ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
> +  ConstraintZ3Ty::Factory &CZFactory = State->get_context<
> ConstraintZ3>();
> +
> +  for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E;
> ++I) {
> +    if (SymReaper.maybeDead(I->first))
> +      CZ = CZFactory.remove(CZ, *I);
> +  }
> +
> +  return State->set<ConstraintZ3>(CZ);
> +}
> +
> +//===------------------------------------------------------
> ------------===//
> +// Internal implementation.
> +//===------------------------------------------------------
> ------------===//
> +
> +ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State,
> +                                                  SymbolRef Sym,
> +                                                  const Z3Expr &Exp) {
> +  // Check the model, avoid simplifying AST to save time
> +  if (checkZ3Model(State, Exp) == Z3_L_TRUE)
> +    return State->add<ConstraintZ3>(std::make_pair(Sym, Exp));
> +
> +  return nullptr;
> +}
> +
> +Z3_lbool Z3ConstraintManager::checkZ3Model(ProgramStateRef State,
> +                                           const Z3Expr &Exp) const {
> +  Solver.reset();
> +  Solver.addConstraint(Exp);
> +  Solver.addStateConstraints(State);
> +  return Solver.check();
> +}
> +
> +Z3Expr Z3ConstraintManager::getZ3Expr(SymbolRef Sym, QualType *RetTy,
> +                                      bool *hasComparison) const {
> +  if (hasComparison) {
> +    *hasComparison = false;
> +  }
> +
> +  return getZ3SymExpr(Sym, RetTy, hasComparison);
> +}
> +
> +Z3Expr Z3ConstraintManager::getZ3NotExpr(const Z3Expr &Exp) const {
> +  return Z3Expr::fromUnOp(UO_LNot, Exp);
> +}
> +
> +Z3Expr Z3ConstraintManager::getZ3ZeroExpr(const Z3Expr &Exp, QualType Ty,
> +                                          bool Assumption) const {
> +  ASTContext &Ctx = getBasicVals().getContext();
> +  if (Ty->isRealFloatingType()) {
> +    llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.
> getFloatTypeSemantics(Ty));
> +    return Z3Expr::fromFloatBinOp(Exp, Assumption ? BO_EQ : BO_NE,
> +                                  Z3Expr::fromAPFloat(Zero));
> +  } else if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType()
> ||
> +             Ty->isBlockPointerType() || Ty->isReferenceType()) {
> +    bool isSigned = Ty->isSignedIntegerOrEnumerationType();
> +    // Skip explicit comparison for boolean types
> +    if (Ty->isBooleanType())
> +      return Assumption ? getZ3NotExpr(Exp) : Exp;
> +    return Z3Expr::fromBinOp(Exp, Assumption ? BO_EQ : BO_NE,
> +                             Z3Expr::fromInt("0", Ctx.getTypeSize(Ty)),
> +                             isSigned);
> +  }
> +
> +  llvm_unreachable("Unsupported type for zero value!");
> +}
> +
> +Z3Expr Z3ConstraintManager::getZ3SymExpr(SymbolRef Sym, QualType *RetTy,
> +                                         bool *hasComparison) const {
> +  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
> +    if (RetTy)
> +      *RetTy = Sym->getType();
> +
> +    return getZ3DataExpr(SD->getSymbolID(), Sym->getType());
> +  } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
> +    if (RetTy)
> +      *RetTy = Sym->getType();
> +
> +    QualType FromTy;
> +    Z3Expr Exp = getZ3SymExpr(SC->getOperand(), &FromTy, hasComparison);
> +    // Casting an expression with a comparison invalidates it. Note that
> this
> +    // must occur after the recursive call above.
> +    // e.g. (signed char) (x > 0)
> +    if (hasComparison)
> +      *hasComparison = false;
> +    return getZ3CastExpr(Exp, FromTy, Sym->getType());
> +  } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
> +    Z3Expr Exp = getZ3SymBinExpr(BSE, hasComparison, RetTy);
> +    // Set the hasComparison parameter, in post-order traversal order.
> +    if (hasComparison)
> +      *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
> +    return Exp;
> +  }
> +
> +  llvm_unreachable("Unsupported SymbolRef type!");
> +}
> +
> +Z3Expr Z3ConstraintManager::getZ3DataExpr(const SymbolID ID,
> +                                          QualType Ty) const {
> +  ASTContext &Ctx = getBasicVals().getContext();
> +  return Z3Expr::fromData(ID, Ty->isBooleanType(),
> Ty->isRealFloatingType(),
> +                          Ctx.getTypeSize(Ty));
> +}
> +
> +Z3Expr Z3ConstraintManager::getZ3CastExpr(const Z3Expr &Exp, QualType
> FromTy,
> +                                          QualType ToTy) const {
> +  ASTContext &Ctx = getBasicVals().getContext();
> +  return Z3Expr::fromCast(Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
> +                          Ctx.getTypeSize(FromTy));
> +}
> +
> +Z3Expr Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
> +                                            bool *hasComparison,
> +                                            QualType *RetTy) const {
> +  QualType LTy, RTy;
> +  BinaryOperator::Opcode Op = BSE->getOpcode();
> +
> +  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
> +    RTy = getAPSIntType(SIE->getRHS());
> +    Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), &LTy, hasComparison);
> +    Z3Expr RHS = Z3Expr::fromAPSInt(SIE->getRHS());
> +    return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
> +  } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
> +    LTy = getAPSIntType(ISE->getLHS());
> +    Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS());
> +    Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
> +    return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
> +  } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
> +    Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), &LTy, hasComparison);
> +    Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
> +    return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
> +  } else {
> +    llvm_unreachable("Unsupported BinarySymExpr type!");
> +  }
> +}
> +
> +Z3Expr Z3ConstraintManager::getZ3BinExpr(const Z3Expr &LHS, QualType LTy,
> +                                         BinaryOperator::Opcode Op,
> +                                         const Z3Expr &RHS, QualType RTy,
> +                                         QualType *RetTy) const {
> +  Z3Expr NewLHS = LHS;
> +  Z3Expr NewRHS = RHS;
> +  doTypeConversion(NewLHS, NewRHS, LTy, RTy);
> +  // Update the return type parameter if the output type has changed.
> +  if (RetTy) {
> +    // A boolean result can be represented as an integer type in C/C++,
> but at
> +    // this point we only care about the Z3 type. Set it as a boolean
> type to
> +    // avoid subsequent Z3 errors.
> +    if (BinaryOperator::isComparisonOp(Op) ||
> BinaryOperator::isLogicalOp(Op)) {
> +      ASTContext &Ctx = getBasicVals().getContext();
> +      *RetTy = Ctx.BoolTy;
> +    } else {
> +      *RetTy = LTy;
> +    }
> +
> +    // If the two operands are pointers and the operation is a
> subtraction, the
> +    // result is of type ptrdiff_t, which is signed
> +    if (LTy->isAnyPointerType() && LTy == RTy && Op == BO_Sub) {
> +      ASTContext &Ctx = getBasicVals().getContext();
> +      *RetTy = Ctx.getIntTypeForBitwidth(Ctx.getTypeSize(LTy), true);
> +    }
> +  }
> +
> +  return LTy->isRealFloatingType()
> +             ? Z3Expr::fromFloatBinOp(NewLHS, Op, NewRHS)
> +             : Z3Expr::fromBinOp(NewLHS, Op, NewRHS,
> +                                 LTy->isSignedIntegerOrEnumerationTy
> pe());
> +}
> +
> +//===------------------------------------------------------
> ------------===//
> +// Helper functions.
> +//===------------------------------------------------------
> ------------===//
> +
> +QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int)
> const {
> +  ASTContext &Ctx = getBasicVals().getContext();
> +  return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
> +}
> +
> +void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
> +                                           QualType &LTy, QualType &RTy)
> const {
> +  ASTContext &Ctx = getBasicVals().getContext();
> +
> +  // Perform type conversion
> +  if (LTy->isIntegralOrEnumerationType() &&
> +      RTy->isIntegralOrEnumerationType()) {
> +    if (LTy->isArithmeticType() && RTy->isArithmeticType())
> +      return doIntTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS,
> RTy);
> +  } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
> +    return doFloatTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS,
> RTy);
> +  } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
> +             (LTy->isBlockPointerType() || RTy->isBlockPointerType()) ||
> +             (LTy->isReferenceType() || RTy->isReferenceType())) {
> +    // TODO: Refactor to Sema::FindCompositePointerType(), and
> +    // Sema::CheckCompareOperands().
> +
> +    uint64_t LBitWidth = Ctx.getTypeSize(LTy);
> +    uint64_t RBitWidth = Ctx.getTypeSize(RTy);
> +
> +    // Cast the non-pointer type to the pointer type.
> +    // TODO: Be more strict about this.
> +    if ((LTy->isAnyPointerType() ^ RTy->isAnyPointerType()) ||
> +        (LTy->isBlockPointerType() ^ RTy->isBlockPointerType()) ||
> +        (LTy->isReferenceType() ^ RTy->isReferenceType())) {
> +      if (LTy->isNullPtrType() || LTy->isBlockPointerType() ||
> +          LTy->isReferenceType()) {
> +        LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
> +        LTy = RTy;
> +      } else {
> +        RHS = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
> +        RTy = LTy;
> +      }
> +    }
> +
> +    // Cast the void pointer type to the non-void pointer type.
> +    // For void types, this assumes that the casted value is equal to the
> value
> +    // of the original pointer, and does not account for alignment
> requirements.
> +    if (LTy->isVoidPointerType() ^ RTy->isVoidPointerType()) {
> +      assert((Ctx.getTypeSize(LTy) == Ctx.getTypeSize(RTy)) &&
> +             "Pointer types have different bitwidths!");
> +      if (RTy->isVoidPointerType())
> +        RTy = LTy;
> +      else
> +        LTy = RTy;
> +    }
> +
> +    if (LTy == RTy)
> +      return;
> +  }
> +
> +  // Fallback: for the solver, assume that these types don't really matter
> +  if ((LTy.getCanonicalType() == RTy.getCanonicalType()) ||
> +      (LTy->isObjCObjectPointerType() && RTy->isObjCObjectPointerType()))
> {
> +    LTy = RTy;
> +    return;
> +  }
> +
> +  // TODO: Refine behavior for invalid type casts
> +}
> +
> +template <typename T,
> +          T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
> +void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType &LTy, T
> &RHS,
> +                                              QualType &RTy) const {
> +  ASTContext &Ctx = getBasicVals().getContext();
> +
> +  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
> +  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
> +
> +  // 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)(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)(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)(RHS, LTy, LBitWidth, RTy, RBitWidth);
> +      RTy = LTy;
> +    } else {
> +      LHS = (*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 = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
> +      RTy = LTy;
> +    } else {
> +      LHS = (*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 = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
> +      RTy = LTy;
> +    } else {
> +      LHS = (*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 = (*doCast)(RHS, LTy, LBitWidth, RTy, RBitWidth);
> +    RTy = NewTy;
> +    LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
> +    LTy = NewTy;
> +  }
> +}
> +
> +template <typename T,
> +          T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
> +void Z3ConstraintManager::doFloatTypeConversion(T &LHS, QualType &LTy, T
> &RHS,
> +                                                QualType &RTy) const {
> +  ASTContext &Ctx = getBasicVals().getContext();
> +
> +  uint64_t LBitWidth = Ctx.getTypeSize(LTy);
> +  uint64_t RBitWidth = Ctx.getTypeSize(RTy);
> +
> +  // Perform float-point type promotion
> +  if (!LTy->isRealFloatingType()) {
> +    LHS = (*doCast)(LHS, RTy, RBitWidth, LTy, LBitWidth);
> +    LTy = RTy;
> +    LBitWidth = RBitWidth;
> +  }
> +  if (!RTy->isRealFloatingType()) {
> +    RHS = (*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 = Z3Expr::fromCast(RHS, LTy, LBitWidth, RTy, RBitWidth);
> +    RTy = LTy;
> +  } else if (order == 0) {
> +    LHS = Z3Expr::fromCast(LHS, RTy, RBitWidth, LTy, LBitWidth);
> +    LTy = RTy;
> +  } else {
> +    llvm_unreachable("Unsupported floating-point type cast!");
> +  }
> +}
> +
> +llvm::APSInt Z3ConstraintManager::castAPSInt(const llvm::APSInt &V,
> +                                             QualType ToTy, uint64_t
> ToWidth,
> +                                             QualType FromTy,
> +                                             uint64_t FromWidth) {
> +  APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationTy
> pe());
> +  return TargetType.convert(V);
> +}
> +
> +//==-------------------------------------------------------
> -----------------==/
> +// Pretty-printing.
> +//==-------------------------------------------------------
> -----------------==/
> +
> +void Z3ConstraintManager::print(ProgramStateRef St, raw_ostream &OS,
> +                                const char *nl, const char *sep) {
> +
> +  ConstraintZ3Ty CZ = St->get<ConstraintZ3>();
> +
> +  OS << nl << sep << "Constraints:";
> +  for (ConstraintZ3Ty::iterator I = CZ.begin(), E = CZ.end(); I != E;
> ++I) {
> +    OS << nl << ' ' << I->first << " : ";
> +    I->second.print(OS);
> +  }
> +  OS << nl;
> +}
> +
> +#endif
> +
> +std::unique_ptr<ConstraintManager>
> +ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine
> *Eng) {
> +#if CLANG_ANALYZER_WITH_Z3
> +  return llvm::make_unique<Z3ConstraintManager>(Eng,
> StMgr.getSValBuilder());
> +#else
> +  llvm::report_fatal_error("Clang was not compiled with Z3 support!",
> false);
> +  return nullptr;
> +#endif
> +}
>
> Modified: cfe/trunk/test/Analysis/expr-inspection.c
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/
> Analysis/expr-inspection.c?rev=299463&r1=299462&r2=299463&view=diff
> ============================================================
> ==================
> --- cfe/trunk/test/Analysis/expr-inspection.c (original)
> +++ cfe/trunk/test/Analysis/expr-inspection.c Tue Apr  4 14:52:25 2017
> @@ -19,4 +19,4 @@ void foo(int x) {
>
>  // CHECK: Expressions:
>  // CHECK-NEXT: clang_analyzer_printState : &code{clang_analyzer_
> printState}
> -// CHECK-NEXT: Ranges are empty.
> +// CHECK-NEXT: {{(Ranges are empty.)|(Constraints:[[:space:]]*$)}}
>
> Modified: cfe/trunk/test/Analysis/lit.local.cfg
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/
> Analysis/lit.local.cfg?rev=299463&r1=299462&r2=299463&view=diff
> ============================================================
> ==================
> --- cfe/trunk/test/Analysis/lit.local.cfg (original)
> +++ cfe/trunk/test/Analysis/lit.local.cfg Tue Apr  4 14:52:25 2017
> @@ -10,6 +10,10 @@ class AnalyzerTest(lit.formats.ShTest, o
>          if result.code == lit.Test.FAIL:
>              return result
>
> +        # If z3 backend available, add an additional run line for it
> +        if test.config.clang_staticanalyzer_z3 == '1':
> +            result = self.executeWithAnalyzeSubstitution(test,
> litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3')
> +
>          return result
>
>      def executeWithAnalyzeSubstitution(self, test, litConfig,
> substitution):
>
> Added: cfe/trunk/test/Analysis/unsupported-types.c
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/
> Analysis/unsupported-types.c?rev=299463&view=auto
> ============================================================
> ==================
> --- cfe/trunk/test/Analysis/unsupported-types.c (added)
> +++ cfe/trunk/test/Analysis/unsupported-types.c Tue Apr  4 14:52:25 2017
> @@ -0,0 +1,31 @@
> +// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection
> -verify %s
> +// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection
> -triple x86_64-unknown-linux -verify %s
> +// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection
> -triple powerpc64-linux-gnu -verify %s
> +
> +#define _Complex_I      (__extension__ 1.0iF)
> +
> +void clang_analyzer_eval(int);
> +
> +void complex_float(double _Complex x, double _Complex y) {
> +  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
> +  if (x != 1.0 + 3.0 * _Complex_I && y != 1.0 - 4.0 * _Complex_I)
> +    return
> +  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
> +  clang_analyzer_eval(x + y == 2.0 - 1.0 * _Complex_I); //
> expected-warning{{UNKNOWN}}
> +}
> +
> +void complex_int(int _Complex x, int _Complex y) {
> +  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
> +  if (x != 1.0 + 3.0 * _Complex_I && y != 1.0 - 4.0 * _Complex_I)
> +    return
> +  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
> +  clang_analyzer_eval(x + y == 2.0 - 1.0 * _Complex_I); //
> expected-warning{{UNKNOWN}}
> +}
> +
> +void longdouble_float(long double x, long double y) {
> +  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
> +  if (x != 0.0L && y != 1.0L)
> +    return
> +  clang_analyzer_eval(x == y); // expected-warning{{UNKNOWN}}
> +  clang_analyzer_eval(x + y == 1.0L); // expected-warning{{UNKNOWN}}
> +}
>
> Modified: cfe/trunk/test/lit.cfg
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/lit.
> cfg?rev=299463&r1=299462&r2=299463&view=diff
> ============================================================
> ==================
> --- cfe/trunk/test/lit.cfg (original)
> +++ cfe/trunk/test/lit.cfg Tue Apr  4 14:52:25 2017
> @@ -361,6 +361,9 @@ if config.clang_default_cxx_stdlib != ''
>  if config.clang_staticanalyzer:
>      config.available_features.add("staticanalyzer")
>
> +    if config.clang_staticanalyzer_z3 == '1':
> +        config.available_features.add("z3")
> +
>  # As of 2011.08, crash-recovery tests still do not pass on FreeBSD.
>  if platform.system() not in ['FreeBSD']:
>      config.available_features.add('crash-recovery')
>
> Modified: cfe/trunk/test/lit.site.cfg.in
> URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/lit.
> site.cfg.in?rev=299463&r1=299462&r2=299463&view=diff
> ============================================================
> ==================
> --- cfe/trunk/test/lit.site.cfg.in (original)
> +++ cfe/trunk/test/lit.site.cfg.in Tue Apr  4 14:52:25 2017
> @@ -18,6 +18,7 @@ config.have_zlib = @HAVE_LIBZ@
>  config.clang_arcmt = @CLANG_ENABLE_ARCMT@
>  config.clang_default_cxx_stdlib = "@CLANG_DEFAULT_CXX_STDLIB@"
>  config.clang_staticanalyzer = @CLANG_ENABLE_STATIC_ANALYZER@
> +config.clang_staticanalyzer_z3 = "@CLANG_ANALYZER_WITH_Z3@"
>  config.clang_examples = @CLANG_BUILD_EXAMPLES@
>  config.enable_shared = @ENABLE_SHARED@
>  config.enable_backtrace = @ENABLE_BACKTRACES@
>
>
> _______________________________________________
> cfe-commits mailing list
> cfe-commits at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20170405/947a29c5/attachment-0001.html>


More information about the cfe-commits mailing list