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:
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 (i) a vertex for each variable, (ii) an edge from vertex i to vertex j when i is used on the right-hand side of an assignment to j, (iii) parentheses that match as the labels on edges that run from a to c and c to d, and (iv) parentheses that do not match as the labels on edges that run from b to c and c to d.
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: PostScript, PDF.)