Undecidability of context-sensitive data-dependence analysis

A number of program-analysis problems can be tackled by transforming them into certain kinds of graph-reachability problems in labeled directed graphs. The edge labels can be used to filter out paths that are not interest: a path P from vertex s to vertex t only counts as a“valid connection” between s and t if the word spelled out by P is in a certain language. Often the languages used for such filtering purposes are languages of matching parantheses. In some cases, the matched-parenthesis condition is used to filter out paths with mismatched calls and returns. This leads to so-called “context-sensitive” program analyses, such as context-sensitive interprocedural slicing and context-sensitive interprocedural dataflow analysis. In other cases, the matched-parenthesis condition is used to capture a graph-theoretic analog of McCarthy's rules: “car (cons(x,y)) = x” and “cdr(cons(x,y)) =y”. That is, in the code fragment

c = cons(a,b); d = car(c);

the fact that there is a “structure-transmitted data-dependence” from a to d, but not from b to d, is captured in a graph by (1) using a vertex for each variable, (2)an edge from vertex i to vertex j when i is used on the right-hand side of an assignment to j, (3) parentheses that match as the labels on the edges that run from a to c and c to d, and (4) parentheses that do not match as the labels on the edges that run from a to c and c to d. However, structure-transmitted data-dependence analysis is context-insensitive, because there are no constraints that filter out paths with mismatched calls and returns. Thus, a natural question is whether these two kinds of uses of parentheses can be combined to create a context-sensitive analysis for structure-transmitted data-dependences. This article answers the question in the negative: in general, the problem of context sensitive, structure-transmitted data-dependence analysis is undecidable. The results imply that in general, both context-sensitive set-based analysis and ∞-CFA (when data constructors and selectors and selectors are taken into account) are also undecidable.