BinaryAnalysisPlatform / bap

Binary Analysis Platform
MIT License
2.07k stars 273 forks source link

undefined symbol: Z3_mk_lambda #1586

Open duplys opened 1 year ago

duplys commented 1 year ago

I encounter an error when trying to run BAP in a Docker container:

root@9607051f0674:/# bap -h
Failed to load plugin "primus-symbolic-executor": Failed to load z3ml: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/tmp/z3mle4c664.cmxs: undefined symbol: Z3_mk_lambda\")")
Failed to load 1 plugins, details follow:
The plugin `/usr/local/lib/bap/primus_symbolic_executor.plugin' has failed with the following error:
Failed to load z3ml: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"/tmp/z3mle4c664.cmxs: undefined symbol: Z3_mk_lambda\")")

From what I understand, z3ml is an OCaml binding for the Z3 theorem prover and Z3_mk_lambda seems to be part of the Z3 C API. However, I could not find any other Z3 packages that I could install to fix the error.

Is there something simple I'm missing that solves this issue?

The Docker container was built using the following Dockerfile (based on Ubuntu 18.04 since BAP requires libffi6 and 18.04 seems to be the last (?) Ubuntu release having libffi6). The BAP installation using wget and dpkg -i <...> follows the instructions from this repository.

FROM ubuntu:18.04

RUN apt update && apt install -y \
    gcc \
    libtinfo5 \
    libffi6 \
    libz3-cil \
    libz3-ocaml-dev \
    make \
    wget \
    z3 \
    && rm -rf /var/lib/apt/lists/*

WORKDIR /opt/bap

RUN wget https://github.com/BinaryAnalysisPlatform/bap/releases/download/v2.5.0/bap_2.5.0.deb && \
    wget https://github.com/BinaryAnalysisPlatform/bap/releases/download/v2.5.0/libbap_2.5.0.deb && \
    wget https://github.com/BinaryAnalysisPlatform/bap/releases/download/v2.5.0/libbap-dev_2.5.0.deb
RUN dpkg -i bap_2.5.0.deb && \
    dpkg -i libbap_2.5.0.deb && \
    dpkg -i libbap-dev_2.5.0.deb