Static Analysis by Elimination

In this paper we describe a program analysis technique for finding value ranges for variables in the LLVM compiler infrastructure. Range analysis has several important applications for embedded systems, including elimination of assertions in programs, automatically deducing numerical stability, eliminating array bounds checking, and integer overflow detection. Determining value ranges poses a major challenge in program analysis because it is difficult to ensure the termination and precision of the program analysis in the presence of program cycles. This work uses a technique where loops are detected intrinsically within the program analysis. Our work combines methods of elimination-based data flow analysis with abstract interpretation. We have implemented a prototype of the proposed framework in the LLVM compiler framework and have conducted experiments with a suite of test programs to show the feasibility of our approach.