Type-Preserving Flow Analysis and Interprocedural Unboxing (Extended Version)

TL;DR

This paper extends interprocedural flow analysis to typed programs, enabling type-preserving unboxing optimizations that are safe, modular, and maintain program semantics and garbage collector correctness.

Contribution

It introduces a type-preserving interprocedural flow analysis framework and proves the correctness and modularity of a typed unboxing optimization.

Findings

Unboxing optimization preserves program semantics.

The analysis maintains type and GC safety.

Optimization can be applied modularly to separate program components.

Abstract

Interprocedural flow analysis can be used to eliminate otherwise unnecessary heap allocated objects (unboxing), and in previous work we have shown how to do so while maintaining correctness with respect to the garbage collector. In this paper, we extend the notion of flow analysis to incorporate types, enabling analysis and optimization of typed programs. We apply this typed analysis to specify a type preserving interprocedural unboxing optimization, and prove that the optimization preserves both type and GC safety along with program semantics. We also show that the unboxing optimization can be applied independently to separately compiled program modules, and prove via a contextual equivalence result that unboxing a module in isolation preserves program semantics.