Copyright	(c) Galois Inc 2014-2018
License	BSD3
Maintainer	Luke Maurer <lukemaurer@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.Utils.RegRewrite

Contents

Main interface
Annotation monad

Description

A rewrite engine for registerized CFGs.

Synopsis

annotateCFGStmts :: forall ext u (ret :: CrucibleType) (init :: Ctx CrucibleType). 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 :: forall ext s h (ret :: CrucibleType) u. Posd (Stmt ext s) -> Rewriter ext h s ret u ()
addInternalStmt :: forall ext s h (ret :: CrucibleType) u. Stmt ext s -> Rewriter ext h s ret u ()
ifte :: forall s ext h (ret :: CrucibleType) u. Atom s BoolType -> Rewriter ext h s ret u () -> Rewriter ext h s ret u () -> Rewriter ext h s ret u ()
freshAtom :: forall (tp :: CrucibleType) ext h s (ret :: CrucibleType) u. TypeRepr tp -> Rewriter ext h s ret u (Atom s tp)

Main interface

annotateCFGStmts Source #

Arguments

:: forall ext u (ret :: CrucibleType) (init :: Ctx CrucibleType). 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

Instances details

MonadState u (Rewriter ext h s ret u) Source #
Instance details Defined in Lang.Crucible.Utils.RegRewrite Methods get :: Rewriter ext h s ret u u # put :: u -> Rewriter ext h s ret u () # state :: (u -> (a, u)) -> Rewriter ext h s ret u a #
Applicative (Rewriter ext h s ret u) Source #
Instance details 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 #
Instance details Defined in Lang.Crucible.Utils.RegRewrite Methods fmap :: (a -> b) -> Rewriter ext h s ret u a -> Rewriter ext h s ret u b # (<$) :: a -> Rewriter ext h s ret u b -> Rewriter ext h s ret u a #
Monad (Rewriter ext h s ret u) Source #
Instance details Defined in Lang.Crucible.Utils.RegRewrite Methods (>>=) :: Rewriter ext h s ret u a -> (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 b # return :: a -> Rewriter ext h s ret u a #

addStmt :: forall ext s h (ret :: CrucibleType) u. Posd (Stmt ext s) -> Rewriter ext h s ret u () Source #

Add a new statement at the current position.

addInternalStmt :: forall ext s h (ret :: CrucibleType) u. Stmt ext s -> Rewriter ext h s ret u () Source #

Add a new statement at the current position, marking it as internally generated.

ifte :: forall s ext h (ret :: CrucibleType) u. 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.

freshAtom :: forall (tp :: CrucibleType) ext h s (ret :: CrucibleType) u. TypeRepr tp -> Rewriter ext h s ret u (Atom s tp) Source #

Create a new atom with a freshly allocated id. The id will not have been used anywhere in the original CFG.