CFL-based methods for approximating interleaved Dyck reachability

Abstract Interleaved Dyck Reachability is a standard, graph-based formulation of a plethora of static analyses that seek to be context- and field- sensitive, where each type of sensitivity is expressed via a CFL/Dyck language. Unfortunately, the problem is well known to be undecidable in general, and thus existing approaches resort to clever overapproximations. Recently, a mutual-refinement algorithm, that iteratively considers each of the two sensitivities in isolation until a fixpoint is reached, was shown to achieve high precision. In this work we present a more precise approximation of Interleaved Dyck Reachability, by extending the mutual-refinement algorithm in three general directions. First, we develop refined CFLs to express each type of sensitivity precisely, while simultaneously also lightly overapproximating the opposite type. Second, we modify the graph information in a way to highlight unreachable paths not previously captured by the algorithm. Third, we apply the resulting algorithm on an on-demand basis, which effectively masks out imprecision incurred by parts of the graph that are irrelevant for the query at hand. Our experiments show that the new approach offers significantly higher precision than the vanilla mutual-refinement algorithm and other common baselines; for a particularly challenging benchmark, we report, on average, $51\%$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mn>51</mml:mn> <mml:mi>%</mml:mi> </mml:math> of the reachable pairs compared to the most recent alternative.