Solvers for dataflow inequations.

A forward dataflow problem is a set of inequations of the form

• X(s) >= transf n X(n) if program point s is a successor of program point n
• X(n) >= a if (n, a) belongs to a given list of (program points, approximations).

The unknowns are the X(n), indexed by program points (e.g. nodes in the CFG graph of a RTL function). They range over a given ordered set that represents static approximations of the program state at each point. The transf function is the abstract transfer function: it computes an approximation transf n X(n) of the program state after executing instruction at point n, as a function of the approximation X(n) of the program state before executing that instruction.

Symmetrically, a backward dataflow problem is a set of inequations of the form

• X(n) >= transf s X(s) if program point s is a successor of program point n
• X(n) >= a if (n, a) belongs to a given list of (program points, approximations).

The only difference with a forward dataflow problem is that the transfer function transf now computes the approximation before a program point s from the approximation X(s) after point s.

This file defines three solvers for dataflow problems. The first two solve (optimally) forward and backward problems using Kildall's worklist algorithm. They assume that the unknowns range over a semi-lattice, that is, an ordered type equipped with a least upper bound operation.

The last solver corresponds to propagation over extended basic blocks: it returns approximate solutions of forward problems where the unknowns range over any ordered type having a greatest element top. It simply sets X(n) = top for all merge points n, that is, program points having several predecessors. This solver is useful when least upper bounds of approximations do not exist or are too expensive to compute.

Solving forward dataflow problems using Kildall's algorithm

A forward dataflow solver has the following generic interface. Unknowns range over the type L.t, which is equipped with semi-lattice operations (see file Lattice).

fixpoint successors transf entrypoints is the solver. It returns either an error or a mapping from program points to values of type L.t representing the solution. successors is a finite map returning the list of successors of the given program point. transf is the transfer function, and entrypoints the additional constraints imposed on the solution.

The fixpoint_solution theorem shows that the returned solution, if any, satisfies the dataflow inequations.

The fixpoint_entry theorem shows that the returned solution, if any, satisfies the additional constraints expressed by entrypoints.

Finally, any property that is preserved by L.lub and transf and that holds for L.bot also holds for the results of the analysis.

Kildall's algorithm manipulates worklists, which are sets of CFG nodes equipped with a ``pick next node to examine'' operation. The algorithm converges faster if the nodes are chosen in an order consistent with a reverse postorder traversal of the CFG. For now, we parameterize the dataflow solver over a module that implements sets of CFG nodes.

We now define a generic solver that works over any semi-lattice structure.

The state of the iteration has two components:

• A mapping from program points to values of type L.t representing the candidate solution found so far.
• A worklist of program points that remain to be considered.

Kildall's algorithm, in pseudo-code, is as follows:

    while st_wrk is not empty, do
        extract a node n from st_wrk
        compute out = transf n st_in[n]
        for each successor s of n:
            compute in = lub st_in[s] out
            if in <> st_in[s]:
                st_in[s] := in
                st_wrk := st_wrk union {s}
            end if
        end for
    end while
    return st_in

The initial state is built as follows:

• The initial mapping sets all program points to L.bot, except those mentioned in the entrypoints list, for which we take the associated approximation as initial value. Since a program point can be mentioned several times in entrypoints, with different approximations, we actually take the l.u.b. of these approximations.
• The initial worklist contains all the program points.

propagate_succ corresponds, in the pseudocode, to the body of the for loop iterating over all successors.

propagate_succ_list corresponds, in the pseudocode, to the for loop iterating over all successors.

step corresponds to the body of the outer while loop in the pseudocode.

The whole fixpoint computation is the iteration of step from the start state.

Monotonicity properties

We first show that the st_in part of the state evolves monotonically: at each step, the values of the st_in[n] either remain the same or increase with respect to the L.ge ordering.

Correctness invariant

The following invariant is preserved at each iteration of Kildall's algorithm: for all program points n, either n is in the worklist, or the inequations associated with n (st_in[s] >= transf n st_in[n] for all successors s of n) hold. In other terms, the worklist contains all nodes that do not yet satisfy their inequations.

