christoftorres / Osiris

A tool to detect integer bugs in Ethereum smart contracts (ACSAC 2018).
62 stars 17 forks source link

running Osiris using the latest Z3 #2

Closed sunbeomso closed 5 years ago

sunbeomso commented 5 years ago

Hi, I am trying to run Osiris using the latest version of Z3 (v 4.8.4). However, Osiris produces the following error message:

Traceback (most recent call last):
  File "osiris/osiris.py", line 10, in <module>
    import symExec
  File "/home/sunbeom/Osiris/osiris/symExec.py", line 14, in <module>
    import z3
  File "/home/sunbeom/Osiris/osiris/z3/__init__.py", line 1, in <module>
    from .z3 import *
  File "/home/sunbeom/Osiris/osiris/z3/z3.py", line 44, in <module>
    from . import z3core
  File "/home/sunbeom/Osiris/osiris/z3/z3core.py", line 732, in <module>
    _lib.Z3_get_parser_error.restype = ctypes.c_char_p
  File "/usr/lib/python2.7/ctypes/__init__.py", line 379, in __getattr__
    func = self.__getitem__(name)
  File "/usr/lib/python2.7/ctypes/__init__.py", line 384, in __getitem__
    func = self._FuncPtr((name_or_ordinal, self))
AttributeError: /usr/lib/libz3.so: undefined symbol: Z3_get_parser_error

I tested on Ubuntu 18.04.2 . My attempt to install the latest Z3 using the docker image provided by you also failed.

christoftorres commented 5 years ago

Osiris currently only supports up to version 4.7.1 of Z3. The Z3 used inside the docker image is 4.6.0. I suggest you to use an older version of Z3 or to use the version that is provided with the docker image.

sunbeomso commented 5 years ago

Thanks for the response! I close the issue.