[llvm] r353590 - This reverts commit 1440a848a635849b97f7a5cfa0ecc40d37451f5b.
Mikhail R. Gadelha via llvm-commits
llvm-commits at lists.llvm.org
Fri Feb 8 16:46:12 PST 2019
Author: mramalho
Date: Fri Feb 8 16:46:12 2019
New Revision: 353590
URL: http://llvm.org/viewvc/llvm-project?rev=353590&view=rev
Log:
This reverts commit 1440a848a635849b97f7a5cfa0ecc40d37451f5b.
and commit a1853e834c65751f92521f7481b15cf0365e796b.
They broke arm and aarch64
Removed:
llvm/trunk/cmake/modules/FindZ3.cmake
llvm/trunk/include/llvm/Support/SMTAPI.h
llvm/trunk/lib/Support/Z3Solver.cpp
Modified:
llvm/trunk/CMakeLists.txt
llvm/trunk/cmake/modules/LLVMConfig.cmake.in
llvm/trunk/include/llvm/Config/config.h.cmake
llvm/trunk/lib/Support/CMakeLists.txt
Modified: llvm/trunk/CMakeLists.txt
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/CMakeLists.txt?rev=353590&r1=353589&r2=353590&view=diff
==============================================================================
--- llvm/trunk/CMakeLists.txt (original)
+++ llvm/trunk/CMakeLists.txt Fri Feb 8 16:46:12 2019
@@ -383,32 +383,6 @@ option(LLVM_ENABLE_THREADS "Use threads
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()
Removed: llvm/trunk/cmake/modules/FindZ3.cmake
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/cmake/modules/FindZ3.cmake?rev=353589&view=auto
==============================================================================
--- llvm/trunk/cmake/modules/FindZ3.cmake (original)
+++ llvm/trunk/cmake/modules/FindZ3.cmake (removed)
@@ -1,51 +0,0 @@
-# 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
- )
-
-find_program(Z3_EXECUTABLE z3
- NO_DEFAULT_PATH
- PATHS ${LLVM_Z3_INSTALL_DIR}
- PATH_SUFFIXES 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
- )
-
-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: llvm/trunk/cmake/modules/LLVMConfig.cmake.in
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/cmake/modules/LLVMConfig.cmake.in?rev=353590&r1=353589&r2=353590&view=diff
==============================================================================
--- llvm/trunk/cmake/modules/LLVMConfig.cmake.in (original)
+++ llvm/trunk/cmake/modules/LLVMConfig.cmake.in Fri Feb 8 16:46:12 2019
@@ -44,8 +44,6 @@ 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@)
Modified: llvm/trunk/include/llvm/Config/config.h.cmake
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/include/llvm/Config/config.h.cmake?rev=353590&r1=353589&r2=353590&view=diff
==============================================================================
--- llvm/trunk/include/llvm/Config/config.h.cmake (original)
+++ llvm/trunk/include/llvm/Config/config.h.cmake Fri Feb 8 16:46:12 2019
@@ -347,9 +347,6 @@
/* 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}"
Removed: llvm/trunk/include/llvm/Support/SMTAPI.h
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/include/llvm/Support/SMTAPI.h?rev=353589&view=auto
==============================================================================
--- llvm/trunk/include/llvm/Support/SMTAPI.h (original)
+++ llvm/trunk/include/llvm/Support/SMTAPI.h (removed)
@@ -1,405 +0,0 @@
-//===- 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 <memory>
-
-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;
-
-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;
-
-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;
-
- // 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 llvm
-
-#endif
Modified: llvm/trunk/lib/Support/CMakeLists.txt
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/lib/Support/CMakeLists.txt?rev=353590&r1=353589&r2=353590&view=diff
==============================================================================
--- llvm/trunk/lib/Support/CMakeLists.txt (original)
+++ llvm/trunk/lib/Support/CMakeLists.txt Fri Feb 8 16:46:12 2019
@@ -44,13 +44,6 @@ 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
@@ -158,7 +151,6 @@ add_llvm_library(LLVMSupport
regfree.c
regstrlcpy.c
xxhash.cpp
- Z3Solver.cpp
# System
Atomic.cpp
@@ -184,14 +176,7 @@ 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} ${Z3_LINK_FILES}
+ LINK_LIBS ${system_libs} ${delayload_flags}
)
set_property(TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS "${system_libs}")
-
-if(LLVM_WITH_Z3)
- target_include_directories(LLVMSupport SYSTEM
- PRIVATE
- ${Z3_INCLUDE_DIR}
- )
-endif()
Removed: llvm/trunk/lib/Support/Z3Solver.cpp
URL: http://llvm.org/viewvc/llvm-project/llvm/trunk/lib/Support/Z3Solver.cpp?rev=353589&view=auto
==============================================================================
--- llvm/trunk/lib/Support/Z3Solver.cpp (original)
+++ llvm/trunk/lib/Support/Z3Solver.cpp (removed)
@@ -1,832 +0,0 @@
-//== 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 <set>
-
-using namespace llvm;
-
-#if LLVM_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
-
-llvm::SMTSolverRef llvm::CreateZ3Solver() {
-#if LLVM_WITH_Z3
- return llvm::make_unique<Z3Solver>();
-#else
- llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
- "with -DLLVM_ENABLE_Z3_SOLVER=ON",
- false);
- return nullptr;
-#endif
-}
-
-LLVM_DUMP_METHOD void SMTSort::dump() const { print(llvm::errs()); }
-LLVM_DUMP_METHOD void SMTExpr::dump() const { print(llvm::errs()); }
-LLVM_DUMP_METHOD void SMTSolver::dump() const { print(llvm::errs()); }
-
-
More information about the llvm-commits
mailing list