We show that the start state satisfies the invariant, and that the step function preserves it.

Correctness of the solution returned by iterate.

As a consequence of the good_state invariant, the result of fixpoint, if defined, is a solution of the dataflow inequations, since st_wrk is empty when the iteration terminates.

As a consequence of the monotonicity property, the result of fixpoint, if defined, is pointwise greater than or equal the initial mapping. Therefore, it satisfies the additional constraints stated in entrypoints.

Preservation of a property over solutions

Solving backward dataflow problems using Kildall's algorithm

A backward dataflow problem on a given flow graph is a forward dataflow program on the reversed flow graph, where predecessors replace successors. We exploit this observation to cheaply derive a backward solver from the forward solver.

Construction of the predecessor relation

Solving backward dataflow problems

The interface to a backward dataflow solver is as follows.

We construct a generic backward dataflow solver, working over any semi-lattice structure, by applying the forward dataflow solver with the predecessor relation instead of the successor relation.

Analysis on extended basic blocks

We now define an approximate solver for forward dataflow problems that proceeds by forward propagation over extended basic blocks. In other terms, program points with multiple predecessors are mapped to L.top (the greatest, or coarsest, approximation) and the other program points are mapped to transf p X[p] where p is their unique predecessor.

This analysis applies to any type of approximations equipped with an ordering and a greatest element.

The interface of the solver is similar to that of Kildall's forward solver. We provide one additional theorem fixpoint_invariant stating that any property preserved by the transf function holds for the returned solution.

The implementation of the ``extended basic block'' solver is a functor parameterized by any ordered type with a top element.

As in Kildall's solver, the state of the iteration has two components:

• A mapping from program points to values of type L.t representing the candidate solution found so far.
• A worklist of program points that remain to be considered.

The ``extended basic block'' algorithm, in pseudo-code, is as follows:

    st_wrk := the set of all points n having multiple predecessors
    st_in  := the mapping n -> L.top

    while st_wrk is not empty, do
        extract a node n from st_wrk
        compute out = transf n st_in[n]
        for each successor s of n:
            if s has only one predecessor (namely, n):
                st_in[s] := out
                st_wrk := st_wrk union {s}
            end if
        end for
    end while
    return st_in

)

Fixpoint propagate_successors (bb: bbmap) (succs: list positive) (l: L.t) (st: state) {struct succs} : state := match succs with | nil => st | s1 :: sl => if bb s1 then propagate_successors bb sl l st else propagate_successors bb sl l (mkstate (PMap.set s1 l st.(st_in)) (s1 :: st.(st_wrk))) end.

Definition step (bb: bbmap) (st: state) : result + state := match st.(st_wrk) with | nil => inl _ st.(st_in) | pc :: rem => inr _ (propagate_successors bb (successors!!!pc) (transf pc st.(st_in)!!pc) (mkstate st.(st_in) rem)) end.

(** Recognition of program points that have more than one predecessor.

The computation of the approximate solution.

Properties of predecessors and multiple-predecessors nodes

Correctness invariant

The invariant over the state is as follows:

• Points with several predecessors are mapped to L.top
• Points not in the worklist satisfy their inequations (as in Kildall's algorithm).

Correctness of the returned solution

Preservation of a property over solutions

Node sets

We now define implementations of the NODE_SET interface appropriate for forward and backward dataflow analysis. As mentioned earlier, we aim for a traversal of the CFG nodes in reverse postorder (for forward analysis) or postorder (for backward analysis). We take advantage of the following fact, valid for all CFG generated by translation from Cminor: the enumeration n-1, n-2, ..., 3, 2, 1 where n is the top CFG node is a reverse postorder traversal. Therefore, for forward analysis, we will use an implementation of NODE_SET where the pick operation selects the greatest node in the working list. For backward analysis, we will similarly pick the smallest node in the working list.