Pearl: A Multi-Derivation Approach to Efficient CFL-Reachability Solving

Context-free language (CFL) reachability is a fundamental framework for formulating program analyses. CFL-reachability analysis works on top of an edge-labeled graph by deriving reachability relations and adding them as labeled edges to the graph. Existing CFL-reachability algorithms typically adopt a single-reachability relation derivation (SRD) strategy, i.e., one reachability relation is derived at a time. Unfortunately, this strategy can lead to redundancy, hindering the efficiency of the analysis. To address this problem, this paper proposes <small>Pearl</small>, a <i>multi-derivation</i> approach that reduces derivation redundancy for CFL-reachability solving, which significantly improves the efficiency of CFL-reachability analysis. Our key insight is that multiple edges can be simultaneously derived via batch propagation of reachability relations. We also tailor our multi-derivation approach to tackle transitive relations that frequently arise when solving CFL-reachability. Specifically, we present a highly efficient transitive-aware variant, <small>Pearl^PG</small>, which enhances <small>Pearl</small> with <i>propagation graphs</i>, a lightweight but effective graph representation, to further diminish redundant derivations. We evaluate the performance of our approach on two clients, i.e., context-sensitive value-flow analysis and field-sensitive alias analysis for C/C++. By eliminating a large amount of redundancy, our approach outperforms two baselines including the standard CFL-reachability algorithm and a state-of-the-art solver <small>Pocr</small> specialized for fast transitivity solving. In particular, the empirical results demonstrate that, for value-flow analysis and alias analysis respectively, <small>Pearl^PG</small> runs 3.09<inline-formula><tex-math notation="LaTeX">$\times$</tex-math></inline-formula> faster on average (up to 4.44<inline-formula><tex-math notation="LaTeX">$\times$</tex-math></inline-formula>) and 2.25<inline-formula><tex-math notation="LaTeX">$\times$</tex-math></inline-formula> faster on average (up to 3.31<inline-formula><tex-math notation="LaTeX">$\times$</tex-math></inline-formula>) than <small>Pocr</small>, while also consuming less memory.