Copyright	(c) Galois Inc 2016
License	BSD3
Maintainer	Simon Winwood <sjw@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.Utils.CoreRewrite

Description

Synopsis

annotateCFGStmts :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). TraverseExt ext => (forall (cin :: Ctx CrucibleType) (cout :: Ctx CrucibleType). Some (BlockID blocks) -> Size cout -> Stmt ext cin cout -> Maybe (StmtSeq ext blocks UnitType cout)) -> (forall (ctx' :: Ctx CrucibleType). Some (BlockID blocks) -> Size ctx' -> TermStmt blocks ret ctx' -> Maybe (StmtSeq ext blocks UnitType ctx')) -> CFG ext blocks ctx ret -> CFG ext blocks ctx ret

Documentation

annotateCFGStmts Source #

Arguments

:: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) (ctx :: Ctx CrucibleType). TraverseExt ext
=> (forall (cin :: Ctx CrucibleType) (cout :: Ctx CrucibleType). Some (BlockID blocks) -> Size cout -> Stmt ext cin cout -> Maybe (StmtSeq ext blocks UnitType cout))	This is the annotation function. The resulting `StmtSeq` gets spliced in after the statement so that they can inspect the result if desired. The terminal statement is ignored.
-> (forall (ctx' :: Ctx CrucibleType). Some (BlockID blocks) -> Size ctx' -> TermStmt blocks ret ctx' -> Maybe (StmtSeq ext blocks UnitType ctx'))	As above but for the final term stmt, where the annotation will be _before_ the term stmt.
-> CFG ext blocks ctx ret
-> CFG ext blocks ctx ret

This function walks through all the blocks in the CFG calling fS on each Stmt and fT on each TermStmt. These functions return a possible annotaition statement (which has access to the result of the statement, if any) along with a context diff which describes any new variables.