Dataflow framework for global analysis: Why meet, then apply?

Question

In Chapter 9 of the Dragon Book, the authors describe the dataflow framework for global analysis (described also in these slides). In this framework, an analysis is defined by a set of transfer functions, along with a meet semilattice.

At each step of the iteration, the algorithm works by maintaining two values for each basic block: an IN set representing information known to be true on input to the basic block, and an OUT set representing information known to be true on output from the basic block. The algorithm works as follows:

1. Compute the meet of the OUT sets for all predecessors of the current basic block, and set that value as the IN set to the current basic block.
2. Compute $f(IN)$ for the current basic block, where $f$ is a transfer function representing the effects of the basic block. Then set OUT for this block equal to this value.

I am confused about why this algorithm works by taking the meet of all the input blocks before applying the transfer function. In some cases (non-distributive analyses), this causes a loss of precision. Wouldn't it make more sense to apply the transfer function to each of the OUT values of the predecessors of the given block, then to meet all of those values together? Or is this not sound?

Thanks!

Answer 1

It's the classic precision/efficiency tradeoff. You can, in fact, move the meet outside, since $f(x \sqcap y) \sqsubseteq f(x) \sqcap f(y)$. A canonical example of where this makes a difference is in the following constraint-propagation problem:

IF b
  x = 1
ELSE
  x = -1

y = x*x

The Dragon Book's suggestion will compute $(x=1) \sqcap (x=-1)=\top$ before evaluating $x*x$, and will thus not capture that $y$ is a constant. By computing the meet after (twice) evaluating the multiplication, yours will. What you have effectively done is added a small amount of path-sensitivity, for a small price in efficiency. You can continue down this path arbitrarily. Two steps of this analysis may compute $f(f(w\sqcap x) \sqcap f(y\sqcap z))$. Your suggestion would instead compute $f(f(w)\sqcap f(x)) \sqcap f(f(y) \sqcap f(z))$, but you can take this farther and increase the path-sensitivity by computing $f(f(w))\sqcap f(f(x))\sqcap f(f(y)) \sqcap f(f(z))$. The fully path-sensitive MOP (meet-over-paths) solution is undecidable. The Dragon Book's algorithm gives an MFP (maximal fixed point) solution, which safely approximates the MOP. You've simply refined the approximation a bit.