Fast Graph Simplification for Interleaved Dyck-Reachability
Many program-analysis problems can be formulated as graph-reachability problems. Interleaved Dyck language reachability. Interleaved Dyck language reachability (InterDyck-reachability) is a fundamental framework to express a wide variety of program-analysis problems over edge-labeled graphs. The InterDyck language represents an intersection of multiple matched-parenthesis languages (i.e., Dyck languages). In practice, program analyses typically leverage one Dyck language to achieve context-sensitivity, and other Dyck languages to model data dependences, such as field-sensitivity and pointer references/dereferences. In the ideal case, an InterDyck-reachability framework should model multiple Dyck languages simultaneously.
Unfortunately, precise InterDyck-reachability is undecidable. Any practical solution must over-approximate the exact answer. In the literature, a lot of work has been proposed to over-approximate the InterDyck-reachability formulation. This paper offers a new perspective on improving both the precision and the scalability of InterDyck-reachability: we aim to simplify the underlying input graph $G$. Our key insight is based on the observation that if an edge is not contributing to any InterDyck-path, we can safely eliminate it from $G$. Our technique is orthogonal to the InterDyck-reachability formulation, and can serve as a pre-processing step with any over-approximating approaches for InterDyck-reachability. We have applied our graph simplification algorithm to pre-processing the graphs from a recent InterDyck-reachability-based taint analysis for Android. Our evaluation on three popular InterDyck-reachability algorithms yields promising results. In particular, our graph-simplification method improves both the scalability and precision of all three InterDyck-reachability algorithms, sometimes dramatically.
Fri 19 JunDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 17:00 | Static AnalysisPLDI Research Papers at PLDI Research Papers live stream Chair(s): Julian Dolby IBM Research, USA | ||
16:00 20mTalk | Automated Derivation of Parametric Data Movement Lower Bounds for Affine Programs PLDI Research Papers Auguste Olivry Inria, France, Julien Langou University of Colorado at Denver, USA, Louis-Noël Pouchet Colorado State University, USA, Saday Sadayappan University of Utah, USA, Fabrice Rastello Inria, France | ||
16:20 20mTalk | Fast Graph Simplification for Interleaved Dyck-Reachability PLDI Research Papers Yuanbo Li Georgia Institute of Technology, USA, Qirun Zhang Georgia Institute of Technology, USA, Thomas Reps University of Wisconsin-Madison, USA | ||
16:40 20mTalk | Static Analysis of Java Enterprise Applications: Frameworks and Caches, the Elephants in the Room PLDI Research Papers Anastasios Antoniadis University of Athens, Greece, Nikos Filippakis CERN, Switzerland, Paddy Krishnan Oracle Labs, Australia, Raghavendra Ramesh ConsenSys, Australia, Nicholas Allen Oracle Labs, Australia, Yannis Smaragdakis University of Athens, Greece Pre-print |