FINISH IT

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")

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

src/api/python/.gitignore

@@ -0,0 +1,7 @@
+MANIFEST
+dist
+core
+build
+*.egg-info
+bin
+z3/lib

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 *

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"
+    LIBRARY_FILE = "libz3.dylib"
-elif sys.platform == 'win32':
+elif sys.platform in ('win32', 'cygwin'):
-    library_file = "libz3.dll"
+    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(SRC_DIR, 'scripts', 'mk_make.py')]
-        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:
+    if sys.platform == 'win32' and platform.architecture()[0] == '64bit':
-            raise LibError("Unable to configure Z3.")
+        args += ['-x']
-    else:   # linux and osx
+
-        if subprocess.call([os.path.join(build_dir, 'configure')],
+    if subprocess.call(args, env=build_env, cwd=SRC_DIR) != 0:
-                    env=build_env, cwd=build_dir) != 0:
+        raise LibError("Unable to configure Z3.")
-            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'),
+        if subprocess.call(['make', '-j', str(multiprocessing.cpu_count())],
-                            '-j', str(multiprocessing.cpu_count())],
+                    env=build_env, cwd=BUILD_DIR) != 0:
-                    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'))
+#try: os.makedirs(os.path.join(ROOT_DIR, 'build'))
-except OSError: pass
+#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=['z3'],
-    packages=[''],
+    include_package_data=True,
-    data_files=[
+    package_data={
-        ('lib', (os.path.join(build_dir, 'build', library_file),)),
+        'z3': ['lib/*', 'include/*']
-        ('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',
+    scripts=['bin/z3'],
-                     'src/api/z3_api.h', 'src/api/z3_algebraic.h',
+    #scripts=[os.path.join(ROOT_DIR, 'build', 'z3')] if sys.version_info[0] == 2 else [],
-                     'src/api/z3_polynomial.h', 'src/api/z3_rcf.h',
+    cmdclass={'build': build, 'develop': develop, 'sdist': sdist, 'bdist_egg': bdist_egg},
-                     '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},
 )