[klee-dev] Updating KLEE-uClibc to the most recent version of uClibc

[Marko Dimjašević]

Hi KLEE devs and users,

In my efforts to run KLEE on a large collection of programs from
Debian, I've noticed there might be issues with KLEE-uClibc. As
Cristian Cadar pointed out in a discussion [1], upgrading KLEE-uClibc
to the most recent version of uClibc would be a good thing to do.
Therefore, I decided to give that a try.

Here I describe what I did along those lines and I ask for help and
comments. Note I'm no expert in C and I'm not familiar with uClibc's
code base.


At the moment KLEE-uClibc is based on the 0.9.29 version of uClibc.
This is around 8 years old. The most recent release of uClibc is
0.9.33.2 from May 2012. KLEE's version of the library has, if I am not
mistaken, a few dozen of commits on top of the upstream's 0.9.29
version: Dan Liew made 29 commits and Martin Nowack 2 commits. Some of
these KLEE-side commits are back-ports from more recent uClibc
releases. Am I right?

The KLEE-uClibc repo [2] has, among others, branches called
klee_0_9_29, 0_9_30, 0.9.31, 0.9.32, and 0.9.33. I assumed these are
for corresponding upstream releases.

I decided to do the update of the KLEE-uClibc library in steps. Every
step would correspond to upgrading KLEE-uClibc from one uClibc release
to the next release. Therefore, the hope is that even if I don't manage
to get all the way to the most recent version 0.9.33.2, at least I
might get a more recent version than what is there now.

My first upgrade to 0.9.30 is here:

https://github.com/mdimjasevic/klee-uclibc/tree/klee_0_9_30

This is how I did it. First I cloned the klee-uclibc repo [2]. I
created a new branch called klee_0_9_30 based on the klee_0_9_29
branch. Then I tried to merge from branch 0_9_30. Most of the files
were successfully merged automatically, but around 50 files had
conflicts that had to be resolved manually. In doing this, I read
commits and corresponding messages of Dan and Martin to see what they
did and why. I am not saying I understood everything, but I tried to
make sense of it. When in doubt, I preferred a change from the 0_9_30
branch.

The klee_0_9_30 branch compiles. I am not saying I haven't introduced
any errors in the merge. It's very likely I have. I compiled KLEE 1.2.0
along with KLEE-uClibc's klee_0_9_30 branch. I also ran regression
tests that KLEE has, but I'm not sure how many of them (if any) utilize
the C library. If none utilize it, probably it'd be a good idea to have
such tests as well for cases when KLEE is configured with the
--with-uclibc parameter.

Next, I ran it on amd64 on a few programs I've been looking at. This is
where I run into problems. For example, if I run KLEE on dc.bc like
this:

$ klee -max-time=30 -libc=uclibc --posix-runtime dc.bc
KLEE: NOTE: Using klee-uclibc : /usr/lib/klee/runtime/klee-uclibc.bca
KLEE: NOTE: Using model: /usr/lib/klee/runtime/libkleeRuntimePOSIX.bca
KLEE: output directory is "/tmp/tmp.NntD0fHoAJ/buildd/tmp.k2RqlRwscq/usr/bin/klee-out-4"
Using STP solver backend
KLEE: WARNING: undefined reference to function: __ctype_b_loc
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 41031664)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: __syscall_rt_sigaction: silently ignoring

KLEE: HaltTimer invoked
KLEE: halting execution, dumping remaining states

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



I reach the 30-second timeout whereas it finishes just fine when I run
the same command, but that was compiled against KLEE-uClibc's
klee_0_9_29 branch. If you're interested, the dc.bc file is here:

http://soarlab.org/files/klee/bug-reports/klee-uclibc/klee_0_9_30/dc.bc


I've been promising to package KLEE to a Debian package. Once KLEE
moves to LLVM 3.6, that will be doable as new Debian packages depending
on LLVM have to depend on at least LLVM 3.6. One benefit of packaging
is that we'll be able to build and test KLEE and KLEE-uClibc on
multiple processor architectures available on Debian build servers, and
in particular on those at the intersection of what uClibc has been
ported to and what Debian has been ported to [3]. (I do have a
work-in-progress version of the package for KLEE 1.2.0 based on LLVM
3.4 for the amd64 architecture.)


If you have any comments on the approach I've taken to update
KLEE-uClibc or on how to debug the issue with dc.bc above or on
anything related, I would appreciate it.


[1] https://github.com/klee/klee/issues/404#issuecomment-222302440
[2] https://github.com/klee/klee-uclibc
[3] https://www.debian.org/ports/


-- 
Kind regards,
Marko Dimjašević <marko at cs.utah.edu> .   University of Utah
https://dimjasevic.net/marko         . PGP key ID: 1503F0AA
Learn email self-defense!  https://emailselfdefense.fsf.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20160602/4f5db440/attachment.sig>