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 {D_k}, where D_k 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 D_k ⊙ D_k-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., D₁ ⊙ D₁-reachability) of bidirected InterDyck-reachability. In D₁ ⊙ D₁-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 D₁ ⊙ D₁ problem is in PTIME. We also show that when one extends each Dyck language to involve k different kinds of parentheses (i.e., D_k ⊙ D_k-reachability), the problem is NP-hard (and therefore much harder).

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