| Copyright | (c) Galois Inc 2014-2018 |
|---|---|
| License | BSD3 |
| Maintainer | Luke Maurer <lukemaurer@galois.com> |
| Stability | provisional |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Lang.Crucible.Utils.RegRewrite
Contents
Description
A rewrite engine for registerized CFGs.
Synopsis
- annotateCFGStmts :: TraverseExt ext => u -> (forall s h. Posd (Stmt ext s) -> Rewriter ext h s ret u ()) -> (forall s h. Posd (TermStmt s ret) -> Rewriter ext h s ret u ()) -> SomeCFG ext init ret -> SomeCFG ext init ret
- data Rewriter ext h s (ret :: CrucibleType) u a
- addStmt :: Posd (Stmt ext s) -> Rewriter ext h s ret u ()
- addInternalStmt :: Stmt ext s -> Rewriter ext h s ret u ()
- ifte :: Atom s BoolType -> Rewriter ext h s ret u () -> Rewriter ext h s ret u () -> Rewriter ext h s ret u ()
- freshAtom :: TypeRepr tp -> Rewriter ext h s ret u (Atom s tp)
Main interface
Arguments
| :: TraverseExt ext | |
| => u | Initial user state |
| -> (forall s h. Posd (Stmt ext s) -> Rewriter ext h s ret u ()) | Action to run on each non-terminating statement; must explicitly add the original statement back if desired |
| -> (forall s h. Posd (TermStmt s ret) -> Rewriter ext h s ret u ()) | Action to run on each terminating statement |
| -> SomeCFG ext init ret | Graph to rewrite |
| -> SomeCFG ext init ret |
Add statements to each block in a CFG according to the given
instrumentation functions. See the Rewriter monad for the
operations provided for adding code.
Annotation monad
data Rewriter ext h s (ret :: CrucibleType) u a Source #
Monad providing operations for modifying a basic block by adding
statements and/or splicing in conditional braches. Also provides a
MonadState instance for storing user state.
Instances
| MonadState u (Rewriter ext h s ret u) Source # | |
| Applicative (Rewriter ext h s ret u) Source # | |
Defined in Lang.Crucible.Utils.RegRewrite Methods pure :: a -> Rewriter ext h s ret u a # (<*>) :: Rewriter ext h s ret u (a -> b) -> Rewriter ext h s ret u a -> Rewriter ext h s ret u b # liftA2 :: (a -> b -> c) -> Rewriter ext h s ret u a -> Rewriter ext h s ret u b -> Rewriter ext h s ret u c # (*>) :: Rewriter ext h s ret u a -> Rewriter ext h s ret u b -> Rewriter ext h s ret u b # (<*) :: Rewriter ext h s ret u a -> Rewriter ext h s ret u b -> Rewriter ext h s ret u a # | |
| Functor (Rewriter ext h s ret u) Source # | |
| Monad (Rewriter ext h s ret u) Source # | |
addStmt :: Posd (Stmt ext s) -> Rewriter ext h s ret u () Source #
Add a new statement at the current position.
addInternalStmt :: Stmt ext s -> Rewriter ext h s ret u () Source #
Add a new statement at the current position, marking it as internally generated.
ifte :: Atom s BoolType -> Rewriter ext h s ret u () -> Rewriter ext h s ret u () -> Rewriter ext h s ret u () Source #
Add a conditional at the current position. This will cause the current block to end and new blocks to be generated for the two branches and the remaining statements in the original block.