r353590 - This reverts commit 1440a848a635849b97f7a5cfa0ecc40d37451f5b.
Shoaib Meenai via cfe-commits
cfe-commits at lists.llvm.org
Fri Feb 8 18:22:10 PST 2019
I was gonna point to the directions for using llvm/utils/git-svn/git-svnrevert, but it looks like that script only works with git svn and not with the git monorepo. James, was updating the revert script something on your roadmap? If not, I'd be happy to take a stab at it (and I'm wondering if it makes sense to introduce a revert subcommand to `git llvm` rather than having a separate script).
On 2/8/19, 5:30 PM, "cfe-commits on behalf of Richard Smith via cfe-commits" <cfe-commits-bounces at lists.llvm.org on behalf of cfe-commits at lists.llvm.org> wrote:
On Fri, 8 Feb 2019 at 16:45, Mikhail R. Gadelha via cfe-commits
<cfe-commits at lists.llvm.org> wrote:
> Author: mramalho
> Date: Fri Feb 8 16:46:12 2019
> New Revision: 353590
>
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject-3Frev-3D353590-26view-3Drev&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=HF64M7rSDlri8fYyPLRCpEDRRnw_8cw91dU3-ZX_HY4&e=
> Log:
> This reverts commit 1440a848a635849b97f7a5cfa0ecc40d37451f5b.
> and commit a1853e834c65751f92521f7481b15cf0365e796b.
Please include SVN revision numbers in revert messages until LLVM
moves over to git.
> They broke arm and aarch64
>
> Added:
> cfe/trunk/cmake/modules/FindZ3.cmake
> cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
> cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
> Removed:
> cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
> Modified:
> cfe/trunk/CMakeLists.txt
> cfe/trunk/include/clang/Config/config.h.cmake
> cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
> cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
> cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
> cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt
> cfe/trunk/test/CMakeLists.txt
> cfe/trunk/test/lit.site.cfg.py.in
>
> Modified: cfe/trunk/CMakeLists.txt
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_CMakeLists.txt-3Frev-3D353590-26r1-3D353589-26r2-3D353590-26view-3Ddiff&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=PSdqknpf3IrSNcvN1YRqhUvqdPEQHudcT7ORCKdt2AY&e=
> ==============================================================================
> --- cfe/trunk/CMakeLists.txt (original)
> +++ cfe/trunk/CMakeLists.txt Fri Feb 8 16:46:12 2019
> @@ -411,9 +411,34 @@ option(CLANG_BUILD_TOOLS
> option(CLANG_ENABLE_ARCMT "Build ARCMT." ON)
> option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON)
>
> +set(CLANG_ANALYZER_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.")
> +
> +find_package(Z3 4.7.1)
> +
> +if (CLANG_ANALYZER_Z3_INSTALL_DIR)
> + if (NOT Z3_FOUND)
> + message(FATAL_ERROR "Z3 4.7.1 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR: ${CLANG_ANALYZER_Z3_INSTALL_DIR}.")
> + endif()
> +endif()
> +
> +set(CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
> +
> +option(CLANG_ANALYZER_ENABLE_Z3_SOLVER
> + "Enable Support for the Z3 constraint solver in the Clang Static Analyzer."
> + ${CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT}
> +)
> +
> +if (CLANG_ANALYZER_ENABLE_Z3_SOLVER)
> + if (NOT Z3_FOUND)
> + message(FATAL_ERROR "CLANG_ANALYZER_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.")
> + endif()
> +
> + set(CLANG_ANALYZER_WITH_Z3 1)
> +endif()
> +
> option(CLANG_ENABLE_PROTO_FUZZER "Build Clang protobuf fuzzer." OFF)
>
> -if(NOT CLANG_ENABLE_STATIC_ANALYZER AND CLANG_ENABLE_ARCMT)
> +if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_ENABLE_Z3_SOLVER))
> message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3")
> endif()
>
>
> Added: cfe/trunk/cmake/modules/FindZ3.cmake
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_cmake_modules_FindZ3.cmake-3Frev-3D353590-26view-3Dauto&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=yw58_RYhB1Z7hXxc4_EPOOivPWp9UOdBBnyvwRHLe7M&e=
> ==============================================================================
> --- cfe/trunk/cmake/modules/FindZ3.cmake (added)
> +++ cfe/trunk/cmake/modules/FindZ3.cmake Fri Feb 8 16:46:12 2019
> @@ -0,0 +1,51 @@
> +# Looking for Z3 in CLANG_ANALYZER_Z3_INSTALL_DIR
> +find_path(Z3_INCLUDE_DIR NAMES z3.h
> + NO_DEFAULT_PATH
> + PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}/include
> + PATH_SUFFIXES libz3 z3
> + )
> +
> +find_library(Z3_LIBRARIES NAMES z3 libz3
> + NO_DEFAULT_PATH
> + PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}
> + PATH_SUFFIXES lib bin
> + )
> +
> +find_program(Z3_EXECUTABLE z3
> + NO_DEFAULT_PATH
> + PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}
> + PATH_SUFFIXES bin
> + )
> +
> +# If Z3 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR look in the default directories
> +find_path(Z3_INCLUDE_DIR NAMES z3.h
> + PATH_SUFFIXES libz3 z3
> + )
> +
> +find_library(Z3_LIBRARIES NAMES z3 libz3
> + PATH_SUFFIXES lib bin
> + )
> +
> +find_program(Z3_EXECUTABLE z3
> + PATH_SUFFIXES bin
> + )
> +
> +if(Z3_INCLUDE_DIR AND Z3_LIBRARIES 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: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_include_clang_Config_config.h.cmake-3Frev-3D353590-26r1-3D353589-26r2-3D353590-26view-3Ddiff&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=F1SPW_VEQJbFUen1MlXdgI2YxxjuM-44DYy6VFKe-wk&e=
> ==============================================================================
> --- cfe/trunk/include/clang/Config/config.h.cmake (original)
> +++ cfe/trunk/include/clang/Config/config.h.cmake Fri Feb 8 16:46:12 2019
> @@ -54,6 +54,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}
>
>
> Added: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_include_clang_StaticAnalyzer_Core_PathSensitive_SMTAPI.h-3Frev-3D353590-26view-3Dauto&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=suOV-Xx8kTAlnx1mh8yHUQbKixUyBfT27nGQCh71n5M&e=
> ==============================================================================
> --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h (added)
> +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h Fri Feb 8 16:46:12 2019
> @@ -0,0 +1,404 @@
> +//===- SMTAPI.h -------------------------------------------------*- C++ -*-===//
> +//
> +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
> +// See https://urldefense.proofpoint.com/v2/url?u=https-3A__llvm.org_LICENSE.txt&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=bor1IHVhMKXiwQcvy9jhYjuptSsoAQm0Yr0eFW3v9sw&e= for license information.
> +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
> +//
> +//===----------------------------------------------------------------------===//
> +//
> +// This file defines a SMT generic Solver API, which will be the base class
> +// for every SMT solver specific class.
> +//
> +//===----------------------------------------------------------------------===//
> +
> +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
> +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSOLVER_H
> +
> +#include "clang/Basic/TargetInfo.h"
> +#include "llvm/ADT/APSInt.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;
> + };
> +
> + virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
> +
> + bool operator<(const SMTSort &Other) const {
> + llvm::FoldingSetNodeID ID1, ID2;
> + Profile(ID1);
> + Other.Profile(ID2);
> + return ID1 < ID2;
> + }
> +
> + 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 = const SMTSort *;
> +
> +/// 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);
> + Other.Profile(ID2);
> + return ID1 < ID2;
> + }
> +
> + virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
> +
> + 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 = const SMTExpr *;
> +
> +/// 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()); }
> +
> + // 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!");
> + }
> +
> + // Returns a boolean sort.
> + virtual SMTSortRef getBoolSort() = 0;
> +
> + // Returns an appropriate bitvector sort for the given bitwidth.
> + virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
> +
> + // Returns a floating-point sort of width 16
> + virtual SMTSortRef getFloat16Sort() = 0;
> +
> + // Returns a floating-point sort of width 32
> + virtual SMTSortRef getFloat32Sort() = 0;
> +
> + // Returns a floating-point sort of width 64
> + virtual SMTSortRef getFloat64Sort() = 0;
> +
> + // Returns a floating-point sort of width 128
> + virtual SMTSortRef getFloat128Sort() = 0;
> +
> + // Returns an appropriate sort for the given AST.
> + virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
> +
> + /// Given a constraint, adds it to the solver
> + virtual void addConstraint(const SMTExprRef &Exp) const = 0;
> +
> + /// Creates a bitvector addition operation
> + virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector subtraction operation
> + virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector multiplication operation
> + virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector signed modulus operation
> + virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector unsigned modulus operation
> + virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector signed division operation
> + virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector unsigned division operation
> + virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector logical shift left operation
> + virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector arithmetic shift right operation
> + virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector logical shift right operation
> + virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector negation operation
> + virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
> +
> + /// Creates a bitvector not operation
> + virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
> +
> + /// Creates a bitvector xor operation
> + virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector or operation
> + virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector and operation
> + virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector unsigned less-than operation
> + virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector signed less-than operation
> + virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector unsigned greater-than operation
> + virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector signed greater-than operation
> + virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector unsigned less-equal-than operation
> + virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector signed less-equal-than operation
> + virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector unsigned greater-equal-than operation
> + virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a bitvector signed greater-equal-than operation
> + virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
> +
> + /// Creates a boolean not operation
> + virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
> +
> + /// 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;
> +
> + /// Creates a bitvector sign extension operation
> + virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;
> +
> + /// Creates a bitvector zero extension operation
> + virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
> +
> + /// Creates a bitvector extract operation
> + virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
> + const SMTExprRef &Exp) = 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 signed bitvector to
> + /// floatint-point operation
> + virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From,
> + const SMTSortRef &To) = 0;
> +
> + /// Creates a floating-point conversion from unsigned bitvector to
> + /// floatint-point operation
> + virtual SMTExprRef mkUBVtoFP(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, unsigned ToWidth) = 0;
> +
> + /// Creates a floating-point conversion from floatint-point to unsigned
> + /// bitvector operation
> + virtual SMTExprRef mkFPtoUBV(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;
> +
> + // 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 llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
> + bool isUnsigned) = 0;
> +
> + // If the a model is available, returns the value of a given boolean symbol
> + virtual bool getBoolean(const SMTExprRef &Exp) = 0;
> +
> + /// Constructs an SMTExprRef from a boolean.
> + virtual SMTExprRef mkBoolean(const bool b) = 0;
> +
> + /// Constructs an SMTExprRef from a finite APFloat.
> + virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
> +
> + /// Constructs an SMTExprRef from an APSInt and its bit width
> + virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
> +
> + /// 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;
> +
> + /// Check if the constraints are satisfiable
> + virtual Optional<bool> check() const = 0;
> +
> + /// Push the current solver state
> + virtual void push() = 0;
> +
> + /// Pop the previous solver state
> + virtual void pop(unsigned NumStates = 1) = 0;
> +
> + /// Reset the solver and remove all constraints.
> + virtual void reset() = 0;
> +
> + /// Checks if the solver supports floating-points.
> + virtual bool isFPSupported() = 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
> +SMTSolverRef CreateZ3Solver();
> +
> +} // namespace ento
> +} // namespace clang
> +
> +#endif
>
> Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_include_clang_StaticAnalyzer_Core_PathSensitive_SMTConstraintManager.h-3Frev-3D353590-26r1-3D353589-26r2-3D353590-26view-3Ddiff&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=9ablQOCr5sS8TbukfpsDGYXGEejSvSD01PAW6jzYyRA&e=
> ==============================================================================
> --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original)
> +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Fri Feb 8 16:46:12 2019
> @@ -18,7 +18,7 @@
> #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
>
> typedef llvm::ImmutableSet<
> - std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
> + std::pair<clang::ento::SymbolRef, const clang::ento::SMTExpr *>>
> ConstraintSMTTy;
> REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy)
>
> @@ -26,7 +26,7 @@ namespace clang {
> namespace ento {
>
> class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
> - mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
> + mutable SMTSolverRef Solver = CreateZ3Solver();
>
> public:
> SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
> @@ -44,8 +44,7 @@ public:
> QualType RetTy;
> bool hasComparison;
>
> - llvm::SMTExprRef Exp =
> - SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
> + SMTExprRef Exp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
>
> // Create zero comparison for implicit boolean cast, with reversed
> // assumption
> @@ -81,12 +80,12 @@ public:
>
> QualType RetTy;
> // The expression may be casted, so we cannot call getZ3DataExpr() directly
> - llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
> - llvm::SMTExprRef Exp =
> + SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
> + SMTExprRef Exp =
> SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
>
> // Negate the constraint
> - llvm::SMTExprRef NotExp =
> + SMTExprRef NotExp =
> SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
>
> ConditionTruthVal isSat = checkModel(State, Sym, Exp);
> @@ -119,7 +118,7 @@ public:
> // this method tries to get the interpretation (the actual value) from
> // the solver, which is currently not cached.
>
> - llvm::SMTExprRef Exp =
> + SMTExprRef Exp =
> SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
>
> Solver->reset();
> @@ -135,7 +134,7 @@ public:
> return nullptr;
>
> // A value has been obtained, check if it is the only value
> - llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
> + SMTExprRef NotExp = SMTConv::fromBinOp(
> Solver, Exp, BO_NE,
> Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
> : Solver->mkBitvector(Value, Value.getBitWidth()),
> @@ -273,7 +272,7 @@ public:
> protected:
> // Check whether a new model is satisfiable, and update the program state.
> virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
> - const llvm::SMTExprRef &Exp) {
> + const SMTExprRef &Exp) {
> // Check the model, avoid simplifying AST to save time
> if (checkModel(State, Sym, Exp).isConstrainedTrue())
> return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
> @@ -290,9 +289,9 @@ protected:
>
> // Construct the logical AND of all the constraints
> if (I != IE) {
> - std::vector<llvm::SMTExprRef> ASTs;
> + std::vector<SMTExprRef> ASTs;
>
> - llvm::SMTExprRef Constraint = I++->second;
> + SMTExprRef Constraint = I++->second;
> while (I != IE) {
> Constraint = Solver->mkAnd(Constraint, I++->second);
> }
> @@ -303,7 +302,7 @@ protected:
>
> // Generate and check a Z3 model, using the given constraint.
> ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
> - const llvm::SMTExprRef &Exp) const {
> + const SMTExprRef &Exp) const {
> ProgramStateRef NewState =
> State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
>
>
> Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_include_clang_StaticAnalyzer_Core_PathSensitive_SMTConv.h-3Frev-3D353590-26r1-3D353589-26r2-3D353590-26view-3Ddiff&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=Qy_mV1oH6tLvZ5lF9WSm4uUGseRWPLmDYAgeI0oN8jA&e=
> ==============================================================================
> --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h (original)
> +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h Fri Feb 8 16:46:12 2019
> @@ -15,8 +15,8 @@
>
> #include "clang/AST/Expr.h"
> #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
> +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTAPI.h"
> #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
> -#include "llvm/Support/SMTAPI.h"
>
> namespace clang {
> namespace ento {
> @@ -24,8 +24,8 @@ namespace ento {
> class SMTConv {
> public:
> // Returns an appropriate sort, given a QualType and it's bit width.
> - static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,
> - const QualType &Ty, unsigned BitWidth) {
> + static inline SMTSortRef mkSort(SMTSolverRef &Solver, const QualType &Ty,
> + unsigned BitWidth) {
> if (Ty->isBooleanType())
> return Solver->getBoolSort();
>
> @@ -35,10 +35,10 @@ public:
> return Solver->getBitvectorSort(BitWidth);
> }
>
> - /// Constructs an SMTSolverRef from an unary operator.
> - static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver,
> - const UnaryOperator::Opcode Op,
> - const llvm::SMTExprRef &Exp) {
> + /// Constructs an SMTExprRef from an unary operator.
> + static inline SMTExprRef fromUnOp(SMTSolverRef &Solver,
> + const UnaryOperator::Opcode Op,
> + const SMTExprRef &Exp) {
> switch (Op) {
> case UO_Minus:
> return Solver->mkBVNeg(Exp);
> @@ -54,10 +54,10 @@ public:
> llvm_unreachable("Unimplemented opcode");
> }
>
> - /// Constructs an SMTSolverRef from a floating-point unary operator.
> - static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver,
> - const UnaryOperator::Opcode Op,
> - const llvm::SMTExprRef &Exp) {
> + /// Constructs an SMTExprRef from a floating-point unary operator.
> + static inline SMTExprRef fromFloatUnOp(SMTSolverRef &Solver,
> + const UnaryOperator::Opcode Op,
> + const SMTExprRef &Exp) {
> switch (Op) {
> case UO_Minus:
> return Solver->mkFPNeg(Exp);
> @@ -70,28 +70,27 @@ public:
> llvm_unreachable("Unimplemented opcode");
> }
>
> - /// Construct an SMTSolverRef from a n-ary binary operator.
> - static inline llvm::SMTExprRef
> - fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op,
> - const std::vector<llvm::SMTExprRef> &ASTs) {
> + /// Construct an SMTExprRef from a n-ary binary operator.
> + static inline SMTExprRef fromNBinOp(SMTSolverRef &Solver,
> + const BinaryOperator::Opcode Op,
> + const std::vector<SMTExprRef> &ASTs) {
> assert(!ASTs.empty());
>
> if (Op != BO_LAnd && Op != BO_LOr)
> llvm_unreachable("Unimplemented opcode");
>
> - llvm::SMTExprRef res = ASTs.front();
> + SMTExprRef res = ASTs.front();
> for (std::size_t i = 1; i < ASTs.size(); ++i)
> res = (Op == BO_LAnd) ? Solver->mkAnd(res, ASTs[i])
> : Solver->mkOr(res, ASTs[i]);
> return res;
> }
>
> - /// Construct an SMTSolverRef from a binary operator.
> - static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver,
> - const llvm::SMTExprRef &LHS,
> - const BinaryOperator::Opcode Op,
> - const llvm::SMTExprRef &RHS,
> - bool isSigned) {
> + /// Construct an SMTExprRef from a binary operator.
> + static inline SMTExprRef fromBinOp(SMTSolverRef &Solver,
> + const SMTExprRef &LHS,
> + const BinaryOperator::Opcode Op,
> + const SMTExprRef &RHS, bool isSigned) {
> assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
> "AST's must have the same sort!");
>
> @@ -163,10 +162,9 @@ public:
> llvm_unreachable("Unimplemented opcode");
> }
>
> - /// Construct an SMTSolverRef from a special floating-point binary
> - /// operator.
> - static inline llvm::SMTExprRef
> - fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS,
> + /// Construct an SMTExprRef from a special floating-point binary operator.
> + static inline SMTExprRef
> + fromFloatSpecialBinOp(SMTSolverRef &Solver, const SMTExprRef &LHS,
> const BinaryOperator::Opcode Op,
> const llvm::APFloat::fltCategory &RHS) {
> switch (Op) {
> @@ -197,11 +195,11 @@ public:
> llvm_unreachable("Unimplemented opcode");
> }
>
> - /// Construct an SMTSolverRef from a floating-point binary operator.
> - static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver,
> - const llvm::SMTExprRef &LHS,
> - const BinaryOperator::Opcode Op,
> - const llvm::SMTExprRef &RHS) {
> + /// Construct an SMTExprRef from a floating-point binary operator.
> + static inline SMTExprRef fromFloatBinOp(SMTSolverRef &Solver,
> + const SMTExprRef &LHS,
> + const BinaryOperator::Opcode Op,
> + const SMTExprRef &RHS) {
> assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) &&
> "AST's must have the same sort!");
>
> @@ -255,13 +253,11 @@ public:
> llvm_unreachable("Unimplemented opcode");
> }
>
> - /// Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy,
> - /// and their bit widths.
> - static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver,
> - const llvm::SMTExprRef &Exp,
> - QualType ToTy, uint64_t ToBitWidth,
> - QualType FromTy,
> - uint64_t FromBitWidth) {
> + /// Construct an SMTExprRef from a QualType FromTy to a QualType ToTy, and
> + /// their bit widths.
> + static inline SMTExprRef fromCast(SMTSolverRef &Solver, const SMTExprRef &Exp,
> + QualType ToTy, uint64_t ToBitWidth,
> + QualType FromTy, uint64_t FromBitWidth) {
> if ((FromTy->isIntegralOrEnumerationType() &&
> ToTy->isIntegralOrEnumerationType()) ||
> (FromTy->isAnyPointerType() ^ ToTy->isAnyPointerType()) ||
> @@ -295,7 +291,7 @@ public:
> }
>
> if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) {
> - llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
> + SMTSortRef Sort = Solver->getFloatSort(ToBitWidth);
> return FromTy->isSignedIntegerOrEnumerationType()
> ? Solver->mkSBVtoFP(Exp, Sort)
> : Solver->mkUBVtoFP(Exp, Sort);
> @@ -310,7 +306,7 @@ public:
> }
>
> // Callback function for doCast parameter on APSInt type.
> - static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver,
> + static inline llvm::APSInt castAPSInt(SMTSolverRef &Solver,
> const llvm::APSInt &V, QualType ToTy,
> uint64_t ToWidth, QualType FromTy,
> uint64_t FromWidth) {
> @@ -318,32 +314,30 @@ public:
> return TargetType.convert(V);
> }
>
> - /// Construct an SMTSolverRef from a SymbolData.
> - static inline llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver,
> - const SymbolID ID, const QualType &Ty,
> - uint64_t BitWidth) {
> + /// Construct an SMTExprRef from a SymbolData.
> + static inline SMTExprRef fromData(SMTSolverRef &Solver, const SymbolID ID,
> + const QualType &Ty, uint64_t BitWidth) {
> llvm::Twine Name = "$" + llvm::Twine(ID);
> return Solver->mkSymbol(Name.str().c_str(), mkSort(Solver, Ty, BitWidth));
> }
>
> - // Wrapper to generate SMTSolverRef from SymbolCast data.
> - static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,
> - ASTContext &Ctx,
> - const llvm::SMTExprRef &Exp,
> - QualType FromTy, QualType ToTy) {
> + // Wrapper to generate SMTExprRef from SymbolCast data.
> + static inline SMTExprRef getCastExpr(SMTSolverRef &Solver, ASTContext &Ctx,
> + const SMTExprRef &Exp, QualType FromTy,
> + QualType ToTy) {
> return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
> Ctx.getTypeSize(FromTy));
> }
>
> - // Wrapper to generate SMTSolverRef from unpacked binary symbolic
> - // expression. Sets the RetTy parameter. See getSMTSolverRef().
> - static inline llvm::SMTExprRef
> - getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx,
> - const llvm::SMTExprRef &LHS, QualType LTy,
> - BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS,
> - QualType RTy, QualType *RetTy) {
> - llvm::SMTExprRef NewLHS = LHS;
> - llvm::SMTExprRef NewRHS = RHS;
> + // Wrapper to generate SMTExprRef from unpacked binary symbolic expression.
> + // Sets the RetTy parameter. See getSMTExprRef().
> + static inline SMTExprRef getBinExpr(SMTSolverRef &Solver, ASTContext &Ctx,
> + const SMTExprRef &LHS, QualType LTy,
> + BinaryOperator::Opcode Op,
> + const SMTExprRef &RHS, QualType RTy,
> + QualType *RetTy) {
> + SMTExprRef NewLHS = LHS;
> + SMTExprRef NewRHS = RHS;
> doTypeConversion(Solver, Ctx, NewLHS, NewRHS, LTy, RTy);
>
> // Update the return type parameter if the output type has changed.
> @@ -371,40 +365,36 @@ public:
> LTy->isSignedIntegerOrEnumerationType());
> }
>
> - // Wrapper to generate SMTSolverRef from BinarySymExpr.
> - // Sets the hasComparison and RetTy parameters. See getSMTSolverRef().
> - static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver,
> - ASTContext &Ctx,
> - const BinarySymExpr *BSE,
> - bool *hasComparison,
> - QualType *RetTy) {
> + // Wrapper to generate SMTExprRef from BinarySymExpr.
> + // Sets the hasComparison and RetTy parameters. See getSMTExprRef().
> + static inline SMTExprRef getSymBinExpr(SMTSolverRef &Solver, ASTContext &Ctx,
> + const BinarySymExpr *BSE,
> + bool *hasComparison, QualType *RetTy) {
> QualType LTy, RTy;
> BinaryOperator::Opcode Op = BSE->getOpcode();
>
> if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
> - llvm::SMTExprRef LHS =
> + SMTExprRef LHS =
> getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison);
> llvm::APSInt NewRInt;
> std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS());
> - llvm::SMTExprRef RHS =
> - Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
> + SMTExprRef RHS = Solver->mkBitvector(NewRInt, NewRInt.getBitWidth());
> return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
> }
>
> if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
> llvm::APSInt NewLInt;
> std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS());
> - llvm::SMTExprRef LHS =
> - Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
> - llvm::SMTExprRef RHS =
> + SMTExprRef LHS = Solver->mkBitvector(NewLInt, NewLInt.getBitWidth());
> + SMTExprRef RHS =
> getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison);
> return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
> }
>
> if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
> - llvm::SMTExprRef LHS =
> + SMTExprRef LHS =
> getSymExpr(Solver, Ctx, SSM->getLHS(), <y, hasComparison);
> - llvm::SMTExprRef RHS =
> + SMTExprRef RHS =
> getSymExpr(Solver, Ctx, SSM->getRHS(), &RTy, hasComparison);
> return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy);
> }
> @@ -414,10 +404,9 @@ public:
>
> // Recursive implementation to unpack and generate symbolic expression.
> // Sets the hasComparison and RetTy parameters. See getExpr().
> - static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
> - ASTContext &Ctx, SymbolRef Sym,
> - QualType *RetTy,
> - bool *hasComparison) {
> + static inline SMTExprRef getSymExpr(SMTSolverRef &Solver, ASTContext &Ctx,
> + SymbolRef Sym, QualType *RetTy,
> + bool *hasComparison) {
> if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
> if (RetTy)
> *RetTy = Sym->getType();
> @@ -431,7 +420,7 @@ public:
> *RetTy = Sym->getType();
>
> QualType FromTy;
> - llvm::SMTExprRef Exp =
> + SMTExprRef Exp =
> getSymExpr(Solver, Ctx, SC->getOperand(), &FromTy, hasComparison);
>
> // Casting an expression with a comparison invalidates it. Note that this
> @@ -443,8 +432,7 @@ public:
> }
>
> if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
> - llvm::SMTExprRef Exp =
> - getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
> + SMTExprRef Exp = getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
> // Set the hasComparison parameter, in post-order traversal order.
> if (hasComparison)
> *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
> @@ -454,14 +442,13 @@ public:
> llvm_unreachable("Unsupported SymbolRef type!");
> }
>
> - // Generate an SMTSolverRef 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.
> - static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver,
> - ASTContext &Ctx, SymbolRef Sym,
> - QualType *RetTy = nullptr,
> - bool *hasComparison = nullptr) {
> + static inline SMTExprRef getExpr(SMTSolverRef &Solver, ASTContext &Ctx,
> + SymbolRef Sym, QualType *RetTy = nullptr,
> + bool *hasComparison = nullptr) {
> if (hasComparison) {
> *hasComparison = false;
> }
> @@ -469,11 +456,11 @@ public:
> return getSymExpr(Solver, Ctx, Sym, RetTy, hasComparison);
> }
>
> - // Generate an SMTSolverRef that compares the expression to zero.
> - static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver,
> - ASTContext &Ctx,
> - const llvm::SMTExprRef &Exp,
> - QualType Ty, bool Assumption) {
> + // Generate an SMTExprRef that compares the expression to zero.
> + static inline SMTExprRef getZeroExpr(SMTSolverRef &Solver, ASTContext &Ctx,
> + const SMTExprRef &Exp, QualType Ty,
> + bool Assumption) {
> +
> if (Ty->isRealFloatingType()) {
> llvm::APFloat Zero =
> llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty));
> @@ -498,21 +485,21 @@ public:
> llvm_unreachable("Unsupported type for zero value!");
> }
>
> - // Wrapper to generate SMTSolverRef from a range. If From == To, an
> - // equality will be created instead.
> - static inline llvm::SMTExprRef
> - getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym,
> - const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) {
> + // Wrapper to generate SMTExprRef from a range. If From == To, an equality
> + // will be created instead.
> + static inline SMTExprRef getRangeExpr(SMTSolverRef &Solver, ASTContext &Ctx,
> + SymbolRef Sym, const llvm::APSInt &From,
> + const llvm::APSInt &To, bool InRange) {
> // Convert lower bound
> QualType FromTy;
> llvm::APSInt NewFromInt;
> std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From);
> - llvm::SMTExprRef FromExp =
> + SMTExprRef FromExp =
> Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth());
>
> // Convert symbol
> QualType SymTy;
> - llvm::SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
> + SMTExprRef Exp = getExpr(Solver, Ctx, Sym, &SymTy);
>
> // Construct single (in)equality
> if (From == To)
> @@ -522,17 +509,16 @@ public:
> QualType ToTy;
> llvm::APSInt NewToInt;
> std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To);
> - llvm::SMTExprRef ToExp =
> - Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
> + SMTExprRef ToExp = Solver->mkBitvector(NewToInt, NewToInt.getBitWidth());
> assert(FromTy == ToTy && "Range values have different types!");
>
> // Construct two (in)equalities, and a logical and/or
> - llvm::SMTExprRef LHS =
> + SMTExprRef LHS =
> getBinExpr(Solver, Ctx, Exp, SymTy, InRange ? BO_GE : BO_LT, FromExp,
> FromTy, /*RetTy=*/nullptr);
> - llvm::SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
> - InRange ? BO_LE : BO_GT, ToExp, ToTy,
> - /*RetTy=*/nullptr);
> + SMTExprRef RHS = getBinExpr(Solver, Ctx, Exp, SymTy,
> + InRange ? BO_LE : BO_GT, ToExp, ToTy,
> + /*RetTy=*/nullptr);
>
> return fromBinOp(Solver, LHS, InRange ? BO_LAnd : BO_LOr, RHS,
> SymTy->isSignedIntegerOrEnumerationType());
> @@ -564,24 +550,23 @@ public:
> // Perform implicit type conversion on binary symbolic expressions.
> // May modify all input parameters.
> // TODO: Refactor to use built-in conversion functions
> - static inline void doTypeConversion(llvm::SMTSolverRef &Solver,
> - ASTContext &Ctx, llvm::SMTExprRef &LHS,
> - llvm::SMTExprRef &RHS, QualType <y,
> - QualType &RTy) {
> + static inline void doTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx,
> + SMTExprRef &LHS, SMTExprRef &RHS,
> + QualType <y, QualType &RTy) {
> assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
>
> // Perform type conversion
> if ((LTy->isIntegralOrEnumerationType() &&
> RTy->isIntegralOrEnumerationType()) &&
> (LTy->isArithmeticType() && RTy->isArithmeticType())) {
> - SMTConv::doIntTypeConversion<llvm::SMTExprRef, &fromCast>(
> - Solver, Ctx, LHS, LTy, RHS, RTy);
> + SMTConv::doIntTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, LHS, LTy,
> + RHS, RTy);
> return;
> }
>
> if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
> - SMTConv::doFloatTypeConversion<llvm::SMTExprRef, &fromCast>(
> - Solver, Ctx, LHS, LTy, RHS, RTy);
> + SMTConv::doFloatTypeConversion<SMTExprRef, &fromCast>(Solver, Ctx, LHS,
> + LTy, RHS, RTy);
> return;
> }
>
> @@ -639,11 +624,12 @@ public:
> // Perform implicit integer type conversion.
> // May modify all input parameters.
> // TODO: Refactor to use Sema::handleIntegerConversion()
> - template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
> - QualType, uint64_t, QualType, uint64_t)>
> - static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver,
> - ASTContext &Ctx, T &LHS, QualType <y,
> - T &RHS, QualType &RTy) {
> + template <typename T, T (*doCast)(SMTSolverRef &Solver, const T &, QualType,
> + uint64_t, QualType, uint64_t)>
> + static inline void doIntTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx,
> + T &LHS, QualType <y, T &RHS,
> + QualType &RTy) {
> +
> uint64_t LBitWidth = Ctx.getTypeSize(LTy);
> uint64_t RBitWidth = Ctx.getTypeSize(RTy);
>
> @@ -721,11 +707,12 @@ public:
> // Perform implicit floating-point type conversion.
> // May modify all input parameters.
> // TODO: Refactor to use Sema::handleFloatConversion()
> - template <typename T, T (*doCast)(llvm::SMTSolverRef &Solver, const T &,
> - QualType, uint64_t, QualType, uint64_t)>
> + template <typename T, T (*doCast)(SMTSolverRef &Solver, const T &, QualType,
> + uint64_t, QualType, uint64_t)>
> static inline void
> - doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
> + doFloatTypeConversion(SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,
> QualType <y, T &RHS, QualType &RTy) {
> +
> uint64_t LBitWidth = Ctx.getTypeSize(LTy);
> uint64_t RBitWidth = Ctx.getTypeSize(RTy);
>
> @@ -762,4 +749,4 @@ public:
> } // namespace ento
> } // namespace clang
>
> -#endif
> +#endif
> \ No newline at end of file
>
> Modified: cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_lib_StaticAnalyzer_Core_BugReporterVisitors.cpp-3Frev-3D353590-26r1-3D353589-26r2-3D353590-26view-3Ddiff&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=ik8iEN-OS_2k10ATgZtDntMGJSaHBK5wZaQ9ges53zs&e=
> ==============================================================================
> --- cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (original)
> +++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp Fri Feb 8 16:46:12 2019
> @@ -2411,7 +2411,7 @@ void FalsePositiveRefutationBRVisitor::f
> VisitNode(EndPathNode, BRC, BR);
>
> // Create a refutation manager
> - llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
> + SMTSolverRef RefutationSolver = CreateZ3Solver();
> ASTContext &Ctx = BRC.getASTContext();
>
> // Add constraints to the solver
> @@ -2419,7 +2419,7 @@ void FalsePositiveRefutationBRVisitor::f
> const SymbolRef Sym = I.first;
> auto RangeIt = I.second.begin();
>
> - llvm::SMTExprRef Constraints = SMTConv::getRangeExpr(
> + SMTExprRef Constraints = SMTConv::getRangeExpr(
> RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
> /*InRange=*/true);
> while ((++RangeIt) != I.second.end()) {
>
> Modified: cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_lib_StaticAnalyzer_Core_CMakeLists.txt-3Frev-3D353590-26r1-3D353589-26r2-3D353590-26view-3Ddiff&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=W-BH1ZnPKKh2FJ1B9zcpZgkk-2NQJ9jnTDgE0hnuu-I&e=
> ==============================================================================
> --- cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt (original)
> +++ cfe/trunk/lib/StaticAnalyzer/Core/CMakeLists.txt Fri Feb 8 16:46:12 2019
> @@ -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
> @@ -39,7 +46,6 @@ add_clang_library(clangStaticAnalyzerCor
> SarifDiagnostics.cpp
> SimpleConstraintManager.cpp
> SimpleSValBuilder.cpp
> - SMTConstraintManager.cpp
> Store.cpp
> SubEngine.cpp
> SValBuilder.cpp
> @@ -47,6 +53,7 @@ add_clang_library(clangStaticAnalyzerCor
> SymbolManager.cpp
> TaintManager.cpp
> WorkList.cpp
> + Z3ConstraintManager.cpp
>
> LINK_LIBS
> clangAST
> @@ -56,5 +63,12 @@ add_clang_library(clangStaticAnalyzerCor
> clangCrossTU
> clangLex
> clangRewrite
> + ${Z3_LINK_FILES}
> )
>
> +if(CLANG_ANALYZER_WITH_Z3)
> + target_include_directories(clangStaticAnalyzerCore SYSTEM
> + PRIVATE
> + ${Z3_INCLUDE_DIR}
> + )
> +endif()
>
> Removed: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_lib_StaticAnalyzer_Core_SMTConstraintManager.cpp-3Frev-3D353589-26view-3Dauto&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=G-SBHN2q_V2w5MxEPqlIKIGT-PRkh3rKIRlBKxalYo0&e=
> ==============================================================================
> --- cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp (original)
> +++ cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp (removed)
> @@ -1,18 +0,0 @@
> -//== SMTConstraintManager.cpp -----------------------------------*- C++ -*--==//
> -//
> -// The LLVM Compiler Infrastructure
> -//
> -// This file is distributed under the University of Illinois Open Source
> -// License. See LICENSE.TXT for details.
> -//
> -//===----------------------------------------------------------------------===//
> -
> -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
> -
> -using namespace clang;
> -using namespace ento;
> -
> -std::unique_ptr<ConstraintManager>
> -ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
> - return llvm::make_unique<SMTConstraintManager>(Eng, StMgr.getSValBuilder());
> -}
>
> Added: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_lib_StaticAnalyzer_Core_Z3ConstraintManager.cpp-3Frev-3D353590-26view-3Dauto&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=wHKUfudKIqMNF3gjtBMAesIaRPxlxdcpiknd6s7tRUU&e=
> ==============================================================================
> --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (added)
> +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Fri Feb 8 16:46:12 2019
> @@ -0,0 +1,835 @@
> +//== Z3ConstraintManager.cpp --------------------------------*- C++ -*--==//
> +//
> +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
> +// See https://urldefense.proofpoint.com/v2/url?u=https-3A__llvm.org_LICENSE.txt&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=bor1IHVhMKXiwQcvy9jhYjuptSsoAQm0Yr0eFW3v9sw&e= for license information.
> +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
> +//
> +//===----------------------------------------------------------------------===//
> +
> +#include "clang/Basic/TargetInfo.h"
> +#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
> +#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
> +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
> +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
> +
> +#include "clang/Config/config.h"
> +
> +using namespace clang;
> +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(Context, Error)));
> +}
> +
> +/// Wrapper for Z3 context
> +class Z3Context {
> +public:
> + Z3_context Context;
> +
> + Z3Context() {
> + 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) : 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 &Other) : Context(Other.Context), Sort(Other.Sort) {
> + Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
> + }
> +
> + /// Override implicit copy assignment constructor for correct reference
> + /// counting.
> + Z3Sort &operator=(const Z3Sort &Other) {
> + Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Other.Sort));
> + Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
> + Sort = Other.Sort;
> + return *this;
> + }
> +
> + Z3Sort(Z3Sort &&Other) = delete;
> + Z3Sort &operator=(Z3Sort &&Other) = delete;
> +
> + ~Z3Sort() {
> + if (Sort)
> + Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
> + }
> +
> + void Profile(llvm::FoldingSetNodeID &ID) const {
> + ID.AddInteger(
> + Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort)));
> + }
> +
> + bool isBitvectorSortImpl() const override {
> + return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
> + }
> +
> + bool isFloatSortImpl() const override {
> + return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
> + }
> +
> + bool isBooleanSortImpl() const override {
> + return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);
> + }
> +
> + unsigned getBitvectorSortSizeImpl() const override {
> + return Z3_get_bv_sort_size(Context.Context, Sort);
> + }
> +
> + unsigned getFloatSortSizeImpl() const override {
> + return Z3_fpa_get_ebits(Context.Context, Sort) +
> + Z3_fpa_get_sbits(Context.Context, Sort);
> + }
> +
> + bool equal_to(SMTSort const &Other) const override {
> + return Z3_is_eq_sort(Context.Context, Sort,
> + static_cast<const Z3Sort &>(Other).Sort);
> + }
> +
> + void print(raw_ostream &OS) const override {
> + OS << Z3_sort_to_string(Context.Context, Sort);
> + }
> +}; // end class Z3Sort
> +
> +static const Z3Sort &toZ3Sort(const SMTSort &S) {
> + return static_cast<const Z3Sort &>(S);
> +}
> +
> +class Z3Expr : public SMTExpr {
> + friend class Z3Solver;
> +
> + Z3Context &Context;
> +
> + Z3_ast AST;
> +
> +public:
> + Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
> + Z3_inc_ref(Context.Context, AST);
> + }
> +
> + /// Override implicit copy constructor for correct reference counting.
> + Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
> + Z3_inc_ref(Context.Context, AST);
> + }
> +
> + /// Override implicit copy assignment constructor for correct reference
> + /// counting.
> + Z3Expr &operator=(const Z3Expr &Other) {
> + Z3_inc_ref(Context.Context, Other.AST);
> + Z3_dec_ref(Context.Context, AST);
> + AST = Other.AST;
> + return *this;
> + }
> +
> + Z3Expr(Z3Expr &&Other) = delete;
> + Z3Expr &operator=(Z3Expr &&Other) = delete;
> +
> + ~Z3Expr() {
> + if (AST)
> + Z3_dec_ref(Context.Context, AST);
> + }
> +
> + void Profile(llvm::FoldingSetNodeID &ID) const override {
> + ID.AddInteger(Z3_get_ast_id(Context.Context, AST));
> + }
> +
> + /// Comparison of AST equality, not model equivalence.
> + bool equal_to(SMTExpr const &Other) const override {
> + assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
> + Z3_get_sort(Context.Context,
> + static_cast<const Z3Expr &>(Other).AST)) &&
> + "AST's must have the same sort");
> + return Z3_is_eq_ast(Context.Context, AST,
> + static_cast<const Z3Expr &>(Other).AST);
> + }
> +
> + void print(raw_ostream &OS) const override {
> + OS << Z3_ast_to_string(Context.Context, AST);
> + }
> +}; // end class Z3Expr
> +
> +static const Z3Expr &toZ3Expr(const SMTExpr &E) {
> + return static_cast<const Z3Expr &>(E);
> +}
> +
> +class Z3Model {
> + friend class Z3Solver;
> +
> + Z3Context &Context;
> +
> + Z3_model Model;
> +
> +public:
> + Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) {
> + Z3_model_inc_ref(Context.Context, Model);
> + }
> +
> + Z3Model(const Z3Model &Other) = delete;
> + Z3Model(Z3Model &&Other) = delete;
> + Z3Model &operator=(Z3Model &Other) = delete;
> + Z3Model &operator=(Z3Model &&Other) = delete;
> +
> + ~Z3Model() {
> + if (Model)
> + Z3_model_dec_ref(Context.Context, Model);
> + }
> +
> + void print(raw_ostream &OS) const {
> + OS << Z3_model_to_string(Context.Context, Model);
> + }
> +
> + LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
> +}; // end class Z3Model
> +
> +/// 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();
> + }
> +}
> +
> +// 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));
> +}
> +
> +class Z3Solver : public SMTSolver {
> + friend class Z3ConstraintManager;
> +
> + Z3Context Context;
> +
> + Z3_solver Solver;
> +
> + // Cache Sorts
> + std::set<Z3Sort> CachedSorts;
> +
> + // Cache Exprs
> + std::set<Z3Expr> CachedExprs;
> +
> +public:
> + Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
> + Z3_solver_inc_ref(Context.Context, Solver);
> + }
> +
> + Z3Solver(const Z3Solver &Other) = delete;
> + Z3Solver(Z3Solver &&Other) = delete;
> + Z3Solver &operator=(Z3Solver &Other) = delete;
> + Z3Solver &operator=(Z3Solver &&Other) = delete;
> +
> + ~Z3Solver() {
> + if (Solver)
> + Z3_solver_dec_ref(Context.Context, Solver);
> + }
> +
> + void addConstraint(const SMTExprRef &Exp) const override {
> + Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
> + }
> +
> + // Given an SMTSort, adds/retrives it from the cache and returns
> + // an SMTSortRef to the SMTSort in the cache
> + SMTSortRef newSortRef(const SMTSort &Sort) {
> + auto It = CachedSorts.insert(toZ3Sort(Sort));
> + return &(*It.first);
> + }
> +
> + // Given an SMTExpr, adds/retrives it from the cache and returns
> + // an SMTExprRef to the SMTExpr in the cache
> + SMTExprRef newExprRef(const SMTExpr &Exp) {
> + auto It = CachedExprs.insert(toZ3Expr(Exp));
> + return &(*It.first);
> + }
> +
> + SMTSortRef getBoolSort() override {
> + return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));
> + }
> +
> + SMTSortRef getBitvectorSort(unsigned BitWidth) override {
> + return newSortRef(
> + Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));
> + }
> +
> + SMTSortRef getSort(const SMTExprRef &Exp) override {
> + return newSortRef(
> + Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
> + }
> +
> + SMTSortRef getFloat16Sort() override {
> + return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));
> + }
> +
> + SMTSortRef getFloat32Sort() override {
> + return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));
> + }
> +
> + SMTSortRef getFloat64Sort() override {
> + return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));
> + }
> +
> + SMTSortRef getFloat128Sort() override {
> + return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));
> + }
> +
> + SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
> + }
> +
> + SMTExprRef mkBVNot(const SMTExprRef &Exp) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
> + }
> +
> + SMTExprRef mkNot(const SMTExprRef &Exp) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
> + }
> +
> + SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
> + return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));
> + }
> +
> + SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
> + return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));
> + }
> +
> + SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkFPNeg(const SMTExprRef &Exp) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
> + }
> +
> + SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override {
> + return newExprRef(Z3Expr(
> + Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
> + }
> +
> + SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
> + }
> +
> + SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override {
> + return newExprRef(Z3Expr(
> + Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
> + }
> +
> + SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {
> + return newExprRef(Z3Expr(
> + Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
> + }
> +
> + SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + SMTExprRef RoundingMode = getFloatRoundingMode();
> + return newExprRef(
> + Z3Expr(Context,
> + Z3_mk_fpa_mul(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
> + }
> +
> + SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + SMTExprRef RoundingMode = getFloatRoundingMode();
> + return newExprRef(
> + Z3Expr(Context,
> + Z3_mk_fpa_div(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
> + }
> +
> + SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + SMTExprRef RoundingMode = getFloatRoundingMode();
> + return newExprRef(
> + Z3Expr(Context,
> + Z3_mk_fpa_add(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
> + }
> +
> + SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + SMTExprRef RoundingMode = getFloatRoundingMode();
> + return newExprRef(
> + Z3Expr(Context,
> + Z3_mk_fpa_sub(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST, toZ3Expr(*RoundingMode).AST)));
> + }
> +
> + SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
> + toZ3Expr(*RHS).AST)));
> + }
> +
> + 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 mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {
> + return newExprRef(Z3Expr(
> + Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
> + }
> +
> + SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {
> + return newExprRef(Z3Expr(
> + Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
> + }
> +
> + 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 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(
> + Context,
> + Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
> + toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
> + }
> +
> + SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
> + SMTExprRef RoundingMode = getFloatRoundingMode();
> + return newExprRef(Z3Expr(
> + Context,
> + Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
> + toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
> + }
> +
> + SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
> + SMTExprRef RoundingMode = getFloatRoundingMode();
> + return newExprRef(Z3Expr(
> + Context,
> + Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
> + toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
> + }
> +
> + SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) override {
> + SMTExprRef RoundingMode = getFloatRoundingMode();
> + return newExprRef(Z3Expr(
> + Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
> + toZ3Expr(*From).AST, ToWidth)));
> + }
> +
> + SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) override {
> + SMTExprRef RoundingMode = getFloatRoundingMode();
> + return newExprRef(Z3Expr(
> + Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
> + toZ3Expr(*From).AST, ToWidth)));
> + }
> +
> + SMTExprRef mkBoolean(const bool b) override {
> + return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
> + : Z3_mk_false(Context.Context)));
> + }
> +
> + SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {
> + const SMTSortRef Sort = getBitvectorSort(BitWidth);
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_numeral(Context.Context, Int.toString(10).c_str(),
> + toZ3Sort(*Sort).Sort)));
> + }
> +
> + SMTExprRef mkFloat(const llvm::APFloat Float) override {
> + SMTSortRef Sort =
> + getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
> +
> + llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
> + SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth());
> + return newExprRef(Z3Expr(
> + Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
> + toZ3Sort(*Sort).Sort)));
> + }
> +
> + SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {
> + return newExprRef(
> + Z3Expr(Context, Z3_mk_const(Context.Context,
> + Z3_mk_string_symbol(Context.Context, Name),
> + toZ3Sort(*Sort).Sort)));
> + }
> +
> + llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
> + bool isUnsigned) override {
> + return llvm::APSInt(
> + llvm::APInt(BitWidth,
> + Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
> + 10),
> + isUnsigned);
> + }
> +
> + bool getBoolean(const SMTExprRef &Exp) override {
> + return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
> + }
> +
> + SMTExprRef getFloatRoundingMode() override {
> + // TODO: Don't assume nearest ties to even rounding mode
> + return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
> + }
> +
> + bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
> + llvm::APFloat &Float, bool useSemantics) {
> + assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");
> +
> + llvm::APSInt Int(Sort->getFloatSortSize(), true);
> + const llvm::fltSemantics &Semantics =
> + getFloatSemantics(Sort->getFloatSortSize());
> + SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());
> + if (!toAPSInt(BVSort, AST, Int, true)) {
> + return false;
> + }
> +
> + if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
> + assert(false && "Floating-point types don't match!");
> + return false;
> + }
> +
> + Float = llvm::APFloat(Semantics, Int);
> + return true;
> + }
> +
> + bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,
> + llvm::APSInt &Int, bool useSemantics) {
> + if (Sort->isBitvectorSort()) {
> + if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {
> + assert(false && "Bitvector types don't match!");
> + return false;
> + }
> +
> + // FIXME: This function is also used to retrieve floating-point values,
> + // which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything
> + // between 1 and 64 bits long, which is the reason we have this weird
> + // guard. In the future, we need proper calls in the backend to retrieve
> + // floating-points and its special values (NaN, +/-infinity, +/-zero),
> + // then we can drop this weird condition.
> + if (Sort->getBitvectorSortSize() <= 64 ||
> + Sort->getBitvectorSortSize() == 128) {
> + Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
> + return true;
> + }
> +
> + assert(false && "Bitwidth not supported!");
> + return false;
> + }
> +
> + if (Sort->isBooleanSort()) {
> + if (useSemantics && Int.getBitWidth() < 1) {
> + assert(false && "Boolean type doesn't match!");
> + return false;
> + }
> +
> + Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),
> + Int.isUnsigned());
> + return true;
> + }
> +
> + llvm_unreachable("Unsupported sort to integer!");
> + }
> +
> + bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
> + Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
> + 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);
> + }
> +
> + bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
> + Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
> + 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);
> + }
> +
> + Optional<bool> check() const override {
> + Z3_lbool res = Z3_solver_check(Context.Context, Solver);
> + if (res == Z3_L_TRUE)
> + return true;
> +
> + if (res == Z3_L_FALSE)
> + return false;
> +
> + return Optional<bool>();
> + }
> +
> + void push() override { return Z3_solver_push(Context.Context, Solver); }
> +
> + void pop(unsigned NumStates = 1) override {
> + assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
> + return Z3_solver_pop(Context.Context, Solver, NumStates);
> + }
> +
> + bool isFPSupported() override { return true; }
> +
> + /// Reset the solver and remove all constraints.
> + void reset() override { Z3_solver_reset(Context.Context, Solver); }
> +
> + void print(raw_ostream &OS) const override {
> + OS << Z3_solver_to_string(Context.Context, Solver);
> + }
> +}; // end class Z3Solver
> +
> +} // end anonymous namespace
> +
> +#endif
> +
> +SMTSolverRef clang::ento::CreateZ3Solver() {
> +#if CLANG_ANALYZER_WITH_Z3
> + return llvm::make_unique<Z3Solver>();
> +#else
> + llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
> + "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
> + false);
> + return nullptr;
> +#endif
> +}
> +
> +std::unique_ptr<ConstraintManager>
> +ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
> + return llvm::make_unique<SMTConstraintManager>(Eng, StMgr.getSValBuilder());
> +}
>
> Modified: cfe/trunk/test/CMakeLists.txt
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_test_CMakeLists.txt-3Frev-3D353590-26r1-3D353589-26r2-3D353590-26view-3Ddiff&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=GSC0lSzCKGUA3jmuCO6OrIc9DZkWvuCIT98NfAAnPII&e=
> ==============================================================================
> --- cfe/trunk/test/CMakeLists.txt (original)
> +++ cfe/trunk/test/CMakeLists.txt Fri Feb 8 16:46:12 2019
> @@ -144,7 +144,7 @@ if (CLANG_ENABLE_STATIC_ANALYZER)
> set_target_properties(check-clang-analyzer PROPERTIES FOLDER "Clang tests")
>
>
> - if (LLVM_WITH_Z3)
> + if (CLANG_ANALYZER_WITH_Z3)
> add_lit_testsuite(check-clang-analyzer-z3 "Running the Clang analyzer tests, using Z3 as a solver"
> ${CMAKE_CURRENT_BINARY_DIR}/Analysis
> PARAMS ${ANALYZER_TEST_PARAMS_Z3}
>
> Modified: cfe/trunk/test/lit.site.cfg.py.in
> URL: https://urldefense.proofpoint.com/v2/url?u=http-3A__llvm.org_viewvc_llvm-2Dproject_cfe_trunk_test_lit.site.cfg.py.in-3Frev-3D353590-26r1-3D353589-26r2-3D353590-26view-3Ddiff&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=O29ruiRrk3zXCsAy7B1VA2oLbj3yxp9I7pz4tR37Lto&e=
> ==============================================================================
> --- cfe/trunk/test/lit.site.cfg.py.in (original)
> +++ cfe/trunk/test/lit.site.cfg.py.in Fri Feb 8 16:46:12 2019
> @@ -20,7 +20,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 = "@LLVM_WITH_Z3@"
> +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
> https://urldefense.proofpoint.com/v2/url?u=https-3A__lists.llvm.org_cgi-2Dbin_mailman_listinfo_cfe-2Dcommits&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=XBVzUiFg4mokEqEBsdxVLJgauWIkiXJsXCwZHjM5J9o&e=
_______________________________________________
cfe-commits mailing list
cfe-commits at lists.llvm.org
https://urldefense.proofpoint.com/v2/url?u=https-3A__lists.llvm.org_cgi-2Dbin_mailman_listinfo_cfe-2Dcommits&d=DwIGaQ&c=5VD0RTtNlTh3ycd41b3MUw&r=o3kDXzdBUE3ljQXKeTWOMw&m=aepigNtcB7YIT8UBidW_1L_WrJGW-Zw_5JscfbewUQw&s=XBVzUiFg4mokEqEBsdxVLJgauWIkiXJsXCwZHjM5J9o&e=
More information about the cfe-commits
mailing list