From fa6cc19184f564b819b925aa22aa4fe9451f8321 Mon Sep 17 00:00:00 2001 From: Andrew Dutcher Date: Wed, 14 Sep 2016 01:33:07 -0700 Subject: [PATCH 1/8] Moved python bindings into package --- scripts/update_api.py | 4 ++-- src/api/python/z3/__init__.py | 10 ++++++++++ src/api/python/{ => z3}/z3.py | 8 ++++---- src/api/python/{ => z3}/z3num.py | 6 +++--- src/api/python/{ => z3}/z3poly.py | 2 +- src/api/python/{ => z3}/z3printer.py | 4 ++-- src/api/python/{ => z3}/z3rcf.py | 6 +++--- src/api/python/{ => z3}/z3types.py | 2 +- src/api/python/{ => z3}/z3util.py | 2 +- 9 files changed, 27 insertions(+), 17 deletions(-) create mode 100644 src/api/python/z3/__init__.py rename src/api/python/{ => z3}/z3.py (99%) rename src/api/python/{ => z3}/z3num.py (99%) rename src/api/python/{ => z3}/z3poly.py (98%) rename src/api/python/{ => z3}/z3printer.py (99%) rename src/api/python/{ => z3}/z3rcf.py (98%) rename src/api/python/{ => z3}/z3types.py (99%) rename src/api/python/{ => z3}/z3util.py (99%) diff --git a/scripts/update_api.py b/scripts/update_api.py index 733d5b1fa..5295b19b1 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1600,8 +1600,8 @@ def write_core_py_preamble(core_py): core_py.write('# Automatically generated file\n') core_py.write('import sys, os\n') core_py.write('import ctypes\n') - core_py.write('from z3types import *\n') - core_py.write('from z3consts import *\n') + core_py.write('from .z3types import *\n') + core_py.write('from .z3consts import *\n') core_py.write( """ _lib = None diff --git a/src/api/python/z3/__init__.py b/src/api/python/z3/__init__.py new file mode 100644 index 000000000..c4f08371f --- /dev/null +++ b/src/api/python/z3/__init__.py @@ -0,0 +1,10 @@ +from .z3 import * + +from . import z3core +from . import z3num +from . import z3poly +from . import z3printer +from . import z3rcf +from . import z3types +from . import z3util +from . import z3consts diff --git a/src/api/python/z3.py b/src/api/python/z3/z3.py similarity index 99% rename from src/api/python/z3.py rename to src/api/python/z3/z3.py index 83e9eaae9..d7571a3c7 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3/z3.py @@ -41,10 +41,10 @@ Z3 exceptions: ... print("failed: %s" % ex) failed: sort mismatch """ -from z3core import * -from z3types import * -from z3consts import * -from z3printer import * +from .z3core import * +from .z3types import * +from .z3consts import * +from .z3printer import * from fractions import Fraction import sys import io diff --git a/src/api/python/z3num.py b/src/api/python/z3/z3num.py similarity index 99% rename from src/api/python/z3num.py rename to src/api/python/z3/z3num.py index b219829d3..14d8550e6 100644 --- a/src/api/python/z3num.py +++ b/src/api/python/z3/z3num.py @@ -5,9 +5,9 @@ # # Author: Leonardo de Moura (leonardo) ############################################ -from z3 import * -from z3core import * -from z3printer import * +from .z3 import * +from .z3core import * +from .z3printer import * from fractions import Fraction def _to_numeral(num, ctx=None): diff --git a/src/api/python/z3poly.py b/src/api/python/z3/z3poly.py similarity index 98% rename from src/api/python/z3poly.py rename to src/api/python/z3/z3poly.py index 0b8bf9457..4a5cac46c 100644 --- a/src/api/python/z3poly.py +++ b/src/api/python/z3/z3poly.py @@ -5,7 +5,7 @@ # # Author: Leonardo de Moura (leonardo) ############################################ -from z3 import * +from .z3 import * def subresultants(p, q, x): """ diff --git a/src/api/python/z3printer.py b/src/api/python/z3/z3printer.py similarity index 99% rename from src/api/python/z3printer.py rename to src/api/python/z3/z3printer.py index c8d69900a..e02c28a96 100644 --- a/src/api/python/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -6,8 +6,8 @@ # Author: Leonardo de Moura (leonardo) ############################################ import sys, io, z3 -from z3consts import * -from z3core import * +from .z3consts import * +from .z3core import * from ctypes import * ############################## diff --git a/src/api/python/z3rcf.py b/src/api/python/z3/z3rcf.py similarity index 98% rename from src/api/python/z3rcf.py rename to src/api/python/z3/z3rcf.py index 84c724910..9d6f2f6ad 100644 --- a/src/api/python/z3rcf.py +++ b/src/api/python/z3/z3rcf.py @@ -9,9 +9,9 @@ # # Author: Leonardo de Moura (leonardo) ############################################ -from z3 import * -from z3core import * -from z3printer import * +from .z3 import * +from .z3core import * +from .z3printer import * from fractions import Fraction def _to_rcfnum(num, ctx=None): diff --git a/src/api/python/z3types.py b/src/api/python/z3/z3types.py similarity index 99% rename from src/api/python/z3types.py rename to src/api/python/z3/z3types.py index 44b19d33a..8b585e0ee 100644 --- a/src/api/python/z3types.py +++ b/src/api/python/z3/z3types.py @@ -6,7 +6,7 @@ # Author: Leonardo de Moura (leonardo) ############################################ -import ctypes, z3core +import ctypes class Z3Exception(Exception): def __init__(self, value): diff --git a/src/api/python/z3util.py b/src/api/python/z3/z3util.py similarity index 99% rename from src/api/python/z3util.py rename to src/api/python/z3/z3util.py index 2494461cf..fe7e76b86 100644 --- a/src/api/python/z3util.py +++ b/src/api/python/z3/z3util.py @@ -11,7 +11,7 @@ Usage: import common_z3 as CM_Z3 """ -from z3 import * +from .z3 import * def vset(seq, idfun=None, as_list=True): # This functions preserves the order of arguments while removing duplicates. From 0bbd172af3693165ab7a3e9f16cf4268edbed703 Mon Sep 17 00:00:00 2001 From: Andrew Dutcher Date: Thu, 25 Aug 2016 19:25:12 -0500 Subject: [PATCH 2/8] First steps to a sane python build --- .gitignore | 4 +- contrib/cmake/src/api/python/CMakeLists.txt | 11 ++- scripts/mk_genfile_common.py | 2 +- scripts/mk_util.py | 17 ++-- scripts/update_api.py | 2 +- src/api/python/setup.py | 88 +++++++++++++++++++++ src/api/python/z3/__init__.py | 4 +- src/api/python/z3/z3poly.py | 4 +- src/api/python/z3/z3types.py | 1 - 9 files changed, 110 insertions(+), 23 deletions(-) create mode 100644 src/api/python/setup.py diff --git a/.gitignore b/.gitignore index fcff2132d..cc1c2a754 100644 --- a/.gitignore +++ b/.gitignore @@ -59,8 +59,8 @@ src/api/dotnet/Enumerations.cs src/api/dotnet/Native.cs src/api/dotnet/Properties/AssemblyInfo.cs src/api/dotnet/Microsoft.Z3.xml -src/api/python/z3consts.py -src/api/python/z3core.py +src/api/python/z3/z3consts.py +src/api/python/z3/z3core.py src/ast/pattern/database.h src/util/version.h src/api/java/Native.cpp diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/contrib/cmake/src/api/python/CMakeLists.txt index 555333c9f..6babb2069 100644 --- a/contrib/cmake/src/api/python/CMakeLists.txt +++ b/contrib/cmake/src/api/python/CMakeLists.txt @@ -9,7 +9,6 @@ set(z3py_files z3poly.py z3printer.py z3rcf.py - z3test.py z3types.py z3util.py ) @@ -18,12 +17,12 @@ set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}") set(build_z3_python_bindings_target_depends "") foreach (z3py_file ${z3py_files}) - add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${z3py_file}" + add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/${z3py_file}" COMMAND "${CMAKE_COMMAND}" "-E" "copy" - "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}" - "${z3py_bindings_build_dest}" - DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}" - COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}" + "${CMAKE_CURRENT_SOURCE_DIR}/z3/${z3py_file}" + "${z3py_bindings_build_dest}/z3.py" + DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/z3/${z3py_file}" + COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}/z3.py/${z3py_file}" ) list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/${z3py_file}") endforeach() diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index cbeb8a82d..2ecb06776 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -98,7 +98,7 @@ def mk_z3consts_py_internal(api_files, output_dir): openbrace_pat = re.compile("{ *") closebrace_pat = re.compile("}.*;") - z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w') + z3consts = open(os.path.join(output_dir, 'z3/z3consts.py'), 'w') z3consts_output_path = z3consts.name z3consts.write('# Automatically generated file\n\n') for api_file in api_files: diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 66191e160..0d1555e5b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2737,6 +2737,8 @@ def mk_def_files(): def cp_z3py_to_build(): mk_dir(BUILD_DIR) + z3py_dest = os.path.join(BUILD_DIR, 'z3.py') + z3py_src = os.path.join(Z3PY_SRC_DIR, 'z3') # Erase existing .pyc files for root, dirs, files in os.walk(Z3PY_SRC_DIR): for f in files: @@ -2746,20 +2748,19 @@ def cp_z3py_to_build(): if compileall.compile_dir(Z3PY_SRC_DIR, force=1) != 1: raise MKException("failed to compile Z3Py sources") # Copy sources to build - for py in filter(lambda f: f.endswith('.py'), os.listdir(Z3PY_SRC_DIR)): - shutil.copyfile(os.path.join(Z3PY_SRC_DIR, py), os.path.join(BUILD_DIR, py)) - if is_verbose(): - print("Copied '%s'" % py) + shutil.copytree(z3py_src, z3py_dest) + if is_verbose(): + print("Copied python bindings") # Python 2.x support - for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(Z3PY_SRC_DIR)): - shutil.copyfile(os.path.join(Z3PY_SRC_DIR, pyc), os.path.join(BUILD_DIR, pyc)) + for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(z3py_src)): + shutil.copyfile(os.path.join(z3py_src, pyc), os.path.join(z3py_dest, pyc)) if is_verbose(): print("Generated '%s'" % pyc) # Python 3.x support - src_pycache = os.path.join(Z3PY_SRC_DIR, '__pycache__') + src_pycache = os.path.join(z3py_src, '__pycache__') if os.path.exists(src_pycache): for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(src_pycache)): - target_pycache = os.path.join(BUILD_DIR, '__pycache__') + target_pycache = os.path.join(z3py_dest, '__pycache__') mk_dir(target_pycache) shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc)) if is_verbose(): diff --git a/scripts/update_api.py b/scripts/update_api.py index 5295b19b1..047564cde 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1706,7 +1706,7 @@ def generate_files(api_files, with mk_file_or_temp(api_output_dir, 'api_log_macros.h') as log_h: with mk_file_or_temp(api_output_dir, 'api_log_macros.cpp') as log_c: with mk_file_or_temp(api_output_dir, 'api_commands.cpp') as exe_c: - with mk_file_or_temp(z3py_output_dir, 'z3core.py') as core_py: + with mk_file_or_temp(z3py_output_dir, 'z3/z3core.py') as core_py: # Write preambles write_log_h_preamble(log_h) write_log_c_preamble(log_c) diff --git a/src/api/python/setup.py b/src/api/python/setup.py new file mode 100644 index 000000000..9d17f431f --- /dev/null +++ b/src/api/python/setup.py @@ -0,0 +1,88 @@ +import os +import sys +import platform +import subprocess +import multiprocessing +from setuptools import setup +from distutils.errors import LibError +from distutils.command.build import build as _build +from setuptools.command.develop import develop as _develop + + +build_env = dict(os.environ) +build_env['PYTHON'] = sys.executable +build_env['CXXFLAGS'] = "-std=c++11" + +build_dir = os.path.abspath(os.path.dirname(__file__)) + +if sys.platform == 'darwin': + library_file = "libz3.dylib" +elif sys.platform == 'win32': + library_file = "libz3.dll" +else: + library_file = "libz3.so" + +def _configure_z3(): + if sys.platform == 'win32': + args = [sys.executable, os.path.join(build_dir, 'scripts', + 'mk_make.py')] + if platform.architecture()[0] == '64bit': + args += ['-x'] + + if subprocess.call(args, env=build_env, cwd=build_dir) != 0: + raise LibError("Unable to configure Z3.") + else: # linux and osx + if subprocess.call([os.path.join(build_dir, 'configure')], + env=build_env, cwd=build_dir) != 0: + raise LibError("Unable to configure Z3.") + +def _build_z3(): + if sys.platform == 'win32': + if subprocess.call(['nmake'], env=build_env, + cwd=os.path.join(build_dir, 'build')) != 0: + raise LibError("Unable to build Z3.") + else: # linux and osx + if subprocess.call(['make', '-C', os.path.join(build_dir, 'build'), + '-j', str(multiprocessing.cpu_count())], + env=build_env, cwd=build_dir) != 0: + raise LibError("Unable to build Z3.") + +class build(_build): + def run(self): + self.execute(_configure_z3, (), msg="Configuring Z3") + self.execute(_build_z3, (), msg="Building Z3") + +class develop(_develop): + def run(self): + self.execute(_configure_z3, (), msg="Configuring Z3") + self.execute(_build_z3, (), msg="Building Z3") + +# the build directory needs to exist +try: os.makedirs(os.path.join(build_dir, 'build')) +except OSError: pass + +setup( + name='angr-only-z3-custom', + version='4.4.1.post4', + description='pip installable distribution of The Z3 Theorem Prover, for use with angr. Please send all support requests to angr@lists.cs.ucsb.edu!', + long_description='Z3 is a theorem prover from Microsoft Research. This version is slightly modified by the angr project to enable installation via pip, making it unsupportable by the Z3 project. Please direct all support requests to angr@lists.cs.ucsb.edu!', + author="The Z3 Theorem Prover Project", + maintainer="Yan Shoshitaishvili", + maintainer_email="yans@yancomm.net", + url='https://github.com/angr/angr-z3', + license='MIT License', + keywords=['z3', 'smt', 'sat', 'prover', 'theorem'], + package_dir={'': 'build'}, + packages=[''], + data_files=[ + ('lib', (os.path.join(build_dir, 'build', library_file),)), + ('include', tuple(os.path.join(build_dir, f) for f in ('src/api/z3.h', + 'src/api/z3_v1.h', 'src/api/z3_macros.h', + 'src/api/z3_api.h', 'src/api/z3_algebraic.h', + 'src/api/z3_polynomial.h', 'src/api/z3_rcf.h', + 'src/api/z3_interp.h', 'src/api/z3_fpa.h', + 'src/api/c++/z3++.h') )), + ], + #scripts=[os.path.join(build_dir, 'build', 'z3')] if sys.version_info[0] == 2 else [], + cmdclass={'build': build, 'develop': develop}, +) diff --git a/src/api/python/z3/__init__.py b/src/api/python/z3/__init__.py index c4f08371f..f7aa29ab1 100644 --- a/src/api/python/z3/__init__.py +++ b/src/api/python/z3/__init__.py @@ -1,10 +1,12 @@ from .z3 import * -from . import z3core from . import z3num from . import z3poly from . import z3printer from . import z3rcf from . import z3types from . import z3util + +# generated files +from . import z3core from . import z3consts diff --git a/src/api/python/z3/z3poly.py b/src/api/python/z3/z3poly.py index 4a5cac46c..169944291 100644 --- a/src/api/python/z3/z3poly.py +++ b/src/api/python/z3/z3poly.py @@ -5,6 +5,7 @@ # # Author: Leonardo de Moura (leonardo) ############################################ + from .z3 import * def subresultants(p, q, x): @@ -32,6 +33,3 @@ if __name__ == "__main__": import doctest if doctest.testmod().failed: exit(1) - - - diff --git a/src/api/python/z3/z3types.py b/src/api/python/z3/z3types.py index 8b585e0ee..7cf61f49e 100644 --- a/src/api/python/z3/z3types.py +++ b/src/api/python/z3/z3types.py @@ -121,4 +121,3 @@ class FuncEntryObj(ctypes.c_void_p): class RCFNumObj(ctypes.c_void_p): def __init__(self, e): self._as_parameter_ = e def from_param(obj): return obj - From 704105306c013cb1d30ff9edb8e8943e8a782496 Mon Sep 17 00:00:00 2001 From: Andrew Dutcher Date: Sat, 27 Aug 2016 19:36:53 -0500 Subject: [PATCH 3/8] FINISH IT --- scripts/mk_util.py | 1 + scripts/update_api.py | 7 +- src/api/python/.gitignore | 7 ++ src/api/python/MANIFEST.in | 4 ++ src/api/python/setup.py | 135 +++++++++++++++++++++++++++---------- 5 files changed, 116 insertions(+), 38 deletions(-) create mode 100644 src/api/python/.gitignore create mode 100644 src/api/python/MANIFEST.in diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0d1555e5b..0d2b23a3e 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2748,6 +2748,7 @@ def cp_z3py_to_build(): if compileall.compile_dir(Z3PY_SRC_DIR, force=1) != 1: raise MKException("failed to compile Z3Py sources") # Copy sources to build + shutil.rmtree(z3py_dest, ignore_errors=True) shutil.copytree(z3py_src, z3py_dest) if is_verbose(): print("Copied python bindings") diff --git a/scripts/update_api.py b/scripts/update_api.py index 047564cde..1f0ae4e4c 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1600,6 +1600,7 @@ def write_core_py_preamble(core_py): core_py.write('# Automatically generated file\n') core_py.write('import sys, os\n') core_py.write('import ctypes\n') + core_py.write('import pkg_resources\n') core_py.write('from .z3types import *\n') core_py.write('from .z3consts import *\n') core_py.write( @@ -1608,15 +1609,15 @@ _lib = None def lib(): global _lib if _lib == None: - _dir = os.path.dirname(os.path.abspath(__file__)) + _dir = pkg_resources.resource_filename('z3', 'lib') for ext in ['dll', 'so', 'dylib']: try: - init('libz3.%s' % ext) + init(os.path.join(_dir, 'libz3.%s' % ext)) break except: pass try: - init(os.path.join(_dir, 'libz3.%s' % ext)) + init('libz3.%s' % ext) break except: pass diff --git a/src/api/python/.gitignore b/src/api/python/.gitignore new file mode 100644 index 000000000..a0a01631f --- /dev/null +++ b/src/api/python/.gitignore @@ -0,0 +1,7 @@ +MANIFEST +dist +core +build +*.egg-info +bin +z3/lib diff --git a/src/api/python/MANIFEST.in b/src/api/python/MANIFEST.in new file mode 100644 index 000000000..209e0cfa3 --- /dev/null +++ b/src/api/python/MANIFEST.in @@ -0,0 +1,4 @@ +include core/LICENSE.txt +recursive-include core/src * +recursive-include core/scripts * +recursive-include core/examples * diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 9d17f431f..6ccd45c60 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -1,65 +1,135 @@ import os import sys +import shutil import platform import subprocess import multiprocessing from setuptools import setup from distutils.errors import LibError from distutils.command.build import build as _build +from distutils.command.sdist import sdist as _sdist from setuptools.command.develop import develop as _develop +from setuptools.command.bdist_egg import bdist_egg as _bdist_egg build_env = dict(os.environ) build_env['PYTHON'] = sys.executable build_env['CXXFLAGS'] = "-std=c++11" -build_dir = os.path.abspath(os.path.dirname(__file__)) +ROOT_DIR = os.path.abspath(os.path.dirname(__file__)) +SRC_DIR_LOCAL = os.path.join(ROOT_DIR, 'core') +SRC_DIR_REPO = os.path.join(ROOT_DIR, '../../..') +SRC_DIR = SRC_DIR_LOCAL if os.path.exists(SRC_DIR_LOCAL) else SRC_DIR_REPO +BUILD_DIR = os.path.join(SRC_DIR, 'build') # implicit in configure script +LIBS_DIR = os.path.join(ROOT_DIR, 'z3', 'lib') +HEADERS_DIR = os.path.join(ROOT_DIR, 'z3', 'include') +BINS_DIR = os.path.join(ROOT_DIR, 'bin') if sys.platform == 'darwin': - library_file = "libz3.dylib" -elif sys.platform == 'win32': - library_file = "libz3.dll" + LIBRARY_FILE = "libz3.dylib" +elif sys.platform in ('win32', 'cygwin'): + LIBRARY_FILE = "libz3.dll" else: - library_file = "libz3.so" + LIBRARY_FILE = "libz3.so" + +def _clean_bins(): + """ + Clean up the binary files and headers that are installed along with the bindings + """ + shutil.rmtree(LIBS_DIR, ignore_errors=True) + shutil.rmtree(BINS_DIR, ignore_errors=True) + shutil.rmtree(HEADERS_DIR, ignore_errors=True) def _configure_z3(): - if sys.platform == 'win32': - args = [sys.executable, os.path.join(build_dir, 'scripts', - 'mk_make.py')] - if platform.architecture()[0] == '64bit': - args += ['-x'] + args = [sys.executable, os.path.join(SRC_DIR, 'scripts', 'mk_make.py')] - if subprocess.call(args, env=build_env, cwd=build_dir) != 0: - raise LibError("Unable to configure Z3.") - else: # linux and osx - if subprocess.call([os.path.join(build_dir, 'configure')], - env=build_env, cwd=build_dir) != 0: - raise LibError("Unable to configure Z3.") + if sys.platform == 'win32' and platform.architecture()[0] == '64bit': + args += ['-x'] + + if subprocess.call(args, env=build_env, cwd=SRC_DIR) != 0: + raise LibError("Unable to configure Z3.") def _build_z3(): if sys.platform == 'win32': if subprocess.call(['nmake'], env=build_env, - cwd=os.path.join(build_dir, 'build')) != 0: + cwd=BUILD_DIR) != 0: raise LibError("Unable to build Z3.") else: # linux and osx - if subprocess.call(['make', '-C', os.path.join(build_dir, 'build'), - '-j', str(multiprocessing.cpu_count())], - env=build_env, cwd=build_dir) != 0: + if subprocess.call(['make', '-j', str(multiprocessing.cpu_count())], + env=build_env, cwd=BUILD_DIR) != 0: raise LibError("Unable to build Z3.") +def _copy_bins(): + """ + Copy the library and header files into their final destinations + """ + # STEP 1: If we're performing a build from a copied source tree, + # copy the generated python files into the package + + _clean_bins() + + if SRC_DIR == SRC_DIR_LOCAL: + shutil.copy(os.path.join(SRC_DIR, 'src/api/python/z3/z3core.py'), os.path.join(ROOT_DIR, 'z3')) + shutil.copy(os.path.join(SRC_DIR, 'src/api/python/z3/z3consts.py'), os.path.join(ROOT_DIR, 'z3')) + + # STEP 2: Copy the shared library, the executable and the headers + + os.mkdir(LIBS_DIR) + os.mkdir(BINS_DIR) + os.mkdir(HEADERS_DIR) + os.mkdir(os.path.join(HEADERS_DIR, 'c++')) + shutil.copy(os.path.join(BUILD_DIR, 'libz3.so'), LIBS_DIR) + shutil.copy(os.path.join(BUILD_DIR, 'z3'), BINS_DIR) + for fname in ('z3.h', 'z3_v1.h', 'z3_macros.h', 'z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h', 'z3_fpa.h', 'c++/z3++.h'): + shutil.copy(os.path.join(SRC_DIR, 'src/api', fname), os.path.join(HEADERS_DIR, fname)) + +def _copy_sources(): + """ + Prepare for a source distribution by assembling a minimal set of source files needed + for building + """ + shutil.rmtree(SRC_DIR_LOCAL, ignore_errors=True) + os.mkdir(SRC_DIR_LOCAL) + + shutil.copy(os.path.join(SRC_DIR_REPO, 'LICENSE.txt'), SRC_DIR_LOCAL) + shutil.copytree(os.path.join(SRC_DIR_REPO, 'scripts'), os.path.join(SRC_DIR_LOCAL, 'scripts')) + shutil.copytree(os.path.join(SRC_DIR_REPO, 'examples'), os.path.join(SRC_DIR_LOCAL, 'examples')) + shutil.copytree(os.path.join(SRC_DIR_REPO, 'src'), os.path.join(SRC_DIR_LOCAL, 'src'), + ignore=lambda src, names: ['python'] if 'api' in src else []) + + # stub python dir to make build happy + os.mkdir(os.path.join(SRC_DIR_LOCAL, 'src/api/python')) + os.mkdir(os.path.join(SRC_DIR_LOCAL, 'src/api/python/z3')) + open(os.path.join(SRC_DIR_LOCAL, 'src/api/python/z3/.placeholder'), 'w').close() + class build(_build): def run(self): self.execute(_configure_z3, (), msg="Configuring Z3") self.execute(_build_z3, (), msg="Building Z3") + self.execute(_copy_bins, (), msg="Copying binaries") + _build.run(self) class develop(_develop): def run(self): self.execute(_configure_z3, (), msg="Configuring Z3") self.execute(_build_z3, (), msg="Building Z3") + self.execute(_copy_bins, (), msg="Copying binaries") + _develop.run(self) + +class bdist_egg(_bdist_egg): + def run(self): + self.run_command('build') + _bdist_egg.run(self) + +class sdist(_sdist): + def run(self): + self.execute(_clean_bins, (), msg="Cleaning binary files") + self.execute(_copy_sources, (), msg="Copying source files") + _sdist.run(self) # the build directory needs to exist -try: os.makedirs(os.path.join(build_dir, 'build')) -except OSError: pass +#try: os.makedirs(os.path.join(ROOT_DIR, 'build')) +#except OSError: pass setup( name='angr-only-z3-custom', @@ -72,17 +142,12 @@ setup( url='https://github.com/angr/angr-z3', license='MIT License', keywords=['z3', 'smt', 'sat', 'prover', 'theorem'], - package_dir={'': 'build'}, - packages=[''], - data_files=[ - ('lib', (os.path.join(build_dir, 'build', library_file),)), - ('include', tuple(os.path.join(build_dir, f) for f in ('src/api/z3.h', - 'src/api/z3_v1.h', 'src/api/z3_macros.h', - 'src/api/z3_api.h', 'src/api/z3_algebraic.h', - 'src/api/z3_polynomial.h', 'src/api/z3_rcf.h', - 'src/api/z3_interp.h', 'src/api/z3_fpa.h', - 'src/api/c++/z3++.h') )), - ], - #scripts=[os.path.join(build_dir, 'build', 'z3')] if sys.version_info[0] == 2 else [], - cmdclass={'build': build, 'develop': develop}, + packages=['z3'], + include_package_data=True, + package_data={ + 'z3': ['lib/*', 'include/*'] + }, + scripts=['bin/z3'], + #scripts=[os.path.join(ROOT_DIR, 'build', 'z3')] if sys.version_info[0] == 2 else [], + cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_egg': bdist_egg}, ) From cb83c42100e7fc1a2bbf7182523b9e19cda53bdf Mon Sep 17 00:00:00 2001 From: Andrew Dutcher Date: Sat, 10 Sep 2016 11:41:04 -0700 Subject: [PATCH 4/8] Make python stuff live in a python directory in the build tree --- scripts/mk_project.py | 3 +- scripts/mk_util.py | 75 +++++++++++++++++++++++++------------------ scripts/update_api.py | 21 ++++++------ 3 files changed, 56 insertions(+), 43 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 78bc290f8..00b5cdef5 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -87,7 +87,8 @@ def init_project_def(): reexports=['api'], dll_name='libz3', static=build_static_lib(), - export_files=API_files) + export_files=API_files, + staging_link='python') add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties', default_key_file='src/api/dotnet/Microsoft.Z3.snk') add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.microsoft.z3", manifest_file='manifest') add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml') diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0d2b23a3e..eca0c4738 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1230,7 +1230,7 @@ def get_so_ext(): return 'dll' class DLLComponent(Component): - def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static): + def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static, staging_link=None): Component.__init__(self, name, path, deps) if dll_name is None: dll_name = name @@ -1239,6 +1239,7 @@ class DLLComponent(Component): self.reexports = reexports self.install = install self.static = static + self.staging_link = staging_link # link a copy of the shared object into this directory on build def get_link_name(self): if self.static: @@ -1294,6 +1295,11 @@ class DLLComponent(Component): out.write(' $(SLINK_EXTRA_FLAGS)') if IS_WINDOWS: out.write(' /DEF:%s.def' % os.path.join(self.to_src_dir, self.name)) + if self.staging_link: + if IS_WINDOWS or IS_OSX: + out.write('\n\tcp %s %s' % (self.dll_file(), self.staging_link)) + else: + out.write('\n\tln -s %s %s' % (os.path.join(reverse_path(self.staging_link), self.dll_file()), self.staging_link)) out.write('\n') if self.static: if IS_WINDOWS: @@ -1432,13 +1438,18 @@ class PythonInstallComponent(Component): def mk_install(self, out): if not is_python_install_enabled(): return - MakeRuleCmd.make_install_directory(out, self.pythonPkgDir, in_prefix=self.in_prefix_install) + MakeRuleCmd.make_install_directory(out, + os.path.join(self.pythonPkgDir, 'z3'), + in_prefix=self.in_prefix_install) + MakeRuleCmd.make_install_directory(out, + os.path.join(self.pythonPkgDir, 'z3', 'lib'), + in_prefix=self.in_prefix_install) # Sym-link or copy libz3 into python package directory if IS_WINDOWS or IS_OSX: MakeRuleCmd.install_files(out, self.libz3Component.dll_file(), - os.path.join(self.pythonPkgDir, + os.path.join(self.pythonPkgDir, 'z3', 'lib', self.libz3Component.dll_file()), in_prefix=self.in_prefix_install ) @@ -1449,34 +1460,29 @@ class PythonInstallComponent(Component): # staged installs that use DESTDIR). MakeRuleCmd.create_relative_symbolic_link(out, self.libz3Component.install_path(), - os.path.join(self.pythonPkgDir, + os.path.join(self.pythonPkgDir, 'z3', 'lib', self.libz3Component.dll_file() ), ) - MakeRuleCmd.install_files(out, 'z3*.py', self.pythonPkgDir, + MakeRuleCmd.install_files(out, os.path.join('python', 'z3', '*.py'), + os.path.join(self.pythonPkgDir, 'z3'), in_prefix=self.in_prefix_install) if sys.version >= "3": - pythonPycacheDir = os.path.join(self.pythonPkgDir, '__pycache__') + pythonPycacheDir = os.path.join(self.pythonPkgDir, 'z3', '__pycache__') MakeRuleCmd.make_install_directory(out, pythonPycacheDir, in_prefix=self.in_prefix_install) MakeRuleCmd.install_files(out, - '{}*.pyc'.format(os.path.join('__pycache__', 'z3')), + os.path.join('python', 'z3', '__pycache__', '*.pyc'), pythonPycacheDir, in_prefix=self.in_prefix_install) else: MakeRuleCmd.install_files(out, - 'z3*.pyc', + os.path.join('python', 'z3', '*.pyc'), self.pythonPkgDir, in_prefix=self.in_prefix_install) if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): - if os.uname()[0] == 'Darwin': - LD_LIBRARY_PATH = "DYLD_LIBRARY_PATH" - else: - LD_LIBRARY_PATH = "LD_LIBRARY_PATH" - out.write('\t@echo Z3 shared libraries were installed at \'%s\', make sure this directory is in your %s environment variable.\n' % - (os.path.join(PREFIX, INSTALL_LIB_DIR), LD_LIBRARY_PATH)) out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR) def mk_uninstall(self, out): @@ -1488,13 +1494,13 @@ class PythonInstallComponent(Component): in_prefix=self.in_prefix_install ) MakeRuleCmd.remove_installed_files(out, - '{}*.py'.format(os.path.join(self.pythonPkgDir, 'z3')), + os.path.join(self.pythonPkgDir, 'z3', '*.py'), in_prefix=self.in_prefix_install) MakeRuleCmd.remove_installed_files(out, - '{}*.pyc'.format(os.path.join(self.pythonPkgDir, 'z3')), + os.path.join(self.pythonPkgDir, 'z3', '*.pyc'), in_prefix=self.in_prefix_install) MakeRuleCmd.remove_installed_files(out, - '{}*.pyc'.format(os.path.join(self.pythonPkgDir, '__pycache__', 'z3')), + os.path.join(self.pythonPkgDir, 'z3', '__pycache__', '*.pyc'), in_prefix=self.in_prefix_install ) @@ -2157,9 +2163,9 @@ class PythonExampleComponent(ExampleComponent): def mk_makefile(self, out): full = os.path.join(EXAMPLE_DIR, self.path) for py in filter(lambda f: f.endswith('.py'), os.listdir(full)): - shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, py)) + shutil.copyfile(os.path.join(full, py), os.path.join(BUILD_DIR, 'python', py)) if is_verbose(): - print("Copied Z3Py example '%s' to '%s'" % (py, BUILD_DIR)) + print("Copied Z3Py example '%s' to '%s'" % (py, os.path.join(BUILD_DIR, 'python'))) out.write('_ex_%s: \n\n' % self.name) @@ -2189,8 +2195,8 @@ def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True): c = ExtraExeComponent(name, exe_name, path, deps, install) reg_component(name, c) -def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False): - c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static) +def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False, staging_link=None): + c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static, staging_link) reg_component(name, c) return c @@ -2519,9 +2525,9 @@ def mk_makefile(): if c.main_component(): out.write(' %s' % c.name) out.write('\n\t@echo Z3 was successfully built.\n') - out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % BUILD_DIR) + out.write("\t@echo \"Z3Py scripts can already be executed in the \'%s\' directory.\"\n" % os.path.join(BUILD_DIR, 'python')) pathvar = "DYLD_LIBRARY_PATH" if IS_OSX else "PATH" if IS_WINDOWS else "LD_LIBRARY_PATH" - out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH and %s environment variables.\"\n" % (BUILD_DIR, pathvar)) + out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be executed if the \'%s\' directory is added to the PYTHONPATH environment variable and the \'%s\' directory is added to the %s environment variable.\"\n" % (os.path.join(BUILD_DIR, 'python'), BUILD_DIR, pathvar)) if not IS_WINDOWS: out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n") out.write('\t@echo " sudo make install"\n\n') @@ -2737,35 +2743,40 @@ def mk_def_files(): def cp_z3py_to_build(): mk_dir(BUILD_DIR) - z3py_dest = os.path.join(BUILD_DIR, 'z3.py') + mk_dir(os.path.join(BUILD_DIR, 'python')) + z3py_dest = os.path.join(BUILD_DIR, 'python', 'z3') z3py_src = os.path.join(Z3PY_SRC_DIR, 'z3') + # Erase existing .pyc files for root, dirs, files in os.walk(Z3PY_SRC_DIR): for f in files: if f.endswith('.pyc'): rmf(os.path.join(root, f)) # Compile Z3Py files - if compileall.compile_dir(Z3PY_SRC_DIR, force=1) != 1: + if compileall.compile_dir(z3py_src, force=1) != 1: raise MKException("failed to compile Z3Py sources") + if is_verbose: + print("Generated python bytecode") # Copy sources to build - shutil.rmtree(z3py_dest, ignore_errors=True) - shutil.copytree(z3py_src, z3py_dest) - if is_verbose(): - print("Copied python bindings") + mk_dir(z3py_dest) + for py in filter(lambda f: f.endswith('.py'), os.listdir(z3py_src)): + shutil.copyfile(os.path.join(z3py_src, py), os.path.join(z3py_dest, py)) + if is_verbose(): + print("Copied '%s'" % py) # Python 2.x support for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(z3py_src)): shutil.copyfile(os.path.join(z3py_src, pyc), os.path.join(z3py_dest, pyc)) if is_verbose(): - print("Generated '%s'" % pyc) + print("Copied '%s'" % pyc) # Python 3.x support src_pycache = os.path.join(z3py_src, '__pycache__') + target_pycache = os.path.join(z3py_dest, '__pycache__') if os.path.exists(src_pycache): for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(src_pycache)): - target_pycache = os.path.join(z3py_dest, '__pycache__') mk_dir(target_pycache) shutil.copyfile(os.path.join(src_pycache, pyc), os.path.join(target_pycache, pyc)) if is_verbose(): - print("Generated '%s'" % pyc) + print("Copied '%s'" % pyc) def mk_bindings(api_files): if not ONLY_MAKEFILES: diff --git a/scripts/update_api.py b/scripts/update_api.py index 1f0ae4e4c..48a4d6114 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1605,23 +1605,20 @@ def write_core_py_preamble(core_py): core_py.write('from .z3consts import *\n') core_py.write( """ +_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so' + _lib = None def lib(): global _lib - if _lib == None: - _dir = pkg_resources.resource_filename('z3', 'lib') - for ext in ['dll', 'so', 'dylib']: + if _lib is None: + _dirs = ['.', pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), ''] + for _dir in _dirs: try: - init(os.path.join(_dir, 'libz3.%s' % ext)) + init(_dir) break except: pass - try: - init('libz3.%s' % ext) - break - except: - pass - if _lib == None: + if _lib is None: raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python") return _lib @@ -1644,6 +1641,10 @@ else: return "" def init(PATH): + PATH = os.path.realpath(PATH) + if os.path.isdir(PATH): + PATH = os.path.join(PATH, 'libz3.%s' % _ext) + global _lib _lib = ctypes.CDLL(PATH) """ From 02783d0bfba4cc6b424651327baefd0b8761aa38 Mon Sep 17 00:00:00 2001 From: Andrew Dutcher Date: Wed, 14 Sep 2016 01:10:44 -0700 Subject: [PATCH 5/8] Minor tweaks to make things more reliable/less obnoxious --- scripts/mk_util.py | 2 +- src/api/python/.gitignore | 1 + src/api/python/setup.py | 3 +++ 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index eca0c4738..305f94609 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1299,7 +1299,7 @@ class DLLComponent(Component): if IS_WINDOWS or IS_OSX: out.write('\n\tcp %s %s' % (self.dll_file(), self.staging_link)) else: - out.write('\n\tln -s %s %s' % (os.path.join(reverse_path(self.staging_link), self.dll_file()), self.staging_link)) + out.write('\n\tln -f -s %s %s' % (os.path.join(reverse_path(self.staging_link), self.dll_file()), self.staging_link)) out.write('\n') if self.static: if IS_WINDOWS: diff --git a/src/api/python/.gitignore b/src/api/python/.gitignore index a0a01631f..86e4bc9ce 100644 --- a/src/api/python/.gitignore +++ b/src/api/python/.gitignore @@ -5,3 +5,4 @@ build *.egg-info bin z3/lib +z3/include diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 6ccd45c60..a43ded92e 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -41,6 +41,9 @@ def _clean_bins(): shutil.rmtree(HEADERS_DIR, ignore_errors=True) def _configure_z3(): + # bail out early if we don't need to do this - it forces a rebuild every time otherwise + if os.path.exists(BUILD_DIR): + return args = [sys.executable, os.path.join(SRC_DIR, 'scripts', 'mk_make.py')] if sys.platform == 'win32' and platform.architecture()[0] == '64bit': From 02217d048be04e21bf3fc96be625c8869e41f601 Mon Sep 17 00:00:00 2001 From: Andrew Dutcher Date: Wed, 14 Sep 2016 14:19:10 -0700 Subject: [PATCH 6/8] replace all non-portable filepath slashes with os.path.join --- scripts/mk_genfile_common.py | 2 +- scripts/update_api.py | 2 +- src/api/python/setup.py | 21 ++++++++++----------- 3 files changed, 12 insertions(+), 13 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 2ecb06776..7e7cb5584 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -98,7 +98,7 @@ def mk_z3consts_py_internal(api_files, output_dir): openbrace_pat = re.compile("{ *") closebrace_pat = re.compile("}.*;") - z3consts = open(os.path.join(output_dir, 'z3/z3consts.py'), 'w') + z3consts = open(os.path.join(output_dir, 'z3', 'z3consts.py'), 'w') z3consts_output_path = z3consts.name z3consts.write('# Automatically generated file\n\n') for api_file in api_files: diff --git a/scripts/update_api.py b/scripts/update_api.py index 48a4d6114..d8b2bec58 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1708,7 +1708,7 @@ def generate_files(api_files, with mk_file_or_temp(api_output_dir, 'api_log_macros.h') as log_h: with mk_file_or_temp(api_output_dir, 'api_log_macros.cpp') as log_c: with mk_file_or_temp(api_output_dir, 'api_commands.cpp') as exe_c: - with mk_file_or_temp(z3py_output_dir, 'z3/z3core.py') as core_py: + with mk_file_or_temp(z3py_output_dir, os.path.join('z3', 'z3core.py')) as core_py: # Write preambles write_log_h_preamble(log_h) write_log_c_preamble(log_c) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index a43ded92e..c6d7d8824 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -18,7 +18,7 @@ build_env['CXXFLAGS'] = "-std=c++11" ROOT_DIR = os.path.abspath(os.path.dirname(__file__)) SRC_DIR_LOCAL = os.path.join(ROOT_DIR, 'core') -SRC_DIR_REPO = os.path.join(ROOT_DIR, '../../..') +SRC_DIR_REPO = os.path.join(ROOT_DIR, '..', '..', '..') SRC_DIR = SRC_DIR_LOCAL if os.path.exists(SRC_DIR_LOCAL) else SRC_DIR_REPO BUILD_DIR = os.path.join(SRC_DIR, 'build') # implicit in configure script LIBS_DIR = os.path.join(ROOT_DIR, 'z3', 'lib') @@ -72,8 +72,8 @@ def _copy_bins(): _clean_bins() if SRC_DIR == SRC_DIR_LOCAL: - shutil.copy(os.path.join(SRC_DIR, 'src/api/python/z3/z3core.py'), os.path.join(ROOT_DIR, 'z3')) - shutil.copy(os.path.join(SRC_DIR, 'src/api/python/z3/z3consts.py'), os.path.join(ROOT_DIR, 'z3')) + shutil.copy(os.path.join(SRC_DIR, 'src', 'api', 'python', 'z3', 'z3core.py'), os.path.join(ROOT_DIR, 'z3')) + shutil.copy(os.path.join(SRC_DIR, 'src', 'api', 'python', 'z3', 'z3consts.py'), os.path.join(ROOT_DIR, 'z3')) # STEP 2: Copy the shared library, the executable and the headers @@ -83,8 +83,8 @@ def _copy_bins(): os.mkdir(os.path.join(HEADERS_DIR, 'c++')) shutil.copy(os.path.join(BUILD_DIR, 'libz3.so'), LIBS_DIR) shutil.copy(os.path.join(BUILD_DIR, 'z3'), BINS_DIR) - for fname in ('z3.h', 'z3_v1.h', 'z3_macros.h', 'z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h', 'z3_fpa.h', 'c++/z3++.h'): - shutil.copy(os.path.join(SRC_DIR, 'src/api', fname), os.path.join(HEADERS_DIR, fname)) + for fname in ('z3.h', 'z3_v1.h', 'z3_macros.h', 'z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h', 'z3_fpa.h', os.path.join('c++', 'z3++.h')): + shutil.copy(os.path.join(SRC_DIR, 'src', 'api', fname), os.path.join(HEADERS_DIR, fname)) def _copy_sources(): """ @@ -101,9 +101,9 @@ def _copy_sources(): ignore=lambda src, names: ['python'] if 'api' in src else []) # stub python dir to make build happy - os.mkdir(os.path.join(SRC_DIR_LOCAL, 'src/api/python')) - os.mkdir(os.path.join(SRC_DIR_LOCAL, 'src/api/python/z3')) - open(os.path.join(SRC_DIR_LOCAL, 'src/api/python/z3/.placeholder'), 'w').close() + os.mkdir(os.path.join(SRC_DIR_LOCAL, 'src', 'api', 'python')) + os.mkdir(os.path.join(SRC_DIR_LOCAL, 'src', 'api', 'python', 'z3')) + open(os.path.join(SRC_DIR_LOCAL, 'src', 'api', 'python', 'z3', '.placeholder'), 'w').close() class build(_build): def run(self): @@ -148,9 +148,8 @@ setup( packages=['z3'], include_package_data=True, package_data={ - 'z3': ['lib/*', 'include/*'] + 'z3': [os.path.join('lib', '*'), os.path.join('include', '*')] }, - scripts=['bin/z3'], - #scripts=[os.path.join(ROOT_DIR, 'build', 'z3')] if sys.version_info[0] == 2 else [], + scripts=[os.path.join('bin', 'z3')], cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_egg': bdist_egg}, ) From 9e498536b6af7770570db41ab59ec505b59e1c30 Mon Sep 17 00:00:00 2001 From: Andrew Dutcher Date: Thu, 15 Sep 2016 00:28:19 -0700 Subject: [PATCH 7/8] Fix cmake build to work with the new system --- contrib/cmake/examples/CMakeLists.txt | 1 + contrib/cmake/examples/python/CMakeLists.txt | 24 ++++++++++ contrib/cmake/src/api/python/CMakeLists.txt | 49 +++++++++++++------- 3 files changed, 56 insertions(+), 18 deletions(-) create mode 100644 contrib/cmake/examples/python/CMakeLists.txt diff --git a/contrib/cmake/examples/CMakeLists.txt b/contrib/cmake/examples/CMakeLists.txt index 49ea72fdc..e596ed3dd 100644 --- a/contrib/cmake/examples/CMakeLists.txt +++ b/contrib/cmake/examples/CMakeLists.txt @@ -1,3 +1,4 @@ add_subdirectory(c) add_subdirectory(c++) add_subdirectory(tptp) +add_subdirectory(python) diff --git a/contrib/cmake/examples/python/CMakeLists.txt b/contrib/cmake/examples/python/CMakeLists.txt new file mode 100644 index 000000000..fdbb7891f --- /dev/null +++ b/contrib/cmake/examples/python/CMakeLists.txt @@ -0,0 +1,24 @@ +set(python_example_files + example.py + visitor.py +) + +set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}/python") + +set(build_z3_python_examples_target_depends "") +foreach (example_file ${python_example_files}) + add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${example_file}" + COMMAND "${CMAKE_COMMAND}" "-E" "copy" + "${CMAKE_CURRENT_SOURCE_DIR}/${example_file}" + "${z3py_bindings_build_dest}/${example_file}" + DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${example_file}" + COMMENT "Copying \"${example_file}\" to ${z3py_bindings_build_dest}/${example_file}" + ) + list(APPEND build_z3_python_examples_target_depends "${z3py_bindings_build_dest}/${example_file}") +endforeach() + +add_custom_target(build_z3_python_examples + ALL + DEPENDS + ${build_z3_python_examples_target_depends} +) diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/contrib/cmake/src/api/python/CMakeLists.txt index 6babb2069..375890c91 100644 --- a/contrib/cmake/src/api/python/CMakeLists.txt +++ b/contrib/cmake/src/api/python/CMakeLists.txt @@ -4,31 +4,34 @@ message(STATUS "Emitting rules to build Z3 python bindings") ############################################################################### # This allows the python bindings to be used directly from the build directory set(z3py_files - z3.py - z3num.py - z3poly.py - z3printer.py - z3rcf.py - z3types.py - z3util.py + z3/__init__.py + z3/z3.py + z3/z3num.py + z3/z3poly.py + z3/z3printer.py + z3/z3rcf.py + z3/z3types.py + z3/z3util.py ) -set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}") +set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}/python") +file(MAKE_DIRECTORY "${z3py_bindings_build_dest}") +file(MAKE_DIRECTORY "${z3py_bindings_build_dest}/z3") set(build_z3_python_bindings_target_depends "") foreach (z3py_file ${z3py_files}) - add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/${z3py_file}" + add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${z3py_file}" COMMAND "${CMAKE_COMMAND}" "-E" "copy" - "${CMAKE_CURRENT_SOURCE_DIR}/z3/${z3py_file}" - "${z3py_bindings_build_dest}/z3.py" - DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/z3/${z3py_file}" - COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}/z3.py/${z3py_file}" + "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}" + "${z3py_bindings_build_dest}/${z3py_file}" + DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}" + COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}/${z3py_file}" ) list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/${z3py_file}") endforeach() # Generate z3core.py -add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3core.py" +add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py" COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/update_api.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} @@ -43,10 +46,10 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3core.py" COMMENT "Generating z3core.py" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} ) -list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3core.py") +list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3core.py") # Generate z3consts.py -add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3consts.py" +add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3consts.py" COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} @@ -59,13 +62,23 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3consts.py" COMMENT "Generating z3consts.py" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} ) -list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3consts.py") +list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3consts.py") + +# Link libz3 into the python directory so bindings work out of the box +add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" + COMMAND "${CMAKE_COMMAND}" "-E" "create_symlink" + "${CMAKE_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" + "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" + DEPENDS libz3 + COMMENT "Linking libz3 into python directory" +) # Convenient top-level target add_custom_target(build_z3_python_bindings ALL DEPENDS ${build_z3_python_bindings_target_depends} + "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" ) ############################################################################### @@ -116,7 +129,7 @@ if (INSTALL_PYTHON_BINDINGS) # Using DESTDIR still seems to work even if we use an absolute path message(STATUS "Python bindings will be installed to \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"") install(FILES ${build_z3_python_bindings_target_depends} - DESTINATION "${CMAKE_INSTALL_PYTHON_PKG_DIR}" + DESTINATION "${CMAKE_INSTALL_PYTHON_PKG_DIR}/z3" ) else() message(STATUS "Not emitting rules to install Z3 python bindings") From f451363a8f8430d665be9e3a81ca8f0de7cc6578 Mon Sep 17 00:00:00 2001 From: Andrew Dutcher Date: Wed, 21 Sep 2016 15:15:21 -0700 Subject: [PATCH 8/8] use copy instead of create_symlink when not on unix --- contrib/cmake/src/api/python/CMakeLists.txt | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/contrib/cmake/src/api/python/CMakeLists.txt index 375890c91..dcd6f09e0 100644 --- a/contrib/cmake/src/api/python/CMakeLists.txt +++ b/contrib/cmake/src/api/python/CMakeLists.txt @@ -64,9 +64,15 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3consts.py" ) list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3consts.py") +if (UNIX) + set(LINK_COMMAND "create_symlink") +else() + set(LINK_COMMAND "copy") +endif() + # Link libz3 into the python directory so bindings work out of the box add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" - COMMAND "${CMAKE_COMMAND}" "-E" "create_symlink" + COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}" "${CMAKE_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" DEPENDS libz3