Trouble Importing Z3 in Example

[KevinCooper]

On a 32 and 64 bit Ubuntu images, I am successfully able to import z3 like in the following examples
Python 2.7.6 (default, Mar 22 2014, 22:59:56)
[GCC 4.8.2] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>>

However, when I try to use z3 in a sample example file on both 64 and 32 bit images, I get the following import error.

student@ubuntu:~/Desktop/pin_dir/source/tools/Python_Pin$ sudo bash ../../../pin.sh -t obj-ia32/Python_Pin.so -m examples/call_chain.py -- /bin/echo "hello"
Traceback (most recent call last):
File "examples/call_chain.py", line 2, in
from z3 import *
File "/usr/lib/python2.7/dist-packages/z3.py", line 43, in
from z3core import *
File "/usr/lib/python2.7/dist-packages/z3core.py", line 3, in
import ctypes
File "/usr/lib/python2.7/ctypes/init.py", line 10, in
from _ctypes import Union, Structure, Array
ImportError: /usr/lib/python2.7/lib-dynload/_ctypes.i386-linux-gnu.so: undefined symbol: PyFloat_Type
hello

Would there be some possible fix for this?

[KevinCooper]

This is an extension of problem #1 mentioned on the page.

[blankwall]

This is an issue with Ctypes and your Python build. @ancat will give us some more details when he can and he should be able to provide a solution.

[ancat]

Hi Kevin! This is an issue regarding the default builds of python that come with your OS. A lot of core python modules are implemented as shared objects (ctypes for example) without symbols, so resolution fails. You'll need to compile python yourself. First, you'll need to pull down the latest version of the code since I had to modify the makefile to get it working. Here's what I did after downloading and extracting Python 2.7.8 to /opt/Python-2.7.8:

In /opt/Python-2.7.8:
Configure Python: ./configure --enable-shared
Build Python: make

In the Python_Pin directory:
Build Python-Pin to use the new python instead: make CUSTOM_PYTHON=true
Run your pintool: PYTHONPATH=/opt/Python-2.7.8/Lib:/opt/Python-2.7.8/build/lib.linux-x86_64-2.7 LD_LIBRARY_PATH=/opt/Python-2.7.8 ../../../pin -t obj-intel64/Python_Pin.so -m <your python> -- <your binary>

Unfortunately I could only get it working with those environment variables; I have no idea how to get Python_Pin.so to load the non-system-default libpython2.7.so:

$ ldd obj-intel64/Python_Pin.so
        linux-vdso.so.1 =>  (0x00007fffd41f1000)
        libdwarf.so => not found
        libelf.so.0 => /usr/lib/x86_64-linux-gnu/libelf.so.0 (0x00007f91a9477000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007f91a9272000)
-->     libpython2.7.so.1.0 => /usr/lib/x86_64-linux-gnu/libpython2.7.so.1.0 (0x00007f91a8d0b000)
        libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007f91a8a07000)
        libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007f91a87f0000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f91a842a000)
        /lib64/ld-linux-x86-64.so.2 (0x00007f91a9bd6000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007f91a820c000)
        libz.so.1 => /lib/x86_64-linux-gnu/libz.so.1 (0x00007f91a7ff2000)
        libutil.so.1 => /lib/x86_64-linux-gnu/libutil.so.1 (0x00007f91a7def000)
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f91a7ae9000)

versus

$ LD_LIBRARY_PATH=/opt/Python-2.7.8 ldd obj-intel64/Python_Pin.so
        linux-vdso.so.1 =>  (0x00007fff7d9fe000)
        libdwarf.so => not found
        libelf.so.0 => /usr/lib/x86_64-linux-gnu/libelf.so.0 (0x00007f9eff6e1000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007f9eff4dc000)
-->     libpython2.7.so.1.0 => /opt/Python-2.7.8/libpython2.7.so.1.0 (0x00007f9eff0d4000)
        libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007f9efedd0000)
        libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007f9efebb9000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f9efe7f3000)
        /lib64/ld-linux-x86-64.so.2 (0x00007f9effe40000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007f9efe5d5000)
        libutil.so.1 => /lib/x86_64-linux-gnu/libutil.so.1 (0x00007f9efe3d1000)
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f9efe0cb000)

Using this, I was able to get shared object modules working (both ctypes and z3). Let me know if this works for you.

[KevinCooper]

Ancat, thank you very much for your help. You both have been very helpful. My commands for those that may be interested down the road were:

cd /opt
sudo tar xf Python-2.7.8.tgz /opt/
sudo cp -r /home/user/z3/ /opt/
cd Python-2.7.8/
sudo ./configure --enable-shared
sudo make -j 4
#Ignore errors from above make if necessary modules not built do not include ctypes
cd ../z3
sudo autoconf
sudo ./configure
sudo python scripts/mk_make.py
cd build/ ; sudo make -j 2
cp ../src/api/python/*  ../../Python-2.7.8/Lib/
cp ../build/libz3.so ../../Python-2.7.8/build/lib.linux-x86_64-2.7/
cd ~/Desktop/pin_dir/source/tools/Python_Pin
sudo make clean
make CUSTOM_PYTHON=true -j 2
sudo PYTHONPATH=/opt/Python-2.7.8/Lib:/opt/Python-2.7.8/build/lib.linux-x86_64-2.7 LD_LIBRARY_PATH=/opt/Python-2.7.8 bash ../../../pin.sh -t obj-intel64/Python_Pin.so -m examples/taint.py -- ../../../../taint