Function Pointer Eliminator for C Programs

Verification of memory safety such as absence of null pointer dereferences and memory leaks in system software is important in practice. O'Hearn's group proposed a new method of memory safety analysis/verification by modular abstract interpretation with separation logic and biabduction. To realize this method, one has to construct a call graph before the modular abstract interpretation. This paper aims to analyze/verify memory safety of system software written in C programming language by this method, and as the first step this paper provides a function pointer eliminator tool to eliminate function pointer calls in order to construct a call graph. The tool uses SVF for pointer analysis. First C programs are translated into LLVM programs by Clang and then SVF analyses the LLVM programs. The tool given in this paper finds correspondence between function pointer calls in C programs and those in LLVM programs, and transforms the C programs into C programs with the same functionality and without any function pointer calls. The experimental results for gzip, git, and OpenSSL using this function pointer eliminator are presented and they show that this tool is sufficiently efficient and precise for the purpose.