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ć <[email protected]> . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org
signature.asc
Description: This is a digitally signed message part
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
