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.