Phase 1: Transfer Functions

The symbolic behavior of a region R is a relative map describing every variable's value on exit in terms of enclosing loop indices and variable values on entry to R. The following operations are defined:

• : forms a map showing the effect of the block on every program variable: unmodified variables are mapped to themselves, modified variables are mapped to a symbolic value expression representing the value on exit in terms of the values on entry. New variables are introduced to represent the values of certain operations with unknown results (e.g., load from memory, I/O read). These variables are limited in scope to the nearest enclosing loop or procedure body.

• Composition (): apply to every bound value in :

  

• Meet (), with identity element :

  

• Iteration: finds loop invariants and induction variables and rephrases them in terms of the given index variable i. Auxiliary maps (loop invariants) and (induction variables) are used to compute , as follows:

  

  gives the net change after i iterations of the loop, and includes loop invariant and induction variable recognition.

• Closure: substitutes an expression if then else 0 for the most recent loop index variable i throughout .
• : maps formals to actuals everywhere in .