Inferring Region Types via an Abstract Notion of Environment Transformation

Region-based type systems are a powerful tool for various kinds of program analysis. We introduce a new inference algorithm for region types based on an abstract notion of environment transformation. It analyzes the code of a method only once, even when there are multiple invocations of the method of different region types in the program. Elements of such an abstract transformation are essentially constraints for equality and subtyping that capture flow information of the program. In particular, we work with access graphs in the definition of abstract transformations to guarantee the termination of the inference algorithm, because they provide a finite representation of field access paths.Comment: To appear at APLAS'22; arXiv version contains appendices on the construction of concatenation and join for abstract transformations and an example of type inferenc