Optimal Interprocedural Code Motion: The IDFA-Algorithms

Abstract

In this chapter we present the interprocedural counterparts of the DFA-algorithms of Chapter 4. For every program property involved in the IBCMtransformation and ILCM -transformation we specify an IDFA-algorithm and prove it to be precise for the respective property. The specifications and the proofs of being precise follow the cookbook style of Section 9.2. Hence, the specifications consist of a lattice of data flow information, a local semantic functional, a return functional, a start information, and an interpretation of the lattice elements in the set of Boolean truth values. The proofs of being precise consist of four steps. Proving that the function lattice satisfies the descending chain condition, that the local semantic functions and the return functions are distributive, and finally, that the interprocedural meet over all paths solution is precise for the program property under consideration. All proofs are given in full detail in order to illustrate the similarities to their intraprocedural counterparts. For convenience, we identify throughout Chapter 11 the specification of an IDFA with the algorithm it induces (cf. Definition 8.6.1).