Undecidability of Context-Sensitive Data-Dependence Analysis

Thomas Reps
University of Wisconsin

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 of 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 parentheses:

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 using parentheses that match as the labels on edges that run from a to c and c to d, and using parentheses that do not match as the labels on edges that run from b 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 paper answers the question in the negative: In general, the problem of context-sensitive, structure-transmitted data-dependence analysis is undecidable.

The results of this paper imply that, in general, both context-sensitive set-based analysis and infinity-CFA (when data constructors and selectors are taken into account) are also undecidable.

(Click here to access the paper.)