Improving KLEE support

[dukc]

Description

BetterC D code can already be analyzed with KLEE, a LLVM bitcode verification tool. See https://theartofmachinery.com/2019/05/28/d_and_klee.html for great introduction. The idea is that some or all regular D features would be made compatible with the tool.

What are rough milestones of this project?

1. Take a simple better C program, which can be analyzed now. Get that analyzed without using the -betterC switch, linking to DRuntime instead. Document how others can do the same.

2. Get KLEE to analyze code using other DRuntime features. Submit required DRuntime changes upstream. Not everything needs to work, port what is reasonable. If... no, when you find DRuntime bugs from KLEE reports, report then to Bugzilla. You may also fix them.

3. If time remains, use KLEE to debug our toolchain, preferably the D compilers or DUB. Give a conference talk or write a post about the experience.

How does this project help the D community?

D already has good mechanical bug-preventing when it comes to memory safety. KLEE lets us to mechanically check for other sorts of problems too, much more comprehensively than the type system practically allows.

We might also get some toolchain bugs discovered and fixed.

Recommended skills

-Some understanding of how compilers work. Experience with LLVM IR is plus but not necessary.

What can students expect to get out of doing this project?

-Experience with LLVM toolchain and compilers in general
-Experience with DRuntime
-A good start in using a very effective bug-finder

References

https://theartofmachinery.com/2019/05/28/d_and_klee.html - a great introduction from D prespective
https://klee.github.io/ - KLEE homepage
http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf - the original research paper of the tool. Encouraging read.

[maxhaton]

I have just started fiddling around with bolting Z3 onto the dmd-frontend, so it may be possible to attack this area from both sides eventually.

[sarneaud]

In theory, you could take the D runtime, stub out things like threading support, and make an LLVM bitcode build that links with non-betterC code that's runnable under KLEE. ldc2 has support for building bitcode runtimes for LTO, and I once had a go combining a bitcode build with a stub pthreads implementation to get a KLEE-compatible runtime but didn't get it working in the end. It should totally be doable for someone willing to put just a little more time into it, though.

Here's another use-case. When I translated Google's robots.txt parser from C++ to D, I used KLEE on the C++ code to generate a regression test suite. Being able to run KLEE on the D code, too, would have helped guard against D-specific bugs in translation (like accidental auto-decoding). In any case, KLEE is a great tool when translating code, and better D support would help make more native D versions of things. If someone got KLEE working on non-betterC code, and used it to verify some small library translated from (say) JavaScript or whatever, I'd call that a successful project and I'd want to see the talk at DConf :)

https://gitlab.com/sarneaud/unrobotstxt/-/blob/3ad717018166eb6590d267e7893555252ba60a6d/source/unrobotstxt/test_extra.d