Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Klee aborts when running on latest version of tar #1213

Closed
norhh opened this issue Feb 4, 2020 · 7 comments
Closed

Klee aborts when running on latest version of tar #1213

norhh opened this issue Feb 4, 2020 · 7 comments

Comments

@norhh
Copy link

norhh commented Feb 4, 2020

Steps

  • Download tar-1.32 and extract
  • >./configure
  • > make CC=wllvm
  • cd src
  • extract-bc tar
  • run klee --libc=uclibc tar.bc <any_tar_args>

Versions

  • KLEE 2.0
  • LLVM 6.0
  • uclibc version tag = klee_0_9_29

Error Msg

inlinable function call in a function with debug info must have a !dbg location
  call void @klee_overshift_check(i64 32, i64 %int_cast_to_i64)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_overshift_check(i64 32, i64 %int_cast_to_i641)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_overshift_check(i64 32, i64 %int_cast_to_i642)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_div_zero_check(i64 %1066)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_div_zero_check(i64 %1097)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_div_zero_check(i64 %1170)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_div_zero_check(i64 %73)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_div_zero_check(i64 %73)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_div_zero_check(i64 %73)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_div_zero_check(i64 %73)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_div_zero_check(i64 %73)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_div_zero_check(i64 %73)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_div_zero_check(i64 %73)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_div_zero_check(i64 %73)
inlinable function call in a function with debug info must have a !dbg location
  call void @klee_overshift_check(i64 64, i64 %2)
LLVM ERROR: Broken module found, compilation aborted!
@norhh
Copy link
Author

norhh commented Feb 5, 2020

Got a similar error for core-utils-8.31 when run on ls

@MartinNowack
Copy link
Contributor

@norhh Can you try master? This should be fixed already.

@norhh
Copy link
Author

norhh commented Feb 6, 2020

It doesn't seem to work. Got the same error. Check out the Dockerfile which I used.

FROM ubuntu:18.04

ARG DEBIAN_FRONTEND=noninteractive
RUN apt-get update && apt-get upgrade -y && apt-get autoremove -y

RUN apt-get install -y build-essential \
                       curl \
                       wget \
                       libcap-dev \
                       git \
                       cmake \
                       libncurses5-dev \
                       python-minimal \
                       python-pip \
                       python3 \
                       python3-pip \
                       unzip \
                       libtcmalloc-minimal4 \
                       libgoogle-perftools-dev \
                       zlib1g-dev \
                       libsqlite3-dev \
                       doxygen
                       

ENV LLVM_VERSION=6.0

RUN apt-get install -y clang-${LLVM_VERSION} \
                       llvm-${LLVM_VERSION} \
                       llvm-${LLVM_VERSION}-dev \
                       llvm-${LLVM_VERSION}-tools

ENV Z3_VERSION=4.8.4

WORKDIR /z3

RUN wget -qO- https://github.com/Z3Prover/z3/archive/z3-${Z3_VERSION}.tar.gz | tar xz --strip-components=1 && \
    python scripts/mk_make.py && \
    cd build && \
    make && \
    make install

ENV PATH=/usr/lib/llvm-${LLVM_VERSION}/bin/:${PATH}

ENV KLEE_UCLIBC_VERSION=klee_0_9_29

WORKDIR /klee-uclibc

RUN git clone https://github.com/klee/klee-uclibc.git . && \
    git checkout ${KLEE_UCLIBC_VERSION} && \
    CC=clang ./configure --make-llvm-lib && \ 
    make -j2

ENV KLEE_VERSION=2.0

WORKDIR /klee

RUN git clone https://github.com/klee/klee . && \
    mkdir build && \
    cd build && \
    cmake \
        -DENABLE_SOLVER_Z3=ON \
        -DENABLE_POSIX_RUNTIME=ON \
        -DENABLE_KLEE_UCLIBC=ON \
        -DKLEE_UCLIBC_PATH=/klee-uclibc \
        -DENABLE_UNIT_TESTS=OFF \
        -DENABLE_SYSTEM_TESTS=OFF \
            .. && \
    make

ENV PATH=/klee/build/bin/:${PATH}

ENV LLVM_COMPILER=clang

RUN python -m pip install --upgrade pip && python -m pip install wllvm

COPY klee-example/ /klee-example

WORKDIR /klee-example

@kren1
Copy link
Contributor

kren1 commented Feb 7, 2020

See #937 . I guess the easiest fix is to strip debug info with opt

@ccadar ccadar added this to Possibly related bug reports in Retiring LLVM <6 Mar 3, 2020
@SuperSadGuy23
Copy link

@kren1
Using opt to strip debug-info gives me this error:
KLEE: WARNING ONCE: calling external: g_strdup_printf(94725645800528, 94725644597424) at [no debug info]
KLEE: ERROR: (location information missing) failed external call: g_strdup_printf

Any helps?
Selection_001

@kren1
Copy link
Contributor

kren1 commented Mar 4, 2020

That seems like a glib function. That means you need to compile glib with wllvm too.

@ccadar
Copy link
Contributor

ccadar commented Jul 28, 2020

I think since we have #937 open we can close this, but please re-open if needed.

@ccadar ccadar closed this as completed Jul 28, 2020
@ccadar ccadar removed this from Possibly related bug reports in Retiring LLVM <6 Sep 29, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

5 participants