Solving Regular Tree Grammar Based Constraints

Yanhong A. Liu, Ning Li, Scott D. Stoller

To appear at Static Analysis Symposium (SAS01), Paris, France, 16-18 July 2001


Abstract

This paper describes the precise specification, design, analysis, implementation, and measurements of an efficient algorithm for solving regular tree grammar based constraints. The particular constraints are for dead-code elimination on recursive data, but the method used for the algorithm design and complexity analysis is general and applies to other program analysis problems as well. The method is centered around Paige's finite differencing, i.e., computing expensive set expressions incrementally, and allows the algorithm to be derived and analyzed formally and implemented easily. We study higher-level transformations that make the derived algorithm concise and allow its complexity to be analyzed accurately. Although a rough analysis shows that the worst-case time complexity is cubic in program size, an accurate analysis shows that it is linear in the number of live program points and in other parameters, including mainly the arity of data constructors and the number of selector applications into whose arguments the value constructed at a program point might flow. These parameters explain the performance of the analysis in practice. Our implementation also runs two to ten times as fast as a previous implementation of an informally designed algorithm.


Server START Conference Manager
Update Time 31 Mar 2001 at 16:55:39
Maintainer sas01@ens.fr.
Start Conference Manager
Conference Systems