FlowCFL: A Framework for Type-based Reachability Analysis in the Presence of Mutable Data

TL;DR

FlowCFL introduces a type-based framework for precise reachability analysis in programs with mutable data, leveraging CFL-reachability semantics and inverse edges to improve accuracy and correctness.

Contribution

It defines a dynamic semantics for flow analysis, proves correctness of CFL-reachability with inverse edges, and establishes the equivalence and correctness of a new type-based reachability analysis.

Findings

Empirical results show improved precision by avoiding infeasible inverse edges.

Formal correctness proofs for the CFL-reachability approach.

Type-based analysis is proven equivalent to CFL-reachability semantics.

Abstract

Reachability analysis is a fundamental program analysis with a wide variety of applications. We present FlowCFL, a framework for type-based reachability analysis in the presence of mutable data. Interestingly, the underlying semantics of FlowCFL is CFL-reachability. We make three contributions. First, we define a dynamic semantics that captures the notion of flow commonly used in reachability analysis. Second, we establish correctness of CFL-reachability over graphs with inverse edges (inverse edges are necessary for the handling of mutable heap data). Our approach combines CFL-reachability with reference immutability to avoid the addition of certain infeasible inverse edges and we demonstrate empirically that avoiding those edges results in precision improvement. Our formal account of correctness extends to this case as well. Third, we present a type-based reachability analysis and establish equivalence between a certain CFL-reachability analysis and the type-based analysis, thus proving correctness of the type-based analysis.