[llvmlinux] Qualified type inference for Memory Analysis in the Linux Kernel

[Marcelo Sousa]

Hello all,

I have developed a static analysis tool for the Linux Kernel with a similar
goal of sparse, MECA and CQUAL; namely type qualifier inference to identify
misuses of different semantic pointers. The novelty of my tool is that
operates at the LLVM IR level and that also lifts some parts of inline
assembly that handle atomic instructions such as cmpxchg. The tool is quite
fast, takes less than 5 min to analyse the entire source code of x86.
However, the precision is dependent on an initial environment composed of
function signatures annotated with the qualified types.
At the moment, I'm trying to focus on separation of IO memory addresses and
regular memory addresses, i.e. the environment
annotates ioremap, ioremap_nocache, ioread*, iowrite* for IO mem and
kmalloc, kfree, etc. for regular mem.
The motivation for this particular analysis is the NVRAM e1000e, i.e. uses
of cmpxchg on an io memory address.
Since you are the experts in the Linux Kernel, I would like to get feedback
on this particular analysis: if you find it relevant and there are
particular use cases that you are interested in testing.

References to a complete API that handles IO pointers would be very
helpful. I'm also thinking on misuses of the DMA api. The tool is not
restricted to just pointer analysis but also we could specify qualified
types to have a struct type with different qualified types at the field
level.

Also, I'm quite interested in some of the finding of the Google summer
project on clang-analyser that can point me into a good direction too.

Finally, if you any contacts of people that might be interested in using
this sort of analysis that would be great.

Thanks a lot,
Marcelo
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.linuxfoundation.org/pipermail/llvmlinux/attachments/20130906/0c69626d/attachment.html>