Sets of States at Each Program Point

Consider the program

i = 0;
while (i < 10) {
if (i > 1)
i = i + 3;
else
i = i + 2;
}

A possible corresponding control-flow graph is:

Suppose that

• program state is given by the value of the integer variable i
• initially, it is possible that i has any value

Compute the set of states at each vertex in CFG

For each program point we associate a set of states , , …, .

Running the Program

One way to describe the set of state: for each initial state, run the CFG with this state and insert the modified states at appropriate points.

Reachable States as A Set of Recursive Equations

If is the label on the edge of the graph, let denote the relation between initial and final state that describes the meaning of statement. For example,

We will write for the image of set under relation . For example,

Note that that if [p] is a condition (as generated by 'if' and 'while') then

If an edge has no label, we denote it skip. So, .

Now, we can describe the meaning of our program using recursive equations:

Note that the solution we computed satisfies the recursive equations. In fact, our solution is the unique least solution of these equations.

The problem with these exact equations is that they are as difficult to compute as running the program on all possible input states. Instead, when we do data-flow analysis, as with type systems, we will consider approximate descriptions of these sets of states.