I am a bit late with a blog post this time around, but I implemented all things needed to have a Debile plugin for KLEE! While this is very exciting, I have to admit I haven’t tested it yet.
The past week I spent quite a lot of time trying to build a Debian package for KLEE. While I had a setup for building the package before, I needed something slightly different now. Up to now I would build KLEE for Debian Jessie, the current stable release. However, Debile is a package analysis infrastructure that is most useful for non-stable releases of Debian, e.g. Debian Testing (the current testing release is codenamed Stretch) and Debian Unstable (the usual Sid). Therefore, I need to figure out how to build KLEE for e.g. Debian Stretch, which has different packages and their versions than Debian Jessie and doesn’t have LLVM 3.4, which is what KLEE still depends on. I am still not done with figuring this out, but I have some ideas how to go about it.
The rest of the time I spent on finishing the Debile side of the story, namely providing a command, a runner, and a wrapper for KLEE. As I implemented support for outputting results in the Firehose format in KLEE itself, I believe the wrapper is not needed; nothing to wrap there. I wrote all of this blindly, i.e. without testing it. Therefore, in the remaining 10 or so days of time left for GSoC coding, I’ll be debugging this and fixing any issues I run into.
You can find my past/this week’s changes to Debile on the usual klee branch of my fork.