Abstract Interpretation of Unstructured Imperative Languages on Unbounded Domains

Abstract: In this thesis we present a novel program analysis technique that applies abstract interpretation to low-level intermediate languages with unbounded abstract domains. Unbounded abstract domains in program analysis occur in applications such as finding ranges of variables and its applications include elimination of assertions in programs, automatically deducing numerical stability, and array bounds checking. Unbounded abstract domains impose a major challenge in program analysis because it is difficult to ensure the termination of the analysis in the presence of program cycles. State-of-the-art methods propose a technique that relies on a structured composition of programs, e.g., they permit abstract interpretation with unbounded abstract domains for program languages that have while and if statements but do not have goto statements. This work demonstrates that unbounded abstract domains can be employed in program analysis for low-level intermediate languages commonly used in program language tools including compilers, integrated-development environments, and bug-checkers, where loops are implicit within the control flow graph. Our work combines methods of elimination-based data flow analysis with abstract interpretation. We have implemented the proposed framework in the LLVM compiler framework as a program analysis pass and have conducted experiments with a suite of test programs to show the feasibility of our approach.