Symbolic Program Analysis in Almost-Linear Time

This paper describes an algorithm to construct, for each expression in a given program text, a symbolic expression whose value is equal to the value of the text expression for all executions of the program. We call such a mapping from text expressions to symbolic expressions a cover. Covers are useful in such program optimization techniques as constant propagation and code motion. The particular cover constructed by our methods is in general weaker than the covers obtainable by the methods of Ki, FKU, RL, R2 but our method has the advantage of being very efficient. It requires O (m (m, n) + l) operations if extended bit vector operations have unit cost, where n is the number of vertices in the control flow graph of the program, m is the number of edges, l is the length of the program text, and is related to a functional inverse of Ackermann’s function T2. Our method does not require that the program be well-structured nor that the flow graph be reducible.