Region Analysis for Imperative Languages

This paper presents a region inference framework designed specifically for imperative programs with dynamic allocation and destructive updates. Given an input program, the algorithm automatically translates it into an output program with region annotations on procedures and allocation commands, and with explicit region creation and removal commands. Our framework formulates the analysis problem as a three-step algorithm. In the first phase, it infers region annotations for record declarations in the input language. Second, it performs a unification-based flow analysis of the program, inferring region types at each point in the program. In particular, it determines region types for allocation commands and procedure calls. In the third phase, it uses a single-pass algorithm to inspect each point in the program and insert region creation and removal commands in the control flow of the output program. This transformation ensures that regions are live whenever they are being used, while minimizing region lifetimes. The algorithm is simple, efficient, and provably correct. Furthermore, we show that the framework can be extended with more aggressive analyses (at the expense of making it less modular or more complex), such as interprocedural region liveness or shape analysis, to further improve the accuracy and performance of memory management. More generally, our framework allows existing analysis technology for imperative languages, such as points-to or shape analysis, to be easily integrated and applied to the region inference problem