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}, )