LART – LLVM Abstraction and Refinement Tool

The goal of this tool is to provide LLVM-to-LLVM transformations that implement various program abstractions. The resulting programs are, in terms of the instruction set, normal, concrete LLVM programs that can be executed and analysed. Extra information about the abstraction(s) in effect over a (fragment of) a program is inserted using special LLVM intrinsic functions and LLVM metadata nodes.

LART provides both a standalone tool that processes on-disk bitcode files, as well as a framework that can be integrated into complex LLVM-based tools. The main motivation behind LART is to provide a “preprocessor” for LLVM-based model checkers and other analysis tools, simplifying their job by reducing the problem size without compromising soundness of the analyses.

The abstractions implemented by LART can be usually refined based on specific instructions about which “part” of the abstraction is too rough (an abstraction which is too rough will create spurious errors visible to subsequent analyses but not present in the original program).