[LLVMdev] [LLVM] What has happened to LLVM bitcode archive support?

Daniel Liew daniel.liew at imperial.ac.uk
Fri Dec 20 14:58:31 PST 2013


> Excuse me for the diversion but, is that interpreter of LLVM IR available
> somewhere? Details on how it works, performance, etc? I'd be interested

Yes it is available. The tool (KLEE [1]) is actually a lot more than
an interpreter (although it can be used as one). KLEE allows you to
mark certain variables (e.g. program inputs) as "symbolic". What this
means is that the variable marked as symbolic is allowed to have any
initially value and as program execution progresses, constraints are
gathered on the symbolic variable(s). Every time a conditional branch
is reached (e.g. if (x > 5) ) then KLEE will try to follow all
feasible paths and the record the constraints to each path (e.g. on
one path (x>5) and on the other (x <=5)).

The purpose of exploring these multiple paths is to

- Automatically generate test cases based
- Find bugs whilst exploring paths

If you don't mark any variables as symbolic then KLEE will just follow
a single path and so it acts just like an interpreter.

Unfortunately KLEE has not been that well maintained over the last few
years so the LLVM version that it builds against has slipped behind.
Several developers (including myself) are trying to upgrade it to work
correctly against LLVM 3.3. We have quite some way to go
unfortunately. It builds against LLVM3.3 but linking in our modified C
library (klee-uclibc [2]) doesn't work yet (which is why I'm asking
about bitcode archives) and some LLVM intrinsics and new instructions
added since LLVM2.7 aren't supported yet :(

We're getting there though! If you have any questions feel free to
drop a question on the KLEE mailing list.

If you'd rather read a paper then look at code then you could take a
look at the original 2008 OSDI paper [3].

[1] http://ccadar.github.io/klee/GetStarted.html (note these
instructions are for llvm 2.9 :( . Don't worry these instructions will
be updated eventually)
[2] https://github.com/ccadar/klee-uclibc/tree/klee_0_9_29
[3] http://llvm.org/pubs/2008-12-OSDI-KLEE.html

Thanks,
Dan Liew.



More information about the llvm-dev mailing list