| Copyright | (c) Galois Inc 2020 |
|---|---|
| License | BSD3 |
| Maintainer | |
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Lang.Crucible.CFG.EarlyMergeLoops
Description
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.
Synopsis
- 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)
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) Source #
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.