A Better Approximation for Interleaved Dyck Reachability

TY - GEN

T1 - A Better Approximation for Interleaved Dyck Reachability

AU - Conrado, Giovanna Kobus

AU - Pavlogiannis, Andreas

N1 - Publisher Copyright: © 2024 Copyright held by the owner/author(s).

PY - 2024/6

Y1 - 2024/6

N2 - 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 as such, 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 two directions. First, we develop refined CFLs to express each type of sensitivity precisely, while simultaneously also lightly overapproximating the opposite type. Second, 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% of the reachable pairs compared to the most recent alternative.

AB - 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 as such, 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 two directions. First, we develop refined CFLs to express each type of sensitivity precisely, while simultaneously also lightly overapproximating the opposite type. Second, 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% of the reachable pairs compared to the most recent alternative.

KW - CFL Reachability

KW - Graphs

KW - Static Analysis

UR - http://www.scopus.com/inward/record.url?scp=85198622688&partnerID=8YFLogxK

U2 - 10.1145/3652588.3663318

DO - 10.1145/3652588.3663318

M3 - Article in proceedings

AN - SCOPUS:85198622688

SP - 18

EP - 25

BT - SOAP 2024 - Proceedings of the 13th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis

PB - Association for Computing Machinery

T2 - 13th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis, SOAP 2024, co-located with the 45th ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2024

Y2 - 25 June 2024

ER -