On the complexity of bidirected interleaved Dyck-reachability

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 𝐷 𝑘 , where 𝐷 𝑘 has 𝑘 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 𝐷 𝑘 ⊙ 𝐷 𝑘 -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 ⟨𝑝, 𝑞⟩ labeled by an open parenthesis "( 𝑎 ", there is an edge ⟨𝑞, 𝑝⟩ labeled by the corresponding close parenthesis ") 𝑎 ", and vice versa. Language-reachability on a bidirected graph has proven to be useful both (i) in its own right, as a way to formalize many program-analysis problems, such as pointer analysis, and (ii) 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., 𝐷 1 ⊙ 𝐷 1 -reachability) of bidirected InterDyck-reachability. In 𝐷 1 ⊙ 𝐷 1 -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 𝐷 1 ⊙ 𝐷 1 -reachability problem is in PTIME. We also show that when one extends each Dyck language to involve 𝑘 different kinds of parentheses (i.e., 𝐷 𝑘 ⊙ 𝐷 𝑘 -reachability with 𝑘 ≥ 2), the problem is NP-hard (and therefore much harder).

We have implemented the polynomial-time algorithm for bidirected 𝐷 1 ⊙ 𝐷 1 -reachability. 𝐷 1 ⊙ 𝐷 1reachability provides a new over-approximation method for bidirected 𝐷 𝑘 ⊙ 𝐷 𝑘 -reachability in the sense that 𝐷 𝑘 ⊙ 𝐷 𝑘 -reachability can first be relaxed to bidirected 𝐷 1 ⊙ 𝐷 1 -reachability, and then the resulting bidirected 𝐷 1 ⊙ 𝐷 1 -reachability problem is solved precisely. We compare this 𝐷 1 ⊙ 𝐷 1 -reachability-based approach against another known over-approximating 𝐷 𝑘 ⊙ 𝐷 𝑘 -reachability algorithm. Surprisingly, we found that the over-approximation approach based on bidirected 𝐷 1 ⊙ 𝐷 1 -reachability computes more precise solutions, even though the 𝐷 1 ⊙ 𝐷 1 formalism is inherently less expressive than the 𝐷 𝑘 ⊙ 𝐷 𝑘 formalism.