Compilers and Translators:
Software Verification Tools
Lecture 6: Foundations of Data-Flow Analysis
September 20, 2007
- 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
- Introduction to data-flow analysis
- Data-flow schemas
- Reaching definitions
- Live-variable analysis
2. Available Expressions
- 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.
3. Basic Questions about the Iterative Algorithm
- 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?
4. Lattices and Semilattices
- 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.
5. Data-Flow Analysis Frameworks
- Definition of a data-flow analysis framework.
- Transfer functions.
- Monotone frameworks.
- Distributive frameworks.
6. The Iterative Algorithm for General 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.
7. Meaning of a Data-Flow Solution
- For a forward data-flow framework, the IDEAL[B] solution for a block B is the meet over all
feasible paths P of fP(vENTRY).
- 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.