[klee-dev] LibC recommendations? [Re: Updating KLEE-uClibc to the most recent version of uClibc]

[Cristian Cadar]

Hi Marko,

Sorry for the delayed response.  I appreciate trying to upgrade KLEE's 
uClibc to the latest version.

However, if the latest available uClibC version is from 2012, I think we 
should investigate switching to other libC implementations.

I see there is a fork of uClibc which is maintained, so this would be 
one option:
http://tests.embedded-test.org/uClibc-ng/

I heard good things about musl too:
https://www.musl-libc.org/
I believe Martin has tried it with KLEE.

Does anyone have any suggestions/advice?

Best,
Cristian

On 03/06/16 04:19, Marko Dimjašević wrote:
> 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/
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>