From 987a6ac4c90d0d87161474256eea9edb18859e9a Mon Sep 17 00:00:00 2001 From: "Mikhail R. Gadelha" Date: Mon, 25 Mar 2019 17:47:45 +0000 Subject: [PATCH] Moved everything SMT-related to LLVM and updated the cmake scripts. Differential Revision: https://reviews.llvm.org/D54978 git-svn-id: https://llvm.org/svn/llvm-project/llvm/trunk@356929 91177308-0d34-0410-b5e6-96231b3b80d8 --- CMakeLists.txt | 25 + cmake/modules/FindZ3.cmake | 110 ++++ cmake/modules/LLVMConfig.cmake.in | 2 + include/llvm/Config/config.h.cmake | 3 + include/llvm/Support/SMTAPI.h | 405 ++++++++++++++ lib/Support/CMakeLists.txt | 17 +- lib/Support/Z3Solver.cpp | 826 +++++++++++++++++++++++++++++ 7 files changed, 1387 insertions(+), 1 deletion(-) create mode 100644 cmake/modules/FindZ3.cmake create mode 100644 include/llvm/Support/SMTAPI.h create mode 100644 lib/Support/Z3Solver.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 4028096d030..80ca9128975 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -377,6 +377,31 @@ option(LLVM_ENABLE_THREADS "Use threads if available." ON) option(LLVM_ENABLE_ZLIB "Use zlib for compression/decompression if available." ON) +set(LLVM_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.") + +find_package(Z3 4.7.1) + +if (LLVM_Z3_INSTALL_DIR) + if (NOT Z3_FOUND) + message(FATAL_ERROR "Z3 >= 4.7.1 has not been found in LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.") + endif() +endif() + +set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}") + +option(LLVM_ENABLE_Z3_SOLVER + "Enable Support for the Z3 constraint solver in LLVM." + ${LLVM_ENABLE_Z3_SOLVER_DEFAULT} +) + +if (LLVM_ENABLE_Z3_SOLVER) + if (NOT Z3_FOUND) + message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.") + endif() + + set(LLVM_WITH_Z3 1) +endif() + if( LLVM_TARGETS_TO_BUILD STREQUAL "all" ) set( LLVM_TARGETS_TO_BUILD ${LLVM_ALL_TARGETS} ) endif() diff --git a/cmake/modules/FindZ3.cmake b/cmake/modules/FindZ3.cmake new file mode 100644 index 00000000000..04294275535 --- /dev/null +++ b/cmake/modules/FindZ3.cmake @@ -0,0 +1,110 @@ +INCLUDE(CheckCXXSourceRuns) + +# Function to check Z3's version +function(check_z3_version z3_include z3_lib) + # The program that will be executed to print Z3's version. + file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c + "#include + #include + int main() { + unsigned int major, minor, build, rev; + Z3_get_version(&major, &minor, &build, &rev); + printf(\"%u.%u.%u\", major, minor, build); + return 0; + }") + + # Get lib path + get_filename_component(z3_lib_path ${z3_lib} PATH) + + try_run( + Z3_RETURNCODE + Z3_COMPILED + ${CMAKE_BINARY_DIR} + ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c + COMPILE_DEFINITIONS -I"${z3_include}" + LINK_LIBRARIES -L${z3_lib_path} -lz3 + RUN_OUTPUT_VARIABLE SRC_OUTPUT + ) + + if(Z3_COMPILED) + string(REGEX REPLACE "([0-9]*\\.[0-9]*\\.[0-9]*\\.[0-9]*)" "\\1" + z3_version "${SRC_OUTPUT}") + set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE) + endif() +endfunction(check_z3_version) + +# Looking for Z3 in LLVM_Z3_INSTALL_DIR +find_path(Z3_INCLUDE_DIR NAMES z3.h + NO_DEFAULT_PATH + PATHS ${LLVM_Z3_INSTALL_DIR}/include + PATH_SUFFIXES libz3 z3 + ) + +find_library(Z3_LIBRARIES NAMES z3 libz3 + NO_DEFAULT_PATH + PATHS ${LLVM_Z3_INSTALL_DIR} + PATH_SUFFIXES lib bin + ) + +# If Z3 has not been found in LLVM_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 + ) + +# Searching for the version of the Z3 library is a best-effort task +unset(Z3_VERSION_STRING) + +# First, try to check it dynamically, by compiling a small program that +# prints Z3's version +if(Z3_INCLUDE_DIR AND Z3_LIBRARIES) + # We do not have the Z3 binary to query for a version. Try to use + # a small C++ program to detect it via the Z3_get_version() API call. + check_z3_version(${Z3_INCLUDE_DIR} ${Z3_LIBRARIES}) +endif() + +# If the dynamic check fails, we might be cross compiling: if that's the case, +# check the version in the headers, otherwise, fail with a message +if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND + Z3_INCLUDE_DIR AND + EXISTS "${Z3_INCLUDE_DIR}/z3_version.h")) + # TODO: print message warning that we couldn't find a compatible lib? + + # Z3 4.8.1+ has the version is in a public header. + file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h" + z3_version_str REGEX "^#define[\t ]+Z3_MAJOR_VERSION[\t ]+.*") + string(REGEX REPLACE "^.*Z3_MAJOR_VERSION[\t ]+([0-9]).*$" "\\1" + Z3_MAJOR "${z3_version_str}") + + file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h" + z3_version_str REGEX "^#define[\t ]+Z3_MINOR_VERSION[\t ]+.*") + string(REGEX REPLACE "^.*Z3_MINOR_VERSION[\t ]+([0-9]).*$" "\\1" + Z3_MINOR "${z3_version_str}") + + file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h" + z3_version_str REGEX "^#define[\t ]+Z3_BUILD_NUMBER[\t ]+.*") + string(REGEX REPLACE "^.*Z3_BUILD_VERSION[\t ]+([0-9]).*$" "\\1" + Z3_BUILD "${z3_version_str}") + + set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD}) + unset(z3_version_str) +endif() + +if(NOT Z3_VERSION_STRING) + # Give up: we are unable to obtain a version of the Z3 library. Be + # conservative and force the found version to 0.0.0 to make version + # checks always fail. + set(Z3_VERSION_STRING "0.0.0") +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) diff --git a/cmake/modules/LLVMConfig.cmake.in b/cmake/modules/LLVMConfig.cmake.in index c3c3af37f62..df97c723efa 100644 --- a/cmake/modules/LLVMConfig.cmake.in +++ b/cmake/modules/LLVMConfig.cmake.in @@ -44,6 +44,8 @@ set(LLVM_ENABLE_ZLIB @LLVM_ENABLE_ZLIB@) set(LLVM_LIBXML2_ENABLED @LLVM_LIBXML2_ENABLED@) +set(LLVM_WITH_Z3 @LLVM_WITH_Z3@) + set(LLVM_ENABLE_DIA_SDK @LLVM_ENABLE_DIA_SDK@) set(LLVM_NATIVE_ARCH @LLVM_NATIVE_ARCH@) diff --git a/include/llvm/Config/config.h.cmake b/include/llvm/Config/config.h.cmake index e30cb8a8ac2..1a38bc15ab9 100644 --- a/include/llvm/Config/config.h.cmake +++ b/include/llvm/Config/config.h.cmake @@ -344,6 +344,9 @@ /* Whether GlobalISel rule coverage is being collected */ #cmakedefine01 LLVM_GISEL_COV_ENABLED +/* Define if we have z3 and want to build it */ +#cmakedefine LLVM_WITH_Z3 ${LLVM_WITH_Z3} + /* Define to the default GlobalISel coverage file prefix */ #cmakedefine LLVM_GISEL_COV_PREFIX "${LLVM_GISEL_COV_PREFIX}" diff --git a/include/llvm/Support/SMTAPI.h b/include/llvm/Support/SMTAPI.h new file mode 100644 index 00000000000..418c251d5ac --- /dev/null +++ b/include/llvm/Support/SMTAPI.h @@ -0,0 +1,405 @@ +//===- SMTAPI.h -------------------------------------------------*- C++ -*-===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt 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_SUPPORT_SMTAPI_H +#define LLVM_SUPPORT_SMTAPI_H + +#include "llvm/ADT/APFloat.h" +#include "llvm/ADT/APSInt.h" +#include "llvm/ADT/FoldingSet.h" +#include "llvm/Support/raw_ostream.h" +#include + +namespace llvm { + +/// 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 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; + +/// Convenience method to create and Z3Solver object +SMTSolverRef CreateZ3Solver(); + +} // namespace llvm + +#endif diff --git a/lib/Support/CMakeLists.txt b/lib/Support/CMakeLists.txt index 234db82a0c2..b5246b27ca1 100644 --- a/lib/Support/CMakeLists.txt +++ b/lib/Support/CMakeLists.txt @@ -44,6 +44,13 @@ if (MSVC) set (delayload_flags delayimp -delayload:shell32.dll -delayload:ole32.dll) endif() +# Link Z3 if the user wants to build it. +if(LLVM_WITH_Z3) + set(Z3_LINK_FILES ${Z3_LIBRARIES}) +else() + set(Z3_LINK_FILES "") +endif() + add_llvm_library(LLVMSupport AArch64TargetParser.cpp ARMTargetParser.cpp @@ -152,6 +159,7 @@ add_llvm_library(LLVMSupport regfree.c regstrlcpy.c xxhash.cpp + Z3Solver.cpp # System Atomic.cpp @@ -177,7 +185,14 @@ add_llvm_library(LLVMSupport ${LLVM_MAIN_INCLUDE_DIR}/llvm/ADT ${LLVM_MAIN_INCLUDE_DIR}/llvm/Support ${Backtrace_INCLUDE_DIRS} - LINK_LIBS ${system_libs} ${delayload_flags} + LINK_LIBS ${system_libs} ${delayload_flags} ${Z3_LINK_FILES} ) set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}") + +if(LLVM_WITH_Z3) + target_include_directories(LLVMSupport SYSTEM + PRIVATE + ${Z3_INCLUDE_DIR} + ) +endif() diff --git a/lib/Support/Z3Solver.cpp b/lib/Support/Z3Solver.cpp new file mode 100644 index 00000000000..a8374522bda --- /dev/null +++ b/lib/Support/Z3Solver.cpp @@ -0,0 +1,826 @@ +//== Z3Solver.cpp -----------------------------------------------*- C++ -*--==// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// + +#include "llvm/ADT/Twine.h" +#include "llvm/Config/config.h" +#include "llvm/Support/SMTAPI.h" +#include + +using namespace llvm; + +#if LLVM_WITH_Z3 + +#include + +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(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(Sort)); + } + + /// Override implicit copy assignment constructor for correct reference + /// counting. + Z3Sort &operator=(const Z3Sort &Other) { + Z3_inc_ref(Context.Context, reinterpret_cast(Other.Sort)); + Z3_dec_ref(Context.Context, reinterpret_cast(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(Sort)); + } + + void Profile(llvm::FoldingSetNodeID &ID) const override { + ID.AddInteger( + Z3_get_ast_id(Context.Context, reinterpret_cast(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(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(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(Other).AST)) && + "AST's must have the same sort"); + return Z3_is_eq_ast(Context.Context, AST, + static_cast(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(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 CachedSorts; + + // Cache Exprs + std::set 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 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(); + } + + 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 + +llvm::SMTSolverRef llvm::CreateZ3Solver() { +#if LLVM_WITH_Z3 + return llvm::make_unique(); +#else + llvm::report_fatal_error("LLVM was not compiled with Z3 support, rebuild " + "with -DLLVM_ENABLE_Z3_SOLVER=ON", + false); + return nullptr; +#endif +} -- 2.50.1