Optimizing compilers attempt to understand programs in order to produce excellent code. One way in which they express their understanding is to transform a program into one embodying all of the information crucial to that program’s meaning, while providing no irrelevant information. Such transformations are hard to get right without mechanical verification.

Mechanical verification requires a model that defines the meaning of correctness. This paper describes PIM, an equational logic that models the transformations used to obtain the essential dataflow in an imperative program. PIM has a graphical form that is closely related to several common intermediate representations found in optimizing compilers. Common transformations carried out by these compilers can be modeled in PIM, and their correctness can be demonstrated according to that model.

The paper is concerned primarily with the theoretical properties of PIM, although a series of well-chosen examples illustrates the relationship between PIM and common optimization techniques. A small subset of C, incorporating integer operations and address arithmetic, is used to code the examples. The appendix shows how programs in this subset of C can be translated into PIM terms and PIM graphs.

As a practitioner rather than a theorist, I found this paper interesting as an indication of how the largely ad hoc process of optimization might be given a theoretical basis sufficient for producing optimizer generators. It also provides another potentially useful way of rigorously explaining dataflow analysis to students.