In order to optimize a program, I am trying to figure out how the idea of a lattice applies to data-flow graphs, as introduced by this presentation (first diagram below). The lattice seems to take a program, order its inputs and outputs, and allow for easily determining flow of variables and state, so you can perform verification and optimization. But I am not sure how to construct the lattice from the program statements.
In this question I would like to know how to construct the lattice from the program.
Specifically, given a program such as this:
var x = 10
var y = 20
var z = 0
var i = z
while (i < x) {
y = y + x * i
i = i + 1
z = y + i
}
We can construct a Control-Flow Graph (CFG) where each node is a program statement such as var x = 10. From that we can construct a Data-Flow Graph (DFG) where we are keeping track of how a variable is used. This creates an def-use ordering, along the lines of:
x, y, i at the same time
z comes after i
...
That's where I start getting lost. But once we have a partial ordering, somehow a lattice is created. Finally from the lattice, we can do things such as doing pointer analysis (Figure 2) and computing fix-points (Figure 3). That will help in optimization and verification of the program.
I'm wondering only the first part, how to construct the lattice from the example program above. Wondering what is needed to construct the lattice at a high-level. I understand the upper and lower bounds of a lattice, which seems to correspond to CFG inputs and outputs being joined, but I don't quite see how to actually do the join (meet), what the nodes/vertices are in the lattice (not sure if it's a single program statement, a variable, or what), and what the edges are in the lattice. Once that is defined, then doing the rest of the stuff should be straightforward. Thank you for your help.
^- Figure (1).
^- Figure (2).
^- Figure (3).
