Paper Info
Title
On the complexity of bidirected interleaved Dyck-reachability
Abstract
Many program analyses need to reason about pairs of matching actions, such as call/return, lock/unlock, or set-field/get-field. The family of Dyck languages {Dk}, where Dk has k kinds of parenthesis pairs, can be used to model matching actions as balanced parentheses. Consequently, many program-analysis problems can be formulated as Dyck-reachability problems on edge-labeled digraphs. Interleaved Dyck-reachability (InterDyck-reachability), denoted by Dk ⊙ Dk-reachability, is a natural extension of Dyck-reachability that allows one to formulate program-analysis problems that involve multiple kinds of matching-action pairs. Unfortunately, the general InterDyck-reachability problem is undecidable. In this paper, we study variants of InterDyck-reachability on bidirected graphs, where for each edge ⟨ p, q ⟩ labeled by an open parenthesis ”(a”, there is an edge ⟨ q, p ⟩ labeled by the corresponding close parenthesis ”)a”, and vice versa. Language-reachability on a bidirected graph has proven to be useful both (1) in its own right, as a way to formalize many program-analysis problems, such as pointer analysis, and (2) as a relaxation method that uses a fast algorithm to over-approximate language-reachability on a directed graph. However, unlike its directed counterpart, the complexity of bidirected InterDyck-reachability still remains open. We establish the first decidable variant (i.e., D1 ⊙ D1-reachability) of bidirected InterDyck-reachability. In D1 ⊙ D1-reachability, each of the two Dyck languages is restricted to have only a single kind of parenthesis pair. In particular, we show that the bidirected D1 ⊙ D1 problem is in PTIME. We also show that when one extends each Dyck language to involve k different kinds of parentheses (i.e., Dk ⊙ Dk-reachability with k ≥ 2), the problem is NP-hard (and therefore much harder). We have implemented the polynomial-time algorithm for bidirected D1 ⊙ D1-reachability. Dk ⊙ Dk-reachability provides a new over-approximation method for bidirected Dk ⊙ Dk-reachability in the sense that Dk⊙ Dk-reachability can first be relaxed to bidirected D1 ⊙ D1-reachability, and then the resulting bidirected D1 ⊙ D1-reachability problem is solved precisely. We compare this D1 ⊙ D1-reachability-based approach against another known over-approximating Dk ⊙ Dk-reachability algorithm. Surprisingly, we found that the over-approximation approach based on bidirected D1 ⊙ D1-reachability computes more precise solutions, even though the D1⊙ D1 formalism is inherently less expressive than the Dk⊙ Dk formalism.
Year
DOI
Venue
2021
10.1145/3434340
Proceedings of the ACM on Programming Languages
Keywords
DocType
Volume
Complexity,Formal Language Graph Reachability,Interleaved-Dyck Language,Static Analysis
Journal
5
Issue
ISSN
Citations 
POPL
2475-1421
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Yuanbo Li111.03
Qirun Zhang21078.40
Thomas W. Reps3395.67