KLEE abruptly halts before executing everything in tar

[norhh]

Description

When the following command on tar-1.32

> touch foo
> klee --libc=uclibc --posix-runtime --external-calls=all ./tar.bc -cvf archive.tar --verify foo

The verify part isn't executed.

....
....
KLEE: WARNING ONCE: calling external: textdomain(94914299277936) at [no debug info]
KLEE: WARNING ONCE: sigaction: silently ignoring
KLEE: WARNING ONCE: calling external: getpagesize() at [no debug info]
KLEE: WARNING ONCE: calling external: __strcpy_chk(94914244668480, 94914296842816, 18446744073709551615) at [no debug info]
KLEE: WARNING ONCE: calling external: dcgettext(0, 94914298909536, 5) at [no debug info]
KLEE: WARNING ONCE: calling external: __ctype_get_mb_cur_max() at [no debug info]
foo
foo: file changed as we read it
KLEE: ERROR: /klee/runtime/POSIX/fd.c:865: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 850768
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

Environment

Tar-1.32 is compiled with WLLVM, CFLAGS=-O1

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

[251]

Just a quick analysis:

• tar calls ioctl (archive, FDFLUSH); in compare.c
• KLEE's ioctl has no support for FDFLUSH
• the reason for the error is that KLEE calls buf = va_arg(ap, void*); although there is no further argument
• fix: implement FDFLUSH + call va_arg in every case and not before switch

[norhh]

@251 probably that's not the case, I removed the function and the error still persists.
But the error is at a different location, fprintf (stdlis, _("Verify "));

foo
foo: file changed as we read it
KLEE: WARNING ONCE: calling external: __fprintf_chk(93845108395352, 1, 93845123625088) at [no debug info]
KLEE: ERROR: (location information missing) failed external call: __fprintf_chk
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 864389
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

[251]

probably that's not the case

It is.

the error still persists

No, now you're getting a different error. You should use -g -O1 -Xclang -disable-llvm-passes -D__NO_STRING_INLINES -D_FORTIFY_SOURCE=0 -U__OPTIMIZE__ when you compile something to bitcode with newer versions of LLVM as stated in the documentation. Otherwise it replaces functions with "safer" (*_chk()) versions that have no model in KLEE.

[ccadar]

I'm closing this, as the need for _chk functions is recorded in #925