Semantic Foundations of Data Flow Analysis

Abstract

Abstract Interpretation (P. Cousot, R. Cousot and others) is a method for program analysis that is able to describe many data flow analyses. We investigate and weaken the assumptions made in abstract interpretation and express abstract interpretation within Denotational Semantics. As an example we specify constant propagation.

Some authors have used abstract interpretation to formulate ''available expressions'' (a so-called ''history-sensitive'' data flow analysis). Our development of ''available expressions'' is better justified, semantically.

In traditional data flow analysis and abstract interpretation it is generally assumed that the ''Meet Over all Paths'' solution is wanted. We prove that the solution specified by our approach is the ''Meet Over all Paths'' solution to a certain system of equations obtained from the program.

To indicate the usefulness of our approach we show how to validate a class of program transformations, including ''constant folding''.

Throughout this paper we use a toy language consisting of declarations, expressions and commands (involving conditional and iteration). Excluded are procedures and jumps.