Compilers and Translators:

Software Verification Tools

Lecture 6: Foundations of Data-Flow Analysis

September 20, 2007

- Review
- Available expressions
- Basic questions about the iterative algorithm
- Lattices and semilattices
- Transfer functions
- The iterative algorithm for general frameworks
- Meaning of a data-flow solution
- Reading

- Introduction to data-flow analysis
- Data-flow schemas
- Reaching definitions
- Live-variable analysis

- Available expressions is a forward data-flow analysis problem similar to reaching definitions.
- We say an expression x + y is
*available*at a point p in a flow graph if every path from ENTRY to p evaluates x + y and between the last such evaluation and p there are no assignments tox or y. - A block kills x + y if it assigns x or y and does not subsequently recompute x + y.
- A block generates x + y if it evaluates x + y and does not subsequently define x or y.
- We can compute the set of generated expressions for each point in a block working from the beginning of the block to the end.
- Transfer equations and control-flow equations for available expressions: pp. 610-614.
- Iterative algorithm for available expressions: Alg. 9.17, p. 614.

- Basic questions
- When is the iterative algorithm correct?
- How precise is the solution?
- Under what conditions does the iterative algorithm converge?
- What is the meaning of the solution to the data-flow equations?

- The following definitions are fundamental (Sect. 9.3.1, pp. 618-623).
- Lattice vs. semilattice.
- Partial order defined by the meet operator of a semilattice.
- Greatest lower bound, least upper bound.
- Maximum fixed point.
- Lattice diagram (c.f., DAG, Hasse diagram).
- Product lattices.
- Height of a lattice.

- Definition of a data-flow analysis framework.
- Transfer functions.
- Monotone frameworks.
- Distributive frameworks.

- The iterative algorithm takes as input:
- A data-flow graph with an ENTRY and EXIT node.
- A direction, forward or backward.
- A set of values V for IN and OUT.
- A meet operator ∧ on V such that (V, ∧) forms a semilattice.
- A set of transfer functions for the blocks of the data-flow graph.
- A constant value for the boundary condition.
- The iterative algorithm produces as output the sets IN[B] and OUT[B] for each block B in the data-flow graph.
- The algorithm is given in Fig. 9.23, p. 627.
- Important properties of the algorithm:
- If the algorithm converges, the result is a solution to the data-flow equations.
- If the framework is monotone, the solution is the MFP of the data-flow equations.
- If the semilattice of the framework is monotone and of finite height, the algorithm is guaranteed to converge.

- For a forward data-flow framework, the IDEAL[B] solution for a block B is the meet over all
feasible paths P of f
_{P}(v_{ENTRY}). - Any answer greater than IDEAL is incorrect.
- Any answer smaller than or equal to IDEAL is safe.
- MOP[B], the meet over all paths solution, assumes that every path in the data-flow graph can be taken, but some of these paths may not be feasible. Thus, MOP[B] ≤ IDEAL[B] for all blocks B.
- The MFP solution is always smaller than or equal to the MOP solution. Therefore, MFP ≤ MOP ≤ IDEAL.

- ALSU: section 9.3

aho@cs.columbia.edu