Type-based analysis for LLVM IR

I am interested in type-based verification of LLVM IR in the areas of certified compilation and software verification. It seems to me that the LLVM IR type system is rather informal in the sense that there is no paper with a proper formalization of the type rules, and for example, a proof of soundness for well-formedness of the code.
I would like to know if you are aware of any work in this direction for LLVM IR so that I can compare with my own implementation.
Moreover, it would be valuable to get some feedback on suitable type-based analysis that the LLVM community would like to have in the infrastructure.

Regards,
Marcelo

Hi Marcello,

It sounds like Vellvm could be interesting for you to consider

http://www.cis.upenn.edu/~jianzhou/Vellvm/

Regards,
  Roel

Can you explain what you mean by type-based verification? Do you mean that you want to use a set of typing rules to perform verification, or do you mean something else? Another important feature of the LLVM type system is that it is not a “safe” type system. It is possible to do all sorts of type unsafe things, such as casting integers to pointers and dereferencing them. One of the standard LLVM transforms (load widening) will generate loads that access memory past the end of a memory object. LLVM IR is capable of representing all the unsafe computations that C can do. The SAFECode/SVA work uses a points-to analysis called DSA which infers the types of memory objects. A key result of the work is that the points-to analysis/type inference results of DSA can be made sound at run-time. The original version of DSA, working on older versions of LLVM, was able to find a fairly decent number of type-safe memory objects. The SAFECode/SVA work developed a simple type checker that verified that the type-inference results returned by DSA are consistent (i.e., if DSA says that a memory object is used in a type-safe manner, then it is actually used in a type-safe manner). There is also some work by Greg Morrisett’s group at Harvard at creating a verified type-checker for the SAFECode/SVA system. SAFECode/SVA papers can be found at . As far as formalisms for the LLVM IR, there is one from University of Pennsylvania (Santosh Nagarakatte, now at Rutgers, was involved with that work), the one used by Greg Morrisett’s group for the verified type checker, and there might be one from Grigore Rosu’s group here at the University of Illinois. There is also an LLVM translation validator from Greg Morrisett’s group (). I think another person wrote asking about translation validation a few months ago. You might want to search the llvmdev archives for that conversation. LLVM already as a type-based alias analysis (called TBAA) which is used for optimization. There’s a proposal floating around on the list to improve it; you might want to take a look at that. SAFECode can use type-safety to optimize away load/store checks (provided that it uses garbage collection or automatic pool allocation to make the optimization sound). Using TBAA instead of DSA might generate better results. Address Sanitizer (ASan) might benefit from that optimization as well. Automatic pool allocation could also benefit from something like TBAA. I think you’ll have to be more specific, though, on what you mean by type-based analysis and provide details on how it could be applied. I apologize if my response is a bit of a ramble; I’m basically providing a bit of information hoping that some of it is relevant to what you are asking. I hope you find some of it useful. – John T.

Hello,