Inferring Region Types via an Abstract Notion of Environment Transformation

TL;DR

This paper presents a novel inference algorithm for region types that uses an abstract environment transformation, enabling efficient analysis of methods with multiple invocation types by leveraging access graphs for termination guarantees.

Contribution

It introduces a new inference approach based on environment transformation and access graphs, improving analysis efficiency and termination guarantees in region-based type systems.

Findings

Analyzes code with a single method pass regardless of invocation types.

Uses access graphs to ensure finite and terminating inference.

Captures flow information through constraints for equality and subtyping.

Abstract

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.