A LOGIC-BASED APPROACH TO PROGRAM FLOW-ANALYSIS

A formalism is presented for tracking assertions which hold universall y, i.e., at the end of all the execution paths to a given program poin t, and assertions which hold existentialIy, i.e., at the end of some e xecution paths. In the formalism, the assertions which hold at a given execution path are uniformly defined by an entry environment which co ntains the assertions which hold when the execution of the program beg ins and an environment transformer for every program construct. The no vel aspect of our formalism is that Horn clauses are used to specify t he consistent environments and the meaning of program constructs. The best iterative algorithm (a notion defined by P. Cousot and R. Cousot) for tracking universal and existential assertions simultaneously is g iven. Conditions are presented under which the best iterative algorith m can be efficiently implemented. The formalism is applied to the poin ter equality problem in Pascal. It is shown that universal pointer equ alities may be used to reduce the number of superfluous existential eq ualities, and that existential equalities may be used to obtain more u niversal equalities. Recent empirical results indicate that tracking t he combination of may and must equalities leads to substantial improve ments in the result of the analysis. For programs without recursively defined records, the best iterative algorithm can be effectively imple mented. These results apply to multiple levels of pointers and can be extended to handle possibly recursive procedures. However, for program s with recursively defined data types further approximations are neces sary, e.g., by using a finite graph to model all the possible pointer equalities. For simplicity, this paper does not present an analysis al gorithm for this case.