Undecidability of context-sensitive data-dependence analysis

Abstract

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 (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 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 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 are taken into account) are also undecidable.