First steps to a sane python build

.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

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

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:

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))
+    shutil.copytree(z3py_src, z3py_dest)
     if is_verbose():
-            print("Copied '%s'" % py)
+        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():

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)

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

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

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

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
-