Lang.Crucible.CFG.EarlyMergeLoops

This modules exposes a transformation that attempts to ensure that loop branches are post-dominated by nodes in the loop.

The module is organized into 3 main components: 1. An analysis that computes the natural loops of a CFG; 2. An analysis that inserts postdominators into loops that have "early exits" (and hence have postdominators outside the loop); 3. A "fixup" pass that ensures that, in the transformed CFG, all values are well defined along all (new) paths.

Documentation

earlyMergeLoops :: (TraverseExt ext, Monad m, Show (CFG ext s init ret)) => NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret)

This is the main pass that attempts to optimize early exits in the loops in a CFG. In particular, this transformation ensures that the postdominator of the loop header is a member of the loop.

Given a natural loop, its members are a set of blocks bs. Let the exit edges be the edges from some block b in bs to either the loop header or a block not in bs.

Let (i, j) be such an exit edge.This transofrmation inserts a new block r such that in the transformed cfg there is an edge (i, r) and an edge (r, j). Moreover, the transformation ensures that [i, r, j'] is not feasible for j' != j. This works by setting a "destination" register d := j in each block i for each exit edge (i, j), and switching on the value of d in the block r.